Horn Clauses for Verification and Synthesis

Add to your list(s) Download to your calendar using vCal

• Andrey Rybalchenko, Microsoft Research Cambridge
• Thursday 25 August 2016, 10:30-11:15
• Auditorium, Microsoft Research Ltd, 21 Station Road, Cambridge, CB1 2FB.

If you have a question about this talk, please contact lecturescam.

 Please note, this event may be recorded. Microsoft will own the copyright of any recording and reserves the right to distribute it as required.

We will show how Horn constraints can be used to describe verification and synthesis problems, and how such constraints can be solved efficiently. 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 information flow properties and parametrized systems. We also consider non-stratified negation and aggregation, and their use for modelling network protocols.

This talk is part of the Microsoft Research Cambridge, public talks series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Auditorium, Microsoft Research Ltd, 21 Station Road, Cambridge, CB1 2FB
• Cambridge Centre for Data-Driven Discovery (C2D3)
• Cambridge talks
• Chris Davis' list
• Guy Emerson's list
• Interested Talks
• Microsoft Research Cambridge, public talks
• Optics for the Cloud
• PMRFPS's
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• ndk22's list
• ob366-ai4er
• personal list
• rp587

Note that ex-directory lists are not shown.