Clustered relational thread-modular abstract interpretation with local traces

DOI10.1007/978-3-031-30044-8_2MaRDI QIDQ6535225zbMATH OpenFDO

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

Publication date 24 November 2023

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-031-30044-8_2

zbMATH Keywords

clusterscollecting local trace semanticsconcurrencydynamic thread creationthread-modular relational abstract interpretation

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Semantics in the theory of computing (68Q55) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Improving thread-modular abstract interpretation
• Precise thread-modular abstract interpretation of concurrent programs using relational interference abstractions
• Relational thread-modular static value analysis by abstract interpretation
• Relational thread-modular abstract interpretation under relaxed memory models
• Thread-Modular Verification Is Cartesian Abstract Interpretation

Cites work

• A survey on product operators in abstract interpretation
• Abstract interpretation of mobile systems
• Affine relationships among variables of a program
• An Abstract Domain Extending Difference-Bound Matrices with Disequality Constraints
• Fast numerical program analysis with reinforcement learning
• Fast polyhedra abstract domain
• scientific article; zbMATH DE number 1953274 (Why is no real title available?)
• scientific article; zbMATH DE number 1738295 (Why is no real title available?)
• scientific article; zbMATH DE number 2090856 (Why is no real title available?)
• Improving thread-modular abstract interpretation
• Learning a variable-clustering strategy for Octagon from labeled data generated by a static analysis
• Logahedra: a new weakly relational domain
• May-Happen-in-Parallel Analysis with Returned Futures
• Pentagons: a weakly relational abstract domain for the efficient validation of array accesses
• Precise thread-modular abstract interpretation of concurrent programs using relational interference abstractions
• Programming Languages and Systems
• Qualified Data Flow Problems
• Relational abstract domain of weighted hexagons
• Relational string abstract domains
• Relational thread-modular abstract interpretation under relaxed memory models
• Some ways to reduce the space dimension in polyhedra computations
• Static analysis of communicating processes using symbolic transducers
• Static analysis of run-time errors in embedded real-time parallel C programs
• The octagon abstract domain
• The reduced relative power operation on abstract domains
• Thread-Local Semantics and Its Efficient Sequential Abstractions for Race-Free Programs
• Thread-modular analysis of release-acquire concurrency
• Three improvements to the top-down solver
• Two variables per linear inequality as an abstract domain
• Verification of parameterized concurrent programs by modular reasoning about data and control
• Why does Astrée scale up?

This page was built for publication: Clustered relational thread-modular abstract interpretation with local traces

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