The specification statement

Cited In (39)

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

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)