HiFrog: SMT-based Function Summarization for Software Verification

被引：9
|
作者：
Alt, Leonardo [1 ]
Asadi, Sepideh [1 ]
Chockler, Hana [2 ]
Mendoza, Karine Even [2 ]
Fedyukovich, Grigory [3 ]
Hyvarinen, Antti E. J. [1 ]
Sharygina, Natasha [1 ]
机构：
[1] Univ Svizzera Italiana, Lugano, Switzerland
[2] Kings Coll London, London, England
[3] Univ Washington, Seattle, WA 98195 USA
来源：
TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, TACAS 2017, PT II | 2017年 / 10206卷
关键词：
D O I：
10.1007/978-3-662-54580-5_12
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
Function summarization can be used as a means of incremental verification based on the structure of the program. HiFrog is a fully featured function-summarization-based model checker that uses SMT as the modeling and summarization language. The tool supports three encoding precisions through SMT: uninterpreted functions, linear real arithmetics, and propositional logic. In addition the tool allows optimized traversal of reachability properties, counter-example-guided summary refinement, summary compression, and user-provided summaries. We describe the use of the tool through the description of its architecture and a rich set of features. The description is complemented by an experimental evaluation on the practical impact the different SMT precisions have on model-checking.
引用
收藏
页码：207 / 213
页数：7
相关论文
共 50 条
  • [21] Formal Verification of Software Designs in Hierarchical State Transition Matrix with SMT-based Bounded Model Checking
    Kong, Weiqiang
    Katahira, Noriyuki
    Watanabe, Masahiko
    Katayama, Tetsuro
    Hisazumi, Kenji
    Fukuda, Akira
    2011 18TH ASIA-PACIFIC SOFTWARE ENGINEERING CONFERENCE (APSEC 2011), 2011, : 81 - 88
  • [22] Building SMT-Based Software Model Checkers: An Experience Report
    Armando, Alessandro
    FRONTIERS OF COMBINING SYSTEMS, PROCEEDINGS, 2009, 5749 : 1 - 17
  • [23] SMT-Based Stability Verification of an Industrial Switched PI Control Systems
    Basagiannis, Stylianos
    Battista, Ludovico
    Becchi, Anna
    Cimatti, Alessandro
    Giantamidis, Georgios
    Mover, Sergio
    Tacchella, Alberto
    Tonetta, Stefano
    Tsachouridis, Vassilios
    2023 53RD ANNUAL IEEE/IFIP INTERNATIONAL CONFERENCE ON DEPENDABLE SYSTEMS AND NETWORKS WORKSHOPS, DSN-W, 2023, : 243 - 250
  • [24] SMT-based Formal Verification of Synchronous Reactive Model for Zone Controller
    Li T.-F.
    Sun J.-F.
    Lv X.-J.
    Chen X.
    Liu J.
    Sun H.-Y.
    He J.-F.
    Ruan Jian Xue Bao/Journal of Software, 2023, 34 (07):
  • [25] Scaling up the formal verification of Lustre programs with SMT-based techniques
    Hagen, George
    Tinelli, Cesare
    2008 FORMAL METHODS IN COMPUTER-AIDED DESIGN, 2008, : 109 - 117
  • [26] SAT and SMT-Based Verification of Security Protocols Including Time Aspects
    Szymoniak, Sabina
    Siedlecka-Lamch, Olga
    Zbrzezny, Agnieszka M.
    Zbrzezny, Andrzej
    Kurkowski, Miroslaw
    SENSORS, 2021, 21 (09)
  • [27] SMT-based Verification Applied to Non-convex Optimization Problems
    Araujo, Rodrigo
    Bessa, Iury
    Cordeiro, Lucas C.
    Chaves Filho, Joao Edgar
    2016 VI BRAZILIAN SYMPOSIUM ON COMPUTING SYSTEMS ENGINEERING (SBESC 2016), 2016, : 1 - 8
  • [28] SMT-based Bounded Model Checking for Cooperative Software with a Deterministic Scheduler
    Zhang, Haitao
    Lu, Yonggang
    STRUCTURED OBJECT-ORIENTED FORMAL LANGUAGE AND METHOD, 2017, 10189 : 181 - 200
  • [29] SMT-Based Verification of Persistency Invariants of Px86 Programs
    Marmanis, Iason
    Vafeiadis, Viktor
    VERIFIED SOFTWARE. THEORIES, TOOLS AND EXPERIMENTS, VSTTE 2022, 2023, 13800 : 92 - 110
  • [30] SMT-Based Modeling and Verification of Spiking Neural Networks: A Case Study
    Banerjee, Soham
    Ghosh, Sumana
    Banerjee, Ansuman
    Mohalik, Swarup K.
    VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION, VMCAI 2023, 2023, 13881 : 25 - 43
12345