Abstract Interpretation from Buchi Automata

被引:9
作者
Hofmann, Martin [1 ]
Chen, Wei [2 ]
机构
[1] Ludwig Maximilians Univ Munchen, Munich, Germany
[2] Univ Edinburgh, Edinburgh, Midlothian, Scotland
来源
PROCEEDINGS OF THE JOINT MEETING OF THE TWENTY-THIRD EACSL ANNUAL CONFERENCE ON COMPUTER SCIENCE LOGIC (CSL) AND THE TWENTY-NINTH ANNUAL ACM/IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS) | 2014年
关键词
Type Systems; Type-and-Effect Systems; Temporal Properties; Liveness; MODAL MU-CALCULUS; MODEL CHECKING; SYSTEM; TREES;
D O I
10.1145/2603088.2603127
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
We describe the construction of an abstract lattice from a given Buchi automata. The abstract lattice is finite and has the following key properties. (i) There is a Galois connection between it and the (infinite) lattice of languages of finite and infinite words over a given alphabet. (ii) The abstraction is faithful with respect to acceptance by the automaton. (iii) Least fixpoints and omega-iterations (but not in general greatest fixpoints) can be computed on the level of the abstract lattice. This allows one to develop an abstract interpretation capable of checking whether finite and infinite traces of a (recursive) program are accepted by a policy automaton. It is also possible to cast this analysis in form of a type and effect system with the effects being elements of the abstract lattice. While the resulting decidability and complexity results are known (regular model checking for pushdown systems) the abstract lattice provides a new point of view and enables smooth integration with data types, objects, higher-order functions which are best handled with abstract interpretation or type systems. We demonstrate this by generalising our type-and-effect systems to object-oriented programs and higher-order functions.
引用
收藏
页数:10
相关论文
共 50 条
  • [21] An abstract interpretation toolkit for μCRL
    Valero Espada, Miguel
    van de Pol, Jaco
    FORMAL METHODS IN SYSTEM DESIGN, 2007, 30 (03) : 249 - 273
  • [22] An abstract interpretation toolkit for μCRL
    Miguel Valero Espada
    Jaco van de Pol
    Formal Methods in System Design, 2007, 30 : 249 - 273
  • [23] An Abstract Interpretation Framework for Termination
    Cousot, Patrick
    Cousot, Radhia
    POPL 12: PROCEEDINGS OF THE 39TH ANNUAL ACM SIGPLAN-SIGACT SYMPOSIUM ON PRINCIPLES OF PROGRAMMING LANGUAGES, 2012, : 245 - 257
  • [24] An Abstract Interpretation Framework for Termination
    Cousot, Patrick
    Cousot, Radhia
    ACM SIGPLAN NOTICES, 2012, 47 (01) : 245 - 257
  • [25] Abstract interpretation of reactive systems
    Dams, D
    Gerth, R
    Grumberg, O
    ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 1997, 19 (02): : 253 - 291
  • [26] Test reactive systems with Buchi automata: acceptance condition coverage criteria and performance evaluation
    Zeng, Bolong
    Tan, Li
    2015 IEEE 16TH INTERNATIONAL CONFERENCE ON INFORMATION REUSE AND INTEGRATION, 2015, : 380 - 387
  • [27] LTL Formulae to Buchi Automata Translation Using on-the-Fly De-generalization
    Shan Laixiang
    Qin Zheng
    CHINESE JOURNAL OF ELECTRONICS, 2015, 24 (04) : 674 - 678
  • [28] Inference of ranking functions for proving temporal properties by abstract interpretation
    Urban, Caterina
    Mine, Antoine
    COMPUTER LANGUAGES SYSTEMS & STRUCTURES, 2017, 47 : 77 - 103
  • [29] Abstract Interpretation under Speculative Execution
    Wu, Meng
    Wang, Chao
    PROCEEDINGS OF THE 40TH ACM SIGPLAN CONFERENCE ON PROGRAMMING LANGUAGE DESIGN AND IMPLEMENTATION (PLDI '19), 2019, : 802 - 815
  • [30] Refining Model Checking by Abstract Interpretation
    Cousot P.
    Cousot R.
    Automated Software Engineering, 1999, 6 (1) : 69 - 95