Computer-Aided Verification (CAV) '96 is the eighth annual conference in a series dedicated to the advancement of the theory and practice of computer-assisted formal analysis methods for software and hardware systems. The conference covers the spectrum from theoretical results to concrete applications, with an emphasis on verification tools and the algorithms and techniques that are needed for their implementation. The contributed presentations at CAV '96 include 32 regular papers and 20 short presentations on tools and case studies. The program also includes invited lectures by Michael Rabin and Bill Roscoe, FLoC plenary addresses by Robin Milner and John Rushby, an after-dinner speech by Amir Pnueli, and a morning session with six invited talks by representatives from industry. Student registration at CAV '96 is subsidized due to financial support from Cadence Berkeley Labs, Lucent Technologies, and Siemens Corporate Research and Development. The proceedings of CAV '96 are published by Springer-Verlag.
Program Chairs: R. Alur, T.A. Henzinger.
Program Committee: R.K. Brayton, K. Cerans, D.L. Dill, E.A. Emerson, O. Grumberg, K.G. Larsen, D.E. Long, K.L. McMillan, A.K. Mok, D. Peled, A. Pnueli, C.-J.H. Seger, J. Sifakis, S.A. Smolka, M.K. Srivas, W. Thomas, F. Vaandrager, M.Y. Vardi, and P. Wolper.
Steering Committee: E.M. Clarke, R.P. Kurshan, A. Pnueli, J. Sifakis.
Email: cav96@research.att.com
FLoC Plenary Session: 20:00-21:30. Chair: M.Y. Vardi.
Calculi for Interactions
R. Milner
(Cambridge University, United Kingdom)
Formal methods in the IC industry: trends and directions
J. Harlow & P. Verhofstadt
(Semiconductor Research Corporation, USA)
From wired homes to automated highways: a perspective on verification in the 21st century
P. Scaglia
(Cadence Berkeley Labs, USA)
Coffee Break: 9:50-10:15.
Industrial Session II: 10:15-11:05. Chair: D.L. Dill.
Formal verification at Siemens: achievements, problems, trends
W. Büttner
(Siemens Corporate Research and Development, Germany)
User experiences with FormalCheck
G. de Palma
(Lucent Technologies, USA)
Coffee Break: 11:05-11:30.
Industrial Session III: 11:30-12:20. Chair: C.-J.H. Seger.
Formal and informal functional verification in a commercial environment
C. Pixley
(Motorola, USA)
Model checking at work
S. Ben-David
(IBM Haifa Research Laboratory, Israel)
Lunch Break: 12:20-14:00.
Session 1A: 14:00-15:15. Chair: D.E. Long.
Symbolic verification of communication protocols with infinite state spaces using QDDs
B. Boigelot
(Université de Liège, Belgium) &
P. Godefroid
(Bell Labs, USA)
A conjunctively decomposed boolean representation for symbolic model checking
K.L. McMillan
(Cadence Berkeley Labs, USA)
Symbolic model checking using algebraic geometry
G.S. Avrunin
(University of Massachusetts at Amherst, USA)
Session 1B: 15:15-15:45. Chair: D.E. Long.
The state of SPIN
G.J. Holzmann & D. Peled
(Bell Labs, USA)
The Murphi verification system
D.L. Dill, A.J. Hu, C.H. Yang, A. Drexler, R. Melton, S. Park, C.N. Ip & U. Stern
(Stanford University, USA)
Coffee Break: 15:45-16:10.
Session 2A: 16:10-17:00. Chair: K.G. Larsen.
A partition refinement algorithm for the Pi-calculus
M. Pistore
(University of Pisa, Italy) &
D. Sangiorgi
(INRIA Sophia-Antipolis, France)
Polynomial-time algorithms for testing probabilistic bisimulation and simulation
C. Baier
(Universität Mannheim, Germany)
Session 2B: 17:00-18:00. Chair: K.G. Larsen.
The NCSU Concurrency Workbench
R. Cleaveland & S.T. Sims
(North Carolina State University, USA)
The Concurrency Factory: an integrated environment for specification, simulation, verification, and implementation of real-time concurrent systems
R. Cleaveland
(North Carolina State University, USA),
P.M. Lewis, S.A. Smolka & O. Sokolsky
(SUNY at Stony Brook, USA)
XVERSA: an integrated graphical and textual toolset for the specification and analysis of resource-bound real-time systems
D. Clarke, H. Ben-Abdallah, I. Lee, H. Xie
(University of Pennsylvania, USA) &
O. Sokolsky
(Computer Command and Control Company, USA)
EVP: integration of FDTs for analysis and verification of communication protocols
P.M. Gómez & J.M.T. Linero
(Universidad de Málaga, Spain)
Reception and Business Meeting: 20:00-22:00.
Randomization and protocol verification
M.O. Rabin
(Harvard University, USA, and Hebrew University, Israel)
Coffee Break: 10:15-10:40.
Session 3: 10:40-12:20. Chair: W. Thomas.
Pushdown processes: games and model checking
I. Walukiewicz
(Aarhus University, Denmark)
Module checking
O. Kupferman
(Bell Labs, USA) &
M.Y. Vardi
(Rice University, USA)
Automatic verification of parameterized synchronous systems
E.A. Emerson & K.S. Namjoshi
(The University of Texas at Austin, USA)
HORNSAT, model checking, verification, and games
S.K. Shukla, H.B. Hunt III & D.J. Rosenkrantz
(SUNY at Albany, USA)
Lunch Break: 12:20-14:00.
Session 4A: 14:00-15:15. Chair: K.L. McMillan.
Verifying the SRT division algorithm using theorem proving techniques
E.M. Clarke
(Carnegie Mellon University, USA),
S.M. German
(IBM T.J. Watson Research Center, USA) &
X. Zhao
(Carnegie Mellon University, USA)
Modular verification of SRT division
H. Rueß, M.K. Srivas & N. Shankar
(SRI International, USA)
Mechanically verifying a family of multiplier circuits
D. Kapur & M. Subramaniam
(SUNY at Albany, USA)
Session 4B: 15:15-15:45. Chair: K.L. McMillan.
PVS: combining specification, proof checking, and model checking
S. Owre, S. Rajan, J.M. Rushby, N. Shankar & M.K. Srivas
(SRI International, USA)
STeP: deductive-algorithmic verification of reactive and real-time systems
N. Bjørner, A. Browne, E. Chang, M. Colón, A. Kapur, Z. Manna, H.B. Sipma & T.E. Uribe
(Stanford University, USA)
Coffee Break: 15:45-16:10.
Session 5A: 16:10-17:00. Chair: M.K. Srivas.
Verifying systems with replicated components in Murphi
C.N. Ip & D.L. Dill
(Stanford University, USA)
Verification of arithmetic circuits by comparing two similar circuits
M. Fujita
(Fujitsu Laboratories, USA)
Session 5B: 17:00-18:00. Chair: M.K. Srivas.
Symbolic model checking
E.M. Clarke
(Carnegie Mellon University, USA),
K.L. McMillan
(Cadence Berkeley Labs, USA),
S. Campos & V. Hartonas-Garmhausen
(Carnegie Mellon University, USA)
COSPAN
R.H. Hardin
(Bell Labs, USA),
Z. Har'El
(The Technion, Israel) &
R.P. Kurshan
(Bell Labs, USA)
VIS: a system for verification and synthesis
R.K. Brayton, A. Sangiovanni-Vincentelli, A. Aziz, S.-T. Cheng, S. Edwards, S. Khatri, Y. Kukimoto, S. Qadeer, R.K. Ranjan, T.R. Shiple, G. Swamy, T. Villa
(University of California at Berkeley, USA),
G.D. Hachtel, F. Somenzi, A. Pardo
(University of Colorado at Boulder, USA) &
S. Sarwary
(Lattice Semiconductor, USA)
MDG tools for the verification of RTL designs
Z. Zhou, X. Song
(Université de Montréal, Canada),
F. Corella
(Hewlett-Packard, USA),
M. Langevin
(GMD, Germany),
E. Cerny & S. Tahar
(Université de Montréal, Canada)
Joint Banquet with CADE: 18:30-23:00. Dinner speech by Amir Pnueli (Weizmann Institute, Israel), ``The Potential and Sensible Scopes of Formal Methods.''
Automated Deduction and Formal Methods
J. Rushby
(SRI International, USA)
Coffee Break: 10:15-10:40.
Session 6: 10:40-12:20. Chair: E.A. Emerson.
A platform for combining deductive with algorithmic verification
A. Pnueli & E. Shahar
(Weizmann Institute, Israel)
Verifying invariants using theorem proving
S. Graf & H. Saidi
(VERIMAG, France)
Deductive model checking
H.B. Sipma, T.E. Uribe & Z. Manna
(Stanford University, USA)
Automated verification by induction with associative-commutative operators
N. Berregeb, A. Bouhoula & M. Rusinowitch
(INRIA Lorraine, France)
Lunch Break: 12:20-14:00.
Session 7A: 14:00-15:15. Chair: S.A. Smolka.
Analysis of timed systems based on time-abstracting bisimulations
S. Tripakis & S. Yovine
(VERIMAG, France)
Verification of an audio protocol with bus collision using UPPAAL
J. Bengtsson
(Uppsala University, Sweden),
D. Griffioen
(CWI, The Netherlands),
K. Kristoffersen, K.G. Larsen
(Aalborg University, Denmark),
F. Larsson, P. Pettersson & W. Yi
(Uppsala University, Sweden)
Selective quantitative analysis and interval model checking: verifying different facets of a system
S. Campos, E.M. Clarke
(Carnegie Mellon University, USA) &
O. Grumberg
(The Technion, Israel)
Session 7B: 15:15-15:45. Chair: S.A. Smolka.
CADP (CÆSAR/ALDÉBARAN Distribution Package): a protocol validation and verification toolbox
J.-C. Fernandez, H. Garavel, A. Kerbrat, R. Mateescu, L. Mounier & M. Sighireanu
(INRIA/VERIMAG, France)
The FC2Tools set
A. Bouali, A. Ressouche, V. Roy & R. de Simone
(INRIA Sophia-Antipolis, France)
Coffee Break: 15:45-16:10.
Session 8A: 16:10-17:00. Chair: F. Vaandrager.
Verifying continuous-time Markov chains
A. Aziz
(The University of Texas at Austin, USA),
K. Sanwal
(Bell Labs, USA),
V. Singhal
(Cadence Berkeley Labs, USA) &
R.K. Brayton
(University of California at Berkeley, USA)
Verifying safety properties of differential equations
M.R. Greenstreet
(University of British Columbia, Canada)
Session 8B: 17:00-18:00. Chair: F. Vaandrager.
The real-time graphical interval logic toolset
L.E. Moser, P.M. Melliar-Smith, Y.S. Ramakrishna, G. Kutty & L.K. Dillon
(University of California at Santa Barbara, USA)
The METAFrame'95 environment
B. Steffen, T. Margaria, A. Claßen & V. Braun
(Universität Passau, Germany)
Verification support environment
F. Koob, M. Ullmann & S. Wittmann
(Bundesamt für Sicherheit in der Informationstechnik, Germany)
Marrella: a tool for simulation and verification
D. Ambroise
(Université de Caen, France) &
B. Rozoy
(Université de Paris XI, France)
Refinement-based model checking
A.W. Roscoe
(Oxford University, United Kingdom)
Coffee Break: 10:15-10:40.
Session 9: 10:40-12:20. Chair: P. Wolper.
Temporal verification by diagram transformations
L. de Alfaro & Z. Manna
(Stanford University, USA)
Protocol verification by aggregation of distributed actions
S. Park & D.L. Dill
(Stanford University, USA)
Atomicity refinement and trace reduction theorems
E.P. Gribomont
(Université de Liège, Belgium)
Powerful techniques for the automatic generation of invariants
S. Bensalem
(VERIMAG, France),
Y. Lakhnech
(Christian-Albrechts-Universität Kiel, Germany) &
H. Saidi
(VERIMAG, France)
Lunch Break: 12:20-14:00.
Session 10A: 14:00-15:15. Chair: D. Peled.
Saving space by fully exploiting invisible transitions
H. Miller & S. Katz
(The Technion, Israel)
Model checking local properties of distributed systems
F. Wallner & J. Esparza
(Technische Universität München, Germany)
Using on-the-fly verification techniques for the generation of conformance test suites
J.-C. Fernandez
(INRIA/VERIMAG, France),
C. Jard
(CNRS Rennes, France),
T. Jéron
(INRIA/IRISA, France) &
G. Viho
(Université de Rennes I, France)
Session 10B: 15:15-15:45. Chair: D. Peled.
Verifying the safety of a practical concurrent garbage collector
G. Gonthier
(INRIA Rocquencourt, France)
Verification by behavior abstraction: a case study of service interaction detection in intelligent telephone networks
C. Capellmann
(Deutsche Telekom, Germany),
R. Demant, R. Galvez-Estrada, F. Fatahi-Vanani, U. Nitsche & P. Ochsenschläger
(GMD, Germany)
Coffee Break: 15:45-16:10.
Session 11: 16:10-17:00. Chair: O. Grumberg.
Automatic translation of natural-language system specifications into temporal logic
R. Nelken
(Tel-Aviv University, Israel) &
N. Francez
(The Technion, Israel)
Verification of fair transition systems
O. Kupferman
(Bell Labs, USA) &
M.Y. Vardi
(Rice University, USA)
![[Next]](nextbutton.gif)
![[Prev]](prevbutton.gif)
![[Contents]](contentbutton.gif)
