| 2005 | A Generic Theorem Prover of CSP Refinement. Yoshinao Isobe, Markus Roggenbach |
| 2005 | A New Algorithm for Strategy Synthesis in LTL Games. Aidan Harding, Mark Ryan, Pierre-Yves Schobbens |
| 2005 | A Note on On-the-Fly Verification Algorithms. Stefan Schwoon, Javier Esparza |
| 2005 | A Two-Tier Technique for Supporting Quantifiers in a Lazily Proof-Explicating Theorem Prover. K. Rustan M. Leino, Madan Musuvathi, Xinming Ou |
| 2005 | Algorithmic Verification of Recursive Probabilistic State Machines. Kousha Etessami, Mihalis Yannakakis |
| 2005 | An Abstract Interpretation-Based Refinement Algorithm for Strong Preservation. Francesco Ranzato, Francesco Tapparo |
| 2005 | An Incremental and Layered Procedure for the Satisfiability of Linear Arithmetic Logic. Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Peter van Rossum, Stephan Schulz, Roberto Sebastiani |
| 2005 | Applications of Craig Interpolants in Model Checking. Kenneth L. McMillan |
| 2005 | BISIMULATOR: A Modular Tool for On-the-Fly Equivalence Checking. Damien Bergamini, Nicolas Descoubes, Christophe Joubert, Radu Mateescu |
| 2005 | Bounded Validity Checking of Interval Duration Logic. Babita Sharma, Paritosh K. Pandya, Supratik Chakraborty |
| 2005 | Complementation Constructions for Nondeterministic Automata on Infinite Words. Orna Kupferman, Moshe Y. Vardi |
| 2005 | Compositional Message Sequence Charts (CMSCs) Are Better to Implement Than MSCs. Blaise Genest |
| 2005 | Context-Bounded Model Checking of Concurrent Software. Shaz Qadeer, Jakob Rehof |
| 2005 | Dependent Types for Program Understanding. Raghavan Komondoor, Ganesan Ramalingam, Satish Chandra, John Field |
| 2005 | Dynamic Symmetry Reduction. E. Allen Emerson, Thomas Wahl |
| 2005 | Efficient Conflict Analysis for Finding All Satisfying Assignments of a Boolean Circuit. HoonSang Jin, HyoJung Han, Fabio Somenzi |
| 2005 | Empirically Efficient Verification for a Class of Infinite-State Systems. Jesse D. Bingham, Alan J. Hu |
| 2005 | FocusCheck: A Tool for Model Checking and Debugging Sequential C Programs. Curtis W. Keller, Diptikalyan Saha, Samik Basu, Scott A. Smolka |
| 2005 | JML-Testing-Tools: A Symbolic Animator for JML Specifications Using CLP. Fabrice Bouquet, Frédéric Dadeau, Bruno Legeard, Mark Utting |
| 2005 | Java-MOP: A Monitoring Oriented Programming Environment for Java. Feng Chen, Grigore Rosu |
| 2005 | Localization and Register Sharing for Predicate Abstraction. Himanshu Jain, Franjo Ivancic, Aarti Gupta, Malay K. Ganai |
| 2005 | Mining Temporal Specifications for Error Detection. Westley Weimer, George C. Necula |
| 2005 | Model Checking Infinite-State Markov Chains. Anne Remke, Boudewijn R. Haverkort, Lucia Cloth |
| 2005 | Monte Carlo Model Checking. Radu Grosu, Scott A. Smolka |
| 2005 | On Some Transformation Invariants Under Retiming and Resynthesis. Jie-Hong Roland Jiang |
| 2005 | On-the-Fly Reachability and Cycle Detection for Recursive State Machines. Rajeev Alur, Swarat Chaudhuri, Kousha Etessami, P. Madhusudan |
| 2005 | SATABS: SAT-Based Predicate Abstraction for ANSI-C. Edmund M. Clarke, Daniel Kroening, Natasha Sharygina, Karen Yorav |
| 2005 | Separating Fairness and Well-Foundedness for the Analysis of Fair Discrete Systems. Amir Pnueli, Andreas Podelski, Andrey Rybalchenko |
| 2005 | Shortest Counterexamples for Symbolic Model Checking of LTL with Past. Viktor Schuppan, Armin Biere |
| 2005 | Simulation-Based Iteration of Tree Transducers. Parosh Aziz Abdulla, Axel Legay, Julien d'Orso, Ahmed Rezine |
| 2005 | Snapshot Verification. Blaise Genest, Dietrich Kuske, Anca Muscholl, Doron A. Peled |
| 2005 | Symbolic Test Selection Based on Approximate Analysis. Bertrand Jeannet, Thierry Jéron, Vlad Rusu, Elena Zinovieva |
| 2005 | Symstra: A Framework for Generating Object-Oriented Unit Tests Using Symbolic Execution. Tao Xie, Darko Marinov, Wolfram Schulte, David Notkin |
| 2005 | Temporal Logic for Scenario-Based Specifications. Hillel Kugler, David Harel, Amir Pnueli, Yuan Lu, Yves Bontemps |
| 2005 | Time-Efficient Model Checking with Magnetic Disk. Tonglaga Bao, Michael D. Jones |
| 2005 | Tools and Algorithms for the Construction and Analysis of Systems, 11th International Conference, TACAS 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005, Edinburgh, UK, April 4-8, 2005, Proceedings Nicolas Halbwachs, Lenore D. Zuck |
| 2005 | Truly On-the-Fly LTL Model Checking. Moritz Hammer, Alexander Knapp, Stephan Merz |
| 2005 | Using BDDs to Decide CTL. Will Marrero |
| 2005 | Using Language Inference to Verify Omega-Regular Properties. Abhay Vardhan, Koushik Sen, Mahesh Viswanathan, Gul Agha |
| 2005 | Verifying Programs with Dynamic 1-Selector-Linked Structures in Regular Model Checking. Ahmed Bouajjani, Peter Habermehl, Pierre Moro, Tomás Vojnar |
| 2005 | jETI: A Tool for Remote Tool Integration. Tiziana Margaria, Ralf Nagel, Bernhard Steffen |
| 2005 | jMoped: A Java Bytecode Checker Based on Moped. Dejvuth Suwimonteerabuth, Stefan Schwoon, Javier Esparza |