[Club2] Julian's talk moved to 13:30! Julian Brunner: Wed., July 9, 13:30, Room: Turing (00.09.38)

[Andrei Popescu]

Best regards, 

   Andrei 





On Monday, July 7, 2014 12:59 AM, Andrei Popescu <uuomul at yahoo.com> wrote:

 

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,
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/club2/attachments/20140708/8e44ae49/attachment.html>