IRIT - UMR5505

Jan-Georg 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 since 2001. 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üchi-automata and temporal logic is verified using interactive theorem proving. This work was done in the CAVA project.
- In 2011 I have started to study applications of interactive theorem proving to programming language semantics and to game theory.
Between 2004 and 2011, I did 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 pseudo-Boolean constraints. A linear pseudo-Boolean 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 input-consuming 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 well-typed 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 proof-theoretic 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 ACI-unification.






		Jan-Georg 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 since 2001. 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üchi-automata and temporal logic is verified using interactive theorem proving. This work was done in the CAVA project. In 2011 I have started to study applications of interactive theorem proving to programming language semantics and to game theory. Between 2004 and 2011, I did 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 pseudo-Boolean constraints. A linear pseudo-Boolean 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 input-consuming 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 well-typed 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 proof-theoretic 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 ACI-unification.