| 2016 | Reasoning with Sets and Sums of Sets. | Markus Bender |
| 2016 | Efficient Instantiation Techniques in SMT (Work In Progress). | Haniel Barbosa |
| 2016 | A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT. | Kshitij Bansal, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli |
| 2016 | Algebraic Polynomial-based Synthesis for Abstract Boolean Network Analysis. | Peter Backeman, Christoph M. Wintersteiger, Boyan Yordanov, Sara-Jane Dunn |
| 2016 | A Logical Framework for Developing and Mechanizing Set Theories. | Arnon Avron |
| 2016 | Unbounded-Thread Program Verification using Thread-State Equations. | Konstantinos Athanasiou, Peizun Liu, Thomas Wahl |
| 2016 | Model Checking Parameterised Multi-token Systems via the Composition Method. | Benjamin Aminof, Sasha Rubin |
| 2016 | Evaluating Automated Theorem Provers Using Adimen-SUMO. | Javier lvez, Paqui Lucio, German Rigau |
| 2016 | Counting Constraints in Flat Array Fragments. | Francesco Alberti, Silvio Ghilardi, Elena Pagani |
| 2016 | Nominal Confluence Tool. | Takahito Aoto, Kentaro Kikuchi |
| 2015 | MathCheck: A Math Assistant via a Combination of Computer Algebra Systems and SAT Solvers. | Edward Zulkoski, Vijay Ganesh, Krzysztof Czarnecki |
| 2015 | There is no one Logic to Model Human Reasoning: the Case from Interpretation. | Alexandra Varga, Keith Stenning, Laura Martignon |
| 2015 | Program Synthesis Using Dual Interpretation. | Ashish Tiwari, Adri Gascn, Bruno Dutertre |
| 2015 | Things You Can't do With a Vampire. | Geoff Sutcliffe |
| 2015 | CoLL: A Confluence Tool for Left-Linear Term Rewrite Systems. | Kiraku Shintani, Nao Hirokawa |
| 2015 | Encoding Dependency Pair Techniques and Control Strategies for Maximal Completion. | Haruhiko Sato, Sarah Winkler |
| 2015 | Non-E-Overlapping, Weakly Shallow, and Non-Collapsing TRSs are Confluent. | Masahiko Sakai, Michio Oyamaguchi, Mizuhito Ogawa |
| 2015 | Exploring Theories with a Model-Finding Assistant. | Salman Saghafi, Ryan Danas, Daniel J. Dougherty |
| 2015 | A Decision Procedure for (Co)datatypes in SMT Solvers. | Andrew Reynolds, Jasmin Christian Blanchette |
| 2015 | Cooperating Proof Attempts. | Giles Reger, Dmitry Tishkovsky, Andrei Voronkov |
| 2015 | Playing with AVATAR. | Giles Reger, Martin Suda, Andrei Voronkov |
| 2015 | The Uses of SAT Solvers in Vampire. | Giles Reger, Martin Suda |
| 2015 | A Uniform Substitution Calculus for Differential Dynamic Logic. | Andr Platzer |
| 2015 | History and Prospects for First-Order Automated Deduction. | David A. Plaisted |
| 2015 | Inductive Beluga: Programming Proofs. | Brigitte Pientka, Andrew Cave |