Logical Abstract Domains and Interpretations

被引：5
|
作者：
Cousot, Patrick [2 ,3 ]
Cousot, Radhia [1 ,3 ]
Mauborgne, Laurent [3 ,4 ]
机构：
[1] CNRS, Paris, France
[2] NYU, Courant Inst Math Sci, New York, NY 10003 USA
[3] Ecole Normale Super, Paris, France
[4] Inst Madrileno Estudios Avanzados, Madrid, Spain
来源：
FUTURE OF SOFTWARE ENGINEERING | 2011年
关键词：
BOUNDED MODEL CHECKING; COMPLETENESS; SYSTEM;
D O I：
10.1007/978-3-642-15187-3_3
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
We give semantic foundations to abstract domains consisting in first order logic formula in a theory, as used in verification tools or methods using SMT-solvers or theorem provers. We exhibit conditions for a sound usage of such methods with respect to multi-interpreted semantics and extend their usage to automatic invariant generation by abstract interpretation.
引用
收藏
页码：48 / 71
页数：24
相关论文
共 50 条
  • [1] IMPROVING ABSTRACT INTERPRETATIONS BY COMBINING DOMAINS
    CODISH, M
    MULKERS, A
    BRUYNOOGHE, M
    DELABANDA, MG
    HERMENEGILDO, M
    [J]. ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 1995, 17 (01): : 28 - 44
  • [2] A logical model for relational abstract domains
    Giacobazzi, R
    Scozzari, F
    [J]. ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 1998, 20 (05): : 1067 - 1109
  • [3] Lifting abstract interpreters to quantified logical domains
    Gulwani, Sumit
    McCloskey, Bill
    Tiwari, Ashish
    [J]. ACM SIGPLAN NOTICES, 2008, 43 (01) : 235 - 246
  • [4] Lifting Abstract Interpreters to Quantified Logical Domains
    Gulwani, Sumit
    McCloskey, Bill
    Tiwari, Ashish
    [J]. POPL'08: PROCEEDINGS OF THE 35TH ANNUAL ACM SIGPLAN-SIGACT SYMPOSIUM ON PRINCIPLES OF PROGRAMMING LANGUAGES, 2008, : 235 - 246
  • [5] Safety of abstract interpretations for free, via logical relations and Galois connections
    Backhouse, K
    Backhouse, R
    [J]. SCIENCE OF COMPUTER PROGRAMMING, 2004, 51 (1-2) : 153 - 196
  • [6] Extracting Program Logics From Abstract Interpretations Defined by Logical Relations
    Schmidt, David A.
    [J]. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2007, 173 : 339 - 356
  • [7] Logical Pluralism and Interpretations of Logical Systems
    Tajer, Diego
    Fiore, Camillo
    [J]. LOGIC AND LOGICAL PHILOSOPHY, 2022, 31 (02) : 209 - 234
  • [8] Logical Interpretations of Autoencoders
    Fuxjaeger, Anton
    Belle, Vaishak
    [J]. ECAI 2020: 24TH EUROPEAN CONFERENCE ON ARTIFICIAL INTELLIGENCE, 2020, 325 : 2481 - 2488
  • [9] REVERSING ABSTRACT INTERPRETATIONS
    HUGHES, J
    LAUNCHBURY, J
    [J]. LECTURE NOTES IN COMPUTER SCIENCE, 1992, 582 : 269 - 286
  • [10] REVERSING ABSTRACT INTERPRETATIONS
    HUGHES, J
    LAUNCHBURY, J
    [J]. SCIENCE OF COMPUTER PROGRAMMING, 1994, 22 (03) : 307 - 326
12345