Soundness and Completeness of an Axiom System for Program Verification
From MaRDI portal
Publication:4151703
DOI10.1137/0207005zbMath0374.68009OpenAlexW2075350371WikidataQ114615493 ScholiaQ114615493MaRDI QIDQ4151703
Publication date: 1978
Published in: SIAM Journal on Computing (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1137/0207005
Related Items (only showing first 100 items - show all)
Differential Game Logic ⋮ The Hoare Logic of Deterministic and Nondeterministic Monadic Recursion Schemes ⋮ Indexed and fibered structures for partial and total correctness assertions ⋮ Complexity of proving program correctness ⋮ On mechanizing proofs within a complete proof system for Unity ⋮ On Fixpoint/Iteration/Variant Induction Principles for Proving Total Correctness of Programs with Denotational Semantics ⋮ Specification and verification of concurrent systems by causality and realizability ⋮ Sound and relatively complete belief Hoare logic for statistical hypothesis testing programs ⋮ Program correctness and matricial iteration theories ⋮ An algebraic glimpse at bunched implications and separation logic ⋮ Using Hoare Logic in a Process Algebra Setting ⋮ Proving correctness of Constraint Logic Programs with dynamic scheduling ⋮ An axiomatic semantics for nested concurrency ⋮ Non-standard algorithmic and dynamic logic ⋮ A trace-based compositional proof theory for fault tolerant distributed systems ⋮ Partial correctness of exits from concurrent structures ⋮ Stratified least fixpoint logic ⋮ Completeness for recursive procedures in separation logic ⋮ Secure mechanical verification of mutually recursive procedures ⋮ Symbioses between mathematical logic and computer science ⋮ Combining Model Checking and Deduction ⋮ Arithmetical axiomatization of first-order temporal logic ⋮ Specification and verification of object-oriented programs using supertype abstraction ⋮ Verification conditions are code ⋮ The Rely-Guarantee method for verifying shared variable concurrent programs ⋮ A compositional proof system for distributed programs ⋮ Some general incompleteness results for partial correctness logics ⋮ Semantics and verification of monitors and systems of monitors and processes ⋮ Arithmetical completeness versus relative completeness ⋮ Comments on a paper by Neuhold and Studer ⋮ A methodology for designing proof rules for fair parallel programs ⋮ A language independent proof of the soundness and completeness of generalized Hoare logic ⋮ A compositional natural semantics and Hoare logic for low-level languages ⋮ Automated compositional proofs for real-time systems ⋮ An observationally complete program logic for imperative higher-order functions ⋮ Horn Clause Solvers for Program Verification ⋮ Unnamed Item ⋮ Completeness and expressiveness of pointer program verification by separation logic ⋮ Proving the correctness of regular deterministic programs: A unifying survey using dynamic logic ⋮ Recursive assertions and parallel programs ⋮ A genetically modified Hoare logic ⋮ Completeness of Hoare logic with inputs over the standard model ⋮ The Birth of Model Checking ⋮ Hoare logic for Java in Isabelle/HOL ⋮ Unnamed Item ⋮ A simple relation between relational and predicate transformer semantics for nondeterministic programs ⋮ Completeness of Hoare Logic Relative to the Standard Model ⋮ Verification of object-oriented programs: a transformational approach ⋮ Floyd's principle, correctness theories and program equivalence ⋮ A complete logic for reasoning about programs via nonstandard model theory. II ⋮ Semantical analysis of specification logic ⋮ Synthesis of Strategies Using the Hoare Logic of Angelic and Demonic Nondeterminism ⋮ On termination problems for finitely interpreted ALGOL-like programs ⋮ Programs and program verifications in a general setting ⋮ The \(\mathbf{M}\)-computations induced by accessibility relations in nonstandard models \(\mathbf{M}\) of Hoare logic ⋮ Reasoning about actions with loops via Hoare logic ⋮ Linear dependent types in a call-by-value scenario ⋮ Some natural structures which fail to possess a sound and decidable Hoare-like logic for their while-programs ⋮ On the completeness of modular proof systems ⋮ Unnamed Item ⋮ Hoare's logic and Peano's arithmetic ⋮ A mechanical analysis of program verification strategies ⋮ A Hoare-like verification system for a language with an exception handling mechanism ⋮ Completing the temporal picture ⋮ Hoare type theory, polymorphism and separation ⋮ Deductive verification of alternating systems ⋮ A program logic for resources ⋮ Axiomatizing fixpoint logics ⋮ Programming with Infinitesimals: A While-Language for Hybrid System Modeling ⋮ Semantics and reasoning with free procedures ⋮ Mechanical verification of mutually recursive procedures ⋮ Axiomatic system for proving the properties of simple multimodule programs ⋮ Proof methods of declarative properties of definite programs ⋮ VERIFYING PROBABILISTIC PROGRAMS USING A HOARE LIKE LOGIC ⋮ Existential Fixed-Point Logic, Universal Quantifiers, and Topoi ⋮ Some applications of topology to program semantics ⋮ One Useful Logic That Defines Its Own Truth ⋮ On strictly arithmetical completeness in logics of programs ⋮ Reasoning about procedures as parameters in the language L4 ⋮ Fifty years of Hoare's logic ⋮ Axiomatic semantics of projection temporal logic programs ⋮ Formalizing Single-Assignment Program Verification: An Adaptation-Complete Approach ⋮ Recursive assertions are not enough - or are they? ⋮ On the Completeness of Dynamic Logic ⋮ Inductive Completeness of Logics of Programs ⋮ Eliminating the substitution axiom from UNITY logic ⋮ Semantics of algorithmic languages ⋮ Wythoff games, continued fractions, cedar trees and Fibonacci searches ⋮ Current methods for proving program correctness ⋮ Hoare's logic for nondeterministic regular programs: A nonstandard approach ⋮ Secure information flow by self-composition ⋮ An adaptation-complete proof system for local reasoning about cloud storage systems ⋮ Equational theories for automata ⋮ Generating algebraic laws from imperative programs ⋮ Differential dynamic logic for hybrid systems ⋮ Completeness of Hoare-calculi revisited ⋮ On the notion of expressiveness and the rule of adaptation ⋮ Proving program inclusion using Hoare's logic ⋮ Correctness of programs with Pascal-like procedures without global variables ⋮ A probabilistic dynamic logic
This page was built for publication: Soundness and Completeness of an Axiom System for Program Verification
