7 citations · 27 across the 17 of their papers we have counts for
18 papers
CBMC: The C Bounded Model Checker
Daniel Kroening, Peter Schrammel, Michael Tautschnig
The C Bounded Model Checker (CBMC) demonstrates the violation of assertions in C programs, or proves safety of the assertions under a given bound. CBMC implements a bit-precise tra…
JBMC: A Bounded Model Checking Tool for Java Bytecode
Romain Brenguier, Lucas Cordeiro, Daniel Kroening +1
JBMC is an open-source SAT- and SMT-based bounded model checking tool for verifying Java bytecode. JBMC relies on an operational model of the Java libraries, which conservatively a…
2LS for Program Analysis
Daniel Kroening, Viktor Malík, Peter Schrammel +1
2LS ("tools") is a verification tool for C programs, built upon the CPROVER framework. It allows one to verify user-specified assertions, memory safety properties (e.g. buffer over…
BlueCov: Integrating Test Coverage and Model Checking with JBMC
Matthias Güdemann, Peter Schrammel
Automated test case generation tools help businesses to write tests and increase the safety net provided by high regression test coverage when making code changes. Test generation…
How Testable is Business Software?
Peter Schrammel
Most businesses rely on a significant stack of software to perform their daily operations. This software is business-critical as defects in this software have major impacts on reve…
2LS: Heap Analysis and Memory Safety (Competition Contribution)
Viktor Malik, Martin Hruska, Peter Schrammel +1
2LS is a framework for analysis of sequential C programs that can verify and refute program assertions and termination. The 2LS framework is built upon the CPROVER infrastructure a…
Benchmarking of Java Verification Tools at the Software Verification Competition (SV-COMP)
Lucas Cordeiro, Daniel Kroening, Peter Schrammel
Empirical evaluation of verification tools by benchmarking is a common method in software verification research. The Competition on Software Verification (SV-COMP) aims at standard…
Lifting CDCL to Template-based Abstract Domains for Program Verification
Rajdeep Mukherjee, Peter Schrammel, Leopold Haller +2
The success of Conflict Driven Clause Learning (CDCL) for Boolean satisfiability has inspired adoption in other domains. We present a novel lifting of CDCL to program analysis call…
Sound Static Deadlock Analysis for C/Pthreads (Extended Version)
Daniel Kroening, Daniel Poetzl, Peter Schrammel +1
We present a static deadlock analysis approach for C/pthreads. The design of our method has been guided by the requirement to analyse real-world code. Our approach is sound (i.e.,…
Challenges in Decomposing Encodings of Verification Problems
Peter Schrammel
Modern program verifiers use logic-based encodings of the verification problem that are discharged by a back end reasoning engine. However, instances of such encodings for large pr…
Assisted Coverage Closure
Adam Nellis, Pascal Kesseli, Philippa Ryan Conmy +3
The malfunction of safety-critical systems may cause damage to people and the environment. Software within those systems is rigorously designed and verified according to domain spe…
Safety Verification and Refutation by k-invariants and k-induction (extended version)
Martin Brain, Saurabh Joshi, Daniel Kroening +1
Most software verification tools can be classified into one of a number of established families, each of which has their own focus and strengths. For example, concrete counterexamp…
Unbounded-Time Analysis of Guarded LTI Systems with Inputs by Abstract Acceleration (extended version)
Dario Cattaruzza, Alessandro Abate, Peter Schrammel +1
Linear Time Invariant (LTI) systems are ubiquitous in control applications. Unbounded-time reachability analysis that can cope with industrial-scale models with thousands of variab…
Synthesising Interprocedural Bit-Precise Termination Proofs (extended version)
Hong-Yi Chen, Cristina David, Daniel Kroening +2
Proving program termination is key to guaranteeing absence of undesirable behaviour, such as hanging programs and even security vulnerabilities such as denial-of-service attacks. T…
Incremental Bounded Model Checking for Embedded Software (extended version)
Peter Schrammel, Daniel Kroening, Martin Brain +3
Program analysis is on the brink of mainstream in embedded systems development. Formal verification of behavioural requirements, finding runtime errors and automated test case gene…
Speeding Up Logico-Numerical Strategy Iteration (extended version)
David Monniaux, Peter Schrammel
We introduce an efficient combination of polyhedral analysis and predicate partitioning. Template polyhedral analysis abstracts numerical variables inside a program by one polyhedr…
Abstract Acceleration of General Linear Loops
Bertrand Jeannet, Peter Schrammel, Sriram Sankaranarayanan
We present abstract acceleration techniques for computing loop invariants for numerical programs with linear assignments and conditionals. Whereas abstract interpretation technique…
Chaining Test Cases for Reactive System Testing (extended version)
Peter Schrammel, Tom Melham, Daniel Kroening
Testing of synchronous reactive systems is challenging because long input sequences are often needed to drive them into a state at which a desired feature can be tested. This is pa…