Jan-Georg Smaus

51 papers A* 1A 2B 7C 3Misc 4Journal 14Unranked 16

Year	Rank	Type	Title / Venue / Authors
2024	—	`conf`	Proving the Existence of Stable Assignments in Democratic Forking Using Isabelle/HOL. ICTCS Jan-Georg Smaus
2023	J	`jnl`	Implementations of two Algorithms for the Threshold Synthesis Problem. CoRR Jan-Georg Smaus, Christian Schilling, Fabian Wenzelmann
2017	—	`conf`	An Existence Theorem of Nash Equilibrium in Coq and Isabelle. GandALF Stéphane Le Roux, Érik Martin-Dorel, Jan-Georg Smaus
2015	Misc	`conf`	Abstracting an Operational Semantics to Finite Automata. ICTERI Nadezhda Baklanova, Wilmer Ricciotti, Jan-Georg Smaus, Martin Strecker
2015	—	`conf`	Abstracting an Operational Semantics to Finite Automata. ICTERI (Revised Selected Papers) Nadezhda Baklanova, Wilmer Ricciotti, Jan-Georg Smaus, Martin Strecker
2015	—	`conf`	Büchi Automata Optimisations Formalised in Isabelle/HOL. ICLA Alexander Schimpf, Jan-Georg Smaus
2014	J	`jnl`	A Fully Verified Executable LTL Model Checker. Arch. Formal Proofs Javier Esparza, Peter Lammich, René Neumann, Tobias Nipkow, Alexander Schimpf, Jan-Georg Smaus
2014	J	`jnl`	Abstracting an operational semantics to finite automata. CoRR Nadezhda Baklanova, Wilmer Ricciotti, Jan-Georg Smaus, Martin Strecker
2013	A*	`conf`	A Fully Verified Executable LTL Model Checker. CAV Javier Esparza, Peter Lammich, René Neumann, Tobias Nipkow, Alexander Schimpf, Jan-Georg Smaus
2013	C	`conf`	A Pretty Complete Combinatorial Algorithm for the Threshold Synthesis Problem. IWOCA Christian Schilling, Jan-Georg Smaus, Fabian Wenzelmann
2012	Misc	`conf`	Implementations of two algorithms for the threshold synthesis problem. ISAIM Jan-Georg Smaus, Christian Schilling, Fabian Wenzelmann
2011	—	`ed.`	Model Checking and Artificial Intelligence - 6th International Workshop, MoChArt 2010, Atlanta, GA, USA, July 11, 2010, Revised Selected and Invited Papers MoChArt Ron van der Meyden, Jan-Georg Smaus
2010	—	`conf`	Automated Invariant Generation for the Verification of Real-Time Systems. WING@ETAPS/IJCAR Bahareh Badban, Stefan Leue, Jan-Georg Smaus
2010	J	`jnl`	Reports of the AAAI 2010 Conference Workshops. AI Mag. 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, Leslie Pack Kaelbling, Kristian Kersting, Maithilee Kunda, Luís C. Lamb, Bhaskara Marthi, Keith McGreggor, Vivi Nastase, Gregory M. Provan, Anita Raja, Ashwin Ram, Mark O. Riedl, Stuart Russell, Ashish Sabharwal, Jan-Georg Smaus, Gita Sukthankar, Karl Tuyls, Ron van der Meyden, Alon Y. Halevy, Lilyana Mihalkova, Sriraam Natarajan
2009	—	`conf`	Automated Predicate Abstraction for Real-Time Models INFINITY Bahareh Badban, Stefan Leue, Jan-Georg Smaus
2009	—	`conf`	Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL. TPHOLs Alexander Schimpf, Stephan Merz, Jan-Georg Smaus
2009	—	`conf`	Finding Errors of Hybrid Systems by Optimising an Abstraction-Based Quality Estimate. TAP@TOOLS Stefan Ratschan, Jan-Georg Smaus
2008	—	`conf`	Relaxation Refinement: A New Method to Generate Heuristic Functions. MoChArt Jan-Georg Smaus, Jörg Hoffmann
2007	B	`conf`	On Boolean Functions Encodable as a Single Linear Pseudo-Boolean Constraint. CPAIOR Jan-Georg Smaus
2006	—	`conf`	Using Predicate Abstraction to Generate Heuristic Functions in UPPAAL. MoChArt Jörg Hoffmann, Jan-Georg Smaus, Andrey Rybalchenko, Sebastian Kupferschmid, Andreas Podelski
2006	—	`conf`	Verification-Integrated Falsification of non-Deterministic Hybrid Systems. ADHS Stefan Ratschan, Jan-Georg Smaus
2004	—	`ch.`	Characterisations of Termination in Logic Programming. Program Development in Computational Logic Dino Pedreschi, Salvatore Ruggieri, Jan-Georg Smaus
2004	B	`conf`	Termination of Logic Programs Using Various Dynamic Selection Rules. ICLP Jan-Georg Smaus
2004	J	`jnl`	Termination of simply moded logic programs with dynamic scheduling. ACM Trans. Comput. Log. Annalisa Bossi, Sandro Etalle, Sabina Rossi, Jan-Georg Smaus
2003	B	`conf`	Is There an Optimal Generic Semantics for First-Order Equations?. ICLP Jan-Georg Smaus
2003	B	`conf`	Termination of Logic Programs for Various Dynamic Selection Rules. ICLP Jan-Georg Smaus
2002	J	`jnl`	Classes of terminating logic programs. Theory Pract. Log. Program. Dino Pedreschi, Salvatore Ruggieri, Jan-Georg Smaus
2002	—	`conf`	MultiMedia Instruction in Safe and Secure Systems. WADT 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
2002	J	`jnl`	Subject Reduction of Logic Programs as Proof-Theoretic Property. J. Funct. Log. Program. Pierre Deransart, Jan-Georg Smaus
2002	Misc	`conf`	The Head Condition and Polymorphic Recursion. FLOPS Jan-Georg Smaus
2001	J	`jnl`	Analysis of Polymorphically Typed Logic Programs Using ACI-Unification CoRR Jan-Georg Smaus
2001	B	`conf`	Analysis of Polymorphically Typed Logic Programs Using ACI-Unification. LPAR Jan-Georg Smaus
2001	J	`jnl`	Classes of Terminating Logic Programs CoRR Dino Pedreschi, Salvatore Ruggieri, Jan-Georg Smaus
2001	J	`jnl`	Semantics and Termination of Simply-Moded Logic Programs with Dynamic Scheduling CoRR Annalisa Bossi, Sandro Etalle, Sabina Rossi, Jan-Georg Smaus
2001	A	`conf`	Semantics and Termination of Simply-Moded Logic Programs with Dynamic Scheduling. ESOP Annalisa Bossi, Sandro Etalle, Sabina Rossi, Jan-Georg Smaus
2001	J	`jnl`	Verifying Termination and Error-Freedom of Logic Programs with Theory Pract. Log. Program. Jan-Georg Smaus, Patricia M. Hill, Andy King
2001	Misc	`conf`	Well-Typed Logic Programs Are not Wrong. FLOPS Pierre Deransart, Jan-Georg Smaus
2000	—	`conf`	Les programmes bien typés ont tout bon. JFPLC Pierre Deransart, Jan-Georg Smaus
2000	J	`jnl`	Using Modes to Ensure Subject Reduction for Typed Logic Programs with Subtyping CoRR Jan-Georg Smaus, François Fages, Pierre Deransart
2000	—	`conf`	Using Modes to Ensure Subject Reduction for Typed Logic Programs with Subtyping. FSTTCS Jan-Georg Smaus, François Fages, Pierre Deransart
2000	J	`jnl`	Verifying Termination and Error-Freedom of Logic Programs with block Declarations CoRR Jan-Georg Smaus, Patricia M. Hill, Andy King
2000	J	`jnl`	Well-Typed Logic Programs Are not Wrong CoRR Pierre Deransart, Jan-Georg Smaus
1999	C	`conf`	Mode Analysis Domains for Typed Logic Programs. LOPSTR Jan-Georg Smaus, Patricia M. Hill, Andy King
1999	—	`—`	Modes and types in logic programming. Jan-Georg Smaus
1999	—	`conf`	Preface - Workshop on Verification of Logic Programs. Verification of Logic Programs@ICLP Sandro Etalle, Jan-Georg Smaus
1999	B	`conf`	Proving Termination of Input-Consuming Logic Programs. ICLP Jan-Georg Smaus
1999	A	`conf`	Quotienting ESOP Andy King, Jan-Georg Smaus, Patricia M. Hill
1999	—	`ed.`	Workshop on Verification of Logic Programs 1999, in connection with the International Conference on Logic Programming, ICLP 1999, Las Cruces, New Mexico, USA, December 1, 1999 Verification of Logic Programs@ICLP Sandro Etalle, Jan-Georg Smaus
1998	C	`conf`	Preventing Instantiation Errors and Loops for Logic Programs with Multiple Modes Using block Declarations. LOPSTR Jan-Georg Smaus, Patricia M. Hill, Andy King
1998	—	`conf`	Termination of Logic Programs with block Declarations Running in Several Modes. PLILP/ALP Jan-Georg Smaus, Patricia M. Hill, Andy King
1997	B	`conf`	Domain Construction for Mode Analysis of Typed Logic Programs. ICLP Jan-Georg Smaus, Patricia M. Hill, Andy King