Aarti Gupta

Princeton University

Automated Verification of Programs and Networks using SAT/SMT

Brief Bio

Aarti Gupta is a Professor in the Department of Computer Science at Princeton University. She received a PhD in Computer Science from Carnegie Mellon University. Her broad research interests are in the areas of formal verification of programs and systems, automatic decision procedures, and electronic design automation. She has served on the technical program committees of many leading conferences in these areas, and is currently serving on the Steering Committee of the CAV (Computer Aided Verification) Conference. She is an ACM Fellow.

Pramod Subramanyan

IIT Kanpur

Modeling and Verification of Security Properties of Hardware and Software Systems

Brief Bio

Pramod Subramanyan is an Assistant Professor in the Department of Computer Science and Engineering at the Indian Institute of Technology, Kanpur. His research addresses systems security concerns using formal methods. He obtained his Ph.D. from the Department of Electrical Engineering at Princeton University under the guidance of Prof. Sharad Malik. Prior to joining Princeton, Pramod obtained an M.Sc. (Engg.) degree from the Indian Institute of Science and a B.E. degree from the R. V. College of Engineering, Bangalore. Before entering academia for his doctoral studies, Pramod was a software engineer at National Instruments and a hardware design engineer at AMD.

Vijay Ganesh

University of Waterloo

SAT and SMT Solvers- A Foundational Perspective

Brief Bio

Dr. Vijay Ganesh is an associate professor at the University of Waterloo. Prior to joining Waterloo in 2012, he was a research scientist at MIT (2007-2012) and completed his PhD in computer science from Stanford University in 2007. Vijay's primary area of research is the theory and practice of automated mathematical reasoning algorithms aimed at software engineering, formal methods, security, and mathematics. In this context he has led the development of many SAT/SMT solvers, most notably, STP, Z3 string, MapleSAT, and MathCheck. He has also proved several decidability and complexity results in the context of first-order theories. He has won over 25 awards, honors, and medals to-date for his research, including an ACM Test of Time Award at CCS 2016, an Ontario Early Researcher Award 2016, two Google Faculty Research Awards in 2011 and 2013, and a Ten-Year Most Influential Paper citation at DATE 2008.