An Inference Method of Quasi-Weakest Preconditions by Minimal Unsatisfiable Core Enumeration

DOI

Bibliographic Information

Other Title
  • Minimal Unsatisfiable Core列挙によるプログラムの準最弱な事前条件推定

Search this article

Description

In this article, we propose a novel method to infer preconditions of a program. This method firstly generates a set of predicates from the program text, converts the program code into a logical formula, negates the postcondition given by the user, and conjuncts them all into a formula. Then, our method enumearates (possibly multiple) minimal unsatisfiable cores (or MUC) of the conjunctive formula. Our technique finally extracts proper preconditions from the MUCs. We call them as “quasi-weakest” preconditions in that each of the precondition is the weakest among all the conjunctions of the predicates.<BR>We prototyped a tool named SMUCE that realizes the proposed method using CForge, a bounded verifier for C code. Thereafter, we applied the tool to nine C functions implementing textbook algorithms with two postconditions, and compared the generated preconditions with manually-specified ones. The result showed that SMUCE extracted equivalent, or even weaker preconditions than manually-specified ones from ten of the total of 18 programs, indicating the proposed method can infer applicative preconditions in principle.

Journal

  • Computer Software

    Computer Software 30 (2), 2_207-2_226, 2013

    Japan Society for Software Science and Technology

Details 詳細情報について

  • CRID
    1390282679714440448
  • NII Article ID
    130004892253
  • DOI
    10.11309/jssst.30.2_207
  • ISSN
    02896540
  • Text Lang
    ja
  • Data Source
    • JaLC
    • CiNii Articles
  • Abstract License Flag
    Disallowed

Report a problem

Back to top