MoonWalker: Verification of .NET Programs

Niels H.M. Aan de Brugh; Viet Yen Nguyen; Theo C. Ruys

doi:10.1007/978-3-642-00768-2_15

MoonWalker: Verification of .NET Programs

Niels H.M. Aan de Brugh, Viet Yen Nguyen, Theo C. Ruys

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

9 Citations (Scopus)

1 Downloads (Pure)

Abstract

MoonWalker is a software model checker for CIL bytecode programs, which is able to detect deadlocks and assertion violations in CIL assemblies, better known as Microsoft .NET programs. The design of MoonWalker is inspired by the Java PathFinder (JPF), a model checker for Java programs. The performance of MoonWalker is on par with JPF. This paper presents the new version of MoonWalker and discusses its most important features.

Original language	English
Title of host publication	Tools and Algorithms for the Construction and Analysis of Systems
Subtitle of host publication	15th International Conference, TACAS 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009, Proceedings
Editors	Stefan Kowalewski, Anna Philippou
Place of Publication	Berlin, Heidelberg
Publisher	Springer
Pages	170-173
Number of pages	4
ISBN (Electronic)	978-3-642-00768-2
ISBN (Print)	978-3-642-00767-5
DOIs	https://doi.org/10.1007/978-3-642-00768-2_15
Publication status	Published - Mar 2009
Event	15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2009 - York, United Kingdom Duration: 22 Mar 2009 → 29 Mar 2009 Conference number: 15

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	5505
ISSN (Print)	0302-9743

Name	Theoretical Computer Science and General Issues
Publisher	Springer
ISSN (Print)	2512-2010
ISSN (Electronic)	2512-2029

Conference

Conference	15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2009
Abbreviated title	TACAS
Country/Territory	United Kingdom
City	York
Period	22/03/09 → 29/03/09

Keywords

FMT-MC: MODEL CHECKING
n/a OA procedure

Access to Document

10.1007/978-3-642-00768-2_15

Cite this

Aan de Brugh, N. H. M., Nguyen, V. Y., & Ruys, T. C. (2009). MoonWalker: Verification of .NET Programs. In S. Kowalewski, & A. Philippou (Eds.), Tools and Algorithms for the Construction and Analysis of Systems: 15th International Conference, TACAS 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009, Proceedings (pp. 170-173). (Lecture Notes in Computer Science; Vol. 5505), (Theoretical Computer Science and General Issues). Springer. https://doi.org/10.1007/978-3-642-00768-2_15

Aan de Brugh, Niels H.M. ; Nguyen, Viet Yen ; Ruys, Theo C. / MoonWalker : Verification of .NET Programs. Tools and Algorithms for the Construction and Analysis of Systems: 15th International Conference, TACAS 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009, Proceedings. editor / Stefan Kowalewski ; Anna Philippou. Berlin, Heidelberg : Springer, 2009. pp. 170-173 (Lecture Notes in Computer Science). (Theoretical Computer Science and General Issues).

@inproceedings{ac7e36f383b5414db1b7d3a3aac324e6,

title = "MoonWalker: Verification of .NET Programs",

abstract = "MoonWalker is a software model checker for CIL bytecode programs, which is able to detect deadlocks and assertion violations in CIL assemblies, better known as Microsoft .NET programs. The design of MoonWalker is inspired by the Java PathFinder (JPF), a model checker for Java programs. The performance of MoonWalker is on par with JPF. This paper presents the new version of MoonWalker and discusses its most important features.",

keywords = "FMT-MC: MODEL CHECKING, n/a OA procedure",

author = "{Aan de Brugh}, {Niels H.M.} and Nguyen, {Viet Yen} and Ruys, {Theo C.}",

year = "2009",

month = mar,

doi = "10.1007/978-3-642-00768-2_15",

language = "English",

isbn = "978-3-642-00767-5",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "170--173",

editor = "Stefan Kowalewski and Anna Philippou",

booktitle = "Tools and Algorithms for the Construction and Analysis of Systems",

address = "Germany",

note = "15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2009, TACAS ; Conference date: 22-03-2009 Through 29-03-2009",

}

Aan de Brugh, NHM, Nguyen, VY & Ruys, TC 2009, MoonWalker: Verification of .NET Programs. in S Kowalewski & A Philippou (eds), Tools and Algorithms for the Construction and Analysis of Systems: 15th International Conference, TACAS 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009, Proceedings. Lecture Notes in Computer Science, vol. 5505, Theoretical Computer Science and General Issues, Springer, Berlin, Heidelberg, pp. 170-173, 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2009, York, United Kingdom, 22/03/09. https://doi.org/10.1007/978-3-642-00768-2_15

MoonWalker: Verification of .NET Programs. / Aan de Brugh, Niels H.M.; Nguyen, Viet Yen; Ruys, Theo C.
Tools and Algorithms for the Construction and Analysis of Systems: 15th International Conference, TACAS 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009, Proceedings. ed. / Stefan Kowalewski; Anna Philippou. Berlin, Heidelberg: Springer, 2009. p. 170-173 (Lecture Notes in Computer Science; Vol. 5505), (Theoretical Computer Science and General Issues).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - MoonWalker

T2 - 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2009

AU - Aan de Brugh, Niels H.M.

AU - Nguyen, Viet Yen

AU - Ruys, Theo C.

N1 - Conference code: 15

PY - 2009/3

Y1 - 2009/3

N2 - MoonWalker is a software model checker for CIL bytecode programs, which is able to detect deadlocks and assertion violations in CIL assemblies, better known as Microsoft .NET programs. The design of MoonWalker is inspired by the Java PathFinder (JPF), a model checker for Java programs. The performance of MoonWalker is on par with JPF. This paper presents the new version of MoonWalker and discusses its most important features.

AB - MoonWalker is a software model checker for CIL bytecode programs, which is able to detect deadlocks and assertion violations in CIL assemblies, better known as Microsoft .NET programs. The design of MoonWalker is inspired by the Java PathFinder (JPF), a model checker for Java programs. The performance of MoonWalker is on par with JPF. This paper presents the new version of MoonWalker and discusses its most important features.

KW - FMT-MC: MODEL CHECKING

KW - n/a OA procedure

U2 - 10.1007/978-3-642-00768-2_15

DO - 10.1007/978-3-642-00768-2_15

M3 - Conference contribution

SN - 978-3-642-00767-5

T3 - Lecture Notes in Computer Science

SP - 170

EP - 173

BT - Tools and Algorithms for the Construction and Analysis of Systems

A2 - Kowalewski, Stefan

A2 - Philippou, Anna

PB - Springer

CY - Berlin, Heidelberg

Y2 - 22 March 2009 through 29 March 2009

ER -

Aan de Brugh NHM, Nguyen VY, Ruys TC. MoonWalker: Verification of .NET Programs. In Kowalewski S, Philippou A, editors, Tools and Algorithms for the Construction and Analysis of Systems: 15th International Conference, TACAS 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009, Proceedings. Berlin, Heidelberg: Springer. 2009. p. 170-173. (Lecture Notes in Computer Science). (Theoretical Computer Science and General Issues). doi: 10.1007/978-3-642-00768-2_15

MoonWalker: Verification of .NET Programs

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Cite this