1st Microsoft Research and IMDEA Software Institute Collaboration Workshop (MICW 2014)

2–4 April 2014 | Madrid, Spain

1st Microsoft Research and IMDEA Software Institute Collaboration Workshop (MICW 2014)

These workshops brought together researchers and students to discuss their collaborative work on hot topics in software in order to advance the state of the art and, where possible, to bring those advances to Microsoft’s businesses. The focus of the first workshop was verification, programming languages, and security.

Overview

The first Workshop of the Joint Research Center between Microsoft Research and the IMDEA Software Institute, Madrid took place April 2–4, 2014. at IMDEA.

The workshop was the launch activity of the Center, at which researchers from both sides continued to work on topics of joint interest, which fall into the following broad categories:

  • Cloud storage systems and mobile platforms
  • Cloud/web security / malware detection
  • Cryptography, privacy
  • Concurrency, parallelism, and memory models
  • Programming languages and verification

Keynote speakers

Martín AbadiMartín Abadi is a Principal Researcher at Microsoft Research Silicon Valley. He has been a Professor at UC Santa Cruz, where he is now Professor Emeritus, and also held the Chair “Informatique et sciences numériques” at the Collège de France. Earlier, he studied at Stanford University and worked at Digital's System Research Center and other industrial labs. His research is mainly on computer and network security, programming languages, and specification and verification methods. He has contributed, for example, to the design and analysis of security protocols and to the foundations of object-oriented languages. His research on security has been recognized with the Outstanding Innovation Award of the ACM Special Interest Group on Security, Audit and Control, and with the Hall of Fame Award of the ACM Special Interest Group on Operating Systems. He is a Fellow of the ACM and of the American Association for the Advancement of Science.

Ben LivshitsBen Livshits is a research scientist at Microsoft Research and an affiliate professor at the University of Washington. He received a bachelor's degree in Computer Science and Math from Cornell University, and his M.S. and Ph.D. in Computer Science from Stanford University, respectively. Ben’s research interests include application of analysis techniques to finding errors in programs, and, more generally, privacy, security, and performance of large programs.

Alexy GotsmanAlexy Gotsman is a tenure-track Assistant Research Professor at the IMDEA Software Institute. Before joining IMDEA, he was a postdoctoral fellow at the University of Cambridge, where received his Ph.D. His research interests are in software verfication, particularly, in developing reasoning techniques and automated verification tools for real-world concurrent systems software.

 

Honoured guest

Luiga Figar de LacalleLucia Figar de Lacalle, Regional Minister of Education, Youth and Sports, Communidad de Madrid

Programme

Wednesday, 2 April 2014

Time

Topic/event

Chairs/presenter

Morning

Researchers who arrive early can meet colleagues, roam the building, etc.

13:00–14:15

Lunch

14:15–14:30

Welcome

Manuel Hermenegildo and Judith Bishop

14:30–15:30

Plenary Keynote
Finding Malware on a Web Scale

Ben Livshits, Microsoft Research

15:30–18:00

Security Session

Chairs: Juan Caballero and Ben Livshits

15:30–15:55

Cost-effective protection against side-channel attacks

Boris Koepf, IMDEA

15:55–16:20

Secure Delegation of Computation on Outsourced Data

Dario Fiore, IMDEA

16:20–16:45

Break

16:45–17:10

Automating Proofs of Relational Properties of Probabilistic Programs

Andrey Rybalchenko, Microsoft

17:10–17:35

Computer-Aided Cryptographic Design and Analysis

Benedikt Schmidt, IMDEA

17:35–18:00

CyberProbe: Towards Internet-Scale Active Detection of Malicious Servers

Juan Caballero, IMDEA

 

Thursday, 3 April 2014

Time

Topic/event

Chairs/presenter

09:30–10:30

Individual and group collaboration session

10:30–11:30

Plenary Keynote
A Timely Dataflow Model and the Naiad System

Martin Abadi, Microsoft Research

11:30–12:15

Break

Visitors, with presentations at stations

12:30–13:30

Inauguration of the Joint Research Center

Dignitaries, Executives and Honoured Guests

13:30–15:00

Reception and lunch in IMDEA Building

All invited participants

15:00–17:30

Languages Session

Chairs: Pierre-Yves Strub and Cédric Fournet

15:00–15:25

Communicating State Transition Systems for Fine-Grained Concurrent Resources

Ilya Sergey, IMDEA

15:25–15:50

TouchDevelop - mobile, cloud and touch programming

Judith Bishop, Microsoft Research

15:50–16:15

Programming Language Techniques for Low-Level Cryptographic Security

François Dupressoir, IMDEA

16:15–16:40

Break

16:40–17:05

Gradual Typing Embedded Securely in JavaScript

Pierre-Yves Strub, IMDEA

17:05–17:30

Generating provably correct x86 using a proof assistant

Andrew Kennedy, Microsoft Research

 

Friday, 4 April 2014

Time

Topic/event

Chair/speaker

09:30–10:30

Plenary Keynote

Reasoning about Eventual Consistency and Replicated Data Types

Alexey Gotsman, IMDEA

10:30–11:00

Break

11:00–13:30

Verification Session

Chairs: Alexy Gotsman and Francesco Logozzo

11:00–11:25

Horn clauses with cardinality constraints

Andrey Rybalchenko, Microsoft Research

11:25–11:50

Verification of Observational Refinement by Counting

Michael Emmi, IMDEA

11:50–12:15

Abstraction based verification of stability of hybrid systems

Pavithra Prabhakar, IMDEA

12:15–12:40

Break

12:40–13:05

Energy and Resource Usage Analysis and Verification in the CiaoPP System

Pedro López García, IMDEA

13:05–13:30

Verification Modulo versions

Francesco Logozzo, Microsoft Research

13:30–14:30

Lunch

14:30–15:45

New directions (15 min talks)

 

Network Verification - from circuit to packet switched and software defined networks

The future of meta-programming

Surveyz: a privacy-preserving protocol for online surveys

Chairs: Gilles Barthe and Andrew Kennedy

Nikolaj Bjorner, Microsoft Research

 

John Gallagher, IMDEA

Cedric Fournet, Microsoft Research

15:45:16:00

Close

Manuel Hermenegildo and Judith Bishop

 

Organization

Steering Committee

  • Gilles Barthe, IMDEA Software Institute
  • Judith BIshop, Microsoft Research
  • Georges Gonthier, Microsoft Research
  • Manuel Hermenegildo, IMDEA Software Institute

Convenors

  • Languages: Pierre-Yves Strub and Georges Gonthier
  • Security: Juan Caballero and Ben Livshits
  • Verification: Alexey Gotsman and Francesco Logozzo

Logistics

Paola Huerta and Andrea Iannetta, IMDEA Software Institute

Contact: msr-imdeasw-opening@software.imdea.org

Registration

The Workshop is by invitation only. The registration link will be sent to all invited participants.

Hotels

These hotels are recommended. Make your own reservations. We shall try to provide transport:

Venue

Instituto IMDEA Software
Campus Montegancedo s/n
28223 Pozuelo de Alarcon, Madrid
SPAIN

Telephone: +34-91-101-2202