3 Papers accepted at ISoLA'20: "An Interface Theory for Program Verification", "Verification Artifacts in Cooperative Verification", and "Violation Witnesses and Result Validation for Multi-Threaded Programs"

Karlheinz Friedberger

Picture of 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
E-Mail
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
Interpolants build from an arbitrary SMT solver (develop a layer into JavaSMT to get (tree) interpolants without explicit support of the solver e.g. from proofs or unsat cores) [1, 2, 3, 4]
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
CWE-Ids for Software Analysis in CPAchecker and SV-COMP (subtopic from 'Real-World Requirements for Software Analysis') [1, 2, 3, 4, 5, 6, 7]

The long description of the supertopic can be found under 'Real-World Requirements for Software Analysis'.
This subtopic is a specialization for finding and documenting CWE-Ids that match them against CPAchecker's analyses. The target is not as broad as the supertopic, but more related to our own software project. Plan:

  • Which CWE-Ids are supported by CPAchecker? Can we simply extend CPAchecker for a few more?
  • Can we describe CWE-Ids with a specification like the BLAST query language?
  • Does SV-COMP provide tasks for the found CWE-Ids?
  • Provide a nice overview (webpage?) for those CWE-Ids?
The thesis does not include much code-related work, but focuses more on literature research and documentation.

Predicate-based Analysis of Concurrent Programs [1, 2, 3]

Issue 464

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
Unify analyses (ValueAnalysis, IntervalAnalysis, SignAnalysis) in CPAchecker by using a common data-wrapper for numerical values (integers, bitvectors, floats, ...), optional: support for symbolic values, BDDs, and Octagons [1]
Define and evaluate different refinement approaches for interval domain or BDD domain (widening, splitting, interpolation, path prefixes) [1, 2, 3]
Symbolic Memory Graphs in CPAchecker [1, 2]
Multi-process architecture for BAM-parallel to provide cluster-based software analysis, maybe with central or shared database for reached states
Backwards analysis for CPAchecker, initially BDD- and predicate-based (both partially implemented somewhere), later symbolic and explicit analysis.
Parallel BDDs in Java (cf. Sylvan) [1]
SMT query caching, slicing, and simplification module for Java SMT [1]

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:

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

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

  • ESEC/FSE 2020: Domain-Independent Interprocedural Program Analysis using Block-Abstraction Memoization
  • ISoLA 2020: Violation Witnesses and Result Validation for Multi-Threaded Programs, pdf, supplementary website
  • 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