BEGIN:VCALENDAR
CALSCALE:GREGORIAN
VERSION:2.0
X-WR-TIMEZONE:Europe/Paris
METHOD:PUBLISH
PRODID:-//LIP6//www.lip6.fr//FR
X-WR-CALNAME;VALUE=TEXT:Séminaire LIP6
X-LIC-LOCATION:Europe/Paris
BEGIN:VTIMEZONE
TZID:Europe/Paris
BEGIN:DAYLIGHT
TZOFFSETFROM:+0100
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
DTSTART:19810329T020000
TZNAME:GMT+02:00
TZOFFSETTO:+0200
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0200
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
DTSTART:19961027T030000
TZNAME:GMT+01:00
TZOFFSETTO:+0100
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
SUMMARY:Abstract Interpretation of Temporal Safety Effects of Higher 
 Order Programs
ORGANIZER;CN=Antoine Mine:MAILTO:Antoine.Mine@lip6.fr
ATTENDEE;CN=Eric Koskinen (Stevens Institute of Technology);CUTYPE=IN
 DIVIDUAL;PARTSTAT=ACCEPTED:mailto:Antoine.Mine@lip6.fr
DESCRIPTION:In recent years temporal verification has been increasing
 ly applied to higher-order programs. Some researchers have developed 
 automated approaches via higher-order recursion schemes, reductions t
 o fair-termination or constrained Horn clauses, while others have ext
 ended type and effect systems to reason about liveness properties. De
 spite these works, today's automated tools are often limited to somew
 hat small examples. 
  In this talk I will discuss our recent work on 
 a new abstract interpretation-based approach to verify temporal safet
 y properties of recursive, higher-order programs. We begin with a new
  automata-based “abstract effect domain” for summarizing context-
 sensitive dependent effects, capable of abstracting relations between
  the program environment and the automaton control state. Our analysi
 s includes a new transformer for abstracting event prefixes to automa
 tically computed context-sensitive effect summaries, and is instantia
 ted in a type-and-effect system grounded in abstract interpretation. 
 Since the analysis is parametric on the automaton, we next instantiat
 e it to a broader class of history/register (or “accumulator”) au
 tomata, beyond finite state automata to express some context-free pro
 perties, input-dependency, event summation, resource usage, cost, equ
 al event magnitude, etc.
  We implemented a prototype evDrift that com
 putes dependent effect summaries (and validates assertions) for OCaml
 -like recursive higher-order programs. As a basis of comparison, we d
 escribe reductions to assertion checking for higher-order but effect-
 free programs, and demonstrate that our approach outperforms prior to
 ols Drift, RCaml/Spacer, MoCHi, and ReTHFL. Overall, across a set of 
 23 benchmarks, Drift verified 12 benchmarks, RCaml/Spacer verified 6,
  MoCHi verified 11, ReTHFL verified 18, and evDrift verified 21; evDr
 ift also achieved a 6.3x, 5.3x, 16.8x, and 6.4x speedup over Drift, R
 Caml/Spacer, MoCHi, and ReTHFL, respectively, on those benchmarks tha
 t both tools could solve.
  This work appeared in OOPSLA 2025 and is j
 oint with Mihai Nicola, Chaitanya Agarwal, and Thomas Wies.
DTSTAMP:20260423T212545Z
DTSTART;TZID=Europe/Paris:20260519T110000
DURATION:PT2H
URL;VALUE=URI:https://www.lip6.fr/liens/organise-fiche.php?ident=O1238
UID:LIP6/SEM/O1238
LOCATION:Salle 428, couloir 26-00, 4 place Jussieu - 75005 Paris
GEO:48.84669;2.354759
END:VEVENT
END:VCALENDAR