Peter Schrammel


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.



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)



DiffBlue - AI for Code