[LLVMdev] [klee-dev] Linearizability

Baris Kasikci bariskasikci at gmail.com
Thu Oct 25 08:03:15 PDT 2012

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.


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


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



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


More information about the llvm-dev mailing list