Skip to content

Research at St Andrews

Automatic predicate testing in formal certification: you’ve only proven what you’ve said, not what you meant!

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Author(s)

School/Research organisations

Abstract

The use of formal methods and proof assistants helps to increase the confidence in critical software. However, a formal proof is only a guarantee relative to a formal specification, and not necessary about the real requirements. There is always a jump when going from an informal specification to a formal specification expressed in a logical theory. Thus, proving the correctness of a piece of software always makes the implicit assumption that there is adequacy between the formalised specification -written with logical statements and predicates- and the real requirements -often written in English-. Unfortunately, a huge part of the complexity lies precisely in the specification itself, and it is far from obvious that the formal specification says exactly and completely what it should say. Why should we trust more these predicates than the code that we’ve first refused to trust blindly, leading to these proofs? We show in this paper that the proving activity has not replaced the testing activity but has only changed the object which requires to be tested. Instead of testing code, we now need to test predicates.We present recent ideas about how to conduct these tests inside the proof assistant on a few examples, and how to automate them as far as possible.

Close

Details

Original languageEnglish
Title of host publicationTests and Proofs - 10th International Conference, TAP 2016 Held as Part of STAF 2016
EditorsBernhard K. Aichernig, Carlo A. Furia
PublisherSpringer-Verlag
Pages191-198
Number of pages8
ISBN (Electronic)9783319411354
ISBN (Print)9783319411347
DOIs
StatePublished - 2016
Event10th International Conference on Tests and Proofs, TAP 2016 and Held as Part of Software Technologies: Applications and Foundations, STAF 2016 - Vienna, Austria
Duration: 5 Jul 20167 Jul 2016

Publication series

NameLecture Notes in Computer Science
Volume9762
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference10th International Conference on Tests and Proofs, TAP 2016 and Held as Part of Software Technologies: Applications and Foundations, STAF 2016
CountryAustria
CityVienna
Period5/07/167/07/16

    Research areas

  • Formal certification, Predicate testing, Proof assistant

Discover related content
Find related publications, people, projects and more using interactive charts.

View graph of relations

Related by author

  1. Automatically proving equivalence by type-safe reflection

    Slama, F. & Brady, E. C. 2017 Intelligent Computer Mathematics: 10th International Conference, CICM 2017, Edinburgh, UK, July 17-21, 2017, Proceedings. Geuvers, H., England, M., Hasan, O., Rabe, F. & Teschke, O. (eds.). Cham: Springer, p. 40-55 (Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence); vol. 10383)

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

ID: 256566008