Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
How testing helps to diagnose proof failures
Petiot G., Kosmatov N., Botella B., Giorgetti A., Julliand J.  Formal Aspects of Computing 30 (6): 629-657, 2018. Type: Article
Date Reviewed: May 10 2019

Petiot et al. present testing software components that help optimize the effort of “applying deductive verification to formally prove that a [computer] program respects its formal specification.”

The purpose of the proposed research is to deliver a methodology that exploits test cases “to identify the reason of a proof failure and to produce a counterexample clearly illustrating the issue.” For this, the authors define categories of proof failures, for example, non-compliance, subcontract weakness (after discussing the notions of contract and subcontract), and prover incapacity, and subsequently provide detailed examples with code excerpts of how these failures get detected by applying tests. After outlining the testing cases and methodology for detecting these failures, the authors introduce a method of structural testing that identifies the failure type and suggests the most suitable actions related to the verification task.

The described method is implemented as a FRAMA-C plugin, called STADY. The reported experiments with STADY, based on 26 annotated programs, show that the proposed method is able to correctly classify most of the proof failures.

A very thoroughly presented account with many technical details and a solid related work analysis, this paper is a good read for theoretical computer scientists and programmers looking to optimize the performance of their programming practices or to design methods to automate the detection of proof failures.

Reviewer:  Mariana Damova Review #: CR146566 (1908-0315)
Bookmark and Share
  Editor Recommended
Featured Reviewer
Deduction And Theorem Proving (I.2.3 )
Deduction (I.2.3 ... )
Proof Theory (F.4.1 ... )
Would you recommend this review?
Other reviews under "Deduction And Theorem Proving": Date
Actual causality
Halpern J.,  The MIT Press, Cambridge, MA, 2016. 240 pp. Type: Book (978-0-262035-02-6)
Feb 28 2017
Computational intelligence: revised and selected papers of the International Joint Conference, IJCCI 2013, Vilamoura, Portugal, September 20-22, 2013
Madani K., Dourado A., Rosa A., Filipe J., Kacprzyk J.,  Springer International Publishing, New York, NY, 2015. 518 pp. Type: Book (978-3-319233-91-8)
Jul 26 2016
Commonsense reasoning and commonsense knowledge in artificial intelligence
Davis E., Marcus G.  Communications of the ACM 58(9): 92-103, 2015. Type: Article
Mar 23 2016

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright © 2000-2022 ThinkLoud, Inc.
Terms of Use
| Privacy Policy