-
Notifications
You must be signed in to change notification settings - Fork 39
Home
Hi there! Welcome to the wiki for JDart, which serves the purpose of providing information about the configuration and usage of JDart.
JDart is a tool that executes Java Bytecode programs concolically. The concolic execution is triggered from within the regular execution of a Java program. The JDart configuration allows users to specify a method which is executed concolically: upon the first invocation of this method, a certain set of values (see below) will be treated symbolically. Once the method execution is finished, an attempt will be made to find a valuation (i.e., an assignment of concrete values to the symbolic variables) which triggers a different execution path through the program.
The result of the concolic execution is a constraints tree, i.e., a tree with its inner
nodes reflecting the decisions (involving at least one symbolic variable) that were made
during the execution of the program. The leaves are labeled with the status (OK if the
method was regularly exited, ERROR if there was an exception, or DONT_KNOW if no
valuation could be or should have been generated for the respective path). In case
the status in OK or ERROR, the leaf will also contain a concrete valuation suitable
for triggering exactly this path through the concolically executed method.