Making prophecies with decision predicates

DOI10.1145/1926385.1926431zbMath1284.68389OpenAlexW4254770492MaRDI QIDQ5408559

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 verificationmodel checkingprogram analysisterminationlinear temporal logic

Mathematics Subject Classification ID

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

Related Items (6)

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 ⋮ Temporal prophecy for proving temporal properties of infinite-state systems ⋮ Automatic analysis of DMA races using model checking and \(k\)-induction

Uses Software

• PostgreSQL

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