

JanGeorg Smaus
Research
Most of the research has been done in collaboration with
various colleagues.

Through my teaching, I have been involved with the field of
interactive theorem proving for around ten years.
Around 2008 I
started doing research in this field.

The link to model checking: In one work, part of a model
checking procedure for Büchiautomata and temporal logic is
verified using interactive theorem proving. This work will be continued in the
CAVA project.

Recently I have started to study applications of interactive theorem proving to
programming language semantics and to game theory.

Since 2004 I have done research in timed and hybrid systems, and
related areas, within the
AVACS project.
 Heuristic Search in Timed Automata.
I am interested in applying ideas coming from artificial intelligence
to model checking of timed automata. In artificial intelligence,
heuristics have proven very useful for doing search. In model
checking, similar techniques can be applied for generating heuristics
that will speed up the search for suitably specified error states of a
timed automata system.
 Finding error paths in hybrid systems.
Although technically somewhat different, the aim of this
line of research is the same as for timed automata: finding
error trajectories. For this aim, I use simulations guided
by abstractions that were originally conceived for
verification purposes.
 Linear pseudoBoolean constraints.
A linear pseudoBoolean constraint (LPB) is a
generalisation of a propositional clause.
I am interested in analysing the expressiveness of LPBs
thoroughly. Among other results, I have developed a combinatorial algorithm that
will transform a propositional formula into an LPB if this is
possible, a problem which has been open for more than 30 years.

Until 2004 my interests were mainly in logic programming.
 Verification of logic programs with dynamic scheduling.
In logic programming, dynamic scheduling refers to the situation
that an atom is selected in each step of program execution
by some criteria related to the instantiation of the atom,
rather than simply always selecting the leftmost atom as is
the standard. I have contributed methods for ensuring and proving
termination and other correctness properties in this
context. In particular, I have developed the notion of
inputconsuming derivations which is more abstract
and more amenable to a theoretic analysis than the
directives used in concrete programming languages.
I have written surveys on termination of logic
programs depending on the selection rule.
 Typed logic programming languages.
I have worked on typed logic programming languages
such as Gödel or Mercury. In particular I have studied
subject reduction, i.e. the property that only welltyped
queries can occur in the computation of a typed program. I am
interested in how this property can be regarded as a property of the
prooftheoretic semantics of a program, and how the property can be
obtained for systems allowing for subtyping.
In another work, I investigated the relationship between
typing and recursion in both logic and functional programming.
 Mode analysis of typed logic programs.
I have developed methods for characterising the degree of
instantiation of variables based on the types of a program
(mode analysis). In particular, one can analyse how the
instantiation of variables proceeds during program execution
by running the program on a special abstract domain and
replacing ordinary unification with ACIunification.

