Isabelle/HOL Related Projects
- 2007 Formalization of pre* for DPNs
- Dec. 2007 Program Conflict Analysis
- Jan. 2009 Isabelle Formalization of Hedge-Constrained pre* and DPNs with Locks
- Nov. 2009 Isabelle Collections Framework
- Nov. 2009 Tree Automata
Formalization of pre* for DPNs
Peter Lammich2007
(Preliminary version, not yet published)
Abstract
We present a formalization of Dynamic Pushdown Networks (DPNs) and the automata based algorithm for computing backward reachability sets using Isabelle/HOL.
Dynamic pushdown networks are an abstract model for multithreaded, interprocedural programs with dynamic thread creation that was presented by Bouajjani, Müller-Olm and Touili in 2005.
We formalize the notion of a DPN in Isabelle and describe the algorithm for computing the $pre^*$-set from a regular set of configurations, and prove its correctness. We first give a nondeterministic description of the algorithm, from that we then infer a deterministic one, from which we can generate executable code using Isabelle's code-generation tool.
Proof Document
Proof Outline
Isabelle Sources (Not stripped, contains some unrelated/obsolete stuff)
TODO-List until final version:
- Make efficient implementation, using collection's framework. The current implementatioon is executable, but really slow.
- Perhaps extend to witness computation: The saturation algorithm can compute a tree-regular representation of all executions that lead from a start to an end configuration.
- Perhaps extend to weighted DPN (WDPN), a DPN model where transitions are assigned weights, and one computes the join of the weights of all executions.
Program Conflict Analysis
Peter Lammich and Markus Müller-OlmDec. 2007
In AFP, the entry can be found here
See also the related paper Conflict Analysis of Programs with Procedures, Dynamic Thread Creation, and Monitors.
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.
Proof Outline (from AFP)
Proof Document (from AFP)
Isabelle Sources (from AFP)
Isabelle Formalization of Hedge-Constrained pre* and DPNs with Locks
Peter LammichJan. 2009
Published as technical report.
See also the related paper Predecessor Sets of Dynamic Pushdown Networks with Tree-Regular Constraints.
Abstract
Dynamic Pushdown Networks (DPNs) are a model for concurrent
programs with recursive procedures and thread creation. We formalize
a true-concurrency semantics for DPNs. Executions of this semantics
have a tree structure. We show the relation of our semantics to
the original interleavings semantics. We then show how to compute
predecessor sets of regular sets of con gurations w.r.t. tree-regular
constraints on the execution.
Acquisition histories have been introduced by Kahlon et al. to
model-check parallel pushdown systems with well-nested locks , but
without thread creation. We generalize acquisistion histories to be
used with DPNs. For this purpose, our tree-based semantics can be
naturally applied. Moreover, the generalized acquisition histories enable
us to characterize the (tree-based) executions that have a schedule
that is valid w.r.t. locks, thus obtaining an algorithm to compute locksensitive
predecessor sets.
Proof Outline
Proof Document
Isabelle Sources
Isabelle Collections Framework
Peter LammichNov. 2009
In AFP, the entry can be found here
Abstract
This development provides an efficient, extensible, machine checked collections framework. The library adopts the concepts of interface, implementation and generic algorithm from object-oriented programming and implements them in Isabelle/HOL. The framework features the use of data refinement techniques to refine an abstract specification (using high-level concepts like sets) to a more concrete implementation (using collection datastructures, like red-black-trees). The code-generator of Isabelle/HOL can be used to generate efficient code.
Proof Outline (from AFP)
Proof Document (from AFP)
Isabelle Sources (from AFP)
Userguide
Tree Automata
Peter LammichNov. 2009
In AFP, the entry can be found here
Abstract
This work presents a machine-checked tree automata library for Standard-ML, OCaml and Haskell. The algorithms are efficient by using appropriate data structures like RB-trees. The available algorithms for non-deterministic automata include membership query, reduction, intersection, union, and emptiness check with computation of a witness for non-emptiness. The executable algorithms are derived from less-concrete, non-executable algorithms using data-refinement techniques. The concrete data structures are from the Isabelle Collections Framework. Moreover, this work contains a formalization of the class of tree-regular languages and its closure properties under set operations.
Proof Outline (from AFP)
Proof Document (from AFP)
Isabelle Sources (from AFP)
Old version
Proof DocumentIsabelle Sources
Kill/Gen Analysis for Programs with Procedures and Thread Creation
Peter LammichMay 2006
Formalization of kill/gen forward analysis for programs with Procedures and Thread Creation
The formalization was done related to my diploma thesis, and later extended, but never put into a
consistent shape suitable for publication.
Our paper Precise Fixpoint-Based Analysis of Programs with Thread-Creation and Procedures describes (a generalization of) the analysis.
- Aktuelles
-
- Wochenplan
- Stellen FB10
- Stellen extern
- Studieren:
- Prüfungsamt
- BSc/MSc Hinweise
- Prüfungsordnung BSc Informatik
- Fachspezifische Bestimmungen 2-Fach BSc (Lehramt)
- HIS/LSF/Vorlesungen
- Arbeitsgruppen
- Computer Vision and Pattern Recognition
- Datenbanken¸ Informationssysteme und Workflow-Management
- Parallele und Verteilte Systeme (PVS)
- Routing in selbstorg. Funknetzwerken (DIRC)
- Softcomputing
- Softwareentwicklung und Verifikation
- Visualisierung und Computergrafik
- Didaktik der Informatik
