An axiomatic basis for computer programming
From MaRDI portal
Publication:5569944
DOI10.1145/363235.363259zbMath0179.23105OpenAlexW2987907651WikidataQ55867309 ScholiaQ55867309MaRDI QIDQ5569944
Publication date: 1969
Published in: Communications of the ACM (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/363235.363259
Related Items (more than 100 items found here)
Preserving Contract Satisfiability Under Non-monotonic Composition ⋮ The Hoare Logic of Deterministic and Nondeterministic Monadic Recursion Schemes ⋮ Abstract Program Slicing ⋮ Program Verification with Separation Logic ⋮ Formal Derivation of a High-Trustworthy Generic Algorithmic Program for Solving a Class of Path Problems ⋮ Natural Quantum Operational Semantics with Predicates ⋮ On Fixpoint/Iteration/Variant Induction Principles for Proving Total Correctness of Programs with Denotational Semantics ⋮ Automated Algebraic Reasoning for Collections and Local Variables with Lenses ⋮ Verifying the Correctness of Disjoint-Set Forests with Kleene Relation Algebras ⋮ Abstract interpretation, Hoare logic, and incorrectness logic for quantum programs ⋮ Algebra-Based Loop Analysis ⋮ Logic for reasoning about bugs in loops over data sequences (IFIL) ⋮ Analysis and Transformation of Constrained Horn Clauses for Program Verification ⋮ Programming language semantics: It’s easy as 1,2,3 ⋮ Stateful Behavioral Types for Active Objects ⋮ Adversarial logic ⋮ A matching logic foundation for Alk ⋮ From interface automata to hypercontracts ⋮ Embedded domain specific verifiers ⋮ Limits and difficulties in the design of under-approximation abstract domains ⋮ Semantic embedding for quantum algorithms ⋮ Formal verification of termination criteria for first-order recursive functions ⋮ Proofs as stateful programs: A first-order logic with abstract Hoare triples, and an interpretation into an imperative language ⋮ A dynamic logic with branching modalities ⋮ Symbolic encoding of LL(1) parsing and its applications ⋮ Sound and relatively complete belief Hoare logic for statistical hypothesis testing programs ⋮ A verified VCGen based on dynamic logic: an exercise in meta-verification with Why3 ⋮ Solving invariant generation for unsolvable loops ⋮ Local completeness logic on Kleene algebra with tests ⋮ A note on the for statement ⋮ Why3-do: the way of harmonious distributed system proofs ⋮ Unnamed Item ⋮ Liminf progress measures ⋮ Toward a theory of program repair ⋮ Symbolic computation in automated program reasoning ⋮ Reasoning about promises in weak memory models with event structures ⋮ A fine-grained semantics for arrays and pointers under weak memory models ⋮ RHLE: modular deductive verification of relational \(\forall \exists\) properties ⋮ From Gödel's incompleteness theorem to the completeness of bot beliefs (extended abstract) ⋮ An algebraic glimpse at bunched implications and separation logic ⋮ DISTANCES BETWEEN FORMAL THEORIES ⋮ Steps in modular specifications for concurrent modules (invited tutorial paper) ⋮ VPHL: a verified partial-correctness logic for probabilistic programs ⋮ Unnamed Item ⋮ Action systems in incremental and aspect-oriented modeling ⋮ Matching µ-logic: Foundation of K framework ⋮ Highly Automated Formal Proofs over Memory Usage of Assembly Code ⋮ Using Hoare Logic in a Process Algebra Setting ⋮ All-Path Reachability Logic ⋮ -adhesive transformation systems with nested application conditions. Part 1: parallelism, concurrency and amalgamation ⋮ Verification of Concurrent Systems with VerCors ⋮ Loop invariants ⋮ Transforming Programs into Recursive Functions ⋮ KeY: A Formal Method for Object-Oriented Systems ⋮ Meanings of Model Checking ⋮ Extended Static Checking by Calculation Using the Pointfree Transform ⋮ An introduction to compositional methods for concurrency and their application to real-time. ⋮ Models and logics for true concurrency. ⋮ Logical models of discrete even systems: a comparative exposition ⋮ Symbolic Verification Method for Definite Iterations over Tuples of Altered Data Structures and Its Application to Pointer Programs ⋮ An Inference-Rule-Based Decision Procedure for Verification of Heap-Manipulating Programs with Mutable Data and Cyclic Data Structures ⋮ DEL-sequents for progression ⋮ DEL-sequents for progression ⋮ Unnamed Item ⋮ A logical analysis of aliasing in imperative higher-order functions ⋮ Schema Mappings: A Case of Logical Dynamics in Database Theory ⋮ Dynamic Epistemic Logics ⋮ Notes on Recent Achievements in Proving Stability using KeYmaeraX ⋮ Reasoning about Separation Using Abstraction and Reification ⋮ Extending separation logic with fixpoints and postponed substitution ⋮ A formalization of programs in first-order logic with a discrete linear order ⋮ Completeness for recursive procedures in separation logic ⋮ The reflective Milawa theorem prover is sound (down to the machine code that runs it) ⋮ Ghost signals: verifying termination of busy waiting ⋮ Integrating Owicki-Gries for C11-style memory models into Isabelle/HOL ⋮ Analysis of linear definite iterative loops ⋮ Pair algebras and Galois connections. ⋮ Certifying low-level programs with hardware interrupts and preemptive threads ⋮ Developments in concurrent Kleene algebra ⋮ Formalization and implementation of modern SAT solvers ⋮ Proof optimization for partial redundancy elimination ⋮ Why does Astrée scale up? ⋮ A method for computing the number of iterations in data dependent loops ⋮ Verification conditions are code ⋮ Generalised rely-guarantee concurrency: an algebraic foundation ⋮ Online belief tracking using regression for contingent planning ⋮ Deciding Boolean algebra with Presburger arithmetic ⋮ An integrated approach to high integrity software verification ⋮ Semantics of higher-order quantum computation via geometry of interaction ⋮ Synthesis of large dynamic concurrent programs from dynamic specifications ⋮ A verifiable low-level concurrent programming model based on colored Petri nets ⋮ Recent advances in program verification through computer algebra ⋮ Certifying assembly programs with trails ⋮ Formal correctness proofs of a nondeterministic program ⋮ Applicability conditions for plans with loops: computability results and algorithms ⋮ The Schorr-Waite graph marking algorithm ⋮ Towards ``dynamic domains: totally continuous cocomplete \(\mathcal Q\)-categories ⋮ A compositional natural semantics and Hoare logic for low-level languages ⋮ Mechanical inference of invariants for FOR-loops ⋮ Reflexive transitive invariant relations: A basis for computing loop functions
This page was built for publication: An axiomatic basis for computer programming
