Ranking Function Synthesis for Loop Programs via Counterexample Guided Deep Learning
Author:
Affiliation:

Clc Number:

TP311

Fund Project:

  • Article
  • |
  • Figures
  • |
  • Metrics
  • |
  • Reference
  • |
  • Related
  • |
  • Cited by
  • |
  • Materials
  • |
  • Comments
    Abstract:

    This study proposes a novel approach for synthesizing ranking functions that are expressed as feed-forward neural networks. The approach employs a counter example-guided synthesis procedure, where a learner and a verifier interact to synthesize ranking function. The learner trains a candidate ranking function that satisfies the ranking function conditions over a set of sampled data, and the verifier either ensures the validity of the candidate ranking function or yields counterexamples, which are passed back to further guide the learner. The procedure leverages efficient supervised learning algorithm, while guaranteeing formal soundness via SMT solver. The tool SyntheRF is implemented, then, its scalability and effectiveness are evaluated over a set of benchmark examples.

    Reference
    Related
    Cited by
Get Citation

林开鹏,梅国泉,林望,丁佐华.基于深度学习和反例制导的循环程序秩函数生成.软件学报,2022,33(8):2918-2929

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:September 05,2021
  • Revised:October 14,2021
  • Adopted:
  • Online: January 28,2022
  • Published: August 06,2022
You are the firstVisitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address:4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code:100190
Phone:010-62562563 Fax:010-62562533 Email:jos@iscas.ac.cn
Technical Support:Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063