Abstract interpretation of CTL properties

DOI10.1007/978-3-319-99725-4_24MaRDI QIDQ6045023zbMATH OpenOpenAlexFDO

Authors C. Urban, Samuel Ueltschi, Peter Müller

Publication date 26 May 2023

Published in Static Analysis (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-99725-4_24

Mathematics Subject Classification ID

Temporal logic (03B44) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Semantics in the theory of computing (68Q55)

Recommendations

• A CTL-based logic for program abstractions
• Property directed abstract interpretation
• scientific article; zbMATH DE number 1953027
• Abstract interpretation from a denotational-semantics perspective
• scientific article; zbMATH DE number 2090155
• Abstract Interpretation Frameworks
• scientific article; zbMATH DE number 1405453
• Frameworks for abstract interpretation
• Tools and Algorithms for the Construction and Analysis of Systems

Cited in

(8)

• On automation of \(\mathsf{CTL}^*\) verification for infinite-state systems
• Constraint-based abstract semantics for temporal logic: a direct approach to design and implementation
• A CTL-based logic for program abstractions
• Fold/unfold transformations for fixpoint logic
• Proving guarantee and recurrence temporal properties by abstract interpretation
• Algebraic Methodology and Software Technology
• Temporal verification of programs via first-order fixpoint logic
• Automatic detection of vulnerable variables for CTL properties of programs

This page was built for publication: Abstract interpretation of CTL properties

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