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

Publications

Google Scholar
DBLP
ORCID
Scopus

Systems and methods for automatic test generation (with Daniel Kroening) US Patent 11,442,845 2022
Idiomatic source code generation US Patent 11,650,802 2023

Static Data Race Detection via Lazy Sequentialization (joint work with Bernd Fischer, Giulio Garbi, Salvatore La Torre, and Gennaro Parlato) International Conference on Networked Systems, NETYS, 2024
JCWIT: A Correctness-Witness Validator for Java Programs Based on Bounded Model Checking (joint work with Zaiyu Cheng, Tong Wu, Norbert Tihanyi, Eddie de Lima Filho, and Lucas Cordeiro) International Symposium on Software Testing and Analysis, ISSTA, 2024
Template-Based Verification of Array-Manipulating Programs (joint work with Viktor Malík and Tomás Vojnar) Taming the Infinities of Concurrency, LNCS, 2024
2LS: Arrays and Loop Unwinding - Competition Contribution (joint work with Viktor Malík, Frantisek Necas, and Tomás Vojnar) Tools and Algorithms for the Construction and Analysis of Systems, TACAS, 2023
BlueCov: Integrating Test Coverage and Model Checking with JBMC (joint work Matthias Güdemann) Symposium on Applied Computing, SAC, 2023
CBMC-SSM: Bounded Model Checking of C Programs with Symbolic Shadow Memory (joint work with Bernd Fischer, Salvatore La Torre, and Gennaro Parlato) Automated Software Engineering, ASE, 2022
Wit4Java: A Violation-Witness Validator for Java Verifiers - Competition Contribution (joint work with Tong Wu and Lucas Cordeiro) Tools and Algorithms for the Construction and Analysis of Systems, TACAS, 2022
Unbounded-Time Safety Verification of Guarded LTI Models with Inputs by Abstract Acceleration (joint work with Dario Cattaruzza, Alessandro Abate, and Daniel Kroening) Journal of Automatic Reasoning, 2021
2LS: Heap Analysis and Memory Safety - Competition Contribution (joint work with Viktor Malík and Tomás Vojnar) Tools and Algorithms for the Construction and Analysis of Systems, TACAS, 2020
JBMC: A Bounded Model Checking Tool for Verifying Java Bytecode - Competition Contribution (joint work with Lucas Cordeiro and Daniel Kroening) Tools and Algorithms for the Construction and Analysis of Systems, TACAS, 2019
Benchmarking of Java Verification Tools at the Software Verification Competition (SV-COMP) (joint work with Lucas Cordeiro and Daniel Kroening) Java Pathfinder, JPF@ESEC/FSE, 2018
Template-Based Verification of Heap-Manipulating Programs (joint work with Viktor Malik, Martin Hruska, and Tomas Vojnar) Formal Methods in Computer Aided Design, FMCAD, 2018
JBMC: A Bounded Model Checking Tool for Verifying Java Bytecode (joint work with Lucas Cordeiro, Pascal Kesseli, Daniel Kroening and Marek Trtik) Computer Aided Verification, CAV, 2018
2LS: Memory Safety and Non-termination - Competition Contribution (joint work with Viktor Malík, Stefan Marticek, Mandayam K. Srivas, Tomás Vojnar, Johanan Wahlang) Tools and Algorithms for the Construction and Analysis of Systems, TACAS, 2018
Effective Verification for Low-Level Software with Competing Interrupts (joint work with Lihao Liang, Daniel Kroening, Tom Melham, and Michael Tautschnig) Transactions on Embedded Computing Systems, TECS, 2018
Bit-Precise Procedure-Modular Termination Analysis (joint work with Hong-Yi Chen, Cristina David, Daniel Kroening, and Björn Wachter) Transactions on Programming Languages and Systems, TOPLAS, 2018
Parallel bug-finding in concurrent programs via reduced interleaving instances (joint work with Truc L. Nguyen, Bernd Fischer, Salvatore La Torre and Gennaro Parlato) Automated Software Engineering, ASE, 2017
Lifting CDCL to Template-based Abstract Domains for Program Verification (joint work with Rajdeep Mukherjee, Leopold Haller, Daniel Kroening, and Tom Melham) Automated Technology for Verification and Analysis, ATVA, 2017
Concurrent Program Verification with Invariant-guided Underapproximation (joint work with Sumanth Prabhu, Mandayam Srivas, Michael Tautschnig, and Anand Yeoleka) Automated Technology for Verification and Analysis, ATVA, 2017
Compositional Safety Refutation Techniques (joint work with Kumar Madhukar and Mandayam Srivas) Automated Technology for Verification and Analysis, ATVA, 2017
Sound Numerical Computations in Abstract Acceleration (joint work with Dario Cattaruzza, Alessandro Abate, and Daniel Kroening) Numerical Software Verification, NSV, 2017
Incremental Bounded Model Checking for Embedded Software (joint work with Daniel Kroening, Martin Brain, Ruben Martins, Tino Teige, and Tom Bienmüller) Journal Formal Aspects of Computing, 2017
Sound Static Deadlock Analysis for C/Pthreads (joint work with Daniel Kroening, Daniel Poetzl, and Björn Wachter) Automated Software Engineering, ASE, 2016
Assisted Coverage Closure (joint work with Adam Nellis, Pascal Kesseli, Philippa Ryan Conmy, Daniel Kroening and Michael Tautschnig) NASA Formal Methods, NFM, 2016
2LS for Program Analysis - Competition Contribution (joint work with Daniel Kroening) Tools and Algorithms for the Construction and Analysis of Systems, TACAS, 2016
Challenges in Decomposing Encodings of Verification Problems Horn Clauses for Verification and Synthesis, HCVS, 2016
Unbounded safety verification for hardware using software analyzers (joint work with Rajdeep Mukherjee, Daniel Kroening and Tom Melham) Design, Automation and Test in Europe, DATE, 2016
Unbounded-time reachability analysis of hybrid systems by abstract acceleration Embedded Software, EMSOFT, 2015
Synthesising Interprocedural Bit-Precise Termination Proofs (joint work with Hong-Yi Chen, Cristina David, Daniel Kroening and Björn Wachter) Automated Software Engineering, ASE, 2015
Safety Verification and Refutation by k-Invariants and k-Induction (joint work with Martin Brain, Saurabh Joshi and Daniel Kroening) Static Analysis Symposium, SAS, 2015
Unbounded-Time Analysis of Guarded LTI Systems with Inputs by Abstract Acceleration (joint work with Dario Cattaruzza, Alessandro Abate and Daniel Kroening) Static Analysis Symposium, SAS, 2015
Successful Use of Incremental BMC in the Automotive Industry (joint work with Daniel Kroening, Martin Brain, Ruben Martins, Tino Teige and Tom Bienmüller) Formal Methods for Industrial Critical Systems, FMICS, 2015
Generating Test Case Chains for Reactive Systems (joint work with Tom Melham and Daniel Kroening) Journal on Software Tools for Technology Transfer, STTT, 2015
Effective Verification of Low-Level Software with Nested Interrupts (joint work with Lihao Liang, Daniel Kroening, Tom Melham, and Michael Tautschnig) Design, Automation and Test in Europe, DATE, 2015
Necessary and Sufficient Preconditions via Eager Abstraction (joint work with Mohamed Nassim Seghir) Asian Symposium on Programming Languages and Systems, APLAS, 2014
Accelerated test execution using GPUs (joint work with Ajitha Rajan, Subodh Sharma and Daniel Kroening) Automated Software Engineering, ASE, 2014
Speeding Up Logico-Numerical Strategy Iteration (joint work with David Monniaux) Static Analysis Symposium, SAS, 2014
Abstract acceleration in linear relation analysis (joint work with Laure Gonnord) Journal Science of Computer Programming, 2014
Model and Proof Generation for Heap-Manipulating Programs (joint work with Martin Brain, Cristina David and Daniel Kroening) European Symposium on Programming, ESOP, 2014
Abstract Acceleration of General Linear Loops (joint work with Bertrand Jeannet and Sriram Sankaranarayanan) Principles of Programming Languages, POPL, 2014
Chaining Test Cases for Reactive System Testing (joint work with Tom Melham and Daniel Kroening) Testing Software and Systems, ICTSS, 2013
Logico-Numerical Max-Strategy Iteration (joint work with Pavle Subotic) Verification, Model Checking and Abstract Interpretation, VMCAI, 2013
Logico-Numerical Verification Methods for Discrete and Hybrid Systems (PhD thesis) Université Grenoble Alpes, France, 2012
From Hybrid Data-Flow Languages to Hybrid Automata: A Complete Translation (joint work with Bertrand Jeannet) Hybrid Systems: Computation and Control, HSCC, 2012
Applying abstract acceleration to (co-)reachability analysis of reactive programs (joint work with Bertrand Jeannet) Journal of Symbolic Computation, 2011
Logico-Numerical Abstract Acceleration and Application to the Verification of Data-Flow Programs (joint work with Bertrand Jeannet) Static Analysis Symposium, SAS, 2011
Extending Abstract Acceleration Methods to Data-Flow Programs with Numerical Inputs (joint work with Bertrand Jeannet) Numerical and Symbolic Abstract Domains, NSAD, 2010
System Architecture (book chapter) Optimizing Processes with RFID and Auto ID, 2009
Feasibility study for RFID-based temperature monitoring of blood bags (Master's thesis) University of Technology, Vienna, Austria, 2006

Software

2LS for Program Analysis

A verification and static analysis tool for C programs

JBMC

The Java bounded model checker

Incremental BMC

Options 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


Activities

JBMC Silver medal in Java-Overall category, 1st in Runtime Exception demo category Software Verification Competition 2025
JBMC Silver medal in Java-Overall category Software Verification Competition 2024
2LS Bronze medal in Termination category, 10th in Overall category Software Verification Competition 2024
JBMC Gold medal in Java-Overall category Software Verification Competition 2023
2LS Bronze medal in Termination category, 8th in Overall category Software Verification Competition 2023
JBMC Silver medal in Java-Overall category Software Verification Competition 2022
2LS Bronze medal in Termination category, 9th in Overall category Software Verification Competition 2022
JBMC Bronze medal in Java-Overall category Software Verification Competition 2021
2LS Bronze medal in Termination category, 7th in Overall category Software Verification Competition 2021
JBMC Silver medal in Java-Overall category Software Verification Competition 2020
2LS Bronze medal in Termination category, 7th in Overall category Software Verification Competition 2020
JBMC Gold medal in Java-Overall category Software Verification Competition 2019
2LS 4th in Termination category, 7th in Overall category Software Verification Competition 2019
2LS 4th in Termination category, 7th in Overall category Software Verification Competition 2018
2LS Top 5 in two categories Software Verification Competition 2017
2LS Gold medal in the Floats category Software Verification Competition 2016

Does AI generated code need to be tested? Oxford Leaders in Tech Meetup, 2024
From Academic Research to Industrial Impact: The Diffblue Journey Invited talk at Theoretical Aspects of Software Engineering, TASE, 2023
JBMC: Bounded Model Checking for Java Bytecode - Competition Contribution Tools and Algorithms for the Construction and Analysis of Systems, TACAS, 2023
CBMC-SSM: Bounded Model Checking of C Programs with Symbolic Shadow Memory Automated Software Engineering, ASE, 2022
Writing Better Java Unit Tests with AI Oxford Artificial Intelligence Meetup, 2022
Parallel Bug-finding in Concurrent Programs via Reduced Interleaving Instances Verification seminar talk at IIT Delhi, India, 2022
Automatically writing unit tests with Diffblue Cover Tutorial at A-Test, 2020 (co-located with ESEC/FSE 2020)
How testable is business software? Invited talk at Formal Methods in Computer Aided Design, FMCAD, 2020
How Automated Tools Change the Way We Write Code Atlas lecture at University of Manchester, UK, 2019
JBMC: Bounded Model Checking for Java Bytecode ETAPS TOOLympics, 2019
Template-Based Verification of Heap-Manipulating Programs Seminar talk at Chennai Mathematical Institute, India, 2018
Benchmarking of Java Verification Tools at the Software Verification Competition (SV-COMP) Java Pathfinder, JPF@ESEC/FSE, 2018
JBMC: A Bounded Model Checking Tool for Verifying Java Bytecode Computer Aided Verification, CAV, 2018
Procedure-Modular Termination Analysis Workshop on Termination, WST, 2018
How Automated Tools Change the Way We Write Code Invited talk at Verification and Synthesis for Software Evolution, VSSE, 2018
Lifting CDCL to Template-Based Abstract Domains for Program Verification Automated Technology for Verification and Analysis, ATVA, 2017
From Programs to Logic: The CPROVER verification tools Tutorial at Formal Methods, FM, 2016 (with Martin Brain)
Assisted Coverage Closure NASA Formal Methods, NFM, 2016
Safety Verification and Refutation by k-invariants and k-induction Seminar talk at University of Southampton, UK, 2016
Challenges in Decomposing Encodings of Verification Problems Horn Clauses for Verification and Synthesis, HCVS, 2016
Safety Verification and Refutation by k-invariants and k-induction Seminar talk at ONERA, Toulouse, France, 2015
Safety Verification and Refutation by k-invariants and k-induction Seminar talk at Uppsala University, Sweden, 2015
Synthesising Interprocedural Bit-Precise Termination Proofs Automated Software Engineering, ASE, 2015
Unbounded-Time Analysis of Guarded LTI Systems with Inputs by Abstract Acceleration Invited talk at Embedded Software, EMSOFT, 2015
Unbounded-time reachability analysis of hybrid systems by abstract acceleration Static Analysis Symposium, SAS, 2015
Safety Verification and Refutation by k-Invariants and k-Induction Static Analysis Symposium, SAS, 2015
From Programs to Logic: The CPROVER verification tools Tutorial at Conference on Automated Deduction, CADE, 2015 (with Martin Brain)
Successful Use of Incremental BMC in the Automotive Industry Formal Methods for Industrial Critical Systems, FMICS, 2015
Speeding Up Logico-Numerical Strategy Iteration Static Analysis Symposium, SAS, 2014
Inferring Invariants by Strategy Iteration Dagstuhl Seminar on Decision Procedures and Abstract Interpretation 2014
Abstract Acceleration of General Linear Loops Principles of Programming Languages, POPL, 2014
Chaining Test Cases for Reactive System Testing Testing Software and Systems, ICTSS, 2013
Automated Firmware Verification Invited talk at Intel European Research and Innovation Conference, 2013
Logico-Numerical Max-Strategy Iteration Verification, Model Checking and Abstract Interpretation, VMCAI, 2013
Méthodes logico-numériques pour la vérification des systèmes discrets et hybrides. (Logico-Numerical Verification Methods for Discrete and Hybrid Systems) PhD Defense / Soutenance, Inria Grenoble, 2012
From Hybrid Data-Flow Languages to Hybrid Automata: A Complete Translation Hybrid Systems: Computation and Control, HSCC, 2012
Logico-Numerical Abstract Acceleration and Application to the Verification of Data-Flow Programs Seminar talk at LSV, ENS Cachan, France, 2012
From Hybrid Data-Flow Languages to Hybrid Automata: A Complete Translation SYNCHRON, 2011
Logico-Numerical Abstract Acceleration and Application to the Verification of Data-Flow Programs Static Analysis Symposium, SAS, 2011
Logico-Numerical Abstract Acceleration and Application to the Verification of Data-Flow Programs SYNCHRON, 2010
Extending Abstract Acceleration Methods to Data-Flow Programs with Numerical Inputs Numerical and Symbolic Abstract Domains, NSAD, 2010

Service

PC member International Conference on Software Engineering, ICSE, 2026
PC member Computer-Aided Verification, CAV, 2024
PC member Foundations of Software Engineering, FSE, 2024
Reviewer Software: Practice and Experience, 2022
Reviewer Information Processing Letters, 2022
Reviewer Transactions on Software Engineering and Methodology, TOSEM, 2021
Reviewer Journal Expert Systems with Applications, 2021
Reviewer Journal Information and Software Technology, 2021
Student Forum Chair Formal Methods for Computer Aided Design, FMCAD, 2020
Co-PC Chair Numerical Software Verification, NSV, 2020 (co-located with CAV 2020)
External or sub-reviewer International Colloquium on Automata, Languages and Programming, ICALP, 2020
PC member Verified Software: Theories, Tools and Experiments, VSTTE, 2019
Reviewer Journal on Software Tools for Technology Transfer, STTT, 2019
External or sub-reviewer International Conference on Industrial Informatics, INDIN, 2019
Reviewer Journal for Engineering Science and Technology, 2019
PC member Verified Software: Theories, Tools and Experiments, VSTTE, 2018
Reviewer EURASIP Journal on Embedded Systems, 2018
Reviewer Journal of Systems and Software, 2018
External or sub-reviewer International Conference on Engineering of Complex Computer Systems, ICCECS, 2017
Reviewer Formal Methods in System Design, FMSD, 2017
External or sub-reviewer International Conference on Engineering of Complex Computer Systems, ICCECS, 2015
Reviewer Transactions on Software Engineering, TSE, 2017
PC member Verified Software: Theories, Tools and Experiments, VSTTE, 2017
External or sub-reviewer Static Analysis Symposium, SAS, 2017
External or sub-reviewer Computer-Aided Verification, CAV, 2017
Reviewer Journal Formal Aspects of Computing, 2016
External or sub-reviewer Conference on Decision and Control, CDC, 2016
External or sub-reviewer Formal Methods in Computer-Aided Design, FMCAD, 2016
External or sub-reviewer NASA Formal Methods, NFM, 2016
External or sub-reviewer International Symposium on Software Testing and Analysis, ISSTA, 2016
External or sub-reviewer Tools and Algorithms for the Construction and Analysis of Systems, TACAS, 2016
External or sub-reviewer Fundamental Approaches to Software Engineering, FASE, 2016
Artifact Evaluation Committee member Principles of Programming Languages, POPL, 2016
External or sub-reviewer International Conference on Computer Design, ICCD, 2015
External or sub-reviewer International Conference on Engineering of Complex Computer Systems, ICCECS, 2015
Reviewer Journal Logical Methods in Computer Science, 2015
Reviewer Journal of Systems and Software, 2015
Reviewer Journal Science of Computer Programming, 2015
External or sub-reviewer Formal Methods in Computer-Aided Design, FMCAD, 2015
External or sub-reviewer Computer Aided Verification, 2015
Reviewer Oxford Computer Journal, 2014
External or sub-reviewer Verification, Model Checking and Abstract Interpretation, VMCAI, 2014
Reviewer Journal Nonlinear Analysis: Hybrid Systems, 2014
External or sub-reviewer Formal Methods and Models for System Design, MEMOCODE, 2014
External or sub-reviewer Computer Aided Verification, CAV, 2014
External or sub-reviewer International Joint Conference on Automated Reasoning, IJCAR, 2014
External or sub-reviewer Design, Automation and Test in Europe, DATE, 2014
External or sub-reviewer International Conference on Computer Design, ICCD, 2013
External or sub-reviewer Design and Implementation of Formal Tools and Systems, DIFTS, 2013
External or sub-reviewer Theory and Applications of Satisfiability Testing, SAT, 2013
External or sub-reviewer European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/FSE, 2013
External or sub-reviewer Hybrid Systems: Computation and Control, HSCC, 2013
Reviewer Journal Simulation Modelling Practice and Theory, 2012
External or sub-reviewer Design, Automation and Test in Europe, DATE, 2012
External or sub-reviewer Hybrid Systems: Computation and Control, HSCC, 2012
External or sub-reviewer Formal Methods and Models for System Design, MEMOCODE, 2011

Generative AI for the Software Development Life Cycle UKRI Innovate UK £724k Principal Investigator Mar 2025
Series A3 - Diffblue Ltd £4.8m Co-founder Oct 2024
Series A2 - Diffblue Ltd £6.3m Co-founder Nov 2022
Series A1 - Diffblue Ltd £5.7m Co-founder Jan 2022
Shott Scale Accelerator Programme Royal Academy of Engineering, UK £10k SME Leader 2018
Series A - Diffblue Ltd £17.3m Co-founder 2017
Efficient Software Verification by Reasoning about Abstractions EPSRC, UK £99k (offered) Principal Investigator 2017
Seed funding - Diffblue Ltd £1.5m Co-founder 2016
Industrial impact of Verification of Evolving Software Oxford University Innovation, UK £75k Principal Investigator (with Daniel Kroening) 2016
Industrial impact of C/C++ formal verification tools through plug-ins for the Eclipse IDE UKRI Impact Acceleration, UK £35k Principal Investigator (with Daniel Kroening) 2015

Chennai Mathematical Institute, India with Mandayam K. Srivas October 2017, June and November 2018
University of Colorado Boulder, US with Sriram Sankaranarayanan February 2012

Mikhail Ramalho Gadelha Scalable and precise verification based on k-induction, symbolic execution and floating-point theory University of Southampton, UK external examiner 2019
Madhukar Kumar Scalable Safety Verification of Statechart-like Programs Chennai Mathematical Institute, India co-supervisor together with Mandayam K. Srivas 2015-2018
Daniel Pötzl Lock correctness Unversity of Oxford, UK co-supervisor together with Daniel Kroening 2015-2018
Rajdeep Mukherjee Precise abstract interpretation of hardware designs Unversity of Oxford, UK informal co-supervisor together with Daniel Kroening and Tom Melham 2015-2018
Lihao Liang Verification of Interrupt-driven Software Unversity of Oxford, UK informal co-supervisor together with Daniel Kroening, Tom Melham and Luke Ong 2015-2018
Dario Cattaruzza Verification and synthesis of linear systems by abstract acceleration Unversity of Oxford, UK informal co-supervisor together with Daniel Kroening and Alessandro Abate 2015-2018

Formal Verification of C Code – CBMC Introduction guest lecture for Knowledge Engineering module Ulster University, UK winter term 2024/25
Formal Verification of C Code – CBMC Introduction guest lecture for Knowledge Engineering module Ulster University, UK winter term 2023/24
Formal Verification of C Code – CBMC Introduction guest lecture for Software Reliability Engineering module Ulster University, UK spring term 2022/23
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

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 fellow of Advance HE, member of the Royal Academy of Engineering Enterprise Hub, and of the ACM.

Legal Notices