Improving thread-modular abstract interpretation

DOI10.1007/978-3-030-88806-0_18MaRDI QIDQ2145342zbMATH OpenOpenAlexFDO

Authors Michael Schwarz, Simmo Saan, Helmut Seidl, Kalmer Apinis, Julian Erhard, Vesal Vojdani

Publication date 17 June 2022

Full work available at URL https://arxiv.org/abs/2108.07613

zbMATH Keywords

concurrent systemsglobal invariantsside-effectscollecting trace semanticsthread-modular abstract interpretation

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Semantics in the theory of computing (68Q55) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Abstract: We give thread-modular non-relational value analyses as abstractions of a local trace semantics. The semantics as well as the analyses are formulated by means of global invariants and side-effecting constraint systems. We show that a generalization of the analysis provided by the static analyzer Goblint as well as a natural improvement of Antoine Min'e's approach can be obtained as instances of this general scheme. We show that these two analyses are incomparable w.r.t. precision and provide a refinement which improves on both precision-wise. We also report on a preliminary experimental comparison of the given analyses on a meaningful suite of benchmarks.

Recommendations

• Relational thread-modular static value analysis by abstract interpretation
• Precise thread-modular abstract interpretation of concurrent programs using relational interference abstractions
• Thread-Modular Verification Is Cartesian Abstract Interpretation
• scientific article; zbMATH DE number 2087567
• Thread-modular counterexample-guided abstraction refinement

Cites work

• scientific article; zbMATH DE number 6712238 (Why is no real title available?)
• A semantics for concurrent separation logic
• Communicating state transition systems for fine-grained concurrent resources
• Computer Aided Verification
• Dataflow analysis for datarace-free programs
• Fast and Accurate Static Data-Race Detection for Concurrent Programs
• Precise thread-modular abstract interpretation of concurrent programs using relational interference abstractions
• Relational thread-modular abstract interpretation under relaxed memory models
• Relational thread-modular static value analysis by abstract interpretation
• Resources, concurrency, and local reasoning
• Static Analysis Via Abstract Interpretation of the Happens-Before Memory Model
• Static analysis of run-time errors in embedded real-time parallel C programs
• Thread-Local Semantics and Its Efficient Sequential Abstractions for Race-Free Programs
• Time, clocks, and the ordering of events in a distributed system

Cited in

(4)

• scientific article; zbMATH DE number 1955854 (Why is no real title available?)
• Clustered relational thread-modular abstract interpretation with local traces
• Precise thread-modular abstract interpretation of concurrent programs using relational interference abstractions
• Relational thread-modular static value analysis by abstract interpretation

Describes a project that uses

Uses Software

• Goblint

This page was built for publication: Improving thread-modular abstract interpretation

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2145342)