Using a Push-Button Verifying Compiler to Build Verified Software Components

Speaker  Murali Sitaraman

Affiliation  School of Computing at Clemson

Host  Rustan Leino

Duration  01:15:58

Date recorded  31 March 2014

This talk will discuss how to design, specify, implement, and verify software components in a modular fashion, one component at a time, using a push-button verifying compiler. It will discuss how to engineer specifications and how to design and annotate imperative, object-based component implementations to facilitate verification. It will discuss language support necessary for building verified components including the need for extensible mathematical developments. To present the ideas, the talk will use RESOLVE, an integrated specification and programming language, and a supporting web-integrated software engineering environment. The environment has been used in undergraduate courses at multiple institutions. It is freely available and requires no software installation. The talk will conclude with a discussion of remaining research and educational challenges.

©2014 Microsoft Corporation. All rights reserved.
> Using a Push-Button Verifying Compiler to Build Verified Software Components