- Cryptographic Protocol Synthesis and Verification for Multiparty Sessions Karthikeyan Bhargavan, Ricardo Corin, Pierre-Malo Denielou, Cédric Fournet, James J. Leifer. CSF 2009.
- Lectures on Principles and Applications of Refinement Types Andy Gordon. 2009.
- HiPiLoT Carsten Ihlemann, Viorica Sofronie-Stokkermans. CADE 2009.
- Incremental Instance Generation in Local Reasoning (iLoRe) Swen Jacobs. CAV 2009.
- VS3: SMT Solvers for Program Verification Saurabh Srivastava, Sumit Gulwani and Jeff Foster, PLDI 2009.
- Static and Precise Detection of Concurrency Errors in Systems Code Using SMT Solvers, in Computer Aided Verification Shuvendu K. Lahiri, Shaz Qadeer, and Zvonimir Rakamaric. CAV 2009.
- Intra-Module Inference, in Computer Aided Verification Shuvendu K. Lahiri, Shaz Qadeer, Juan P. Galeotti, Jan W. Voung, and Thomas Wies. CAV 2009.
- Program Verification using Templates over Predicate Abstraction, Saurabh Srivastava and Sumit Gulwani, PLDI 2009.
- Input-Output Model Programs Margus Veanes, Nikolaj Bjřrner. ICTAC 2009
- Symbolic Bounded Conformance Checking of Model Programs Margus Veanes, Nikolaj Bjørner. PSI 2009.
- Modular Bug-finding for Integer Overflows in the Large: Sound, Efficient, Bit-precise Static Analysis Yannick Moy, Nikolaj Bjørner, Dave Sielaff (MSR-TR-2009-57)
- Path Feasibility Analysis for String-Manipulating Programs Nikolaj Bjørner, Nikolai Tillmann, Andrei Voronkov. TACAS 2009.
- A Practical Verification Methodology for Concurrent Programs Ernie Cohen, Michal Moskal, Wolfram Schulte, and Stephan Tobies, MSR-TR-2009-15, February 2009
- Automated Verification of Practical Garbage Collectors Chris Hawblitzel and Erez Petrank. In POPL 2009.
- Valigator: A Verification Tool with Bound and Invariant Generation T. A. Henzinger, T. Hottelier and L. Kovács. In LPAR 2008.
- Vx86: x86 Assembler Simulated in C Powered by Automated Theorem Proving Stefan Maus, Michal Moskal, Wolfram Schulte. 12th International Conference on Algebraic Methodology and Software Technology, AMAST 2008.
- Back to the Future: Revisiting Precise Program Verification using SMT Solvers, Shuvendu K. Lahiri, Shaz Qadeer. POPL 2008.
- Automatic verification of textbook programs that use comprehensions, K. Rustan M. Leino and Rosemary Monahan. FTfJP 2007.
- An Automatic Verifier for Java-like Programs Based on Dynamic Frames, Jan Smans, Bart Jacobs, Frank Piessens, Wolfram Schulte. FASE 2008. See also VeriCool2 and VeriFast.
- Demand-Driven Compositional Symbolic Execution, Saswat Anand, Patrice Godefroid, Nikolai Tillmann. TACAS 2008.
- An SMT Approach to Bounded Reachability Analysis of Model Programs, Margus Veanes, Nikolaj Bjørner, and Alexander Raschke. FORTE 2008.
- Model Generation for Horn Logic with Stratified Negation, Ethan Jackson and Wolfram Schulte. FORTE 2008.
- Refinement Types for Secure Implementations, Jesper Bengtson, Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon. CSF 2008.
- Better bug reporting with better privacy, Miguel Castro, Manuel Costa and Jean-Philippe Martin. ASPLOS2008.
- Efficient Well-Definedness Checking, Adam Darvas, Farhad Mehta, and Arsenii Rudich. IJCAR 2008.
- Program Analysis as Constraint Solving, Sumit Gulwani, Saurabh Srivastava, Ramarathnam Venkatesan. PLDI 2008.
Please let us know if we forgot something.
An Efficient SMT Solver