[go: up one dir, main page]

Li et al., 2025 - Google Patents

Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs

Li et al., 2025

View PDF
Document ID
290907791684555706
Author
Li K
Aguirre A
Gregersen S
Haselwarter P
Tassarotti J
Birkedal L
Publication year
Publication venue
Proceedings of the ACM on Programming Languages

External Links

Snippet

We present Coneris, the first* higher-order concurrent separation logic* for reasoning about error probability bounds of higher-order concurrent probabilistic programs with higher-order state. To support modular reasoning about concurrent (non-probabilistic) program modules …
Continue reading at dl.acm.org (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/44—Arrangements for executing specific programmes
    • G06F9/4421—Execution paradigms
    • G06F9/4428—Object-oriented
    • 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/52—Programme synchronisation; Mutual exclusion, e.g. by means of semaphores; Contention for resources among tasks
    • 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/466—Transaction processing
    • 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/48—Programme initiating; Programme switching, e.g. by interrupt
    • G06F9/4806—Task transfer initiation or dispatching
    • 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
    • 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/43—Checking; Contextual analysis
    • G06F8/436—Semantic checking
    • G06F8/437—Type checking
    • 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
    • G06F8/44—Encoding
    • 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
    • G06F17/30286—Information retrieval; Database structures therefor; File system structures therefor in structured data stores
    • G06F17/30587—Details of specialised database models
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F8/00—Arrangements for software engineering
    • G06F8/30—Creation or generation of source code
    • G06F8/31—Programming languages or programming paradigms
    • G06F8/315—Object-oriented languages
    • 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
    • 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
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F8/00—Arrangements for software engineering
    • G06F8/10—Requirements analysis; Specification techniques

Similar Documents

Publication Publication Date Title
Turon et al. GPS: Navigating weak memory with ghosts, protocols, and separation
Liang et al. Modular verification of linearizability with non-fixed linearization points
Raad et al. On library correctness under weak memory consistency: Specifying and verifying concurrent libraries under declarative consistency models
Liang et al. Progress of concurrent objects with partial methods
Kuper et al. Taming the parallel effect zoo: Extensible deterministic parallelism with LVish
Colvin et al. Designing a semantic model for a wide-spectrum language with concurrency
Frumin et al. ReLoC Reloaded: A Mechanized Relational Logic for Fine-Grained Concurrency and Logical Atomicity
Kragl et al. The civl verifier
Hobor et al. Barriers in concurrent separation logic: now with tool support!
Moine et al. A high-level separation logic for heap space under garbage collection
Zilberstein et al. Outcome separation logic: Local reasoning for correctness and incorrectness with computational effects
Derrick et al. Verifying correctness of persistent concurrent data structures: a sound and complete method
Dodds et al. Verifying custom synchronization constructs using higher-order separation logic
Peterson et al. A transactional correctness tool for abstract data types
Haselwarter et al. Approximate Relational Reasoning for Higher-Order Probabilistic Programs
Aguirre et al. Error credits: Resourceful reasoning about error bounds for higher-order probabilistic programs
Li et al. Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs
Gregersen et al. Almost-Sure Termination by Guarded Refinement
Groves et al. Trace-based derivation of a scalable lock-free stack algorithm
Lee et al. Lilo: A Higher-Order, Relational Concurrent Separation Logic for Liveness
Ghica et al. Synchronous game semantics via round abstraction
Reinhard et al. Ghost Signals: Verifying Termination of Busy Waiting: Verifying Termination of Busy Waiting
Hinrichsen Sessions and Separation
Reinhard et al. Ghost Signals: Verifying Termination of Busy-Waiting (Extended Version)
Buhr et al. Implicit-signal monitors