We have various topics for BSc, MSc and PhD theses.
If you are interested in writing a thesis in the group, just contact us.
Area: Study theories for which complete instantiation method exists:
Most of the algorithms for checking satisfiability modulo theories were devised for being used for ground formulae. Therefore, the state-of-the-art SMT solvers with support for quantifiers use heuristics for quantifier instantiation. Such heuristics are in general sound but incomplete: if a contradiction is derived after instantiating a set N of clauses, then N is clearly unsatisfiable. However, if no contradiction can be derived after instantiation we do not know anyting about the satisfiability of N (it could happen that not all instantiations needed for deriving a contradiction were considered). It is therefore important to identify classes of theories for which complete instantiation methods exists, i.e. in which we can characterize the set of instances which are necessary and sufficient for deriving a contradiction in case of unsatisfiability. The advantage of having a complete instantiation method is that if unsatisfiability cannot be derived from the set of instances of N, we have the guarantee that the set N of quantified clauses is satisfiable. In fact, we often can effectively construct a model of N from a model of its set of instances.
Topics for PhD theses are available in the following areas:
- Automated reasoning and applications
Verification (reactive and real time systems/hybrid systems)
- Ontologies/description logics
If you are interested in a thesis in one of the areas above (or in related areas) please contact Viorica Sofronie-Stokkermans
Topics for BSc and/or MSc theses:
1. Recognize theories with complete instantiation
The goal is to obtain systematic ways of recognizing theories for which complete instantiation methods exist: - Semantic criteria - Syntactic criteria (automatically recognize formulae in the array property fragment; pointer fragment, boundedness, monotonicity, ...) - Other criteria (to be discussed) - Saturation under ordered resolution and to use these results for systematically investigating the complete instantiation schemata for classes of theories.
2. Model generation:
Starting from a theory for which a complete instantiation schema is known, we would like to obtain ways of constructing models for satisfiable sets of (quantified) formulae. The challenge here would be to obtain means of synthetically and finitely representing potentially infinite models. Such examples can be used as counterexamples e.g, in mathematics, or as examples of systems with undesired unsafe behavior, for instance in verification.
Remark: Topics 1 and 2 can be considered together (for a BSc/MSc thesis)
BSc thesis on this topic already assigned.
3. Parametric verification and quantifier elimination:
The hierarchical reasoning method in theory extensions which we proposed, allows not only to check the satisfiability of a given set of constraints. We can also consider parametric problems (in which some of the constants which appear can be considered to be parametric) and generate constraints on the parameters which guarantee the satisfiability/unsatisfiability of certain formulae. This is extremely useful e.g. in program verification and design, as well the verification and design of parametric real time or hybrid systems.
4. Programming project: Reasoning in extensions and combinations of theories and applications (logic, verification, databases)
5. Programming project: Interpolant generation.
Interpolants are explanations for unsatisfiability of conjunctions of formulae A, B containing only logical symbols used in both A and B;they are nowadays widely used in verification and databases. We identified ways for efficiently computing interpolants in various theories. The goal of this project/thesis is to implement these methods.