Please log in to watch this conference skillscast.
In this talk, we present an automated approach for formally verifying the correctness of functional programming assignments. Our approach takes a small set of reference solutions and a set of student submissions and checks, for each submission, whether it is provably correct. We start by introducing our technique for automated equivalence checking, using the Stainless verification system. Our approach automatically matches function calls, generates proofs by induction, and checks them using SMT solvers. We then present our clustering algorithm that efficiently treats many programs at once. We conclude by demonstrating the effectiveness of our approach in practice, looking at various introductory Scala exercises.
YOU MAY ALSO LIKE:
- Rust Nation 23 (in London on 16th - 17th February 2023)
- F# eXchange 2023: In-Person (in London on 7th - 8th March 2023)
- Haskell In Person: Bring Your Project, Get help with your code & socialise (in Berlin on 1st February 2023)
- How to teach IntelliJ IDEA to your juniors (Online Meetup on 2nd February 2023)
- Teaching Haskell...To High Schoolers! (SkillsCast recorded in December 2022)
- Teaching Haskell...To High Schoolers! (SkillsCast recorded in December 2022)