Predicate abstraction of ANSI-C programs using SAT

Predicate abstraction of ANSI-C programs using SAT

Бусад хувилбаруудыг харуулах (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...

Бүрэн тодорхойлолт

Номзүйн дэлгэрэнгүй
Үндсэн зохиолчид:	Clarke, E, Kroening, D, Sharygina, N, al., E
Формат:	Journal article
Хэвлэсэн:	Springer 2004

Ижил төстэй зүйлс

Predicate Abstraction of ANSI-C Programs Using SAT.
-н: Clarke, E, зэрэг
Хэвлэсэн: (2004)

Predicate Abstraction of ANSI-C Programs Using SAT
-н: Clarke, E, зэрэг
Хэвлэсэн: (2004)

Predicate Abstraction of ANSI–C Programs using SAT
-н: Clarke, E, зэрэг
Хэвлэсэн: (2015)

SATABS: SAT−based Predicate Abstraction for ANSI−C
-н: Clarke, E, зэрэг
Хэвлэсэн: (2005)

Word Level Predicate Abstraction and Refinement for Verifying RTL Verilog
-н: Jain, H, зэрэг
Хэвлэсэн: (2008)

Word Level Predicate Abstraction and Refinement for Verifying RTL Verilog
-н: Jain, H, зэрэг
Хэвлэсэн: (2005)

Word level predicate abstraction and refinement for verifying RTL verilog
-н: Jain, H, зэрэг
Хэвлэсэн: (2005)

Word-Level Predicate-Abstraction and Refinement Techniques for Verifying RTL Verilog.
-н: Jain, H, зэрэг
Хэвлэсэн: (2008)

Verification of SpecC using Predicate Abstraction
-н: Clarke, E, зэрэг
Хэвлэсэн: (2007)

Verification of SpecC using predicate abstraction.
-н: Clarke, E, зэрэг
Хэвлэсэн: (2007)

Word-level predicate-abstraction and refinement rechniques for verifying RTL Verilog
-н: Jain, H, зэрэг
Хэвлэсэн: (2008)

Checking consistency of C and Verilog using predicate abstraction and induction
-н: Kroening, D, зэрэг
Хэвлэсэн: (2004)

Checking Consistency of C and Verilog using Predicate Abstraction and Induction
-н: Kroening, D, зэрэг
Хэвлэсэн: (2004)

Verification of SpecC and Verilog using Predicate Abstraction
-н: Jain, H, зэрэг
Хэвлэсэн: (2004)

Hardware Verification using ANSI−C Programs as a Reference
-н: Clarke, E, зэрэг
Хэвлэсэн: (2003)

Hardware verification using ANSI-C programs as a reference
-н: Clarke, E, зэрэг
Хэвлэсэн: (2003)

A Tool for Checking ANSI−C Programs
-н: Clarke, E, зэрэг
Хэвлэсэн: (2004)

Verification and Falsification of Programs with Loops Using Predicate Abstraction
-н: Kroening, D, зэрэг
Хэвлэсэн: (2009)

Verification and falsification of programs with loops using predicate abstraction.
-н: Kroening, D, зэрэг
Хэвлэсэн: (2010)

Approximating Predicate Images for Bit−Vector Logic
-н: Kroening, D, зэрэг
Хэвлэсэн: (2006)

Image Computation and Predicate Refinement for RTL Verilog using Word Level Proofs
-н: Kroening, D, зэрэг
Хэвлэсэн: (2007)

Verifying C++ with STL Containers via Predicate Abstraction
-н: Blanc, N, зэрэг
Хэвлэсэн: (2007)

Verifying C++ with STL containers via predicate abstraction
-н: Blanc, N, зэрэг
Хэвлэсэн: (2007)

Counterexamples with Loops for Predicate Abstraction
-н: Kroening, D, зэрэг
Хэвлэсэн: (2006)

VCEGAR: Verilog CounterExample Guided Abstraction Refinement
-н: Jain, H, зэрэг
Хэвлэсэн: (2007)

Model Checking with Abstraction for Web Services
-н: Sharygina, N, зэрэг
Хэвлэсэн: (2007)

Programming with ANSI C++ /
-н: 229185 Trivedi, Bhushan
Хэвлэсэн: (2007)

Programming in ANSI C /
-н: 279425 Kochan, Stephen G.
Хэвлэсэн: (1988)

Illustrated C programming (ANSI) /
-н: 198287 Beam, J. Emmett
Хэвлэсэн: (1989)

SAT−based Summarisation for Boolean Programs
-н: Basler, G, зэрэг
Хэвлэсэн: (2007)

Formal Verification of SystemC by Automatic Hardware/Software Partitioning
-н: Kroening, D, зэрэг
Хэвлэсэн: (2005)

A SAT−Based Algorithm for Reparameterization in Symbolic Simulation
-н: Chauhan, P, зэрэг
Хэвлэсэн: (2004)

A SAT-based algorithm for reparameterization in symbolic simulation
-н: Chauhan, P, зэрэг
Хэвлэсэн: (2004)

Accurate Theorem Proving for Program Verification
-н: Cook, B, зэрэг
Хэвлэсэн: (2006)

Verification of Boolean Programs with Unbounded Thread Creation
-н: Cook, B, зэрэг
Хэвлэсэн: (2007)

Verification of Boolean programs with unbounded thread creation.
-н: Cook, B, зэрэг
Хэвлэсэн: (2007)

Cogent: Accurate theorem proving for program verification
-н: Cook, B, зэрэг
Хэвлэсэн: (2005)

Symbolic model checking for asynchronous Boolean programs
-н: Cook, B, зэрэг
Хэвлэсэн: (2005)

Over−Approximating Boolean Programs with Unbounded Thread Creation
-н: Cook, B, зэрэг
Хэвлэсэн: (2006)

An expectation transformer approach to predicate abstraction and data independence for probabilistic programs
-н: Ukachukwu Ndukwu, зэрэг
Хэвлэсэн: (2010-06-01)