Test-case generation and bug-finding through symbolic execution
Willem Bester, Cornelia P. Inggs, W. C. Visser · 2012
In this paper we present Artemis, a tool to analyse Java bytecode and discover run-time errors. Artemis uses the method of symbolic execution to perform path-sensitive analysis on compiled Java classes, in the process building up constraints under which errors like null pointer dereferences and division-by-zero errors can occur. During the analysis, many warnings for possible errors may occur, but not all paths leading to these warnings are feasible. Artemis uses an external decision procedure---a constraint solver---to decide the feasibility of paths, and only if a path is feasible does it generate a JUnit test case for that path. It signals the possibility of a real error only if a test case manages to detect an expected exception during an actual run by the JUnit core.