Precise thread-modular abstract interpretation of concurrent programs using relational interference abstractions
DOI10.1007/978-3-319-52234-0_21zbMATH Open1484.68050OpenAlexW2569507975MaRDI QIDQ2961579FDOQ2961579
Authors: Raphaël Monat, Antoine Miné 
Publication date: 21 February 2017
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://hal.inria.fr/hal-01490178/file/vmcai17.pdf
Recommendations
abstract interpretationprogram verificationconcurrent programsrely-guarantee methodsnumeric invariant generationthread-modular analyses
Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19)
Cites Work
- Title not available (Why is that?)
- Partial-order methods for the verification of concurrent systems. An approach to the state-explosion problem
- Myths about the mutual exclusion problem
- How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs
- A new solution of Dijkstra's concurrent programming problem
- Tools and Algorithms for the Construction and Analysis of Systems
- On the verification problem for weak memory models
- Counterexample-guided abstraction refinement for symmetric concurrent programs
- Local proofs for global safety properties
- Relational thread-modular static value analysis by abstract interpretation
- Static analysis of run-time errors in embedded critical parallel C programs
- Thread-Modular Verification Is Cartesian Abstract Interpretation
- Static analysis of run-time errors in embedded real-time parallel C programs
Cited In (12)
- Thread-Local Semantics and Its Efficient Sequential Abstractions for Race-Free Programs
- Abstract interpretation of trace semantics for concurrent calculi
- Relational thread-modular abstract interpretation under relaxed memory models
- Precise Thread-Modular Verification
- Thread Quantification for Concurrent Shape Analysis
- Improving thread-modular abstract interpretation
- Thread-modular analysis of release-acquire concurrency
- Abstract interpretation with unfoldings
- Relational thread-modular static value analysis by abstract interpretation
- Multithreaded-Cartesian abstract interpretation of multithreaded recursive programs Is polynomial
- On interference abstractions
- Clustered relational thread-modular abstract interpretation with local traces
Uses Software
This page was built for publication: Precise thread-modular abstract interpretation of concurrent programs using relational interference abstractions
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2961579)
