Institute of Cybernetics at TUT
Tuesday, 15 May 2012, 14:00 (note the unusual weekday)
Cybernetica Bldg (Akadeemia tee 21), room B101
Abstract: Spec# is a programming system for the development of correct programs. It consists of a programming language, a verification methodology, and tools. The Spec# language extends C# with contracts, which allow programmers to document their design decisions in the code. The verification methodology provides rules and guidelines for how to use the Spec# features to express and check properties of interesting implementations. Finally, the tool support consists of a compiler that emits run-time checks for many contracts and a static program verifier that attempts to prove automatically that an implementation satisfies its specification. In this talk I will show how use of the Spec# system, focusing on specification and static verification.