7 citations · 27 across the 17 of their papers we have counts for
10 papers · 1 filter
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…
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…
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…
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…