BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Horn Clauses for Verification and Synthesis  - Andrey Rybalchenko\
 , Microsoft Research Cambridge
DTSTART:20160825T093000Z
DTEND:20160825T101500Z
UID:TALK67024@talks.cam.ac.uk
CONTACT:44515
DESCRIPTION:We will show how Horn constraints can be used to describe veri
 fication and synthesis problems\, and how such constraints can be solved e
 fficiently. In particular\, we will demonstrate how cardinality operators 
 help to reason about quantitative properties and carry out counting-based 
 correctness arguments\, which are useful for the verification of informati
 on flow properties and parametrized systems. We also consider non-stratifi
 ed negation and aggregation\, and their use for modelling network protocol
 s. 
LOCATION:Auditorium\, Microsoft Research Ltd\, 21 Station Road\, Cambridge
 \, CB1 2FB
END:VEVENT
END:VCALENDAR