Advertisement

jMoped: A Java Bytecode Checker Based on Moped

  • Dejvuth Suwimonteerabuth
  • Stefan Schwoon
  • Javier Esparza
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3440)

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].

References

  1. 1.
    Schwoon, S.: Model-Checking Pushdown Systems. PhD thesis, TU Munich (2002)Google Scholar
  2. 2.
    Suwimonteerabuth, D.: Verifying Java bytecode with the Moped model checker. Master’s thesis, University of Stuttgart (2004)Google Scholar
  3. 3.
    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)CrossRefGoogle Scholar
  4. 4.
    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)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Dejvuth Suwimonteerabuth
    • 1
  • Stefan Schwoon
    • 1
  • Javier Esparza
    • 1
  1. 1.Institut für Formale Methoden der InformatikUniversität Stuttgart 

Personalised recommendations