Welcome to Check 'n' Crash


We present an automatic error-detection approach that combines static checking and concrete test-case generation. Our approach consists of taking the abstract error conditions inferred using theorem proving techniques by a static checker (ESC/Java), deriving specific error conditions using a constraint solver, and producing concrete test cases (with the JCrasher tool) that are executed to determine whether an error truly exists. The combined technique has advantages over both static checking and automatic testing individually.


Overview of the Check 'n' Crash analysis pipeline: 
Check 'n' Crash uses ESC/Java to statically check the testee for potential bugs. In this example, ESC/Java warns about a potential runtime exception in the analyzed method when passing a negative parameter (the ESC/Java warning is not shown). Check 'n' Crash then compiles ESC/Java's bug warnings to concrete test cases to eliminate those warnings that cannot be reproduced in actual executions. In this example, Check 'n' Crash produces a test case that passes -1 into the method and confirms that it throws the runtime exception ESC/Java has warned about.


Download Check 'n' Crash--it's free.

DSD-Crasher is the successor of Check 'n' Crash.

Technical Talks

Technical Papers

Others using Check 'n' Crash in teaching

Others using Check 'n' Crash in research


We grant a liberal open source license ("MIT license").



This product includes software developed by the Apache Software Foundation (http://www.apache.org/).
See our license page for a list of third party components included in Check 'n' Crash.

This Website