An axiomatic basis for computer programming

Cited in

(only showing first 100 items - show all)

The Hoare logic of concurrent programs
On invariant checking
scientific article; zbMATH DE number 2156365 (Why is no real title available?)
Highly automated formal proofs over memory usage of assembly code
Loop summarization using state and transition invariants
Unified reasoning about robustness properties of symbolic-heap separation logic
Mechanical translation of set theoretic problem specifications into efficient RAM code - a case study
A learning-based approach to synthesizing invariants for incomplete verification engines
Mac Lane's comparison theorem for the Kleisli construction formalized in Coq
A deductive clustering approach
A contraction-free and cut-free sequent calculus for propositional dynamic logic
Reasoning about iteration and recursion uniformly based on big-step semantics
A distributed algorithm to prevent mutual drift between n logical clocks
Steps in modular specifications for concurrent modules (invited tutorial paper)
PASCAL in LCF: Semantics and examples of proof
A compositional modelling and verification framework for stochastic hybrid systems
On the completeness of modular proof systems
Schematic program proofs with abstract execution. Theory and applications
scientific article; zbMATH DE number 7649967 (Why is no real title available?)
A unified approach of program verification
Logical foundations for programming semantics
Loop invariants in floating point algorithms
Constructive game logic
Expressive completeness of separation logic in block-based cloud storage systems
Bi-inductive structural semantics
Arithmetical axiomatization of first-order temporal logic
An Isbell duality theorem for type refinement systems
Invariants for parameterised Boolean equation systems
Formal design and implementation of constraints in software components
Axiomatic semantics of projection temporal logic programs
Formal validation of data-parallel programs: a two-component assertional proof system for a simple language
TERMINATION ANALYSIS OF LINEAR LOOPS
-adhesive transformation systems with nested application conditions. Part 1: parallelism, concurrency and amalgamation
Preserving Contract Satisfiability Under Non-monotonic Composition
Unifying Operational Weak Memory Verification: An Axiomatic Approach
Time-bounded termination analysis for probabilistic programs with delays
Ghost signals: verifying termination of busy waiting
Integrating Owicki-Gries for C11-style memory models into Isabelle/HOL
Indexed and fibred structures for Hoare logic
Deaccumulation techniques for improving provability
Action systems in incremental and aspect-oriented modeling
Fair termination revisited - with delay
Specification and verification of database dynamics
A note on undefined expression values in programming logics
Meanings of model checking
A categorical treatment of pre- and post-conditions
The clean termination of Pascal programs
Application of modal logic to programming
Program invariants as fixedpoints
A decomposition rule for the Hoare logic
Distances between formal theories
Calculating sharp adaptation rules.
Extended Static Checking by Calculation Using the Pointfree Transform
An algebraic approach to simulation and verification for cyber-physical systems with shared-variable concurrency
The congruence of two programming language definitions
System ST toward a type system for extraction and proofs of programs
Matrix Code
A relation-algebraic approach to the ``Hoare logic of functional dependencies
The laws of programming unify process calculi
An evaluation of interaction paradigms for active objects
The refinement calculus of reactive systems
A safe variant of the unsafe integer arithmetic of Java™
Process synchronization in high-level languages
An iterative modular multiplication algorithm
Semantics, specification logic, and Hoare logic of exact real computation
Dual choice and iteration in an abstract algebra of action
A generic complete dynamic logic for reasoning about purity and effects
Partial correctness of a Fibonacci algorithm
One Useful Logic That Defines Its Own Truth
Proving the correctness of regular deterministic programs: A unifying survey using dynamic logic
Extending rely-guarantee thinking to handle real-time scheduling
The verification of modules
Inference rules for programming languages with side effects in expressions
A formalization of programs in first-order logic with a discrete linear order
Verification of a class of link-level protocols
An abstract interpretation-based model for safety semantics
Two-level realization of logical formulas for deductive program synthesis
(Co)inductive proof systems for compositional proofs in reachability logic
A proof rule for while loop in VDM
Limits and difficulties in the design of under-approximation abstract domains
Weakest precondition reasoning for expected run-times of probabilistic programs
Automated Algebraic Reasoning for Collections and Local Variables with Lenses
Verifying the Correctness of Disjoint-Set Forests with Kleene Relation Algebras
Axiomatic approach to side effects and general jumps
From proposition to program. Embedding the refinement calculus in Coq
rCOS: defining meanings of component-based software architectures
Programming and reasoning about actors that share state
Secure information flow by self-composition
Modular verification of procedure equivalence in the presence of memory allocation
A proof system for distributed processes
Preserving consistency in geometric modeling with graph transformations
Some general incompleteness results for partial correctness logics
Analysis and Transformation of Constrained Horn Clauses for Program Verification
Abstract program slicing: an abstract interpretation-based approach to program slicing
Formal modelling, analysis and verification of hybrid systems
Well-behaved (co)algebraic semantics of regular expressions in Dafny
Probabilistic datatypes
Towards leveraging domain knowledge in state-based formal methods
Alternating states for dual nondeterminism in imperative programming
A complete semantics of \(\mathbb{K}\) and its translation to Isabelle

This page was built for publication: An axiomatic basis for computer programming

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