Software and Computational Systems Lab

Explicit Value Analysis with Symbolic Memory Graphs (SMGs) can analyse programs, including memory operations, fast and efficient. However, Value Analysis often over-approximates values beyond an already encountered bound. The goal is to combine the existing SMG based Value Analysis with the existing Numerical Abstract Domain (APRON) using a composite analysis, reusing the already existing components. This is then implemented in CPAchecker and evaluated against other verification approaches over the SV-COMP benchmark set.

JavaSMT is a framework that provides a common API for several SMT solvers. SMT solvers are capable of returning a proof for a verdict. These proofs however are different from solver to solver. The goal of this thesis is first an analysis of the different proofs returned by the solvers to develop a common interface, then implementing this in JavaSMT and finally connecting all possible SMT solvers to this interface (with automated tests and possible build documentation). This topic is suited for a bachelor's thesis

JavaSMT is a framework that provides a common API for several SMT solvers. However, some SMT solvers lack support for quantifier theory and quantifier elimination. UltimateEliminator bridges this gap by offering solver-independent quantifier elimination. The goal of this thesis is adding a solver-independent quantifier layer to JavaSMT and connecting UltimateEliminator to it, allowing all solvers to utilize quantifiers as long as they are eliminated in the end (with automated tests and build documentation). This topic is suited for a bachelor's thesis

JavaSMT is a framework that provides a common API for several SMT solvers. However, there are solver that do not offer parsing/dumping of formulas in the SMT2 format. The goal of this thesis would be the extension of our solver-independent SMT-LIB2 parser/generator layer in JavaSMT, that enables users to generate SMT2 formulas in String form using the API, but also read arbitrary SMT2 formulas into any of the existing solvers APIs without using the solvers parsing abilities. To evaluate this extension, we add a SMT solver using the parser/generator. This topic is suited for a bachelor's thesis