scientific article
From MaRDI portal
Publication:4054648
zbMath0299.68012MaRDI QIDQ4054648
Publication date: 1974
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Related Items
Non-standard algorithmic and dynamic logic, Does “N+1 times” prove more programs correct than “N times”?, On proving the termination of algorithms by machine, The Schorr-Waite graph marking algorithm, Weak second order characterizations of various program verification systems, Méthode axiomatique sur les propriétés de fatalité des programmes parallèles, On Fixpoint/Iteration/Variant Induction Principles for Proving Total Correctness of Programs with Denotational Semantics, Unnamed Item, Proving the correctness of regular deterministic programs: A unifying survey using dynamic logic, On the algebra of order, The Birth of Model Checking, Application of modal logic to programming, Unnamed Item, Reuse of proofs in software verification, Linear temporal logic symbolic model checking, Synthesis of list algorithms by mechanical proving, A case study in program transformation, RGITL: a temporal logic framework for compositional reasoning about interleaved programs, ``A la Burstall intermittent assertions induction principles for proving inevitability properties of programs, Tableaux for constructive concurrent dynamic logic, KeY: A Formal Method for Object-Oriented Systems, Meanings of Model Checking, From Philosophical to Industrial Logics, Total correctness in nonstandard logics of programs, A proof method for cyclic programs, From Monadic Logic to PSL, The correctness of the Schorr-Waite list marking algorithm, Formal derivation of strongly correct concurrent programs, Axiomatic proofs of total correctness of programs, Constructive modal logics. I, Is ``Some-other-time sometimes better than ``Sometime for proving partial correctness of programs?, Formal Verification of a Lock-Free Stack with Hazard Pointers, Correctness of recursive parallel nondeterministic flow programs, Verifying programs by induction on their data structure: general format and applications, Sometime = always + recursion \(\equiv\) always. On the equivalence of the intermittent and invariant assertions methods for proving inevitability properties of programs
