[go: up one dir, main page]

Nalumasu et al., 1995 - Google Patents

Explicit-enumeration based verification made memory-efficient

Nalumasu et al., 1995

View PDF
Document ID
475982828905085925
Author
Nalumasu R
Gopalakrishnan G
Publication year
Publication venue
Proceedings of ASP-DAC'95/CHDL'95/VLSI'95 with EDA Technofair

External Links

Snippet

We investigate new techniques for reducing the memory requirements of an on-the-fly model checking tool that employs explicit enumeration. Two techniques are studied in depth: exploiting symmetries in the model, and exploiting sequential regions in the model. These …
Continue reading at collections.lib.utah.edu (PDF) (other versions)

Classifications

    • 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
    • G06F9/54—Interprogramme communication; Intertask communication
    • G06F9/546—Message passing systems or structures, e.g. queues
    • 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/4421—Execution paradigms
    • 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
    • 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
    • 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
    • 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/30—Information retrieval; Database structures therefor; File system structures therefor
    • 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
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F7/00—Methods or arrangements for processing data by operating upon the order or content of the data handled
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F15/00—Digital computers in general; Data processing equipment in general
    • G06F15/16—Combinations of two or more digital computers each having at least an arithmetic unit, a programme unit and a register, e.g. for a simultaneous processing of several programmes
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06Q—DATA PROCESSING SYSTEMS OR METHODS, SPECIALLY ADAPTED FOR ADMINISTRATIVE, COMMERCIAL, FINANCIAL, MANAGERIAL, SUPERVISORY OR FORECASTING PURPOSES; SYSTEMS OR METHODS SPECIALLY ADAPTED FOR ADMINISTRATIVE, COMMERCIAL, FINANCIAL, MANAGERIAL, SUPERVISORY OR FORECASTING PURPOSES, NOT OTHERWISE PROVIDED FOR
    • G06Q10/00—Administration; Management

Similar Documents

Publication Publication Date Title
Bryant Binary decision diagrams
Ball et al. Automatic predicate abstraction of C programs
Biere Resolve and expand
Holzmann The model checker SPIN
Chaki et al. Efficient verification of sequential and concurrent C programs
Perrone et al. A model checker for bigraphs
Nakamura et al. A mathematical model of CPU
Holzmann Explicit-state model checking
Raimondi et al. Verification of multiagent systems via ordered binary decision diagrams: an algorithm and its implementation
van Hee et al. Resource-constrained workflow nets
Kupferman et al. Pushdown specifications
Wachter et al. Probabilistic model checking modulo theories
Emerson et al. Rapid parameterized model checking of snoopy cache coherence protocols
Holzmann et al. SPIN model checking: An introduction
Yahav et al. Automatically verifying concurrent queue algorithms
Nalumasu et al. Explicit-enumeration based verification made memory-efficient
Cousot et al. Verification of embedded software: Problems and perspectives
Ranise et al. Applying light-weight theorem proving to debugging and verifying pointer programs
US6526551B2 (en) Formal verification of a logic design through implicit enumeration of strongly connected components
Stern Algorithmic techniques in verification by explicit state enumeration
Engelhardt et al. Model checking knowledge and linear time: PSPACE cases
Hoare Software model checking
Donaldson et al. SPIN-to-GRAPE: a tool for analysing symmetry in Promela models
Nain et al. Synthesizing probabilistic composers
Huang et al. An efficient algorithm for match pair approximation in message passing