Navigation

• Education
  • International programmes
  • Faculties
  • ECTS
  • Vision and policy
• Research
  • Research at KU Leuven
  • Support and funding
  • Industry and Society
  • Phd
  • Postdoc researcher
  • Output and impact
  • Networking
  • Vision and policy
• Admissions
  • How to apply
  • Scholarships
  • Degree seeking students
  • Non-degree seeking students
  • Doctoral students
  • Reseachers
  • Short term study visits
  • Prepare your stay
• Living in Leuven
  • Welcome activities
  • News and agenda
  • Student Services
  • Housing
  • Insurance
  • Sports and culture
  • Student organisations
• About KU Leuven
  • Mission statement
  • Facts and figures
  • International networks
  • Development Cooperation
  • Academic Calendar
  • Alumni
  • Fundraising
  • Services and support
  • Boards and councils
  • News and press
  • Jobs

CW 493

Bart Jacobs and Frank Piessens
Inspector methods for state abstraction: soundness proof

Abstract

This note formalizes and proves the soundness of an approach for modular static verification of safety properties of object-oriented programs where module specifications refer to module state abstractly, using inspector methods, to eliminate dependencies of clients on a module?s internal implementation details.