Sometime = always + recursion \(\equiv\) always. On the equivalence of the intermittent and invariant assertions methods for proving inevitability properties of programs

DOI10.1007/BF00290704zbMath0586.68019OpenAlexW2061903816MaRDI QIDQ1071491

Patrick Cousot, Radhia Cousot

Publication date: 1987

Published in: Acta Informatica (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bf00290704

zbMATH Keywords

induction principlesBurstall's intermittent assertionscorrectness of sequential programsFloyd's invariant assertionsinevitability properties of programsnondeterministic transition systems

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items

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