Abstract animator for temporal specifications: Application to TLA

DOI10.1007/3-540-48294-6_18MaRDI QIDQ4494386zbMATH OpenFDO

Authors Dominique Cansell, Dominique Mery

Publication date 10 August 2000

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-48294-6_18

zbMATH Keywords

temporal specificationsTLA

Mathematics Subject Classification ID

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

Recommendations

• Temporal abstract interpretation
• Constraint-based abstract semantics for temporal logic: a direct approach to design and implementation
• scientific article; zbMATH DE number 1390334

Cited in

(6)

• Automatic verification of TLA\(^{ + }\) proof obligations with SMT solvers
• scientific article; zbMATH DE number 4119617 (Why is no real title available?)
• Animating TLA specifications
• Timed Abstract Dialectical Frameworks: A Simple Translation-Based Approach
• Temporal abstract interpretation
• Extracting Symbolic Transitions from TLA$$^{+}$$+ Specifications

This page was built for publication: Abstract animator for temporal specifications: Application to TLA

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