Temporal abstract interpretation

DOI10.1145/325694.325699MaRDI QIDQ5178838zbMATH OpenOpenAlexFDO

Authors Patrick Cousot, Radhia Cousot

Publication date 17 March 2015

Published in Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/325694.325699

Mathematics Subject Classification ID

Temporal logic (03B44) Functional programming and lambda calculus (68N18) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Constraint-based abstract semantics for temporal logic: a direct approach to design and implementation
• scientific article; zbMATH DE number 1692938
• scientific article; zbMATH DE number 1948413
• A CTL-based logic for program abstractions
• scientific article; zbMATH DE number 1487859

Cited in

(35)

• Constructive design of a hierarchy of semantics of a transition system by abstract interpretation
• Parsing as abstract interpretation of grammar semantics
• Semantics of temporal classes
• On collecting semantics for program analysis
• Fixpoint theory -- upside down
• Incompleteness of states w.r.t. traces in model checking
• scientific article; zbMATH DE number 1692938 (Why is no real title available?)
• Abstract interpretation from a denotational-semantics perspective
• Constraint-based abstract semantics for temporal logic: a direct approach to design and implementation
• Abstraction and abstraction refinement
• Towards the Verification of Attributed Graph Transformation Systems
• Inverse-limit and topological aspects of abstract interpretation
• scientific article; zbMATH DE number 1948413 (Why is no real title available?)
• scientific article; zbMATH DE number 1487859 (Why is no real title available?)
• Model-checking view-based partial specifications
• Refining and compressing abstract model checking
• A CTL-based logic for program abstractions
• Constructive Galois connections
• scientific article; zbMATH DE number 7559481 (Why is no real title available?)
• Extracting program logics from abstract interpretations defined by logical relations
• Internal and External Logics of Abstract Interpretations
• Programming Languages and Systems
• Calculational design of a regular model checker by abstract interpretation
• Observational Completeness on Abstract Interpretation
• Abstract interpretation, Hoare logic, and incorrectness logic for quantum programs
• Towards automatic temporal logic verification of value passing process algebra using abstract interpretation
• A state/event-based model-checking approach for the analysis of abstract system properties
• Syntactic and semantic soundness of structural dataflow analysis
• Systems of fixpoint equations: abstraction, games, up-to techniques and local algorithms
• Expressive quantale-valued logics for coalgebras: an adjunction-based approach
• A monoidal view on fixpoint checks
• Trace-based deductive verification
• Model checking as program verification by abstract interpretation
• On model checking multiple hybrid views
• Partial model checking via abstract interpretation

This page was built for publication: Temporal abstract interpretation

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