### Karlheinz Friedberger

Software and Computational Systems Lab

Institute for Informatics

Ludwig-Maximilians-Universität München (LMU Munich)

Oettingenstraße 67

80538
Munich
(Germany)

- Office
- Room F 009, Oettingenstr. 67
- Phone
- +49 (89) 2180-9182
- firstname.lastname@ifi.lmu.de

#### GPG-Key

Please send me encrypted mails!

My GPG key: 0xACCD6DC1

Fingerprint: 8C88 203A 21B7 5B34 78E3 DAFB 4D6D 84D3 ACCD 6DC1

#### Thesis Mentoring

## Available topics

## Fuzzing for SMT Solvers on API Level [1, 2]

Formal methods use SMT solvers extensively for deciding formula satisfiability. However, solvers may contain critical bugs that lead to unsound results. We can use tools for mutation-based fuzzing on our own API and the underlying SMT solvers. We can report bugs back to the developers and update JavaSMT with fixed solver libraries or bindings.

## Currently assigned topics

## JavaSMT: integrate a new solver (with automated tests and build documentation). Possible candidates: ~~CVC4~~, ~~Boolector~~, ~~OpenSMT~~, ~~STP~~, ~~Yices~~,...

JavaSMT is a framework that provides a common API for several SMT solvers. Adding support for an additional solver is straightforward. However, JavaSMT is written in Java, while most solvers are written in C or C++. This means one usually has to write bindings using the Java Native Interface. This topic is suited for a bachelor's thesis

## Implementing a fast SMT Solver based on interval-computation [1]

An SMT formula is a boolean formula that includes numbers and common arithmetic operations. Since formal verification techniques often use SMT formulas to represent programs and models , the speed of solving SMT formulas is a very important aspect of formal verification. Studies show that SMT formulas that are created by model checkers or symbolic execution often have a specific structure: The relation between program variables (e.g., "x == y + z") is dependent on program constraints over these variables that only contain a single variable each, e.g., x > 0, y > 0, and z > 10. This example would be represented as the SMT formula x == y + z ∧ x > 0 ∧ y > 0 ∧ z > 10.

The satisfiability of SMT formulas with this specific structure can be computed through the following decision procedure:

1. For each program variable in the formula, compute the interval(s) of possible values for this variable for which the constraints of this variable are satisfied, and

2. Check whether the relations between program variables can be satisfied with the computed intervals.

The goal of this topic is to implement this procedure and to make it available as a Java library. Work on this in the symbolic execution engine Klee has shown great potential, leading to speedups of up to 55x compared to the use of existing complete SMT solvers.

## Finished topics

## BDD support in JavaSMT, e.g. add Regions/RegionManager or even something like Q3B to JavaSMT [1, 2, 3]

JavaSMT is a framework that provides a common API for several SMT solvers. For certain problem types, BDDs can be used as a replacement of SMT solvers, as demonstrated by Q3B. The verifier CPAchecker too contains an abstraction layer (Regions/RegionManager) that enables switching between solver and BDDs, while it uses JavaSMT to be able to switch between different solvers. Ideally, the code can be refactored such that the switching between SMT solver and BDD is moved from CPAchecker to JavaSMT. The goal is NOT to add Q3B to the list of solvers supported by JavaSMT, but rather have our own implementation that takes the Regions/RegionManager of CPAchecker as starting point.

If you're a student interested in writing your thesis at our chair, you should also have a look at our full list of currently available theses.

#### Teaching & Organization

LMU Munich:

- WS 2019/20: Softwaretechnik (Übung)
- SS 2019: Praktikum "SEP: Java-Programmierung"
- WS 2018/19: Softwaretechnik (Übung)
- SS 2018: Praktikum "SEP: Java-Programmierung"
- WS 2017/18: Softwaretechnik (Übung)
- SS 2017: SWEP

University of Passau:

- WS 2016/17: Programmierung 2 (Übung)
- SS 2016: Software Engineering (Übung), Sommercamp Informatik
- WS 2015/16: Programmierung 2 (Übung), Entwurfsautomatisierung (Übung)

#### Projects

- CPAchecker
- JavaSmt
- BenchExec
- VerifierCloud
- Evaluation of Tools at the Competitions on Software Verification 2012, 2013, 2014, and 2015

#### Publications, Presentations, and Co (List at SoSy-Lab, List at DBLP)

- ISoLA 2018: In-Place vs. Copy-on-Write CEGAR Refinement for Block Summarization with Caching, pdf, slides, supplementary website
- CPA 2018: Domain-Independent Multi-threaded Software Model Checking, slides
- ASE 2018: Domain-Independent Multi-threaded Software Model Checking, pdf, supplementary website
- AVM 2017: Block-Abstraction Memoization with CEGAR (In-Place vs. Copy-On-Write Refinement), poster
- CPA 2017: Block Abstraction Memoization with Copy-On-Write Refinement, slides
- TACAS 2017: CPAchecker for Reachability, Memory Safety, Overflows, Concurrency, and Termination (Competition Contribution), poster
- TACAS 2017: CPA-BAM-BnB: Block-Abstraction Memoization and Region-Based Memory Models for Predicate Abstractions (Competition Contribution), doi
- MEMICS 2016: A Light-Weight Approach for Verifying Multi-Threaded Programs with CPAchecker, doi, pdf
- CPA 2016: A Light-Weight Approach for Verifying Multi-Threaded Programs with CPAchecker, slides
- RERS 2016:
Gold medal in
*Reachability Plain*and silver medal in*Reachability Arithmetic*, results - VSTTE 2016: JavaSMT: A Unified Interface for SMT Solvers in Java, doi, project
- TACAS 2016: CPA-BAM: Block-Abstraction Memoization in CPAchecker (Competition Contribution), doi, pdf, slides
- Master's Thesis 2015: Block-Abstraction Memoization as an Approach to Verify Recursive Procedures, pdf
- HVC 2013: Domain Types: Abstract-Domain Selection Based on Variable Usage, doi, pdf
- Bachelor's Thesis 2012: Ein typbasierter Ansatz zur Kombination verschiedener Verifikationstechniken, pdf