Wed 21 Jun 2023 09:20 - 09:40 at Royal - PLDI: Testing & Verification Chair(s): Yao Li

We present an automated approach to verify the correctness of programming assignments, such as the ones that arise in a functional programming course. Our approach takes as input student submissions and reference solutions, and uses equivalence checking to automatically prove or disprove correctness of each submission. To be effective in the context of a real-world programming course, an automated grading system must be both robust, to support programs written in a variety of style, and scalable, to treat hundreds of submissions at once. We achieve robustness by handling recursion using functional induction and by handling auxiliary functions using function call matching. We achieve scalability using a clustering algorithm that leverages the transitivity of equivalence to discover intermediate reference solutions among student submissions. We implement our approach on top of the Stainless verification system, to support equivalence checking of Scala programs. We evaluate our system and its components on over 4000 programs drawn from a functional programming course and from the program equivalence checking literature; this is the largest such evaluation to date. We show that our system is capable of proving program correctness by generating inductive equivalence proofs, and providing counterexamples for incorrect programs, with a high success rate.

Wed 21 Jun

Displayed time zone: Eastern Time (US & Canada) change

09:00 - 11:00
PLDI: Testing & VerificationPLDI Research Papers at Royal
Chair(s): Yao Li Portland State University

#pldi-wed-0900-testing-royal Discord icon small YouTube icon small

09:00
20m
Talk
Mostly Automated Proof Repair for Verified LibrariesDistinguished Paper
PLDI Research Papers
Kiran Gopinathan National University of Singapore, Mayank Keoliya National University of Singapore, Ilya Sergey National University of Singapore
DOI Pre-print
09:20
20m
Talk
Proving and Disproving Equivalence of Functional Programming Assignments
PLDI Research Papers
Dragana Milovancevic EPFL, Viktor Kunčak EPFL, Switzerland
DOI Pre-print
09:40
20m
Talk
Feature-Sensitive Coverage for Conformance Testing of Programming Language Implementations
PLDI Research Papers
Jihyeok Park Korea University, Dongjun Youn KAIST, Kanguk Lee KAIST, Sukyoung Ryu KAIST
DOI Pre-print
10:00
20m
Talk
Psym: Efficient Symbolic Exploration of Distributed Systems
PLDI Research Papers
Lauren Pick University of Wisconsin-Madison and University of California, Berkeley, Ankush Desai Amazon Web Services, Aarti Gupta Princeton University
DOI
10:20
20m
Talk
Modular Control Plane Verification via Temporal Invariants
PLDI Research Papers
Tim Alberdingk Thijm Princeton University, Ryan Beckett Microsoft Research, USA, Aarti Gupta Princeton University, David Walker Princeton University
DOI
10:40
20m
Talk
Fair Operational Semantics
PLDI Research Papers
Dongjae Lee Seoul National University, Minki Cho Seoul National University, Jinwoo Kim Seoul National University, Soonwon Moon Inha University, Youngju Song MPI-SWS, Chung-Kil Hur Seoul National University
DOI