Philippe Suter Defends his Doctoral Dissertation

December 2012. Philippe Suter defended his doctoral dissertation entitled "Programming with Specifications", demonstrating, in an accessible and convincing way, the benefits of developing software specifications and using them for a range of software development tasks. These include run-time monitoring, verification, rapid prototyping through executing specifications, and synthesis of code from specifications.

The algorithmic basis of Philippe's results are new techniques he developed to solve expressive constraints involving recursive functions. The results are backed up by a verification tool, Leon, that provides automated check that eliminate program errors in all possible executions, as well as constraint solvers that enhance automated theorem proving capabilities and integrate constraint programming into Scala. The results have also been adopted by others working in industry and academia, where they have been shown to provide useful foundation of more profound compiler checks.