Formal Methods (FM) are mathematical and logical-based methods and systems that can improve the trustworthiness of software systems. This tutorial starts with an overview of various formal methods and then focuses on introducing state-based and event-based formal modeling and reasoning techniques with practical examples. In particular, it covers:
• Formal Specification Language Z (developed at Oxford University)
• CSP Communicating Sequential Process (developed at Oxford University)
• Model Checking: PAT Concurrent and Real-time Systems (developed at NUS)

Machine Learning (ML) systems have become increasingly integral to safety and security-critical applications. However, a significant challenge arises from the inherent lack of explainability and verifiability in many ML systems. Our recent research has focused on addressing this issue through the development of a Trusted ML system. The initial segment of this presentation delves into the "Silas: Trusted Machine Learning System," an initiative that seamlessly integrates open machine learning with formal automated reasoning (www.depintel.com). In the subsequent part of the discussion, we explore the reasoning capabilities of ChatGPT+ (encompassing ChatGPT3.5 and GPT4). Specifically, we discuss the approaches to link ChatGPT with formal reasoning techniques, aiming to establish a framework for trusted decision-making.

Dr. Jin-Song Dong is a professor and deputy head of the Computer Science Department at the National University of Singapore. His research is in the areas of formal methods, safety and security systems, probabilistic reasoning, sports analytics, and trusted machine learning. He co-founded the commercialized PAT verification system which has attracted thousands of registered users from 1000+ organizations in 150 countries. He also co-founded “Silas: Trusted Machine Learning” (www.depintel.com). He received several best paper awards including the ACM SIGSOFT Distinguished Paper Award. Jin Song has been on the editorial board of ACM Transaction on Software Engineering and Methodology, Formal Aspects of Computing, and Innovations in Systems and Software Engineering, A NASA Journal. He has successfully supervised 28 PhD students and many of them have become tenured faculty members in leading universities around the world. He is a Fellow of the Institute of Engineers Australia. In his spare time, he developed Markov Decision Process (MDP) models for tennis strategy analysis in PAT and helped professional players in their pre-match analysis (beating the world's best). Jin Song is also a Grand Slam junior coach and enjoys coaching tennis to his 3 kids who all reached the #1 Singapore/Australia national junior ranking.

Cloud computing has become a very popular paradigm for data processing and storage of modern applications. However, the cloud may not be the best place for processing applications which require low response times. This is due to the significant physical distance between the cloud data center and the data generation sources. Edge computing involves bringing the cloud closer to the users, and offers lower response times to modern applications. In this tutorial, we will go through the basic concepts of edge computing, discuss scheduling and resource allocation at the edge, and discuss various modern day applications that can benefit from edge computing, for example - smart vehicles, agriculture, and medicine.

Nitin Auluck received the B. E. degree from PDA College of Engineering, Gulbarga University in 1998 and PhD degree from the University of Cincinnati, USA in 2004. He was an assistant professor in the Department of Computer Science, Quincy University, Quincy, USA from 2004 to 2010. He has been with the CSE Department at IIT Ropar since 2010, first as assistant professor, and currently, as an associate professor. His research interests include fog computing, real-time systems, and parallel and distributed systems. He has collaborations with universities in the UK, Canada, Australia, and Singapore. He is an editor of Wiley’s CCPE journal, and is involved in the organisation of various conferences, such as IEEE CCGRID, IEEE EDGE.