Abstract is missing.
- On the Construction of Automata from Linear Arithmetic ConstraintsPierre Wolper, Bernard Boigelot. 1-19 [doi]
- An Extensible Type System for Component-Based DesignYuhong Xiong, Edward A. Lee. 20-37 [doi]
- Proof General: A Generic Tool for Proof DevelopmentDavid Aspinall. 38-42 [doi]
- ViewPoint-Oriented Software Development: Tool Support for Integrating Multiple Perspectives by Distributed Graph TransformationMichael Goedicke, Bettina Enders, Torsten Meyer, Gabriele Taentzer. 43-47 [doi]
- Consistent Integration of Formal MethodsPeter Braun 0003, Heiko Lötzbeyer, Bernhard Schätz, Oscar Slotosch. 48-62 [doi]
- An Architecture for Interactive Program ProversJörg Meyer, Arnd Poetzsch-Heffter. 63-77 [doi]
- The PROSPER ToolkitLouise A. Dennis, Graham Collins, Michael Norrish, Richard J. Boulton, Konrad Slind, Graham Robinson, Michael J. C. Gordon, Thomas F. Melham. 78-92 [doi]
- CASL: From Semantics to ToolsTill Mossakowski. 93-108 [doi]
- On the Construction of Live Timed SystemsSébastien Bornot, Gregor Gößler, Joseph Sifakis. 109-126 [doi]
- On Memory-Block Traversal Problems in Model-Checking Timed-SystemsFredrik Larsson, Paul Pettersson, Wang Yi. 127-141 [doi]
- Symbolic Model Checking for Rectangular Hybrid SystemsThomas A. Henzinger, Rupak Majumdar. 142-156 [doi]
- Efficient Data Structure for Fully Symbolic Verification of Real-Time Software SystemsFarn Wang. 157-171 [doi]
- Verification of Parameterized Systems Using Logic Program TransformationsAbhik Roychoudhury, K. Narayan Kumar, C. R. Ramakrishnan, I. V. Ramakrishnan, Scott A. Smolka. 172-187 [doi]
- Abstracting WS1S Systems to Verify Parameterized NetworksKai Baukus, Saddek Bensalem, Yassine Lakhnech, Karsten Stahl. 188-203 [doi]
- FMona: A Tool for Expressing Validation Techniques over Infinite State SystemsJean-Paul Bodeveix, Mamoun Filali. 204-219 [doi]
- Transitive Closures of Regular Relations for Verifying Infinite-State SystemsBengt Jonsson, Marcus Nilsson. 220-234 [doi]
- Using Static Analysis to Improve Automatic Test GenerationMarius Bozga, Jean-Claude Fernandez, Lucian Ghirvu. 235-250 [doi]
- Efficient Diagnostic Generation for Boolean Equation SystemsRadu Mateescu. 251-265 [doi]
- Compositional State Space Generation with Partial Order Reductions for Asynchronous Communicating SystemsJean-Pierre Krimm, Laurent Mounier. 266-282 [doi]
- Checking for CFFD-Preorder with Tester ProcessesJuhana Helovuo, Antti Valmari. 283-298 [doi]
- Fair BisimulationThomas A. Henzinger, Sriram K. Rajamani. 299-314 [doi]
- Integrating Low Level Symmetries into Reachability AnalysisKarsten Schmidt 0004. 315-330 [doi]
- Model Checking Support for the ASM High-Level LanguageGiuseppe Del Castillo, Kirsten Winter. 331-346 [doi]
- A Markov Chain Model CheckerHolger Hermanns, Joost-Pieter Katoen, Joachim Meyer-Kayser, Markus Siegle. 347-362 [doi]
- Model Checking SDL with SpinDragan Bosnacki, Dennis Dams, Leszek Holenderski, Natalia Sidorova. 363-377 [doi]
- Salsa: Combining Constraint Solvers with BDDs for Automatic Invariant CheckingRamesh Bharadwaj, Steve Sims. 378-394 [doi]
- Symbolic Model Checking of Probabilistic Processes Using MTBDDs and the Kronecker RepresentationLuca de Alfaro, Marta Z. Kwiatkowska, Gethin J. Norman, David Parker, Roberto Segala. 395-410 [doi]
- Symbolic Reachability Analysis Based on SAT-SolversParosh Aziz Abdulla, Per Bjesse, Niklas Eén. 411-425 [doi]
- Symbolic Representation of Upward-Closed SetsGiorgio Delzanno, Jean-François Raskin. 426-440 [doi]
- BDD vs. Constraint-Based Model Checking: An Experimental Evaluation for Asynchronous Concurrent SystemsTevfik Bultan. 441-455 [doi]
- Tool-Based Specification of Visual Languages and Graphic EditorsMagnus Niemann, Roswitha Bardohl. 456-470 [doi]
- VIP: A Visual Editor and Compiler for v-PromelaMoataz Kamel, Stefan Leue. 471-486 [doi]
- A Comparison of Two Verification Methods for Speculative Instruction ExecutionTamarah Arons, Amir Pnueli. 487-502 [doi]
- Partial Order Reductions for Security Protocol VerificationEdmund M. Clarke, Somesh Jha, Wilfredo R. Marrero. 503-518 [doi]
- Model Checking Security Protocols Using a Logic of BeliefMassimo Benerecetti, Fausto Giunchiglia. 519-534 [doi]
- A Formal Specification and Validation of a Critical System in Presence of Byzantine ErrorsStefania Gnesi, Diego Latella, Gabriele Lenzini, C. Abbaneo, Arturo M. Amendola, P. Marmo. 535-549 [doi]