Falsification of Hybrid Systems Using Adaptive Probabilistic Search.

Sudeep Kanav

Picture of Sudeep Kanav

Software and Computational Systems Lab
Department of Computer Science
Ludwig-Maximilians-Universität München (LMU Munich)
Oettingenstraße 67
80538 Munich (Germany)

Room F 005, Oettingenstr. 67
+49 89 2180 9178
Office Hours
Tuesday, 15:00 – 16:00, or by appointment


Please send me encrypted mails!
My GPG key: 0xCDC40629
Fingerprint: 9789 7F83 5133 D9F6 D446 AEAD 2ED8 6F1D CDC4 0629

Thesis Mentoring

Currently assigned topics
Developing a Verifier Based on Parallel Portfolio with CoVeriTeam

CoVeriTeam is a framework to compose verification tools. We can compose different tools resulting in a verification tool. This thesis aims to construct a new verifier based on a composition of a few tools that solves more tasks than (most of) the verifiers participating in SVCOMP.
In this work, we aim to develop a verifier that is fast with respect to walltime (not cputime). This verifier will be a portfolio solver. We will develop a new kind of composition called portfolio in CoVeriTeam. This composition will make use of MPI technology to execute the processes on different machines.
evaluation: execute the composed verifier on the SVCOMP benchmarks and compare it with the participants in the walltime track competition. The implementation will be done in Python.

Topics on automatic program repair

Debugging software usually consists of three steps: 1. finding an error in the program, 2. finding the cause for that error (the fault), and 3. fixing that fault. By default, fixing the fault is done manually by a programmer, which often consumes vast amount of resources and may introduce new bugs. To ease that task, this topic is concerned with automatic program repair. After finding a potential fault in a program, automatic program repair proposes fixes and often checks the validity of these fixes. The goal is to implement and evaluate a technique for automatic program repair in C programs in the state-of-the-art verification framework CPAchecker. The complexity of the technique and the scope of the topic is based on the thesis type (project, bachelor or master). Programming is done in Java.

SV-comp Benchmarks for Weak Memory Models [1]

SV-Comp is the International Competition on Software Verification. It serves as a platform for the research community to evaluate tools targeting verification of C and Java programs. A total of 28 tools from 11 different countries participate in SV-Comp’20.

The simplest (and strongest) model of computation for concurrent programs is sequential consistency (SC), i.e. interleaving semantics. However, for performance reasons, mainstream processors perform optimisations that results in more possible executions than those allowed by SC. This new execution can result in bugs in the program which are hard to detect. All executions which are valid according to a certain processor are specified by its memory model.

We aim to create a new category in SV-Comp dealing with memory models. We currently have a collection of more than twelve thousand benchmarks that were used to validate the formalisation of the memory models of x86, Arm and Power processors and the Linux kernel. Those benchmarks are written in the litmus format, which is only supported by a small number of tools. The goal of this thesis is to port the benchmarks from the litmus format to C code. Dartagnan is a verification tool with support for memory model that can already parse all such benchmarks. What is required, is to implement an exporter from Dartagnan’s intermediate representation of programs to C.

Finished topics
Verification Witnesses: from Llvm to C [1]

Dartagnan is a software verification tool. It takes a C program, it compiles it to Llvm and then it performs the verification on the Llvm code. In 2020, Dartagnan participated for the first time in Sv-Comp, the International Competition on Software Verification. One of the requirements of Sv-Comp, is to provide verification witnesses: a proof of correctness or a counterexample. Dartagnan can already generate a counterexample witness as a graph. However, this graph refers to the Llvm code while Sv-Comp requires to generate a counterexample witness w.r.t to input C program. The information mapping the C instructions with the corresponding Llvm code is provided by the transformation from C to Llvm used by Dartagnan. However it is not currently used. The goal of this thesis is to use this information and convert the counterexamples generated by Dartagnan to witnesses w.r.t the C code, thus fulfilling Sv-Comp requirements.

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.