| 2015 | ICTERI | Abstracting an Operational Semantics to Finite Automata. | Nadezhda Baklanova, Wilmer Ricciotti, Jan-Georg Smaus, Martin Strecker |
| 2015 | ICTERI | Abstracting an Operational Semantics to Finite Automata. | Nadezhda Baklanova, Wilmer Ricciotti, Jan-Georg Smaus, Martin Strecker |
| 2013 | CAV | A Fully Verified Executable LTL Model Checker. | Javier Esparza, Peter Lammich, Ren Neumann, Tobias Nipkow, Alexander Schimpf, Jan-Georg Smaus |
| 2013 | IWOCA | A Pretty Complete Combinatorial Algorithm for the Threshold Synthesis Problem. | Christian Schilling, Jan-Georg Smaus, Fabian Wenzelmann |
| 2012 | ISAIM | Implementations of two algorithms for the threshold synthesis problem. | Jan-Georg Smaus, Christian Schilling, Fabian Wenzelmann |
| 2010 | CADE | Automated Invariant Generation for the Verification of Real-Time Systems. | Bahareh Badban, Stefan Leue, Jan-Georg Smaus |
| 2009 | TAP | Finding Errors of Hybrid Systems by Optimising an Abstraction-Based Quality Estimate. | Stefan Ratschan, Jan-Georg Smaus |
| 2007 | CPAIOR | On Boolean Functions Encodable as a Single Linear Pseudo-Boolean Constraint. | Jan-Georg Smaus |
| 2004 | ICLP | Termination of Logic Programs Using Various Dynamic Selection Rules. | Jan-Georg Smaus |
| 2003 | ICLP | Is There an Optimal Generic Semantics for First-Order Equations?. | Jan-Georg Smaus |
| 2003 | ICLP | Termination of Logic Programs for Various Dynamic Selection Rules. | Jan-Georg Smaus |
| 2002 | FLOPS | The Head Condition and Polymorphic Recursion. | Jan-Georg Smaus |
| 2001 | ESOP | Semantics and Termination of Simply-Moded Logic Programs with Dynamic Scheduling. | Annalisa Bossi, Sandro Etalle, Sabina Rossi, Jan-Georg Smaus |
| 2001 | FLOPS | Well-Typed Logic Programs Are not Wrong. | Pierre Deransart, Jan-Georg Smaus |
| 2001 | LPAR | Analysis of Polymorphically Typed Logic Programs Using ACI-Unification. | Jan-Georg Smaus |
| 1999 | ESOP | Quotienting | Andy King, Jan-Georg Smaus, Patricia M. Hill |
| 1999 | ICLP | Proving Termination of Input-Consuming Logic Programs. | Jan-Georg Smaus |
| 1999 | LOPSTR | Mode Analysis Domains for Typed Logic Programs. | Jan-Georg Smaus, Patricia M. Hill, Andy King |
| 1998 | LOPSTR | Preventing Instantiation Errors and Loops for Logic Programs with Multiple Modes Using block Declarations. | Jan-Georg Smaus, Patricia M. Hill, Andy King |
| 1997 | ICLP | Domain Construction for Mode Analysis of Typed Logic Programs. | Jan-Georg Smaus, Patricia M. Hill, Andy King |