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

model checkingtemporal logicformal verificationprogram analysishigher-order programs

Mathematics Subject Classification ID

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

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)

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

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)