The specification statement

Cited in

(41)

A calculus of refinements for program derivations
Data refinement of predicate transformers
Combining angels, demons and miracles in program specifications
On the lattice of specifications: Applications to a specification methodology
Joining specification statements
The lattice of data refinement
A relation algebraic model of robust correctness
Procedures and atomicity refinement
Coordinating action systems
Designing a semantic model for a wide-spectrum language with concurrency
Action systems, unbounded nondeterminism, and infinite traces
Exits in the refinement calculus
Base-type languages: Program design by upper semantic approximation
Specification and refinement of networks of asynchronously communicating agents using the assumption/commitment paradigm
Superposition refinement of reactive systems
In praise of algebra
Using schedulers to test probabilistic distributed systems
A unification of probabilistic choice within a design-based model of reversible computation
A wide-spectrum language for verification of programs on weak memory models
An adaptation-complete proof system for local reasoning about cloud storage systems
Loop verification with invariants and contracts
Abstract implementation of algebraic specifications in a temporal logic language
A synchronous program algebra: a basis for reasoning about shared-memory and event-based concurrency
A theory for execution-time derivation in real-time programs
HOL-Boogie -- an interactive prover-backend for the verifying C compiler
Set-theoretic models of computations
On rely-guarantee reasoning
Developments in concurrent Kleene algebra
Generalised rely-guarantee concurrency: an algebraic foundation
HOL-Boogie — An Interactive Prover for the Boogie Program-Verifier
Mechanised support for sound refinement tactics
Footprints in Local Reasoning
A formal software development approach using refinement calculus
Preface
Specifying and reasoning about shared-variable concurrency
Predicate transformers and higher-order programs
A single complete rule for data refinement
Formalization of Refinement Calculus for Reactive Systems
Algebra of Monotonic Boolean Transformers
The behavioural semantics of Event-B refinement
An analysis of refinement in an abortive paradigm

This page was built for publication: The specification statement

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