Omnibus: a clean language and supporting tool for integrating different assertion-based verification techniques. Omnibus is a new system for the development of reliable ObjectOriented software. It includes a clean language that is superficially similar to Java but removes aspects that particularly complicate verification. Integrated support is provided for run-time assertion checking, extended static checking and full formal verification. The language is supported by a prototype IDE with a type checker, Java code generator, HTML documentation generator and a range of verifiers. This paper presents the case for Omnibus, gives an overview of the language and tools and discusses its relationship to dependable systems development.
Keywords for this software
References in zbMATH (referenced in 3 articles )
Showing results 1 to 3 of 3.
- James, Perry R.; Chalin, Patrice: Faster and more complete extended static checking for the Java modeling language (2010)
- Wilson, Thomas; Maharaj, Savi; Clark, Robert G.: Flexible and configurable verification policies with Omnibus (2008)
- Leavens, Gary T.; Leino, K.Rustan M.; Müller, Peter: Specification and verification challenges for sequential object-oriented programs (2007)