This project involves the following possible topics in the area of string solving:

• investigating reduction or simplification rules for extended string operations,
• optimisation of regex (including simplifying regex in general or skipping redundant cases in terms of regex membership constraints solving),
• algorithmic improvements of the string/Nielsen datastructures (efficiently detecting unit propagation cases, tracking integer lengths, variable substitution, etc.)

Operators that are associative and commutative (in short AC) often show up in logical formulations, but their naive handling can be very explosive in saturation-based proof search. The goal of this project is to implement and combine existing simplifications in Vampire to handle AC (associative-commutative) symbols efficiently, or devise new approaches.

Master thesis: Combine Dafny and the Vampire theorem prover to enable deductive program synthesis directly inside Dafny. Transform method signatures with specifications into forall-exists benchmarks. Adapted speification is given to the built-in synthesis tool of Vampire which returns a witness. The interface returns output of Vampire in Dafny code.

Working on implementation of program synthesis tool within Vampire. In particular, implementation of manualy solved number theoretic synthesis problem that make use of well-founded induction. Possible to compare results with program synthesis tool of Snark, a theorem developed at Stanford Research International.

Finding compact representations of pseudo-Boolean polynomials is important for efficient reasoning in verification and optimization. This thesis/project studies how to represent integer pseudo-Boolean polynomials using flipped variables in order to obtain the shortest equivalent formulation.

Subsumption and subsumption resolution are critical simplification rules in state-of-the-art theorem provers. Both of these inferences are known to be NP-Complete, leading to the natural use of a SAT solver for detectign this sorts of redundancy. The current implementation in Vampire performs subsumption checks, one clause pair at a time.

We are searching for a bachelor/master student, with some familiarity with C++ programming, to investigate the benefits of bundling the queries into one larger SAT call.

Higher-order logic (i.e. the lambda calculus) is one of the most prominent new directions in saturation-based theorem proving, with Vampire being one of the most successful forerunners in this direction (see the THF division of CASC). Yet, Vampire lacks the efficient higher-order adaption of some essential simplification techniques, such as subsumption or demodulation; or efficient higher-order-specific simplifications such as beta-eta reduction or argument pruning. The aim of this project is to explore simplification techniques that advance the higher-order reasoning capabilities of Vampire.

NapSAT is a research SAT solver designed to support multiple backtracking strategies. This project aims at implementing missing state-of-the-art techniques to make NapSAT more competitive and analyze their impact on backtracking variants. We are searching for a master student familiar with C++ and eager to learn sharp and precise algorithms and adapt them in a medium size solver.

Automatically generating synthesis benchmarks from existing benchmark sets by existentially quantifying subterms. Evaluation of different tools using original benchmarks and modified synthesis benchmarks.

Circuit verification is a key bottleneck in modern hardware design. This project/thesis explores how machine learning can support automated reasoning techniques used in verification, e.g., by guiding solvers or improving reasoning over circuit constraints.

This project builds upon theoretic results of a deductive program synthesis framework. In particular the research is about completeness results of deductive program synthesis including induction with respect to realizability conditions. (Master thesis)

Side channel attacks are a powerful class of attacks that exploit information leaked by the physical implementation of a system. In this project, we will study how to verify the probe resistance of randomized hardware designs using Boolean polynomials. The theoretical foundations of this approach have already been developed. The goal of this project is to implement a prototype tool and evaluate its performance on a set of benchmark circuits.

We are searching for a student with good programming skills (preferably C++). The project is divided into four main tasks

1. Implementing or adapting a Boolean polynomial manipulation library.
2. Implementing a polynomial theory for a mini SMT solver.
3. Combining the theory solver with a SAT solver to solve formulas with propositional structure.
4. Encode the probe-isolating non-interference property using the previously developed tools and evaluate the performance of the tool on a set of benchmark circuits.

A bachelor thesis is expected to achieve the first two tasks, while a master thesis is expected to achieve all four tasks.