Constraint-based abstract semantics for temporal logic: a direct approach to design and implementation

DOI10.1007/978-3-642-17511-4_3MaRDI QIDQ3066089zbMATH OpenOpenAlexFDO

Authors Gourinath Banda, John P. Gallagher

Publication date 7 January 2011

Published in Logic for Programming, Artificial Intelligence, and Reasoning (Search for Journal in Brave)

Full work available at URL https://rucforsk.ruc.dk/ws/files/31511034/lpar16.pdf

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Recommendations

• Abstract interpretation of CTL properties
• Temporal abstract interpretation
• Refining and compressing abstract model checking
• scientific article; zbMATH DE number 2110619
• A CTL-based logic for program abstractions

Cited in

(12)

• Towards automatic temporal logic verification of value passing process algebra using abstract interpretation
• An abstract interpretation toolkit for \(\mu\)CRL
• Verifying increasingly expressive temporal logics for infinite-state systems
• Systems of fixpoint equations: abstraction, games, up-to techniques and local algorithms
• Program specialization for verifying infinite state systems: an experimental evaluation
• Efficient CTL verification via Horn constraints solving
• scientific article; zbMATH DE number 2086974 (Why is no real title available?)
• scientific article; zbMATH DE number 1504838 (Why is no real title available?)
• A CTL-based logic for program abstractions
• scientific article; zbMATH DE number 7559481 (Why is no real title available?)
• Abstract interpretation with infinitesimals. Towards scalability in nonstandard static analysis
• Temporal abstract interpretation

Describes a project that uses

Uses Software

• PHAVer
• HyTech
• Uppaal
• PPL

This page was built for publication: Constraint-based abstract semantics for temporal logic: a direct approach to design and implementation

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