| 2012 | Specification Inference and Invariant Generation: A Machine Learning Perspective. | Aditya V. Nori |
| 2012 | Reachability Analysis of Program Variables. | Durica Nikolic, Fausto Spoto |
| 2012 | SAT and SMT Are Still Resolution: Questions and Challenges. | Robert Nieuwenhuis |
| 2012 | A Framework for Verified Depth-First Algorithms. | Ren Neumann |
| 2012 | Regression Tests and the Inventor's Dilemma. | Leonardo Mendona de Moura |
| 2012 | Building an Efficient OWL 2 DL Reasoner. | Boris Motik |
| 2012 | CDCL with Less Destructive Backtracking through Partial Ordering. | Anthony Monnet, Roger Villemaire |
| 2012 | Synthesising and Implementing Tableau Calculi for Interrogative Epistemic Logics. | Stefan Minica, Mohammad Khodadadi, Renate A. Schmidt, Dmitry Tishkovsky |
| 2012 | Abstract Domains for Bit-Level Machine Integer and Floating-point Operations. | Antoine Min |
| 2012 | An SMT-based approach to automated configuration. | Raphal Michel, Arnaud Hubaux, Vijay Ganesh, Patrick Heymans |
| 2012 | Challenges in Comparing Software Verification Tools for C. | Florian Merz, Carsten Sinz, Stephan Falke |
| 2012 | Enlarging the Scope of Applicability of Successful Techniques for Automated Reasoning in Mathematics. | Yuri V. Matiyasevich |
| 2012 | New Algorithms for Unification Modulo One-Sided Distributivity and Its Variants. | Andrew M. Marshall, Paliath Narendran |
| 2012 | Bounded Higher-order Unification using Regular Terms. | Tomer Libal |
| 2012 | Exploiting parallelism in the ME calculus. | Tianyi Liang, Cesare Tinelli |
| 2012 | A Resolution Calculus for Second-order Logic with Eager Unification. | Alexander Leitsch, Tomer Libal |
| 2012 | Branching Time? Pruning Time! | Markus Latte, Martin Lange |
| 2012 | Learning from Multiple Proofs: First Experiments. | Daniel Khlwein, Josef Urban |
| 2012 | Overview and Evaluation of Premise Selection Techniques for Large Theory Mathematics. | Daniel Khlwein, Twan van Laarhoven, Evgeni Tsivtsivadze, Josef Urban, Tom Heskes |
| 2012 | On the Complexity of Fixed-Size Bit-Vector Logics with Binary Encoded Bit-Width. | Gergely Kovsznai, Andreas Frhlich, Armin Biere |
| 2012 | Logical Difference Computation with CEX2.5. | Boris Konev, Michel Ludwig, Frank Wolter |
| 2012 | Synthesising Graphical Theories. | Aleks Kissinger |
| 2012 | Initial Experiments with External Provers and Premise Selection on HOL Light Corpora. | Cezary Kaliszyk, Josef Urban |
| 2012 | Solving Non-linear Arithmetic. | Dejan Jovanovic, Leonardo Mendona de Moura |
| 2012 | Inprocessing Rules. | Matti Jrvisalo, Marijn Heule, Armin Biere |