[Club2] talk by Julian Brunner: Wed., July 9, 11:00, Room: Turing (00.09.38)

[Andrei Popescu]

Dear All, 

On Wednesday we start our marathon with Julian's Master thesis presentation.

Best regards,
   Andrei 


Implementation and Verification of Partial Order Reduction for On-The-Fly Model Checking
Julian Brunner
======================================================================
Wed., July 9, 11:00, Room: Turing (00.09.38)

We present our effort of formally verifying the on-the-fly partial
order reduction technique described in [Combining Partial Order
Reductions with On-the-Fly Model-Checking, Doron Peled, Formal Methods
in System Design, 1996] using the proof assistant Isabelle in
conjunction with the HOL logic library. First, we briefly introduce
the idea of partial order reduction. The on-the-fly partial order
reduction algorithm we want to formalize is built on top of an
off-line partial order reduction algorithm. Thus, we first present the
implementation and verification of significant parts of this off-line
partial order reduction algorithm. Next, we describe the architecture
of the correctness proof for the on-the-fly partial order reduction
algorithm. There, we point out a problem with one of the proof steps
and provide a counterexample showing that the proof of this step is
not valid. Finally, we give an overview of the formal theories and
present ideas for further work.



On Sunday, July 6, 2014 12:35 PM, Tobias Nipkow <nipkow at in.tum.de> wrote:
 


Andrei,

When you announce Julian's talk on Monday, please do so separately and send a
copy to Javier who may also want to forward it to his group.

Thanks
Tobias
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/club2/attachments/20140706/324f270d/attachment.html>