Publications

Stéphane Le Roux, Érik Martin-Dorel, Jan-Georg Smaus

An Existence Theorem of Nash Equilibrium in Coq and Isabelle

8th International Symposium on Games, Automata, Logics and Formal Verification (GandALF 2017), Sep 2017, Rome, Italy. pp.46-60, ⟨10.4204/EPTCS.256.4⟩

Accès: https://hal.science/hal-03434697

Stéphane Le Roux, Érik Martin-Dorel, Jan-Georg Smaus

Formalization of an existence theorem of Nash equilibrium in Coq and Isabelle (Journées FAC 2017)

Journées FAC 2017, Groupe IFSE du RTRA STAE, Mar 2017, Toulouse, France

Accès: https://hal.science/hal-03131861

Nadezhda Baklanova, Wilmer Ricciotti, Jan-Georg Smaus, Martin Strecker

Abstracting an Operational Semantics to Finite Automata

11th International Conference onICT in Education, Research, and Industrial Applications (ICTERI 2015), May 2015, Lviv, Ukraine. pp.109-123, ⟨10.1007/978-3-319-30246-1_7⟩

Accès: https://hal.science/hal-01782563

Alexander Schimpf, Jan-Georg Smaus

Büchi Automata Optimisations Formalised in Isabelle/HOL

6th Indian Conference on Logics and its Applications (ICLA 2015), Jan 2015, Mumbai, India. pp.158-169, ⟨10.1007/978-3-662-45824-2_11⟩

Accès: https://hal.science/hal-01782564

Javier Esparza, Peter Lammich, René Neumann, Tobias Nipkow, Alexander Schimpf, Jan-Georg Smaus

A Fully Verified Executable LTL Model Checker (regular paper)

Dans : International Conference on Computer Aided Verification (CAV 2013), Saint Petersbourg, 13/06/13-19/07/13, Vol. 8044, Helmut Veith, Natasha Sharygina (Eds.), Springer, LNCS, (en ligne), juillet 2013.

Résumé Accès : http://link.springer.com/chapter/10.1007%2F978-3-642-39799-8_31 – https://oatao.univ-toulouse.fr/12671/
BibTeX

Evgeny Dantsin, Jan-Georg Smaus, Sergei Soloviev

Algorithms in Games Evolving in Time: Winning Strategies Based on Testing Hypotheses

Dans : Isabelle Users Workshop of the International Conference on Interactive Theorem Proving, Princeton, USA, 12/08/12-12/08/12, Tobias Nipkow, Larry Paulson, Makarius Wenzel (Eds.).

Résumé
BibTeX

Jan-Georg Smaus, Christian Schilling, Fabian Wenzelmann

Implementations of two algorithms for the threshold synthesis problem

Dans : International Symposium on Artificial Intelligence and Mathematics, Fort Lauderdale, 09/01/12-11/01/12 (conférencier invité).

Résumé Accès : http://www.cs.uic.edu/pub/Isaim2012/WebPreferences/ISAIM2012_Boolean_Schilling_etal.pdf
BibTeX