Behavioral consistency of C and Verilog programs using bounded model checking

By Edmund M. Clarke, Daniel Kroening, Karen Yorav. 2003

314 citations recorded by the source corpus.

We present an algorithm that checks behavioral consistency between an ANSI-C program and a circuit given in Verilog using Bounded Model Checking. Both the circuit and the program are unwound and translated into a formula that represents behavioral consistency. The formula is then checked using a SAT solver. We are able to translate C programs that include side effects, pointers, dynamic memory allocation, and loops with conditions that cannot be evaluated statically. We describe experimental results on various reactive circuits and programs, including a small processor given in Verilog and its Instruction Set Architecture given in ANSI-C.

Subfields: Artificial Intelligence, Computational Theory and Mathematics, Program Analysis & Verification

How researchers see this paper

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

In Artificial Intelligence

In Computational Theory and Mathematics

In Program Analysis & Verification

Citations in the corpus

A Survey of Machine Learning for Big Code and Naturalness (2017, background): “Many elegant and powerful abstractions, definitions, algorithms, and proof techniques have been developed, which have led to important practical tools for program verification, bug finding, and refactoring [24, 42, 45].”
Software model checking (2009, unknown): “The first, such as CBMC [Kroening et al. 2003], F-Soft [Ivancic et al.”
Combinatorial sketching for finite programs (2006, methodology): “Our translation to boolean functions largely follows the standard approach used by other verifiers [3, 17].”
A Tool for Checking ANSI-C Programs (2004, methodology): “The full details of the transformation are described in [3].”
Secure two-party computations in ANSI C (2012, methodology): “On input of an ANSI C program f and a bound k, CBMC first translates the program into a cycle-free GOTO program.”
KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs (2008, unknown): “ecution systems [17, 18, 32] are static in a strict sense and do not interact with the running environment at all.”
Program sketching (2012, methodology): “Interestingly, the validation procedure that results from this symbolic manipulation is equivalent to the SAT-based bounded model checker developed by Clarke et al. [6].”
Program synthesis by sketching (2008, methodology): “Interestingly, the validation procedure that results from this symbolic manipulation is equivalent to the SAT-based bounded model checker developed by Clarke, Kroening and Yorav [19].”
A Survey of Automated Techniques for Formal Software Verification (2008, methodology): “One of the first implementations of BMC for C programs is CBMC [83], [38], developed at CMU; it emulates a wide range of architectures as environment for the design under test.”