Proving consistency of pure methods and model fields

R. Leino, R. Middelkoop

    Onderzoeksoutput: Hoofdstuk in Boek/Rapport/CongresprocedureConferentiebijdrageAcademicpeer review

    3 Citaten (Scopus)


    Pure methods and model fields are useful and common specification constructs that can be interpreted by the introduction of axioms in a program verifier’s underlying proof system. Care has to be taken that these axioms do not introduce an inconsistency into the proof system. This paper describes and proves sound an approach that ensures no inconsistencies are introduced. Unlike some previous syntax-based approaches, this approach is based on semantics, which lets it admit some natural but previously problematical specifications. The semantic conditions are discharged by the program verifier using an SMT solver, and the paper describes heuristics that help avoid common problems in finding witnesses with trigger-based SMT solvers. The paper reports on the positive experience with using this approach in Spec# for over a year.
    Originele taal-2Engels
    TitelFundamental Approaches to Software Engineering (12th International Conference, FASE'09, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009. Proceedings)
    RedacteurenM. Chechik, M. Wirsing
    Plaats van productieBerlin
    ISBN van geprinte versie978-3-642-00592-3
    StatusGepubliceerd - 2009

    Publicatie series

    NaamLecture Notes in Computer Science
    ISSN van geprinte versie0302-9743


    Duik in de onderzoeksthema's van 'Proving consistency of pure methods and model fields'. Samen vormen ze een unieke vingerafdruk.

    Citeer dit