I found this pretty funny - read the docs while being totally excited and then saw my name second on the contributors list, I wrote a little code waaaaay back when Crosshair first started but completely forgot about it. Will definitely check out using it later today :)
This seems to be an instance of concolic execution which has seen some success in the fuzzing and testing research community. The key ideas originate from these papers:
The technique works well when parts of the program space (including paths through the program) can be easily represented in SMT solvers (like booleans, bit vectors, and arithmetic), and the remainder program space can be explored using random testing. I am excited to see this work being brought to Crosshair in Python via Hypothesis!
3 comments
[ 3.6 ms ] story [ 19.2 ms ] thread[1] https://web.eecs.umich.edu/~weimerw/590/reading/p213-godefro...
[2] https://mir.cs.illinois.edu/marinov/publications/SenETAL05CU...
The Wikipedia page gives a good overview of the area and some successful applications: https://en.wikipedia.org/wiki/Concolic_testing
The technique works well when parts of the program space (including paths through the program) can be easily represented in SMT solvers (like booleans, bit vectors, and arithmetic), and the remainder program space can be explored using random testing. I am excited to see this work being brought to Crosshair in Python via Hypothesis!