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.


                                       1





[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
           UNITY-based algorithm  design assistant. In  TACAS, pages 131--145.
           vi+334pp.

[Mat]      Abstract, PostScript, DVI.
           Seán Matthews.  Implementing FS0 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
           1020 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.


                                       2





           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.
























                                       3