Type based software verification

随着互联网的发展和计算机在我们生活中的广泛使用，计算机系统的安全性和可靠性已经具有了新的意义。尽管Java的速度相对较慢，而且它使用了一种被认为效率低下的内存管理技术(垃圾收集器)，但它最近的成功表明，人们的注意力已经从性能转移到了健壮性和开发的简易性上。Java的健壮性的很大一部分可以直接归因于使用强静态类型化，这是目前软件开发中使用的最流行的正式方法。然而，仍然有许多情况下Java的类型系统不够好，要么是因为它太强大，阻碍了程序员编写他想要的代码，要么相反，因为它太弱，不能表达所需的正确性属性。你仍然可以使用诸如扩展静态检查、模型检查、Hoare逻辑中的完全证明等工具来机械地验证感兴趣的正确性属性。但从只使用类型注释到开发模型甚至整个正确性证明的转换是非常大的一步，需要大量的工作和专业知识。因此，这种好处很少被认为值得努力，将这些技术留给小众。我的研究计划旨在采取另一种方法，基于使类型系统更强大，因此，可以用它来表示和验证任意属性，从而可以无缝地涵盖从传统的简单类型注释到任意更复杂的正确性属性的范围。这将使编写和维护健壮的软件变得更容易，其中健壮性被机械地验证。正规的方法彻底改变了硬件的设计方式，计算机软件的世界正在经历类似的变革；引领它可以给加拿大的软件业带来巨大的战略利益。另一种评估这种发展影响的方式是看我们整个社会目前对非常简单的计算机病毒的脆弱性。正式验证每一个程序正在成为一种必要，就像验证每一座桥的建设计划的合理性一样。

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.