Proceedings of the Workshop on Tools and Algorithms for the

Construction and Analysis of Systems (Aarhus, Denmark, 19–20 May, 1995)

May 1995

This document is also available as PostScript, DVI, Text.

References

[MN] Abstract, PostScript, DVI.

Olaf Müller and Tobias Nipkow. Combining model checking and deduction for I/O-automata. In TACAS, pages 1–12. vi+334pp.

[LSW] Abstract, PostScript.

Kim G. Larsen, Bernhard Steffen, and Carsten Weise. A constraint oriented proof methodology based on modal transition systems. In TACAS, pages 13–28. vi+334pp.

[HH] Abstract, PostScript, DVI.

Tom Henzinger and Pei-Hsin Ho. HyTech: The Cornell Hybrid Technology Tool. In TACAS, pages 29–43. vi+334pp.

[Mad] Abstract, PostScript, DVI.

Angelika Mader. The modal μ-calculus, model checking, equation systems and Gauß elimination. In TACAS, pages 44–57. vi+334pp.

[GJJ+] Abstract, PostScript.

Jesper G. Henriksen, Ole J. L. Jensen, Michael E. Jørgensen, Nils Klarlund, Robert Paige, Theis Rauhe, and Anders B. Sandholm. MONA: Monadic second-order logic in practice. In TACAS, pages 58–73. vi+334pp.

[MP] Abstract, PostScript, DVI.

Oliver Matz and Andreas Potthoff. Computing small nondeterministic finite automata. In TACAS, pages 74–88. vi+334pp.

[EL] Abstract, PostScript, DVI.

Uffe H. Engberg and Kim S. Larsen. Efficient simplification of bisimulation formulas. In TACAS, pages 89–103. vi+334pp.

[Lin] Abstract, PostScript.

Huimin Lin. On implementing unique fixpoint induction for value-passing processes. In TACAS, pages 104–118. vi+334pp.

[BP] Abstract, PostScript, DVI. Doeko J.B. Bosscher and Alban Ponse. Translating a process algebra with symbolic data values to linear format. In TACAS, pages 119–130. vi+334pp.

[CHP] Abstract, PostScript. Michel Charpentier, Gérard Padiou, and Abdellah El Hadri. A UNITYbased algorithm design assistant. In TACAS, pages 131–145. vi+334pp.

[Mat] Abstract, PostScript, DVI. Seán Matthews. Implementing F S_{0} in Isabelle: adding structure at the metalevel. In TACAS, pages 146–158. vi+334pp.

[BF] Abstract, PostScript. J.P. Bodeveix and M. Filali. A framework for parallel program refinement. In TACAS, pages 159–173. vi+334pp.

[Che] Abstract, PostScript, DVI. Boutheina Chetali. Formal verification of concurrent program using the Larch Prover. In TACAS, pages 174–186. vi+334pp.

[RGG+] Abstract, PostScript, DVI. Andrew W. Roscoe, Poul H.B. Gardiner, Michael H. Goldsmith, Jason R. Hulance, David M. Jackson, and J. Bryan Scattergood. Hierarchical compression for model-checking CSP or how to check 10^{20} dining philosophers for deadlock. In TACAS, pages 187–200. vi+334pp.

[CMS] Abstract, PostScript, DVI. Rance Cleaveland, Eric Madelaine, and Steve Sims. A front-end generator for verification tools. In TACAS, pages 201–215. vi+334pp.

[GR] Abstract, PostScript, DVI. Pascal Gribomont and Didier Rossetto. CAVEAT: technique and tool for computer aided verification and transformation. In TACAS, pages 216–229. vi+334pp.

[DHG] Abstract, PostScript, DVI. Werner Damm, Hardi Hungar, and Orne Grumberg. What if model checking must be truly symbolic? In TACAS, pages 230–244. vi+334pp.

[Tof] Abstract, PostScript, DVI. Chris Tofts. Analytic and locally approximate solutions to properties of probabilistic processes. In TACAS, pages 245–259. vi+334pp.

[FFGI] Abstract, PostScript, DVI. Nicoletta De Francesco, Alessandro Fantechi, Stefania Gnesi, and Paola Inverardi. Model checking of non-finite state processes by finite approximation. In TACAS, pages 260–274. vi+334pp.

[BR] Abstract, PostScript, DVI. Jürgen Bohn and Stephan Rössig. On automatic and interactive design of communicating systems. In TACAS, pages 275–289. vi+334pp.

[MK] Abstract, PostScript, DVI. Arnulf Mester and Heiko Krumm. Composition and refinement mapping based construction of distributed applications. In TACAS, pages 290–303. vi+334pp.

[Jan] Abstract, PostScript, DVI.

Wil Janssen. Layers as knowledge transitions in the design of distributed systems. In TACAS, pages 304–318. vi+334pp.

[KSV] Abstract, PostScript.

Jens Knoop, Bernhard Steffen, and Jürgen Vollmer. Parallelism for free: Efficient and optimal bitvector analyses for parallel programs. In TACAS, pages 319–333. vi+334pp.

[NS-95-2] Uffe H. Engberg, Kim G. Larsen, and Arne Skou, editors. Proceedings of the Workshop on Tools and Algorithms for The Construction and Analysis of Systems, TACAS (Aarhus, Denmark, 19–20 May, 1995), May 1995. vi+334pp.