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)