| Home |
| About |
| Submission |
| Updating Entries |
| Using Entries |
| Search |
| Statistics |
| Index |
| Download |
Formalization of Conflict Analysis of Programs with Procedures, Thread Creation, and Monitors
| Title: | Formalization of Conflict Analysis of Programs with Procedures, Thread Creation, and Monitors |
| Authors: | Peter Lammich and Markus Müller-Olm |
| Submission date: | 2007-12-14 |
| 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. |
| BibTeX: |
@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 = dec,
year = 2007,
note = {\url{http://isa-afp.org/entries/Program-Conflict-Analysis.html},
Formal proof development},
ISSN = {2150-914x},
}
|
| License: | BSD License |
| Used by: | Flow_Networks |
| Status: [ok] | This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations. |
|
Proof outline Proof document |
| Browse theories |
| Download this entry |