BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Memento EPFL//
BEGIN:VEVENT
SUMMARY:Liveness of Randomised Parameterised Systems under Arbitrary Sched
 ulers
DTSTART:20160714T140000
DTEND:20160714T153000
DTSTAMP:20260407T043642Z
UID:714c1d548b96f8e23899a575b486e547ee14603f820d65a020120f74
CATEGORIES:Conferences - Seminars
DESCRIPTION:by Philipp RuemmerABSTRACT\nWe consider the problem of verifyi
 ng liveness for systems with a finite\,\nbut unbounded\, number of process
 es\, commonly known as\nparameterised systems. Typical examples of such sy
 stems include\ndistributed protocols (e.g. for the dining philosopher prob
 lem).\nUnlike the case of verifying safety\, proving liveness is still\nco
 nsidered extremely challenging\, especially in the presence of\nrandomness
  in the system. In this paper we consider liveness under\narbitrary (inclu
 ding unfair) schedulers\, which is often considered a\ndesirable property 
 in the literature of self-stabilising systems. In\nthis paper we introduce
  an automatic method of proving liveness\nfor randomised parameterised sys
 tems under arbitrary schedulers.\nViewing liveness as a two-player reachab
 ility game (between Scheduler\nand Process)\, our method is a CEGAR approa
 ch that synthesises a progress\nrelation for Process that can be symbolica
 lly represented as a\nfinite-state automaton. The method incrementally con
 structs a\nprogress relation\, exploiting both Angluin's $L*$ algorithm an
 d\nSAT-solvers. Our experiments show that our algorithm is able to prove\n
 liveness automatically for well-known randomised distributed protocols\,\n
 including Lehmann-Rabin Randomised Dining Philosopher Protocol and\nrandom
 ised self-stabilising protocols (such as the Israeli-Jalfon\nProtocol). To
  the best of our knowledge\, this is the first\nfully-automatic method tha
 t can prove liveness for randomised protocols.\nJoint work with Anthony W.
  Lin.SPEAKER BIOGRAPHY\nPhilipp Ruemmer is an assistant professor at Uppsa
 la University\, Sweden.\nHe received his doctorate in Computer Science fro
 m Chalmers University\nand Gothenburg University in 2008. Before joining U
 ppsala University as\nan assistant professor\, he has been research assist
 ant at the Oxford\nUniversity Computing Laboratory. His research interests
  include various\ndirections in program verification\, theorem proving and
  SMT reasoning\,\nand application of such methods in the area of embedded 
 systems. Philipp\nreceived the Oscar Prize of Uppsala University in 2013\,
  for\ncontributions to the field of program correctness\, and the IJCAR be
 st\npaper award in 2014\; the theorem prover Princess resulting from his\n
 research won the TFA division of the theorem proving competition CASC in\n
 2012.More information
LOCATION:BC 410 https://plan.epfl.ch/?room==BC%20410
STATUS:CONFIRMED
END:VEVENT
END:VCALENDAR