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 条
  • [41] Probabilistic abstraction for model checking: An approach based on property testing
    Laplante, Sophie
    Lassaigne, Richard
    Magniez, Frederic
    Peyronnet, Sylvain
    De Rougemont, Michel
    ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, 2007, 8 (04)
  • [42] Model checking software via abstraction of loop transitions
    Sharygina, N
    Browne, JC
    FUNDAMENTAL APPROACHES TO SOFTWARE ENGINEERING, PROCEEDINGS, 2003, 2621 : 325 - 340
  • [43] Model Checking Is Static Analysis of Modal Logic
    Nielson, Flemming
    Nielson, Hanne Riis
    FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATIONAL STRUCTURES, PROCEEDINGS, 2010, 6014 : 191 - 205
  • [44] Generating test items for checking illegal behaviors in software testing
    Hirayama, M
    Okayasu, J
    Yamamoto, T
    Mizuno, O
    Kikuno, T
    PROCEEDINGS OF THE NINTH ASIAN TEST SYMPOSIUM (ATS 2000), 2000, : 235 - 240
  • [45] An automated testing methodology based on self-checking software
    Reinhart, T
    Boettcher, C
    Wasserman, H
    PROCEEDINGS OF THE IEEE 1998 NATIONAL AEROSPACE AND ELECTRONICS CONFERENCE, 1998, : 205 - 212
  • [46] Formal software analysis - Emerging trends in software model checking
    Dwyer, Matthew B.
    Hatcliff, John
    Robby
    Pasareanu, Corina S.
    Visser, Willem
    FOSE 2007: FUTURE OF SOFTWARE ENGINEERING, 2007, : 120 - +
  • [47] Static property checking using ATPG v.s. BDD techniques
    Huang, CY
    Yang, BL
    Tsai, HC
    Cheng, KT
    INTERNATIONAL TEST CONFERENCE 2000, PROCEEDINGS, 2000, : 309 - 316
  • [48] Property-Based Testing - The ProTest Project
    Derrick, John
    Walkinshaw, Neil
    Arts, Thomas
    Earle, Clara Benac
    Cesarini, Francesco
    Fredlund, Lars-Ake
    Gulias, Victor
    Hughes, John
    Thompson, Simon
    FORMAL METHODS FOR COMPONENTS AND OBJECTS, 2010, 6286 : 250 - +
  • [49] Static Analysis of Software Executables
    Melski, David
    Teitelbaum, Tim
    Reps, Thomas
    CATCH 2009: CYBERSECURITY APPLICATIONS AND TECHNOLOGY CONFERENCE FOR HOMELAND SECURITY, PROCEEDINGS, 2009, : 97 - 102
  • [50] Static analysis and software assurance
    Wagner, D
    STATIC ANALYSIS, PROCEEDINGS, 2001, 2126 : 431 - 431
12345