Encoding Queues in Satisfiability Modulo Theories Based Bounded Model Checking

被引：1
|
作者：
Junttila, Tommi [1 ]
Dubrovin, Jori [1 ]
机构：
[1] Aalto Univ, Dept Informat & Comp Sci, FIN-02015 Helsinki, Finland
来源：
LOGIC FOR PROGRAMMING, ARTIFICIAL INTELLIGENCE, AND REASONING, PROCEEDINGS | 2008年 / 5330卷
关键词：
D O I：
10.1007/978-3-540-89439-1_21
中图分类号：
TP18 [人工智能理论];
学科分类号：
081104 ; 0812 ; 0835 ; 1405 ;
摘要：
Using a Satisfiability Modulo Theories (SMT) solver as the back-end in SAT-based software model checking allows common data types to be represented directly in the language of the solver. A problem is that many software systems involve first-in-first-out queues but current SMT solvers do not support the theory of queues. This paper Studies how to encode queues in the context of SMT-based bounded model checking, using only widely supported theories such as linear arithmetic and uninterpreted functions. Various encodings with considerably different compactness and requirements for available theories are proposed. An experimental comparison of the relative efficiency of the encodings is given.
引用
收藏
页码：290 / 304
页数：15
相关论文
共 50 条
  • [1] Satisfiability Modulo Bounded Checking
    Cruanes, Simon
    AUTOMATED DEDUCTION - CADE 26, 2017, 10395 : 114 - 129
  • [2] Bounded Model Checking of Dense-Timed Deontic Interpreted Systems: A Satisfiability Modulo Theories Approach
    Wozna-Szczesniak, Bozena
    Szczesniak, Ireneusz
    Olszewski, Ireneusz
    APPLIED SCIENCES-BASEL, 2025, 15 (05):
  • [3] Proof Checking Technology for Satisfiability Modulo Theories
    Stump, Aaron
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2009, 228 : 121 - 133
  • [4] Satisfiability modulo theories
    Barrett, Clark
    Sebastiani, Roberto
    Seshia, Sanjit A.
    Tinelli, Cesare
    Frontiers in Artificial Intelligence and Applications, 2009, 185 (01) : 825 - 885
  • [5] Model Learning as a Satisfiability Modulo Theories Problem
    Smetsers, Rick
    Fiterau-Brostean, Paul
    Vaandrager, Frits
    LANGUAGE AND AUTOMATA THEORY AND APPLICATIONS (LATA 2018), 2018, 10792 : 182 - 194
  • [6] A fixpoint based encoding for bounded model checking
    Frisch, A
    Sheridan, D
    Walsh, T
    FORMAL METHODS IN COMPUTER-AIDED DESIGN, PROCEEDINGS, 2002, 2517 : 238 - 255
  • [7] Probabilistic model checking modulo theories
    Wachter, Bjoern
    Zhang, Lijun
    Hermanns, Holger
    FOURTH INTERNATIONAL CONFERENCE ON THE QUANTITATIVE EVALUATION OF SYSTEMS, 2007, : 129 - +
  • [8] Bounded model checking using satisfiability solving
    Clarke, E
    Biere, A
    Raimi, R
    Zhu, Y
    FORMAL METHODS IN SYSTEM DESIGN, 2001, 19 (01) : 7 - 34
  • [9] Bounded Model Checking Using Satisfiability Solving
    Edmund Clarke
    Armin Biere
    Richard Raimi
    Yunshan Zhu
    Formal Methods in System Design, 2001, 19 : 7 - 34
  • [10] From propositional satisfiability to satisfiability modulo theories
    Sheini, Hossein M.
    Sakallah, Karem A.
    THEORY AND APPLICATIONS OF SATISFIABILITY TESTING - SAT 2006, PROCEEDINGS, 2006, 4121 : 1 - 9
12345