3 ms·
Is this applicable to proofs of concurrent code? Or is Dafny not the right tool?
by anonymousDan 1y ago
Is this applicable to proofs of concurrent code? Or is Dafny not the right tool?
- lou1306 1y agoI am not a Dafny expert but from what I have gathered it uses a deductive procedure underneath, so it's rather geared towards sequential code. To analyse concurrent code, one needs to essentially build a sequential program that _also models the scheduler_ (see e.g., [1]). This procedure is unsurprisingly called sequentialization and (somewhat less unsurprisingly) is also a pretty good approach when applied to other techniques, such as bounded model checking [2]. [1] https://leino.science/papers/krml260.pdf https://leino.science/papers/krml260.pdf [2] https://research.cs.wisc.edu/wpis/papers/cav08.pdf https://research.cs.wisc.edu/wpis/papers/cav08.pdf