Proofs as a substrate for tool integration supporting high-confidence embedded software

ManuscriptAs the size and complexity of software in safety-critical embedded systems increases, the ability of programmers to deliver these systems in a timely fashion decreases. Specific difficulties are that embedded software must interact with the physical world in real time and that it must make efficient use of resources such as memory and energy. Our work is driven by the observation that the fundamental scarcity limiting our ability to create high-confidence embedded software is human developer time. A practical and incremental solution to this problem is tool-rich software development where software tools such as verifiers, static bug finders, stub generators, and optimizing compilers automate as many development tasks as possible