Omnibus is a project I have been working on for the last 5 years and aims to support the development of reliable software by typical software developers. It is built around the new Omnibus language which is designed to be both amenable to formal analysis and familiar to Java programmers. The language is supported by an integrated development environment providing a range of assertion-based verification tools from run-time checking or extended static checking of lightweight assertion annotations to full formal verification with respect to heavyweight specifications. The Omnibus project has it's own home page. Also see the dissertation and Joose project for earlier pieces of work on the project.

Papers

"Push-button tools for application developers, Full formal verification for component vendors"
- (Departmental Technical Report to be published early 2007)
- Sets out my case for the use of the push-button approaches of run-time assertion checking with test harnasses and extended static checking for application-specific code and full formal verification for reusable components.
"Omnibus Verification Policies: A flexible, configurable approach to assertion-based software verification"
- (SEFM 2005 at Koblenz University in September 2005)
- Explains the benefits of using the different assertion-based verification approaches together, present a set of guidelines to avoid potential conflicts and give an overview of how the Omnibus IDE provides support for the full range of assertion-based verification approaches within a single tool.
"Omnibus: A clean language and supporting tool for integrating different assertion-based verification techniques"
- (REFT 2005, part of FM 2005 at University of Newcastle upon Tyne in July 2005)
- Gives an overview of the Omnibus project, explaining how it (1) uses a mathematically clean language to reduce annotation burdens and increase automation within the theorem proving process and (2) allows different assertion-based verification approaches to be used together in different parts of a single software project.

Reports

"Assertion-based Object-Oriented techniques for Reliable Software Development and Safe Software Component Reuse"
- (Submitted to Department of Computing Science and Mathematics department at University of Stirling in July 2004)
- Presents the results of the first year of my Ph.D. investigating the use of assertion-based Object-Oriented techniques to produce reliable software and enable software components to be reused safely

Omnibus

Papers

Reports

Related pages