Abstract is missing.
- Pæan to Zohar MannaNachum Dershowitz. 1-10 [doi]
- A Logic of Object-Oriented ProgramsMartín Abadi, K. Rustan M. Leino. 11-41 [doi]
- Formal Analysis of Hierarchical State MachinesRajeev Alur. 42-66 [doi]
- Abstraction as the Key for Invariant VerificationSaddek Bensalem, Susanne Graf, Yassine Lakhnech. 67-99 [doi]
- Domain Engineering: a Radical Innovation for Software and Systems Engineering? A Biased AccountDines Bjørner. 100-144 [doi]
- The ASM Ground Model Method as a Foundation for Requirements EngineeringEgon Börger. 145-160 [doi]
- A Functional Calculus for Specification and Verification of Nondeterministic Interactive SystemsManfred Broy. 161-181 [doi]
- Notes from the Logbook of a Proof-Checker s ProjectDomenico Cantone, Eugenio G. Omodeo, Jacob T. Schwartz, Pietro Ursino. 182-207 [doi]
- Counterexamples Revisited: Principles, Algorithms, ApplicationsEdmund M. Clarke, Helmut Veith. 208-224 [doi]
- Easy Intruder DeductionsHubert Comon-Lundh, Ralf Treinen. 225-242 [doi]
- Verification by Abstract InterpretationPatrick Cousot. 243-268 [doi]
- Game Models for Open SystemsLuca de Alfaro. 269-289 [doi]
- A Compositional Operational Semantics for Java::MT::Erika Ábrahám, Frank S. de Boer, Willem P. de Roever, Martin Steffen. 290-303 [doi]
- Bounded FairnessNachum Dershowitz, D. N. Jayasimha, Seungjoon Park. 304-317 [doi]
- Efficient Boundary Values Generation in General Metric Spaces for Software Component TestingAlfredo Ferro, Rosalba Giugno, Alfredo Pulvirenti. 318-331 [doi]
- Extreme Model CheckingThomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Marco A. A. Sanvido. 332-358 [doi]
- Automata MistaGérard P. Huet. 359-372 [doi]
- Aspect Validation Using Model CheckingShmuel Katz, Marcelo Sihman. 373-394 [doi]
- Qualitative Theorem Proving in Linear ConstraintsVijay Chandru, Jean-Louis Lassez. 395-406 [doi]
- Some Institutional Requirements for Temporal Reasoning on Dynamic Reconfiguration of Component Based SystemsNazareno Aguirre, T. S. E. Maibaum. 407-435 [doi]
- A Formal Basis for Reasoning on Programmable QoSRocco De Nicola, Gian Luigi Ferrari, Ugo Montanari, Rosario Pugliese, Emilio Tuosto. 436-479 [doi]
- A Hierarchical Completeness Proof for Propositional Temporal LogicBen C. Moszkowski. 480-523 [doi]
- Computational Proof as Experiment: Probabilistic Algorithms from a Thermodynamic PerspectiveKrishna V. Palem. 524-547 [doi]
- Unit Checking: Symbolic Model Checking for a Unit of CodeElsa L. Gunter, Doron Peled. 548-567 [doi]
- Colimits for Concurrent CollectorsDusko Pavlovic, Peter Pepper, Douglas R. Smith. 568-597 [doi]
- TLPVS: A PVS-Based LTL Verification SystemAmir Pnueli, Tamarah Arons. 598-625 [doi]
- Binary Extensions of S1S and the Composition MethodEnrico Marzano, Angelo Montanari, Alberto Policriti. 626-644 [doi]
- Deriving Effcient Graph AlgorithmsJohn H. Reif, William L. Scherlis. 645-681 [doi]
- Petri Net Analysis Using Invariant GenerationSriram Sankaranarayanan, Henny Sipma, Zohar Manna. 682-701 [doi]
- Fair Equivalence RelationsOrna Kupferman, Nir Piterman, Moshe Y. Vardi. 702-732 [doi]
- Digital Algebra and CircuitsJean Vuillemin. 733-746 [doi]
- Program Synthesis for Multi-agent Question AnsweringRichard J. Waldinger, Peter Jarvis, Jennifer L. Dungan. 747-761 [doi]
- Combining Sets with ElementsCalogero G. Zarba. 762-782 [doi]