Probing the Depths of CSP-M: A new FDR-compliant Validation Tool
[PDF] [Bibtex]ICFEM 2008, 2008.
We present a new animation and model checking tool for CSP. The tool covers the CSP-M language, as supported by existing tools such as fdr and probe. Compared to those tools, it provides visual feedback in the source code, has an LTL model checker and can be used for combined CSP||B specifications. During the development of the tool some intricate issues were uncovered with the CSP-M language. We discuss those issues, and provide suggestions for improvement. We also explain how we have ensured conformance with fdr, by using fdr itself to validate our tool's output. We also provide empirical evidence on the performance of our tool compared to fdr, showing that it can be used on industrial-strength specifications.
The Ecce and Logen Partial Evaluators and their Web Interfaces
[PDF] [Bibtex]In Proceedings PEPM 06, IBM Press, 2006.
We present Ecce and Logen, two partial evaluators for Prolog using the online and offline approach respectively. We briefly present the foundations of these tools and discuss various applications. We also present new implementations of these tools, carried out in Ciao Prolog. In addition to a command-line interface new user-friendly web interfaces were developed. These enable non-expert users to specialise logic programs using a web browser, without the need for a local installation.