Jan‐Georg Smaus

Université Toulouse III - Paul Sabatier — France

Computer Science · Physical Sciences

11h-index343citations59works0.02yr avg
OpenAlex↗Google Scholar↗Lab page↗

Accepting Students?

No reports yet. Know if this professor is taking students?

Research Topics

Formal Methods in Verification(38), Logic, programming, and type systems(33), Logic, Reasoning, and Knowledge(23), Model-Driven Software Engineering Techniques(10), Software Testing and Debugging Techniques(7)

Publications59 total

Assignments and Strategies in Democratic Forking Analysed with
SPIRE - Sciences Po Institutional REpository·2026Open Access
Proving the Existence of Stable Assignments in Democratic Forking Using Isabelle/HOL
SPIRE - Sciences Po Institutional REpository·2024Open Access
Implementations of two Algorithms for the Threshold Synthesis Problem
arXiv (Cornell University)·2023Open Access
Modes and types in logic programming
Kent Academic Repository (University of Kent)·2022· 21 citedOpen Access
Existence of Nash Equilibria in Preference Priority Games Proven in Isabelle
SPIRE - Sciences Po Institutional REpository·2021Open Access
Existence of Nash Equilibria in 2-Player Simultaneous Games and Priority Games Proven in Isabelle
SPIRE - Sciences Po Institutional REpository·2021
Automated Invariant Generation for the Verification of Real-Time Systems
EPiC series in computing·2018· 2 citedOpen Access
An Existence Theorem of Nash Equilibrium in Coq and Isabelle
Electronic Proceedings in Theoretical Computer Science·2017· 6 citedOpen Access
Formalization of an existence theorem of Nash equilibrium in Coq and Isabelle (Journées FAC 2017)
HAL (Le Centre pour la Communication Scientifique Directe)·2017
Abstracting an Operational Semantics to Finite Automata
Communications in computer and information science·2016· 10 citedOpen Access
Büchi Automata Optimisations Formalised in Isabelle/HOL
Lecture notes in computer science·2014· 1 citedOpen Access
A Fully Verified Executable LTL Model Checker
2014· 4 cited
A Pretty Complete Combinatorial Algorithm for the Threshold Synthesis Problem
Lecture notes in computer science·2013
A Fully Verified Executable LTL Model Checker
Lecture notes in computer science·2013· 84 citedOpen Access
Model Checking and Artificial Intelligence
Lecture notes in computer science·2011
Reports of the AAAI 2010 Conference Workshops
AI Magazine·2010Open Access
Proceedings of the 6th international conference on Model checking and artificial intelligence
2010
Automated Predicate Abstraction for Real-Time Models
2009Open Access
Automated Predicate Abstraction for Real-Time Models
Electronic Proceedings in Theoretical Computer Science·2009· 3 citedOpen Access
Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL
Lecture notes in computer science·2009· 15 cited
page 1 of 3Next →

Frequent Co-authors

Pierre Deransart(6), Andy King(5), Sandro Etalle(5), Alexander Schimpf(4), Dino Pedreschi(3), Salvatore Ruggieri(3), Patricia M. Hill(3), Pat Hill(3), Annalisa Bossi(3), Sabina Rossi(3), Stefan Ratschan(3), François Fages(3), Bahareh Badban(3), Stefan Leue(3), Peter Lammich(2), René Neumann(2), Tobias Nipkow(2), Jörg Hoffmann(2), Stéphane Le Roux(2), Érik Martin-Dorel(2)