Formalization of Refinement Calculus for Reactive Systems

MaRDI QIDQ7361174FDO

Authors Viorel Preoteasa

Publication date 8 October 2014

Cites work

• A calculus of refinements for program derivations
• A completeness theorem for Kleene algebras and the algebra of regular events
• A contribution to the programming calculus
• A formulation of the simple theory of types.
• A lattice-theoretical fixpoint theorem and its applications
• A sharp proof rule for procedures in WP semantics
• A theoretical basis for stepwise refinement and the programming calculus
• Algebra of monotonic Boolean transformers
• Algebraic Notions of Termination
• Algebraic separation logic
• Algebras of modal operators and partial correctness
• An algebraic treatment of procedure refinement to support mechanical verification
• An autobiography of polyadic algebras
• An axiomatic basis for computer programming
• An efficient machine-independent procedure for garbage collection in various list structures
• Assignment and Procedure Call Proof Rules
• Automatic program verification. I: A logical basis and its implementation
• BI as an assertion language for mutable data structures
• Calculating sharp adaptation rules.
• Calculating with pointers
• Calculational derivation of pointer algorithms from tree operations
• Complementary definitions of programming language semantics
• Compositional action system refinement
• Computer Science Logic
• Concurrent Kleene Algebra
• Continuous Action System Refinement
• Countable nondeterminism and random assignment
• Data refinement of invariant based programs
• Dual choice and iteration in an abstract algebra of action
• Duality in specification languages: A lattice-theoretical approach
• Enabledness and termination in refinement algebra
• Encoding, decoding and data refinement
• FME 2003: Formal methods. International symposium of formal methods Europe, Pisa, Italy, September 8--14, 2003. Proceedings
• Frame rule for mutually recursive procedures manipulating pointers
• Guarded commands, nondeterminacy and formal derivation of programs
• Hoare logic and auxiliary variables
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Interfaces for refining recursion and procedures
• Invariant diagrams with data refinement
• Isabelle/HOL. A proof assistant for higher-order logic
• Kleene algebra with domain
• Logic for Programming, Artificial Intelligence, and Reasoning
• Modeling in Event B. System and software engineering.
• Modelling angelic and demonic nondeterminism with multirelations
• On correct refinement of programs
• On the notion of expressiveness and the rule of adaptation
• On Two Dually Nondeterministic Refinement Algebras
• Predicate transformers for recursive procedures with local variables
• Procedures, parameters, and abstraction: Separate concerns
• Program development by stepwise refinement
• Programming with Verification Conditions
• Proof of correctness of data representations
• Proving pointer programs in higher-order logic
• Proving total correctness of nondeterministic programs in infinitary logic
• Reasoning about rational agents
• Reasoning algebraically about loops
• Recent advances in parallel virtual machine and message passing interface. 5th European PVM/MPI users' group meeting. Liverpool, GB, September 7--9, 1998. Proceedings
• Refinement algebra for probabilistic programs
• Refinement Calculus
• Refinement of fair action systems
• Secure mechanical verification of mutually recursive procedures
• Soundness and Completeness of an Axiom System for Program Verification
• Specification and Development of Interactive Systems
• The B-Book
• The complementation problem for Büchi automata with applications to temporal logic
• The specification statement
• Towards a refinement algebra
• Towards pointer algebra
• Unfolding pointer algorithms
• Verification of Array, Record, and Pointer Operations in Pascal
• Verification of procedural programs
• Verification of programs that destructively manipulated data
• Winskel is (almost) right: Towards a mechanized semantics textbook

This page was built for software: Formalization of Refinement Calculus for Reactive Systems