Domain Construction for Mode Analysis of Typed Logic Programs. - Jan-Georg Smaus; Patricia M. Hill; Andy King (ICLP, 1997)

Preventing Instantiation Errors and Loops for Logic Programs with Multiple Modes Using block Declarations. - Jan-Georg Smaus; Patricia M. Hill; Andy King (LOPSTR, 1998)

Termination of Logic Programs with block Declarations Running in Several Modes. - Jan-Georg Smaus; Patricia M. Hill; Andy King (PLILP/ALP, 1998)

Quotienting Share for Dependency Analysis. - Andy King; Jan-Georg Smaus; Patricia M. Hill (ESOP, 1999)

Proving Termination of Input-Consuming Logic Programs. - Jan-Georg Smaus (ICLP, 1999)

Mode Analysis Domains for Typed Logic Programs. - Jan-Georg Smaus; Patricia M. Hill; Andy King (LOPSTR, 1999)

Preface - Workshop on Verification of Logic Programs. - Sandro Etalle; Jan-Georg Smaus (Verification of Logic Programs@ICLP, 1999)

Modes and types in logic programming. - Jan-Georg Smaus (1999)

Using Modes to Ensure Subject Reduction for Typed Logic Programs with Subtyping. - Jan-Georg Smaus; François Fages; Pierre Deransart (FSTTCS, 2000)

Les programmes bien typés ont tout bon. - Pierre Deransart; Jan-Georg Smaus (JFPLC, 2000)

Verifying Termination and Error-Freedom of Logic Programs with block Declarations - Jan-Georg Smaus; Patricia M. Hill; Andy King (CoRR, 2000)

Semantics and Termination of Simply-Moded Logic Programs with Dynamic Scheduling. - Annalisa Bossi; Sandro Etalle; Sabina Rossi; Jan-Georg Smaus (ESOP, 2001)

Well-Typed Logic Programs Are not Wrong. - Pierre Deransart; Jan-Georg Smaus (FLOPS, 2001)

Analysis of Polymorphically Typed Logic Programs Using ACI-Unification. - Jan-Georg Smaus (LPAR, 2001)

Verifying Termination and Error-Freedom of Logic Programs with block Declarations. - Jan-Georg Smaus; Patricia M. Hill; Andy King (Theory Pract. Log. Program., 2001)

The Head Condition and Polymorphic Recursion. - Jan-Georg Smaus (FLOPS, 2002)

MultiMedia Instruction in Safe and Secure Systems. - Bernd Krieg-Brückner; Dieter Hutter; Arne Lindow; Christoph Lüth; Achim Mahnke; Erica Melis; Philipp Meier; Arnd Poetzsch-Heffter; Markus Roggenbach; George Russell; Jan-Georg Smaus; Martin Wirsing (WADT, 2002)

Subject Reduction of Logic Programs as Proof-Theoretic Property. - Pierre Deransart; Jan-Georg Smaus (J. Funct. Log. Program., 2002)

Classes of terminating logic programs. - Dino Pedreschi; Salvatore Ruggieri; Jan-Georg Smaus (Theory Pract. Log. Program., 2002)

Is There an Optimal Generic Semantics for First-Order Equations?. - Jan-Georg Smaus (ICLP, 2003)

Termination of Logic Programs for Various Dynamic Selection Rules. - Jan-Georg Smaus (ICLP, 2003)

Termination of Logic Programs Using Various Dynamic Selection Rules. - Jan-Georg Smaus (ICLP, 2004)

Characterisations of Termination in Logic Programming. - Dino Pedreschi; Salvatore Ruggieri; Jan-Georg Smaus (Program Development in Computational Logic, 2004)

Termination of simply moded logic programs with dynamic scheduling. - Annalisa Bossi; Sandro Etalle; Sabina Rossi; Jan-Georg Smaus (ACM Trans. Comput. Log., 2004)

Verification-Integrated Falsification of non-Deterministic Hybrid Systems. - Stefan Ratschan; Jan-Georg Smaus (ADHS, 2006)

Using Predicate Abstraction to Generate Heuristic Functions in UPPAAL. - Jörg Hoffmann 001; Jan-Georg Smaus; Andrey Rybalchenko; Sebastian Kupferschmid; Andreas Podelski (MoChArt, 2006)

On Boolean Functions Encodable as a Single Linear Pseudo-Boolean Constraint. - Jan-Georg Smaus (CPAIOR, 2007)

Relaxation Refinement: A New Method to Generate Heuristic Functions. - Jan-Georg Smaus; Jörg Hoffmann 001 (MoChArt, 2008)

Finding Errors of Hybrid Systems by Optimising an Abstraction-Based Quality Estimate. - Stefan Ratschan; Jan-Georg Smaus (TAP@TOOLS, 2009)

Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL. - Alexander Schimpf; Stephan Merz; Jan-Georg Smaus (TPHOLs, 2009)

Automated Predicate Abstraction for Real-Time Models - Bahareh Badban; Stefan Leue; Jan-Georg Smaus (INFINITY, 2009)

Automated Invariant Generation for the Verification of Real-Time Systems. - Bahareh Badban; Stefan Leue; Jan-Georg Smaus (WING@ETAPS/IJCAR, 2010)

Reports of the AAAI 2010 Conference Workshops. - David W. Aha; Mark S. Boddy; Vadim Bulitko; Artur S. d'Avila Garcez; Prashant Doshi; Stefan Edelkamp; Christopher W. Geib; Piotr J. Gmytrasiewicz; Robert P. Goldman; Pascal Hitzler; Charles L. Isbell Jr.; Darsana P. Josyula; et al. (AI Mag., 2010)

Implementations of two algorithms for the threshold synthesis problem. - Jan-Georg Smaus; Christian Schilling 001; Fabian Wenzelmann (ISAIM, 2012)

A Pretty Complete Combinatorial Algorithm for the Threshold Synthesis Problem. - Christian Schilling 001; Jan-Georg Smaus; Fabian Wenzelmann (IWOCA, 2013)

A Fully Verified Executable LTL Model Checker. - Javier Esparza; Peter Lammich; René Neumann; Tobias Nipkow; Alexander Schimpf; Jan-Georg Smaus (Arch. Formal Proofs, 2014)

Büchi Automata Optimisations Formalised in Isabelle/HOL. - Alexander Schimpf; Jan-Georg Smaus (ICLA, 2015)

Abstracting an Operational Semantics to Finite Automata. - Nadezhda Baklanova; Wilmer Ricciotti; Jan-Georg Smaus; Martin Strecker (ICTERI (Revised Selected Papers), 2015)

An Existence Theorem of Nash Equilibrium in Coq and Isabelle. - Stéphane Le Roux 001; Érik Martin-Dorel; Jan-Georg Smaus (GandALF, 2017)

Proving the Existence of Stable Assignments in Democratic Forking Using Isabelle/HOL. - Jan-Georg Smaus (ICTCS, 2024)