Tools for Verified Scala
Explore tools for code verification, synthesis, and repair developed by Viktor Kuncak's research group at EPFL in this 52-minute keynote from Scala Days Copenhagen 2017. Dive into Stainless, a tool that analyzes Scala programs, and learn how to use 'require' and 'ensuring' statements for input elaboration and output verification. Examine practical examples, including adding two naturals and implementing an IntSet, while understanding how to state and prove algebraic properties using postconditions. Investigate automated verification techniques, such as induction and uniform decision procedures, and their integration with types. Discover the potential of program synthesis through an insertion sort example. Gain insights into cutting-edge research that enhances Scala development practices and promotes more reliable, verifiable code.