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
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
