Soundness and Completeness of an Axiom System for Program Verification

Cited In (only showing first 100 items - show all)

Inductive completeness of logics of programs
On the completeness of modular proof systems
Axiomatic semantics of projection temporal logic programs
Arithmetical axiomatization of first-order temporal logic
The Birth of Model Checking
Recursive assertions and parallel programs
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
Some general incompleteness results for partial correctness logics
Automated compositional proofs for real-time systems
Recursive assertions are not enough - or are they?
Differential dynamic logic for hybrid systems
Completeness for recursive procedures in separation logic
Semantical analysis of specification logic
The Rely-Guarantee method for verifying shared variable concurrent programs
Verification conditions are code
Horn clause solvers for program verification
An observationally complete program logic for imperative higher-order functions
A probabilistic dynamic logic
Reasoning about procedures as parameters in the language L4
VERIFYING PROBABILISTIC PROGRAMS USING A HOARE LIKE LOGIC
A program logic for resources
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
Proof methods of declarative properties of definite programs
Non-standard algorithmic and 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
Ten years of Hoare's logic: A survey. II: Nondeterminism
Proving partial order properties
Average case optimality for linear problems
Completeness of Hoare logic with inputs over the standard model
Generating algebraic laws from imperative programs
Hoare's logic for nondeterministic regular programs: A nonstandard approach
Semantics of algorithmic languages
An axiomatic semantics for nested concurrency
A language independent proof of the soundness and completeness of generalized Hoare logic
Axiomatizing fixpoint logics
On the completeness of propositional Hoare logic
Completing the temporal picture
A simple relation between relational and predicate transformer semantics for nondeterministic programs
A trace-based compositional proof theory for fault tolerant distributed systems
Hoare logic for Java in Isabelle/HOL
A mechanical analysis of program verification strategies
Proving program inclusion using Hoare's logic
Two theorems about the completeness of Hoare's logic
The axiomatic semantics of programs based on Hoare's logic
Specification and verification of concurrent systems by causality and realizability
On the notion of expressiveness and the rule of adaptation
Secure mechanical verification of mutually recursive procedures
Deductive verification of alternating systems
Weakly expressive models for Hoare logic
A complete axiomatic semantics of spawning
Floyd's principle, correctness theories and program equivalence
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
Existential fixed-point logic, universal quantifiers, and topoi
On Fixpoint/Iteration/Variant Induction Principles for Proving Total Correctness of Programs with Denotational Semantics
Some questions about expressiveness and relative completeness in Hoare's logic
Partial correctness of exits from concurrent structures
Hoare type theory, polymorphism and separation
Wythoff games, continued fractions, cedar trees and Fibonacci searches
Eliminating the substitution axiom from UNITY logic
Complexity of proving program correctness
On mechanizing proofs within a complete proof system for Unity
Semantics, specification logic, and Hoare logic of exact real computation
Sound and relatively complete belief Hoare logic for statistical hypothesis testing programs
Axiomatic system for proving the properties of simple multimodule programs
Proving correctness of constraint logic programs with dynamic scheduling
Linear dependent types in a call-by-value scenario
Semantics and verification of monitors and systems of monitors and processes
Arithmetical completeness versus relative completeness
Reasoning about actions with loops via Hoare logic
Title not available (Why is that?)
Fifty years of Hoare's logic
A compositional proof system for distributed programs
Symbioses between mathematical logic and computer science
Completeness of Hoare logic relative to the standard model
Using Hoare logic in a process algebra setting
Some applications of topology to program semantics
Regular separability of well-structured transition systems
Completeness and expressiveness of pointer program verification by separation logic
Indexed and fibered structures for partial and total correctness assertions
Verifying programs with logic and extended proof rules: deep embedding vs. shallow embedding
On the Completeness of Dynamic Logic
A genetically modified Hoare logic
Specification and verification of object-oriented programs using supertype abstraction
Current methods for proving program correctness
Title not available (Why is that?)
The Hoare logic of deterministic and nondeterministic monadic recursion schemes
On the mechanical derivation of loop invariants
An algebraic glimpse at bunched implications and separation logic
A Hoare-like verification system for a language with an exception handling mechanism
Stratified least fixpoint logic
Computer Science for Continuous Data

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)