scientific article; zbMATH DE number 605806

zbMATH Open0829.68083MaRDI QIDQ4301161FDOQ4301161

Authors: Carroll Morgan 

Publication date: 13 July 1994

Title of this publication is not available (Why is that?)

Recommendations

• Laws of data refinement
• A theoretical basis for stepwise refinement and the programming calculus
• Designware: Software development by refinement
• scientific article; zbMATH DE number 1086636
• Publication:4934624
• Formal models of stepwise refinements of programs
• scientific article; zbMATH DE number 1497802
• scientific article; zbMATH DE number 3951983
• scientific article; zbMATH DE number 177527
• scientific article; zbMATH DE number 497680

zbMATH Keywords

codeprogram refinementprogram developmentspecifications

Mathematics Subject Classification ID

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

Cited In (only showing first 100 items - show all)

• A wide-spectrum language for verification of programs on weak memory models
• Inferring Loop Invariants Using Postconditions
• Modelling and analysing neural networks using a hybrid process algebra
• Laws of mission-based programming
• Emergence and refinement
• A semantics for behavior trees using CSP with specification commands
• Structural operational semantics through context-dependent behaviour
• Compiling quantum programs
• Title not available (Why is that?)
• Soundness of data refinement for a higher-order imperative language
• Balancing expressiveness in formal approaches to concurrency
• Angelic nondeterminism in the unifying theories of programming
• Trace-based derivation of a scalable lock-free stack algorithm
• The specification logic \(\nu \)Z
• A theory of software product line refinement
• Combining Decision Procedures by (Model-)Equality Propagation
• On computing representatives
• Hoare semigroups
• Compositional refinement in agent-based security protocols
• Compositional noninterference from first principles
• Experiments in program verification using Event-B
• Combining decision procedures by (model-)equality propagation
• Refinement-oriented models of Stateflow charts
• Refining specifications to programmable logic
• Title not available (Why is that?)
• Refinement and verification in component-based model-driven design
• From control law diagrams to Ada via \textsf{Circus}
• Building program construction and verification tools from algebraic principles
• The shadow knows: refinement and security in sequential programs
• Refinement modal logic
• Provably correct derivation of algorithms using FermaT
• A UTP semantics for \textsf{Circus}
• An operational semantics for object-oriented concepts based on the class hierarchy
• On integrating confidentiality and functionality in a formal method
• Introducing extra operations in refinement
• Test-data generation for control coverage by proof
• An algebraic approach to the design of compilers for object-oriented languages
• Enabledness and termination in refinement algebra
• Graph transformations for object-oriented refinement
• Title not available (Why is that?)
• Generalised rely-guarantee concurrency: an algebraic foundation
• Patterns for refinement automation
• How to brew-up a refinement ordering
• A tactic language for refinement of state-rich concurrent specifications
• Sound refactorings
• Proof-based verification approaches for dynamic properties: application to the information system domain
• rCOS: a refinement calculus of object systems
• Testing for refinement in \textsf{Circus}
• A process algebraic framework for specification and validation of real-time systems
• CSP with Hierarchical State
• Using CafeOBJ to mechanise refactoring proofs and application
• Parallel composition and decomposition of specifications
• Specification and verification challenges for sequential object-oriented programs
• The algebra of multirelations
• Transformational programming and the derivation of algorithms
• In praise of algebra
• Unifying theories in ProofPower-Z
• Type checking \textsf{Circus} specifications
• Algebraic reasoning for probabilistic action systems and while-loops
• Ensuring liveness properties of distributed systems: open problems
• Differential Hoare Logics and Refinement Calculi for Hybrid Systems with Isabelle/HOL
• On the Purpose of Event-B Proof Obligations
• Incremental System Modelling in Event-B
• Predicate transformers and higher-order programs
• Flexible Correct-by-Construction Programming
• Stateflow diagrams in Circus
• Calculating sharp adaptation rules.
• Program derivation using the refinement calculator
• The laws of programming unify process calculi
• A theory for execution-time derivation in real-time programs
• Refinement to certify abstract interpretations: illustrated on linearization for polyhedra
• Data refinement, call by value and higher order programs
• A superposition operator for the refinement of algebraic models
• Simply-typed underdeterminism
• Fifty years of Hoare's logic
• An algebraic approach to refinement with fair choice
• Angelicism in the theory of reactive processes
• Angelic processes for CSP via the UTP
• Simulink timed models for program verification
• A generalisation of stationary distributions, and probabilistic program algebra
• Two-dimensional pattern matching against local and regular-like picture languages
• Program semantics and verification technique for AI-centred programs
• Loop invariants: analysis, classification, and examples
• Linking event-B and concurrent object-oriented programs
• A graph-based implementation for mechanized refinement calculus of OO programs
• The weakest specifunction
• A synchronous program algebra: a basis for reasoning about shared-memory and event-based concurrency
• Relation-algebraic verification of disjoint-set forests
• A formal software development approach using refinement calculus
• Information Flow Control-by-Construction for an Object-Oriented Language
• A stepwise approach to linking theories
• Schedulers and finishers: on generating and filtering the behaviours of an event structure
• Traits: correctness-by-construction for free
• Unifying theories of programming in Isabelle
• Safe Modification of Pointer Programs in Refinement Calculus
• Abstractions of non-interference security: probabilistic versus possibilistic
• Proving Quicksort Correct in Event-B
• Computer-aided development of a real-time program
• Algebra for quantitative information flow
• A refinement methodology for object-oriented programs

This page was built for publication:

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