Soundness and Completeness of an Axiom System for Program Verification

Cited in

(only showing first 100 items - show all)

Hoare's logic and Peano's arithmetic
On strictly arithmetical completeness in logics of programs
Some natural structures which fail to possess a sound and decidable Hoare-like logic for their while-programs
Synthesis of strategies using the Hoare logic of angelic and demonic nondeterminism
Completeness of Hoare-calculi revisited
The \(\mathbf{M}\)-computations induced by accessibility relations in nonstandard models \(\mathbf{M}\) of Hoare logic
Existential fixed-point logic, universal quantifiers, and topoi
A methodology for designing proof rules for fair parallel programs
Some questions about expressiveness and relative completeness in Hoare's logic
On Fixpoint/Iteration/Variant Induction Principles for Proving Total Correctness of Programs with Denotational Semantics
Partial correctness of exits from concurrent structures
Wythoff games, continued fractions, cedar trees and Fibonacci searches
Monadic second-order incorrectness logic for GP 2
Incorrectness logic for graph programs
Hoare type theory, polymorphism and separation
Differential game logic
Eliminating the substitution axiom from UNITY logic
Program correctness and matricial iteration theories
Inductive completeness of logics of programs
On the completeness of modular proof systems
Arithmetical axiomatization of first-order temporal logic
Axiomatic semantics of projection temporal logic programs
The Birth of Model Checking
Complexity of proving program correctness
On mechanizing proofs within a complete proof system for Unity
Recursive assertions and parallel programs
Semantics, specification logic, and Hoare logic of exact real computation
One Useful Logic That Defines Its Own Truth
Proving the correctness of regular deterministic programs: A unifying survey using dynamic logic
Secure information flow by self-composition
Automated compositional proofs for real-time systems
Some general incompleteness results for partial correctness logics
Recursive assertions are not enough - or are they?
Differential dynamic logic for hybrid systems
Sound and relatively complete belief Hoare logic for statistical hypothesis testing programs
Axiomatic system for proving the properties of simple multimodule programs
Completeness for recursive procedures in separation logic
Proving correctness of constraint logic programs with dynamic scheduling
Linear dependent types in a call-by-value scenario
Semantical analysis of specification logic
Semantics and verification of monitors and systems of monitors and processes
Arithmetical completeness versus relative completeness
The Rely-Guarantee method for verifying shared variable concurrent programs
Reasoning about actions with loops via Hoare logic
Verification conditions are code
scientific article; zbMATH DE number 3688675 (Why is no real title available?)
Fifty years of Hoare's logic
An observationally complete program logic for imperative higher-order functions
Horn clause solvers for program verification
Symbioses between mathematical logic and computer science
Completeness of Hoare logic relative to the standard model
A compositional proof system for distributed programs
Using Hoare logic in a process algebra setting
A probabilistic dynamic logic
Reasoning about procedures as parameters in the language L4
A program logic for resources
VERIFYING PROBABILISTIC PROGRAMS USING A HOARE LIKE LOGIC
Verification of object-oriented programs: a transformational approach
Correctness of programs with Pascal-like procedures without global variables
Comments on a paper by Neuhold and Studer
A compositional natural semantics and Hoare logic for low-level languages
Some applications of topology to program semantics
Completeness and expressiveness of pointer program verification by separation logic
Proof methods of declarative properties of definite programs
Regular separability of well-structured transition systems
Non-standard algorithmic and dynamic logic
Indexed and fibered structures for partial and total correctness assertions
On the Completeness of Dynamic Logic
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
Verifying programs with logic and extended proof rules: deep embedding vs. shallow embedding
A genetically modified Hoare logic
Specification and verification of object-oriented programs using supertype abstraction
Ten years of Hoare's logic: A survey. II: Nondeterminism
Proving partial order properties
Average case optimality for linear problems
Current methods for proving program correctness
Completeness of Hoare logic with inputs over the standard model
scientific article; zbMATH DE number 7456057 (Why is no real title available?)
The Hoare logic of deterministic and nondeterministic monadic recursion schemes
Generating algebraic laws from imperative programs
On the mechanical derivation of loop invariants
Hoare's logic for nondeterministic regular programs: A nonstandard approach
Semantics of algorithmic languages
A Hoare-like verification system for a language with an exception handling mechanism
An axiomatic semantics for nested concurrency
A language independent proof of the soundness and completeness of generalized Hoare logic
Stratified least fixpoint logic
Axiomatizing fixpoint logics
An algebraic glimpse at bunched implications and separation logic
Completing the temporal picture
On the completeness of propositional Hoare logic
A simple relation between relational and predicate transformer semantics for nondeterministic programs
Computer Science for Continuous Data
First order Büchi automata and their application to verification of LTL specifications
Formalizing Single-Assignment Program Verification: An Adaptation-Complete Approach
A trace-based compositional proof theory for fault tolerant distributed systems
Combining Model Checking and Deduction
Hoare logic for Java in Isabelle/HOL

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)