Abstract is missing.
- Branching vs. Linear Time: Final ShowdownMoshe Y. Vardi. 1-22 [doi]
- Propositional ReasoningMichael P. Fourman. 23 [doi]
- Language Containment Checking with Nondeterministic BDDsBernd Finkbeiner. 24-38 [doi]
- Satisfiability Checking Using Boolean Expression DiagramsPoul Frederick Williams, Henrik Reif Andersen, Henrik Hulgaard. 39-51 [doi]
- A Library for Composite Symbolic RepresentationsTuba Yavuz-Kahveci, Murat Tuncer, Tevfik Bultan. 52-66 [doi]
- Synthesis of Linear Ranking FunctionsMichael Colón, Henny Sipma. 67-81 [doi]
- Automatic Deductive Verification with Invisible InvariantsAmir Pnueli, Sitvanit Ruah, Lenore D. Zuck. 82-97 [doi]
- Incremental Verification by AbstractionYassine Lakhnech, Saddek Bensalem, Sergey Berezin, Sam Owre. 98-112 [doi]
- A Technique for Invariant GenerationAshish Tiwari, Harald Rueß, Hassen Saïdi, Natarajan Shankar. 113-127 [doi]
- Model Checking Syllabi and Student CarreersRoberto Sebastiani, Alessandro Tomasi, Fausto Giunchiglia. 128-142 [doi]
- Verification of Vortex WorkflowsXiang Fu, Tevfik Bultan, Richard Hull, Jianwen Su. 143-157 [doi]
- Parameterized Verification of Multithreaded Software LibrariesThomas Ball, Sagar Chaki, Sriram K. Rajamani. 158-173 [doi]
- Efficient Guiding Towards Cost-Optimality in UPPAALGerd Behrmann, Ansgar Fehnker. 174-188 [doi]
- Linear Parametric Model Checking of Timed AutomataThomas Hune, Judi Romijn, Mariëlle Stoelinga, Frits W. Vaandrager. 189-203 [doi]
- Abstraction in Probabilistic Process AlgebraSuzana Andova, Jos C. M. Baeten. 204-219 [doi]
- First Passage Time Analysis of Stochastic Process Algebra Using Partial OrdersTheo C. Ruys, Rom Langerak, Joost-Pieter Katoen, Diego Latella, Mieke Massink. 220-235 [doi]
- Hardware/Software Co-Design Using Functional LanguagesAlan Mycroft, Richard Sharp. 236-251 [doi]
- Automatic Abstraction of Memories in the Formal Verification of Superscalar MicroprocessorsMiroslav N. Velev. 252-267 [doi]
- Boolean and Cartesian Abstraction for Model Checking C ProgramsThomas Ball, Andreas Podelski, Sriram K. Rajamani. 268-283 [doi]
- Finding Feasible Counter-examples when Model Checking Abstracted Java ProgramsCorina S. Pasareanu, Matthew B. Dwyer, Willem Visser. 284-298 [doi]
- The LOOP Compiler for Java and JMLJoachim van den Berg, Bart Jacobs. 299-312 [doi]
- Searching Powerset Automata by Combining Explicit-State and Symbolic Model CheckingAlessandro Cimatti, Marco Roveri, Piergiorgio Bertoli. 313-327 [doi]
- Saturation: An Efficient Iteration Strategy for Symbolic State-Space GenerationGianfranco Ciardo, Gerald Lüttgen, Radu Siminiceanu. 328-342 [doi]
- Automated Test Generation from Timed AutomataBrian Nielsen, Arne Skou. 343-357 [doi]
- Testing an Intentional Naming Scheme Using Genetic AlgorithmsSarfraz Khurshid. 358-372 [doi]
- Building a Tool for the Analysis and Testing of Web Applications: Problems and SolutionsFilippo Ricca, Paolo Tonella. 373-388 [doi]
- TATOO: Testing and Analysis Tool for Object- Oriented SoftwareAmie L. Souter, Tiffany M. Wong, Stacey A. Shindo, Lori L. Pollock. 389-403 [doi]
- Implementing a Multi-valued Symbolic Model CheckerMarsha Chechik, Benet Devereux, Steve M. Easterbrook. 404-419 [doi]
- Is There a Best Symbolic Cycle-Detection Algorithm?Kathi Fisler, Ranan Fraer, Gila Kamhi, Moshe Y. Vardi, Zijiang Yang. 420-434 [doi]
- Combining Structural and Enumerative Techniques for the Validation of Bounded Petri NetsRubén Carvajal-Schiaffino, Giorgio Delzanno, Giovanni Chiola. 435-449 [doi]
- A Sweep-Line Method for State Space ExplorationSøren Christensen, Lars Michael Kristensen, Thomas Mailund. 450-464 [doi]
- Assume-Guarantee Based Compositional Reasoning for Synchronous Timing DiagramsNina Amla, E. Allen Emerson, Kedar S. Namjoshi, Richard J. Trefler. 465-479 [doi]
- Simulation RevisitedLi Tan, Rance Cleaveland. 480-495 [doi]
- Compositional Message Sequence ChartsElsa L. Gunter, Anca Muscholl, Doron Peled. 496-511 [doi]
- An Automata Based Interpretation of Live Sequence ChartsJochen Klose, Hartmut Wittke. 512-527 [doi]
- Coverage Metrics for Temporal Logic Model CheckingHana Chockler, Orna Kupferman, Moshe Y. Vardi. 528-542 [doi]
- Parallel Model Checking for the Alternation Free µ-CalculusBenedikt Bollig, Martin Leucker, Michael Weber 0002. 543-558 [doi]
- Model Checking CTL*[DC]Paritosh K. Pandya. 559-573 [doi]
- CPN/Tools: A Tool for Editing and Simulating Coloured Petri Nets ETAPS Tool Demonstration Related to TACASMichel Beaudouin-Lafon, Wendy E. Mackay, Mads Jensen, Peter Andersen, Paul Janecek, Henry Michael Lassen, Kasper Lund, Kjeld Høyer Mortensen, Stephanie Munck, Anne V. Ratzer, Katrine Ravn, Søren Christensen, Kurt Jensen. 574-577 [doi]
- The ASM Workbench - A Tool Environment for Computer-Aided Analysis and Validation of Abstract State Machine Models Tool DemonstrationGiuseppe Del Castillo. 578-581 [doi]
- The Erlang Verification ToolThomas Noll, Lars-Åke Fredlund, Dilian Gurov. 582-586 [doi]