Abstract is missing.
- What Are We Trying to Prove? Reflections on Experiences with Proof-Carrying CodePeter Lee. 1 [doi]
- Automatic Abstraction without CounterexamplesKenneth L. McMillan, Nina Amla. 2-17 [doi]
- Bounded Model Checking for Past LTLMarco Benedetti, Alessandro Cimatti. 18-33 [doi]
- Experimental Analysis of Different Techniques for Bounded Model CheckingNina Amla, Robert P. Kurshan, Kenneth L. McMillan, Ricardo Medel. 34-48 [doi]
- On the Universal and Existential Fragments of the µ-CalculusThomas A. Henzinger, Orna Kupferman, Rupak Majumdar. 49-64 [doi]
- Resets vs. Aborts in Linear Temporal LogicRoy Armoni, Doron Bustan, Orna Kupferman, Moshe Y. Vardi. 65-80 [doi]
- A Generic On-the-Fly Solver for Alternation-Free Boolean Equation SystemsRadu Mateescu. 81-96 [doi]
- Decidability of Invariant Validation for Paramaterized SystemsPascal Fontaine, E. Pascal Gribomont. 97-112 [doi]
- Verification and Improvement of the Sliding Window ProtocolDmitri Chkliaev, Jozef Hooman, Erik P. de Vink. 113-127 [doi]
- Simple Representative Instantiations for Multicast ProtocolsJavier Esparza, Monika Maidl. 128-143 [doi]
- Rapid Parameterized Model Checking of Snoopy Cache Coherence ProtocolsE. Allen Emerson, Vineet Kahlon. 144-159 [doi]
- Proof-Like Counter-ExamplesArie Gurfinkel, Marsha Chechik. 160-175 [doi]
- Multiple-Counterexample Guided Iterative Abstraction Refinement: An Industrial EvaluationMarcelo Glusman, Gila Kamhi, Sela Mador-Haim, Ranan Fraer, Moshe Y. Vardi. 176-191 [doi]
- Verification of Hybrid Systems Based on Counterexample-Guided Abstraction RefinementEdmund M. Clarke, Ansgar Fehnker, Zhi Han, Bruce H. Krogh, Olaf Stursberg, Michael Theobald. 192-207 [doi]
- Counter-Example Guided Predicate Abstraction of Hybrid SystemsRajeev Alur, Thao Dang, Franjo Ivancic. 208-223 [doi]
- Schedulability Analysis Using Two ClocksElena Fersman, Leonid Mokrushin, Paul Pettersson, Wang Yi. 224-239 [doi]
- On Optimal Scheduling under UncertaintyYasmina Abdeddaïm, Eugene Asarin, Oded Maler. 240-253 [doi]
- Static Guard Analysis in Timed Automata VerificationGerd Behrmann, Patricia Bouyer, Emmanuel Fleury, Kim Guldstrand Larsen. 254-277 [doi]
- Verics: A Tool for Verifying Timed Automata and Estelle SpecificationsPiotr Dembinski, Agata Janowska, Pawel Janowski, Wojciech Penczek, Agata Pólrola, Maciej Szreter, Bozena Wozna, Andrzej Zbrzezny. 278-283 [doi]
- A New Knowledge Representation Strategy for Cryptographic Protocol AnalysisIvan Cibrario Bertolotti, Luca Durante, Riccardo Sisto, Adriano Valenzano. 284-298 [doi]
- Pattern-Based Abstraction for Verifying Secrecy in ProtocolsLiana Bozga, Yassine Lakhnech, Michaël Périn. 299-314 [doi]
- Compositional Analysis for Verification of Parameterized SystemsSamik Basu, C. R. Ramakrishnan. 315-330 [doi]
- Learning Assumptions for Compositional VerificationJamieson M. Cobleigh, Dimitra Giannakopoulou, Corina S. Pasareanu. 331-346 [doi]
- Automated Module CompositionStavros Tripakis. 347-362 [doi]
- Modular Strategies for Recursive Game GraphsRajeev Alur, Salvatore La Torre, P. Madhusudan. 363-378 [doi]
- Saturation UnboundGianfranco Ciardo, Robert M. Marmorstein, Radu Siminiceanu. 379-393 [doi]
- Construction of Efficient BDDs for Bounded Arithmetic ConstraintsConstantinos Bartzis, Tevfik Bultan. 394-408 [doi]
- Modeling and Analysis of Power-Aware SystemsOleg Sokolsky, Anna Philippou, Insup Lee, Kyriakos Christou. 409-425 [doi]
- A Set of Performance and Dependability Analysis Components for CADPHolger Hermanns, Christophe Joubert. 425-430 [doi]
- The Integrated CWB-NC/PIOATool for Functional Verification and Performance Analysis of Concurrent SystemsDezhuang Zhang, Rance Cleaveland, Eugene W. Stark. 431-436 [doi]
- BANANA - A Tool for Boundary Ambients Nesting ANAlysisChiara Braghin, Agostino Cortesi, Stefano Filippone, Riccardo Focardi, Flaminia L. Luccio, Carla Piazza. 437-441 [doi]
- State Class Constructions for Branching Analysis of Time Petri NetsBernard Berthomieu, François Vernadat. 442-457 [doi]
- Branching Processes of High-Level Petri NetsVictor Khomenko, Maciej Koutny. 458-472 [doi]
- Using Petri Net Invariants in State Space ConstructionKarsten Schmidt 0004. 473-488 [doi]
- Optimistic Synchronization-Based State-Space ReductionScott D. Stoller, Ernie Cohen. 489-504 [doi]
- Checking Properties of Heap-Manipulating Procedures with a Constraint SolverMandana Vaziri, Daniel Jackson. 505-520 [doi]
- An Online Proof-Producing Decision Procedure for Mixed-Integer Linear ArithmeticSergey Berezin, Vijay Ganesh, David L. Dill. 521-536 [doi]
- Strategies for Combining Decision ProceduresSylvain Conchon, Sava Krstic. 537-552 [doi]
- Generalized Symbolic Execution for Model Checking and TestingSarfraz Khurshid, Corina S. Pasareanu, Willem Visser. 553-568 [doi]
- Code-Based Test Generation for Validation of Functional Processor DescriptionsFabrice Baray, Philippe Codognet, Daniel Diaz, Henri Michel. 569-584 [doi]
- Large State Space VisualizationJan Friso Groote, Frank van Ham. 585-590 [doi]
- Automatic Test Generation with AGATHACéline Bigot, Alain Faivre, Jean-Pierre Gallois, Arnault Lapitre, David Lugato, Jean-Yves Pierron, Nicolas Rapin. 591-596 [doi]
- LTSA-MSC: Tool Support for Behaviour Model Elaboration Using Implied ScenariosSebastián Uchitel, Robert Chatley, Jeff Kramer, Jeff Magee. 597-601 [doi]