Verifying properties of hardware and software by predicate abstraction and model checking

被引：0
|
作者：
Bryant, RE [1 ]
Rajamani, SK [1 ]
机构：
[1] Carnegie Mellon Univ, Pittsburgh, PA 15213 USA
来源：
ICCAD-2004: INTERNATIONAL CONFERENCE ON COMPUTER AIDED DESIGN, IEEE/ACM DIGEST OF TECHNICAL PAPERS | 2004年
关键词：
formal verification; predicate abstraction; model checking; symbolic execution; decision procedures;
D O I：
10.1109/ICCAD.2004.1382615
中图分类号：
TP3 [计算技术、计算机技术];
学科分类号：
0812 ;
摘要：
This tutorial describes automatic techniques for formally verifying hardware and software by creating Boolean abstractions of the underlying unbounded system state variables.
引用
收藏
页码：437 / 438
页数：2
相关论文
共 50 条
  • [1] Combining Predicate and Numeric Abstraction for Software Model Checking
    Gurfinkel, Arie
    Chaki, Sagar
    2008 FORMAL METHODS IN COMPUTER-AIDED DESIGN, 2008, : 127 - 135
  • [2] Combining predicate and numeric abstraction for software model checking
    Gurfinkel A.
    Chaki S.
    International Journal on Software Tools for Technology Transfer, 2010, 12 (06) : 409 - 427
  • [3] Algorithms for Software Model Checking: Predicate Abstraction vs. IMPACT
    Beyer, Dirk
    Wendler, Philipp
    PROCEEDINGS OF THE 12TH CONFERENCE ON FORMAL METHODS IN COMPUTER-AIDED DESIGN (FMCAD 2012), 2012, : 106 - 113
  • [4] Competent predicate abstraction in model checking
    Li Li
    XiaoYu Song
    Ming Gu
    XiangYu Luo
    Science China Information Sciences, 2011, 54 : 258 - 267
  • [5] Competent predicate abstraction in model checking
    Li Li
    Song XiaoYu
    Gu Ming
    Luo XiangYu
    SCIENCE CHINA-INFORMATION SCIENCES, 2011, 54 (02) : 258 - 267
  • [6] Competent predicate abstraction in model checking
    LI Li1
    2Key Laboratory for Information System Security
    3School of Software
    4Department of ECE
    ScienceChina(InformationSciences), 2011, 54 (02) : 258 - 267
  • [7] Model Checking Recursive Programs with Exact Predicate Abstraction
    Gurfinkel, Arie
    Wei, Ou
    Chechik, Marsha
    AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, PROCEEDINGS, 2008, 5311 : 95 - +
  • [8] Shape analysis through predicate abstraction and model checking
    Dams, D
    Namjoshi, KS
    VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION, 2003, 2575 : 310 - 323
  • [9] An improved method of k-induction combined with predicate abstraction and CEGAR for software model checking
    Wang, Shun
    Du, Ye
    Han, Zhen
    CLUSTER COMPUTING-THE JOURNAL OF NETWORKS SOFTWARE TOOLS AND APPLICATIONS, 2019, 22 (Suppl 3): : S6219 - S6229
  • [10] An improved method of k-induction combined with predicate abstraction and CEGAR for software model checking
    Shun Wang
    Ye Du
    Zhen Han
    Cluster Computing, 2019, 22 : 6219 - 6229
12345