CSP-CASL-Prover: A Generic Tool for Process and Data Refinement | Zendy

Liam O’Reilly | Zendy; Markus Roggenbach | Zendy; Yoshinao Isobe | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

CSP-CASL-Prover: A Generic Tool for Process and Data Refinement

Author(s) -

Liam O’Reilly,

Markus Roggenbach,

Yoshinao Isobe

Publication year - 2009

Publication title -

electronic notes in theoretical computer science

Language(s) - English

Resource type - Journals

SCImago Journal Rank - 0.242

H-Index - 60

ISSN - 1571-0661

DOI - 10.1016/j.entcs.2009.08.018

Subject(s) - hol , computer science , gas meter prover , programming language , automated theorem proving , mathematical proof , process (computing) , theoretical computer science , mathematics , geometry

The specification language Csp-Casl allows one to model processes as well as data of distributed systems within one framework. In our paper, we describe how a combination of the existing tools Hets and Csp-Prover can solve the challenges that Csp-Casl raises on integrated theorem proving for processes and data. For building this new tool, the automated generation of theorems and their proofs in Isabelle/HOL plays a fundamental role. A case study of industrial strength demonstrates that our approach scales up to complex problems.

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research