| 2005 | A Policy Iteration Algorithm for Computing Fixed Points in Static Analysis of Programs. Alexandru Costan, Stephane Gaubert, Eric Goubault, Matthieu Martel, Sylvie Putot |
| 2005 | Abstraction Refinement for Bounded Model Checking. Anubhav Gupta, Ofer Strichman |
| 2005 | Abstraction Refinement via Inductive Learning. Alexey Loginov, Thomas W. Reps, Shmuel Sagiv |
| 2005 | Abstraction for Falsification. Thomas Ball, Orna Kupferman, Greta Yorsh |
| 2005 | Action Language Verifier, Extended. Tuba Yavuz-Kahveci, Constantinos Bartzis, Tevfik Bultan |
| 2005 | Algorithmic Algebraic Model Checking I: Challenges from Systems Biology. Carla Piazza, Marco Antoniotti, Venkatesh Mysore, Alberto Policriti, Franz Winkler, Bud Mishra |
| 2005 | Automated Assume-Guarantee Reasoning for Simulation Conformance. Sagar Chaki, Edmund M. Clarke, Nishant Sinha, Prasanna Thati |
| 2005 | Bounded Model Checking of Concurrent Programs. Ishai Rabinovitz, Orna Grumberg |
| 2005 | Building Your Own Software Model Checker Using the Bogor Extensible Model Checking Framework. Matthew B. Dwyer, John Hatcliff, Matthew Hoosier, Robby |
| 2005 | Cogent: Accurate Theorem Proving for Program Verification. Byron Cook, Daniel Kroening, Natasha Sharygina |
| 2005 | Compositional Analysis of Floating-Point Linear Numerical Filters. David Monniaux |
| 2005 | Computer Aided Verification, 17th International Conference, CAV 2005, Edinburgh, Scotland, UK, July 6-10, 2005, Proceedings Kousha Etessami, Sriram K. Rajamani |
| 2005 | Concrete Model Checking with Abstract Matching and Refinement. Corina S. Pasareanu, Radek Pelánek, Willem Visser |
| 2005 | DPLL(T) with Exhaustive Theory Propagation and Its Application to Difference Logic. Robert Nieuwenhuis, Albert Oliveras |
| 2005 | Data Structure Specifications via Local Equality Axioms. Scott McPeak, George C. Necula |
| 2005 | Efficient Monitoring of omega-Languages. Marcelo d'Amorim, Grigore Rosu |
| 2005 | Efficient Satisfiability Modulo Theories via Delayed Theory Combination. Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Silvio Ranise, Peter van Rossum, Roberto Sebastiani |
| 2005 | Expand, Enlarge and Check... Made Efficient. Gilles Geeraerts, Jean-François Raskin, Laurent Van Begin |
| 2005 | Extended Weighted Pushdown Systems. Akash Lal, Thomas W. Reps, Gogul Balakrishnan |
| 2005 | F-Soft: Software Verification Platform. Franjo Ivancic, Zijiang Yang, Malay K. Ganai, Aarti Gupta, Ilya Shlyakhter, Pranav Ashar |
| 2005 | Formal Verification of Backward Compatibility of Microcode. Tamarah Arons, Elad Elster, Limor Fix, Sela Mador-Haim, Michael Mishaeli, Jonathan Shalev, Eli Singerman, Andreas Tiemeyer, Moshe Y. Vardi, Lenore D. Zuck |
| 2005 | Formal Verification of Pentium® 4 Components with Symbolic Simulation and Inductive Invariants. Roope Kaivola |
| 2005 | IIV: An Invisible Invariant Verifier. Ittai Balaban, Yi Fang, Amir Pnueli, Lenore D. Zuck |
| 2005 | Improved Probabilistic Models for 802.11 Protocol Verification. Amitabha Roy, K. Gopinath |
| 2005 | Incremental Algorithms for Inter-procedural Analysis of Safety Properties. Christopher L. Conway, Kedar S. Namjoshi, Dennis Dams, Stephen A. Edwards |
| 2005 | Incremental and Complete Bounded Model Checking for Full PLTL. Keijo Heljanko, Tommi A. Junttila, Timo Latvala |
| 2005 | Interpolant-Based Transition Relation Approximation. Ranjit Jhala, Kenneth L. McMillan |
| 2005 | JVer: A Java Verifier. Ajay Chander, David Espinosa, Nayeem Islam, Peter Lee, George C. Necula |
| 2005 | Linear Ranking with Reachability. Aaron R. Bradley, Zohar Manna, Henny B. Sipma |
| 2005 | Model Checking x86 Executables with CodeSurfer/x86 and WPDS++. Gogul Balakrishnan, Thomas W. Reps, Nicholas Kidd, Akash Lal, Junghee Lim, David Melski, Radu Gruian, Suan Hsi Yong, Chi-Hua Chen, Tim Teitelbaum |
| 2005 | On Statistical Model Checking of Stochastic Systems. Koushik Sen, Mahesh Viswanathan, Gul Agha |
| 2005 | Predicate Abstraction via Symbolic Decision Procedures. Shuvendu K. Lahiri, Thomas Ball, Byron Cook |
| 2005 | Probabilistic Verification for "Black-Box" Systems. Håkan L. S. Younes |
| 2005 | Program Repair as a Game. Barbara Jobstmann, Andreas Griesmayer, Roderick Bloem |
| 2005 | Randomized Algorithms for Program Analysis and Verification. George C. Necula, Sumit Gulwani |
| 2005 | Reasoning About Threads Communicating via Locks. Vineet Kahlon, Franjo Ivancic, Aarti Gupta |
| 2005 | Romeo: A Tool for Analyzing Time Petri Nets. Guillaume Gardey, Didier Lime, Morgan Magnin, Olivier H. Roux |
| 2005 | SMT-COMP: Satisfiability Modulo Theories Competition. Clark W. Barrett, Leonardo Mendonça de Moura, Aaron Stump |
| 2005 | Saturn: A SAT-Based Tool for Bug Detection. Yichen Xie, Alex Aiken |
| 2005 | Symbolic Compositional Verification by Learning Assumptions. Rajeev Alur, P. Madhusudan, Wonhong Nam |
| 2005 | Symbolic Systems, Explicit Properties: On Hybrid Approaches for LTL Symbolic Model Checking. Roberto Sebastiani, Stefano Tonetta, Moshe Y. Vardi |
| 2005 | Symmetry Reduction in SAT-Based Model Checking. Daijue Tang, Sharad Malik, Aarti Gupta, C. Norris Ip |
| 2005 | Syntax-Driven Reachable State Space Construction of Synchronous Reactive Programs. Eric Vecchié, Robert de Simone |
| 2005 | TRANSYT: A Tool for the Verification of Asynchronous Concurrent Systems. Enric Pastor, Marco A. Peña, Marc Solé |
| 2005 | TVOC: A Translation Validator for Optimizing Compilers. Clark W. Barrett, Yi Fang, Benjamin Goldberg, Ying Hu, Amir Pnueli, Lenore D. Zuck |
| 2005 | The AVISPA Tool for the Automated Validation of Internet Security Protocols and Applications. Alessandro Armando, David A. Basin, Yohan Boichut, Yannick Chevalier, Luca Compagna, Jorge Cuéllar, Paul Hankes Drielsma, Pierre-Cyrille Héam, Olga Kouchnarenko, Jacopo Mantovani, Sebastian Mödersheim, David von Oheimb, Michaël Rusinowitch, Judson Santiago, Mathieu Turuani, Luca Viganò, Laurent Vigneron |
| 2005 | The ComFoRT Reasoning Framework. Sagar Chaki, James Ivers, Natasha Sharygina, Kurt C. Wallnau |
| 2005 | The Orchids Intrusion Detection Tool. Julien Olivain, Jean Goubault-Larrecq |
| 2005 | Validating a Modern Microprocessor. Bob Bentley |
| 2005 | Verification of Tree Updates for Optimization. Michael Benedikt, Angela Bonifati, Sergio Flesca, Avinash Vyas |
| 2005 | Wolf - Bug Hunter for Concurrent Software Using Formal Methods. Sharon Barner, Ziv Glazberg, Ishai Rabinovitz |
| 2005 | Yet Another Decision Procedure for Equality Logic. Orly Meir, Ofer Strichman |
| 2005 | Ymer: A Statistical Model Checker. Håkan L. S. Younes |