[go: up one dir, main page]

Ball et al., 2001 - Google Patents

Parameterized verification of multithreaded software libraries

Ball et al., 2001

View PDF
Document ID
9041547351940000172
Author
Ball T
Chaki S
Rajamani S
Publication year
Publication venue
International Conference on Tools and Algorithms for the Construction and Analysis of Systems

External Links

Snippet

The growing popularity of multi-threading has led to a great number of software libraries that support access by multiple threads. We present Local/Global Finite State Machines (LGFSMs) as a model for a certain class of multithreaded libraries. We have developed a …
Continue reading at www.microsoft.com (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
    • 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/455—Emulation; Software simulation, i.e. virtualisation or emulation of application or operating system execution engines
    • 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
    • G06F11/00—Error detection; Error correction; Monitoring
    • G06F11/36—Preventing errors by testing or debugging software
    • G06F11/362—Software debugging
    • 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
    • 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
    • G06F11/00—Error detection; Error correction; Monitoring
    • G06F11/30—Monitoring
    • G06F11/34—Recording or statistical evaluation of computer activity, e.g. of down time, of input/output operation; Recording or statistical evaluation of user activity, e.g. usability assessment
    • 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
    • G06F21/00—Security arrangements for protecting computers, components thereof, programs or data against unauthorised activity
    • G06F21/10—Protecting distributed programs or content, e.g. vending or licensing of copyrighted material
    • G06F21/12—Protecting executable software
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F2221/00—Indexing scheme relating to security arrangements for protecting computers, components thereof, programs or data against unauthorised activity

Similar Documents

Publication Publication Date Title
Ball et al. Parameterized verification of multithreaded software libraries
Kuncak et al. Role analysis
US5937195A (en) Global control flow treatment of predicated code
Sekar et al. Model-carrying code: a practical approach for safe execution of untrusted applications
US7496791B2 (en) Mock object generation by symbolic execution
Hackett et al. Region-based shape analysis with tracked locations
Cooper et al. A methodology for procedure cloning
Somenzi Binary decision diagrams
Ramalingam et al. Deriving specialized program analyses for certifying component-client conformance
Hoover Alphonse: Incremental computation as a programming abstraction
Ni et al. A formal model and risk assessment method for security-critical real-time embedded systems
Touati et al. Testing language containment for ω-automata using BDDs
Omicini et al. Formal specification and enactment of security policies through Agent Coordination Contexts
Duan et al. A model for abstract process specification, verification and composition
Watanabe et al. Compositional value iteration with pareto caching
Ball et al. Checking Temporal Properties of Ыoftware with Boolean Programs
Leggett et al. Integrating user knowledge with information from parallelisation tools to facilitate the automatic generation of efficient parallel FORTRAN code
Nicolay et al. Static detection of user-specified security vulnerabilities in client-side javascript
Stern Algorithmic techniques in verification by explicit state enumeration
Emeka et al. A Practical Model Driven Approach for Designing Security Aware RESTful Web APIs Using SOFL
Ferrari et al. Model checking for nominal calculi
Wing et al. Extending Ina Jo with temporal logic
Karjoth et al. LOEWE: a LOTOS engineering workbench
Seidl et al. How to win first-order safety games
Ruys Spin beginners’ tutorial