BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Memento EPFL//
BEGIN:VEVENT
SUMMARY:Causality-Based Abstract Interpretation = Super-Optimal DPOR + Abs
 traction
DTSTART:20171024T150000
DTEND:20171024T160000
DTSTAMP:20260406T172849Z
UID:eb688f767112025a87b8442f66de8e1ea1362ad7b58246bec3cf6fd0
CATEGORIES:Conferences - Seminars
DESCRIPTION:By Marcelo Sousa\n\nAbstract\nCausality-based abstract interpr
 etation is a new technique for computing\npath-sensitive interference cond
 itions during abstract interpretation of\nconcurrent programs. In lieu of 
 fixed point computation\, it uses prime event\nstructures to compactly rep
 resent causal dependence and interference between\nsequences of transforme
 rs. \nThe main contribution of the approach is an unfolding algorithm equ
 ivalent to a\nsuper-optimal DPOR that uses a new notion of independence to
  avoid redundant\ntransformer application\, thread-local fixed points to r
 educe the size of the\nunfolding\, and a novel cutoff criterion based on s
 ubsumption to guarantee\ntermination of the analysis. \nIn this talk\, I 
 will describe the main ideas behind causality-based AI and\nmotivate new d
 irections in the application of DPORs to further mitigate the\nstate explo
 sion problem.\n\nBio\nMarcelo Sousa is a PhD student at University of Oxfo
 rd under Daniel Kroening\nand Luke Ong. He has been investigating redundan
 cy-aware procedures in static\nanalysis\, compiler optimisations and state
 -space exploration methods with\napplications to the state explosion probl
 em in analysis of concurrent systems\nand relational verification. \nMarc
 elo is the sole recipient of the 2016 Google PhD Fellowship in Programming
 \nLanguages and Software Engineering.\n\nMore information\n\n\n 
LOCATION:BC 420 https://plan.epfl.ch/?room==BC%20420
STATUS:CONFIRMED
END:VEVENT
END:VCALENDAR