6 citations · 9 across the 8 of their papers we have counts for
9 papers
Implementations of two Algorithms for the Threshold Synthesis Problem
Jan-Georg Smaus, Christian Schilling, Fabian Wenzelmann
A linear pseudo-Boolean constraint (LPB) is an expression of the form , where each is a literal (it assumes the value 1…
An Existence Theorem of Nash Equilibrium in Coq and Isabelle
Stéphane Le Roux, Érik Martin-Dorel, Jan-Georg Smaus
Nash equilibrium (NE) is a central concept in game theory. Here we prove formally a published theorem on existence of an NE in two proof assistants, Coq and Isabelle: starting from…
Abstracting an operational semantics to finite automata
Nadezhda Baklanova, Wilmer Ricciotti, Jan-Georg Smaus +1
There is an apparent similarity between the descriptions of small-step operational semantics of imperative programs and the semantics of finite automata, so defining an abstraction…
Automated Predicate Abstraction for Real-Time Models
Bahareh Badban, Stefan Leue, Jan-Georg Smaus
We present a technique designed to automatically compute predicate abstractions for dense real-timed models represented as networks of timed automata. We use the CIPM algorithm in…
Analysis of Polymorphically Typed Logic Programs Using ACI-Unification
Jan-Georg Smaus
Analysis of (partial) groundness is an important application of abstract interpretation. There are several proposals for improving the precision of such an analysis by exploiting t…
Semantics and Termination of Simply-Moded Logic Programs with Dynamic Scheduling
Annalisa Bossi, Sandro Etalle, Sabina Rossi +1
In logic programming, dynamic scheduling refers to a situation where the selection of the atom in each resolution (computation) step is determined at runtime, as opposed to a fixed…