APR Event November 2023
Date
| Date | Wednesday, November 22, 2023 |
| Time | 9 am to 8:30 pm |
Program
(all times are in the local timezone: Singapore Standard Time, i.e., UTC+8)
| Start | End | Agenda Item |
|---|---|---|
| 09:00 AM | 09:05 AM | Welcome Message |
| 09:05 AM | 09:50 AM | Alex Potanin “Raising Expressivity in Verification and Synthesis Languages” |
| 09:50 AM | 10:35 AM | Sergey Mechtaev “Symbolic Execution of Datalog and its Application to Static Analysis Guided Program Repair” |
| 10:35 AM | 11:00 AM | Coffee Break |
| 11:00 AM | 11:20 AM | Ratnadira Widyasari “XAI4FL: Enhancing Spectrum-Based Fault Localization with Explainable AI” |
| 11:20 AM | 11:40 AM | Yahui Song “Datalog Repair guided by CTL Properties” |
| 11:40 AM | 12:10 PM | Kiran Gopinathan “Mostly Automated Proof Repair for Verified Libraries” |
| 12:10 PM | 12:30 PM | Ting Zhang “Evaluating Pre-trained Language Models for Repairing API Misuses” |
| 12:30 PM | 12:50 PM | Zhiyu Fan “ Intelligent Tutoring for Programming Education “ |
| 12:50 PM | 02:00 PM | Lunch |
| 06:30 PM | 08:30 PM | Dinner at NUSS Scholar |
Scheduled Talks
Talk 1: Raising Expressivity in Verification and Synthesis Languages
Speaker: Alex Potanin
Abstract:
Synthetic Separation Logic (SSL) is a formalism that powers SuSLik, the state-of-the-art approach for the deductive synthesis of provably-correct programs in C-like languages that manipulate with heap-based linked data structures. Despite its expressivity, SSL suffers from two shortcomings that hinder its utility.
First, its main specification component, inductive predicates, only admits first-order definitions of data structure shapes, which leads to the proliferation of ``boiler-plate’’ predicates for specifying common patterns. Second, SSL requires concrete definitions of data structures to synthesise programs that manipulate them, which results in the need to change a specification for a synthesis task every time changes are introduced into the layout of the involved structures.
We propose to significantly lift the level of abstraction used in writing Separation Logic specifications for synthesis - both simplifying the approach and making the specifications more usable and easy to read and follow. We avoid the need to repetitively re-state low-level representation details throughout the specifications - allowing the reuse of different implementations of the same data structure by abstracting away the details of a specific layout used in memory. Our novel high-level front-end language called Pika takes SuSLik to the next level of expressivity and simplicity.
We implemented a layout-agnostic synthesiser from Pika to SuSLik enabling push-the-button synthesis of C programs with in-place memory updates, along with the accompanying full proofs that they meet Separation Logic-style specifications, from high-level specifications that resemble ordinary functional programs. Our experiments show that our tool can produce C code that is comparable in its performance characteristics and is sometimes faster than optimised Haskell.
Speaker bio:
Alex is an Associate Professor at the Australian National University. Alex is originally from Moscow, Russia with a background in Mathematics. He completed his PhD in programming languages in 2006 and took up a job as a Lecturer in Software Engineering at Victoria University of Wellington. During his studies, he took short breaks to work as a Visiting Researcher at Purdue University, and Software Engineer at two Wellington start-ups. He spent 2013 on a sabbatical at Carnegie Mellon University in Pittsburgh, PA, USA. He spent the winter of 2019/2020 on a sabbatical at Kyoto University in Japan. His web page is https://potanin.github.io .
Talk 2: Symbolic Execution of Datalog and its Application to Static Analysis Guided Program Repair
Speaker: Sergey Mechtaev
Abstract:
This talk introduces a new automated reasoning approach, symbolic execution of Datalog (SEDL). Datalog is a query language based on logic programming, which is used, among other applications, as a domain-specific language for defining program analysers. SEDL executes a Datalog query on a database of symbolic facts to compute dependencies between the input and the output of the query. We propose an efficient approach to implement SEDL on top of an existing Datalog solver using meta-programming.
We apply SEDL to static analysis guided program repair. We represent the buggy program that violates a static analysis property as Datalog facts, while the fixed-point equations of the static analysis are expressed through recursive Datalog rules. Then, the act of repairing the program is seen as modifying the corresponding Datalog facts. We execute SEDL to deduce the necessary alterations of the facts to meet the desired static analysis objectives.
We evaluated SEDL with existing third-party Datalog-based static analysers for detecting null pointer exceptions in Java programs, data leaks in Python notebooks, and four types of security vulnerabilities in Solidity smart contracts. We showed that SEDL-based program repair achieves a comparable or better performance than existing ad-hoc approaches designed to fix these classes of bugs, while also decoupling program analyses logic from program repair. It lays the foundation for developing a modular, general-purpose static program repair system that is able to address a wide range of defects.
Speaker bio:
Sergey Mechtaev is a Lecturer at University College London and a member of CREST center. Previously, he obtained a PhD degree from the National University of Singapore. His research interests include automated program repair, symbolic execution, and AI-based program analysis. Among other things, he developed Angelix, the first constraint-based program repair system that scaled to real-world programs, and founded program-repair.org, the largest online community of program repair researchers. For his research on automated program repair, he received ACM SIGSOFT Outstanding Dissertation Award in 2019 and ACM SIGSOFT Distinguished Paper Award in 2023. His web page is http://mechtaev.com.
Talk 3: XAI4FL: Enhancing Spectrum-Based Fault Localization with Explainable AI
Speaker: Ratnadira Widyasari
Abstract:
Manually finding the program unit (e.g., class, method, or statement) responsible for a fault is tedious and time-consuming. To mitigate this problem, many fault localization techniques have been proposed. A popular family of such techniques is spectrum-based fault localization (SBFL), which takes program execution traces (spectra) of failed and passed test cases as input and applies a ranking formula to compute a suspiciousness score for each program unit.
In this study, we propose a novel idea that first models the SBFL task as a classification problem of predicting whether a test case will fail or pass based on spectra information on program units. We subsequently apply eXplainable Artificial Intelligence (XAI) techniques to infer the local importance of each program unit to the prediction of each executed test case. Applying XAI to the failed test case, we retrieve information about which program statements within the test case that are considered the most important (i.e., have the biggest effect in making the test case failed). Such a design can automatically learn the unique contributions of failed test cases to the suspiciousness of a program unit by learning the different and collaborative contributions of program units to each test case’s executed result.
Speaker bio:
Ratnadira Widyasari is a PhD Candidate in Computer Science at the SMU School of Computing and Information Systems, supervised by Prof. David LO. Her main research interests are in the topic of artificial intelligence for software engineering, software debugging, and explainable artificial intelligence.
Talk 4: Datalog Repair guided by CTL Properties
Speaker: Yahui Song
Abstract:
Temporal logic properties can be cast as nested fixed point properties for a large class of temporal logic properties - specifically in alternation-free modal mu-calculus. This would cover well-known logic, such as the branching time logic called Computation tree logic (CTL). Any nested fixed point property in temporal logic can be encoded as a predicate in a stratified Datalog program. The least fixed point semantics of Datalog allows for a straightforward encoding of a least fixed point property, such as reachability properties. The greatest fixed point properties can be captured as a negation of the least fixed property. Thus, arbitrary nesting of least and greatest fixed point properties - can be cast as a predicate in a stratified Datalog program. Recently, we have completed the work on Datalog analysis guided repair. The central intuition is that Datalog is a suitable encoding for static program analyzers, which often capture a least fixed point computation. Thus, bugs discovered by static analysis - can be fixed by a surgery of the facts in the Datalog program encoding the analysis. In the proposed work, we suggest taking our idea of analysis-driven repair to repair temporal bugs. This requires taking our approach forward from Datalog programs to stratified Datalog programs. In that case, we can fix errors that violate a given temporal logic property, which may be encoded as a stratified Datalog program. The approach can be used to fix violations of temporal properties in real-life protocol implementations, such as the LTLfuzzer dataset.
Speaker bio:
Yahui Song has been working on automated temporal verification for several domains, including reactive Systems, time-critical systems, and algebraic effects/handlers. Her recent research focuses and interests are temporal-property guided repair, formal verification, and logic.
Talk 5: Mostly Automated Proof Repair for Verified Libraries
Speaker: Kiran Gopinathan
Abstract:
The cost of maintaining formally specified and verified software is widely considered prohibitively high due to the need to constantly keep code and the proofs of its correctness in sync—the problem known as proof repair. One of the main challenges in automated proof repair for evolving code is to infer invariants for a new version of a once verified program that are strong enough to establish its full functional correctness.
In this work, we present the first proof repair methodology for higher-order imperative functions, whose initial versions were verified in the Coq proof assistant and whose specifications remained unchanged. Our proof repair procedure is based on the combination of dynamic program alignment, enumerative invariant synthesis, and a novel technique for efficiently pruning the space of invariant candidates, dubbed proof-driven testing, enabled by the constructive nature of Coq’s proof certificates.
We have implemented our approach in a mostly-automated proof repair tool called Sisyphus. Given an OCaml function verified in Coq and its unverified new version, Sisyphus produces a Coq proof for the new version, discharging most of the new proof goals automatically and suggesting high-confidence obligations for the programmer to prove for the cases when automation fails. We have evaluated Sisyphus on 10 ubiquitous OCaml functions taken from popular libraries, that manipulate arrays and mutable data structures, considering their verified original and unverified evolved versions. Sisyphus has managed to repair proofs for all those functions, suggesting correct invariants and generating a small number of easy-to-prove residual obligations.
Speaker bio:
Kiran Gopinathan is a fifth-year PhD candidate at the School of Computing at NUS advised by Ilya Sergey in VERSE Lab. His research focuses on developing newer and better tools for the maintenance and automation of formal verification—the process of using computers to construct mathematical proofs about the software correctness—and covers a broad range of techniques, such as proof repair, invariant inference or automated verification. Notable highlights of his work include: producing the first formally verified proof of the probabilistic properties of the Bloom Filter data structure; inventing proof-driven testing, a novel technique that exploits fundamental mathematical truths (the Curry-Howard correspondence) and enables repairing the proofs of real-world programs. More information at https://www.gopiandcode.uk.
Talk 6: Evaluating Pre-trained Language Models for Repairing API Misuses
Speaker: Ting Zhang
Abstract:
API misuses often lead to software bugs, crashes, and vulnerabilities. While several API misuse detectors have been proposed, there are no automatic repair tools specifically designed for this purpose. In a recent study, test-suite-based automatic program repair (APR) tools were found to be ineffective in repairing API misuses. Still, since the study focused on non-learning-aided APR tools, it remains unknown whether learning-aided APR tools are capable of fixing API misuses. In recent years, pre-trained language models (PLMs) have succeeded greatly in many natural language processing tasks. There is a rising interest in applying PLMs to APR. However, there has not been any study that investigates the effectiveness of PLMs in repairing API misuse.
To fill this gap, we conduct a comprehensive empirical study on 11 learning-aided APR tools, which include 9 of the state-of-the-art general-purpose PLMs and two APR tools. We evaluate these models with an API-misuse repair dataset, consisting of two variants. Our results show that PLMs perform better than the studied APR tools in repairing API misuses. Among the 9 pre-trained models tested, CodeT5 is the best performer in terms of the exact match. We also offer insights and potential exploration directions for future research.
Speaker bio:
ZHANG, Ting is a Ph.D. candidate at SMU SCIS, supervised by Prof. David Lo and Prof. Lingxiao Jiang. Her research focuses on automatic software bug management, from detecting duplicate bug reports to repairing API misuse bugs. More info available: https://happygirlzt.com/academic.
Talk 7: Intelligent Tutoring for Programming Education
Speaker: Zhiyu Fan
Abstract:
The increasing number of CS students pushes lecturers and tutors of first-year programming courses to their limits. Existing systems that handle automated grading primarily focus on the automation of test case executions in the context of programming assignments. However, they cannot provide customized feedback about the students’ errors, and hence, cannot replace the help of tutors. Based on the research advances in recent years specifically in automated program repair and synthesis, we have built an intelligent tutoring system that has the capability of providing automated feedback. Furthermore, we designed a Software Engineering course that guides third-year undergraduate students in incrementally developing such a system over several years. Each year, students will make contributions that improve the current implementation, while at the same time, we can deploy the current system for usage by first year students for learning programming. In this seminar, Zhiyu will discuss the throughout effort and experience on building an intelligent tutoring system which is powered by automated repair and its relevant techniques. Beyond that, he will also talk about a new way of auto-grading for CS-1 programming assignment.
Speaker bio:
Zhiyu is a Ph.D. candidate in the School of Computing at the National University of Singapore, advised by Prof. Abhik Roychoudhury. His research interests lies in the areas of automated program repair, large language models, with a focus on intelligent tutoring for programming education.
Guests
We will have Alex Potanin, Sergey Mechtaev and David Lo (as well as two of David’s affiliates, Ratnadira and Ting) as guests.
Contact
For any questions, please contact Andreea Costea.