Invariant Checking for SMT-Based Systems with Quantifiers

被引:0
|
作者
Fondazione Bruno Kessler, Universitá di Trento, Trento, Italy [1 ]
不详 [2 ]
不详 [3 ]
TX, United States
机构
来源
ACM Trans. Comput. Log | 2024年 / 4卷
关键词
D O I
10.1145/3686153
中图分类号
学科分类号
摘要
引用
收藏
相关论文
共 50 条
  • [1] SMT-Based Software Model Checking
    Cimatti, Alessandro
    [J]. MODEL CHECKING SOFTWARE, 2010, 6349 : 1 - 3
  • [2] SMT-based model checking for recursive programs
    Komuravelli, Anvesh
    Gurfinkel, Arie
    Chaki, Sagar
    [J]. FORMAL METHODS IN SYSTEM DESIGN, 2016, 48 (03) : 175 - 205
  • [3] SMT-Based Array Invariant Generation
    Larraz, Daniel
    Rodriguez-Carbonell, Enric
    Rubio, Albert
    [J]. VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION (VMCAI 2013), 2013, 7737 : 169 - 188
  • [4] SMT-based Bounded Model Checking for Real-time Systems
    Xu, Liang
    [J]. QSIC 2008: PROCEEDINGS OF THE EIGHTH INTERNATIONAL CONFERENCE ON QUALITY SOFTWARE, 2008, : 120 - 125
  • [5] Simple SMT-Based Bounded Model Checking for Timed Interpreted Systems
    Zbrzezny, Agnieszka M.
    Zbrzezny, Andrzej
    [J]. ROUGH SETS, IJCRS 2017, PT II, 2017, 10314 : 487 - 504
  • [6] An SMT-based approach to satisfiability checking of MITL
    Bersani, Marcello M.
    Rossi, Matteo
    San Pietro, Pierluigi
    [J]. INFORMATION AND COMPUTATION, 2015, 245 : 72 - 97
  • [7] SMT-based model checking for recursive programs
    Anvesh Komuravelli
    Arie Gurfinkel
    Sagar Chaki
    [J]. Formal Methods in System Design, 2016, 48 : 175 - 205
  • [8] SMT-based Safety Checking of Parameterized Multi-Agent Systems
    Felli, Paolo
    Gianola, Alessandro
    Montali, Marco
    [J]. THIRTY-FIFTH AAAI CONFERENCE ON ARTIFICIAL INTELLIGENCE, THIRTY-THIRD CONFERENCE ON INNOVATIVE APPLICATIONS OF ARTIFICIAL INTELLIGENCE AND THE ELEVENTH SYMPOSIUM ON EDUCATIONAL ADVANCES IN ARTIFICIAL INTELLIGENCE, 2021, 35 : 6321 - 6330
  • [9] SMT-Based Model Checking for Recursive Programs
    Komuravelli, Anvesh
    Gurfinkel, Arie
    Chaki, Sagar
    [J]. COMPUTER AIDED VERIFICATION, CAV 2014, 2014, 8559 : 17 - 34
  • [10] SMT-Based Unbounded Model Checking for ATL
    Kanski, Michal
    Niewiadomski, Artur
    Kacprzak, Magdalena
    Penczek, Wojciech
    Nabialek, Wojciech
    [J]. VERIFICATION AND EVALUATION OF COMPUTER AND COMMUNICATION SYSTEMS (VECOS 2021), 2022, 13187 : 43 - 58