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 条
  • [1] Software testing via model checking
    Belli, F
    Güldali, B
    COMPUTER AND INFORMATION SCIENCES - ISCIS 2004, PROCEEDINGS, 2004, 3280 : 907 - 916
  • [2] The SLAM project: Debugging system software via static analysis
    Ball, T
    Rajamani, SK
    ACM SIGPLAN NOTICES, 2002, 37 (01) : 1 - 3
  • [3] Combining static analysis and model checking for software analysis
    Brat, G
    Visser, W
    16TH ANNUAL INTERNATIONAL CONFERENCE ON AUTOMATED SOFTWARE ENGINEERING (ASE 2001), PROCEEDINGS, 2001, : 262 - 269
  • [4] Static analysis versus software model checking for bug finding
    Engler, D
    Musuvathi, M
    VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION, PROCEEDINGS, 2004, 2937 : 191 - 210
  • [5] CLP based static property checking
    Li, T
    Guo, Y
    Li, SK
    AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, PROCEEDINGS, 2004, 3299 : 495 - 498
  • [6] Probabilistic Model Checking GitHub Repositories for Software Project Analysis
    Jo, Suhee
    Kwon, Ryeonggu
    Kwon, Gihwon
    APPLIED SCIENCES-BASEL, 2024, 14 (03):
  • [7] Property checking driven abstract interpretation-based static analysis
    Massé, D
    VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION, 2003, 2575 : 56 - 69
  • [8] Applying model checking to destructive testing and analysis of software system
    Kumamoto, Hiroki
    Mizuno, Takahisa
    Narita, Kensuke
    Nishizaki, Shin-ya
    Journal of Software, 2013, 8 (05) : 1254 - 1261
  • [9] Static checking of interrupt-driven software
    Brylow, D
    Damgaard, N
    Palsberg, J
    PROCEEDINGS OF THE 23RD INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING, 2001, : 47 - 56
  • [10] In-circuit software testing - beyond static analysis
    Beach, M
    ELECTRONIC ENGINEERING, 2000, 72 (881): : 45 - +
12345