Soundness and Completeness of an Axiom System for Program Verification

Cited in

(only showing first 100 items - show all)

Differential dynamic logic for hybrid systems
Ten years of Hoare's logic: A survey. II: Nondeterminism
Some questions about expressiveness and relative completeness in Hoare's logic
An axiomatic semantics for nested concurrency
Non-standard algorithmic and dynamic logic
Partial correctness of exits from concurrent structures
Arithmetical axiomatization of first-order temporal logic
Some general incompleteness results for partial correctness logics
Semantics and verification of monitors and systems of monitors and processes
Arithmetical completeness versus relative completeness
A language independent proof of the soundness and completeness of generalized Hoare logic
Proving the correctness of regular deterministic programs: A unifying survey using dynamic logic
Recursive assertions and parallel programs
A simple relation between relational and predicate transformer semantics for nondeterministic programs
Floyd's principle, correctness theories and program equivalence
A complete logic for reasoning about programs via nonstandard model theory. II
On termination problems for finitely interpreted ALGOL-like programs
Programs and program verifications in a general setting
Some natural structures which fail to possess a sound and decidable Hoare-like logic for their while-programs
Hoare's logic and Peano's arithmetic
A Hoare-like verification system for a language with an exception handling mechanism
Completing the temporal picture
Axiomatizing fixpoint logics
Semantics and reasoning with free procedures
Recursive assertions are not enough - or are they?
Generating algebraic laws from imperative programs
Proving partial order properties
On the mechanical derivation of loop invariants
A trace-based compositional proof theory for fault tolerant distributed systems
Stratified least fixpoint logic
The Rely-Guarantee method for verifying shared variable concurrent programs
A methodology for designing proof rules for fair parallel programs
On the completeness of propositional Hoare logic
The \(\mathbf{M}\)-computations induced by accessibility relations in nonstandard models \(\mathbf{M}\) of Hoare logic
Reasoning about actions with loops via Hoare logic
Hoare's logic for nondeterministic regular programs: A nonstandard approach
Completeness of Hoare-calculi revisited
On the notion of expressiveness and the rule of adaptation
Secure mechanical verification of mutually recursive procedures
Specification and verification of object-oriented programs using supertype abstraction
An adaptation-complete proof system for local reasoning about cloud storage systems
Equational theories for automata
Monadic second-order incorrectness logic for GP 2
Incorrectness logic for graph programs
On strictly arithmetical completeness in logics of programs
Fifty years of Hoare's logic
Completeness and expressiveness of pointer program verification by separation logic
A genetically modified Hoare logic
Linear dependent types in a call-by-value scenario
A program logic for resources
Symbioses between mathematical logic and computer science
Completeness for recursive procedures in separation logic
Formalizing Single-Assignment Program Verification: An Adaptation-Complete Approach
Inductive completeness of logics of programs
Horn clause solvers for program verification
Completeness of Hoare logic relative to the standard model
Synthesis of strategies using the Hoare logic of angelic and demonic nondeterminism
Programming with Infinitesimals: A While-Language for Hybrid System Modeling
VERIFYING PROBABILISTIC PROGRAMS USING A HOARE LIKE LOGIC
Axiomatic semantics of projection temporal logic programs
Secure information flow by self-composition
Combining Model Checking and Deduction
Some applications of topology to program semantics
The Birth of Model Checking
Hoare type theory, polymorphism and separation
Existential fixed-point logic, universal quantifiers, and topoi
One Useful Logic That Defines Its Own Truth
On the Completeness of Dynamic Logic
Axiomatic system for proving the properties of simple multimodule programs
An observationally complete program logic for imperative higher-order functions
scientific article; zbMATH DE number 3688675 (Why is no real title available?)
Current methods for proving program correctness
Hoare logic for Java in Isabelle/HOL
Verification of object-oriented programs: a transformational approach
A compositional proof system for distributed programs
Mechanical verification of mutually recursive procedures
Regular separability of well-structured transition systems
scientific article; zbMATH DE number 7456057 (Why is no real title available?)
Proving correctness of constraint logic programs with dynamic scheduling
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
Using Hoare logic in a process algebra setting
Differential game logic
The Hoare logic of deterministic and nondeterministic monadic recursion schemes
Reasoning about procedures as parameters in the language L4
Indexed and fibered structures for partial and total correctness assertions
Comments on a paper by Neuhold and Studer
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
Computer Science for Continuous Data
Semantics, specification logic, and Hoare logic of exact real computation
Verifying programs with logic and extended proof rules: deep embedding vs. shallow embedding
First order Büchi automata and their application to verification of LTL specifications
Hoare-style logic for unstructured programs
Proof methods of declarative properties of definite programs
Alignment complete relational Hoare logics for some and all
Quantum weakest preconditions for reasoning about expected runtimes of quantum programs

This page was built for publication: Soundness and Completeness of an Axiom System for Program Verification

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4151703)