A Tool for Checking ANSI-C Programs

By Edmund M. Clarke, Daniel Kroening, Flavio Lerda. International Conference on Tools and Algorithms for Construction and Analysis of Systems, 2004

1,554 citations recorded by the source corpus.

Subfields: Computational Theory and Mathematics, Hardware and Architecture, Software

View Paper: https://www.semanticscholar.org/paper/5f5335a25d2b4ef0fb099ae917ff98d8afea97e3

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Computational Theory and Mathematics

In Hardware and Architecture

In Software

Citations in the corpus

Randomized Differential Testing as a Prelude to Formal Verification (2007, methodology): “We plan to use bounded model checking [7] or other static analysis to discharge the assumption of triviality for each non-covered parameter check.”
The ASTREÉ Analyzer (2005, background): “Considering them as reals (as usually done with theorem provers) or (cid:12)xed point numbers (as in CBMC [11]) would not conform to the norm whence would be unsound.”
SoK: General Purpose Compilers for Secure Multi-Party Computation (2019, methodology): “It is based on CMBC [37], a bounded model checker that translates any C program into a Boolean constraint then adapts the output of this tool to produce an optimized circuit for an MPC computation.”
Secure two-party computations in ANSI C (2012, methodology): “While overapproximating model checkers often model e.g. integer variables by unbounded (mathemat- ical) integer values, a bit-precise model checker will typically model them as a bit vector with real-life overflow behavior.”
SATABS: SAT-Based Predicate Abstraction for ANSI-C (2005, methodology): “SatAbs is integrated into the graphical user interface (GUI) of CBMC.”
A Survey of Automated Techniques for Formal Software Verification (2008, methodology): “One of the first implementations of BMC for C programs is CBMC [38], [83] developed at CMU; it emulates a wide range of architectures as environment for the design under test.”
CPAchecker: A Tool for Configurable Software Verification (2009, methodology): “We have integrated the bounded model checker CBMC [ 7 ] into CPAchecker for a bit-precise path-feasibility check.”
Transaction-Level Modeling with SystemC: TLM Concepts and Applications for Embedded Systems (2010, methodology): “Using Cadence VCC, Giorgio Mastrorocco upgraded a Parades model [5] of a dual processor SoC of STMicroelectronics.”
HAMPI: a solver for string constraints (2009, background): “Many automatic testing [6, 17, 34], analysis [19, 40], and verification [8, 22] techniques for programs can be effectively reduced to a constraint-generation phase followed by a constraint-solving”
The SeaHorn Verification Framework (2015, background): “There is a large number of tools with different capabilities and trade-offs [6,8,9,15–18,20,42].”
KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs (2008, neutral): “ecution systems [17, 18, 32] are static in a strict sense and do not interact with the running environment at all.”
Program synthesis by sketching (2008, background): “Modern model checking tools, for example, are now able to expose errors in complex routines with relatively little user e ort [7,21,37,68].”
Towards automatic generation of vulnerability-based signatures (2006, methodology): “We currently use CBMC [ 16 ] , a bounded model checker , to help build and solve symbolic constraints to produce regular expression signatures .”
TrustVisor: Efficient TCB Reduction and Attestation (2010, methodology): “We also plan to verify the TrustVisor implementation using software model checking methods [9].”
A Pragmatic Introduction to Secure Multi-Party Computation (2019, background): “CBMC (Clarke et al., 2004) is a bounded model checker designed to verify properties of programs written in ANSI C.”
Efficient TCB Reduction and Attestation (2009, methodology): “We also plan to verify the TrustVisor implementation using software model checking methods [8].”