The YOGI Project: Software Property Checking via Static Analysis and Testing

被引：0
|
作者：
Nori, Aditya V.
Rajamani, Sriram K.
Tetali, SaiDeep
Thakur, Aditya V.
机构：
来源：
TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PROCEEDINGS | 2009年 / 5505卷
关键词：
D O I：
暂无
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
We present YOGI, a tool that checks properties of C programs by combining static analysis and testing. YOGI implements the DASH algorithm which performs verification by combining directed testing and abstraction. We have engineered YOGI in such a way that it plugs into Microsoft's Static Driver Verifier framework. We have used this framework to run YOGI on 69 Windows Vista drivers with 85 properties. We find that the new algorithm enables YOGI to scale much better than SLAM, which is the current engine driving Microsoft's Static Driver Verifier.
引用
收藏
页码：178 / 181
页数：4
相关论文
共 50 条
  • [21] A precise and scalable static checking approach for temporal safety property
    Huo, W. (huowei@ict.ac.cn), 1600, Science Press (35):
  • [22] Check 'n' crash: Combining static checking and testing
    Csallner, Christoph
    Smaragdakis, Yannis
    Proc Int Conf Software Eng, (422-431):
  • [23] Check 'n' crash: Combining static checking and testing
    Csallner, C
    Smaragdakis, Y
    ICSE 05: 27TH INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING, PROCEEDINGS, 2005, : 422 - 431
  • [24] Dominance Testing Via Model Checking
    Santhanam, Ganesh Ram
    Basu, Samik
    Honavar, Vasant
    PROCEEDINGS OF THE TWENTY-FOURTH AAAI CONFERENCE ON ARTIFICIAL INTELLIGENCE (AAAI-10), 2010, : 357 - 362
  • [25] Regression testing via model checking
    Xu, LH
    Dias, M
    Richardson, D
    PROCEEDINGS OF THE IASTED INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING, 2004, : 402 - 407
  • [26] Comprehensive Static Analysis for Configurable Software via Combinatorial Instantiation
    Yan, Dong
    Pan, Linjie
    Yan, Rongjie
    Yan, Jun
    Zhang, Jian
    2017 IEEE 41ST ANNUAL COMPUTER SOFTWARE AND APPLICATIONS CONFERENCE (COMPSAC), VOL 1, 2017, : 67 - 74
  • [27] Checking Laws of the Blockchain with Property-Based Testing
    Chepurnoy, Alexander
    Rathee, Mayank
    2018 IEEE 1ST INTERNATIONAL WORKSHOP ON BLOCKCHAIN ORIENTED SOFTWARE ENGINEERING (IWBOSE), 2018, : 40 - 47
  • [28] Static Analysis versus Model Checking
    Nielson, Flemming
    ERCIM NEWS, 2010, (83): : 6 - 6
  • [29] A Survey on Static Analysis and Model Checking
    Garcia-Ferreira, Ivan
    Laorden, Carlos
    Santos, Igor
    Garcia Bringas, Pablo
    INTERNATIONAL JOINT CONFERENCE SOCO'14-CISIS'14-ICEUTE'14, 2014, 299 : 443 - 452
  • [30] Project viability assessment for support of software testing via Bayesian graphical modelling
    Coolen, FPA
    Goldstein, M
    Wooff, DA
    SAFETY AND RELIABILITY, VOLS 1 AND 2, 2003, : 417 - 422
12345