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...

Bibliografske podrobnosti
Main Authors:	Clarke, E, Kroening, D, Sharygina, N, al., E
Format:	Journal article
Izdano:	Springer 2004

Podobne knjige/članki

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Programming with ANSI C++ /
od: 229185 Trivedi, Bhushan
Izdano: (2007)

Programming in ANSI C /
od: 279425 Kochan, Stephen G.
Izdano: (1988)

Illustrated C programming (ANSI) /
od: 198287 Beam, J. Emmett
Izdano: (1989)

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

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

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

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

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

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

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

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

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

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

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