Publications

My research is at the intersection of software engineering and artificial intelligence, i.e. methods for the automation of software engineering.

This requires techniques for automatically learning and understanding the behavior of complex systems on the one hand and techniques for automatically building dependable systems on the other hand. The former means discovering or inferring properties about systems whose behavior we want to be explained; the latter means synthesizing systems that satisfy given properties. Verification is the act of proving the properties that we wanted a built system to satisfy.

My research extends from pure software systems to cyber-physical systems, i.e. combinations of software and physical systems, described by differential equation systems.

The methods involved include techniques from static analysis and decision procedures (model checking, abstract interpretation, satisfiability solving, etc).

Google Scholar
DBLP
Sussex Research Online
Scopus

Activities


Paper accepted at ASE'22: CBMC-SSM: Bounded Model Checking of C Programs with Symbolic Shadow Memory (joint work with Bernd Fischer, Salvatore La Torre, and Gennaro Parlato)

Oxford Artificial Intelligence Meetup: Writing Better Java Unit Tests with AI

Verification seminar talk at IIT Delhi, India: Parallel Bug-finding in Concurrent Programs via Reduced Interleaving Instances

JBMC finished second in the Java-Overall category in the Software Verification Competition 2022.

2LS successfully participated in the Software Verification Competition 2022.


Guest lecture on Static Security Analysis, Security module, University of Manchester, UK

JBMC finished third in the Java-Overall category in the Software Verification Competition 2021.

2LS successfully participated in the Software Verification Competition 2022.

Reviewer for ACM Transactions on Software Engineering and Methodology

Reviewer for Information and Software Technology journal


Tutorial at A-Test 2020 on Diffblue Cover (co-located with ESEC/FSE 2020)

Invited Talk at FMCAD 2020 How testable is business software?

Student Forum Chair of FMCAD 2020

Co-PC Chair of Numerical Software Verification, NSV 2020 co-located with CAV'20

Article accepted for Journal of Automatic Reasoning: Unbounded-Time Safety Verification of Guarded LTI Models with Inputs by Abstract Acceleration (joint work with Dario Cattaruzza, Alessandro Abate, and Daniel Kroening)

Reviewer for ICALP

JBMC finished second in the Java-Overall category in the Software Verification Competition 2020.

2LS successfully participated in the Software Verification Competition 2020.


Guest lecture on Automating Software Quality, Advanced Software Engineering module, University of Sussex, UK

Atlas lecture at University of Manchester: How Automated Tools Change the Way We Write Code

PC member of VSTTE'19

JBMC won the Java-Overall category in the Software Verification Competition 2019.

2LS successfully participated in the Software Verification Competition 2019.

Talk at ETAPS 2019 TOOLympics: JBMC: Bounded Model Checking for Java Bytecode (joint work with Lucas Cordeiro and Daniel Kroening)

Reviewer for STTT

Reviewer for INDIN'19

Reviewer for Journal for Engineering Science and Technology


External examiner of PhD thesis of Mikhail Ramalho Gadelha: Scalable and Precise Verification based on k-induction, Symbolic Execution and Floating-Point Theory, University of Southampton, UK

Seminar Talk at CMI: Template-Based Verification of Heap-Manipulating Programs

Viva voce of PhD thesis of Kumar Madhukar: Scalable Safety Verification of Statechart-like Programs, Chennai Mathematical Institute, India (co-supervised together with Mandayam K. Srivas)

Guest lecture on Automating Software Quality, Advanced Software Engineering module, University of Sussex, UK

Talk at JPF@ESEC/FSE'18: Benchmarking of Java Verification Tools at the Software Verification Competition (SV-COMP)

Royal Academy of Engineering SME Leader Programme

Paper accepted at JPF@ESEC/FSE'18: Benchmarking of Java Verification Tools at the Software Verification Competition (SV-COMP) (joint work with Lucas Cordeiro and Daniel Kroening)

Paper accepted at FMCAD'18: Template-Based Verification of Heap-Manipulating Programs (joint work with Viktor Malik, Martin Hruska, and Tomas Vojnar)

Talk at CAV'18: JBMC: A Bounded Model Checking Tool for Verifying Java Bytecode

Talk at WST'18: Procedure-Modular Termination Analysis

Research visit with Mandayam K. Srivas, Chennai Mathematical Institute, India

PC member of VSTTE'18

2LS successfully participated in the Software Verification Competition 2018.

Invited Talk at VSSE'18: How Automated Tools Change the Way We Write Code

Paper accepted at CAV'18: JBMC: A Bounded Model Checking Tool for Verifying Java Bytecode (joint work with Lucas Cordeiro, Pascal Kesseli, Daniel Kroening and Marek Trtik)

Reviewer for EURASIP Journal on Embedded Systems

Reviewer for Journal of Systems and Software


Paper accepted at TACAS'18: 2LS: Memory Safety and Non-termination - Competition Contribution (joint work with Viktor Malík, Stefan Marticek, Mandayam K. Srivas, Tomás Vojnar, Johanan Wahlang)

Fellow of the UK Higher Education Academy (AdvanceHE)

Article accepted for Transactions on Embedded Computing Systems: Effective Verification for Low-Level Software with Competing Interrupts (joint work with Lihao Liang, Daniel Kroening, Tom Melham, and Michael Tautschnig)

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

Talk at ATVA'17: Lifting CDCL to Template-Based Abstract Domains for Program Verification

Research visit with Mandayam K. Srivas, Chennai Mathematical Institute, India

Reviewer for AFFORD'17

Reviewer for FMSD

Received £99k EPSRC Grant on Efficient Software Verification by Reasoning about Abstractions

Reviewer for ICECCS

Paper accepted at ASE'17: Parallel bug-finding in concurrent programs via reduced interleaving instances (joint work with Truc L. Nguyen, Bernd Fischer, Salvatore La Torre and Gennaro Parlato)

Reviewer for Transactions on Software Engineering

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)

PC member of VSTTE'17

Reviewer for SAS'17

2LS successfully participated in the Software Verification Competition 2017.

Associate Fellow of the UK Higher Education Academy (AdvanceHE)

Reviewer for CAV'17


Reviewer for Journal Formal Aspects of Computing

Guest lecture on Automating Software Quality, Advanced Software Engineering module, University of Sussex, UK

Tutorial at FM'16: The CProver Suite of Verification Tools (with Martin Brain)

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

Paper accepted at ASE'16: Sound Static Deadlock Analysis for C/Pthreads (joint work with Daniel Kroening, Daniel Poetzl, and Björn Wachter)

Reviewer for CDC'16

Talk at NFM'16: Assisted Coverage Closure

Seminar Talk at University of Southampton: Safety Verification and Refutation by k-invariants and k-induction

Reviewer for FMCAD'16

2LS successfully participated in the Software Verification Competition 2016 and won a gold medal in the Floats category.

Talk at HCVS'16: Challenges in Decomposing Encodings of Verification Problems

Paper accepted at NFM'16: Assisted Coverage Closure (joint work with Adam Nellis, Pascal Kesseli, Philippa Ryan Conmy, Daniel Kroening and Michael Tautschnig)

Reviewer for NFM'16

Reviewer for ISSTA'16


Paper accepted at TACAS'16: 2LS for Program Analysis - Competition Contribution (joint work with Daniel Kroening)

Paper accepted at DATE'16: Unbounded safety verification for hardware using software analyzers (joint work with Rajdeep Mukherjee, Daniel Kroening and Tom Melham)

Received £75k Oxford University Innovation Grant on Industrial impact of Verification of Evolving Software (with Daniel Kroening)

Reviewer for TACAS'16

Reviewer for FASE'16

Seminar Talk at ONERA: Safety Verification and Refutation by k-invariants and k-induction

Talk at ASE'15: Synthesising Interprocedural Bit-Precise Termination Proofs

Invited Talk at EMSOFT'15: Unbounded-time reachability analysis of hybrid systems by abstract acceleration

Reviewer for Journal Logical Methods in Computer Science

Talk at SAS'15: Unbounded-Time Analysis of Guarded LTI Systems with Inputs by Abstract Acceleration

Talk at SAS'15: Safety Verification and Refutation by k-Invariants and k-Induction

Reviewer for ICCD'15

Reviewer for ICCECS'15

Tutorial at CADE'15: From Programs to Logic: The CPROVER verification tools (with Martin Brain)

Artifact Evaluation Committee member for POPL'16

Talk at FMICS'15: Successful Use of Incremental BMC in the Automotive Industry

Reviewer for Journal of Systems and Software

Reviewer for Journal Science of Computer Programming

Paper accepted at ASE'15: Synthesising Interprocedural Bit-Precise Termination Proofs (joint work with Hong-Yi Chen, Cristina David and Daniel Kroening)

Reviewer for FMCAD'15

Paper accepted at SAS'15: Safety Verification and Refutation by k-Invariants and k-Induction (joint work with Martin Brain, Saurabh Joshi and Daniel Kroening)

Paper accepted at SAS'15: Unbounded-Time Analysis of Guarded LTI Systems with Inputs by Abstract Acceleration (joint work with Dario Cattaruzza, Alessandro Abate and Daniel Kroening)

Paper accepted at FMICS'15: Successful Use of Incremental BMC in the Automotive Industry (joint work with Daniel Kroening, Martin Brain, Ruben Martins, Tino Teige and Tom Bienmüller)

Reviewer for TGC'15

Reviewer for CAV'15

Article accepted for STTT: Generating Test Case Chains for Reactive Systems (joint work with Tom Melham and Daniel Kroening)


Article accepted at DATE'15: Effective Verification of Low-Level Software with Nested Interrupts (joint work with Lihao Liang, Daniel Kroening, Tom Melham, and Michael Tautschnig)

Received £35k Impact Acceleration Grant on Industrial impact of C/C++ formal verification tools through plug-ins for the Eclipse IDE (with Daniel Kroening)

Talk at SAS'14: Speeding Up Logico-Numerical Strategy Iteration

Reviewer for Oxford Computer Journal

Reviewer for VMCAI'14

Talk at Dagstuhl Seminar on Decision Procedures and Abstract Interpretation 2014: Inferring Invariants by Strategy Iteration

Paper accepted at APLAS'14: Necessary and Sufficient Preconditions via Eager Abstraction (joint work with Mohamed Nassim Seghir)

Reviewer for Journal Nonlinear Analysis: Hybrid Systems

Paper accepted at ASE'14: Accelerated test execution using GPUs (joint work with Ajitha Rajan, Subodh Sharma and Daniel Kroening)

Reviewer for MEMOCODE'14

Paper accepted at SAS'14: Speeding Up Logico-Numerical Strategy Iteration (joint work with David Monniaux)

Reviewer for CAV'14

Reviewer for IJCAR'14

Article accepted for Journal Science of Computer Programming: Abstract acceleration in linear relation analysis (joint work with Laure Gonnord)

Reviewer for DATE'14

Talk at POPL'14: Abstract Acceleration of General Linear Loops


Paper accepted at ESOP'14: Model and Proof Generation for Heap-Manipulating Programs (joint work with Martin Brain, Cristina David and Daniel Kroening)

Talk at ICTSS'13: Chaining Test Cases for Reactive System Testing

Invited Talk at Intel European Research and Innovation Conference 2013: Automated Firmware Verification

Paper accepted at POPL'14: Abstract Acceleration of General Linear Loops (joint work with Bertrand Jeannet and Sriram Sankaranarayanan)

Reviewer for ICCD'13

Reviewer for DIFTS'13

Paper accepted at ICTSS'13: Chaining Test Cases for Reactive System Testing (joint work with Tom Melham and Daniel Kroening)

Reviewer for SAT'13

Reviewer for ESEC-FSE'13

Talk at VMCAI'13: Logico-Numerical Max-Strategy Iteration


Reviewer for HSCC'13

PhD Defense / Soutenance: Méthodes logico-numériques pour la vérification des systèmes discrets et hybrides. (Logico-Numerical Verification Methods for Discrete and Hybrid Systems)

Paper accepted at VMCAI'13: Logico-Numerical Max-Strategy Iteration (joint work with Pavle Subotic)

Reviewer for Journal Simulation Modelling Practice and Theory

Talk at HSCC'12: From Hybrid Data-Flow Languages to Hybrid Automata: A Complete Translation

Reviewer for DATE'12

Research visit with Sriram Sankaranarayanan, UC Boulder, US


Seminar Talk at LSV: Logico-Numerical Abstract Acceleration and Application to the Verification of Data-Flow Programs

Paper accepted at HSCC'12: From Hybrid Data-Flow Languages to Hybrid Automata: A Complete Translation (joint work with Bertrand Jeannet)

Talk at SYNCHRON'11: From Hybrid Data-Flow Languages to Hybrid Automata: A Complete Translation

Reviewer for HSCC'12

Article accepted for Journal of Symbolic Computation: Applying abstract acceleration to (co-)reachability analysis of reactive programs (joint work with Bertrand Jeannet)

Talk at SAS'11: Logico-Numerical Abstract Acceleration and Application to the Verification of Data-Flow Programs

Reviewer for MEMOCODE'11

Paper accepted at SAS'11: Logico-Numerical Abstract Acceleration and Application to the Verification of Data-Flow Programs (joint work with Bertrand Jeannet)


Talk at SYNCHRON'10: Using Abstract Acceleration in the Verification of Logico Numerical Data-Flow Programs

Talk at NSAD'10: Extending Abstract Acceleration Methods to Data-Flow Programs with Numerical Inputs

Paper accepted at NSAD'10: Sound Numerical Computations in Abstract Acceleration (joint work with Bertrand Jeannet)


Teaching

Static Security Analysis guest lectures for Security module University of Manchester, UK spring term 2020/21
Automating Software Quality guest lecture for Advanced Software Engineering module University of Sussex, UK winter term 2019/20
Automating Software Quality guest lecture for Advanced Software Engineering module University of Sussex, UK winter term 2018/19
Automating Software Quality guest lecture for Advanced Software Engineering module University of Sussex, UK winter term 2016/17
Operating Systems module University of Sussex, UK spring term 2016/17
Topics in Foundations of Software Systems lecture and practical on software verification University of Sussex, UK winter term 2016/17
High-Integrity Systems practicals in security and software verification University of Oxford, UK Hilary term 2015/16
Software Verification module University of Oxford, UK Hilary term 2014/15
High-Integrity Systems practicals in security and software verification University of Oxford, UK Hilary term 2014/15
Software Verification classes University of Oxford, UK Hilary term 2013/14
Introduction to C Programming practicals Université Pierre Mendès-France, IUT2, Grenoble, France summer term 2011/12
Introduction to C Programming practicals Université Pierre Mendès-France, IUT2, Grenoble, France summer term 2010/11
Radio Frequency Identification - Principles, Systems, Applications seminar TU Vienna, Austria winter term 2009/10
Radio Frequency Identification - Principles, Systems, Applications seminar TU Vienna, Austria winter term 2008/09
Radio Frequency Identification - Principles, Systems, Applications seminar TU Vienna, Austria winter term 2007/08

Software

2LS for Program Analysis A verification and static analysis tool for C programs
JBMC The Java bounded model checker
Incremental BMC An option for CBMC to unwind and verify loops incrementally
ChainCover A test case generator for reactive systems written in C
ReaVer - Reactive System Verifier A static analyzer for reactive and hybrid system data-flow models

Biography

Peter Schrammel has studied Computer Science with a specialization in embedded computing at TU Vienna, Austria. After his Master's, Peter worked as a software architect at Siemens, developing firmware for RFID transponders, edgeware, mobile device and ERP integrations. In 2009, Peter started a PhD in verification of embedded and hybrid system models using static analysis at Inria, Grenoble, France. After graduation, Peter worked as a post-doc at University of Oxford, UK, combining abstract interpretation and bounded model checking to verify and test ISO 26262-compliant automotive C programs. Peter contributed to the C Bounded Model Checker (CBMC) and developed the software verification tools 2LS and JBMC. In 2016, he became lecturer at University of Sussex, Brigthon, UK, and co-founded the company Diffblue. As CTO of Diffblue, Peter is leading the development of AI-powered unit test generation technology for Java. Peter is member of Advance HE, of the Royal Academy of Engineering Enterprise Hub, and of the ACM.

Legal Notices