Keynote I  VsusFL: Variable-suspiciousness-based Fault Localization for novice programs

Automatically localizing faulty statements is a desired feature for effective learning programming. Most of the existing automated fault localization techniques are developed and evaluated on commercial or well-known open-source projects, which performed poorly on novice programs. In this paper, we propose a novel fault localization technique VsusFL (Variable-suspiciousness-based Fault Localization) for novice programs. VsusFL is inspired by simulating the manual program debugging process and takes advantage of variable value sequences. VsusFL can trace variable value changes, determine whether the intermediate state of the variables is correct, and report the potential faulty statements for novice programs. This paper presents the implementation of VsusFL and conducts empirical studies on 422 real faulty novice programs. Experimental results show that VsusFL performs much better than Grace, ANGELINA, VSBFL, Spectrum-Based Fault Localization (SBFL), and Variable-based Fault Localization (VFL) in terms of TOP-1, TOP-3, and TOP-5 metrics. Specifically, VsusFL can localize 90%, 35% and 9% more faulty statements than the best-performing baseline Grace. Moreover, We analyze the correlation between VsusFL and other techniques and find a weak correlation since they perform well on different programs, indicating the potential to further enhance fault localization performance through strategic integration of VsusFL with other methods.

Keynote II  Flexible Formal Modelling with Stepwise Refinement 

Abstract: Software-based systems are increasingly diverse and complex, while they often have safety requirements to satisfy. Formal models are useful in this situation because they help us rigorously understand the properties of the target system and carry out reasoning on it. However, there are two challenges for constructing formal models: the target system can be complex, and the document of the target system often includes parts with uncertainty.

In this talk, we first introduce Event-B, a method effective for constructing "correct-by-construction" formal models. It supports a stepwise refinement approach based on theorem proving; we repeat evolving an abstract model into a concrete version and checking the consistency between them until we obtain a model concrete enough. Then, we describe our methods for strengthening the approach from the viewpoint of software engineering. They include a method for increasing the explainability and reusability of a given model through automatic abstraction, a method for design space exploration by generating different chains of refinements for a given model, and a method for repairing a given model by generating missing constraints required for safety. In addition, as a case study of applying the stepwise refinement approach to advanced software systems, we present our work on modelling an automated vehicle controller that is guaranteed to achieve a certain complex goal while keeping safety, even if the controller has a black-box module (e.g. machine learning component). The talk concludes with discussions on the core concept common in our studies, that is, supporting software development based on the engineer's rigorous understanding of the target system and its correctness.