JNuke: Efficient Dynamic Analysis for Java

JNuke is a framework for verification and model checking of Java programs. It is a novel combination of run-time verification, explicit-state model checking, and counter-example exploration. Efficiency is crucial in dynamic verification. Therefore JNuke has been written from scratch in C, improving performance and memory usage by an order of magnitude compared to competing approaches and tools.

• Type: Conference
• Year: 2004
• Where: CAV
• Authors: Cyrille Artho, Viktor Schuppan, Armin Biere, Pascal Eugster, Marcel Baur, Boris Zweimüller
• Keywords: CAV 2004, Explicit-state Model Checking, Hardware, Model Checking, Run-time Verification