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.
Chapter PDF
Similar content being viewed by others
References
Aan de Brugh, N.H.M.: Software Model Checking for Mono. Master’s thesis, University of Twente, Enschede, The Netherlands (August 2006)
Artho, C., Schuppan, V., Biere, A., Eugster, P., Baur, M., Zweimüller, B.: JNuke: Efficient Dynamic Analysis for Java. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 462–465. Springer, Heidelberg (2004)
Fargas, P.: Garbage Collection for JNuke. Master’s thesis, ETH Zürich, Switzerland (September 2004)
Flanagan, C., Godefroid, P.: Dynamic Partial-Order Reduction for Model Checking Software. In: Proc. of POPL 2005, pp. 110–121. ACM Press, New York (2005)
Grieskamp, W., Tillmann, N., Schulte, W.: XRT: Exploring Runtime for. NET - Architecture and Applications. ENTCS 144(3), 3–26 (2006); Proc. of SoftMC 2005
Iosif, R., Sisto, R.: Using Garbage Collection in Model Checking. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol. 1885, pp. 20–33. Springer, Heidelberg (2000)
Nguyen, V.Y.: Optimising Techniques for Model Checkers. Master’s thesis, University of Twente, Enschede, The Netherlands (December 2007)
Nguyen, V.Y., Ruys, T.C.: Memoised Garbage Collection for Software Model Checking. In: Knowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 201–214. Springer, Heidelberg (2009)
Ramalingam, G., Reps, T.W.: An Incremental Algorithm for a Generalization of the Shortest-Path Problem. Journal Algorithms 21(2), 267–305 (1996)
Ranganath, V.P., Hatcliff, J., Robby.: Enabling Efficient Partial Order Reductions for Model Checking Object-Oriented Programs. Technical Report SAnToS-TR2007-2, SAnToS Laboratory, CIS Department, Kansas State University (2007)
Ruys, T.C., Aan de Brugh, N.H.M.: MMC: the Mono Model Checker. ENTCS 190(1), 149–160 (2007); Proc. of Bytecode 2007, Braga, Portugal
Visser, W., Havelund, K., Brat, G., Park, S., Lerda, F.: Model Checking Programs. ASE 10(2), 203–232 (2003)
Yi, X., Wang, J., Yang, X.: Stateful Dynamic Partial-Order Reduction. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol. 4260, pp. 149–167. Springer, Heidelberg (2006)
The Java Grande Forum Benchmark Suite, http://www.epcc.ed.ac.uk/research/activities/java-grande/
Java PathFinder, http://javapathfinder.sourceforge.net/
The Mono Project, http://www.mono-project.com/
.NET Languages, http://www.dotnetlanguages.net/
Moonwalker, http://www.cs.utwente.nl/~ruys/moonwalker/
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Aan de Brugh, N.H.M., Nguyen, V.Y., Ruys, T.C. (2009). MoonWalker: Verification of .NET Programs. In: Kowalewski, S., Philippou, A. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2009. Lecture Notes in Computer Science, vol 5505. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-00768-2_15
Download citation
DOI: https://doi.org/10.1007/978-3-642-00768-2_15
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-00767-5
Online ISBN: 978-3-642-00768-2
eBook Packages: Computer ScienceComputer Science (R0)