微信服务号

微信订阅号

2025-5-2- 11
Home > Archive>Volume 33, Issue 8, 2022 >2918-2929. DOI:10.13328/j.cnki.jos.006605
PDF HTML XML Export Cite reminder
Ranking Function Synthesis for Loop Programs via Counterexample Guided Deep Learning
Author:
Affiliation:

Clc Number:

TP311

  • Article
    • | |
  • Metrics
    • |
  • Reference [27]
    • |
  • Related [20]
    • |
  • Cited by
    • | |
  • 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
    [1] Cousot P, Cousot R.An abstract interpretation framework for termination.ACM SIGPLAN Notices, 2012, 47(1):245-258.
    [2] Lee CS, Jones ND, Ben-Amram AM.The size-change principle for program termination.In:Proc.of the 28th ACM SIGPLANSIGACT Symp.on Principles of Programming Languages.2001.81-92.
    [3] Urban C.The abstract domain of segmented ranking functions.In:Proc.of the Int'l Static Analysis Symp.Berlin, Heidelberg:Springer, 2013.43-62.
    [4] Braverman M.Termination of integer linear programs.In:Proc.of the Int'l Conf.on Computer Aided Verification.Berlin, Heidelberg:Springer, 2006.372-385.
    [5] Tiwari A.Termination of linear programs.In:Proc.of the Int'l Conf.on Computer Aided Verification.Berlin, Heidelberg:Springer, 2004.70-82.
    [6] Numbers ONC.With an application to the entschenidugsproblem.1937.
    [7] Colón MA, Sipma HB.Practical methods for proving program termination.In:Proc.of the Int'l Conf.on Computer Aided Verification.Berlin, Heidelberg:Springer, 2002.442-454.
    [8] Podelski A, Rybalchenko A.A complete method for the synthesis of linear ranking functions.In:Proc.of the Int'l Workshop on Verification, Model Checking, and Abstract Interpretation.Berlin, Heidelberg:Springer, 2004.239-251.
    [9] Ben-Amram AM, Genaim S.On multiphase-linear ranking functions.In:Proc.of the Int'l Conf.on Computer Aided Verification.Cham:Springer, 2017:601-620.
    [10] Bradley AR, Manna Z, Sipma HB.The polyranking principle.In:Proc.of the Int'l Colloquium on Automata, Languages, and Programming.Berlin, Heidelberg:Springer, 2005.1349-1361.
    [11] Cook B, See A, Zuleger F.Ramsey vs.lexicographic termination proving.In:Proc.of the Int'l Conf.on Tools and Algorithms for the Construction and Analysis of Systems.Berlin, Heidelberg:Springer, 2013.47-61.
    [12] Urban C.The abstract domain of segmented ranking functions.In:Proc.of the Int'l Static Analysis Symp.Berlin, Heidelberg:Springer, 2013.43-62.
    [13] Chen Y, Xia B, Yang L, et al.Discovering non-linear ranking functions by solving semi-algebraic systems.In:Proc.of the Int'l Colloquium on Theoretical Aspects of Computing.Berlin, Heidelberg:Springer, 2007.34-49.
    [14] Shen L, Wu M, Yang Z, et al.Generating exact nonlinear ranking functions by symbolic-numeric hybrid method.Journal of Systems Science and Complexity, 2013, 26(2):291-301.
    [15] Yuan Y, Li Y.Ranking function detection via SVM:A more general method.Proc.of the IEEE Access, 2019, 7:9971-9979.
    [16] Fan RE, Chang KW, Hsieh CJ, et al.LIBLINEAR:A library for large linear classification.Proc.of the Journal of Machine Learning Research, 2008, 9:1871-1874.
    [17] Li Y, Sun X, Li Y, et al.Synthesizing nested ranking functions for loop programs via SVM.In:Proc.of the Int'l Conf.on Formal Engineering Methods.Cham:Springer, 2019.438-454.https://doi.org/10.1007/978-3-030-32409-4_27
    [18] De Moura L, Bjørner N.Z3:An efficient SMT solver.In:Proc.of the Int'l Conf.on Tools and Algorithms for the Construction and Analysis of Systems.Berlin, Heidelberg:Springer, 2008.337-340.
    [19] Brown CW, Davenport JH.The complexity of quantifier elimination and cylindrical algebraic decomposition.In:Proc.of the 2007 Int'l Symp.on Symbolic and Algebraic Computation (ISSAC 2007).New York:Association for Computing Machinery, 2007.54-60.
    [20] Si X, Dai H, Raghothaman M, et al.Learning loop invariants for program verification.In:Proc.of the of Neural Information Processing Systems.2018.7762-7773.
    [21] Chang YC, Roohi N, Gao S.Neural Lyapunov control.In:Proc.of the 33rd Int'l Conf.on Neural Information Processing Systems.2019.3245-3254.
    [22] Abate A, Ahmed D, Giacobbe M, et al.Formal synthesis of Lyapunov neural networks.Proc.of the IEEE Control Systems Letters, 2020, 5(3):773-778.
    [23] Giacobbe M, Kroening D, Parsert J.Neural termination analysis.arXiv preprint arXiv:2102.03824, 2021.
    [24] Tan W, Li Y.Synthesis of ranking functions via DNN.Proc.of the Neural Computing and Applications, 2021:1-21.https://doi.org/10.1007/s00521-021-05763-8
    [25] Floyd RW.Assigning meanings to programs.In:Proc.of the Symp.in Applied llathematics.1967.
    [26] Cybenko G.Approximations by superpositions of a sigmoidal function.Proc.of the Mathematics of Control, Signals and Systems, 1989, 2:183-192.
    [27] Le TC, Antonopoulos T, Fathololumi P, et al.DynamiTe:Dynamic termination and non-termination proofs.Proc.of the ACM on Programming Languages, 2020, 4(OOPSLA):1-30.
    Cited by
    Comments
    Comments
    分享到微博
    Submit
Get Citation

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

Copy
Share
Article Metrics
  • Abstract:1023
  • PDF: 3681
  • HTML: 2738
  • Cited by: 0
History
  • Received:September 05,2021
  • Revised:October 14,2021
  • Online: January 28,2022
  • Published: August 06,2022
Links:Institute of Software, CASChina Computer FederationCASNSFC
You are the first2041655Visitors
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