Pages that link to "Item:Q4151703"
From MaRDI portal
The following pages link to Soundness and Completeness of an Axiom System for Program Verification (Q4151703):
Displaying 50 items.
- Completeness for recursive procedures in separation logic (Q278747) (← links)
- An observationally complete program logic for imperative higher-order functions (Q387994) (← links)
- Verification of object-oriented programs: a transformational approach (Q439944) (← links)
- Reasoning about procedures as parameters in the language L4 (Q583874) (← links)
- Comments on a paper by Neuhold and Studer (Q598797) (← links)
- Proof methods of declarative properties of definite programs (Q685395) (← links)
- Eliminating the substitution axiom from UNITY logic (Q751848) (← links)
- Semantics of algorithmic languages (Q760200) (← links)
- Wythoff games, continued fractions, cedar trees and Fibonacci searches (Q761983) (← links)
- Proving program inclusion using Hoare's logic (Q789887) (← links)
- Correctness of programs with Pascal-like procedures without global variables (Q790607) (← links)
- A probabilistic dynamic logic (Q792757) (← links)
- Two theorems about the completeness of Hoare's logic (Q794426) (← links)
- Average case optimality for linear problems (Q796299) (← links)
- The axiomatic semantics of programs based on Hoare's logic (Q800712) (← links)
- Weakly expressive models for Hoare logic (Q805248) (← links)
- A complete axiomatic semantics of spawning (Q808281) (← links)
- Verification conditions are code (Q855274) (← links)
- A compositional natural semantics and Hoare logic for low-level languages (Q877026) (← links)
- Automated compositional proofs for real-time systems (Q882449) (← links)
- Completeness of Hoare logic with inputs over the standard model (Q896915) (← links)
- Semantical analysis of specification logic (Q913527) (← links)
- On the completeness of modular proof systems (Q917327) (← links)
- A mechanical analysis of program verification strategies (Q928673) (← links)
- Deductive verification of alternating systems (Q939163) (← links)
- Differential dynamic logic for hybrid systems (Q1040772) (← links)
- Ten years of Hoare's logic: A survey. II: Nondeterminism (Q1056534) (← links)
- Some questions about expressiveness and relative completeness in Hoare's logic (Q1064046) (← links)
- An axiomatic semantics for nested concurrency (Q1077155) (← links)
- Non-standard algorithmic and dynamic logic (Q1077159) (← links)
- Partial correctness of exits from concurrent structures (Q1080654) (← links)
- Arithmetical axiomatization of first-order temporal logic (Q1101100) (← links)
- Some general incompleteness results for partial correctness logics (Q1110500) (← links)
- Semantics and verification of monitors and systems of monitors and processes (Q1112588) (← links)
- Arithmetical completeness versus relative completeness (Q1117212) (← links)
- A language independent proof of the soundness and completeness of generalized Hoare logic (Q1122978) (← links)
- Proving the correctness of regular deterministic programs: A unifying survey using dynamic logic (Q1139368) (← links)
- Recursive assertions and parallel programs (Q1140981) (← links)
- A simple relation between relational and predicate transformer semantics for nondeterministic programs (Q1156476) (← links)
- Floyd's principle, correctness theories and program equivalence (Q1158948) (← links)
- A complete logic for reasoning about programs via nonstandard model theory. II (Q1159461) (← links)
- On termination problems for finitely interpreted ALGOL-like programs (Q1161274) (← links)
- Programs and program verifications in a general setting (Q1162355) (← links)
- Some natural structures which fail to possess a sound and decidable Hoare-like logic for their while-programs (Q1163369) (← links)
- Hoare's logic and Peano's arithmetic (Q1170877) (← links)
- A Hoare-like verification system for a language with an exception handling mechanism (Q1176241) (← links)
- Completing the temporal picture (Q1176248) (← links)
- Axiomatizing fixpoint logics (Q1190508) (← links)
- Semantics and reasoning with free procedures (Q1193855) (← links)
- Recursive assertions are not enough - or are they? (Q1252031) (← links)
