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.

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.

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.)

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

NapSAT is a prototypical SAT solver developed for fast design and implementation of advanced backtracking algorithms. As such, it is equipped with an observer module able to display and replay the solver’s execution. We are searching for a bachelor student proficient with C++ to generalize and improve this architecture.

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.

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.

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)

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.

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.

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.