HILT 2014             ACM logo - Advancing Computing as a Science & Profession

High Integrity Language Technology
ACM SIGAda’s Annual International Conference

Correctness via Compilation to Logic

Thomas Ball


Advances in automated theorem provers over the last decade have led to a renaissance in software tools that compile problems of correctness to problems over logic formula. In this talk, I will review progress in automated theorem provers, such as Z3 from Microsoft Research, and consider a variety of program correctness tools that build upon Z3, such as automated test generators, automated safety/termination checkers, as well as interactive functional verifiers. I'll then describe a number of new projects that make use of the "correctness via compilation to logic" approach, including the design of new programming languages, ensuring the security of data centers, and safely programming gesture recognizers such as Kinect.

Created on 14 October 2014;  website comments and corrections to ClydeRoby at ACM.Org