LOGIN TO YOUR ACCOUNT

Username
Password
Remember Me
Or use your Academic/Social account:

CREATE AN ACCOUNT

Or use your Academic/Social account:

Congratulations!

You have just completed your registration at OpenAire.

Before you can login to the site, you will need to activate your account. An e-mail will be sent to you with the proper instructions.

Important!

Please note that this site is currently undergoing Beta testing.
Any new content you create is not guaranteed to be present to the final version of the site upon release.

Thank you for your patience,
OpenAire Dev Team.

Close This Message

CREATE AN ACCOUNT

Name:
Username:
Password:
Verify Password:
E-mail:
Verify E-mail:
*All Fields Are Required.
Please Verify You Are Human:
fbtwitterlinkedinvimeoflicker grey 14rssslideshare1
Brown, Neil C.C. (2009)
Publisher: EASST
Languages: English
Types: Unknown
Subjects: QA76

Classified by OpenAIRE into

ACM Ref: Software_PROGRAMMINGTECHNIQUES, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS
Tools such as FDR can check whether a CSP model of an implementation is a refinement of a given CSP specification. We present a technique for generating such CSP models of Haskell implementations that use the Communicating Haskell Processes library. Our technique avoids the need for a detailed semantics of\ud the Haskell language, and requires only minimal program annotation. The generated CSP-M model can be checked for deadlock or refinements by FDR, allowing easy use of formal methods without the need to maintain a model of the program implementation alongside the program itself.
  • The results below are discovered through our pilot algorithms. Let us know how we are doing!

    • [Bro08] N. C. C. Brown. Communicating Haskell Processes: Composable Explicit Concurrency Using Monads. In Communicating Process Architectures 2008. Pp. 67-84. Sept. 2008.
    • [BS08] N. C. C. Brown, M. L. Smith. Representation and Implementation of CSP and VCR Traces. In Communicating Process Architectures 2008. Pp. 329-345. Sept. 2008.
    • [CH00] K. Claessen, J. Hughes. QuickCheck: A Lightweight Tool for Random Testing of Haskell Programs. In Proc. of International Conference on Functional Programming (ICFP). ACM SIGPLAN, 2000.
    • [For97] Formal Systems (Europe) Ltd. Failures-Divergence Refinement: FDR2 Manual. 1997.
    • [FW09] L. Freitas, J. Woodcock. FDR Explorer. Formal Aspects of Computing 21:133-154, 2009.
    • [Hoa85] C. A. R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985. http://www.usingcsp.com/
    • [LF08] M. Leuschel, M. Fontaine. Probing the Depths of CSP-M: A new FDR-compliant Validation Tool. ICFEM 2008, 2008.
    • [RNL08] C. Runciman, M. Naylor, F. Lindblad. Smallcheck and Lazy Smallcheck: automatic exhaustive testing for small values. In Haskell '08: Proceedings of the first ACM SIGPLAN symposium on Haskell. Pp. 37-48. ACM, 2008.
    • [Ros97] A. W. Roscoe. The Theory and Practice of Concurrency. Prentice-Hall, 1997. http://www.comlab.ox.ac.uk/people/bill.roscoe/publications/68b.pdf
  • No related research data.
  • No similar publications.

Share - Bookmark

Download from

Cite this article