All hope abandon ye who enter here

1. Consists of the explorer and the executor
   1. The explorer determines the exploration strategy (order of traversal)
      1. Organises recorded (by executor) path into a constraints tree
      2. Decides which paths to explore next and when to stop exploration
      3. Currently uses JConstraints (layer of abstraction for symbolic paths constraints and an interface to the existing constraint solvers)
      4. Solvers supported:
         1. Coral -- supports trigonometric constraints
         2. SMTInterpol
         3. Z3 -- Trig is approximated, floats are approximated by reals

SMT solvers provide decision procedures for first-order logical formulas of from different theories (integer numbers, bit vectors, arrays..) Given a set of constraints, the solver will generate a satisfying assignment

Note on exploration: In order to hit interesting paths quicker when analysing large systems, JDart needs to be able to limit exploration to certain paths. JDart provides configuration options for specifying multiple pre-determined vectors of input values from which the exploration starts It also allows the user to specify assumptions on input parameters as symbolic constarints After those are specified the exploration will be bound by the provided constarints. Finally, JDart can be configured to simply skip exploration of certain parts of a program.

1. The executor executes (obviously) the analysed program and records symbolic constraints

For execution the JPF engine is used that suppotrts native peers, symbolic objects and Concolic Bytecode Semantics. Using it has several benefits such as ease of JDart extension by integration of existing JPF plugins/extenstions. JPF provides easy access to all objects on the heap and stack ans well as to other elements of the JVM (stack frames and classloaders) However, using a full-blown custon JVM (which JPF is) has significant impact on performance.. Thats why the JPF integration in JDart is very loose (possibly swapped to a more light-weight implementation in the future)

1. Provides a few useful plugins, such as:
   1. Method summarisation
   2. JUnit test case generation (leverages the results of dynamic symbolic analysis)
2. Can be used as a symbolic execution component within other tools
   1. PSYCHO -- tool that uses automata learning and dyn symb exec to automatically generate extended interfaces for java library components
   2. JPF-Doop -- tool that combines random feedback-directed generation of method sequences with dynamic symbolic execution for automatic testing of java libraries
3. Has been proven to work and thoroughly tested by NASA (they have used it to generate tests for the air traffic control system - so it practically is proven to be correct)
4. By default, JDart treats only parameters symbolically
   1. But this could be extended to instance fields and return values as well
5. JDart is designed to allow for easy replacement of all of its components, supports different and combined constraint solvers and several exploration strategies and termination criteria
6. JDart provides an interface for implementing customised termination strategies (time vs paths)
7. Progress in only made when evaluating semantics in solvers

The devil is not as black as he is painted

1. Executes programs with concrete and symbolic inputs at the same time
2. Maintains a path constraint (conjunction of symbolic expressions over the inputs that is updated whenever a branch instruction is executed)
3. Combined execution paths for a constraints tree, which is continuously expanded
4. Concrete data values for excercising these paths are generated by a constraint solver

1. Executes java bytecode and performs dynamic symbolic analysis of specific paths ???
2. Implements extensions that build upon the analysis
   1. The Method Summariser -- generates flly abstract method summaries for analysied methods. In the generated summaries, class members, input parameters and return values are symbolic.
   2. The Tests Suite Generator -- generates a JUnit test suit that excercises all the paths found

1. Constraint solver abstration layer
2. Provides representaion for logic expressions, unified access to different SMT and interpolation solvers and useful tools and algorithms for working with constraints
3. Plugins for connecting to basic constraint solvers are easy to implement through solver interface and taking care of translating between a solver-specific API and the object representaion of JConstraints
4. Supports user-defined types -- easy to validate solutions returned by constraint solvers by simply evaluating the path constraint stored by JConstraints with java semantics

Date the paper

1. SPF can work with concolic execution (switch to concrete values - concolic)
2. Parallelising SPF has been done
3. Method summarisation for SPF
4. JDart does not support programs with concurrency... SPF does
5. SPF - lazy initialisation (to deal with unbounded symbolic input data)
6. SPF crashes with Z3, leaving CORAL as the only viable solver, which means that it ignores some constraints
7. JDart generates stronger test suites
8. More stable and way more consistent...

1. Install jpf-core
2. Install jdart
3. Install z3 from ( https://github.com/Z3Prover/z3/releases/download/z3-4.4.1/z3-4.4.1-x64-debian-8.2.zip ) mvn isntall it to a local repository place the libz3java.so and libz3.so into a global java lib folder
4. Install JConstraints mvn install to a local repo
5. Install JConstraints-z3
6. Copy jars from target in JConstraints-z3 to ~/.jconstraints/extensions/
7. Copy com.microsoft.z3.jar to ~/.jconstraints/extensions