### Abstract

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.

### License

BSD License

### Topics

- Computer science/Programming languages/Static analysis

### Session Program-Conflict-Analysis

- Misc
- Interleave
- ConsInterleave
- AcquisitionHistory
- LTS
- ThreadTracking
- Flowgraph
- Semantics
- Normalization
- ConstraintSystems
- MainResult

### Used by

- Flow Networks and the Min-Cut-Max-Flow Theorem

## Cite

×

Program-Conflict-Analysis-AFP

    @article{Program-Conflict-Analysis-AFP,
      author  = {Peter Lammich and Markus Müller-Olm},
      title   = {Formalization of Conflict Analysis of Programs with Procedures, Thread Creation, and Monitors},
      journal = {Archive of Formal Proofs},
      month   = {December},
      year    = {2007},
      note    = {\url{https://isa-afp.org/entries/Program-Conflict-Analysis.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- May 27, 2015 : Isabelle2015
- Aug 28, 2014 : Isabelle2014
- Dec 11, 2013 : Isabelle2013-2
- Nov 17, 2013 : Isabelle2013-1
- Mar 2, 2013 : Isabelle2013
- Feb 16, 2013 : Isabelle2013
- May 24, 2012 : Isabelle2012
- Oct 11, 2011 : Isabelle2011-1
- Feb 11, 2011 : Isabelle2011
- Jul 1, 2010 : Isabelle2009-2
- Dec 12, 2009 : Isabelle2009-1
- Apr 29, 2009 : Isabelle2009
- Jun 10, 2008 : Isabelle2008
- Dec 20, 2007 : Isabelle2007