BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Fencing off Go: Liveness and Safety for Channel-based Programming 
 - Nicholas Ng and Bernardo Toninho\, Imperial College
DTSTART:20161111T140000Z
DTEND:20161111T150000Z
UID:TALK67475@talks.cam.ac.uk
CONTACT:Dominic Mulligan
DESCRIPTION:Go is a production-level statically typed programming language
  whose\ndesign features explicit message-passing primitives and lightweigh
 t\nthreads\, enabling (and encouraging) programmers to develop concurrent 
 systems where components interact through communication more so than by lo
 ck-based shared memory concurrency.  Go can only detect global deadlocks a
 t runtime\, but provides no compile-time protection against all too common
  communication mismatches or partial deadlocks.\n\nThis talk presents a st
 atic verification framework for liveness and\nsafety of Go programs\, aime
 d at detecting communication errors and\ndeadlocks in a general class of r
 ealistic concurrent programs such as\nthose with unbounded thread creation
 \, dynamic channel creation and\nrecursion. Our work infers from a Go prog
 ram an abstract\nrepresentation of its communication patterns as a behavio
 ural type.\nWe define a symbolic execution semantics for types\, which all
 ows us to\ncheck for the absence of communication errors and liveness in a
  finite\nstate space.\n\nBy checking a syntactic restriction on channel us
 age in types\, dubbed\nfencing\, we ensure that programs are made up of fi
 nitely many\ndifferent communication patterns that may be repeated infinit
 ely many\ntimes\, ensuring decidability and soundness of our analyses.\n\n
 Our analysis and inference have been implemented in a publicly\navailable 
 tool-chain. At the end of the talk\, we do a short demo of our tool. \n\nh
 ttp://mrg.doc.ic.ac.uk/tools/gong/
LOCATION:FW26
END:VEVENT
END:VCALENDAR