| 2010 | A Slice-Based Decision Procedure for Type-Based Partial Orders. | Elena Sherman, Brady J. Garvin, Matthew B. Dwyer |
| 2010 | Curry-Style Explicit Substitutions for the Linear and Affine Lambda Calculus. | Anders Schack-Nielsen, Carsten Schrmann |
| 2010 | Probabilistic Logic Encoding of Spatial Domains. | Paulo Eduardo Santos, Fbio Gagliardi Cozman, Valquiria Fenelon, Britta Hummel |
| 2010 | Automatic generation of high quality test sets via CBMC. | Emanuele Di Rosa, Enrico Giunchiglia, Massimo Narizzano, Gabriele Palma, Alessandra Puddu |
| 2010 | Real Analysis for Complex Systems. | Andr Platzer |
| 2010 | MUNCH - Automated Reasoner for Sets and Multisets. | Ruzica Piskac, Viktor Kuncak |
| 2010 | Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description). | Brigitte Pientka, Jana Dunfield |
| 2010 | Designing a solver competition: the QBFEVAL'10 case study. | Claudia Peschiera, Luca Pulina, Armando Tacchella |
| 2010 | Towards Approximative Most Specific Concepts by Completion for EL with Subjective Probabilities. | Rafael Pealoza, Anni-Yasmin Turhan |
| 2010 | Three Years of Experience with Sledgehammer, a Practical Link between Automatic and Interactive Theorem Provers. | Lawrence C. Paulson |
| 2010 | Classical Logic with Partial Functions. | Hans de Nivelle |
| 2010 | Statistical Methodology for Comparison of SAT Solvers. | Mladen Nikolic |
| 2010 | Monotonicity Criteria for Polynomial Interpretations over the Naturals. | Friedrich Neurauter, Aart Middeldorp, Harald Zankl |
| 2010 | Applications and Challenges in Satisfiability Modulo Theories. | Leonardo Mendona de Moura, Nikolaj S. Bjrner |
| 2010 | Bugs, Moles and Skeletons: Symbolic Reasoning for Software Development. | Leonardo Mendona de Moura, Nikolaj S. Bjrner |
| 2010 | Automation for Geometry in Isabelle/HOL. | Laura I. Meikle, Jacques D. Fleuriot |
| 2010 | Herod and Pilate: Two Tableau Provers for Basic Hybrid Logic. | Marta Cialdea Mayer, Serenella Cerrito |
| 2010 | Trie Based Subsumption and Improving the pi-Trie Algorithm. | Andrew Matusiewicz, Neil V. Murray, Erik Rosenthal |
| 2010 | URBiVA: Uniform Reduction to Bit-Vector Arithmetic. | Filip Maric, Predrag Janicic |
| 2010 | Tractable Extensions of the Description Logic | Despoina Magka, Yevgeny Kazakov, Ian Horrocks |
| 2010 | Synthesising Functional Invariants in Separation Logic. | Ewen Maclean, Andrew Ireland, Gudmund Grov |
| 2010 | Refinement and Term Synthesis in Loop Invariant Generation. | Ewen Maclean, Andrew Ireland, Lucas Dixon, Robert Atkey |
| 2010 | A Comparative Study of Invariant Assertions, Invariant Relations, and Invariant Functions. | Asma Louhichi, Olfa Mraihi, Lamia Labed Jilani, Ali Mili |
| 2010 | Finite countermodels as invariants. A case study in verification of parameterized mutual exclusion protocol. | Alexei Lisitsa |
| 2010 | Formal Requirements Capturing using VRS system. | Alexander A. Letichevsky, Alexander Kolchin, Oleksandr Letychevskyy Jr., Stepan Potiyenko, Vladislav A. Volkov, Thomas Weigert |