Pages that link to "Item:Q1071491"
From MaRDI portal
The following pages link to Sometime = always + recursion \(\equiv\) always. On the equivalence of the intermittent and invariant assertions methods for proving inevitability properties of programs (Q1071491):
Displaying 14 items.
- ``A la Burstall'' intermittent assertions induction principles for proving inevitability properties of programs (Q689297) (← links)
- An integrated approach to high integrity software verification (Q861714) (← links)
- Properties of data flow frameworks: A unified model (Q910237) (← links)
- Comments on ``On the proof of a distributed algorithm'': Always-true is not invariant (Q918207) (← links)
- Security protocols: from linear to classical logic by abstract interpretation (Q1041815) (← links)
- Comments on ''Always-true is not invariant'': Assertional reasoning about invariance (Q1183477) (← links)
- Convergence: integrating termination and abort-freedom (Q1647960) (← links)
- Is ``Some-other-time'' sometimes better than ``Sometime'' for proving partial correctness of programs? (Q1825630) (← links)
- Incremental Computation of Succinct Abstractions for Hybrid Systems (Q3172856) (← links)
- Certification Using the Mobius Base Logic (Q3602993) (← links)
- Compositional characterization of observable program properties (Q4020510) (← links)
- From chaotic iteration to constraint propagation (Q4571938) (← links)
- Internal and External Logics of Abstract Interpretations (Q5452722) (← links)
- Does “N+1 times” prove more programs correct than “N times”? (Q5887528) (← links)
