Abstract: Analyzing software reliability requires a formal specification of the intended behavior of the software under analysis. Unfortunately, software many times lacks such specifications, and thus inferring them from existing software elements such as source code, code comments, or program executions, is important, as it can facilitate more effective software analysis. In this talk I will describe some current attempts to infer specifications at the level of source code, in the form of program assertions. I will present techniques that are able to produce program assertions based on three main tasks: (i) executing the program under analysis to obtain samples of the current program behavior, (ii) applying program/state mutation to get samples that deviate from the program behavior, and (iii) employing some generation approach to produce assertions capturing the “valid” program executions, while rejecting the “deviating” ones. The techniques differ on how these three components are realized and composed, and in particular, in the approach used for assertion generation; evolutionary search and fuzzing are two specific mechanisms that have been recently explored for this latter task. Finally, I will discuss some approaches related to specification inference, and current lines of research in this area.

Nazareno Aguirre is an Associate Professor at the University of Rio Cuarto, Argentina, and a Research Scientist at Argentina's National Council for Scientific and Technical Research (CONICET). His current research interests relate to the problem of guaranteeing software correctness and helping produce quality software, mostly via techniques for program specification, automated testing, and program verification, with formal underpinnings. Nazareno Aguirre's research has been published in top-tier software engineering conferences and journals. He regularly serves on program committees of software engineering conferences and is currently an Associate Editor of IEEE Transactions on Software Engineering.

Abstract: Sports analytics encompasses the utilization of data science, artificial intelligence (AI), psychology, and Internet of Things (IoT) devices to enhance sports performance, strategy, and decision-making. This process involves the collection, processing, and interpretation of cloud-based data from a variety of sources, such as video recordings, performance metrics, and scouting reports. The resulting insights aid in evaluating player and team performance, preventing injuries, and supporting coaches and team managers in making well-informed decisions to optimize resources and achieve superior outcomes. One widely recognized formal method, Probabilistic Model Checking (PMC), has traditionally been employed in reliability analysis for safety-critical systems. For instance, the reliability of an aircraft can be determined by evaluating the reliability of its individual components, including the engine, wings, and sensors. We apply PMC to a new application domain: Sports Strategy Analytics. As an example, the reliability (winning percentage) of a tennis player can be ascertained from the reliability (success rate) of their specific sub-skill sets (e.g., serve, forehand, backhand, etc). In this presentation, we will discuss our recent research work, which involves the application of PMC, machine learning, and computer vision to sports analytics. At the end of the presentation, we will present the vision of a new international sports analytics conference series (https://formal-analysis.com/isace/2023/).

Jin Song Dong is a professor and deputy head of the Computer Science Department at the National University of Singapore. His research interests include formal methods, safety and security systems, probabilistic reasoning, sports analytics, and trusted machine learning. He co-founded the commercialized PAT verification system with J. Sun and Y. Liu, which has garnered thousands of registered users from over 150 countries. Jin Song also co-founded the commercialized trusted machine learning system Silas (www.depintel.com) with Z. Hou and H. Bride. He has received numerous best paper awards, including the ACM SIGSOFT ICSE Distinguished Paper Award. He served on the editorial board of ACM Transactions on Software Engineering and Methodology and ACM Formal Aspects of Computing. He has successfully supervised 28 PhD students, many of whom have become tenured faculty members at leading universities worldwide. He is also a Fellow of the Institute of Engineers Australia. In his leisure time, Jin Song developed Markov Decision Process (MDP) models for tennis strategy analysis using PAT, assisting professional players with pre-match analysis (outperforming the world's best). He is a Junior Grand Slam coach and coached tennis to his three children, all of whom have reached the #1 national junior ranking in Singapore/Australia. Two of his children have earned NCAA Division 1 full scholarship, while his second son, Chen Dong, played #1 singles for Australia in the Junior Davis Cup World Final and participated in both the Australian Open and US Open Junior Grand Slams.

Abstract: FM-related techniques are very helpful to ensure the quality of software. For instance, the model checking technique has been successfully applied in hardware/software verification and it becomes the key element for EDA tool chains. In this talk, I will share the experiences of developing the industrial-strength tools for modeling, testing and verification from the formal methods perspective. We will show how to find the real problems about testing and verification from the industry and also show how the formal methods can guide to solve these problems by developing tools. We will illustrate our experiences and insights by three interesting tools under development. The first one is a formal modeling and verification tool for the formal verification of Interlock system of the train, that is key part of signal systems in railway. The second one is a testing tool for embedded systems, where the symbolic execution technique plays an important role. The last one is a new model checking solver for hardware verification, and its performance is tuned effectively by the new observations on the search process in the state space. These tools are successfully applied in our industry partners and their effectiveness is also proved by large scale examples. Last but not least, we will also share the lessons we have learned during the tool development.

Geguang Pu is a full professor of software engineering at East China Normal University. His research interests span the areas of software modeling, automated testing, and model checking. A common thread in Geguang's research is improving software reliability and trustworthiness by developing FM-based tools. Geguang joined East China Normal Universityin 2005 as an assistant professor and prior to that, he studied for Ph. D in Peking University. In July 2018, he was appointed as CEO of Shanghai Trusted Industrial Control Platform Co., Ltd for the technique transfer, where he is leading an effective engineering teams to develop the tool chains for software modeling, testing and verification, and these tools are used by more than 100 institutes/companies for structing more reliable software systems.