Abstract
We present a tool for finding errors in Java programs that translates Java bytecodes into symbolic pushdown systems, which are then checked by the Moped tool [1].
This work is supported by the EPSRC Grant GR/93346 “An Automata-theoretic Approach to Software Model Checking” and by the DFG project “Algorithms for Software Model Checking”.
Chapter PDF
Similar content being viewed by others
References
Schwoon, S.: Model-Checking Pushdown Systems. PhD thesis, TU Munich (2002)
Suwimonteerabuth, D.: Verifying Java bytecode with the Moped model checker. Master’s thesis, University of Stuttgart (2004)
Vaziri, M., Jackson, D.: Checking properties of heap-manipulating procedures with a contraint solver. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 505–520. Springer, Heidelberg (2003)
Esparza, J., Schwoon, S.: A BDD-based model checker for recursive programs. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 324–336. Springer, Heidelberg (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Suwimonteerabuth, D., Schwoon, S., Esparza, J. (2005). jMoped: A Java Bytecode Checker Based on Moped. In: Halbwachs, N., Zuck, L.D. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2005. Lecture Notes in Computer Science, vol 3440. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-31980-1_35
Download citation
DOI: https://doi.org/10.1007/978-3-540-31980-1_35
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-25333-4
Online ISBN: 978-3-540-31980-1
eBook Packages: Computer ScienceComputer Science (R0)