Type based software verification

点击翻译按钮获取中文摘要

Security and reliability of computer systems has taken a new significance with the development of the Internet and more generally with the use of computers in all parts of our lives.  The recent success of Java despite its relative slowness and its use of a memory management technique reputed inefficient (a garbage collector), shows how much the focus has shifted away from performance to robustness and ease of development.A large part of the robustness of Java can be attributed directly to the use of strong static typing, which is by far the most popular formal method in use today in software development.  Yet, there are still many cases where Java's type system is not good enough, either because is is too strong and prevents the programmer from writing the code he wants, or on the contrary because it is too weak to express the desired correctness property.You can still verify mechanically the correctness property of interest, using tools such as: extended static checking, model checking, full proof in Hoare logic.  But the switch from using just type annotations to developing a model or even a whole correctness proof is a very big step which requires a lot of work and expertise.  The benefit is thus rarely considered worth the effort, leaving such techniques to niches.My research program aims to take another approach based on making the type system more powerful, so that arbitrary properties can be expressed and verified with it, making it possible to seamlessly cover the range from traditional simple type annotations to arbitrarily more complex correctness properties.  This will make it easier to write and maintain robust software, where the robustness is mechanically verified.Formal methods have revolutionized the way hardware is designed, and the world of computer software is going through a similar transformation; leading it can bring large strategic benefits to the software industry in Canada.  Another way to evaluate the impact of such a development is to look at the current vulnerability of our society as a whole to very simple computer viruses.  Formally verifying every program is becoming a necessity, just as much as verifying the soundness of the construction plans of every bridge.