scientific article; zbMATH DE number 605806

Publication date: 13 July 1994

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

code specifications program refinement program development

Specification and verification (program logics, model checking, etc.) (68Q60) Research exposition (monographs, survey articles) pertaining to computer science (68-02)

Related Items (only showing first 100 items - show all)

Program semantics and verification technique for AI-centred programs ⋮ Modelling and analysing neural networks using a hybrid process algebra ⋮ Algebra for Quantitative Information Flow ⋮ On computing representatives ⋮ Computer-aided development of a real-time program ⋮ Towards patterns for heaps and imperative lambdas ⋮ The Laws of Programming Unify Process Calculi ⋮ Angelic nondeterminism in the unifying theories of programming ⋮ The specification logic \(\nu \)Z ⋮ rCOS: a refinement calculus of object systems ⋮ Generalised rely-guarantee concurrency: an algebraic foundation ⋮ Specification and verification challenges for sequential object-oriented programs ⋮ Data refinement, call by value and higher order programs ⋮ Traits: correctness-by-construction for free ⋮ An algebraic approach to the design of compilers for object-oriented languages ⋮ A synchronous program algebra: a basis for reasoning about shared-memory and event-based concurrency ⋮ Unifying Theories of Programming in Isabelle ⋮ Differential Hoare Logics and Refinement Calculi for Hybrid Systems with Isabelle/HOL ⋮ Balancing expressiveness in formal approaches to concurrency ⋮ Information Flow Control-by-Construction for an Object-Oriented Language ⋮ Flexible Correct-by-Construction Programming ⋮ In praise of algebra ⋮ Unifying theories in ProofPower-Z ⋮ Modular verification for shared-variable concurrent programs ⋮ Compositional refinement in agent-based security protocols ⋮ Compositional noninterference from first principles ⋮ Experiments in program verification using Event-B ⋮ Emergence and refinement ⋮ Combining decision procedures by (model-)equality propagation ⋮ Refinement-oriented models of Stateflow charts ⋮ A Stepwise Approach to Linking Theories ⋮ Structural operational semantics through context-dependent behaviour ⋮ Safe Modification of Pointer Programs in Refinement Calculus ⋮ From control law diagrams to Ada via \textsf{Circus} ⋮ Safety-critical Java programs from \textsf{Circus} models ⋮ Linking theories in probabilistic programming ⋮ On the Purpose of Event-B Proof Obligations ⋮ The shadow knows: refinement and security in sequential programs ⋮ Enabledness and termination in refinement algebra ⋮ Refinement modal logic ⋮ Proving Quicksort Correct in Event-B ⋮ How to Brew-up a Refinement Ordering ⋮ A Graph-Based Implementation for Mechanized Refinement Calculus of OO Programs ⋮ Algebraic reasoning for probabilistic action systems and while-loops ⋮ Refinement to certify abstract interpretations: illustrated on linearization for polyhedra ⋮ Predicate transformers and higher-order programs ⋮ Hoare Semigroups ⋮ An Algebraic Approach to Refinement with Fair Choice ⋮ Linking Event-B and Concurrent Object-Oriented Programs ⋮ A Generalisation of Stationary Distributions, and Probabilistic Program Algebra ⋮ Unnamed Item ⋮ Angelic processes for CSP via the UTP ⋮ The weakest specifunction ⋮ Compiling quantum programs ⋮ A Superposition Operator for the Refinement of Algebraic Models ⋮ A process algebraic framework for specification and validation of real-time systems ⋮ A tactic language for refinement of state-rich concurrent specifications ⋮ The algebra of multirelations ⋮ Hidden-Markov program algebra with iteration ⋮ Loop invariants ⋮ Inferring Loop Invariants Using Postconditions ⋮ A semantics for behavior trees using CSP with specification commands ⋮ Ensuring liveness properties of distributed systems: open problems ⋮ Stateflow Diagrams in ⋮ Combining Decision Procedures by (Model-)Equality Propagation ⋮ Transformational Programming and the Derivation of Algorithms ⋮ Sound refactorings ⋮ A formal software development approach using refinement calculus ⋮ Abstractions of non-interference security: probabilistic versus possibilistic ⋮ A theory of software product line refinement ⋮ A wide-spectrum language for verification of programs on weak memory models ⋮ CSP with Hierarchical State ⋮ Fifty years of Hoare's logic ⋮ Schedulers and finishers: on generating and filtering the behaviours of an event structure ⋮ Two-dimensional pattern matching against local and regular-like picture languages ⋮ Patterns for Refinement Automation ⋮ A Refinement Methodology for Object-Oriented Programs ⋮ Refinement and verification in component-based model-driven design ⋮ Building program construction and verification tools from algebraic principles ⋮ An operational semantics for object-oriented concepts based on the class hierarchy ⋮ Test-data generation for control coverage by proof ⋮ On integrating confidentiality and functionality in a formal method ⋮ Provably correct derivation of algorithms using FermaT ⋮ Introducing extra operations in refinement ⋮ Angelicism in the Theory of Reactive Processes ⋮ A UTP semantics for \textsf{Circus} ⋮ Graph transformations for object-oriented refinement ⋮ Trace-based derivation of a scalable lock-free stack algorithm ⋮ Incremental System Modelling in Event-B ⋮ Simply-typed underdeterminism ⋮ Testing for refinement in \textsf{Circus} ⋮ Simulink Timed Models for Program Verification ⋮ A theory for execution-time derivation in real-time programs ⋮ Using CafeOBJ to Mechanise Refactoring Proofs and Application ⋮ Parallel composition and decomposition of specifications ⋮ Soundness of data refinement for a higher-order imperative language ⋮ Type Checking Specifications ⋮ Calculating sharp adaptation rules. ⋮ Laws of mission-based programming ⋮ Proof-based verification approaches for dynamic properties: application to the information system domain

This page was built for publication: