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 Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

Nondeterminism in scheduling is the cardinal reason for difficulty in provingcorrectness of concurrent programs. A powerful proof strategy was recentlyproposed [6] to show the correctness of such programs. The approach captureddata-flow dependencies among the instructions of an interleaved and error-freeexecution of threads. These data-flow dependencies were represented by aninductive data-flow graph (iDFG), which, in a nutshell, denotes a set ofexecutions of the concurrent program that gave rise to the discovered data-flowdependencies. The iDFGs were further transformed in to alternative finiteautomatons (AFAs) in order to utilize efficient automata-theoretic tools tosolve the problem. In this paper, we give a novel and efficient algorithm todirectly construct AFAs that capture the data-flow dependencies in a concurrentprogram execution. We implemented the algorithm in a tool called ProofTraPar toprove the correctness of finite state cyclic programs under the sequentiallyconsistent memory model. Our results are encouranging and compare favorably toexisting state-of-the-art tools.

From Traces To Proofs: Proving Concurrent Program Safe