Abstract interpretation with unfoldings

DOI10.1007/978-3-319-63390-9_11MaRDI QIDQ2164221zbMATH OpenOpenAlexFDO

Authors César Rodríguez, Vijay D'Silva, Daniel Kroening, Marcelo S. Sousa

Publication date 12 August 2022

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

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Abstract: We present and evaluate a technique for computing path-sensitive interference conditions during abstract interpretation of concurrent programs. In lieu of fixed point computation, we use prime event structures to compactly represent causal dependence and interference between sequences of transformers. Our main contribution is an unfolding algorithm that uses a new notion of independence to avoid redundant transformer application, thread-local fixed points to reduce the size of the unfolding, and a novel cutoff criterion based on subsumption to guarantee termination of the analysis. Our experiments show that the abstract unfolding produces an order of magnitude fewer false alarms than a mature abstract interpreter, while being several orders of magnitude faster than solver-based tools that have the same precision.

Recommendations

• On interference abstractions
• scientific article; zbMATH DE number 2104620
• Precise thread-modular abstract interpretation of concurrent programs using relational interference abstractions
• Verification of concurrent programs using Petri net unfoldings
• Relational thread-modular static value analysis by abstract interpretation

Cited in

(10)

• Thread-modular analysis of release-acquire concurrency
• Using abstract interpretation to correct synchronization faults
• Incremental Abstract Interpretation
• Abstract interpretation
• scientific article; zbMATH DE number 2104620 (Why is no real title available?)
• scientific article; zbMATH DE number 7453197 (Why is no real title available?)
• Sweeping in Abstract Interpretation
• On interference abstractions
• Causal Dataflow Analysis for Concurrent Programs
• Revisiting local time semantics for networks of timed automata

This page was built for publication: Abstract interpretation with unfoldings

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