BDDs for Cartesian Products + Threshold

BDD-based verification with large polynomial guarantees

• Degree: bachelor | master | research paper
• State: open

We want a BDD-based verification algorithm which is polynomial on the following programs: binary-mutex, all thread-modular-provable programs, bluetooth and all programs whose proofs need at most the threshold function and local reasoning.