Research
As PDF file (contains citations).
Most of the research has been done in collaboration with various colleagues.
-
Until 2004 my interests were mainly in logic programming.
- Verification of logic programs with dynamic scheduling. My first work in this area was on programs using delay declarations, in particular, proving termination and absence of runtime errors for such programs. I have developed a more abstract view of dynamic scheduling by defining the so-called input-consuming derivations. More powerful termination conditions were found later. Recently, I have investigated input-consuming derivations with additional assumptions on the selection rule. I have written surveys on termination of logic programs depending on the selection rule.
- Prescriptive Typing. I have worked on logic programming languages that use ``prescriptive'' types, 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 prescriptive typing and recursion in both logic and functional programming.
- Mode analysis of typed logic programs. I have developed an automatic domain construction for mode analysis of typed logic programs. I have later recast this domain construction by embedding it in an analysis framework based on ACI-unification.
- The ``Computation as Deduction'' Paradigm. Krzysztof Apt has proposed a new approach to using first order logic as a programming language, based on analogies between logic concepts and features in imperative programming languages. Together we have written an article comparing this approach with logic programming. I have written an article discussing the optimality of a semantics of first-order equations, which is at the heart of Apt's approach.
- Domains of propositional formulae in abstract interpretation. I have investigated the classic abstract domains such as Pos, Def and Share and the relationship between them.
-
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 state of a timed automata system.
- Finding error paths in hybrid systems. The behaviour (flow) of real variables in hybrid systems over time is usually described by differential equations. Falsifying a hybrid system, i.e., give an actual trajectory over time that will lead to a suitably specified error state, is usually difficult since the solutions to the differential equations are trigonometric functions and the like. However, for non-deterministic systems, falsification is often easier because one can find error paths where the flows are described by polynomials or even piecewise linear functions.
- Linear pseudo-Boolean constraints. A linear pseudo-Boolean constraint (LPB) is a generalisation of a propositional clause. It has been said that LPBs can be used to represent Boolean functions more compactly than the well-known conjunctive or disjunctive normal forms. I am interested in analysing the expressiveness of LPBs more thoroughly. Among other results, I have developed an algorithm that will transform a propositional formula into an LPB if this is possible
