Peter Schrammel



Research

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.

Read more...


News

Diffblue is hiring C++ developers and research engineers in automated formal verification. Read more...

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

Talk at WST'18: Procedure-Modular Termination Analysis

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)

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.

Reviewer for CAV'17


Reviewer for Journal Formal Aspects of Computing

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)


Berge 
Montagnes 
Mountains 



Musik 



DiffBlue - AI for Code