Predicate abstraction of ANSI-C programs using SAT

Predicate abstraction of ANSI-C programs using SAT

Taispeáin leaganacha eile (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...

Cur síos iomlán

Sonraí bibleagrafaíochta
Príomhchruthaitheoirí:	Clarke, E, Kroening, D, Sharygina, N, al., E
Formáid:	Journal article
Foilsithe / Cruthaithe:	Springer 2004

Míreanna comhchosúla

Predicate Abstraction of ANSI-C Programs Using SAT.
de réir: Clarke, E, et al.
Foilsithe / Cruthaithe: (2004)

Predicate Abstraction of ANSI-C Programs Using SAT
de réir: Clarke, E, et al.
Foilsithe / Cruthaithe: (2004)

Predicate Abstraction of ANSI–C Programs using SAT
de réir: Clarke, E, et al.
Foilsithe / Cruthaithe: (2015)

SATABS: SAT−based Predicate Abstraction for ANSI−C
de réir: Clarke, E, et al.
Foilsithe / Cruthaithe: (2005)

Word Level Predicate Abstraction and Refinement for Verifying RTL Verilog
de réir: Jain, H, et al.
Foilsithe / Cruthaithe: (2008)

Word Level Predicate Abstraction and Refinement for Verifying RTL Verilog
de réir: Jain, H, et al.
Foilsithe / Cruthaithe: (2005)

Word level predicate abstraction and refinement for verifying RTL verilog
de réir: Jain, H, et al.
Foilsithe / Cruthaithe: (2005)

Word-Level Predicate-Abstraction and Refinement Techniques for Verifying RTL Verilog.
de réir: Jain, H, et al.
Foilsithe / Cruthaithe: (2008)

Verification of SpecC using Predicate Abstraction
de réir: Clarke, E, et al.
Foilsithe / Cruthaithe: (2007)

Verification of SpecC using predicate abstraction.
de réir: Clarke, E, et al.
Foilsithe / Cruthaithe: (2007)

Word-level predicate-abstraction and refinement rechniques for verifying RTL Verilog
de réir: Jain, H, et al.
Foilsithe / Cruthaithe: (2008)

Checking consistency of C and Verilog using predicate abstraction and induction
de réir: Kroening, D, et al.
Foilsithe / Cruthaithe: (2004)

Checking Consistency of C and Verilog using Predicate Abstraction and Induction
de réir: Kroening, D, et al.
Foilsithe / Cruthaithe: (2004)

Verification of SpecC and Verilog using Predicate Abstraction
de réir: Jain, H, et al.
Foilsithe / Cruthaithe: (2004)

Hardware Verification using ANSI−C Programs as a Reference
de réir: Clarke, E, et al.
Foilsithe / Cruthaithe: (2003)

Hardware verification using ANSI-C programs as a reference
de réir: Clarke, E, et al.
Foilsithe / Cruthaithe: (2003)

A Tool for Checking ANSI−C Programs
de réir: Clarke, E, et al.
Foilsithe / Cruthaithe: (2004)

Verification and Falsification of Programs with Loops Using Predicate Abstraction
de réir: Kroening, D, et al.
Foilsithe / Cruthaithe: (2009)

Verification and falsification of programs with loops using predicate abstraction.
de réir: Kroening, D, et al.
Foilsithe / Cruthaithe: (2010)

Approximating Predicate Images for Bit−Vector Logic
de réir: Kroening, D, et al.
Foilsithe / Cruthaithe: (2006)

Image Computation and Predicate Refinement for RTL Verilog using Word Level Proofs
de réir: Kroening, D, et al.
Foilsithe / Cruthaithe: (2007)

Verifying C++ with STL Containers via Predicate Abstraction
de réir: Blanc, N, et al.
Foilsithe / Cruthaithe: (2007)

Verifying C++ with STL containers via predicate abstraction
de réir: Blanc, N, et al.
Foilsithe / Cruthaithe: (2007)

Counterexamples with Loops for Predicate Abstraction
de réir: Kroening, D, et al.
Foilsithe / Cruthaithe: (2006)

VCEGAR: Verilog CounterExample Guided Abstraction Refinement
de réir: Jain, H, et al.
Foilsithe / Cruthaithe: (2007)

Model Checking with Abstraction for Web Services
de réir: Sharygina, N, et al.
Foilsithe / Cruthaithe: (2007)

Programming with ANSI C++ /
de réir: 229185 Trivedi, Bhushan
Foilsithe / Cruthaithe: (2007)

Programming in ANSI C /
de réir: 279425 Kochan, Stephen G.
Foilsithe / Cruthaithe: (1988)

Illustrated C programming (ANSI) /
de réir: 198287 Beam, J. Emmett
Foilsithe / Cruthaithe: (1989)

SAT−based Summarisation for Boolean Programs
de réir: Basler, G, et al.
Foilsithe / Cruthaithe: (2007)

Formal Verification of SystemC by Automatic Hardware/Software Partitioning
de réir: Kroening, D, et al.
Foilsithe / Cruthaithe: (2005)

A SAT−Based Algorithm for Reparameterization in Symbolic Simulation
de réir: Chauhan, P, et al.
Foilsithe / Cruthaithe: (2004)

A SAT-based algorithm for reparameterization in symbolic simulation
de réir: Chauhan, P, et al.
Foilsithe / Cruthaithe: (2004)

Accurate Theorem Proving for Program Verification
de réir: Cook, B, et al.
Foilsithe / Cruthaithe: (2006)

Verification of Boolean Programs with Unbounded Thread Creation
de réir: Cook, B, et al.
Foilsithe / Cruthaithe: (2007)

Verification of Boolean programs with unbounded thread creation.
de réir: Cook, B, et al.
Foilsithe / Cruthaithe: (2007)

Cogent: Accurate theorem proving for program verification
de réir: Cook, B, et al.
Foilsithe / Cruthaithe: (2005)

Symbolic model checking for asynchronous Boolean programs
de réir: Cook, B, et al.
Foilsithe / Cruthaithe: (2005)

Over−Approximating Boolean Programs with Unbounded Thread Creation
de réir: Cook, B, et al.
Foilsithe / Cruthaithe: (2006)

An expectation transformer approach to predicate abstraction and data independence for probabilistic programs
de réir: Ukachukwu Ndukwu, et al.
Foilsithe / Cruthaithe: (2010-06-01)