Chaki et al., 2018 - Google Patents

BDD-based symbolic model checking

Chaki et al., 2018

Document ID
12999019684802751875
Author
Chaki S
Gurfinkel A
Publication year
Publication venue
Handbook of Model Checking

External Links

Snippet

Symbolic model checking based on Binary Decision Diagrams (BDDs) is one of the most celebrated breakthroughs in the area of formal verification. It was originally proposed in the context of hardware model checking, and advanced the state of the art in model-checking …
Continue reading at link.springer.com (other versions)

Classifications

    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F17/00—Digital computing or data processing equipment or methods, specially adapted for specific functions
    • G06F17/50—Computer-aided design
    • G06F17/5009—Computer-aided design using simulation
    • G06F17/504—Formal methods
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F17/00—Digital computing or data processing equipment or methods, specially adapted for specific functions
    • G06F17/50—Computer-aided design
    • G06F17/5045—Circuit design
    • G06F17/505—Logic synthesis, e.g. technology mapping, optimisation
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F17/00—Digital computing or data processing equipment or methods, specially adapted for specific functions
    • G06F17/50—Computer-aided design
    • G06F17/5009—Computer-aided design using simulation
    • G06F17/5022—Logic simulation, e.g. for logic circuit operation
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F17/00—Digital computing or data processing equipment or methods, specially adapted for specific functions
    • G06F17/50—Computer-aided design
    • G06F17/5068—Physical circuit design, e.g. layout for integrated circuits or printed circuit boards
    • G06F17/5081—Layout analysis, e.g. layout verification, design rule check
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F9/00—Arrangements for programme control, e.g. control unit
    • G06F9/06—Arrangements for programme control, e.g. control unit using stored programme, i.e. using internal store of processing equipment to receive and retain programme
    • G06F9/44—Arrangements for executing specific programmes
    • G06F9/445—Programme loading or initiating
    • G06F9/44589—Programme code verification, e.g. Java bytecode verification, proof-carrying code
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F8/00—Arrangements for software engineering
    • G06F8/40—Transformations of program code
    • G06F8/41—Compilation
    • G06F8/44—Encoding
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F9/00—Arrangements for programme control, e.g. control unit
    • G06F9/06—Arrangements for programme control, e.g. control unit using stored programme, i.e. using internal store of processing equipment to receive and retain programme
    • G06F9/46—Multiprogramming arrangements
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F11/00—Error detection; Error correction; Monitoring
    • G06F11/36—Preventing errors by testing or debugging software
    • G06F11/3604—Software analysis for verifying properties of programs
    • G06F11/3608—Software analysis for verifying properties of programs using formal methods, e.g. model checking, abstract interpretation
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F17/00—Digital computing or data processing equipment or methods, specially adapted for specific functions
    • G06F17/10—Complex mathematical operations
    • G06F17/11—Complex mathematical operations for solving equations, e.g. nonlinear equations, general mathematical optimization problems
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F2217/00—Indexing scheme relating to computer aided design [CAD]
    • G06F2217/78—Power analysis and optimization
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F2217/00—Indexing scheme relating to computer aided design [CAD]
    • G06F2217/08—Multi-objective optimization
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F21/00—Security arrangements for protecting computers, components thereof, programs or data against unauthorised activity
    • G06F21/50—Monitoring users, programs or devices to maintain the integrity of platforms, e.g. of processors, firmware or operating systems
    • G06F21/57—Certifying or maintaining trusted computer platforms, e.g. secure boots or power-downs, version controls, system software checks, secure updates or assessing vulnerabilities

Similar Documents

Publication Publication Date Title
Chaki et al. BDD-based symbolic model checking
Komuravelli et al. SMT-based model checking for recursive programs
Bryant Binary decision diagrams
Seger et al. Formal verification by symbolic evaluation of partially-ordered trajectories
Bloem et al. Efficient decision procedures for model checking of linear time logic properties
US6163876A (en) Method for verification of RTL generated from scheduled behavior in a high-level synthesis flow
US7930659B2 (en) Software verification
US6301687B1 (en) Method for verification of combinational circuits using a filtering oriented approach
Ganai et al. SAT-based scalable formal verification solutions
Pnueli et al. Liveness and acceleration in parameterized verification
Winter Model Checking for Abstract State Machines.
Grumberg et al. Distributed symbolic model checking for μ-calculus
Bryant et al. Boolean satisfiability with transitivity constraints
Horváth et al. Dynamic constraint satisfaction problems over models
Faghih et al. SMT-based synthesis of distributed self-stabilizing systems
Bryant et al. Boolean satisfiability with transitivity constraints
Baneres et al. A recursive paradigm to solve Boolean relations
Penczek et al. Abstractions and partial order reductions for checking branching properties of time Petri nets
Bryant et al. Convergence testing in term-level bounded model checking
Barnat et al. Temporal verification of simulink diagrams
Bloem et al. Symbolic implementation of alternating automata
Bultan BDD vs. constraint-based model checking: An experimental evaluation for asynchronous concurrent systems
Yavuz-Kahveci et al. Action Language Verifier: An infinite-state model checker for reactive software specifications
Kong et al. On accelerating smt-based bounded model checking of hstm designs
Dixon et al. Temporal logic with capacity constraints