|
|
|
@ -36,7 +36,6 @@ For source code distributions: |
|
|
|
|
|
|
|
If you have problems check the manual, especially the section "Common Problems And Questions". |
|
|
|
|
|
|
|
|
|
|
|
------------- |
|
|
|
DOCUMENTATION |
|
|
|
------------- |
|
|
|
@ -54,7 +53,6 @@ For other PRISM-related information, see the website: |
|
|
|
|
|
|
|
http://www.prismmodelchecker.org/ |
|
|
|
|
|
|
|
|
|
|
|
--------- |
|
|
|
LICENSING |
|
|
|
--------- |
|
|
|
@ -71,42 +69,36 @@ library, see: |
|
|
|
|
|
|
|
http://vlsi.colorado.edu/~fabio/CUDD/ |
|
|
|
|
|
|
|
|
|
|
|
---------------- |
|
|
|
ACKNOWLEDGEMENTS |
|
|
|
---------------- |
|
|
|
|
|
|
|
Currently, development work on PRISM is primarily carried out in the |
|
|
|
Department of Computer Science at the University of Oxford. Previously, PRISM |
|
|
|
was based in the School of Computer Science at the University of Birmingham. |
|
|
|
PRISM was created and is still actively maintained by: |
|
|
|
|
|
|
|
The core team working on PRISM currently comprises: |
|
|
|
* Dave Parker (University of Birmingham) |
|
|
|
* Gethin Norman (University of Glasgow) |
|
|
|
* Marta Kwiatkowska (University of Oxford) |
|
|
|
|
|
|
|
* Dave Parker (Oxford) |
|
|
|
* Gethin Norman (Glasgow) |
|
|
|
* Marta Kwiatkowska (Oxford) |
|
|
|
|
|
|
|
Many others have contributed to PRISM. In approximately reverse chronological order: |
|
|
|
We gratefully acknowledge contributions to the PRISM code-base from various sources, |
|
|
|
including (in approximately reverse chronological order): |
|
|
|
|
|
|
|
* Vojtech Forejt: "Fox-Glynn" implementation, explicit-state model checking |
|
|
|
* Christian von Essen: Contributions to explicit-state model checking library |
|
|
|
* Vincent Nimal: Approximate (simulation-based) model checking techniques |
|
|
|
* Mark Kattenbelt: Wide range of enhancements/additions, especially in the GUI |
|
|
|
* Carlos Bederian (working with Pedro D'Argenio): Addition of LTL model checking for MDPs to PRISM |
|
|
|
* Carlos Bederian (working with Pedro D'Argenio): LTL model checking for MDPs |
|
|
|
* Gethin Norman: Precomputation algorithms, abstraction |
|
|
|
* Alistair John Strachan: Port to 64-bit architectures |
|
|
|
* Alistair John Strachan, Mike Arthur and Zak Cohen: Integration of JFreeChart into PRISM |
|
|
|
* Charles Harley and Sebastian Vermehren: GUI enhancements |
|
|
|
* Rashid Mehmood: Improvements to low-level data structures and numerical solution algorithms |
|
|
|
* Stephen Gilmore: Support for the stochastic process algebra PEPA |
|
|
|
* Paolo Ballarini & Kenneth Chan: Port to Mac OS X |
|
|
|
* Andrew Hinton: Original versions of the GUI, Windows-port and simulator |
|
|
|
* Joachim Meyer-Kayser: Original implementation of the "Fox-Glynn" algorithm |
|
|
|
|
|
|
|
* Andrew Hinton: Original versions of the GUI, Windows port and simulator |
|
|
|
* Joachim Meyer-Kayser: Original implementation of the "Fox-Glynn" algorithm |
|
|
|
|
|
|
|
For more details see: |
|
|
|
|
|
|
|
http://www.prismmodelchecker.org/people.php |
|
|
|
|
|
|
|
|
|
|
|
------- |
|
|
|
CONTACT |
|
|
|
------- |
|
|
|
@ -118,12 +110,10 @@ If you have problems or questions regarding PRISM, please use the help forum pro |
|
|
|
Other comments and feedback about any aspect of PRISM are also very welcome. Please contact: |
|
|
|
|
|
|
|
Dave Parker |
|
|
|
(david.parker@cs.ox.ac.uk) |
|
|
|
Department of Computer Science |
|
|
|
University of Oxford |
|
|
|
Wolfson Building |
|
|
|
Parks Road |
|
|
|
Oxford |
|
|
|
OX1 3QD |
|
|
|
(d.a.parker@cs.bham.ac.uk) |
|
|
|
School of Computer Science |
|
|
|
University of Birmingham |
|
|
|
Edgbaston |
|
|
|
Birmingham |
|
|
|
B15 2TT |
|
|
|
ENGLAND |
|
|
|
|
Dave Parker
14 years ago