Tutorial Presenters

Jakob Nordström

University of Copenhagen, Denmark

Pseudo-Boolean Solving and Optimization

Brief Bio

Jakob Nordström is a professor at the Department of Computer Science at the University of Copenhagen, Denmark, and also has a part-time affiliation with the the Department of Computer Science at Lund University. His research interests lie in understanding combinatorial optimization problems -- to prove formally, on the one hand, that many such problems are beyond the reach of current algorithmic techniques, but also, on the other hand, to develop new algorithms that have the potential to go significantly beyond the current state of the art. Recently, he has also been working on harnessing complexity theory to produce certificates that algorithms are actually computing correct results. Prior to moving to Copenhagen and Lund, Jakob worked at KTH Royal Institute of Technology as an assistant professor and then associate professor during the years 2011-2019. During 2008-2010 he was a postdoc at the Computer Science and Artificial Intelligence Laboratory at the Massachusetts Institute of Technology hosted by Madhu Sudan. Before that he was a PhD student of Johan Håstad in the Theory Group at KTH, where he defended his PhD thesis in May 2008.

Sanjit A. Seshia

University of California, Berkeley

UCLID5’s Elements: Formal Modeling, Verification, Synthesis, and Learning

Brief Bio

Sanjit A. Seshia is the Cadence Founders Chair 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, machine learning, 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, the Frederick Emmons Terman Award for contributions to electrical engineering and computer science education, the Donald O. Pederson Best Paper Award for the IEEE Transactions on CAD, the IEEE Technical Committee on Cyber-Physical Systems (TCCPS) Mid-Career Award, and the Computer-Aided Verification (CAV) Award for pioneering contributions to the foundations of SMT solving. He is a Fellow of the ACM and the IEEE.