| 2011 | Sort It Out with Monotonicity - Translating between Many-Sorted and Unsorted First-Order Logic. | Koen Claessen, Ann Lilliestrm, Nicholas Smallbone |
| 2011 | The Anatomy of Equinox - An Extensible Automated Reasoning Tool for First-Order Logic and Beyond - (Talk Abstract). | Koen Claessen |
| 2011 | Optimized Query Rewriting for OWL 2 QL. | Alexandros Chortaras, Despoina Trivela, Giorgos B. Stamou |
| 2011 | Experimenting with Deduction Modulo. | Guillaume Burel |
| 2011 | Reducing Higher-Order Theorem Proving to a Sequence of SAT Problems. | Chad E. Brown |
| 2011 | Automated Cyclic Entailment Proofs in Separation Logic. | James Brotherston, Dino Distefano, Rasmus Lerchedahl Petersen |
| 2011 | Heaps and Data Structures: A Challenge for Automated Provers. | Sascha Bhme, Michal Moskal |
| 2011 | Extending Sledgehammer with SMT Solvers. | Jasmin Christian Blanchette, Sascha Bhme, Lawrence C. Paulson |
| 2011 | Blocked Clause Elimination for QBF. | Armin Biere, Florian Lonsing, Martina Seidl |
| 2011 | Model Evolution with Equality Modulo Built-in Theories. | Peter Baumgartner, Cesare Tinelli |
| 2011 | Unification in the Description Logic | Franz Baader, Thanh Binh Nguyen, Stefan Borgwardt, Barbara Morawska |
| 2011 | The Matita Interactive Theorem Prover. | Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, Enrico Tassi |
| 2011 | Deciding Security for Protocols with Recursive Tests. | Mathilde Arnaud, Vronique Cortier, Stphanie Delaune |
| 2011 | Backward Trace Slicing for Rewriting Logic Theories. | Mara Alpuente, Demis Ballis, Javier Espert, Daniel Romero |
| 2011 | ASASP: Automated Symbolic Analysis of Security Policies. | Francesco Alberti, Alessandro Armando, Silvio Ranise |
| 2010 | Termination Tools in Ordered Completion. | Sarah Winkler, Aart Middeldorp |
| 2010 | Proving Information Flow Noninterference by Reusing a Machine-Checked Correctness Proof for Slicing. | Daniel Wasserrab, Denis Lohner |
| 2010 | Proving Simpson's Four-Slot Algorithm Using Ownership Transfer. | Shuling Wang, Xu Wang |
| 2010 | Generalisation of Induction Formulae based on Proving by Symbolic Execution. | Angela Wallenburg |
| 2010 | Using f-SHIN to Represent Objects: An Aid to Visual Grasping. | Nicola Vitucci, Mario Arrigoni Neri, Giuseppina Gini |
| 2010 | Towards High-Assurance Multiprocessor Virtualisation. | Michael von Tessin |
| 2010 | Different Proofs are Good Proofs. | Geoff Sutcliffe, Cynthia Chang, Li Ding, Deborah L. McGuinness, Paulo Pinheiro da Silva |
| 2010 | On the Saturation of YAGO. | Martin Suda, Christoph Weidenbach, Patrick Wischnewski |
| 2010 | Hierarchical Reasoning for the Verification of Parametric Systems. | Viorica Sofronie-Stokkermans |
| 2010 | LOOPUS - A Tool for Computing Loop Bounds for C Programs. | Moritz Sinn, Florian Zuleger |