 |
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
|
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 2021.
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)
|
|
|
 |
Berge
Montagnes
Mountains
|
|
 |
Musik
|
|
 |
Diffblue -
AI for Code
|
|
|