[LLVMdev] [klee-dev] Linearizability

[Baris Kasikci]

Hi Andreas,

Cloud9 is a project that has an extensive POSIX environment model
which also lets you symbolically execute multithreaded programs. It is
based on KLEE.

http://dslab.epfl.ch/pubs/cloud9.pdf

Portend builds on top of Cloud9 to perform race detection/classification:

http://dslab.epfl.ch/pubs/portend.pdf

Cloud9 code base is also public, it might be of interest to you:

http://cloud9.epfl.ch/

Best,

On Thu, Oct 25, 2012 at 3:49 PM, Andreas Wilhelm
<andreas.wilhelm at in.tum.de> wrote:
> Hello,
>
> I intend to create a tool for detecting thread-safety problems within libraries.
> Therefore I would like to use the "Linearizability" correctness principle. Were there
> any efforts within the KLEE project regarding to that topic? Would it be interesting
> for the community at all?
>
> Best regards,
> Andreas
> _______________________________________________
> klee-dev mailing list
> klee-dev at keeda.stanford.edu
> http://keeda.Stanford.EDU/mailman/listinfo/klee-dev



-- 
Baris