Speaker Murali Sitaraman
Affiliation School of Computing at Clemson
Host Rustan Leino
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.