The following pages link to (Q4054648):
Displaying 38 items.
- Linear temporal logic symbolic model checking (Q465680) (← links)
- Synthesis of list algorithms by mechanical proving (Q485837) (← links)
- Total correctness in nonstandard logics of programs (Q580955) (← links)
- The Schorr-Waite graph marking algorithm (Q599496) (← links)
- ``A la Burstall'' intermittent assertions induction principles for proving inevitability properties of programs (Q689297) (← links)
- Constructive modal logics. I (Q750417) (← links)
- Correctness of recursive parallel nondeterministic flow programs (Q789165) (← links)
- Verifying programs by induction on their data structure: general format and applications (Q1050765) (← links)
- Sometime = always + recursion \(\equiv\) always. On the equivalence of the intermittent and invariant assertions methods for proving inevitability properties of programs (Q1071491) (← links)
- Non-standard algorithmic and dynamic logic (Q1077159) (← links)
- Weak second order characterizations of various program verification systems (Q1124311) (← links)
- Proving the correctness of regular deterministic programs: A unifying survey using dynamic logic (Q1139368) (← links)
- On the algebra of order (Q1143782) (← links)
- Application of modal logic to programming (Q1150592) (← links)
- A proof method for cyclic programs (Q1242445) (← links)
- The correctness of the Schorr-Waite list marking algorithm (Q1250706) (← links)
- Formal derivation of strongly correct concurrent programs (Q1251066) (← links)
- Axiomatic proofs of total correctness of programs (Q1257332) (← links)
- On proving the termination of algorithms by machine (Q1341666) (← links)
- Reuse of proofs in software verification (Q1419888) (← links)
- Is ``Some-other-time'' sometimes better than ``Sometime'' for proving partial correctness of programs? (Q1825630) (← links)
- RGITL: a temporal logic framework for compositional reasoning about interleaved programs (Q2251128) (← links)
- Tableaux for constructive concurrent dynamic logic (Q2488268) (← links)
- Formal Verification of a Lock-Free Stack with Hazard Pointers (Q3105753) (← links)
- The Birth of Model Checking (Q3512430) (← links)
- From Philosophical to Industrial Logics (Q3601803) (← links)
- Méthode axiomatique sur les propriétés de fatalité des programmes parallèles (Q3761687) (← links)
- A case study in program transformation (Q4109267) (← links)
- (Q4184287) (← links)
- (Q4742767) (← links)
- On Fixpoint/Iteration/Variant Induction Principles for Proving Total Correctness of Programs with Denotational Semantics (Q5097622) (← links)
- Meanings of Model Checking (Q5187832) (← links)
- KeY: A Formal Method for Object-Oriented Systems (Q5428904) (← links)
- From Monadic Logic to PSL (Q5452203) (← links)
- Does “N+1 times” prove more programs correct than “N times”? (Q5887528) (← links)
- Tactical theorem proving in program verification (Q6488526) (← links)
- Abstract execution (Q6535957) (← links)
- Schematic program proofs with abstract execution. Theory and applications (Q6552501) (← links)
