| 2012 | Tableaux Modulo Theories Using Superdeduction - An Application to the Verification of B Proof Rules with the Zenon Automated Theorem Prover. | Mlanie Jacquel, Karim Berkani, David Delahaye, Catherine Dubois |
| 2012 | A One-Pass Tableau-Based Workflow Verification Framework. | Md Zahidul Islam, Wendy MacCaull |
| 2012 | On the Organisation of Program Verification Competitions. | Marieke Huisman, Vladimir Klebanov, Rosemary Monahan |
| 2012 | From Linear Temporal Logic Properties to Rewrite Propositions. | Pierre-Cyrille Ham, Vincent Hugot, Olga Kouchnarenko |
| 2012 | BDD-based automated reasoning in propositional non-classical logics: progress report. | Rajeev Gor, Jimmy Thomson |
| 2012 | BDD-Based Automated Reasoning for Propositional Bi-Intuitionistic Tense Logics. | Rajeev Gor, Jimmy Thomson |
| 2012 | SMT-Based System Verification with DVF. | Amit Goel, Sava Krstic, Rebekah Leslie, Mark R. Tuttle |
| 2012 | Some Notes on Basic Syntactic Mutation. | Kimberly A. Gero, Christopher Bouchard, Paliath Narendran |
| 2012 | δ-Complete Decision Procedures for Satisfiability over the Reals. | Sicun Gao, Jeremy Avigad, Edmund M. Clarke |
| 2012 | Automated Analysis of Regular Algebra. | Simon Foster, Georg Struth |
| 2012 | Combination of Disjoint Theories: Beyond Decidability. | Pascal Fontaine, Stephan Merz, Christoph Weidenbach |
| 2012 | The 2nd Verified Software Competition: Experience Report. | Jean-Christophe Fillitre, Andrei Paskevich, Aaron Stump |
| 2012 | A Theory of Arrays with set and copy Operations. | Stephan Falke, Carsten Sinz, Florian Merz |
| 2012 | Rewriting Induction + Linear Arithmetic = Decision Procedure. | Stephan Falke, Deepak Kapur |
| 2012 | The use of types in designing unification algorithms: two case studies. | Serdar Erbatur, Santiago Escobar, Paliath Narendran |
| 2012 | Proving Non-looping Non-termination Automatically. | Fabian Emmes, Tim Enger, Jrgen Giesl |
| 2012 | EPR-Based Bounded Model Checking at Word Level. | Moshe Emmer, Zurab Khasidashvili, Konstantin Korovin, Christoph Sticksel, Andrei Voronkov |
| 2012 | A Calculus for Generating Ground Explanations. | Mnacho Echenim, Nicolas Peltier |
| 2012 | Reasoning with Triggers. | Claire Dross, Sylvain Conchon, Johannes Kanig, Andrei Paskevich |
| 2012 | Taming Past LTL and Flat Counter Systems. | Stphane Demri, Amit Kumar Dhar, Arnaud Sangnier |
| 2012 | Security Protocols, Constraint Systems, and Group Theories. | Stphanie Delaune, Steve Kremer, Daniel Pasaila |
| 2012 | Benchmarking Static Analyzers. | Pascal Cuoq, Florent Kirchner, Boris Yakobowski |
| 2012 | Authorization Enforcement in Workflows: Maintaining Realizability Via Automated Reasoning. | Jason Crampton, Michael Huth, Jim Huan-Pu Kuo |
| 2012 | Proof Assistants and the Dynamic Nature of Formal Theories. | Robert L. Constable |
| 2012 | Built-in Treatment of an Axiomatic Floating-Point Theory for SMT Solvers. | Sylvain Conchon, Guillaume Melquiond, Cody Roux, Mohamed Iguernelala |