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

  Browse A-Z

Log in

University Account External (via Google)

🔐 Log In

Information on

Subscribing to talksdetails Finding a talkdetails Adding a talkdetails Disseminating talksdetails Help and Documentationdetails

ℹī¸ Information

Horn Clauses for Verification and Synthesis

Download to your calendar using vCal

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

ī‚§ 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:

Note that ex-directory lists are not shown.

Other lists

Department of Biochemistry, Sanger building, Lecture theatre, Tennis Court Road Seminar Room 2, Alan Reece Building Institute for Manufacturing (IfM), 17 Charles Babbage Road, Cambridge CB3 0FS Bateson Room, Department of Genetics, Downing Site

Other talks

Title to be confirmed Title TBC CPH IRC and PHI Reproducibility In Astrophysical Simulations: The AGORA Initiative and a 14-Year Human Experiment (In Memory of Joel Primack) Title to be confirmed Title TBC
 

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