default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDJan-Georg Smaus
Person information
- affiliation: University of Freiburg, Germany
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
2020 – today
- 2024
[c33]Jan-Georg Smaus:
Proving the Existence of Stable Assignments in Democratic Forking Using Isabelle/HOL. ICTCS 2024: 225-240- 2023
- [i8]Jan-Georg Smaus, Christian Schilling, Fabian Wenzelmann:
Implementations of two Algorithms for the Threshold Synthesis Problem. CoRR abs/2301.03667 (2023)
2010 – 2019
- 2017
- [c32]Stéphane Le Roux, Érik Martin-Dorel, Jan-Georg Smaus:
An Existence Theorem of Nash Equilibrium in Coq and Isabelle. GandALF 2017: 46-60 - 2015
- [c31]Alexander Schimpf, Jan-Georg Smaus:
Büchi Automata Optimisations Formalised in Isabelle/HOL. ICLA 2015: 158-169 - [c30]Nadezhda Baklanova, Wilmer Ricciotti, Jan-Georg Smaus, Martin Strecker
:
Abstracting an Operational Semantics to Finite Automata. ICTERI (Revised Selected Papers) 2015: 109-123 - [c29]Nadezhda Baklanova, Wilmer Ricciotti, Jan-Georg Smaus, Martin Strecker:
Abstracting an Operational Semantics to Finite Automata. ICTERI 2015: 354-365 - 2014
- [j6]Javier Esparza, Peter Lammich, René Neumann, Tobias Nipkow, Alexander Schimpf, Jan-Georg Smaus:
A Fully Verified Executable LTL Model Checker. Arch. Formal Proofs 2014 (2014) - [i7]Nadezhda Baklanova, Wilmer Ricciotti, Jan-Georg Smaus, Martin Strecker:
Abstracting an operational semantics to finite automata. CoRR abs/1409.7841 (2014) - 2013
- [c28]Javier Esparza, Peter Lammich, René Neumann, Tobias Nipkow, Alexander Schimpf, Jan-Georg Smaus:
A Fully Verified Executable LTL Model Checker. CAV 2013: 463-478 - [c27]Christian Schilling, Jan-Georg Smaus, Fabian Wenzelmann:
A Pretty Complete Combinatorial Algorithm for the Threshold Synthesis Problem. IWOCA 2013: 458-462 - 2012
- [c26]Jan-Georg Smaus, Christian Schilling, Fabian Wenzelmann:
Implementations of two algorithms for the threshold synthesis problem. ISAIM 2012 - 2011
- [e2]Ron van der Meyden, Jan-Georg Smaus:
Model Checking and Artificial Intelligence - 6th International Workshop, MoChArt 2010, Atlanta, GA, USA, July 11, 2010, Revised Selected and Invited Papers. Lecture Notes in Computer Science 6572, Springer 2011, ISBN 978-3-642-20673-3 [contents] - 2010
- [j5]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:
Reports of the AAAI 2010 Conference Workshops. AI Mag. 31(4): 95-108 (2010) - [c25]Bahareh Badban, Stefan Leue, Jan-Georg Smaus:
Automated Invariant Generation for the Verification of Real-Time Systems. WING@ETAPS/IJCAR 2010: 44-58
2000 – 2009
- 2009
- [c24]Stefan Ratschan, Jan-Georg Smaus:
Finding Errors of Hybrid Systems by Optimising an Abstraction-Based Quality Estimate. TAP@TOOLS 2009: 153-168 - [c23]Alexander Schimpf, Stephan Merz, Jan-Georg Smaus:
Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL. TPHOLs 2009: 424-439 - [c22]Bahareh Badban, Stefan Leue, Jan-Georg Smaus:
Automated Predicate Abstraction for Real-Time Models. INFINITY 2009: 36-43 - 2008
- [c21]Jan-Georg Smaus, Jörg Hoffmann:
Relaxation Refinement: A New Method to Generate Heuristic Functions. MoChArt 2008: 147-165 - 2007
- [c20]Jan-Georg Smaus:
On Boolean Functions Encodable as a Single Linear Pseudo-Boolean Constraint. CPAIOR 2007: 288-302 - 2006
- [c19]Stefan Ratschan, Jan-Georg Smaus:
Verification-Integrated Falsification of non-Deterministic Hybrid Systems. ADHS 2006: 371-376 - [c18]Jörg Hoffmann, Jan-Georg Smaus, Andrey Rybalchenko, Sebastian Kupferschmid, Andreas Podelski:
Using Predicate Abstraction to Generate Heuristic Functions in UPPAAL. MoChArt 2006: 51-66 - 2004
- [j4]Annalisa Bossi, Sandro Etalle, Sabina Rossi, Jan-Georg Smaus:
Termination of simply moded logic programs with dynamic scheduling. ACM Trans. Comput. Log. 5(3): 470-507 (2004) - [c17]Jan-Georg Smaus:
Termination of Logic Programs Using Various Dynamic Selection Rules. ICLP 2004: 43-57 - [p1]Dino Pedreschi, Salvatore Ruggieri, Jan-Georg Smaus:
Characterisations of Termination in Logic Programming. Program Development in Computational Logic 2004: 376-431 - 2003
- [c16]Jan-Georg Smaus:
Is There an Optimal Generic Semantics for First-Order Equations?. ICLP 2003: 438-450 - [c15]Jan-Georg Smaus:
Termination of Logic Programs for Various Dynamic Selection Rules. ICLP 2003: 511-512 - 2002
- [j3]Pierre Deransart, Jan-Georg Smaus:
Subject Reduction of Logic Programs as Proof-Theoretic Property. J. Funct. Log. Program. 2002 (2002) - [j2]Dino Pedreschi, Salvatore Ruggieri, Jan-Georg Smaus:
Classes of terminating logic programs. Theory Pract. Log. Program. 2(3): 369-418 (2002) - [c14]Jan-Georg Smaus:
The Head Condition and Polymorphic Recursion. FLOPS 2002: 259-274 - [c13]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:
MultiMedia Instruction in Safe and Secure Systems. WADT 2002: 82-117 - 2001
- [j1]Jan-Georg Smaus, Patricia M. Hill, Andy King:
Verifying Termination and Error-Freedom of Logic Programs with block Declarations. Theory Pract. Log. Program. 1(4): 447-486 (2001) - [c12]Annalisa Bossi, Sandro Etalle, Sabina Rossi, Jan-Georg Smaus:
Semantics and Termination of Simply-Moded Logic Programs with Dynamic Scheduling. ESOP 2001: 402-416 - [c11]Pierre Deransart, Jan-Georg Smaus:
Well-Typed Logic Programs Are not Wrong. FLOPS 2001: 280-295 - [c10]Jan-Georg Smaus:
Analysis of Polymorphically Typed Logic Programs Using ACI-Unification. LPAR 2001: 282-298 - [i6]Annalisa Bossi, Sandro Etalle, Sabina Rossi, Jan-Georg Smaus:
Semantics and Termination of Simply-Moded Logic Programs with Dynamic Scheduling. CoRR cs.LO/0101022 (2001) - [i5]Jan-Georg Smaus:
Analysis of Polymorphically Typed Logic Programs Using ACI-Unification. CoRR cs.LO/0105007 (2001) - [i4]Dino Pedreschi, Salvatore Ruggieri, Jan-Georg Smaus:
Classes of Terminating Logic Programs. CoRR cs.LO/0106050 (2001) - 2000
- [c9]Jan-Georg Smaus, François Fages, Pierre Deransart:
Using Modes to Ensure Subject Reduction for Typed Logic Programs with Subtyping. FSTTCS 2000: 214-226 - [c8]Pierre Deransart, Jan-Georg Smaus:
Les programmes bien typés ont tout bon. JFPLC 2000: 49-66 - [i3]Jan-Georg Smaus, Patricia M. Hill, Andy King:
Verifying Termination and Error-Freedom of Logic Programs with block Declarations. CoRR cs.LO/0006033 (2000) - [i2]Jan-Georg Smaus, François Fages, Pierre Deransart:
Using Modes to Ensure Subject Reduction for Typed Logic Programs with Subtyping. CoRR cs.LO/0010029 (2000) - [i1]Pierre Deransart, Jan-Georg Smaus:
Well-Typed Logic Programs Are not Wrong. CoRR cs.LO/0012015 (2000)
1990 – 1999
- 1999
- [b1]Jan-Georg Smaus:
Modes and types in logic programming. University of Kent, UK, 1999 - [c7]Andy King, Jan-Georg Smaus, Patricia M. Hill:
Quotienting Share for Dependency Analysis. ESOP 1999: 59-73 - [c6]Jan-Georg Smaus:
Proving Termination of Input-Consuming Logic Programs. ICLP 1999: 335-349 - [c5]Jan-Georg Smaus, Patricia M. Hill, Andy King:
Mode Analysis Domains for Typed Logic Programs. LOPSTR 1999: 82-101 - [c4]Sandro Etalle, Jan-Georg Smaus:
Preface - Workshop on Verification of Logic Programs. Verification of Logic Programs@ICLP 1999: 125 - [e1]Sandro Etalle, Jan-Georg Smaus:
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. Electronic Notes in Theoretical Computer Science 30(1), Elsevier 1999 [contents] - 1998
- [c3]Jan-Georg Smaus, Patricia M. Hill, Andy King:
Preventing Instantiation Errors and Loops for Logic Programs with Multiple Modes Using block Declarations. LOPSTR 1998: 289-307 - [c2]Jan-Georg Smaus, Patricia M. Hill, Andy King:
Termination of Logic Programs with block Declarations Running in Several Modes. PLILP/ALP 1998: 73-88 - 1997
- [c1]Jan-Georg Smaus, Patricia M. Hill, Andy King:
Domain Construction for Mode Analysis of Typed Logic Programs. ICLP 1997: 418
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from 
to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the 
of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from 
, 
, and 
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from 
.
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-11-08 21:31 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
