Isabelle/UTP

A verification toolbox for Isabelle/HOL based on Unifying Theories of Programming

View project on GitHub

Publications

Below are some of the main publications associated with UTP and Isabelle/UTP.

  • Simon Foster, Kangfeng Ye, Ana Cavalcanti, and Jim Woodcock. Calculational Verification of Reactive Programs with Reactive Relations and Kleene Algebra. Accepted for RAMICS 2018. Preprint
  • Simon Foster, Ana Cavalcanti, Jim Woodcock, and Frank Zeyda. Unifying Theories of Time with Generalised Reactive Processes. Information Processing Letters, Volume 135. July 2018. Paper link. Preprint
  • Frank Zeyda, Julian Ouy, Simon Foster, and Ana Cavalcanti. Formalising Cosimulation Models. In Proc. 1st Workshop on Formal Co-Simulation of Cyber-Physical Systems, September 2017. Paper link
  • Simon Foster and Jim Woodcock. Towards Verification of Cyber-Physical Systems with UTP and Isabelle/HOL. In Concurrency, Security, and Puzzles, January 2017. Paper link
  • Simon Foster, Frank Zeyda, and Jim Woodcock. Unifying Heterogeneous State-Spaces with Lenses. Proc. 13th Intl. Colloquium on Theoretical Aspects of Computing (ICTAC 2016). Paper link
  • Frank Zeyda, Simon Foster, and Leo Freitas. An Axiomatic Value Model for Isabelle/UTP. Proc. 6th Intl. UTP Symposium, 2016. Paper link
  • Simon Foster, Frank Zeyda, and Jim Woodcock. Isabelle/UTP: A Mechanised Theory Engineering Framework. Proc. 5th Intl. UTP Symposium, 2014. Paper link
  • Marcel Oliveira, Ana Cavalcanti, and Jim Woodcock. Unifying theories in ProofPower-Z. Formal Aspects of Computing, 25(1):133–158, January 2013. Paper link
  • Frank Zeyda and Ana Cavalcanti. Mechanical reasoning about families of UTP theories. Science of Computer Programming, 77(4):444-479, April 2012. Paper link
  • Abderrahmane Feliachi, Marie-Claude Gaudel, and Burkhart Wolff. Isabelle/Circus: A Process Specification and Verification Environment. Proc. Verified Software: Theories, Tools, Experiments, 243–260, 2012. Paper link
  • Abderrahmane Feliachi, Marie-Claude Gaudel, and Burkhart Wolff. Unifying Theories in Isabelle/HOL. Proc. 3rd Intl. UTP Symposium, 2010. Paper link
  • Ana Cavalcanti and Jim Woodcock. A tutorial introduction to CSP in Unifying Theories of Programming. Proc. IFM 2004. Paper link
  • C. A. R. Hoare and He Jifeng. Unifying Theories of Programming. Prentice Hall 1998. http://unifyingtheories.org/


Isabelle/UTP is supported by projects INTO-CPS, RoboCalc, and CyPhyAssure