Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
malta13 [2013/06/17 15:55]
pace
malta13 [2014/09/17 11:03]
cesar.sanchez
Line 12: Line 12:
 === Sunday, 16 June 2013 === === 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 +^             ^ Title                 ^ Speaker ^ 
-| 11.00-11.30 | **Coffee break** | +| 10.00-10.30 | {{:malta13-colombo.pptx|Verifying Web Applications:​ From Business Level Specifications to Automated Model-Based Testing}} | Christian Colombo ​
-| 11.30-12.00 | //Tarmo Uustalu:// ​Coinductive big-step semantics for concurrency | +| 10.30-11.00 | {{:​malta13-samborski-forlese.pdf|Simulation Relations for Rich Acceptance Conditions}} | Julian Samborski-Forlese | 
-| 12.00-12.30 | //Enric Rodriguez-Carbonell:// To Encode or to Propagate? The Best Choice for Each Constraint in SAT | +| 11.00-11.30 | **Coffee break** ​|
-| 12.30-14.00 | **Lunch** | +| 11.30-12.00 | Coinductive big-step semantics for concurrency ​| Tarmo Uustalu ​
-| 14.00-14.30 | //Tayssir Touilli:// ​Model-checking for efficient malware detection ​+| 12.00-12.30 | {{:malta13-rodriguez-carbonell.pdf|To Encode or to Propagate? The Best Choice for Each Constraint in SAT}} | Enric Rodriguez-Carbonell ​
-| 14.30-15.00 | //Guillermo Perez:// Decidable Classes of Mean-Payoff Games with Imperfect Information | +| 12.30-14.00 | **Lunch** ​|
-| 15.00-15.30 | **Coffee break** | +| 14.00-14.30 | Model-checking for Efficient Malware Detection | Tayssir Touilli ​
-| 15.30-16.00 | //Gordon Pace:// Contract Analysis ​+| 14.30-15.00 | {{:malta13-perez.pdf|Decidable Classes of Mean-Payoff Games with Imperfect Information}} | Guillermo Perez 
-| 16.00-16.30 | //Jonas Jensen:// Fictional Separation Logic | +| 15.00-15.30 | **Coffee break** ​|
-| 16.30-17.30 | MC Meeting | +| 15.30-16.00 | {{:​malta13-pace.pdf|Reasoning About Contracts}} | Gordon Pace | 
-| 19.30- | **Workshop dinner** |+| 16.00-16.30 | {{:malta13-jensen.pdf|Fictional Separation Logic}} | Jonas Jensen ​
 +| 16.30-17.30 | MC Meeting ​|
 +| 19.30- | **Workshop dinner** ​||
  
 === Monday, 17 June 2013 === === Monday, 17 June 2013 ===
  
-| 09.00-10.00 | Invited Speaker**Manuel Hermenegildo** +^             ^ Title                 ^ Speaker ^ 
-| 10.00-10.30 | **Coffee break** | +| 09.00-10.00 | {{:​malta13-hermenegildo.pdf|Analysis and Verification ``of and with''​ Horn Clauses (using the Ciao system) }}**(Invited Speaker)** Manuel Hermenegildo | 
-| 10.30-11.00 | //Tewodros Beyene:// Solving Existentially Quantfied Horn Clauses | +| 10.00-10.30 | **Coffee break** ​|
-| 11.00-11.30 | //Boriss Selajev:// Scaling ​dynamic logic for intermediate states ​+| 10.30-11.00 | {{:malta13-beyene.pdf|Solving Existentially Quantfied Horn Clauses}} | Tewodros Beyene ​
-| 11.30-12.00 | //Ondrej Lengal:// Fully Automated Shape Analysis Based on Forest Automata | +| 11.00-11.30 | {{:malta13-selajev.pdf|Scaling ​Dynamic Logic for Intermediate States}} | Boriss Selajev ​
-| 12.00-12.30 | //Alejandro Sanchez:// Invariant Generation for Parametrized Systems using Self-Reflection | +| 11.30-12.00 | {{:malta13-lengal.pdf|Fully Automated Shape Analysis Based on Forest Automata}} | Ondrej Lengal ​
-| 12.30-14.00 | **Lunch** | +| 12.00-12.30 | {{:malta13-sanchez.pdf|Invariant Generation for Parametrized Systems using Self-Reflection}} | Alejandro Sanchez ​
-| 14.00-15.00 | Invited speaker**John Gallagher** +| 12.30-14.00 | **Lunch** ​|
-| 15.00-15.30 | **Coffee break** | +| 14.00-15.00 | {{:​malta13-gallagher.pdf|Verification by Abstraction and Specialisation of Constraint Logic Programs}} **(Invited speaker)** John Gallagher | 
-| 15:30-16:00 | //Siirtola Antti:// Object-Oriented Programs as Parameterised Systems | +| 15.00-15.30 | **Coffee break** ​|
-| 16.00-16.30 | //Filip Konecni:// Underapproximation of Procedure Summaries for Integer Programs | +| 15:30-16:00 | {{:malta13-siirtola.pdf|Object-Oriented Programs as Parameterised Systems}} | Siirtola Antti 
-| 16.30-17.00 | //Paul Jackson:// Auditing User-provided Axioms in Software Verification Conditions | +| 16.00-16.30 | {{:malta13-konecny.pdf|Underapproximation of Procedure Summaries for Integer Programs}} | Filip Konecni ​
-| 17:00-17:30 | //David Monniaux:// TBA +| 16.30-17.00 | {{:malta13-jackson.pdf|Auditing User-provided Axioms in Software Verification Conditions}} | Paul Jackson ​
-| 17:30-18:00 | Discussion Session: Cross-fertilization between Logic Programming with CLP and Horn Clause Verification |+| 17:00-17:30 | {{:​malta13-monniaux.pdf|Death by a Thousand Cuts (worst-case execution time by bounded model checking)}} | David Monniaux | 
 +| 17:30-18:00 | Discussion Session: Cross-fertilization between Logic Programming with CLP and Horn Clause Verification ​||
  
 ===== General Information ===== ===== General Information =====
Line 104: Line 107:
 //Christian Colombo// //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. ​
  
 ---- ----