Invited Speakers

Keynote Talks

  • Nikolaj Bjorner (Microsoft Research)

    • Z3 to the power of Azure and Azure to the power of Z3 (abstract)
    • Bio: Nikolaj Bjorner is a Principal Researcher at Microsoft Research, Redmond, working in the area of Automated Theorem Proving and Software Engineering. His current main line of work with Leonardo de Moura and Christoph Wintersteiger is around the state-of-the art theorem prover Z3, which is used as a foundation of several software engineering tools. Z3 received the 2015 ACM SIGPLAN Software System award and most influential tool paper in the first 20 years of TACAS in 2014, and test of time award at ETAPS 2018. Previously, he developed the DFSR, Distributed File System – Replication, and Remote Differential Compression protocols, RDC, part of Windows Server since 2005 and before that worked on distributed file sharing systems at a startup, and program synthesis and transformation systems at the Kestrel Institute. He received his Master’s and Ph.D. degrees in computer science from Stanford University, and spent the first few years of university at DTU and DIKU.

  • Corina Pasareanu (NASA Ames Research Center)

    • DeepSafe: A data-driven approach for assessing robustness of neural networks (abstract)
    • Bio: Corina Pasareanu is an Associate Research Professor with CyLab at Carnegie Mellon University, working at the Silicon Valley campus with NASA Ames Research Center. She is an ACM Distinguished Scientist, known for her influential research on software model checking, symbolic execution and assume-guarantee compositional verification, using abstraction and learning-based methods. She is the recipient of an ACM SIGSOFT Distinguished Paper Award in 2002, the ICSE 2010 Most Influential Paper Award, the 2010 ACM SIGSOFT Impact Paper Award and the ISSTA 2018 Retrospective Impact Paper Award. More information is available at her website: https://ti.arc.nasa.gov/profile/pcorina/.

  • Sanjit Seshia (University of California, Berkeley)

    • Towards verified artificial intelligence (abstract)
    • Bio: Sanjit A. Seshia is a Professor in the Department of Electrical Engineering and Computer Sciences at the University of California, Berkeley. He received an M.S. and Ph.D. in Computer Science from Carnegie Mellon University, and a B.Tech. in Computer Science and Engineering from the Indian Institute of Technology, Bombay. His research interests are in formal methods for dependable and secure computing, with a current focus on the areas of cyber-physical systems, computer security, and robotics. He has made pioneering contributions to the areas of satisfiability modulo theories (SMT), SMT-based verification, and inductive program synthesis. He is co-author of a widely-used textbook on embedded, cyber-physical systems and has led the development of technologies for cyber-physical systems education based on formal methods. His awards and honors include a Presidential Early Career Award for Scientists and Engineers (PECASE), an Alfred P. Sloan Research Fellowship, and the Frederick Emmons Terman Award for contributions to electrical engineering and computer science education. He is a Fellow of the IEEE.

Tutorials