jStar: making java verification practical

Software is unreliable. This is a serious problem for modern society. We are in contact with software everyday, but this software often contains critical bugs. Currently, operating systems are susceptible to viruses, and commercial software packages are sold with disclaimers not guarantees. To address this, we need to develop practical verfication methods for real-world programming languages. This is about giving a mathematical specification of what the software should do, and guaranteeing the implementation meets this specification. This proposal focusses on verifying object-oriented programs. The most prominent approaches to object-oriented verification, Boogie and ESC, suffer two major problems. First, their specifications are verbose, in fact sometimes longer than the code. The reason for this is that they only support limited modularity and require redundant annotations, like many loop invariants. Secondly, their specifications are weak since they cannot express functional correctness. The problem here is that although the mantra ``say less to do more'' is alluring in the context of software specification, unfortunately, it does not work for realistic examples, or even just common design patterns. Here, we propose the following novel combination of ideas, which make practical verification for Java possible: * A separation Logic based specification language for OO giving powerful modularity. * Automatic theorem proving for substructural logics which integrates with existing theorem provers for classical logic, e.g. SMT solvers; HOL; etc. * A proof theoretic approach to abstract interpretation, which allows redundant annotations to be inferred and boost abstract interpretation to coverage of full functional correctness properties. Furthermore, we propose that all these concepts can be realised together in a unified prover/abstracter architecture.