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 Computing30 (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
Noninteractive zero-knowledge
Blum M., De Santis A., Micali S., Persiano G. SIAM Journal on Computing 20(6): 1084-1118, 1991. Type: Article
Jan 1 1993
Cut elimination and automatic proof procedures
Zhang W. Theoretical Computer Science 91(2): 265-284, 1991. Type: Article
Apr 1 1993
A non-reified temporal logic
Bacchus F., Tenenberg J., Koomen J. Artificial Intelligence 52(1): 87-108, 1991. Type: Article
Oct 1 1992

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright 1999-2024 ThinkLoud®
Terms of Use
| Privacy Policy