Making prophecies with decision predicates

DOI10.1145/1926385.1926431MaRDI QIDQ5408559zbMATH OpenOpenAlexFDO

Authors Byron Cook, Eric Koskinen

Publication date 10 April 2014

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

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

zbMATH Keywords

formal verificationlinear temporal logicmodel checkingprogram analysistermination

Mathematics Subject Classification ID

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

Recommendations

• Temporal property verification as a program analysis task
• Temporal prophecy for proving temporal properties of infinite-state systems
• scientific article; zbMATH DE number 4153903
• On automation of \(\mathsf{CTL}^*\) verification for infinite-state systems
• Probabilistic propositional temporal logics

Cited in

(8)

• Temporal prophecy for proving temporal properties of infinite-state systems
• Synthesizing precise and useful commutativity conditions
• Temporal property verification as a program analysis task
• Fold/unfold transformations for fixpoint logic
• Automatically verifying temporal properties of pointer programs with cyclic proof
• Proving LTL Properties of Bitvector Programs and Decompiled Binaries
• Temporal verification of programs via first-order fixpoint logic
• Automatic analysis of DMA races using model checking and k-induction

Describes a project that uses

Uses Software

• PostgreSQL

This page was built for publication: Making prophecies with decision predicates

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