SPLIT: A Compositional LTL Verifier

被引：0
|
作者：
Cohen, Ariel [1 ]
Namjoshi, Kedar S. [2 ]
Sa'ar, Yaniv [3 ]
机构：
[1] NYU, New York, NY 10012 USA
[2] Alcatel Lucent, Bell Labs, Murray Hill, NJ USA
[3] Weizmann Inst Sci, Rehovot, Israel
来源：
COMPUTER AIDED VERIFICATION, PROCEEDINGS | 2010年 / 6174卷
基金：
欧洲研究理事会;
关键词：
LOCAL PROOFS;
D O I：
暂无
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
This paper describes SPLIT, a compositional verifier for safety and general LTL., properties of shared-variable, multi-threaded programs. The foundation is a computation of compact local invariants, one for each process, which are used for constructing a proof for the property. An automatic refinement procedure gradually exposes more local information, until a decisive result (proof/disproof) is obtained.
引用
收藏
页码：558 / +
页数：2
相关论文
共 50 条
  • [1] Compositional Algorithms for LTL Synthesis
    Filiot, Emmanuel
    Jin, Nayiong
    Raskin, Jean-Francois
    [J]. AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, 2010, 6252 : 112 - 127
  • [2] Compositional Safety LTL Synthesis
    Bansal, Suguman
    De Giacomo, Giuseppe
    Di Stasio, Antonio
    Li, Yong
    Vardi, Moshe Y.
    Zhu, Shufang
    [J]. VERIFIED SOFTWARE. THEORIES, TOOLS AND EXPERIMENTS, VSTTE 2022, 2023, 13800 : 1 - 19
  • [3] Antichains and compositional algorithms for LTL synthesis
    Emmanuel Filiot
    Naiyong Jin
    Jean-François Raskin
    [J]. Formal Methods in System Design, 2011, 39 : 261 - 296
  • [4] Antichains and compositional algorithms for LTL synthesis
    Filiot, Emmanuel
    Jin, Naiyong
    Raskin, Jean-Francois
    [J]. FORMAL METHODS IN SYSTEM DESIGN, 2011, 39 (03) : 261 - 296
  • [5] From LTL to deterministic automata: A safraless compositional approach
    Esparza J.
    Křetínský J.
    Sickert S.
    [J]. Křetínský, Jan (jan.kretinsky@tum.de), 1600, Springer Science and Business Media, LLC (49): : 219 - 271
  • [6] From LTL to Deterministic Automata: A Safraless Compositional Approach
    Esparza, Javier
    Kretinsky, Jan
    [J]. COMPUTER AIDED VERIFICATION, CAV 2014, 2014, 8559 : 192 - 208
  • [7] Tally Keeping-LTL: An LTL Semantics for Quantitative Evaluation of LTL Specifications
    Khoury, Raphael
    Halle, Sylvain
    [J]. 2018 IEEE INTERNATIONAL CONFERENCE ON INFORMATION REUSE AND INTEGRATION (IRI), 2018, : 495 - 502
  • [8] The quote verifier
    Keyes, R
    [J]. ANTIOCH REVIEW, 2006, 64 (02): : 256 - 266
  • [9] The Gradual Verifier
    Arlt, Stephan
    Rubio-Gonzalez, Cindy
    Ruemmer, Philipp
    Schaef, Martin
    Shankar, Natarajan
    [J]. NASA FORMAL METHODS, NFM 2014, 2014, 8430 : 313 - 327
  • [10] BRAQUE - THE VERIFIER
    ANDRAL, JL
    [J]. CIMAISE, 1994, 41 (230): : 67 - 70
12345