| 2012 | An Asymptotically Correct Finite Path Semantics for LTL. | Andreas Morgenstern, Manuel Gesell, Klaus Schneider |
| 2012 | Matrix Interpretations for Polynomial Derivational Complexity of Rewrite Systems. | Aart Middeldorp |
| 2012 | Automatic Verification of TLA + Proof Obligations with SMT Solvers. | Stephan Merz, Hernn Vanzetto |
| 2012 | Regular Expressions for Data Words. | Leonid Libkin, Domagoj Vrgoc |
| 2012 | r-TuBound: Loop Bounds for WCET Analysis (Tool Paper). | Jens Knoop, Laura Kovcs, Jakob Zwirchmayr |
| 2012 | Confluence of Non-Left-Linear TRSs via Relative Termination. | Dominik Klein, Nao Hirokawa |
| 2012 | Conflict Anticipation in the Search for Graph Automorphisms. | Hadi Katebi, Karem A. Sakallah, Igor L. Markov |
| 2012 | Efficient Rule-Matching for Hyper-Tableaux. | Bjarne Holen, Dag Hovland, Martin Giese |
| 2012 | Linear Constraints over Infinite Trees. | Martin Hofmann, Dulma Rodriguez |
| 2012 | Towards Algorithmic Cut-Introduction. | Stefan Hetzl, Alexander Leitsch, Daniel Weller |
| 2012 | Automatic Generation of Invariants for Circular Derivations in SUP(LA). | Arnaud Fietzke, Evgeny Kruglov, Christoph Weidenbach |
| 2012 | Duality between Merging Operators and Social Contraction Operators. | Jos Luis Chacn, Ramn Pino Prez |
| 2012 | Monitor-Based Statistical Model Checking for Weighted Metric Temporal Logic. | Peter E. Bulychev, Alexandre David, Kim Guldstrand Larsen, Axel Legay, Guangyuan Li, Danny Bgsted Poulsen, Amlie Stainer |
| 2012 | Smart Testing of Functional Programs in Isabelle. | Lukas Bulwahn |
| 2012 | Finding Finite Herbrand Models. | Stefan Borgwardt, Barbara Morawska |
| 2012 | Engineering Theories with Z3. | Nikolaj S. Bjrner |
| 2012 | Dual-Priced Modal Transition Systems with Time Durations. | Nikola Benes, Jan Kretnsk, Kim Guldstrand Larsen, Mikael H. Mller, Jir Srba |
| 2012 | Solving Language Equations and Disequations with Applications to Disunification in Description Logics and Monadic Set Constraints. | Franz Baader, Alexander Okhotin |
| 2012 | Querying Proofs. | David Aspinall, Ewen Denney, Christoph Lth |
| 2012 | Forgetting for Defeasible Logic. | Grigoris Antoniou, Thomas Eiter, Kewen Wang |
| 2012 | Moral Reasoning under Uncertainty. | Han The Anh, Ari Saptawijaya, Lus Moniz Pereira |
| 2012 | Random: R-Based Analyzer for Numerical Domains. | Gianluca Amato, Francesca Scozzari |
| 2012 | Backward Trace Slicing for Conditional Rewrite Theories. | Mara Alpuente, Demis Ballis, Francisco Frechina, Daniel Romero |
| 2012 | Lazy Abstraction with Interpolants for Arrays. | Francesco Alberti, Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise, Natasha Sharygina |
| 2012 | Automatic Inference of Resource Consumption Bounds. | Elvira Albert, Puri Arenas, Samir Genaim, Miguel Gmez-Zamalloa, Germn Puebla |