Dragana Milovancevic
EPFL IC IINFCOM LARA
INR 318 (Bâtiment INR)
Station 14
1015 Lausanne
Web site: Site web: https://lara.epfl.ch
Biographie
I'm a PhD student in the LARA group at EPFL, under the supervision of Viktor Kuncak. My research interests are in the field of formal verification, and include equivalence checking and automated grading.Publications
Publications Infoscience
Formal Autograding in a Classroom (Experience Report)
We report our experience in enhancing automated grading in a functional programming course using formal verification. In our approach, we deploy a verifier for Scala programs to check equivalences between student submissions and reference solutions. Consequently, students receive more thorough evaluation of assignments that explores behaviours beyond those envisioned by tests or test generators. We collect student submissions and make them publicly available. We analyse the collected data set and find that we can use the conservative nature of our program equivalence checking as an advantage: we were able to use such equivalence to differentiate student solutions according to their high-level program structure, in particular their recursion pattern, even when their input-output behaviour is identical.
2024Formula Normalizations in Verification
We propose a new approach for normalization and simplification of logical formulas. Our approach is based on algorithms for lattice-like structures. Specifically, we present two efficient algorithms for computing a normal form and deciding the word problem for two subtheories of Boolean algebra, giving a sound procedure for propositional logical equivalence that is incomplete in general but complete with respect to a subset of Boolean algebra axioms. We first show a new algorithm to produce a normal form for expressions in the theory of ortholattices (OL) in time O(n^2). We also consider an algorithm, recently presented but never evaluated in practice, producing a normal form for a slightly weaker theory, orthocomplemented bisemilattices (OCBSL), in time O(n log(n)^2). For both algorithms, we present an implementation and show efficiency in two domains. First, we evaluate the algorithms on large propositional expressions, specifically combinatorial circuits from a benchmark suite, as well as on large random formulas. Second, we implement and evaluate the algorithms in the Stainless verifier, a tool for verifying the correctness of Scala programs. We used these algorithms as a basis for a new formula simplifier, which is applied before valid verification conditions are saved into a persistent cache. The results show that normalization substantially increases cache hit ratio in large benchmarks.
2023-06-16. 35th International Conference on Computer Aided Verification, Paris, France.Proving and Disproving Equivalence of Functional Programming Assignments
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.
2023. p. 928-951. DOI : 10.1145/3591258.