Proof automation can substantially increase productivity in the formal verification of complex systems. However, the unpredictability of automated provers in handling quantified formulas presents a major hurdle to usability of these tools. Here, we propose to solve this problem not by improving the provers, but by using a modular proof methodology that allows us to produce decidable verification conditions. Decidability greatly improves the predictability of proof automation, resulting in a more practical verification approach. We apply this methodology to develop verified implementations of distributed protocols with competitive performance, showing its effectiveness

Tue 19 Jun

09:00 - 10:30: DeepSpec 2018 - Distributed Systems and Cryptography at Columbus Ballroom B
deepspec-2018-papers09:00 - 10:00
Mooly SagivTel Aviv University
deepspec-2018-papers10:00 - 10:30