University of Cambridge > Talks.cam > Logic and Semantics Seminar (Computer Laboratory) > Verifying Object-Invariants in Spec#

Verifying Object-Invariants in Spec#

Add to your list(s) Download to your calendar using vCal

  • UserWolfram Schulte (Microsoft Research Redmond)
  • ClockFriday 09 February 2007, 14:00-15:00
  • HouseFW11.

If you have a question about this talk, please contact Matthew Parkinson.

Spec# is an experimental extension to C# that adds design-by-contract features. Contracts include method preconditions, postconditions, object invariants and history invariants. Contracts capture programmer intentions about how methods and data are to be used. The Spec# program verifier generates logical verification conditions from a Spec# program. Internally, it uses an automatic theorem prover that analyzes the verification conditions to prove the correctness of the program or find errors in it. In this lecture I will present Spec# and focus on how to verify invariants in the presence of callbacks, various forms of aliasing, and inheritance.

Remark: Incorporates results from Rustan Leino, Mike Barnett, Manuel Fähndrich, Herman Venter, Rob DeLine (all MSR ), Peter Müller and Adam Darvas (ETH), Bart Jacobs (KU Leuven), Bor-Yuh Evan Chang (Berkley), and Angelika Wallenburg (Chalmers)

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2024 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity