Automatic proving or disproving equality loop invariants based on finite difference techniques

被引：2
|
作者：
Li, Mengjun [1 ]
机构：
[1] Natl Univ Def Technol, Sch Comp Sci, Changsha, Hunan, Peoples R China
来源：
INFORMATION PROCESSING LETTERS | 2015年 / 115卷 / 04期
关键词：
Automatic theorem proving; Equality loop invariants; Formal characterization; Formal verification; Finite difference techniques; POLYNOMIAL INVARIANTS;
D O I：
10.1016/j.ipl.2014.11.006
中图分类号：
TP [自动化技术、计算机技术];
学科分类号：
0812 ;
摘要：
Loop invariants play a major role in software verification. In this paper, based on finite difference techniques, a formal characterization for equality loop invariants is presented. Integrating the formal characterization with the automatic verification approach in [5], the algorithm for automatic proving or disproving equality loop invariants is presented. The effectiveness of the algorithm is demonstrated with the experimental results. (C) 2014 Elsevier B.V. All rights reserved.
引用
下载
收藏
页码：468 / 474
页数：7
相关论文
共 14 条
  • [1] Generating Equality Loop Invariants with Functions Based on Random Testing, Constraint Solving and Verification
    Li, Mengjun
    2017 24TH ASIA-PACIFIC SOFTWARE ENGINEERING CONFERENCE (APSEC 2017), 2017, : 606 - 611
  • [2] GSTC-Based Simulation of Metasurfaces in Finite Difference Techniques
    Vahabzadeh, Yousef
    Caloz, Christophe
    2016 IEEE ANTENNAS AND PROPAGATION SOCIETY INTERNATIONAL SYMPOSIUM, 2016, : 373 - 374
  • [3] Impartial Differentiable Automatic Data Augmentation Based on Finite Difference Approximation for Pedestrian Detection
    Zhou, Shirui
    Tang, Yi
    Liu, Min
    Wang, Yaonan
    Wen, He
    IEEE TRANSACTIONS ON INSTRUMENTATION AND MEASUREMENT, 2022, 71
  • [4] Novel numerical techniques based on mimetic finite difference method for pricing two dimensional options
    Attipoe, David Sena
    Tambue, Antoine
    RESULTS IN APPLIED MATHEMATICS, 2022, 13
  • [5] Techniques for improving computational speed in numerical simulation of casting thermal stress based on finite difference method
    Xue Xiang
    Wang Yueping
    ChinaFoundry, 2013, 10 (02) : 81 - 86
  • [6] Techniques for improving computational speed in numerical simulation of casting thermal stress based on finite difference method
    Xue Xiang
    Wang Yueping
    China Foundry, 2013, (02) : 81 - 86
  • [7] Techniques for improving computational speed in numerical simulation of casting thermal stress based on finite difference method
    Xue Xiang
    Wang Yueping
    CHINA FOUNDRY, 2013, 10 (02) : 81 - 86
  • [8] Automatic enmeshment of finite difference for 3D solid modeling based on Auto CAD-AME
    Xitong Gongcheng Lilum yu Shijian, 6 (1-4):
  • [9] Finite-difference time-domain-based optical microscopy simulation of dispersive media facilitates the development of optical imaging techniques
    Zhang, Di
    Capoglu, Ilker
    Li, Yue
    Cherkezyan, Lusik
    Chandler, John
    Spicer, Graham
    Subramanian, Hariharan
    Taflove, Allen
    Backman, Vadim
    JOURNAL OF BIOMEDICAL OPTICS, 2016, 21 (06)
  • [10] NUMERICAL-STUDIES OF SPLIT-OPERATOR FINITE-DIFFERENCE ALTERNATING-DIRECTION IMPLICIT PROPAGATION TECHNIQUES BASED ON GENERALIZED PADE APPROXIMANTS
    YEVICK, D
    GLASNER, M
    HERMANSSON, B
    OPTICS LETTERS, 1992, 17 (10) : 725 - 727
12