[klee-dev] model checking options

[Cristian Cadar]

Hi,

Mainline KLEE does not have any support for concurrency, although there 
are extensions of it which do.
Safety properties of the form that you mention could be encoded with 
some additional custom instrumentation, but there are no command-line 
arguments or intrinsics for specifying them directly.

Best,
Cristian

On 8/22/24 08:00, Jeroen Meijer wrote:
> Does klee have any built-in model checking options? Like deadlock 
> detection, or perhaps checking for some basic linear-time properties 
> (such as "I never want to see a particular sequence of function calls")?
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
-------------- next part --------------
HTML attachment scrubbed and removed