Predicate abstraction of ANSI-C programs using SAT

Predicate abstraction of ANSI-C programs using SAT

Mostra altre versioni (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...

Descrizione completa

Dettagli Bibliografici
Autori principali:	Clarke, E, Kroening, D, Sharygina, N, al., E
Natura:	Journal article
Pubblicazione:	Springer 2004

Documenti analoghi

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Programming with ANSI C++ /
di: 229185 Trivedi, Bhushan
Pubblicazione: (2007)

Programming in ANSI C /
di: 279425 Kochan, Stephen G.
Pubblicazione: (1988)

Illustrated C programming (ANSI) /
di: 198287 Beam, J. Emmett
Pubblicazione: (1989)

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

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

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

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

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

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

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

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

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

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

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