Distributed Collaborative Verification of Concurrent Software Systems
Funded by University College Dublin
Applied formal methods has turned a corner over the past few years. The semantics, specification, and verification communities now have a sufficient level of mathematical sophistication and adequate computational resources available such that automatic and interactive verification of software components written in modern programming languages like Java is possible. Unfortunately, the computational resources necessary to perform the verification of real world programs (as opposed to toy examples) are extreme, particularly with regard to the amount of memory used in the computations. While fund-raising for resources like personnel and travel has been moderately successful in recent years, funding equipment purchases is spartan. There is a dire need for distributed, collaborative computational resources---resources that are in a global common pool, usable by anyone performing large-scale program verification. The intention of this award is to kick-start the the construction of such a computational resource, known as the "Mobius Cluster". These computational resources will be made available transparently via the Mobius Program Verification Environment (PVE), the design and development of which UCD, led by Dr. Kiniry, is responsible.
This proposal's focus is kick-starting the construction of a distributed, collaborative computational cluster for Java program verification. The participants in this collaboration represent several of the major players in this domain, and each of them has the need for, and will have access to, the resources afforded by this award.
The Systems Research Group at the School of Computer Science and Informatics (CSI) at UCD, which Dr. Kiniry co-founded and co-leads, is recognized as a world-class research group in applied formal methods. Support of this effort will continue to raise the profile and quality perceptions of Computer Science researchers around the world of UCD. As a result of this award, UCD will become known as the "keystone" or "computation hub" of concurrent systems verification. Our intention is to kickstart funding of complementary computational resources at partner institutions (listed below).
Partners/Collaborators
INRIA Radboud Universiteit Nijmegen TLS Technologies Ludwig-Maximilian Universit at, Munich ETH Zurich Institute of Cybernetics, Tallinn University of Edinburgh Chalmers Technical University Imperial College, London University of Warsaw Trusted Logic France Telecom Universidad Politecnica de Madrid SAP AG Massachusetts Institute of Technology Iowa State University California Institute of Technology University of Iowa University of California, Santa Cruz Concordia University Kansas State University SRI International Stevens Institute of Technology
One or more research groups at each of the above Universities and companies will have need for, and access to, the resources afforded in this small equipment award. They will use these resources via the Mobius IVE, interactively and automatically performing verifications of concurrent Java components in a distributed, collaborative fashion.
To guarantee high-availability and maximum utility, this project needs two multiprocessor servers to bootstrap the "Mobius Cluster". As we need as much memory as possible in a commodity machine, purchasing multiple Apple Xserve nodes is the most cost-effective choice, as comparable machines from providers like Dell cost twice as much for a comparable configuration. We expect to wait for the new Intel-based Xserve machines to be released before making the purchase, thus budget costs above are only estimates based upon the cost of existing G5-based machines and our knowledge of Apple pricing schemes over the past decade.
The proposed system configuration is as follows:
- Xserve Node G5, 1x500GB Serial ATA, 16GB DDR400 ECC SDRAM - 8x2GB, Dual 2.3GHz PowerPC G5