Reference:

Dejvuth Suwimonteerabuth, Stefan Schwoon, and Javier Esparza. jMoped: A Java bytecode checker based on Moped. In Nicolas Halbwachs and Lenore Zuck, editors, Proceedings of the 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 3440 of Lecture Notes in Computer Science, pages 541–545, Edinburgh, UK, April 2005. Springer. Tool paper.

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.

Suggested BibTeX entry:

@inproceedings{SSE05,
    address = {Edinburgh, UK},
    author = {Dejvuth Suwimonteerabuth and Stefan Schwoon and Javier Esparza},
    booktitle = {Proceedings of the 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)},
    editor = {Nicolas Halbwachs and Lenore Zuck},
    month = {April},
    note = {Tool paper},
    pages = {541--545},
    publisher = {Springer},
    series = {Lecture Notes in Computer Science},
    title = {{jMoped}: A {Java} bytecode checker based on {Moped}},
    volume = {3440},
    year = {2005}
}