| 2017 | A Decision Procedure for Restricted Intensional Sets. | Maximiliano Cristi, Gianfranco Rossi |
| 2017 | Satisfiability Modulo Transcendental Functions via Incremental Linearization. | Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, Roberto Sebastiani |
| 2017 | Biabduction (and Related Problems) in Array Separation Logic. | James Brotherston, Nikos Gorogiannis, Max I. Kanovich |
| 2017 | Certifying Safety and Termination Proofs for Integer Transition Systems. | Marc Brockschmidt, Sebastiaan J. C. Joosten, Ren Thiemann, Akihisa Yamada |
| 2017 | Satisfiability Modulo Theories and Assignments. | Maria Paola Bonacina, Stphane Graham-Lengrand, Natarajan Shankar |
| 2017 | Automated Reasoning for Explainable Artificial Intelligence. | Maria Paola Bonacina |
| 2017 | Translating Between Implicit and Explicit Versions of Proof. | Roberto Blanco, Zakaria Chihani, Dale Miller |
| 2017 | Towards Strong Higher-Order Automation for Fast Interactive Verification. | Jasmin Christian Blanchette, Pascal Fontaine, Stephan Schulz, Uwe Waldmann |
| 2017 | Decision Procedures for Theories of Sets with Measures. | Markus Bender, Viorica Sofronie-Stokkermans |
| 2017 | A Transfinite Knuth-Bendix Order for Lambda-Free Higher-Order Terms. | Heiko Becker, Jasmin Christian Blanchette, Uwe Waldmann, Daniel Wand |
| 2017 | Scalable Fine-Grained Proofs for Formula Processing. | Haniel Barbosa, Jasmin Christian Blanchette, Pascal Fontaine |
| 2017 | Reasoning About Concurrency in High-Assurance, High-Performance Software Systems. | June Andronick |
| 2017 | SC-square: when Satisfiability Checking and Symbolic Computation join forces. | Erika brahm, John Abbott, Bernd Becker, Anna Maria Bigatti, Martin Brain, Alessandro Cimatti, James H. Davenport, Matthew England, Pascal Fontaine, Stephen Forrest, Vijay Ganesh, Alberto Griggio, Daniel Kroening, Werner M. Seiler |
| 2017 | Detecting Inconsistencies in Large First-Order Knowledge Bases. | Stephan Schulz, Geoff Sutcliffe, Josef Urban, Adam Pease |
| 2017 | We know (nearly) nothing!l But can we learn? | Stephan Schulz |
| 2016 | Gen2sat: An Automated Tool for Deciding Derivability in Analytic Pure Sequent Calculi. | Yoni Zohar, Anna Zamansky |
| 2016 | Effective Normalization Techniques for HOL. | Max Wisniewski, Alexander Steen, Kim Kern, Christoph Benzmller |
| 2016 | TPTP and Beyond: Representation of Quantified Non-Classical Logics. | Max Wisniewski, Alexander Steen, Christoph Benzmller |
| 2016 | The PIE Environment for First-Order-Based Proving, Interpolating and Eliminating. | Christoph Wernhard |
| 2016 | Scrambling and Descrambling SMT-LIB Benchmarks. | Tjark Weber |
| 2016 | A Saturation-based Algebraic Reasoner for ELQ. | Jelena Vlasenko, Maryam Daryalal, Volker Haarslev, Brigitte Jaumard |
| 2016 | raSAT: An SMT Solver for Polynomial Constraints. | Vu Xuan Tung, To Van Khanh, Mizuhito Ogawa |
| 2016 | Ordered Resolution with Straight Dismatching Constraints. | Andreas Teucke, Christoph Weidenbach |
| 2016 | A Dynamic Logic for Configuration. | Ching Hoo Tang, Christoph Weidenbach |
| 2016 | Kneecap: Model-based Generation of Network Traffic. | Nik Sultana, Richard Mortier |