Recent improvements to the McErlang model checker

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Recent improvements to the McErlang model checker

Full text

Pdf (523 KB)

Source

International Conference on Functional Programming archive
Proceedings of the 8th ACM SIGPLAN workshop on Erlang table of contents

Edinburgh, Scotland

SESSION: Testing and model checking table of contents

Pages 93-100

Year of Publication: 2009

ISBN:978-1-60558-507-9

Authors

Clara Benac Earle	Universidad Politécnica de Madrid, Madrid, Spain
Lars Ake Fredlund	Universidad Politécnica de Madrid, Madrid, Spain

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages
ACM: Association for Computing Machinery

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 5, Downloads (12 Months): 5, Citation Count: 0

Additional Information:

abstract references index terms

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/1596600.1596613 What is a DOI?

ABSTRACT

In this paper we describe a number of recent improvements to the McErlang model checker, including a new source to source translation to enable more Erlang programs to work under McErlang, a methodology for writing properties that can be verified by McErlang, and a combination of simulation and model checking. The latter two features are illustrated by means of the messenger example found in the documentation of the Erlang/OTP distribution.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	http://erlang.org/doc/getting started/part frame.html.
	2	https://babel.ls.fi.upm.es/trac/McErlang/.
	3	T. Andrews, S. Qadeer, S. Rajamani, J. Rehof, and Y. Xie. Zing: A model checker for concurrent software. In Lecture Notes in Computer Science, volume Vol. 3114, pages 484--487, Jan 2004.
	4	T. Arts, C. Benac Earle, and J. Sanchez Penas. Translating Erlang to mucrl. In Proceedings of the International Conference on Application of Concurrency to System Design (ACSD2004). IEEE Computer Society Press, June 2004.
	5	T. Arts, J. Hughes, J. Johansson, and U. Wiger. Testing telecoms software with Quviq QuickCheck. In ACM Sigplan International Erlang Workshop. ACM Press, 2006.
	6	C. Benac Earle, L. Fredlund, J. Iglesias, and A. Ledezma. Verifying robocup teams. Electronic Notes in Theoretical Computer Science, 5348/2009:34--48, 2008.
	7	R. Carlsson. An introduction to Core Erlang. In Proceedings of the 2001 ACM SIGPLAN Erlang Workshop, 2001.
	8	M. B. Dwyer, J. Hatcliff, M. Hoosier, and Robby. Building your own software model checker using the Bogor extensible model checking framework. In K. Etessami and S. K. Rajamani, editors, CAV, volume 3576 of Lecture Notes in Computer Science, pages 148--152. Springer, 2005.
	9	J.-C. Fernandez, H. Garavel, A. Kerbrat, L. Mounier, R. Mateescu, and M. Sighireanu. CADP: A protocol validation and verification toolbox. In Proceedings of the 8th Conference on Computer-Aided Verification, volume 1102 of Lecture Notes in Computer Science, pages 437--440. Springer, 1996.
	10	L. Fredlund and C. Benac Earle. Model checking Erlang programs: The functional approach. In ACM Sigplan International Erlang Workshop, Portland, USA, 2006.
	11	L. Fredlund, D. Gurov, T. Noll, M. Dam, T. Arts, and G. Chugunov. A verification tool for Erlang. International Journal on Software Tools for Technology Transfer (STTT), 4(4):405--420, Aug 2003.
	12	L. Fredlund and J. Sanchez Penas. Model checking a VoD server using McErlang. In In proceedings of the 2007 Eurocast conference, Feb 2007.
	13	L. Fredlund and H. Svensson. McErlang: a model checker for a distributed functional programming language. In Proceedings of the 12th ACM SIGPLAN International conference on functional programming (ICFP 2007), Oct. 2007.
	14	P. Godefroid. Verisoft: A tool for the automatic analysis of concurrent reactive software. In Computer Aided Verification, pages 476--479, 1997.
	15	G. Holzmann. Design and Validation of Computer Protocols. Prentice-Hall, 1991.
	16	G. J. Holzmann and M. H. Smith. An automated verification method for distributed systems software based on model extraction. IEEE Trans. Softw. Eng., 28(4):364--377, 2002.
	17	F. Huch. Verification of Erlang programs using abstract interpretation and model checking. In Proceedings of the 1999 ACM SIGPLAN International Conference on Functional Programming, 1999.
	18	J. Hughes. Quickcheck testing for fun and profit. In 9th International Symposium on Practical Aspects of Declarative Languages. Springer, 2007.
	19	H. Svensson. Implementing an LTL-to-Buchi translator in Erlang. In Proceedings of the 2009 ACM SIGPLAN Erlang Workshop, 2009.
	20	W. Visser, K. Havelund, G. Brat, and S. Park. Java pathfinder - second generation of a Java model checker, 2000.
	21	J. Yang, P. Twohey, D. Engler, and M. Musuvathi. Using model checking to find serious file system errors. In Sixth Symposium on Operating Systems Design and Implementation, pages 273--288. USENIX, 2004.