Predicate abstraction of ANSI-C programs using SAT

Predicate abstraction of ANSI-C programs using SAT

Hiển thị phiên bản (3) khác

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

Mô tả đầy đủ

Chi tiết về thư mục
Những tác giả chính:	Clarke, E, Kroening, D, Sharygina, N, al., E
Định dạng:	Journal article
Được phát hành:	Springer 2004

Những quyển sách tương tự

Predicate Abstraction of ANSI-C Programs Using SAT.
Bằng: Clarke, E, et al.
Được phát hành: (2004)

Predicate Abstraction of ANSI-C Programs Using SAT
Bằng: Clarke, E, et al.
Được phát hành: (2004)

Predicate Abstraction of ANSI–C Programs using SAT
Bằng: Clarke, E, et al.
Được phát hành: (2015)

SATABS: SAT−based Predicate Abstraction for ANSI−C
Bằng: Clarke, E, et al.
Được phát hành: (2005)

Word Level Predicate Abstraction and Refinement for Verifying RTL Verilog
Bằng: Jain, H, et al.
Được phát hành: (2008)

Word Level Predicate Abstraction and Refinement for Verifying RTL Verilog
Bằng: Jain, H, et al.
Được phát hành: (2005)

Word level predicate abstraction and refinement for verifying RTL verilog
Bằng: Jain, H, et al.
Được phát hành: (2005)

Word-Level Predicate-Abstraction and Refinement Techniques for Verifying RTL Verilog.
Bằng: Jain, H, et al.
Được phát hành: (2008)

Verification of SpecC using Predicate Abstraction
Bằng: Clarke, E, et al.
Được phát hành: (2007)

Verification of SpecC using predicate abstraction.
Bằng: Clarke, E, et al.
Được phát hành: (2007)

Word-level predicate-abstraction and refinement rechniques for verifying RTL Verilog
Bằng: Jain, H, et al.
Được phát hành: (2008)

Checking consistency of C and Verilog using predicate abstraction and induction
Bằng: Kroening, D, et al.
Được phát hành: (2004)

Checking Consistency of C and Verilog using Predicate Abstraction and Induction
Bằng: Kroening, D, et al.
Được phát hành: (2004)

Verification of SpecC and Verilog using Predicate Abstraction
Bằng: Jain, H, et al.
Được phát hành: (2004)

Hardware Verification using ANSI−C Programs as a Reference
Bằng: Clarke, E, et al.
Được phát hành: (2003)

Hardware verification using ANSI-C programs as a reference
Bằng: Clarke, E, et al.
Được phát hành: (2003)

A Tool for Checking ANSI−C Programs
Bằng: Clarke, E, et al.
Được phát hành: (2004)

Verification and Falsification of Programs with Loops Using Predicate Abstraction
Bằng: Kroening, D, et al.
Được phát hành: (2009)

Verification and falsification of programs with loops using predicate abstraction.
Bằng: Kroening, D, et al.
Được phát hành: (2010)

Approximating Predicate Images for Bit−Vector Logic
Bằng: Kroening, D, et al.
Được phát hành: (2006)

Image Computation and Predicate Refinement for RTL Verilog using Word Level Proofs
Bằng: Kroening, D, et al.
Được phát hành: (2007)

Verifying C++ with STL Containers via Predicate Abstraction
Bằng: Blanc, N, et al.
Được phát hành: (2007)

Verifying C++ with STL containers via predicate abstraction
Bằng: Blanc, N, et al.
Được phát hành: (2007)

Counterexamples with Loops for Predicate Abstraction
Bằng: Kroening, D, et al.
Được phát hành: (2006)

VCEGAR: Verilog CounterExample Guided Abstraction Refinement
Bằng: Jain, H, et al.
Được phát hành: (2007)

Model Checking with Abstraction for Web Services
Bằng: Sharygina, N, et al.
Được phát hành: (2007)

Programming with ANSI C++ /
Bằng: 229185 Trivedi, Bhushan
Được phát hành: (2007)

Programming in ANSI C /
Bằng: 279425 Kochan, Stephen G.
Được phát hành: (1988)

Illustrated C programming (ANSI) /
Bằng: 198287 Beam, J. Emmett
Được phát hành: (1989)

SAT−based Summarisation for Boolean Programs
Bằng: Basler, G, et al.
Được phát hành: (2007)

Formal Verification of SystemC by Automatic Hardware/Software Partitioning
Bằng: Kroening, D, et al.
Được phát hành: (2005)

A SAT−Based Algorithm for Reparameterization in Symbolic Simulation
Bằng: Chauhan, P, et al.
Được phát hành: (2004)

A SAT-based algorithm for reparameterization in symbolic simulation
Bằng: Chauhan, P, et al.
Được phát hành: (2004)

Accurate Theorem Proving for Program Verification
Bằng: Cook, B, et al.
Được phát hành: (2006)

Verification of Boolean Programs with Unbounded Thread Creation
Bằng: Cook, B, et al.
Được phát hành: (2007)

Verification of Boolean programs with unbounded thread creation.
Bằng: Cook, B, et al.
Được phát hành: (2007)

Cogent: Accurate theorem proving for program verification
Bằng: Cook, B, et al.
Được phát hành: (2005)

Symbolic model checking for asynchronous Boolean programs
Bằng: Cook, B, et al.
Được phát hành: (2005)

Over−Approximating Boolean Programs with Unbounded Thread Creation
Bằng: Cook, B, et al.
Được phát hành: (2006)

An expectation transformer approach to predicate abstraction and data independence for probabilistic programs
Bằng: Ukachukwu Ndukwu, et al.
Được phát hành: (2010-06-01)