Refinement Calculus of Reactive Systems

RCRS (the Refinement Calculus of Reactive Systems) is a compositional reasoning framework:

Download

Latest version distributed under the MIT license.

The RCRS Toolset

The RCRS Toolset currently includes:



Installation

To install, download the distribution (zip file) and read the README file. The simulink2isabelle Translator is written in Python and requires the third-party component pyparsing.

Awards

TACAS 2018 Distinguished Artifact Award TACAS 2018 Artifact Evaluation Badge

Papers

  1. V. Preoteasa, I. Dragomir, S.Tripakis. Mechanically Proving Determinacy of Hierarchical Block Diagram Translations. VMCAI 2019. Extended version in arXiv 2018.
    [paper]  [technical report]
  2. I. Dragomir, V. Preoteasa, S.Tripakis. The Refinement Calculus of Reactive Systems Toolset. TACAS 2018. Extended version in arXiv 2018. Distinguished Artifact Award.
    [paper]  [technical report] 
  3. V. Preoteasa, I. Dragomir, S.Tripakis. The Refinement Calculus of Reactive Systems. arXiv 2017.
    [technical report] 
  4. V. Preoteasa, I. Dragomir, S.Tripakis. Type Inference of Simulink Hierarchical Block Diagrams in Isabelle. FORTE 2017.
    [paper]  [technical report]  [slides]
  5. V. Preoteasa, S.Tripakis. Towards Compositional Feedback in Non-Deterministic and Non-Input-Receptive Systems. LICS 2016.
    [paper]  [technical report]
  6. S.Tripakis. Compositionality in the Science of System Design. Proceedings of the IEEE 2016.
    [paper]
  7. I. Dragomir, V. Preoteasa, S.Tripakis. Compositional Semantics and Analysis of Hierarchical Block Diagrams. SPIN 2016.
    [paper]  [technical report]  [slides]
  8. V. Preoteasa, S.Tripakis. Refinement Calculus of Reactive Systems. EMSOFT 2014.
    [paper]  [technical report]
  9. V. Preoteasa. Formalization of Refinement Calculus for Reactive Systems. Archive of Formal Proofs 2014.
    [paper]  [source]
  10. S. Tripakis, C. Stergiou, M. Broy, E. A. Lee. Error-Completion in Interface Theories. SPIN 2013.
    [paper]
  11. S. Tripakis, B. Lickly, T. A. Henzinger, E. A. Lee. A Theory of Synchronous Relational Interfaces. ACM TOPLAS 2011.
    [paper]
  12. S. Tripakis, B. Lickly, T. A. Henzinger, E. A. Lee. On Relational Interfaces. EMSOFT 2009.
    [paper]

People


Sponsors

The RCRS project has been sponsored by:
For any enquiries, you can contact us by email.