Predicate abstraction of ANSI-C programs using SAT

Predicate abstraction of ANSI-C programs using SAT

Show other versions (3)

Predicate abstraction is a major method for verification of software. However, the generation of the abstract Boolean program from the set of predicates and the original program suffers from an exponential number of theorem prover calls as well as from soundness issues. This paper presents a novel t...

Disgrifiad llawn

Manylion Llyfryddiaeth
Prif Awduron:	Clarke, E, Kroening, D, Sharygina, N, al., E
Fformat:	Journal article
Cyhoeddwyd:	Springer 2004

Eitemau Tebyg

Predicate Abstraction of ANSI-C Programs Using SAT.
gan: Clarke, E, et al.
Cyhoeddwyd: (2004)

Predicate Abstraction of ANSI-C Programs Using SAT
gan: Clarke, E, et al.
Cyhoeddwyd: (2004)

Predicate Abstraction of ANSI–C Programs using SAT
gan: Clarke, E, et al.
Cyhoeddwyd: (2015)

SATABS: SAT−based Predicate Abstraction for ANSI−C
gan: Clarke, E, et al.
Cyhoeddwyd: (2005)

Word Level Predicate Abstraction and Refinement for Verifying RTL Verilog
gan: Jain, H, et al.
Cyhoeddwyd: (2008)

Word Level Predicate Abstraction and Refinement for Verifying RTL Verilog
gan: Jain, H, et al.
Cyhoeddwyd: (2005)

Word level predicate abstraction and refinement for verifying RTL verilog
gan: Jain, H, et al.
Cyhoeddwyd: (2005)

Word-Level Predicate-Abstraction and Refinement Techniques for Verifying RTL Verilog.
gan: Jain, H, et al.
Cyhoeddwyd: (2008)

Verification of SpecC using Predicate Abstraction
gan: Clarke, E, et al.
Cyhoeddwyd: (2007)

Verification of SpecC using predicate abstraction.
gan: Clarke, E, et al.
Cyhoeddwyd: (2007)

Word-level predicate-abstraction and refinement rechniques for verifying RTL Verilog
gan: Jain, H, et al.
Cyhoeddwyd: (2008)

Checking consistency of C and Verilog using predicate abstraction and induction
gan: Kroening, D, et al.
Cyhoeddwyd: (2004)

Checking Consistency of C and Verilog using Predicate Abstraction and Induction
gan: Kroening, D, et al.
Cyhoeddwyd: (2004)

Verification of SpecC and Verilog using Predicate Abstraction
gan: Jain, H, et al.
Cyhoeddwyd: (2004)

Hardware Verification using ANSI−C Programs as a Reference
gan: Clarke, E, et al.
Cyhoeddwyd: (2003)

Hardware verification using ANSI-C programs as a reference
gan: Clarke, E, et al.
Cyhoeddwyd: (2003)

A Tool for Checking ANSI−C Programs
gan: Clarke, E, et al.
Cyhoeddwyd: (2004)

Verification and Falsification of Programs with Loops Using Predicate Abstraction
gan: Kroening, D, et al.
Cyhoeddwyd: (2009)

Verification and falsification of programs with loops using predicate abstraction.
gan: Kroening, D, et al.
Cyhoeddwyd: (2010)

Approximating Predicate Images for Bit−Vector Logic
gan: Kroening, D, et al.
Cyhoeddwyd: (2006)

Image Computation and Predicate Refinement for RTL Verilog using Word Level Proofs
gan: Kroening, D, et al.
Cyhoeddwyd: (2007)

Verifying C++ with STL Containers via Predicate Abstraction
gan: Blanc, N, et al.
Cyhoeddwyd: (2007)

Verifying C++ with STL containers via predicate abstraction
gan: Blanc, N, et al.
Cyhoeddwyd: (2007)

Counterexamples with Loops for Predicate Abstraction
gan: Kroening, D, et al.
Cyhoeddwyd: (2006)

VCEGAR: Verilog CounterExample Guided Abstraction Refinement
gan: Jain, H, et al.
Cyhoeddwyd: (2007)

Model Checking with Abstraction for Web Services
gan: Sharygina, N, et al.
Cyhoeddwyd: (2007)

Programming with ANSI C++ /
gan: 229185 Trivedi, Bhushan
Cyhoeddwyd: (2007)

Programming in ANSI C /
gan: 279425 Kochan, Stephen G.
Cyhoeddwyd: (1988)

Illustrated C programming (ANSI) /
gan: 198287 Beam, J. Emmett
Cyhoeddwyd: (1989)

SAT−based Summarisation for Boolean Programs
gan: Basler, G, et al.
Cyhoeddwyd: (2007)

Formal Verification of SystemC by Automatic Hardware/Software Partitioning
gan: Kroening, D, et al.
Cyhoeddwyd: (2005)

A SAT−Based Algorithm for Reparameterization in Symbolic Simulation
gan: Chauhan, P, et al.
Cyhoeddwyd: (2004)

A SAT-based algorithm for reparameterization in symbolic simulation
gan: Chauhan, P, et al.
Cyhoeddwyd: (2004)

Accurate Theorem Proving for Program Verification
gan: Cook, B, et al.
Cyhoeddwyd: (2006)

Verification of Boolean Programs with Unbounded Thread Creation
gan: Cook, B, et al.
Cyhoeddwyd: (2007)

Verification of Boolean programs with unbounded thread creation.
gan: Cook, B, et al.
Cyhoeddwyd: (2007)

Cogent: Accurate theorem proving for program verification
gan: Cook, B, et al.
Cyhoeddwyd: (2005)

Symbolic model checking for asynchronous Boolean programs
gan: Cook, B, et al.
Cyhoeddwyd: (2005)

Over−Approximating Boolean Programs with Unbounded Thread Creation
gan: Cook, B, et al.
Cyhoeddwyd: (2006)

An expectation transformer approach to predicate abstraction and data independence for probabilistic programs
gan: Ukachukwu Ndukwu, et al.
Cyhoeddwyd: (2010-06-01)