Sometime = always + recursion \(\equiv\) always. On the equivalence of the intermittent and invariant assertions methods for proving inevitability properties of programs
From MaRDI portal
Publication:1071491
DOI10.1007/BF00290704zbMath0586.68019OpenAlexW2061903816MaRDI QIDQ1071491
Publication date: 1987
Published in: Acta Informatica (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/bf00290704
induction principlesBurstall's intermittent assertionscorrectness of sequential programsFloyd's invariant assertionsinevitability properties of programsnondeterministic transition systems
Related Items (11)
Incremental Computation of Succinct Abstractions for Hybrid Systems ⋮ Convergence: integrating termination and abort-freedom ⋮ An integrated approach to high integrity software verification ⋮ From chaotic iteration to constraint propagation ⋮ Compositional characterization of observable program properties ⋮ Deciding program properties via complete abstractions on bounded domains ⋮ Properties of data flow frameworks: A unified model ⋮ ``A la Burstall intermittent assertions induction principles for proving inevitability properties of programs ⋮ Certification Using the Mobius Base Logic ⋮ Internal and External Logics of Abstract Interpretations ⋮ Security protocols: from linear to classical logic by abstract interpretation
Cites Work
- ``A la Burstall intermittent assertions induction principles for proving inevitability properties of programs
- Is Sometimes Ever Better Than Always?
- Proving Liveness Properties of Concurrent Programs
- Formal verification of parallel programs
- Is “sometime” sometimes better than “always”?
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: Sometime = always + recursion \(\equiv\) always. On the equivalence of the intermittent and invariant assertions methods for proving inevitability properties of programs
