Repository logo

Infoscience

  • English
  • French
Log In
Logo EPFL, École polytechnique fédérale de Lausanne

Infoscience

  • English
  • French
Log In
  1. Home
  2. Academic and Research Output
  3. Conferences, Workshops, Symposiums, and Seminars
  4. Proving and Disproving Equivalence of Functional Programming Assignments
 
conference paper

Proving and Disproving Equivalence of Functional Programming Assignments

Milovancevic, Dragana  
•
Kuncak, Viktor  
2023
Proceedings of the ACM on Programming Languages

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.

  • Files
  • Details
  • Metrics
Loading...
Thumbnail Image
Name

main.pdf

Type

N/a

Access type

openaccess

License Condition

CC BY-NC-ND

Size

232.18 KB

Format

Adobe PDF

Checksum (MD5)

5bc9e7594595973d8cfec65399c930ca

Loading...
Thumbnail Image
Name

3591258.pdf

Type

Publisher

cris-layout.advanced-attachment.oaire.version

http://purl.org/coar/version/c_970fb48d4fbd8a85

Access type

openaccess

License Condition

CC BY

Size

317.49 KB

Format

Adobe PDF

Checksum (MD5)

24df31b72348e75c442444cd8065e456

Logo EPFL, École polytechnique fédérale de Lausanne
  • Contact
  • infoscience@epfl.ch

  • Follow us on Facebook
  • Follow us on Instagram
  • Follow us on LinkedIn
  • Follow us on X
  • Follow us on Youtube
AccessibilityLegal noticePrivacy policyCookie settingsEnd User AgreementGet helpFeedback

Infoscience is a service managed and provided by the Library and IT Services of EPFL. © EPFL, tous droits réservés