Precise thread-modular abstract interpretation of concurrent programs using relational interference abstractions

DOI10.1007/978-3-319-52234-0_21MaRDI QIDQ2961579zbMATH OpenOpenAlexFDO

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

zbMATH Keywords

abstract interpretationprogram verificationconcurrent programsrely-guarantee methodsnumeric invariant generationthread-modular analyses

Mathematics Subject Classification ID

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)

Recommendations

• Relational thread-modular static value analysis by abstract interpretation
• Relational thread-modular abstract interpretation under relaxed memory models
• Improving thread-modular abstract interpretation
• Precise Thread-Modular Verification
• On interference abstractions

Cites work

• scientific article; zbMATH DE number 1953274 (Why is no real title available?)
• A new solution of Dijkstra's concurrent programming problem
• Counterexample-guided abstraction refinement for symmetric concurrent programs
• How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs
• Local proofs for global safety properties
• Myths about the mutual exclusion problem
• On the verification problem for weak memory models
• Partial-order methods for the verification of concurrent systems. An approach to the state-explosion problem
• Relational thread-modular static value analysis by abstract interpretation
• Static analysis of run-time errors in embedded critical parallel C programs
• Static analysis of run-time errors in embedded real-time parallel C programs
• Thread-Modular Verification Is Cartesian Abstract Interpretation
• Tools and Algorithms for the Construction and Analysis of Systems

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

Describes a project that uses

Uses Software

• ASTREE
• Threader
• SymmPa
• Apron

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)