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
Combining angels, demons and miracles in program specifications
On the lattice of specifications: Applications to a specification methodology
HOL-Boogie — An Interactive Prover for the Boogie Program-Verifier
Joining specification statements
Coordinating action systems
Mechanised support for sound refinement tactics
Developments in concurrent Kleene algebra
Using schedulers to test probabilistic distributed systems
A relation algebraic model of robust correctness
Base-type languages: Program design by upper semantic approximation
A calculus of refinements for program derivations
Preface
A synchronous program algebra: a basis for reasoning about shared-memory and event-based concurrency
Footprints in Local Reasoning
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
Specification and refinement of networks of asynchronously communicating agents using the assumption/commitment paradigm
Set-theoretic models of computations
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)