Skip to content

Make adequacy apply to multiple initial threads

Michael Sammler requested to merge msammler/multithread_adequacy into master

This MR adapts wp_strong_adequacy to apply to an initial configuration with multiple threads. This is necessary for RefinedC since it currently does not have a fork operation, but instead relies on multiple threads in the initial configuration for concurrency.

This MR is WIP because I don't know how to prove big_sepL2_fupd without the proof mode. @robbertkrebbers how would you prove it?

Edited by Michael Sammler

Merge request reports