Abstract: Concurrent systems may execute one of an exponential number of paths resulting in a large number of potential states. This often makes it infeasible to consider all possible behaviors of a system. Scalable formal methods, while not guaranteeing correctness, can provide greater confidence about properties of a system. The talk will describe three such methods: Statistical Model Checking (SMC), Euclidean Model Checking (EMC), and Predictive Runtime Verification (PRV). SMC uses statistical methods to check properties expressed in a probabilistic temporal logic. EMC uses linear algebra to check aggregate properties by reasoning about the evolution of probability distributions. PRV automatically generates runtime monitors to verify properties of distributed programs and predict potential violations in future executions. Finally, some applications and limitations of these techniques will be discussed, providing a perspective on open research problems.

Short Bio: Dr. Gul Agha is Professor Emeritus of Computer Science at the University of Illinois at Urbana-Champaign and Interim CEO of Embedor Technologies. He served as Editor-in-Chief of IEEE Concurrency: Parallel, Distributed and Mobile Computing, and of ACM Computing Surveys. Dr. Agha is a Fellow of the ACM and of the IEEE, and received the 2019 ACM Sigsoft Impact Paper Award. Dr. Agha is best known for his formalization of the Actor model, used in languages and frameworks such as Erlang, Scala/Akka, and Orleans, and to develop scalable applications such as Twitter, LinkedIn, and Facebook Chat. Dr. Agha's research contributions include development of Statistical Model Checking, which has applications in biological systems and cyberphysical systems among others; Concolic Testing for programs with memory and concurrency, a method incorporated in industrial software testing tools such as KLEE, Microsoft SAGE, and S2E; Euclidean model checking for reasoning about the evolution of probability distributions and for synthesizing controllers; the application of computational learning to program verification; logical methods for automated decentralized, predictive runtime verification; and distributed algorithms for wireless sensor networks(WSNs). Dr. Agha co-founded Embedor Technologies which is applying WSNs to continually monitor the structural health of bridges, buildings and large machinery. For example, Embedor's technology was used to monitor the world largest Ferris wheel during construction, and will be used to continuously monitor it during operation.