Ranked Predicate Abstraction for Branching Time: Complete, Incremental, and Precise

DOI10.1007/11901914_25MaRDI QIDQ3522918zbMATH OpenOpenAlexFDO

Authors Michael Huth, Harald Fecher

Publication date 4 September 2008

Published in Automated Technology for Verification and Analysis (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/11901914_25

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Abstraction for branching time properties.
• Automated Technology for Verification and Analysis
• Predicate abstraction for dense real-time systems
• Tools and Algorithms for the Construction and Analysis of Systems
• MODULAR RANKING ABSTRACTION

Cited in

(9)

• Refinement sensitive formal semantics of state machines with persistent choice
• Predicate abstraction for dense real-time systems
• Process algebra having inherent choice: revised semantics for concurrent systems
• More Precise Partition Abstractions
• Model Checking for Action Abstraction
• Correct Hardware Design and Verification Methods
• Abstraction for branching time properties.
• Inference of ranking functions for proving temporal properties by abstract interpretation
• Comparing disjunctive modal transition systems with an one-selecting variant

Describes a project that uses

Uses Software

• CESAR

This page was built for publication: Ranked Predicate Abstraction for Branching Time: Complete, Incremental, and Precise

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