Abstract is missing.
- PrefaceEdmund M. Clarke, Robert P. Kurshan.
- Temporal Logic Model Checking: Two Techniques for Avoiding the State Explosion ProblemEdmund M. Clarke. 1-2
- Automatic Verification of Extensions of Hardware DescriptionsHans Eveking. 3-14
- Using Partial-Order Semantics to Avoid the State Explosion Problem in Asynchronous SystemsDavid K. Probst, Hon Fung Li. 15-24
- A Stubborn Attack on State ExplosionAntti Valmari. 25-42
- PAPETRI: Environment for the Analysis of PETRI NetsGérard Berthelot, Colette Johnen, Laure Petrucci. 43-56
- Compositional Minimization of Finite State SystemsSusanne Graf, Bernhard Steffen. 57-74
- Verifying Temporal Properties of Sequential Machines without Building Their State DiagramsOlivier Coudert, Jean Christophe Madre, Christian Berthet. 75-84
- Minimal Model GenerationAhmed Bouajjani, Jean-Claude Fernandez, Nicolas Halbwachs. 85-92
- Verifying Liveness Properties by Verifying Safety PropertiesJerry R. Burch. 93-102
- Extension of the Karp and Miller Procedure to LOTOS SpecificationsMichel Barbeau, Gregor von Bochmann. 103-120
- Formal Verification of Digital Circuits Using Symbolic Ternary System ModelsRandal E. Bryant, Carl-Johan H. Seger. 121-146
- An Algebra for Delay-Insensitive CircuitsMark B. Josephs, Jan Tijmen Udding. 147-176
- Synthesizing Processes and Schedulers from Temporal SpecificationsHoward Wong-Toi, David L. Dill. 177-186
- Verification of Multiprocessor Cache Protocol Using Simulation Relations and Higher-Order LogicPaul Loewenstein, David L. Dill. 187-206
- Memory Efficient Algorithms for the Verification of Temporal PropertiesCostas Courcoubetis, Moshe Y. Vardi, Pierre Wolper, Mihalis Yannakakis. 207-218
- Vectorized Model Checking for Computation Tree LogicHiromi Hiraishi, Shintaro Meki, Kiyoharu Hamaguchi. 219-230
- On Some Implementation of Optimal SimulationsRyszard Janicki, Maciej Koutny. 231-274
- Finiteness Conditions and Structural Construction of Automata for All Process AlgebrasEric Madelaine, Didier Vergamini. 275-292
- A Computation Theory and Implementation of Sequential Hardware EquivalenceCarl Pixley. 293-320
- Using Partial Orders to Improve Automatic Verification MethodsPatrice Godefroid. 321-340
- A Context Dependent Equivalence Relation between Kripke StructuresBernhard Josko. 341-358
- The Modular Framework of Computer-Aided VerificationGil Shurek, Orna Grumberg. 359-380
- Tool Support for the Refinement CalculusDavid A. Carrington, Kenneth Arthur Robinson. 381-394
- A Unified Approach to the Deadlock Detection Problem in Networks of Communicating Finite State MachinesWuxu Peng, S. Purushothaman Iyer. 395-404
- A Computer-Aided Verification Tool for Finite State Controller SystemsMark Bickford, Mandayam K. Srivas. 405-440
- Program Verification by Symbolic Execution of Hyperfinite Ideal MachinesJames M. Morris, Mark Howard. 441-462
- On Automatically Distinguishing Inequivalent ProcessesRance Cleaveland. 463-476
- Auto/AutographValérie Roy, Robert de Simone. 477-492
- A Data Path Verifier for Register Transfer Level Using Temporal Logic Language TokioHiroshi Nakamura, Yuji Kukimoto, Masahiro Fujita, Hidehiko Tanaka. 493-504
- Model Checking and Graph Theory in Sequential ATPGPaolo Camurati, Marco Gilli, Paolo Prinetto, Matteo Sonza Reorda. 505-518
- Compositional Design and Verification of Communication Protocols, Using Labelled PETRI NetsJean Christophe Lloret, Pierre Azéma, François Vernadat. 519-534
- Liveness Analysis and the Automatic Generation of Concurrent ProgramsUgo A. Buy, Robert Moll. 535-550
- Branching Time Regular Temporal Logic for Model Checking with Linear Time ComplexityKiyoharu Hamaguchi, Hiromi Hiraishi, Shuzo Yajima. 551-564
- Issues Arising in the Analysis of L.0Linda A. Ness. 565-576
- Automated RTL Verification Based on Predicate CalculusMichel Langevin. 577-590
- The Algebraic Feedback Product of Automata. A State Machine Based Model of Concurrent SystemsVictor Yodaiken. 591-614
- Results on the Interface between Formal Verification and ATPGHyunwoo Cho, Gary D. Hachtel, Seh-Woong Jeong, Bernard Plessier, Eric M. Schwarz, Fabio Somenzi. 615