Research



Research Interests

I'm generally interested in formal methods for building dependable systems and understanding complex systems. With the help of fully automatic methods, we aim at proving properties that we want these systems to satisfy, inferring properties, that means discovering properties about systems whose behaviour is difficult to understand, or synthesising systems that satisfy given properties. Systems are modelled as discrete transition systems or differential equation systems or combinations thereof, so-called hybrid systems. This comprises any kind of deterministic or non-deterministic system from computer programs to physical systems, which can be combined to cyber-physical systems. The methods involved include techniques from static analysis and decision procedures (model checking, abstract interpretation, satisfiability solving, etc).

My research interests include in particular:

News

DiffBlue is hiring web developers and research engineers in automated formal verification. Read more...

Article accepted in TOPLAS: Bit-Precise Procedure-Modular Termination Analysis (joint work with Hong-Yi Chen, C David, Daniel Kroening, and Björn Wachter)

Article accepted in TECS: Effective Verification for Low-Level Software with Competing Interrupts (joint work with Lihao Liang, Daniel Kroening, Tom Melham, and Michael Tautschnig)

Paper accepted at ATVA'17: Lifting CDCL to Template-based Abstract Domains for Program Verification (joint work with Rajdeep Mukherjee, Leopold Haller, Daniel Kroening, and Tom Melham)

Paper accepted at ATVA'17: Concurrent Program Verification with Invariant-guided Underapproximation (joint work with Sumanth Prabhu, Mandayam Srivas, Michael Tautschnig, and Anand Yeoleka)

Paper accepted at ATVA'17: Compositional Safety Refutation Techniques (joint work with Kumar Madhukar and Mandayam Srivas)

Paper accepted at NSV'17: Sound Numerical Computations in Abstract Acceleration (joint work with Dario Cattaruzza, Alessandro Abate, and Daniel Kroening)

2LS successfully participated in the Software Verification Competition 2017.

Article accepted in FAOC: Incremental Bounded Model Checking for Embedded Software (joint work with Daniel Kroening, Martin Brain, Ruben Martins, Tino Teige, and Tom Bienmüller)


Software

2LS for Program Analysis

Incremental BMC

ChainCover - Test Case Generation for Reactive Systems

ReaVer - Reactive System Verifier

Peter
Schrammel



Biography



Teaching



Publications



Software