Prof. Adam Chlipala

Chlipala's research addresses the software development process, applying formal logic to prove programs are correct using a computer proof assistant. He aims to reduce the human cost of program verification so that it may one day become a standard part of software development. This research could ultimately increase the reliability and security of software. He received an National Science Foundation CAREER Award, and he has written a book that is highly regarded and widely used within the program verification community. He has also developed a new class on interactive theorem proving.