Partial predicate abstraction and counter-example guided refinement

DOI10.1016/J.JLAMP.2019.01.003MaRDI QIDQ2291815zbMATH OpenOpenAlexWikidataFDO

Authors Tuba Yavuz

Publication date 31 January 2020

Published in Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1712.01734

zbMATH Keywords

model checkingpredicate abstractionfixpoint approximations

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70)

Abstract: In this paper we present a counter-example guided abstraction and approximation refinement (CEGAAR) technique for {em partial predicate abstraction}, which combines predicate abstraction and fixpoint approximations for model checking infinite-state systems. The proposed approach incrementally considers growing sets of predicates for abstraction refinement. The novelty of the approach stems from recognizing source of the imprecision: abstraction or approximation. We use Craig interpolation to deal with imprecision due to abstraction. In the case of imprecision due to approximation, we delay application of the approximation. Our experimental results on a variety of models provide insights into effectiveness of partial predicate abstraction as well as refinement techniques in this context.

Recommendations

• Abstract Counterexamples for Non-disjunctive Abstractions
• Tools and Algorithms for the Construction and Analysis of Systems
• Computer Aided Verification
• scientific article; zbMATH DE number 1670775
• Probabilistic CEGAR

Cites work

• scientific article; zbMATH DE number 1670775 (Why is no real title available?)
• scientific article; zbMATH DE number 108539 (Why is no real title available?)
• scientific article; zbMATH DE number 1324833 (Why is no real title available?)
• scientific article; zbMATH DE number 1956569 (Why is no real title available?)
• scientific article; zbMATH DE number 1979542 (Why is no real title available?)
• scientific article; zbMATH DE number 2086591 (Why is no real title available?)
• scientific article; zbMATH DE number 1903358 (Why is no real title available?)
• Action language verifier: An infinite-state model checker for reactive software specifications
• Combining Predicate Abstraction with Fixpoint Approximations
• Linear reasoning. A new form of the Herbrand-Gentzen theorem
• Making predicate abstraction efficient: how to eliminate redundant predicates
• Property preserving abstractions for the verification of concurrent systems
• Theory and Applications of Satisfiability Testing
• Tools and Algorithms for the Construction and Analysis of Systems
• Transition predicate abstraction and fair termination

Cited in

(9)

• Abstract Counterexamples for Non-disjunctive Abstractions
• Relaxed stratification: a new approach to practical complete predicate refinement
• Computer Aided Verification
• Abstract Counterexample-Based Refinement for Powerset Domains
• Unification and combination of a class of traversal strategies made with pattern matching and fixed-points
• Accelerating interpolants
• Predicate Abstraction with Under-approximation Refinement
• Probabilistic CEGAR
• Abstraction refinement for games with incomplete information

Describes a project that uses

Uses Software

• Omega

This page was built for publication: Partial predicate abstraction and counter-example guided refinement

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