Seminar
Advanced Approaches in Software Verification (AASV)

The seminar deals with current research topics of the research group Semantics and Verification of Parallel Systems. You will learn about classical and recent research in the area of software verification (i.e., model checking, program analysis, testing, etc.). The current topics are listed below.

Seminar: Advanced Approaches in Software Verification (AASV)

Lecturer: Prof. Dr. Marie-Christine Jakobs

The seminar is no longer offered. The seminar dealt with current research topics of the research group Semantics and Verification of Parallel Systems. You will learn about classical and recent research in the area of software verification (i.e., model checking, program analysis, testing, etc.).

Course Content

Under the guidance of your supervisor you will

  • use the given literature and search for additional literature to become acquainted with your topic,
  • prepare and give a presentation about your topic and afterwards discuss the topic with the other participants,
  • write a scientific report, which provides a summary of your topic.

At the end of the seminar, students are able to autonomously familiarize themselves with a scientific topic and are able to present this topic to a heterogeneous audience orally and in written form.

More concrete, the students can search for scientific literature and assess the relevance of found literature. They are able to identify the main content of a scientific publication and critically evaluate them. Moreover, they can compare different scientific approaches. Students can explain and defend their topic and results to a heterogeneous audience in an oral presentation. Additionally, they are able to describe their topic and results in a scientific paper.

Previous Knowledge

Recommended. Knowledge about computer science and mathematics taught int the first four terms of the bachelor degree in computer science

Helpful. Participation in a course of the research group Semantics and Verification of Parallel Systems

Seminar Topics in Past Terms

This seminar is about intermediate languages and specification languages for supporting verification. Intermediate languages typically simplify the verifier design, e.g., restricting the language, mapping similar input statements to a single statement in the intermediate language, making implicit behavior explicit, etc. In contrast, specification languages allow one to specify properties of a program, e.g., its functional behavior, caller-callee contracts, etc..

Intermediate Languages

Specification Languages

Combined Intermediate and Specification Languages

This seminar is about tools for verification and analysis of software programs. The tools will differ in the supported programming languages and the underlying techniques for analysis and verification. To this end, we will look into the following tools.

Frameworks for Java Analyis

Frameworks for C Analysis

Verifiers for C Programs

Verifiers for Boogie Programs

This seminar studies topics on automatic test-case generation. The goal of test-case generation is to find test inputs that reveal bugs in the the program or to find a set of test inputs that achieve a certain coverage value. In this seminar, we look into four different types of automatic test-case generation: (1) random input generation, (2) search-based input generation, (3) input generation with symbolic execution, and (4) input generation with reachability analyses.

Random Test Generation

Search-based Test Generation

Test Generation with Symbolic Execution

Test Generation with Reachability Analyses

This seminar studies topics from our research area combination of validation of verification results. The goal of validation is to increase the trust in the validity of the result. Validation allows one to check that the verification was actually done and that the verification tool worked properly. In this seminar, we look into (1) protocols for validation, (2) validation techniques for several analyses like dataflow analysis, abstract interpretation, or model checking.

Validation Protocols

Validating Model Checking Results

  • Temporal Safety Proofs
    Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, George C. Necula, Grégoire Sutre, Westley Weimer: Temporal-Safety Proofs for Systems Code, CAV 2002.
  • Extreme Model Checking
    Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Marco A. A. Sanvido: Extreme Model Checking, Verification: Theory and Practice 2003.

Validating Dataflow Analysis and Abstract Interpretation Results

This seminar studies topics from our research area combination of verification approaches, especially we look into cooperative verification approaches. Cooperative verification approaches aim at leveraging the strengths of different verification approaches. We consider three types of cooperative verification approaches: (1) testification of alarms, (2) distribution of verification effort, and (3) algorithmic integration of different verification approaches.

The goal of alarm testification is the reduction of false alarms and to focus on alarms that can be reproduced by a real test.

To distribute the verification effort among different verification approaches, different parts of the verification (e.g., program paths) need to be inspected by distinct verification tools. Often, sequential combinations are used in which the follow-up tool only inspects the remaining proof obligations.

The algorithmic integration of different verification approaches idea is to develop new verification algorithms that use existing verification approaches as components.

Testification of Alarms

Distribution of Verification Effort

Algorithmic Integration of Different Verification Approaches

The seminar has been cancelled (reason: no participants). The seminar topics of this semester will therefore be discussed next semester.

This seminar studies topics from our research area incremental verification. Techniques in incremental verification are a key enabler for applying formal verification in modern software project. To deal with dozens of rapid changes, incremental verification techniques aim at a more efficient reverification of a modified program. For this purpose, incremental verification reuses information of a previous verification run. The kind of information and its use distinguish the different approaches. In this seminar, we look at four different classes of incremental verification: functional equivalence checking, reuse of intermediate results, proof adaption, and skipped verification.

In functional equivalence checking, it is verified that modified program parts show the same input/output behavior as the part before the verification.

Techniques reusing intermediate results avoid reexploration of known results, e.g., invariants, satisfiability results, or abstraction level. Their assumption is that a large portion of the intermediate results is still valid and needed for the verification of the modified program.

Approaches for proof adaption check which proof parts remain valid and perform a verification step for invalid proof parts.

The fourth class skipped verification is related to the class of proof adaption. Techniques in this class stop verification as soon as modification can be reached or perform a lightweight verification as long as no modification has been reached.

Functional Equivalence Checking

Reusing Intermediate Results

Proof Adaption

Skipped verification