|COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring.|
Compositional Inter-Language Relational Verification
If you have a question about this talk, please contact Microsoft Research Cambridge Talks Admins.
This event may be recorded and made available internally or externally via http://research.microsoft.com. Microsoft will own the copyright of any recordings made. If you do not wish to have your image/voice recorded please consider this before attending
The “relational” approach to program verification involves showing that some lower-level program of interest is equivalent to (or a refinement of) some higher-level program, which may in turn prove more amenable to traditional verification techniques. Thanks to recent advances in theorem proving technology, the relational approach has been shown to scale to the verification of significant software systems, such as seL4 and the certified CompCert compiler for C.
However, existing relational methods apply only to the verification of whole software systems. For instance, the correctness of the CompCert compiler is guaranteed only when it is used to compile whole programs, since the underlying proof method lacks compositionality.
Informally, compositionality means that the verification of a whole program may be obtained by composing together the verification of its modular subcomponents.
In this talk, I will present two notions of compositionality arising in relational verification—horizontal and vertical compositionality—and discuss the extent to which existing relational techniques do or do not support them. I will then discuss my own work toward fully compositional inter-language relational verification, in particular: (1) the development of a compositional, semantic notion of equivalence between high- and low-level languages, and (2) the invention of a novel relational technique, parametric bisimulations, which supports both horizontal and vertical notions of compositionality.
This talk is part of the Microsoft Research Cambridge, public talks series.
This talk is included in these lists:
Note that ex-directory lists are not shown.
Other listsFrench Graduate Research Seminar 2008/2009 Newnham College MCR Speaker Series Humanitarian Centre
Other talksDiagnosing diapycnal mixing in Drake Passage using numerical models and results from the DIMES experiment Molecular excited states and QMC A novel axial pattern skin flap based on the cranial cutaneous branch of the saphenous artery in dogs Tumour natural history, structure and nomenclature (lecture/demonstration) Validity and non-validity of the NLS approximation for the water wave problem - Recent developments and open problems Who by sound and who by ground, who by pin and who by skin: side-channel key extraction from PCs