University of Cambridge > Talks.cam > Microsoft Research Cambridge, public talks > Horn Clauses for Verification and Synthesis

Horn Clauses for Verification and Synthesis

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

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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2022 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity