Abstract is missing.
- Software Documentation and the Verification ProcessDavid Lorge Parnas. 1 [doi]
- Certifying Model CheckersKedar S. Namjoshi. 2-13 [doi]
- Formalizing a JVML Verifier for Initialization in a Theorem ProverYves Bertot. 14-24 [doi]
- Automated Inductive Verification of Parameterized ProtocolsAbhik Roychoudhury, I. V. Ramakrishnan. 25-37 [doi]
- Efficient Model Checking Via Büchi Tableau AutomataGirish Bhat, Rance Cleaveland, Alex Groce. 38-52 [doi]
- Fast LTL to Büchi Automata TranslationPaul Gastin, Denis Oddoux. 53-65 [doi]
- A Practical Approach to Coverage in Model CheckingHana Chockler, Orna Kupferman, Robert P. Kurshan, Moshe Y. Vardi. 66-78 [doi]
- A Fast Bisimulation AlgorithmAgostino Dovier, Carla Piazza, Alberto Policriti. 79-90 [doi]
- Symmetry and Reduced Symmetry in Model CheckingA. Prasad Sistla, Patrice Godefroid. 91-103 [doi]
- Transformation-Based Verification Using Generalized RetimingAndreas Kuehlmann, Jason Baumgartner. 104-117 [doi]
- Meta-BDDs: A Decomposed Representation for Layered Symbolic Manipulation of Boolean FunctionsGianpiero Cabodi. 118-130 [doi]
- CLEVER: Divide and Conquer Combinational Logic Equivalence VERification with False Negative EliminationJohn Moondanos, Carl-Johan H. Seger, Ziyad Hanna, Daher Kaiss. 131-143 [doi]
- Finite Instantiations in Equivalence Logic with Uninterpreted FunctionsYoav Rodeh, Ofer Strichman. 144-154 [doi]
- Model Checking with Formula-Dependent Abstract ModelsAlexander Asteroth, Christel Baier, Ulrich Aßmann. 155-168 [doi]
- Verifying Network Protocol Implementations by Symbolic Refinement CheckingRajeev Alur, Bow-Yaw Wang. 169-181 [doi]
- Automatic Abstraction for Verification of Timed Circuits and SystemsHao Zheng, Eric Mercer, Chris J. Myers. 182-193 [doi]
- Automated Verification of a Randomized Distributed Consensus Protocol Using Cadence SMV and PRISMMarta Z. Kwiatkowska, Gethin J. Norman, Roberto Segala. 194-206 [doi]
- Analysis of Recursive State MachinesRajeev Alur, Kousha Etessami, Mihalis Yannakakis. 207-220 [doi]
- Parameterized Verification with Automatically Computed Inductive AssertionsTamarah Arons, Amir Pnueli, Sitvanit Ruah, Jiazhao Xu, Lenore D. Zuck. 221-234 [doi]
- EVC: A Validity Checker for the Logic of Equality with Uninterpreted Functions and Memories, Exploiting Positive Equality, and Conservative TransformationsMiroslav N. Velev, Randal E. Bryant. 235-240 [doi]
- AGVI - Automatic Generation, Verification, and Implementation of Security ProtocolsDawn Xiaodong Song, Adrian Perrig, Doantam Phan. 241-245 [doi]
- ICS: Integrated Canonizer and SolverJean-Christophe Filliâtre, Sam Owre, Harald Rueß, Natarajan Shankar. 246-249 [doi]
- µCRL: A Toolset for Analysing Algebraic SpecificationsStefan Blom, Wan Fokkink, Jan Friso Groote, Izak van Langevelde, Bert Lisser, Jaco van de Pol. 250-254 [doi]
- Truth/SLC - A Parallel Verification Platform for Concurrent SystemsMartin Leucker, Thomas Noll. 255-259 [doi]
- The SLAM ToolkitThomas Ball, Sriram K. Rajamani. 260-264 [doi]
- Java Bytecode Verification: An OverviewXavier Leroy. 265-285 [doi]
- Iterating TransducersDennis Dams, Yassine Lakhnech, Martin Steffen. 286-297 [doi]
- Attacking Symbolic State ExplosionGiorgio Delzanno, Jean-François Raskin, Laurent Van Begin. 298-310 [doi]
- A Unifying Model Checking Approach for Safety Properties of Parameterized SystemsMonika Maidl. 311-323 [doi]
- A BDD-Based Model Checker for Recursive ProgramsJavier Esparza, Stefan Schwoon. 324-336 [doi]
- Model Checking the World Wide WebLuca de Alfaro. 337-349 [doi]
- Distributed Symbolic Model Checking for µ-CalculusOrna Grumberg, Tamir Heyman, Assaf Schuster. 350-362 [doi]
- The Temporal Logic SugarIlan Beer, Shoham Ben-David, Cindy Eisner, Dana Fisman, Anna Gringauze, Yoav Rodeh. 363-367 [doi]
- TReX: A Tool for Reachability Analysis of Complex SystemsAurore Annichini, Ahmed Bouajjani, Mihaela Sighireanu. 368-372 [doi]
- BooStER: Speeding Up RTL Property Checking of Digital Designs by Word-Level AbstarctionPeer Johannsen. 373-377 [doi]
- SDLcheck: A Model Checking ToolVladimir Levin, Hüsnü Yenigün. 377 [doi]
- EASN: Integrating ASN.1 and Model CheckingVivek K. Shanbhag, K. Gopinath, Markku Turunen, Ari Ahtiainen, Matti Luukkainen. 382-386 [doi]
- Rtdt: A Front-End for Efficient Model Checking of Synchronous Timing DiagramsNina Amla, E. Allen Emerson, Robert P. Kurshan, Kedar S. Namjoshi. 387-390 [doi]
- TAXYS: A Tool for the Development and Verification of Real-Time Embedded SystemsEtienne Closse, Michel Poize, Jacques Pulou, Joseph Sifakis, Patrick Venter, Daniel Weil, Sergio Yovine. 391-395 [doi]
- Microarchitecture Verification by Compositional Model CheckingRanjit Jhala, Kenneth L. McMillan. 396-410 [doi]
- Rewriting for Symbolic Execution of State Machine ModelsJ. Strother Moore. 411-422 [doi]
- Using Timestamping and History Variables to Verify Sequential ConsistencyTamarah Arons. 423-435 [doi]
- Benefits of Bounded Model Checking at an Industrial SettingFady Copty, Limor Fix, Ranan Fraer, Enrico Giunchiglia, Gila Kamhi, Armando Tacchella, Moshe Y. Vardi. 436-453 [doi]
- Finding Bugs in an Alpha Microprocessor Using Satisfiability SolversPer Bjesse, Tim Leonard, Abdel Mokkedem. 454-464 [doi]
- Towards Efficient Verification of Arithmetic Algorithms over Galois Fields GF(2:::m:::)Sumio Morioka, Yasunao Katayama, Toshiyuki Yamane. 465-477 [doi]
- Job-Shop Scheduling Using Timed AutomataYasmina Abdeddaïm, Oded Maler. 478-492 [doi]
- As Cheap as Possible: Efficient Cost-Optimal Reachability for Priced Timed AutomataKim Guldstrand Larsen, Gerd Behrmann, Ed Brinksma, Ansgar Fehnker, Thomas Hune, Paul Pettersson, Judi Romijn. 493-505 [doi]
- Binary Reachability Analysis of Pushdown Timed Automata with Dense ClocksZhe Dang. 506-518 [doi]