Trace Abstraction-Based Verification for Uninterpreted Programs

被引：2
|
作者：
Hong, Weijiang [1 ,2 ]
Chen, Zhenbang [1 ]
Du, Yide [1 ]
Wang, Ji [1 ,2 ]
机构：
[1] Natl Univ Def Technol, Coll Comp, Changsha, Peoples R China
[2] Natl Univ Def Technol, State Key Lab High Performance Comp, Changsha, Peoples R China
来源：
FORMAL METHODS, FM 2021 | 2021年 / 13047卷
基金：
国家重点研发计划;
关键词：
Uninterpreted programs; CEGAR; Trace abstraction; REFINEMENT;
D O I：
10.1007/978-3-030-90870-6_29
中图分类号：
TP39 [计算机的应用];
学科分类号：
081203 ; 0835 ;
摘要：
The verification of uninterpreted programs is undecidable in general. This paper proposes to employ counterexample-guided abstraction refinement (CEGAR) framework for verifying uninterpreted programs. Different from the existing interpolant-based trace abstraction, we propose a congruence-based trace abstraction method for infeasible counterexample paths to refine the program's abstraction model, which is designed specifically for uninterpreted programs. Besides, we propose an optimization method that utilizes the decidable verification result for coherent uninterpreted programs to improve the CEGAR framework's efficiency. We have implemented our verification method and evaluated it on two kinds of benchmark programs. Compared with the state-of-the-art, our method is more effective and efficient, and achieves 3.6x speedups on average.
引用
收藏
页码：545 / 562
页数：18
相关论文
共 50 条
  • [1] Abstraction-Based Performance Verification of NoCs
    Holcomb, Daniel
    Brady, Bryan
    Seshia, Sanjit
    [J]. PROCEEDINGS OF THE 48TH ACM/EDAC/IEEE DESIGN AUTOMATION CONFERENCE (DAC), 2011, : 492 - 497
  • [2] Abstraction-based model checking programs
    Qian, Junyan
    Xu, Baowen
    Zhang, Yingzhou
    [J]. Journal of Computational Information Systems, 2007, 3 (02): : 675 - 682
  • [3] An Abstraction-Based Framework for Neural Network Verification
    Elboher, Yizhak Yisrael
    Gottschlich, Justin
    Katz, Guy
    [J]. COMPUTER AIDED VERIFICATION (CAV 2020), PT I, 2020, 12224 : 43 - 65
  • [4] Towards Abstraction-Based Verification of Shape Calculus
    Buti, F.
    De Donato, M. Callisto
    Corradini, F.
    Di Berardini, M. R.
    Merelli, E.
    Tesei, L.
    [J]. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2012, 284 : 23 - 34
  • [5] Decidable Verification of Uninterpreted Programs
    Mathur, Umang
    Madhusudan, P.
    Viswanathan, Mahesh
    [J]. PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2019, 3 (POPL):
  • [6] Collaborative Verification of Uninterpreted Programs
    Du, Yide
    Hong, Weijiang
    Chen, Zhenbang
    Wang, Ji
    [J]. THEORETICAL ASPECTS OF SOFTWARE ENGINEERING, TASE 2022, 2022, 13299 : 148 - 154
  • [7] Collaborative Verification of Uninterpreted Programs
    Du, Yi-De
    Hong, Wei-Jiang
    Chen, Zhen-Bang
    Wang, Ji
    [J]. Ruan Jian Xue Bao/Journal of Software, 2023, 34 (07):
  • [8] Abstraction-based verification of codiagnosability for discrete event systems
    Schmidt, K.
    [J]. AUTOMATICA, 2010, 46 (09) : 1489 - 1494
  • [9] Abstraction-Based Verification of Approximate Preopacity for Control Systems
    Hou, Junyao
    Liu, Siyuan
    Yin, Xiang
    Zamani, Majid
    [J]. IEEE CONTROL SYSTEMS LETTERS, 2023, 7 : 1087 - 1092
  • [10] Abstraction-Based Verification of Infinite-State Reactive Modules
    Belardinelli, Francesco
    Lomuscio, Alessio
    [J]. ECAI 2016: 22ND EUROPEAN CONFERENCE ON ARTIFICIAL INTELLIGENCE, 2016, 285 : 725 - 733
12345