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 条
  • [21] Using predicate abstraction to reduce object-oriented programs for model checking
    Visser, Willem, 2000, ACM, New York
  • [22] SAT based predicate abstraction for hardware verification
    Clarke, E
    Talupur, M
    Veith, H
    Wang, D
    THEORY AND APPLICATIONS OF SATISFIABILITY TESTING, 2004, 2919 : 78 - 92
  • [23] Relative completeness of abstraction refinement for software model checking
    Ball, T
    Podelski, A
    Rajamani, SK
    TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANAYLSIS OF SYSTEMS, PROCEEDINGS, 2002, 2280 : 158 - 172
  • [24] Formal Hardware/Software Co-Verification by Interval Property Checking with Abstraction
    Nguyen, Minh D.
    Wedler, Markus
    Stoffel, Dominik
    Kunz, Wolfgang
    PROCEEDINGS OF THE 48TH ACM/EDAC/IEEE DESIGN AUTOMATION CONFERENCE (DAC), 2011, : 510 - 515
  • [25] Model checking software via abstraction of loop transitions
    Sharygina, N
    Browne, JC
    FUNDAMENTAL APPROACHES TO SOFTWARE ENGINEERING, PROCEEDINGS, 2003, 2621 : 325 - 340
  • [26] Predicate Abstraction and Refinement for Verifying Multi-Threaded Programs
    Gupta, Ashutosh
    Popeea, Corneliu
    Rybalchenko, Andrey
    ACM SIGPLAN NOTICES, 2011, 46 (01) : 331 - 344
  • [27] Word level predicate abstraction and refinement for verifying RTL verilog
    Jain, H
    Kroening, D
    Sharygina, N
    Clarke, E
    42ND DESIGN AUTOMATION CONFERENCE, PROCEEDINGS 2005, 2005, : 445 - 450
  • [28] Predicate Abstraction and Refinement for Verifying Multi-Threaded Programs
    Gupta, Ashutosh
    Popeea, Corneliu
    Rybalchenko, Andrey
    POPL 11: PROCEEDINGS OF THE 38TH ANNUAL ACM SIGPLAN-SIGACT SYMPOSIUM ON PRINCIPLES OF PROGRAMMING LANGUAGES, 2011, : 331 - 344
  • [29] A symbolic model checking approach to verifying satellite onboard software
    Gan, Xiang
    Dubrovin, Jori
    Heljanko, Keijo
    SCIENCE OF COMPUTER PROGRAMMING, 2014, 82 : 44 - 55
  • [30] Building and verifying hardware at a higher level of abstraction
    Cheng, Tim
    IEEE DESIGN & TEST OF COMPUTERS, 2009, 26 (04): : 2 - 2
12345