Verification and falsification of programs with loops using predicate abstraction.

Verification and falsification of programs with loops using predicate abstraction.

Show other versions (1)

Predicate abstraction is amajor abstraction technique for the verification of software.Data is abstracted by means of Boolean variables, which keep track of predicates over the data. In many cases, predicate abstraction suffers from the need for at least one predicate for each iteration of a loop co...

Disgrifiad llawn

Manylion Llyfryddiaeth
Prif Awduron:	Kroening, D, Weissenbacher, G
Fformat:	Journal article
Iaith:	English
Cyhoeddwyd:	2010

Eitemau Tebyg

Verification and Falsification of Programs with Loops Using Predicate Abstraction
gan: Kroening, D, et al.
Cyhoeddwyd: (2009)

Counterexamples with Loops for Predicate Abstraction
gan: Kroening, D, et al.
Cyhoeddwyd: (2006)

Verification of SpecC using predicate abstraction.
gan: Clarke, E, et al.
Cyhoeddwyd: (2007)

Verification of SpecC using Predicate Abstraction
gan: Clarke, E, et al.
Cyhoeddwyd: (2007)

Verification of SpecC and Verilog using Predicate Abstraction
gan: Jain, H, et al.
Cyhoeddwyd: (2004)

Predicate Abstraction of ANSI-C Programs Using SAT.
gan: Clarke, E, et al.
Cyhoeddwyd: (2004)

Predicate Abstraction of ANSI-C Programs Using SAT
gan: Clarke, E, et al.
Cyhoeddwyd: (2004)

Predicate Abstraction of ANSI–C Programs using SAT
gan: Clarke, E, et al.
Cyhoeddwyd: (2015)

Predicate abstraction of ANSI-C programs using SAT
gan: Clarke, E, et al.
Cyhoeddwyd: (2004)

Checking consistency of C and Verilog using predicate abstraction and induction
gan: Kroening, D, et al.
Cyhoeddwyd: (2004)

Checking Consistency of C and Verilog using Predicate Abstraction and Induction
gan: Kroening, D, et al.
Cyhoeddwyd: (2004)

Verification, falsification and cancellation in KT
gan: Williamson, T
Cyhoeddwyd: (1990)

Verifying C++ with STL Containers via Predicate Abstraction
gan: Blanc, N, et al.
Cyhoeddwyd: (2007)

Verifying C++ with STL containers via predicate abstraction
gan: Blanc, N, et al.
Cyhoeddwyd: (2007)

SATABS: SAT−based Predicate Abstraction for ANSI−C
gan: Clarke, E, et al.
Cyhoeddwyd: (2005)

Under-approximating loops in C programs for fast counterexample detection
gan: Kroening, D, et al.
Cyhoeddwyd: (2015)

Under-approximating loops in C programs for fast counterexample detection
gan: Kroening, D, et al.
Cyhoeddwyd: (2013)

Word Level Predicate Abstraction and Refinement for Verifying RTL Verilog
gan: Jain, H, et al.
Cyhoeddwyd: (2008)

Word Level Predicate Abstraction and Refinement for Verifying RTL Verilog
gan: Jain, H, et al.
Cyhoeddwyd: (2005)

Word level predicate abstraction and refinement for verifying RTL verilog
gan: Jain, H, et al.
Cyhoeddwyd: (2005)

Word-Level Predicate-Abstraction and Refinement Techniques for Verifying RTL Verilog.
gan: Jain, H, et al.
Cyhoeddwyd: (2008)

Word-level predicate-abstraction and refinement rechniques for verifying RTL Verilog
gan: Jain, H, et al.
Cyhoeddwyd: (2008)

A New Approach to Model Verification, Falsification and Selection
gan: Andrew J. Buck, et al.
Cyhoeddwyd: (2015-06-01)

Formal Verification at Higher Levels of Abstraction
gan: Kroening, D, et al.
Cyhoeddwyd: (2007)

Lifting CDCL to template-based abstract domains for program verification
gan: Mukherjee, R, et al.
Cyhoeddwyd: (2017)

Interpolation−based verification of floating−point programs with abstract CDCL
gan: Brain, M, et al.
Cyhoeddwyd: (2013)

Interpolation-based verification of floating-point programs with abstract CDCL
gan: Brain, M, et al.
Cyhoeddwyd: (2013)

Unbounded verification, falsification, and characterization of security protocols by pattern refinement
gan: Cremers, C
Cyhoeddwyd: (2008)

A Survey of Automated Techniques for Formal Software Verification.
gan: D'Silva, V, et al.
Cyhoeddwyd: (2008)

A survey of automated techniques for formal software verification
gan: D'Silva, V, et al.
Cyhoeddwyd: (2008)

A Survey of Automated Techniques for Formal Software Verification
gan: D'Silva, V, et al.
Cyhoeddwyd: (2008)

Convex polyhedral abstractions, specialisation and property-based predicate splitting in Horn clause verification
gan: Bishoksan Kafle, et al.
Cyhoeddwyd: (2014-12-01)

The scyther tool: Verification, falsification, and analysis of security protocols - Tool paper
gan: Cremers, C
Cyhoeddwyd: (2008)

Revelation and falsification :
gan: 9th cent., et al.
Cyhoeddwyd: (2009)

Game−Based Probabilistic Predicate Abstraction in PRISM
gan: Kattenbelt, M, et al.
Cyhoeddwyd: (2008)

Game−Based Probabilistic Predicate Abstraction in PRISM
gan: Kattenbelt, M, et al.
Cyhoeddwyd: (2008)

Quantum Epistemology and Falsification
gan: Giacomo Mauro D’Ariano
Cyhoeddwyd: (2022-03-01)

An expectation transformer approach to predicate abstraction and data independence for probabilistic programs
gan: Ukachukwu Ndukwu, et al.
Cyhoeddwyd: (2010-06-01)

Predicate Abstraction with Under-approximation Refinement
gan: Corina S. Pasareanu, et al.
Cyhoeddwyd: (2007-02-01)

Approximating Predicate Images for Bit−Vector Logic
gan: Kroening, D, et al.
Cyhoeddwyd: (2006)