BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//GREYC UMR CNRS 6072 - Groupe de Recherche en Informatique, Image, et Instrumentation de Caen - ECPv5.7.0//NONSGML v1.0//EN
CALSCALE:GREGORIAN
METHOD:PUBLISH
X-WR-CALNAME:GREYC UMR CNRS 6072 - Groupe de Recherche en Informatique, Image, et Instrumentation de Caen
X-ORIGINAL-URL:https://www.greyc.fr
X-WR-CALDESC:évènements pour GREYC UMR CNRS 6072 - Groupe de Recherche en Informatique, Image, et Instrumentation de Caen
BEGIN:VTIMEZONE
TZID:Europe/Paris
BEGIN:DAYLIGHT
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
TZNAME:CEST
DTSTART:20260329T010000
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
TZNAME:CET
DTSTART:20261025T010000
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20260120T104500
DTEND;TZID=Europe/Paris:20260120T114500
DTSTAMP:20260418T215431
CREATED:20251219T085001Z
LAST-MODIFIED:20260107T104620Z
UID:12013-1768905900-1768909500@www.greyc.fr
SUMMARY:Séminaire Algorithmique : « Eunoia: A Framework for SMT Proof Calculi »\, Hans-Jörg Schurr (Univ. of Iowa\, USA)
DESCRIPTION:Satisfiability Modulo Theories (SMT) solvers combine decision procedures for various theories into a homogeneous automated reasoning framework. They are an indispensable tools to solve formal verification and decision problems. To validate the SMT solver’s responses we can use proof certificates. However\, a major challenge is that different theories and decision procedures use different proof calculi. \nWe will discuss the novel Eunoia language which allows SMT developers to define proof rules precisely. The syntax of Eunoia resembles the standard SMT-LIB format. Proofs using Eunoia-defined rules can be checked using the dedicated Ethos proof checker. We specified all proof calculus of the industrial strength SMT solver cvc5 in Eunoia. We will also discuss ongoing efforts to provide a formal and mechanized type system for Eunoia\, and future directions for proof certificates for SMT solvers.
URL:https://www.greyc.fr/event/seminaire-algorithmique-hans-jorg-schurr-univ-of-iowa-usa/
LOCATION:Sciences 3- S3 351
CATEGORIES:Amacc,General,News,Séminaire Algo
END:VEVENT
END:VCALENDAR