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

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.

Speaker Details

Murali Sitaraman is Professor of Computer Science in the School of Computing at Clemson. He directs the RESOLVE/Reusable Software Research Group (RSRG) at Clemson. His research spans a spectrum of foundational, practical, and educational topics in software engineering, and it has been supported by US NSF grants continuously for over 20 years. He has co-edited a book on Foundations of Component-Based Systems with Gary Leavens for Cambridge University Press. Together with members of his group, he has published over 100 papers in various forums. Sitaraman has taught the ideas to graduate and undergraduate students as well as to educators through several workshops for over 20 years.

Date:
Speakers:
Murali Sitaraman
Affiliation:
School of Computing at Clemson

    • Portrait of Jeff Running

      Jeff Running