Differences

This shows you the differences between two versions of the page.

--- malta13 [2013/06/16 23:17]
cesar.sanchez
+++ malta13 [2013/06/19 23:32]
cesar.sanchez
@@ Line 11: / Line 11: @@
 === Sunday, 16 June 2013 ===
 | 10.00-10.30 | //Christian Colombo:// Verifying Web Applications: From Business Level Specifications to Automated Model-Based Testing |
-| 10.30-11.00 | //Julian Samborski-Forlese:// TBA |
+| 10.30-11.00 | //Julian Samborski-Forlese:// Simulation Relations for Rich Acceptance Conditions |
 | 11.00-11.30 | **Coffee break** |
 | 11.30-12.00 | //Tarmo Uustalu:// Coinductive big-step semantics for concurrency |
@@ Line 30: / Line 32: @@
 | 09.00-10.00 | Invited Speaker: **Manuel Hermenegildo** |
 | 10.00-10.30 | **Coffee break** |
-| 10.30-11.00 | //Tewodros Beyene:// Solving Existentially Quantfied Horn Clauses |
+| 10.30-11.00 | {{:malta13-beyene.pdf|//Tewodros Beyene:// Solving Existentially Quantfied Horn Clauses}} |
 | 11.00-11.30 | //Boriss Selajev:// Scaling dynamic logic for intermediate states |
 | 11.30-12.00 | //Ondrej Lengal:// Fully Automated Shape Analysis Based on Forest Automata |
@@ Line 40: / Line 42: @@
 | 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 |
-| 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 with CLP and Horn Clause Verification |
 ===== General Information =====
@@ Line 103: / Line 106: @@
 //Christian Colombo//
+While the verification of web-based applications is crucial due to their often security-critical nature, it is considerably challenging due to their complex and dynamical nature. The current state of the art involves automated test execution where a test platform automatically interacts with a web application and asserts the expected behaviour. Still, test cases are typically generated manually, particularly when it comes to directing the test to exercise particular execution paths. In this presentation, we propose a novel combination of the QuickCheck testcase generation tool with web-based applications: QuickCheck exploits an executable automata-based specification to drive and assert the application in an automated yet non-random fashion. However, writing the specification is non-trivial and requires manual intervention. To this end, we propose a means of generating QuickCheck specifications from Cucumber specifications – a commonly used high level specification language for communicating with business stakeholders.
 ----
@@ Line 233: / Line 236: @@
 ** Contract Analysis **
 //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.//
 ----