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
Last revision Both sides next revision
malta13 [2013/06/17 14:02]
pace
malta13 [2013/06/24 21:37]
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 | **(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 | Discussion Session: Cross-fertilization between Logic Programming ​and CLP with Horn Clause Verification |+| 16.30-17.00 | {{:malta13-jackson.pdf|Auditing User-provided Axioms in Software Verification Conditions}} | Paul Jackson ​
 +| 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 103: 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. ​
  
 ---- ----