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