Skip header navigation
×

Technical Report

Push-Button Tools for Application Developers, Full Formal Verification for Component Vendors

Citation
Wilson T, Maharaj S & Clark R (2007) Push-Button Tools for Application Developers, Full Formal Verification for Component Vendors. Technical Report CSM, 167. Department of Computing Science and Mathematics, University of Stirling.

Abstract
Software developers have varying abilities and develop software with differing reliability requirements. Sometimes reliability is critical and the developers have the mathematical capabilities to perform interactive theorem proving but this is not usually the case. We believe that most software developers need easy to use tools such as run-time assertion checkers and extended static checkers that can help them produce more reliable application-specific code cheaply. However, these lightweight approaches are not sufficient to allow the safe reuse of software components. To safely reuse software components we need comprehensive descriptions and assurances of correctness. These requirements can be provided for by full formal verification with the additional costs justified by the economies of scale. Our Omnibus verification tool provides integrated support for all these different types of verification. This paper illustrates these concepts through a sorting implementation.

Keywords
Assertion-based verification; Run-time assertion checking; Extended Static Checking; Formal verification; Software Component Reuse; Tool integration; Computer programs Verification; Omnibus (Computer program language)

StatusPublished
Author(s)Wilson, Thomas; Maharaj, Savi; Clark, Robert
Title of seriesTechnical Report CSM
Number in series167
Publication date31/08/2007
URLhttp://hdl.handle.net/1893/1604
PublisherDepartment of Computing Science and Mathematics, University of Stirling
Scroll back to the top