University | Computer Science  

      » Circus Family » Tools » CRefine 

Refinement Calculus Tools

CRefine is a tool that can be used throughout the refinement of concurrent systems in a calculational approach. It automates the application of the Circus refinement calculus by applying various well-proved refinement laws, sometimes with the discharge of proof obligations, most of which are automatically proved. CRefine also automates the process of defining and applying refinement tactics in a program development as a single transformation rule. The tactics are formalized in ArcAngelC, a refinement tactic language for Circus programs. Finally, CRefine can also generate Java object-code (using JCircus, a code generator from Circus to Java) that implements the behaviour of the input specification in Circus.



  • M. S. Conserva Filho, M. V. M. Oliveira. Implementing Tactics of Refinement in CRefine.. In: Software Engineering and Formal Methods, 2012, Thessaloniki. LNCS. Heidelberg: Springer, 2012. v. 7504. p. 342-351.[Bib | PDF]
  • S. L. Barrocas, M. V. M. Oliveira. JCircus 2.0: an extension of an automatic translator from Circus to Java.. In: Communicating Process Architectures 2012, 2012, Dundee. Communicating Processes Architectures - 34th WoTUG Technical Meeting. England: Open Channel Publishing, 2012. p. 15-36.[Bib | PDF]
  • M. S. Conserva Filho, M. V. M. Oliveira. Extending CRefine to Support Tactics of Refinement.. In: 14 Brazilian Symposium on Formal Methods – SBMF 2011, São Paulo. [Bib | PDF]
  • M. V. M. Oliveira, A. C. Gurgel, and C. G. de Castro. CRefine: Support for the Circus Refinement Calculus. In Antonio Cerone and Stefan Gruner, editors, 6th IEEE International Conferences on Software Engineering and Formal Methods, pages 281-290. IEEE Computer Society Press, 2008. © IEEE Computer Society Press.[Bib | PDF]




       Department of Computer Science

       University of York, Deramore Lane, York, YO10 5GH, UK

       Tel: 01904 325500 | Fax:01904 325599                                                                                                                     Last updated on 27 April 2011