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

Опубликовано 21 июня 2016, 22:33

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.