[Club2] talk by Dmitriy Traytel: Friday, Sept. 20, 11:30, Room Turing (00.09.38)

[Andrei Popescu]

Dear All,  

This Friday Dmitriy will rehearse his ICFP talk on 
a verified decision procedure for monadic second-order logic.     

http://icfpconference.org/icfp2013

Cheers, 
 Andrei 


Verified Decision Procedures for MSO on Words Based on Derivatives of Regular Expressions
Dmitriy Traytel
joint work with Tobias Nikow
================================================================
Friday, Sept. 20, 11:30, Room Turing (00.09.38)

Monadic second-order logic on finite words (MSO) is a decidable
yet expressive logic into which many decision problems can be
encoded. Since MSO formulas correspond to regular languages,
equivalence of MSO formulas can be reduced to the equivalence
of some regular structures (e.g. automata). This paper presents
a verified functional decision procedure for MSO formulas that
is not based on automata but on regular expressions. Functional
languages are ideally suited for this task: regular expressions are
data types and functions on them are defined by pattern matching
and recursion and are verified by structural induction.

Decision procedures for regular expression equivalence have
been formalized before, usually based on Brzozowski derivatives.
Yet, for a straightforward embedding of MSO formulas into regular
expressions an extension of regular expressions with a projection
operation is required. We prove total correctness and completeness
of an equivalence checker for regular expressions extended in that
way. We also define a language-preserving translation of formulas
into regular expressions with respect to two different semantics
of MSO. Our results have been formalized and verified in the
theorem prover Isabelle. Using Isabelle’s code generation facility,
this yields purely functional, formally verified programs that decide
equivalence of MSO formulas.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/club2/attachments/20130918/6a8d1d7f/attachment.html>