English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools annual

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

There is a close connection between data-flow analysis and model checking asobserved and studied in the nineties by Steffen and Schmidt. This indicatesthat automata-based analysis techniques developed in the realm ofinfinite-state model checking can be applied as data-flow analyzers thatinterpret complex control structures, which motivates the development of suchanalysis techniques for ever more complex models. One approach proposed byEsparza and Knoop is based on computation of predecessor or successor sets forsets of automata configurations. Our goal is to adapt and exploit this approachfor analysis of multi-threaded Java programs. Specifically, we consider themodel of Monitor-DPNs for concurrent programs. Monitor-DPNs precisely modelunbounded recursion, dynamic thread creation, and synchronization viawell-nested locks with finite abstractions of procedure- and thread-localstate. Previous work on this model showed how to compute regular predecessorsets of regular configurations and tree-regular successor sets of a fixedinitial configuration. By combining and extending different previouslydeveloped techniques we show how to compute tree-regular successor sets oftree-regular sets. Thereby we obtain an iterable, lock-sensitive forwardreachability analysis. We implemented the analysis for Java programs andapplied it to information flow control and data race detection.

Iterable Forward Reachability Analysis of Monitor-DPNs