[Club2] Invitation: Formal Verification of an Executable LTL Model Checker wi... @ Wed Jun 1, 2016 14:00 - 15:00 (Club2)

[julianbrunner at gmail.com]

You have been invited to the following event.

Title: Formal Verification of an Executable LTL Model Checker with Partial  
Order Reduction
Authors: Julian Brunner, Peter Lammich
Speaker: Julian Brunner
Type: NFM rehearsal talk

Abstract:
We present a formally verified and executable on-the-fly LTL model checker  
that uses ample set partial order reduction. The verification is done using  
the proof assistant Isabelle/HOL and covers everything from the abstract  
correctness proof down to the generated SML code.
Building on Doron Peled's paper "Combining Partial Order Reductions with  
On-the-Fly Model-Checking", we formally prove abstract correctness of ample  
set partial order reduction. This theorem is independent of the actual  
reduction algorithm. We then verify a reduction algorithm for a simple but  
expressive fragment of PROMELA. We use static partial order reduction,  
which allows separating the partial order reduction and the model checking  
algorithms regarding both the correctness proof and the implementation.  
Thus, the CAVA model checker that we verified in previous work can be used  
as a back end with only minimal changes. Finally, we generate executable  
SML code using a stepwise refinement approach. We test our model checker on  
some examples, observing the effectiveness of the partial order reduction  
algorithm.
When: Wed Jun 1, 2016 14:00 – 15:00 Berlin
Where: MI 00.09.038 (Turing)
Calendar: Club2
Who:
     * julianbrunner at gmail.com - creator
     * club2 at mailbroy.informatik.tu-muenchen.de

Event details:  
https://www.google.com/calendar/event?action=VIEW&eid=YXZuZzNjNGxoZHJjZmhhajJndm5vbTFhMHMgY2x1YjJAbWFpbGJyb3kuaW5mb3JtYXRpay50dS1tdWVuY2hlbi5kZQ&tok=NTIjc2U2ZWJlM3RvZmY0Y2g1bm11bmlibTVtOThAZ3JvdXAuY2FsZW5kYXIuZ29vZ2xlLmNvbWMyZjU1MmFmZTc4MGQxMzc5M2U5YmQ2NmIwZTY2ZDViZTM0MDEyYzM&ctz=Europe/Berlin&hl=en

Invitation from Google Calendar: https://www.google.com/calendar/

You are receiving this courtesy email at the account  
club2 at mailbroy.informatik.tu-muenchen.de because you are an attendee of  
this event.

To stop receiving future updates for this event, decline this event.  
Alternatively you can sign up for a Google account at  
https://www.google.com/calendar/ and control your notification settings for  
your entire calendar.

Forwarding this invitation could allow any recipient to modify your RSVP  
response. Learn more at  
https://support.google.com/calendar/answer/37135#forwarding
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/club2/attachments/20160525/ecca2f62/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: text/calendar
Size: 2341 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/club2/attachments/20160525/ecca2f62/attachment.ics>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: invite.ics
Type: application/ics
Size: 2387 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/club2/attachments/20160525/ecca2f62/attachment.bin>