Designed for Update

Abstract: Today, the functionality as well as economical value of industrial systems and products, such as cars, air planes, and medical equipment, is defined and realized by software as embedded systems. Dynamical software updates are critical for security updates, new features, and customization, but are not supported for today's safety-critical systems, since we lack techniques to guarantee that the updated system remains safe. In this talk, I will present a model for embedded systems with deterministic timing and functional behaviours. The model provides a foundation for a new design paradigm for building embedded systems which can be updated on demand dynamically, safely, and efficiently over their operational life-time.

Wang Yi, Chair professor, Uppsala University. Ph.D., Chalmers (1991). Fellow of IEEE (2014). Member of Academia Europaea (London, UK, 2015). Fellow of Royal Society of Sciences (Uppsala, Sweden, 2017). CAV Award (2013). Outstanding Technical Achievement and Leadership Award (IEEE Technical Committee on Real-Time Systems, 2019). ERC Advanced Grantee (EU, 2019). ACM SigBed Vice Chair. Steering Committee Member of EMSOFT and ESWEEK.

The Good, the Bad and the Ugly: a Practitioner's Perspective on Formal Methods

Abstract: Formal methods have recently gained a resurgent interest in industry due to the the increasing demand of high-assurance software systems. This can be evidenced by the increasing investment on formal methods in big companies like Microsoft, Amazon and Huawei. In this talk, I will share my experiences in applying formal methods in industry. Specifically, I will describe the efforts in applying formal methods in the design and implementation of critical software systems like operating systems, file systems and distributed system protocols. Based on these, I will further describe the experiences and lessons learned in applying formal methods at a large scale setting, and discuss possible challenges and opportunities in fostering better synergy between academia and industry.

Haibo Chen, Professor at School of Software, Shanghai Jiao Tong University, where he co-founds and leads the Institute of Parallel and Distributed Systems (IPADS) (http://ipads.se.sjtu.edu.cn). Haibo's main research interests are building scalable and dependable systems software, by leveraging cross-layering approaches spanning computer hardware, system virtualization, operating systems as well as formal methods. His research work has been widely adopted by open-source community like Linux and Open JDK as well as commercial products deployed over hundreds of billions of devices, resulted in publications in top systems conference like SOSP/OSDI, and won several best papers from EuroSys, APSys and ICPP. He currently chairs ACM SIGOPS ChinaSys, serves on the program committees of SOSP 2019, CCS 2019, IEEE S&P 2020, ASPLOS 2020 and the editorial boards of ACM Transactions on Storage and Communications of the ACM.

The Rise of Model Counting: A Child of SAT Revolution

Abstract: The paradigmatic NP-complete problem of Boolean satisfiability (SAT) is a central problem in Computer Science. The past 20 years have witnessed a SAT revolution with the development of conflict-driven clause-learning (CDCL) SAT solvers. Such solvers combine a classical backtracking search with a rich set of effective heuristics. While 20 years ago SAT solvers were able to solve instances with at most a few hundred variables, modern SAT solvers solve instances with up to millions of variables in a reasonable time. The SAT revolution opens up opportunities to design practical algorithms with rigorous guarantees for problems in complexity classes beyond NP by replacing a NP oracle with a SAT Solver. In this talk, we will discuss how we use SAT revolution to design practical algorithms for one of the fundamental problems in formal methods and artificial intelligence: model counting. Model counting is a fundamental computational problem with applications in diverse areas spanning neural network verification, reliability estimation, explainable AI, probabilistic inference, security vulnerability analysis, and the like. While counting has been studied extensively by theoreticians for the past three decades. Yet, in spite of this extensive study, it has been extremely difficult to reduce this theory to practice. We examine how the process of revisiting and refining the theory to leverage the SAT revolution has led to the development of the the first scalable framework for model counting: ApproxMC. ApproxMC can handle industrial-scale problem instances involving hundreds of thousands of variables, while providing provably strong approximation guarantees.

Kuldeep Meel, Sung Kah Kay Assistant Professor of Computer Science in School of Computing at the National University of Singapore. He is an affiliate of the Institute of Data Science and holds a long-term visiting faculty position at IIT Bombay. His research interests lie at the intersection of Artificial Intelligence and Formal Methods. He is the recipient of 2019 NRF Fellowship for AI. His work received the 2018 Ralph Budd Award for Best Ph.D. Thesis in Engineering, 2014 Outstanding Masters Thesis Award from Vienna Center of Logic and Algorithms and Best Student Paper Award at CP 2015. He received the IBM Ph.D. Fellowship and the 2016-17 Lodieska Stockbridge Vaughn Fellowship for his work on constrained sampling and counting. He received his Ph.D. (2017) and M.S. (2014) degree in Computer Science from Rice University. He holds B. Tech. (with Honors) degree (2012) in Computer Science and Engineering from Indian Institute of Technology, Bombay.