| 2007 | Lightweight Verification with Dependent Types. | Aaron Stump |
| 2007 | Games, Automata and Matching. | Colin Stirling |
| 2007 | Inferring Invariants by Symbolic Execution. | Peter H. Schmitt, Benjamin Wei |
| 2007 | A Sequent Calculus for Integer Arithmetic with Counterexample Generation. | Philipp Rmmer |
| 2007 | Semantic Selection of Premisses for Automated Theorem Proving. | Petr Pudlk |
| 2007 | Combining Deduction and Algebraic Constraints for Hybrid System Analysis. | Andr Platzer |
| 2007 | Encodings of Bounded LTL Model Checking in Effectively Propositional Logic. | Juan Antonio Navarro Prez, Andrei Voronkov |
| 2007 | System Description: E-KRHyper. | Bjrn Pelzer, Christoph Wernhard |
| 2007 | First Order Reasoning on a Large Ontology. | Adam Pease, Geoff Sutcliffe |
| 2007 | Automation of Formal Verification of PLC Programs Written in IL. | Olivera Pavlovic, Ralf Pinger, Maik Kollmann |
| 2007 | Reflecting Linear Arithmetic: From Dense Linear Orders to Presburger Arithmetic. | Tobias Nipkow |
| 2007 | KeY-C: A Tool for Verification of C Programs. | Oleg Mrk, Daniel Larsson, Reiner Hhnle |
| 2007 | Efficient E-Matching for SMT Solvers. | Leonardo Mendona de Moura, Nikolaj S. Bjrner |
| 2007 | Invited talk: Developing Efficient SMT Solvers. | Leonardo Mendona de Moura |
| 2007 | Optimized Reasoning in Description Logics Using Hypertableaux. | Boris Motik, Robert D. C. Shearer, Ian Horrocks |
| 2007 | Fully Verified Java Card API Reference Implementation. | Wojciech Mostowski |
| 2007 | The Heterogeneous Tool Set (Hets). | Till Mossakowski, Christian Maeder, Klaus Lttich |
| 2007 | A Termination Checker for Isabelle Hoare Logic. | Jia Meng, Lawrence C. Paulson, Gerwin Klein |
| 2007 | Automatic Decidability and Combinability Revisited. | Christopher Lynch, Duc-Khanh Tran |
| 2007 | Conservative Extensions in the Lightweight Description Logic EL. | Carsten Lutz, Frank Wolter |
| 2007 | Compilation as Rewriting in Higher Order Logic. | Guodong Li, Konrad Slind |
| 2007 | Labelled Clauses. | Tal Lev-Ami, Christoph Weidenbach, Thomas W. Reps, Mooly Sagiv |
| 2007 | Designing Verification Conditions for Software. | K. Rustan M. Leino |
| 2007 | Symbolic Fault Injection. | Daniel Larsson, Reiner Hhnle |
| 2007 | A History-based Verification of Distributed Applications. | Bruno Langenstein, Andreas Nonnengart, Georg Rock, Werner Stephan |