Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision Last revision Both sides next revision | ||
|
malta13 [2013/06/18 07:37] 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 | //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 ===== | ||