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)