Email Gateway (Aug 18 2022 at 11:10): Email Gateway (Aug 18 2022 at 11:10):From: Tobias Nipkow <nipkow@in.tum.de>
We are pleased to announce that a new article (again on Threads) has
made it into the Archive of Formal Proofs:
Formalization of Conflict Analysis of Programs with Procedures, Thread
Creation, and Monitors
Peter Lammich
Markus Müller-Olm
In this work we formally verify the soundness and precision of a static
program analysis that detects conflicts (e.g. data races) in programs
with procedures, thread creation and monitors with the Isabelle theorem
prover. As common in static program analysis, our program model
abstracts guarded branching by nondeterministic branching, but
completely interprets the call-/return behavior of procedures,
synchronization by monitors, and thread creation. The analysis is based
on the observation that all conflicts already occur in a class of
particularly restricted schedules. These restricted schedules are suited
to constraint-system-based program analysis. The formalization is based
upon a flowgraph-based program model with an operational semantics as
reference point.
http://afp.sourceforge.net/entries/Program-Conflict-Analysis.shtml
PS I like the acknowledgement: "We also thank the people on the Isabelle
mailing list for quick and useful responses."
Last updated: May 03 2024 at 08:18 UTC