Refinement Calculus of Reactive Systems

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


News


TACAS 2018 Distinguished Artifact Award TACAS 2018 Artifact Evaluation Badge

The RCRS Toolset: Implementation and Download


Our group is developing and distributing (under the MIT license) the RCRS Toolset. The distribution currently includes:


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.

Papers


  1. 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] 
  2. V. Preoteasa, I. Dragomir, S.Tripakis. Mechanically Proving Determinacy of Hierarchical Block Diagram Translations. arXiv 2018.
    [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.