| ||||
| ||||
![]() Title:Auto-active verification using Why3's IDE Authors:Jean-Christophe Filliâtre Conference:F-IDE-18 Tags:auto-active verification, ide and why3 Abstract: Why3 is a platform for deductive program verification. It features a rich language for specification and programming, called WhyML, and relies on external theorem provers, both automated and interactive, to discharge verification conditions. Why3 comes with a dedicated IDE where users edit source files and build proofs interactively using a blend of logical transformations and calls to external theorem provers. In this talk, I will illustrate the typical workflow of program verification using Why3's IDE, focusing on the key features of WhyML, auto-active verification, and proof maintenance. Auto-active verification using Why3's IDE ![]() Auto-active verification using Why3's IDE | ||||
Copyright © 2002 – 2025 EasyChair |