Predicate abstraction of ANSI-C programs using SAT

Predicate abstraction of ANSI-C programs using SAT

Čájet eará veršuvnnaid (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...

Bibliográfalaš dieđut
Váldodahkkit:	Clarke, E, Kroening, D, Sharygina, N, al., E
Materiálatiipa:	Journal article
Almmustuhtton:	Springer 2004

Geahča maid

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Programming with ANSI C++ /
Dahkki: 229185 Trivedi, Bhushan
Almmustuhtton: (2007)

Programming in ANSI C /
Dahkki: 279425 Kochan, Stephen G.
Almmustuhtton: (1988)

Illustrated C programming (ANSI) /
Dahkki: 198287 Beam, J. Emmett
Almmustuhtton: (1989)

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

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

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

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

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

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

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

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

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

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

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