My main line of work is around the state-of-the-art SMT constraint solver Z3. Z3 was developed with Leonardo de Moura, Lev Nachmanson and Christoph Wintersteiger. Z3 is used for program verification, test case generation among several applications. The work around Z3 has received several awards. Karthick Jayaraman and I created the SecGuru tool that is used to validate firewalls and routing configurations for Microsoft Azure and George Varghese introduced me to many insights around network verification and algorithmics. Until 2006, I was in the Core File Systems group where I designed and implemented the core of DFS-R which is included as part of Windows Server 2003 R2, Sharing Folders and Meetings Space. I also designed some of the chunking utilities used in the remote differential compression protocol RDC. I was named as 2021 ACM Fellow.