![]() |
COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring. | ![]() |
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
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. This talk is included in these lists:
Note that ex-directory lists are not shown. |
Other listsPolitical Thought and Intellectual History Cambridge University Southeast Asian Forum Future of Sustainable Development in South AsiaOther talksValidation & testing of novel therapeutic targets to treat osteosarcoma Reframing African Studies through Languages and Translation: Overcoming Barricades to Knowledge and Knowledge Management Planning for sustainable urbanisation in China: a community perspective The interpretation of black hole solutions in general relativity On the morphology and vulnerability of dopamine neurons in Parkinson's disease Metamaterials and the Science of Invisibility Towards a whole brain model of perceptual learning "Mechanosensitive regulation of cancer epigenetics and pluripotency" Towards bulk extension of near-horizon geometries Cambridge Rare Disease Summit 2017 The evolution of photosynthetic efficiency C++ and the Standard Library |