[klee-dev] Checking Tool Equivalence

Cristian Cadar c.cadar at imperial.ac.uk
Thu Jul 30 19:48:26 BST 2020


Hi Linda,

I cannot find that infrastructure anymore, but as explained in the 
paper, the idea was to rename global symbols and link the two tools 
together, accompanied by a new main function that looks similar in 
spirit to the one in Figure 11.  The only tricky part is to capture and 
compare the stdout, for which we used the --sym-stdout option of the 
POSIX runtime.

Hope this helps,
Cristian

On 29/07/2020 07:15, Linda Dart wrote:
> Hello,
> 
> The OSDI 2008 paper mentions that Klee was used for checking tool 
> equivalence, which took two tools and asserted that they were equal. A 
> "simple infrastructure" was built to automate crosschecking of two 
> tools. I was wondering if you could provide more insight on how to 
> implement this infrastructure?
> 
> Thanks,
> Linda
> 
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
> 



More information about the klee-dev mailing list