Predicate Abstraction with Under-approximation Refinement

DOI10.2168/LMCS-3(1:5)2007MaRDI QIDQ5310681zbMATH OpenWikidataFDO

Authors Radek Pelánek, Willem Visser, Corina S. Păsăreanu

Publication date 11 October 2007

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.2168/LMCS-3(1:5)2007

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Combining Predicate Abstraction with Fixpoint Approximations
• Tools and Algorithms for the Construction and Analysis of Systems
• Predicate abstraction in a program logic calculus
• Predicate Abstraction in a Program Logic Calculus
• Predicate abstraction with minimum predicates
• Partial predicate abstraction and counter-example guided refinement
• Predicate abstraction of rewrite theories
• Predicate Abstraction of Programs with Non-linear Computation
• Predicate Abstraction via Symbolic Decision Procedures
• Computer Aided Verification

Cited in

(16)

• Leaping Loops in the Presence of Abstraction
• Test generation from event system abstractions to cover their states and transitions
• Combining Predicate Abstraction with Fixpoint Approximations
• Using Predicate Abstraction to Generate Heuristic Functions in UPPAAL
• An automatic method for the dynamic construction of abstractions of states of a formal model
• Under-approximation generation driven by relevance predicates and variants
• Necessary and Sufficient Preconditions via Eager Abstraction
• Better Under-Approximation of Programs by Hiding Variables
• Proving the existence of fair paths in infinite-state systems
• Predicate abstraction of rewrite theories
• Model Checking Recursive Programs with Exact Predicate Abstraction
• Tools and Algorithms for the Construction and Analysis of Systems
• Approximating event system abstractions by covering their states and transitions
• Underapproximating Predicate Transformers
• Predicate abstraction with indexed predicates
• Predicate abstraction for hyperliveness verification

This page was built for publication: Predicate Abstraction with Under-approximation Refinement

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5310681)