Local temporal reasoning

DOI10.1145/2603088.2603138MaRDI QIDQ4635644zbMATH OpenOpenAlexFDO

Authors Eric Koskinen, Tachio Terauchi

Publication date 23 April 2018

Published in Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) (Search for Journal in Brave)

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

zbMATH Keywords

formal verificationhigher-order programsmodel checkingprogram analysistemporal logic

Mathematics Subject Classification ID

Temporal logic (03B44) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Temporal reasoning for procedural programs
• A fixpoint logic and dependent effects for temporal property verification
• Temporal refinements for guarded recursive types
• scientific article; zbMATH DE number 4153903
• scientific article; zbMATH DE number 4182845

Cited in

(9)

• Temporal refinements for guarded recursive types
• Temporal reasoning for procedural programs
• A fixpoint logic and dependent effects for temporal property verification
• Symbolic and Quantitative Approaches to Reasoning with Uncertainty
• Automated temporal verification for algebraic effects
• Commutativity for concurrent program termination proofs
• Temporal verification of programs via first-order fixpoint logic
• A temporal logic for higher-order functional programs
• Infinitary refinement types for temporal properties in Scott domains

This page was built for publication: Local temporal reasoning

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