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)