Refinement Calculus

DOI10.1007/978-1-4612-1674-2zbMath0949.68094OpenAlexW4253748132MaRDI QIDQ4396958

Publication date: 21 June 1998

Full work available at URL: https://doi.org/10.1007/978-1-4612-1674-2

refinement calculus semantics program construction

Introductory exposition (textbooks, tutorial papers, etc.) pertaining to computer science (68-01) Introductory exposition (textbooks, tutorial papers, etc.) pertaining to mathematical logic and foundations (03-01) Semantics in the theory of computing (68Q55) General topics in the theory of software (68N01)

Related Items

Concurrent Dynamic Algebra, Taming Multirelations, Algebra for Quantitative Information Flow, Computer-aided development of a real-time program, Building Specifications in the Event-B Institution, Automated Algebraic Reasoning for Collections and Local Variables with Lenses, Verifying the Correctness of Disjoint-Set Forests with Kleene Relation Algebras, Differential Hoare Logics and Refinement Calculi for Hybrid Systems with Isabelle/HOL, Information Flow Control-by-Construction for an Object-Oriented Language, Flexible Correct-by-Construction Programming, Verification-Led Smart Contracts, An Algebraic Approach to Refinement with Fair Choice, Unifying Semantics for Concurrent Programming, The algebra of multirelations, Hidden-Markov program algebra with iteration, Combining Top-Down and Bottom-Up Techniques in Program Derivation, Verified Compilation and the B Method: A Proposal and a First Appraisal, Multiple Viewpoint Contract-Based Specification and Design, Effect polymorphism in higher-order logic (proof pearl), Efficient verified (UN)SAT certificate checking, A Multi-level Refinement Approach for Structural Synthesis of Optimal Probabilistic Models, Modelling and analysing neural networks using a hybrid process algebra, Specification and refinement of mobile systems in MTLA and mobile UML, Kleisli, Parikh and Peleg compositions and liftings for multirelations, Evolution of rule-based programs, Automating Induction with an SMT Solver, Predicate transformer semantics for hybrid systems. Verification components for Isabelle/HOL, Developments in concurrent Kleene algebra, Assumption propagation through annotated programs, Towards patterns for heaps and imperative lambdas, Mechanical synthesis of sorting algorithms for binary trees by logic and combinatorial techniques, The Laws of Programming Unify Process Calculi, Deriving Real-Time Action Systems Controllers from Multiscale System Specifications, Integrating formal specifications into applications: the ProB Java API, An analysis of refinement in an abortive paradigm, The specification logic \(\nu \)Z, Towards an Algebra for Real-Time Programs, rCOS: a refinement calculus of object systems, Verification conditions are code, Generalised rely-guarantee concurrency: an algebraic foundation, Traits: correctness-by-construction for free, A verified ODE solver and the Lorenz attractor, Laws of Programming for References, Imperative abstractions for functional actions, Splitting atoms safely, Exploring an Interface Model for CKA, A Relation-Algebraic Approach to Multirelations and Predicate Transformers, A Program Construction and Verification Tool for Separation Logic, 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, The refinement calculus of reactive systems, Designing a semantic model for a wide-spectrum language with concurrency, Unifying Theories of Programming in Isabelle, Knowledge and Games in Modal Semirings, Automatic refinement to efficient data structures: a comparison of two approaches, Consistency-preserving refactoring of refinement structures in Event-B models, Investigating the limits of rely/guarantee relations based on a concurrent garbage collector example, Balancing expressiveness in formal approaches to concurrency, Multirelations with infinite computations, Program algebra for quantitative information flow, Relating computer systems to sequence diagrams: the impact of underspecification and inherent nondeterminism, Integrating stochastic reasoning into Event-B development, Invariant diagrams with data refinement, Compositional noninterference from first principles, Connectors as designs: modeling, refinement and test case generation, Safe Modification of Pointer Programs in Refinement Calculus, A programming model for BSP with partitioned synchronisation, Synthesis of Strategies Using the Hoare Logic of Angelic and Demonic Nondeterminism, On hierarchically developing reactive systems, On the Purpose of Event-B Proof Obligations, A Practical Single Refinement Method for B, Enabledness and termination in refinement algebra, Formalizing network flow algorithms: a refinement approach in Isabelle/HOL, Formal communication elimination and sequentialization equivalence proofs for distributed system models, Reasoning about orchestrations of web services using partial correctness, Using probabilistic Kleene algebra pKA for protocol verification, Data Refinement of Invariant Based Programs, Algebraic reasoning for probabilistic action systems and while-loops, Modelling higher-order dual nondeterminacy, Bridging arrays and ADTs in recursive proofs, Refinement to imperative HOL, An axiomatic approach to existence and liveness for differential equations, Conditions of contracts for separating responsibilities in heterogeneous systems, Formal verification of an executable LTL model checker with partial order reduction, An algebraic approach to multirelations and their properties, Angelic processes for CSP via the UTP, Dual choice and iteration in an abstract algebra of action, The weakest specifunction, Unifying theories of reactive design contracts, Algebraic separation logic, Normal forms in total correctness for while programs and action systems, Alternating states for dual nondeterminism in imperative programming, Refinement algebra for probabilistic programs, Abstractions of non-interference security: probabilistic versus possibilistic, A wide-spectrum language for verification of programs on weak memory models, Patterns for Refinement Automation, A Refinement Methodology for Object-Oriented Programs, Frame rule for mutually recursive procedures manipulating pointers, Refinement and verification in component-based model-driven design, Continuous Functions on Final Coalgebras, The behavioural semantics of Event-B refinement, Derivation of concurrent programs by stepwise scheduling of Event-B models, Automated verification of reactive and concurrent programs by calculation, Angelicism in the Theory of Reactive Processes, Structured calculational proof, Full Abstraction at Package Boundaries of Object-Oriented Languages, Algebra of Monotonic Boolean Transformers, Formalizing the Edmonds-Karp Algorithm, On the design of correct and optimal dynamical systems and games, Don't Care Non-determinism in Logic Program Refinement, Generic Models of the Laws of Programming, Programming interfaces and basic topology, A theory for execution-time derivation in real-time programs, Hybrid action systems, Contracts, games, and refinement., On the relation between concurrent separation logic and concurrent Kleene algebra, A formal model of real-time program compilation, Soundness of data refinement for a higher-order imperative language, Annotation inference for modular checkers, Calculating sharp adaptation rules., Kleene under a modal demonic star