Partial predicate abstraction and counter-example guided refinement

DOI10.1016/j.jlamp.2019.01.003zbMath1494.68177arXiv1712.01734OpenAlexW2963357686WikidataQ128537623 ScholiaQ128537623MaRDI QIDQ2291815

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

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

Related Items (1)

Unification and combination of a class of traversal strategies made with pattern matching and fixed-points

Uses Software

• Omega

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Action language verifier: An infinite-state model checker for reactive software specifications
• Property preserving abstractions for the verification of concurrent systems
• Linear reasoning. A new form of the Herbrand-Gentzen theorem
• Combining Predicate Abstraction with Fixpoint Approximations
• Transition predicate abstraction and fair termination
• Theory and Applications of Satisfiability Testing
• Tools and Algorithms for the Construction and Analysis of Systems
• Computer Aided Verification

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