pefribeiro / csp-prover Goto Github PK
View Code? Open in Web Editor NEWCopy of the CSP-Prover source.
License: Other
Copy of the CSP-Prover source.
License: Other
(*-------------------------------------------* | | | << CSP-Prover >> | | | | August 2004 | | January 2005 (modified) | | February 2005 (modified) | | June 2005 (modified) | | July 2005 (modified) | | November 2005 (modified) | | April 2006 (modified) | | September 2006 (modified) | | August 2007 (modified) | | February 2008 (modified) | | July 2008 (modified) | | July 2009 (modified) | | January 2010 (modified) | | October 2010 (modified) | | April 2011 (modified) | | November 2012 (modified) | | June 2013 (modified) | | May 2016 (modified) | | | | (on Isabelle 2016) | | | | Yoshinao Isobe (AIST JAPAN) | | Markus Roggenbach (SU UK) | | | *-------------------------------------------*) 1. Introduction CSP-Prover [1,2,3,4] is an interactive theorem prover dedicated to refinement proofs within the process algebra CSP [5]. It aims specifically at proofs on infinite state systems, which may also involve infinite non-determinism. 2. Directory CSP-Prover ---+--- CSP | +--- CSP_T | +--- CSP_F | +--- FNF_F | +--- DFP | | +--- ep2 | +--- DM | +--- Test | +--- SA_Kung | +--- NBuff | +--- UCD o CSP : the reusable part of CSP-Prover o CSP_T : the instantiated part for T o CSP_F : the instantiated part for F o FNF_F : full normalising for F o DFP : (Deadlock Freedom Proof) on CSP_F, theorems given in [6] o ep2 : an example (electronic payment system) on CSP_F o DM : an example (Dining Mathematicians) on CSP_F o Test : small examples on CSP_F o SA_Kung: an example on DFP (Kung's Systolic array [3]) o NBuff : an example (Linked n one-buffers) o UCD : an example (Uniform Candy Distribution Puzzle [1]) 3. Installation This CSP-Prover needs Isabelle2016. At first, the environment-variable "CSP_PROVER_HOME" is set to the directory containing CSP, CSP_T,..., and ROOT of CSP-Prover. To make heap-files of CSP, CSP_T, CSP_F, and FNF_F once, execute the command "make_heap" in this directory (CSP_PROVER_HOME). Please read "User Guide CSP-Prover". The latest version can be downloaded from the CSP-Prover's web-site: http://staff.aist.go.jp/y-isobe/CSP-Prover/CSP-Prover.html 4. User interface To start Iasbelle/jEdit with the logic of CSP_F, execute the following command: isabelle jedit -d '$CSP_PROVER_HOME' -l CSP_F 5. Licence agreement Following the ideas of open source software, we allow anyone to use CSP-Prover without fee, under the CSP-Prover licence, which is similar to the Lesser Gnu Public License (LGPL). The details are given in http://staff.aist.go.jp/y-isobe/CSP-Prover/licence.txt You have to agree with the licence before using CSP-Prover. 6. X-symbols X-symbols are used for expressing conventional CSP operators in CSP-Prover, but X-symbols may causes some warnings on syntax. Therefore, we separated the definitions of X-symbols from the main definitions and theorems, and collected them into new files "CSP_*_xsymbols". If you do not use X-symbols of CSP-Processes, it is recommended to use the theories CSP_Main, CSP_T_Main, and CSP_F_Main, instead of CSP, CSP_T, and CSP_F. CSP_*_Main contains all the definitions and theorems of previous CSP-Prover except the definitions on X-symbols, and CSP_* imports CSP_*_Main and CSP_*_xsymbols. References [1] Y.Isobe and M.Roggenbach: CSP-Prover -- a Proof Tool for the Verification of Scalable Concurrent Systems, Journal of Computer Software, Japan Society for Software Science and Technology (JSSST), Vol.25, No.4, pp.85--92, 2008. [2] Y.Isobe and M.Roggenbach: A complete axiomatic semantics for the CSP stable-failures model, CONCUR 2006 (17th International Conference on Concurrency Theory), LNCS 4137, Springer, pp.158-172, August 2006. [3] Y.Isobe, M.Roggenbach, and S.Gruner, Extending CSP-Prover by deadlock-analysis: Towards the verification of systolic arrays, FOSE 2005 (12th Workshop on Foundation of Software Engineering), Japanese Lecture Notes Series 31, pp.257-266, Kindai-kagaku-sha, November 2005. [4] Y.Isobe and M.Roggenbach: A generic theorem prover of CSP refinement, TACAS 2005 (11th Inter\national Conference on Tools and Algorithms for the Construction and Analysis of Systems), LNCS 3440, Springer, pp.108-123, April 2005. [5] A.W.Roscoe, "The Theory and Practice of Concurrency", Prentice Hall, 1998. [6] A.W.Roscoe and N.Dathi, "The pursuit of deadlock freedom", Information and Computation, Vol.75, No.3, pp.289-327, 1987.
A declarative, efficient, and flexible JavaScript library for building user interfaces.
๐ Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. ๐๐๐
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google โค๏ธ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.