jMoped: A Java bytecode checker based on Moped. 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.
Keywords for this software
References in zbMATH (referenced in 7 articles , 1 standard article )
Showing results 1 to 7 of 7.
- Lang, Martin; Löding, Christof: Modeling and verification of infinite systems with resources (2013)
- Esparza, Javier; Kiefer, Stefan; Schwoon, Stefan: Abstraction refinement with Craig interpolation and symbolic pushdown systems (2009)
- Kühnrich, Morten; Schwoon, Stefan; Srba, Jiří; Kiefer, Stefan: Interprocedural dataflow analysis over weight domains with infinite descending chains (2009)
- Lal, Akash; Reps, Thomas: Reducing concurrent analysis under a context bound to sequential analysis (2009)
- Bouajjani, Ahmed; Esparza, Javier: Rewriting models of Boolean programs (2006)
- Suwimonteerabuth, Dejvuth; Schwoon, Stefan; Esparza, Javier: jMoped: A Java bytecode checker based on Moped (2005)
- Esparza, Javier: An algebraic approach to the static analysis of concurrent software (2002)