Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
malta13 [2013/06/16 23:17] cesar.sanchez |
malta13 [2013/06/17 15:19] pace |
||
---|---|---|---|
Line 40: | Line 40: | ||
| 16.00-16.30 | //Filip Konecni:// Underapproximation of Procedure Summaries for Integer Programs | | | 16.00-16.30 | //Filip Konecni:// Underapproximation of Procedure Summaries for Integer Programs | | ||
| 16.30-17.00 | //Paul Jackson:// Auditing User-provided Axioms in Software Verification Conditions | | | 16.30-17.00 | //Paul Jackson:// Auditing User-provided Axioms in Software Verification Conditions | | ||
- | | 17:00-17:30 | Discussion Session: Cross-fertilization between Logic Programming and CLP with Horn Clause Verification | | + | | 17:00-17:30 | //David Monniaux:// TBA | |
+ | | 17:30-18:00 | Discussion Session: Cross-fertilization between Logic Programming and CLP with Horn Clause Verification | | ||
===== General Information ===== | ===== General Information ===== | ||
Line 233: | Line 234: | ||
** Contract Analysis ** | ** Contract Analysis ** | ||
//Gordon J. Pace// | //Gordon J. Pace// | ||
+ | |||
+ | The analysis of contracts to regulating interactive systems poses various challenges, but | ||
+ | is closely linked to the notions of concurrency and synchrony. We present a number of | ||
+ | recent results which take an automaton-based approach to model such contracts. We show how | ||
+ | obligations, permissions and prohibitions can be formalised and how the norms on one of the | ||
+ | parties sometimes imposes constraints on the other. Such formalisation allows for a clean | ||
+ | notion of contract strictness and a derived notion of contract conflict that is enriched | ||
+ | with issues arising from party interdependence. | ||
+ | |||
+ | //Joint work with Fernando Schapachnik and Gerardo Schneider.// | ||
---- | ---- |