An axiomatic basis for computer programming

Cited in

(only showing first 100 items - show all)

Bi-inductive structural semantics
The RISC ProofNavigator: a proving assistant for program verification in the classroom
Operating system verification---an overview
Mathematics for reasoning about loop functions
Verifying programs by induction on their data structure: general format and applications
Programs as proofs: A synopsis
Hoare's logic for programming languages with two data types
Ten years of Hoare's logic: A survey. II: Nondeterminism
On the suitability of trace semantics for modular proofs of communicating processes
Process logic with regular formulas
Some questions about expressiveness and relative completeness in Hoare's logic
Non-standard algorithmic and dynamic logic
The semantics of Hoare's iteration rule
A view of programming languages as symbiosis of meaning and computations
A distributed algorithm to prevent mutual drift between n logical clocks
Specification and verification of database dynamics
A categorical treatment of pre- and post-conditions
A note on undefined expression values in programming logics
A decomposition rule for the Hoare logic
Algebraic specifications of computable and semicomputable data types
Mechanical translation of set theoretic problem specifications into efficient RAM code - a case study
Arithmetical axiomatization of first-order temporal logic
Inductive assertion method for logic pograms
A proof system for distributed processes
Some general incompleteness results for partial correctness logics
A calculus of refinements for program derivations
Semantics and verification of monitors and systems of monitors and processes
A language independent proof of the soundness and completeness of generalized Hoare logic
On a conjecture of Bergstra and Tucker
Remarks on R. D. Tennent's Language design methods based on semantic principles: Algol 68, a language designed using semantic principles
A near-optimal method for reasoning about action
L.P.L. A fuzzy programming language. I: Syntactic aspects
An approach for data type specification and its use in program verification
Correctness of the compiling process based on axiomatic semantics
Proving the correctness of regular deterministic programs: A unifying survey using dynamic logic
L.P.L. - A fuzzy programming language. II: Semantic aspects
On the use of history variables
Application of modal logic to programming
Axiomatic data type specifications: A first order theory of linear lists
The formal definition of a real-time language
A proof technique for communicating sequential processes
Arithmetical completeness in first-order dynamic logic for concurrent programs
The congruence of two programming language definitions
A formal system for parallel programs in discrete time and space
Floyd's principle, correctness theories and program equivalence
Invariants in the application-oriented specification of control systems
Some natural structures which fail to possess a sound and decidable Hoare-like logic for their while-programs
Programs as partial graphs. I: Flow equivalence and correctness
Hoare's logic and Peano's arithmetic
Nonmonotonic reasoning, preferential models and cumulative logics
Domain theory in logical form
Design and verification of fault tolerant systems with CSP
A Hoare-like verification system for a language with an exception handling mechanism
Continuations in possible-world semantics
Dynamic algebras: Examples, constructions, applications
A compositional protocol verification using relativized bisimulation
Axiomatic treatment of processes with shared variables revisited
Weakest precondition semantics for time and concurrency
Order-sorted algebra. I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations
Transformation of programs for fault-tolerance
Translatability of flowcharts into while programs
Reasoning about programs
Structured implementation of symbolic execution: A first part in a program verifier
Knowledge and reasoning in program synthesis
SEMANOL (73), a metalanguage for programming the semantics of programming languages
An axiomatic proof technique for parallel programs
Loop unravelling: a practical tool in proving program correctness
Axiomatic approach to side effects and general jumps
A proof rule for multiple coroutine systems
Rules of inference for procedure calls
A family of rules for recursion removal
On the completeness of the inductive assertion method
The use of Hoare's method of program verification for the Quicksort algorithm
PASCAL in LCF: Semantics and examples of proof
On removing the machine from the language
An interative program to calculate Fibonacci numbers in O(log n) arithmetic operations
Recursive assertions are not enough - or are they?
The clean termination of Pascal programs
Program invariants as fixedpoints
Propositional dynamic logic of regular programs
A proof rule for while loop in VDM
Verifying programs in the calculus of inductive constructions
Symbolic verification method for definite iteration over data structures
Generating algebraic laws from imperative programs
Quantitative semantics, topology, and possibility measures
Deriving correctness properties of compiled code
The completeness of functional logic
Logical debugging
Normal form approach to compiler design
Axiomatic-like performance analysis (ALPA)
Process algebra with guards: Combining hoare logic with process algebra
The verification of modules
Stratified least fixpoint logic
Reasoning about dynamically evolving process structures
An overview of the Tecton proof system
Reasoning about update logic
Properties of concurrent programs
Extending Hoare logic to real-time
Top-down development of layered fault tolerant systems and its problems -- a deontic perspective
A methodology for designing proof rules for fair parallel programs

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)