Programme of SVARM at ETAPS 2011

Friday, April 1

Room E1.3/001

13:55 - 16:00 SESSION 1

13.55: Welcome

 

14.00: Invited Talk: Quantitative reactive models

Tom Henzinger (IST Austria)

 

15.00: Reasoning about explicit resource management in message passing concurrency

Adrian Francalanza (University of Malta)

15.20: Quantitative verification of adaptive IT systems

Radu Calinescu (University of Oxford, UK)

15.40: Provably correct compilation of an abstract behavioral modeling language

Reiner Hähnle (Chalmers University of Technology, Sweden)

16:00 - 16:30 Coffee

16:30 - 17:10 SESSION 2

16.30: Separation logic for OO programs in Coq

Lars Birkedal (IT University of Copenhagen, Denmark)

16:50: Link between interactive and automated theorem provers

Jasmin Blanchette (TU München, Germany)

 

17:10 - 18:00 Business Meeting

 

Saturday, April 2

09:00 - 10:20 SESSION 3

09:00: Craig interpolation for integer arithmetic, uninterpreted functions, and the theory of arrays

Philipp Ruemmer (Uppsala University, Sweden)

09:20: SMT-based symbolic model checking of administrative access control policies

Alessandro Armando (Università di Genova, Italy)

09.40: Synthesis of memory fences

Eran Yahav (Technion - Israel Institute of Technology, Israel)

10.00: Lazy abstraction for size-change termination

Peter Schneide-Kamp (University of Southern Denmark)

 

 

10:30 - 11:00 Coffee

11:00 - 12:30 SESSION 4

11.00: From constructive to inductive proofs of termination

Aliaksei Tsitovich (University of Lugano, Switzerland)

11.20: Cooperation between SAT, SMT provers and Coq

Chantal Keller (INRIA, Rocquencourt-Paris, France)

11.40: On model checking networks of pushdown systems

Tayssir Touili (LIAFA, Paris, France)

 

12.00: Open mike for short research presentations

 

12:30 - 14:00 Lunch           

14:00 - 16:00 SESSION 5

14.00: Invited Talk: S2E: A Platform for In-Vivo Multi-Path Analysis of Software Systems

George Candea (EPFL, Switzerland)

 

15.00: Numerical Transition Systems Competition

Radu Iosif (VERIMAG, France)

16:00 - 16:30 Coffee

16:30 - 17:30 SESSION 6

16.30: Two new tool prototypes for shape analysis

Tomáš Vojnar (Brno University of Technology, Czech Republic)

16.50: Deductive Temporal Verification of Parametrized Concurrent Systems

Alejandro Sánchez (IMDEA-Software, Spain)

17.10: Verified efficient unsatisfiability proof checking for SAT

Filip Maric (Faculty of Mathematics, Belgrade, Serbia)

 

 

Sunday, April 3

09:00 - 10:20 SESSION 7

09.00: Invited talk: Systematic Software Testing Using Test Abstractions

Darko Marinov (University of Illinois at Urbana-Champaign)

 

10.00: Efficient model checking of PSL safety properties

Tuomas Launiainen (Aalto University, Finland)

 

10:30 - 11:00 Coffee

11:00 - 12:20 SESSION 8

11.00: On Rich Models Issues for Trust Management & Qualitative Algebra

Denis Trček (Jožef Stefan Institute, Slovenia)

11.20: Synthesizing Systems with Optimal Average-Case Behavior for Ratio Objectives

Christian von Essen (RWTH Aachen, Germany)

11.40: Verifying Design Patterns using Symbolic Model Checking

Alexis Marechal (Université de Genève, Switzerland)

12.00: Numerical constraint solving based on linear relaxations

Stefan Ratschan (Academy of Sciences of the Czech Republic)

12:30 - 14:00 Lunch           

14:00 - 16:00 SESSION 9

14.00: Analysis and Verification of Higher Order Functional Programs: An Automata Theoretic Approach

Ruslán Garza (Max Planck Institute for Software Systems, Germany)

14.20: Static Analysis of x86 Executables

Johannes Kinder (TU Darmstadt, Germany / EPFL, Switzerland)

14.40: Software Synthesis using Automated Reasoning

Ruzica Piskac (EPFL, Switzerland)

15.00: Verification for control

Rupak Majumdar (Max Planck Institute for Software Systems, Germany)

 

16:00 - 16:30 Coffee

16:30 - 18:00 SESSION 10

16.30: Open Discussions on Future Collaboration Steps

 

 

HOME PAGE:  http://richmodels.epfl.ch/svarm11