Difference between revisions of "Programme"

From Numerical Transition Systems
Jump to: navigation, search
Line 1: Line 1:
 
'''Monday, May 12'''
 
'''Monday, May 12'''
  
14:00-15:00 Keynote talk: Yannis Smaragdakis (University of Athens): Declarative Static Program Analysis
+
14:00-15:00 ''Keynote talk'': Yannis Smaragdakis (University of Athens): Declarative Static Program Analysis
  
15:00-16:00 Static Analysis  
+
15:00-16:00 ''Static Analysis''
  
 
* Moritz Sinn (Vienna University of Technology): A Simple and Scalable Static Analysis for Bound Analysis and Amortized Complexity Analysis
 
* Moritz Sinn (Vienna University of Technology): A Simple and Scalable Static Analysis for Bound Analysis and Amortized Complexity Analysis
Line 9: Line 9:
 
* Tomer Kotek (Vienna University of Technology): Shape and Content: Incorporating Domain Knowledge into Shape Analysis
 
* Tomer Kotek (Vienna University of Technology): Shape and Content: Incorporating Domain Knowledge into Shape Analysis
  
16:00-16:30 Coffee break
+
16:00-16:30 ''Coffee break''
  
16:30-18:30 Automated Reasoning  
+
16:30-18:30 ''Automated Reasoning''
  
 
* Ioan Dragan (Vienna University of Technology): Lingva: Generating and Proving Program Properties using Symbol Elimination
 
* Ioan Dragan (Vienna University of Technology): Lingva: Generating and Proving Program Properties using Symbol Elimination
Line 20: Line 20:
  
 
* Klaus Gleissenthall (TUM,Munich): Solving Horn Clauses with Cardinality Constraints
 
* Klaus Gleissenthall (TUM,Munich): Solving Horn Clauses with Cardinality Constraints
 +
  
 
----
 
----
 +
  
 
'''Tuesday, May 13'''
 
'''Tuesday, May 13'''
  
9:00-10:30 Compositional Methods (3,4,18)
+
9:00-10:30 ''Compositional Methods''
  
 
* Souha Ben Rayana (VERIMAG,Grenoble): Compositional Verification of Component-Based Real-time Systems and Applications
 
* Souha Ben Rayana (VERIMAG,Grenoble): Compositional Verification of Component-Based Real-time Systems and Applications
Line 33: Line 35:
 
* Najah Bensaid (VERIMAG,Grenoble): Information flow security in component-based systems
 
* Najah Bensaid (VERIMAG,Grenoble): Information flow security in component-based systems
  
10:30-11:00 Coffee break
+
10:30-11:00 ''Coffee break''
  
11:00-12:00 Resources
+
11:00-12:00 ''Resources''
  
 
* Ravichandhran Kandhadai Madhavan (EPFL,Lausanne): Symbolic Resource Bound Inference for Functional Programs
 
* Ravichandhran Kandhadai Madhavan (EPFL,Lausanne): Symbolic Resource Bound Inference for Functional Programs
Line 41: Line 43:
 
* Ivan Radicek (Vienna University of Technology): Feedback Generation for Performance Problems in Introductory Programming Assignments
 
* Ivan Radicek (Vienna University of Technology): Feedback Generation for Performance Problems in Introductory Programming Assignments
  
12:00-14:00 Lunch break
+
12:00-14:00 ''Lunch break''
  
14:00-15:00 Keynote talk: Dino Distefano (Queen Mary, London and Facebook): Separation Logic Static Analysis @ Facebook
+
14:00-15:00 ''Keynote talk'': Dino Distefano (Queen Mary, London and Facebook): Separation Logic Static Analysis @ Facebook
  
15:00-16:00 Verification I
+
15:00-16:00 ''Verification I''
  
 
* Amit Kumar Dhar (LIAFA,Paris): Verification of Properties on Flat Counter Systems
 
* Amit Kumar Dhar (LIAFA,Paris): Verification of Properties on Flat Counter Systems
Line 51: Line 53:
 
* Frantisek Blahoudek (Masaryk University,Brno): Chasing the Best Buechi Automata for NestedDFS-Based Model Checking
 
* Frantisek Blahoudek (Masaryk University,Brno): Chasing the Best Buechi Automata for NestedDFS-Based Model Checking
  
16:00-16:30 Coffee break
+
16:00-16:30 ''Coffee break''
  
16:30-18:00 Distributed Systems (5,7,14)
+
16:30-18:00 ''Distributed Systems''
  
 
* Alexios Leikidis (VERIMAG,Grenoble): Rigorous modeling and validation of sensor network systems
 
* Alexios Leikidis (VERIMAG,Grenoble): Rigorous modeling and validation of sensor network systems
Line 67: Line 69:
 
'''Wednesday, May 14'''
 
'''Wednesday, May 14'''
  
9:00-10:30 Compilation & Synthesis (1,16,21)
+
9:00-10:30 ''Compilation & Synthesis''
  
 
* Eva Darulova (EPFL,Lausanne): Compiling Real Numbers with Precision Guarantees
 
* Eva Darulova (EPFL,Lausanne): Compiling Real Numbers with Precision Guarantees
Line 75: Line 77:
 
* Thorsten Tarrach (IST Austria): Regression-free Synthesis for Concurrency  
 
* Thorsten Tarrach (IST Austria): Regression-free Synthesis for Concurrency  
  
10:30-11:00 Coffee break
+
10:30-11:00 ''Coffee break''
  
11:00-12:00 Verification II (20,13)
+
11:00-12:00 ''Verification II''
  
 
* Marco Gario (FBK,Trento): Using Temporal Epistemic Logic for Reasoning about Fault Management
 
* Marco Gario (FBK,Trento): Using Temporal Epistemic Logic for Reasoning about Fault Management
  
 
* Jan Otop and Roopsha Samanta (IST Austria): Robustness Analysis of Transducers
 
* Jan Otop and Roopsha Samanta (IST Austria): Robustness Analysis of Transducers

Revision as of 13:42, 28 March 2014

Monday, May 12

14:00-15:00 Keynote talk: Yannis Smaragdakis (University of Athens): Declarative Static Program Analysis

15:00-16:00 Static Analysis

  • Moritz Sinn (Vienna University of Technology): A Simple and Scalable Static Analysis for Bound Analysis and Amortized Complexity Analysis
  • Tomer Kotek (Vienna University of Technology): Shape and Content: Incorporating Domain Knowledge into Shape Analysis

16:00-16:30 Coffee break

16:30-18:30 Automated Reasoning

  • Ioan Dragan (Vienna University of Technology): Lingva: Generating and Proving Program Properties using Symbol Elimination
  • Leonardo Alt (University of Lugano): PeRIPLO: A Framework for Producing Effective Interpolants in SAT-Based Software Verification
  • Florian Lonsing (Vienna University of Technology): Incremental QBF Solving
  • Klaus Gleissenthall (TUM,Munich): Solving Horn Clauses with Cardinality Constraints




Tuesday, May 13

9:00-10:30 Compositional Methods

  • Souha Ben Rayana (VERIMAG,Grenoble): Compositional Verification of Component-Based Real-time Systems and Applications
  • Corneliu Popeea (TUM,Munich): Reduction for compositional verification of multi-threaded programs
  • Najah Bensaid (VERIMAG,Grenoble): Information flow security in component-based systems

10:30-11:00 Coffee break

11:00-12:00 Resources

  • Ravichandhran Kandhadai Madhavan (EPFL,Lausanne): Symbolic Resource Bound Inference for Functional Programs
  • Ivan Radicek (Vienna University of Technology): Feedback Generation for Performance Problems in Introductory Programming Assignments

12:00-14:00 Lunch break

14:00-15:00 Keynote talk: Dino Distefano (Queen Mary, London and Facebook): Separation Logic Static Analysis @ Facebook

15:00-16:00 Verification I

  • Amit Kumar Dhar (LIAFA,Paris): Verification of Properties on Flat Counter Systems
  • Frantisek Blahoudek (Masaryk University,Brno): Chasing the Best Buechi Automata for NestedDFS-Based Model Checking

16:00-16:30 Coffee break

16:30-18:00 Distributed Systems

  • Alexios Leikidis (VERIMAG,Grenoble): Rigorous modeling and validation of sensor network systems
  • Jad Hamza (LIAFA,Paris): Verifying Eventual Consistency of Optimistic Replication Systems
  • Benjamin Bittner (FBK,Trento): Failure Propagation Analysis for Safety-Critical Systems




Wednesday, May 14

9:00-10:30 Compilation & Synthesis

  • Eva Darulova (EPFL,Lausanne): Compiling Real Numbers with Precision Guarantees
  • Tewodros Beyene (TUM,Munich): Compositional Repair of Reactive Programs
  • Thorsten Tarrach (IST Austria): Regression-free Synthesis for Concurrency

10:30-11:00 Coffee break

11:00-12:00 Verification II

  • Marco Gario (FBK,Trento): Using Temporal Epistemic Logic for Reasoning about Fault Management
  • Jan Otop and Roopsha Samanta (IST Austria): Robustness Analysis of Transducers