BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Memento EPFL//
BEGIN:VEVENT
SUMMARY:The Quest for Systematic Predicate Abstraction
DTSTART:20170308T153000
DTEND:20170308T163000
DTSTAMP:20260407T230814Z
UID:76338f1b18cd79678d2bbda41666103adf0b04d15f541bc9ac2f655e
CATEGORIES:Conferences - Seminars
DESCRIPTION:by Philipp Ruemmer\n\nAbstract\nHeuristics for discovering pre
 dicates for abstraction are an essential part of CEGAR-based software mode
 l checkers or Horn solvers. Picking the right predicates affects the runti
 me of a model checker\, or determines if a model checker is able to solve 
 a verification task at all. This talk will summarise some of our research 
 on how to choose predicates in a systematic way. The first part of the pre
 sentation will explain how Craig interpolation\, one of the standard metho
 ds for refining abstractions\, can be adapted to take program-specific inf
 ormation or refinement heuristics into account. The second part will prese
 nt different methods to actually generate such program-specific informatio
 n: with the help of upfront static analysis of a program\, using domain-sp
 ecific acceleration techniques\, or using type-based analysis to extract v
 ariable roles.\n\nJoint work with Yulia Demyanova\, Jérôme Leroux\, Pavl
 e Subotic\, and Florian Zuleger.\n\nBio\nPhilipp Ruemmer is an assistant p
 rofessor at Uppsala University\, Sweden. He received his doctorate in Comp
 uter Science from Chalmers University and Gothenburg University in 2008. B
 efore joining Uppsala University as an assistant professor\, he has been r
 esearch assistant at the Oxford University Computing Laboratory. His resea
 rch interests include various directions in program verification\, theorem
  proving and SMT reasoning\, and application of such methods in the area o
 f embedded systems. Philipp received the Oscar Prize of Uppsala University
  in 2013\, for contributions to the field of program correctness\, and the
  IJCAR best paper award in 2014\; the theorem prover Princess resulting fr
 om his research won the TFA division of the theorem proving competition CA
 SC in 2012.\n\nMore information
LOCATION:BC 410 https://plan.epfl.ch/?room==BC%20410
STATUS:CONFIRMED
END:VEVENT
END:VCALENDAR