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. In other word, it verifies Circus specifications purely by applying various well-proved refinement laws. CRefine is implemented in Java.



  • 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