Jasmin Christian Blanchette wrote:
Hi all,This is just a reminder that we are all encouraged to let the mailing list know about your Isabelle-based work on the mailing list. This is especially important if you publish your work elsewhere than at the ITP conference or on the Archive of Formal Proof. Other people on the mailing list might be doing something similar without knowing. (This happened recently with an Isabelle-related paper presented at LPAR.)
Ok, I'll try to give a short overview of the Isabelle-related stuff that is going on in our group:Now it's your turn!
Apart from what we published on AFP and/or ITP (ProgramConflictAnalysis, Isabelle Collection Framework, Tree Automata, BinomialQueues, FingerTrees)
+ in Preparation: Dijkstra's algorithm as an example for using ICF and PriorityQueues in a complex algorithm,
we work on program analysis for concurrent programs, and verify many of our techniques in Isabelle/HOL.
The document: Formalization of pre* for DPNs (http://cs.uni-muenster.de/sev/staff/lammich/isabelle/#dpn_prestar) formalizes an automata-based model-checking algorithm for dynamic pushdown networks, and generates
(very inefficient) executable code.
The technical report: Isabelle Formalization of Hedge-Constrained pre* and DPNs with Locks (http://cs.uni-muenster.de/sev/staff/lammich/isabelle/#pca) formalizes an analysis of Dynamic Pushdown Networks with Locks, an abstract model for parallel programs. We are currently extending the results there. On the Isabelle/HOL side, the long-term goal is to derive an executable analyser, that is specified as a datalog-like logical program, that can be efficiently solved with BDD-based techniques (cf. eg. the bddbddb - project)
Moreover, we are exploring how to combine approaches from separation logic with the ImperativeHOL framework. The motivation is to develop a library of efficient imperative datastructures for ImperativeHOL, that allows for nice, modular proofs (An ImperativeHOL-analogon of the Isabelle Collection Framework).