[Club2] Invitation: Talk by Matthias Franze @ Wed Jan 14, 2015 13:00 - 14:00 (Club2)

[julianbrunner at gmail.com]

You have been invited to the following event.

Title: Talk by Matthias Franze
Title: A Purely-Functional, Proof-Producing, Incremental Algorithm for the  
Congruence Closure
Type: Bachelor's Thesis Talk

Abstract:
The Satisfiability Modulo Theories (SMT) problem is essential for
many verification and automated deduction tasks. One
approach to its solution is the DPLL(T) engine with specialized
solvers for each theory.

One such theory is equality of uninterpreted functions (EUF)
which is decidable by constructing the congruence closure of a
set of ground equations. We exhibit the development of an
algorithm for computing the incremental congruence closure in
a DPLL(T) environment, implemented purely-functionally in SML
and embedded in the SMT-solver "sel".
When: Wed Jan 14, 2015 13:00 - 14:00 Berlin
Where: MI 00.09.038 (Turing)
Calendar: Club2
Who:
     * Julian Brunner - creator
     * sascha.boehme at gmx.de
     * club2 at mailbroy.informatik.tu-muenchen.de

Event details:  
https://www.google.com/calendar/event?action=VIEW&eid=bWJyamh1cmtpNjFnOWd2aHBodWE4ZmkxbDAgY2x1YjJAbWFpbGJyb3kuaW5mb3JtYXRpay50dS1tdWVuY2hlbi5kZQ&tok=NTIjc2U2ZWJlM3RvZmY0Y2g1bm11bmlibTVtOThAZ3JvdXAuY2FsZW5kYXIuZ29vZ2xlLmNvbTk2MTA2ZTlhYzQ5NmZmNDhmMGMzY2ViZGM2MTI3MTliZDc2ZmIyYzk&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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/club2/attachments/20141218/3081fef2/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: text/calendar
Size: 2083 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/club2/attachments/20141218/3081fef2/attachment.ics>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: invite.ics
Type: application/ics
Size: 2130 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/club2/attachments/20141218/3081fef2/attachment.bin>