RDP 2017
Wed 18 - Fri 20 January 2017
co-located with
POPL 2017
Toggle navigation
Attending
Campus: Paris Jussieu
Program
RDP Program
Your Program
Wed 18 Jan
Thu 19 Jan
Fri 20 Jan
Track/Call
Organization
RDP 2017 Committees
Track Committees
Program Committee
Contributors
People Index
Search
Series
Sign in
Sign up
POPL 2017
(
series
) /
RDP 2017 (
series
) /
Paris Jussieu
/
Room information: Amphitheater 44
Venue
Paris Jussieu
Room name
Amphitheater 44
Floor
0
Capacity
240
Room Information
No extra information available
Program
Detailed Table
Session Timeline
Detailed Timeline
Program Display Configuration
Time Zone
The program is currently displayed in
(GMT+01:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
.
Use conference time zone: (GMT+01:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
Select other time zone
(GMT-12:00) AoE (Anywhere On Earth)
(GMT-11:00) Midway Island, Samoa
(GMT-10:00) Hawaii-Aleutian
(GMT-10:00) Hawaii
(GMT-09:30) Marquesas Islands
(GMT-09:00) Gambier Islands
(GMT-09:00) Alaska
(GMT-08:00) Tijuana, Baja California
(GMT-08:00) Pitcairn Islands
(GMT-08:00) Pacific Time (US & Canada)
(GMT-07:00) Mountain Time (US & Canada)
(GMT-07:00) Chihuahua, La Paz, Mazatlan
(GMT-07:00) Arizona
(GMT-06:00) Saskatchewan, Central America
(GMT-05:00) Guadalajara, Mexico City, Monterrey
(GMT-05:00) Easter Island
(GMT-06:00) Central Time (US & Canada)
(GMT-05:00) Eastern Time (US & Canada)
(GMT-05:00) Cuba
(GMT-05:00) Bogota, Lima, Quito, Rio Branco
(GMT-04:00) Caracas
(GMT-03:00) Santiago
(GMT-04:00) La Paz
(GMT-03:00) Faukland Islands
(GMT-03:00) Manaus, Amazonas, Brazil
(GMT-04:00) Atlantic Time (Goose Bay)
(GMT-04:00) Atlantic Time (Canada)
(GMT-03:30) Newfoundland
(GMT-03:00) UTC-3
(GMT-03:00) Montevideo
(GMT-03:00) Miquelon, St. Pierre
(GMT-03:00) Greenland
(GMT-03:00) Buenos Aires
(GMT-02:00) Brasilia, Distrito Federal, Brazil
(GMT-02:00) Mid-Atlantic
(GMT-01:00) Cape Verde Is.
(GMT-01:00) Azores
(UTC) Coordinated Universal Time
(GMT) Belfast
(GMT) Dublin
(GMT) Lisbon
(GMT) London
(GMT) Monrovia, Reykjavik
(GMT+01:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
(GMT+01:00) Belgrade, Bratislava, Budapest, Ljubljana, Prague
(GMT+01:00) Brussels, Copenhagen, Madrid, Paris
(GMT+01:00) West Central Africa
(GMT+02:00) Windhoek
(GMT+02:00) Athens
(GMT+02:00) Beirut
(GMT+02:00) Cairo
(GMT+02:00) Gaza
(GMT+02:00) Harare, Pretoria
(GMT+02:00) Jerusalem
(GMT+03:00) Minsk
(GMT+02:00) Syria
(GMT+03:00) Moscow, St. Petersburg, Volgograd
(GMT+03:00) Nairobi
(GMT+03:30) Tehran
(GMT+04:00) Abu Dhabi, Muscat
(GMT+04:00) Yerevan
(GMT+04:30) Kabul
(GMT+05:00) Ekaterinburg
(GMT+05:00) Tashkent
(GMT+05:30) Chennai, Kolkata, Mumbai, New Delhi
(GMT+05:45) Kathmandu
(GMT+06:00) Astana, Dhaka
(GMT+07:00) Novosibirsk
(GMT+06:30) Yangon (Rangoon)
(GMT+07:00) Bangkok, Hanoi, Jakarta
(GMT+07:00) Krasnoyarsk
(GMT+08:00) Beijing, Chongqing, Hong Kong, Urumqi
(GMT+08:00) Irkutsk, Ulaan Bataar
(GMT+08:00) Perth
(GMT+08:45) Eucla
(GMT+09:00) Osaka, Sapporo, Tokyo
(GMT+09:00) Seoul
(GMT+09:00) Yakutsk
(GMT+10:30) Adelaide
(GMT+09:30) Darwin
(GMT+10:00) Brisbane
(GMT+11:00) Hobart
(GMT+10:00) Vladivostok
(GMT+11:00) Lord Howe Island
(GMT+11:00) Solomon Is., New Caledonia
(GMT+11:00) Magadan
(GMT+11:00) Norfolk Island
(GMT+12:00) Anadyr, Kamchatka
(GMT+13:00) Auckland, Wellington
(GMT+12:00) Fiji, Kamchatka, Marshall Is.
(GMT+13:45) Chatham Islands
(GMT+13:00) Nuku'alofa
(GMT+14:00) Kiritimati
The GMT offsets shown reflect the offsets
at the moment of the conference
.
Time Band
By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.
Display full program
Specify a time band
-
Save
×
You're viewing the program in a time zone which is different from your device's time zone
change time zone
Sun 15 Jan
Displayed time zone:
Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
change
09:00 - 10:00
Invited talk 1
VMCAI
at
Amphitheater 44
Chair(s):
David Monniaux
CNRS, VERIMAG
09:00
60m
Talk
Detecting Strict Aliasing Violations in the Wild
VMCAI
Pascal Cuoq
Trust-in-Soft
File Attached
10:30 - 12:00
Program Analysis
VMCAI
at
Amphitheater 44
Chair(s):
Boris Yakobowski
CEA - LIST
10:30
30m
Talk
Partitioned Memory Models for Program Analysis.
VMCAI
Wei Wang
Google, Inc.
,
Clark Barrett
Stanford University
,
Thomas Wies
New York University
File Attached
11:00
30m
Talk
Property Directed Reachability for Proving Absence of Concurrent Modification Errors
VMCAI
Asya Frumkin
Tel Aviv University
,
Yotam M. Y. Feldman
Tel Aviv University
,
Ondřej Lhoták
University of Waterloo, Canada
,
Oded Padon
Tel Aviv University
,
Mooly Sagiv
Tel Aviv University
,
Sharon Shoham
Tel Aviv university
File Attached
11:30
30m
Talk
Stabilizing Floating-Point Programs using Provenance Analysis
VMCAI
Yijia Gu
Northeastern University
,
Thomas Wahl
Northeastern University
14:00 - 15:30
Concurrency 1
VMCAI
at
Amphitheater 44
Chair(s):
Camille Coti
LIPN, Université Paris 13
14:00
30m
Talk
Accuracy of Message Counting Abstraction in Fault-Tolerant Distributed Algorithms
VMCAI
Igor Konnov
TU Wien
,
Josef Widder
TU Wien
,
Francesco Spegni
,
Luca Spalazzi
14:30
30m
Talk
Independence Abstractions and Models of Concurrency
VMCAI
Vijay D'Silva
Google Inc.
,
Daniel Kroening
University of Oxford
,
Marcelo Sousa
University of Oxford
15:00
30m
Talk
Static Analysis of Communicating Process using Symbolic Transducers
VMCAI
Vincent Botbol
CEA LIST + LIP6 Université Pierre & Marie Curie
,
Tristan Le Gall
CEA LIST
,
Emmanuel Chailloux
LIP6 - UPMC
Media Attached
File Attached
16:00 - 17:30
Decision procedures
VMCAI
at
Amphitheater 44
Chair(s):
Andreas Podelski
University of Freiburg, Germany
16:00
30m
Talk
Synthesising Strategy Improvement and Recursive Algorithms for Solving 2.5 Player Parity Games
VMCAI
Ernst Moritz Hahn
State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences
,
Sven Schewe
University of Liverpool
,
Andrea Turrini
State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences
,
Lijun Zhang
Institute of Software, Chinese Academy of Sciences
File Attached
16:30
30m
Talk
Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic
VMCAI
Andrew Reynolds
EPFL
,
Radu Iosif
VERIMAG, CNRS, Université Grenoble-Alpes
,
Cristina Serban
VERIMAG, CNRS, Université Grenoble-Alpes
File Attached
17:00
30m
Talk
Matching multiplications in Bit-Vector formulas
VMCAI
Supratik Chakraborty
IIT Bombay
,
Ashutosh Gupta
,
Rahul Jain
Tata Institute of Fundamental Research
File Attached
Mon 16 Jan
Displayed time zone:
Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
change
09:00 - 10:00
Invited talk 2
VMCAI
at
Amphitheater 44
Chair(s):
Ahmed Bouajjani
IRIF, Université Paris Diderot
09:00
60m
Talk
Verified Concurrent Code: Tricks of the Trade
VMCAI
A:
Ernie Cohen
Amazon Web Services
10:30 - 12:00
Numerical domains
VMCAI
at
Amphitheater 44
Chair(s):
Laure Gonnord
University of Lyon & LIP, France
10:30
30m
Talk
Sound Bit-Precise Numerical Domains
VMCAI
Tushar Sharma
University of Wisconsin - Madison, USA
,
Thomas Reps
University of Wisconsin - Madison and Grammatech Inc.
File Attached
11:00
30m
Talk
Efficient Elimination of Redundancies in Polyhedra using Raytracing
VMCAI
Alexandre Maréchal
,
Michael Perin
Media Attached
File Attached
11:30
30m
Talk
Finding Relevant Templates via the Principal Component Analysis
VMCAI
Yassamine Seladji
University of Tlemcen
File Attached
14:00 - 15:30
Model-checking and bug finding
VMCAI
at
Amphitheater 44
Chair(s):
Andreas Podelski
University of Freiburg, Germany
14:00
30m
Talk
Effective Bug Finding in C Programs with Shape and Effect Abstraction
VMCAI
Iago Abal
IT University of Copenhagen
,
Claus Brabrand
IT University of Copenhagen, Denmark
,
Andrzej Wąsowski
IT University of Copenhagen, Denmark
14:30
30m
Talk
Reduction of Workflow Nets for Generalised Soundness Verification
VMCAI
Hadrien Bride
Femto-ST / Université de Franche-Comté
,
Olga Kouchnarenko
Femto-ST / Université de Franche-Comté
,
Fabien Peureux
Femto-ST / Université de Franche-Comté + Smartesting S&S
Media Attached
15:00
30m
Talk
Dynamic Reductions for Model Checking Concurrent Software.
VMCAI
Henning Günther
Technische Universität Wien
,
Alfons Laarman
Vienna University of Technology
,
Ana Sokolova
University of Salzburg
,
Georg Weissenbacher
Technische Universität Wien
File Attached
16:00 - 17:30
Symbolic analysis and invariant synthesis
VMCAI
at
Amphitheater 44
Chair(s):
Constantin Enea
LIAFA, Université Paris Diderot
16:00
30m
Talk
Block-wise abstract interpretation by combining abstract domains with SMT
VMCAI
Jiahong Jiang
,
Liqian Chen
,
Xueguang Wu
,
Ji Wang
16:30
30m
Talk
IC3 - Flipping the E in ICE
VMCAI
Yakir Vizel
,
Arie Gurfinkel
University of Waterloo
,
Sharon Shoham
Tel Aviv university
,
Sharad Malik
Princeton University
17:00
30m
Talk
Counterexample Validation and Interpolation-Based Refinement for Forest Automata
VMCAI
Lukáš Holík
,
Martin Hruska
Brno University of Technology
,
Ondřej Lengál
Brno University of Technology
,
Adam Rogalewicz
Brno University of Technology
,
Tomáš Vojnar
Brno University of Technology
Tue 17 Jan
Displayed time zone:
Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
change
09:00 - 10:00
Invited talk 3
VMCAI
at
Amphitheater 44
Chair(s):
Andreas Podelski
University of Freiburg, Germany
09:00
60m
Talk
Verification of Cancer Programs
VMCAI
Jasmin Fisher
Microsoft Research
10:30 - 12:00
Model Checking and Synthesis
VMCAI
at
Amphitheater 44
Chair(s):
Ahmed Bouajjani
IRIF, Université Paris Diderot
10:30
30m
Talk
Reachability for dynamic parametric processes
VMCAI
Anca Muscholl
Université de Bordeaux / LaBRI
,
Helmut Seidl
Technische Universität München
,
Igor Walukiewicz
CNRS, LaBRI
11:00
30m
Talk
Synthesizing Non-Vacuous Systems
VMCAI
Roderick Bloem
Institute of Software Technology, Graz University of Technology
,
Hana Chockler
,
ma e
,
Ofer Strichman
Technion
File Attached
11:30
30m
Talk
Solving Nonlinear Integer Arithmetic with MCSat
VMCAI
Dejan Jovanović
SRI International
14:00 - 15:30
Abstract Interpretation
VMCAI
at
Amphitheater 44
Chair(s):
Roberto Giacobazzi
University of Verona, Italy
14:00
30m
Talk
Complete Abstractions and Subclassical Modal Logics
VMCAI
Vijay D'Silva
Google
,
Marcelo Sousa
University of Oxford
14:30
30m
Talk
Structuring Abstract Interpreters through State and Value Abstractions
VMCAI
David Bühler
CEA LIST
,
Boris Yakobowski
CEA - LIST
,
Sandrine Blazy
University of Rennes 1, France
Media Attached
15:00
30m
Talk
Conjunctive Abstract Interpretation using Paramodulation
VMCAI
Mooly Sagiv
Tel Aviv University
,
A:
Or Ozeri
Tel Aviv university
,
Oded Padon
Tel Aviv University
,
Noam Rinetzky
Tel Aviv University
Media Attached
16:00 - 17:30
Concurrency 2
VMCAI
at
Amphitheater 44
Chair(s):
David Monniaux
CNRS, VERIMAG
16:00
30m
Talk
Using Abstract Interpretation to Correct Synchronization Faults
VMCAI
Pietro Ferrara
IBM Research
,
Omer Tripp
IBM Thomas J. Watson Research Center
,
Peng Liu
Purdue University
,
Eric Koskinen
Yale University
16:30
30m
Talk
Detecting All High-Level Dataraces in an RTOS Kernel.
VMCAI
Suvam Mukherjee
Indian Institute of Science
,
Arunkumar S
Indian Institute of Science
,
Deepak D'Souza
17:00
30m
Talk
Precise Thread-Modular Abstract Interpretation of Concurrent Programs using Relational Interference Abstractions
VMCAI
Raphaël Monat
Ecole Normale Supérieure de Lyon
,
Antoine Miné
UPMC, France
Wed 18 Jan
Displayed time zone:
Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
change
10:30 - 12:10
Abstract Interpretation
POPL
at
Amphitheater 44
Chair(s):
Isabella Mastroeni
University of Verona, Italy
10:30
25m
Talk
Ogre and Pythia, An invariance proof method for weak consistency models
POPL
Jade Alglave
University College London
,
Patrick Cousot
New York University
10:55
25m
Talk
A Posteriori Environment Analysis with Pushdown Delta CFA
POPL
Kimball Germane
University of Utah
,
Matthew Might
University of Utah; Harvard Medical School; The White House
11:20
25m
Talk
Semantic-Directed Clumping of Disjunctive Abstract States
POPL
Huisong Li
INRIA/CNRS/ENS/PSL*
,
François Bérenger
INRIA/CNRS/ENS/PSL*
,
Bor-Yuh Evan Chang
University of Colorado Boulder
,
Xavier Rival
INRIA/CNRS/ENS Paris
11:45
25m
Talk
Fast Polyhedra Abstract Domain
POPL
Gagandeep Singh
ETH Zurich, Switzerland
,
Markus Püschel
ETH Zurich
,
Martin Vechev
ETH Zurich
14:20 - 16:00
Probabilistic Programming
POPL
at
Amphitheater 44
Chair(s):
Marco Gaboardi
SUNY Buffalo, USA
14:20
25m
Talk
Beginner's Luck: A Language for Property-Based Generators
POPL
Leonidas Lampropoulos
University of Pennsylvania
,
Diane Gallois-Wong
Inria Paris, ENS Paris
,
Cătălin Hriţcu
Inria Paris
,
John Hughes
Chalmers University of Technology
,
Benjamin C. Pierce
University of Pennsylvania
,
Li-yao Xia
ENS Paris
Pre-print
14:45
25m
Talk
Exact Bayesian Inference by Symbolic Disintegration
POPL
Chung-chieh Shan
Indiana University, USA
,
Norman Ramsey
Pre-print
15:10
25m
Talk
Stochastic Invariants for Probabilistic Termination
POPL
Krishnendu Chatterjee
IST Austria
,
Petr Novotný
IST Austria
,
Djordje Zikelic
University of Cambridge
15:35
25m
Talk
Coupling proofs are probabilistic product programs
POPL
Gilles Barthe
IMDEA
,
Benjamin Gregoire
INRIA
,
Justin Hsu
,
Pierre-Yves Strub
École Polytechnique
16:30 - 17:45
Logic
POPL
at
Amphitheater 44
Chair(s):
Alexandra Silva
University College London
16:30
25m
Talk
Monadic second-order logic on finite sequences
POPL
Loris D'Antoni
University of Wisconsin–Madison
,
Margus Veanes
Microsoft Research
16:55
25m
Talk
On the Relationship Between Higher-Order Recursion Schemes and Higher-Order Fixpoint Logic
POPL
Naoki Kobayashi
University of Tokyo, Japan
,
Etienne Lozes
ENS Cachan
,
Florian Bruse
University of Kassel
17:20
25m
Talk
Coming to Terms with Quantified Reasoning
POPL
Simon Robillard
Chalmers University of Technology
,
Andrei Voronkov
University of Manchester
,
Laura Kovacs
Chalmers University of Technology
Thu 19 Jan
Displayed time zone:
Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
change
10:30 - 12:10
Program Analysis
POPL
at
Amphitheater 44
Chair(s):
Francesco Logozzo
Facebook
10:30
25m
Talk
Relational Cost Analysis
POPL
Ezgi Çiçek
MPI-SWS, Germany
,
Gilles Barthe
IMDEA
,
Marco Gaboardi
SUNY Buffalo, USA
,
Deepak Garg
MPI-SWS, Germany
,
Jan Hoffmann
Carnegie Mellon University
10:55
25m
Talk
Contract-based Resource Verification for Higher-order Functions with Memoization
POPL
Ravichandhran Madhavan
EPFL
,
Sumith Kulal
IIT Bombay
,
Viktor Kunčak
EPFL, Switzerland
11:20
25m
Talk
Context-sensitive data dependence analysis via Linear Conjunctive Language Reachability
POPL
Qirun Zhang
University of California, Davis
,
Zhendong Su
University of California, Davis
11:45
25m
Talk
Towards Automatic Resource Bound Analysis for OCaml
POPL
Jan Hoffmann
Carnegie Mellon University
,
Ankush Das
Carnegie Mellon University
,
Shu-chun Weng
Yale University
14:20 - 16:00
Concurrency 2
POPL
at
Amphitheater 44
Chair(s):
Nobuko Yoshida
Imperial College London, UK
14:20
25m
Talk
Mixed-size Concurrency: ARM, POWER, C/C++11, and SC
POPL
Shaked Flur
University of Cambridge
,
Susmit Sarkar
University of St. Andrews, UK
,
Christopher Pulte
University of Cambridge
,
Kyndylan Nienhuis
University of Cambridge
,
Luc Maranget
INRIA Rocquencourt
,
Kathryn E. Gray
University of Cambridge
,
Ali Sezgin
University of Cambridge
,
Mark Batty
University of Kent
,
Peter Sewell
University of Cambridge
14:45
25m
Talk
Dynamic Race Detection For C++11
POPL
Christopher Lidbury
Imperial College London
,
Alastair F. Donaldson
Imperial College London
15:10
25m
Talk
Serializability for Eventual Consistency: Criterion, Analysis and Applications
POPL
Lucas Brutschy
ETH Zurich
,
Dimitar Dimitrov
ETH Zurich, Switzerland
,
Peter Müller
ETH Zurich
,
Martin Vechev
ETH Zurich
Pre-print
15:35
25m
Talk
Thread Modularity at Many Levels: a Pearl in Compositional Verification
POPL
Jochen Hoenicke
Universität Freiburg
,
Rupak Majumdar
MPI-SWS
,
Andreas Podelski
University of Freiburg, Germany
16:30 - 17:20
Semantic Foundations
POPL
at
Amphitheater 44
Chair(s):
Lars Birkedal
Aarhus University
16:30
25m
Talk
A Semantic Account of Metric Preservation
POPL
Arthur Azevedo de Amorim
University of Pennsylvania, USA
,
Ikram Cherigui
ENS Paris
,
Marco Gaboardi
SUNY Buffalo, USA
,
Justin Hsu
,
Shin-ya Katsumata
Kyoto University
16:55
25m
Talk
Cantor Meets Scott: Semantic Foundations for Probabilistic Networks
POPL
Steffen Smolka
Cornell University
,
Praveen Kumar
Cornell University
,
Nate Foster
Cornell University
,
Dexter Kozen
Cornell University
,
Alexandra Silva
University College London
DOI
File Attached
Fri 20 Jan
Displayed time zone:
Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
change
10:30 - 12:10
Verification and Synthesis
POPL
at
Amphitheater 44
Chair(s):
Benjamin Delaware
Purdue University
10:30
25m
Talk
Component-Based Synthesis for Complex APIs
POPL
Yu Feng
University of Texas at Austin, USA
,
Ruben Martins
,
Yuepeng Wang
University of Texas at Austin
,
Işıl Dillig
UT Austin
,
Thomas Reps
University of Wisconsin - Madison and Grammatech Inc.
10:55
25m
Talk
Learning nominal automata
POPL
Joshua Moerman
Radboud University
,
Matteo Sammartino
University College London
,
Alexandra Silva
University College London
,
Bartek Klin
University of Warsaw
,
Michał Szynwelski
University of Warsaw
11:20
25m
Talk
On Verifying Causal Consistency
POPL
Ahmed Bouajjani
IRIF, Université Paris Diderot
,
Constantin Enea
LIAFA, Université Paris Diderot
,
Rachid Guerraoui
,
Jad Hamza
LIAFA, Université Paris Diderot
11:45
25m
Talk
Complexity Verification Using Guided Theorem Enumeration
POPL
Akhilesh Srikanth
Georgia Institute of Technology
,
Burak Sahin
Georgia Institute of Technology
,
William Harris
14:20 - 16:00
Concurrency 3
POPL
at
Amphitheater 44
Chair(s):
Adam Chlipala
MIT
14:20
25m
Talk
Parallel Functional Arrays
POPL
Ananya Kumar
,
Guy E. Blelloch
Carnegie Mellon University
,
Robert Harper
14:45
25m
Talk
A Short Counterexample Property for Safety and Liveness Verification of Fault-tolerant Distributed Algorithms
POPL
Igor Konnov
TU Wien
,
Marijana Lazić
TU Wien
,
Helmut Veith
TU Wien
,
Josef Widder
TU Wien
DOI
Pre-print
15:10
25m
Talk
Analyzing divergence in bisimulation semantics
POPL
Xinxin Liu
Institute of software, Chinese academy of sciences
,
Tingting Yu
,
Wenhui Zhang
Institute of software, Chinese academy of sciences
15:35
25m
Talk
Fencing off Go: Liveness and Safety for Channel-Based Programming
POPL
Julien Lange
Imperial College London
,
Nicholas Ng
Imperial College London
,
Bernardo Toninho
Imperial College London
,
Nobuko Yoshida
Imperial College London, UK
Pre-print
16:30 - 17:45
Quantum
POPL
at
Amphitheater 44
Chair(s):
Michele Pagani
IRIF, Université Paris Diderot
16:30
25m
Talk
Invariants of Quantum Programs: Characterisations and Generation
POPL
Mingsheng Ying
University of Technology Sydney, Australia
,
Shenggang Ying
University of Technology Sydney, Australia
,
Xiaodi Wu
University of Oregon, USA
16:55
25m
Talk
The Geometry of Parallelism. Classical, Probabilistic, and Quantum Effects
POPL
Ugo Dal Lago
University of Bologna, France
,
Claudia Faggian
,
Benoit Valiron
LRI, CentraleSupelec, Univ. Paris Saclay
,
Akira Yoshimizu
Univ.Tokyo
17:20
25m
Talk
QWIRE: A Core Language for Quantum Circuits
POPL
Jennifer Paykin
,
Robert Rand
University of Pennsylvania
,
Steve Zdancewic
University of Pennsylvania
Sat 21 Jan
Displayed time zone:
Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
change
08:45 - 09:00
Opening
N40AI
at
Amphitheater 44
Chair(s):
Roberto Giacobazzi
University of Verona, Italy
08:45
15m
Day opening
Opening
N40AI
09:00 - 10:00
Industrial Panel 1
N40AI
at
Amphitheater 44
Chair(s):
Antoine Miné
UPMC, France
09:00
30m
Talk
Abstract Interpretation in Absint
N40AI
Christian Ferdinand
AbsInt
09:30
30m
Talk
Abstract Interpretation in Facebook
N40AI
Francesco Logozzo
Facebook
10:30 - 12:00
Industrial Panel 2 & Systems Biology
N40AI
at
Amphitheater 44
Chair(s):
Jerome Feret
INRIA Paris
10:30
30m
Talk
Abstract Interpretation in Amazon
N40AI
Byron Cook
Amazon
11:00
30m
Talk
Abstract Interpretation at Galois
N40AI
Aaron Tomb
Galois, Inc.
11:30
30m
Talk
Systems biology
N40AI
Vincent Danos
ENS Paris/CNRS
14:00 - 15:30
Security, Big Code and Synthesis
N40AI
at
Amphitheater 44
Chair(s):
Xavier Rival
INRIA/CNRS/ENS Paris
14:00
30m
Talk
Security
N40AI
Michael Hicks
University of Maryland at College Park, USA
14:30
30m
Talk
Big Code
N40AI
Bor-Yuh Evan Chang
University of Colorado Boulder
15:00
30m
Talk
Program synthesis
N40AI
Eran Yahav
Technion
16:00 - 18:30
System Verification and Patrick Cousot's Keynote
N40AI
at
Amphitheater 44
Chair(s):
Francesco Ranzato
University of Padova
16:00
30m
Talk
System verification
N40AI
Arie Gurfinkel
University of Waterloo
16:30
75m
Talk
Keynote: the Next 40 years of Abstract Interpretation
N40AI
Patrick Cousot
New York University
17:45
45m
Social Event
Concrete Cheese and Wine
N40AI
Sun 15 Jan
Displayed time zone:
Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
change
Room
9:00
30
10:00
30
11:00
30
12:00
30
13:00
30
14:00
30
15:00
30
16:00
30
17:00
30
Amphitheater 44
VMCAI
Invited talk 1
VMCAI
Program Analysis
VMCAI
Concurrency 1
VMCAI
Decision procedures
Mon 16 Jan
Displayed time zone:
Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
change
Room
9:00
30
10:00
30
11:00
30
12:00
30
13:00
30
14:00
30
15:00
30
16:00
30
17:00
30
Amphitheater 44
VMCAI
Invited talk 2
VMCAI
Numerical domains
VMCAI
Model-checking and bug finding
VMCAI
Symbolic analysis and invariant synthesis
Tue 17 Jan
Displayed time zone:
Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
change
Room
9:00
30
10:00
30
11:00
30
12:00
30
13:00
30
14:00
30
15:00
30
16:00
30
17:00
30
Amphitheater 44
VMCAI
Invited talk 3
VMCAI
Model Checking and Synthesis
VMCAI
Abstract Interpretation
VMCAI
Concurrency 2
Wed 18 Jan
Displayed time zone:
Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
change
Room
10:00
30
11:00
30
12:00
30
13:00
30
14:00
30
15:00
30
16:00
30
17:00
30
Amphitheater 44
POPL
Abstract Interpretation
POPL
Probabilistic Programming
POPL
Logic
Thu 19 Jan
Displayed time zone:
Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
change
Room
10:00
30
11:00
30
12:00
30
13:00
30
14:00
30
15:00
30
16:00
30
17:00
30
Amphitheater 44
POPL
Program Analysis
POPL
Concurrency 2
POPL
Semantic Foundations
Fri 20 Jan
Displayed time zone:
Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
change
Room
10:00
30
11:00
30
12:00
30
13:00
30
14:00
30
15:00
30
16:00
30
17:00
30
Amphitheater 44
POPL
Verification and Synthesis
POPL
Concurrency 3
POPL
Quantum
Sat 21 Jan
Displayed time zone:
Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
change
Room
8:00
30
9:00
30
10:00
30
11:00
30
12:00
30
13:00
30
14:00
30
15:00
30
16:00
30
17:00
30
18:00
30
Amphitheater 44
N40AI
Opening
N40AI
Industrial Panel 1
N40AI
Industrial Panel 2 & Systems Biology
N40AI
Security, Big Code and Synthesis
N40AI
System Verification and Patrick Cousot's Keynote
Sun 15 Jan
Displayed time zone:
Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
change
Room
9:00
15
30
45
10:00
15
30
45
11:00
15
30
45
12:00
15
30
45
13:00
15
30
45
14:00
15
30
45
15:00
15
30
45
16:00
15
30
45
17:00
15
30
45
Amphitheater 44
VMCAI
Detecting Strict Aliasing Violations in the Wild
09:00 - 10:00
VMCAI
Partitioned Memory Models for Program Analysis.
10:30 - 11:00
VMCAI
Property Directed Reachability for Proving Absence of Concurrent Modifi ...
11:00 - 11:30
VMCAI
Stabilizing Floating-Point Programs using Provenance Analysis
11:30 - 12:00
VMCAI
Accuracy of Message Counting Abstraction in Fault-Tolerant Distributed ...
14:00 - 14:30
VMCAI
Independence Abstractions and Models of Concurrency
14:30 - 15:00
VMCAI
Static Analysis of Communicating Process using Symbolic Transducers
15:00 - 15:30
VMCAI
Synthesising Strategy Improvement and Recursive Algorithms for Solving ...
16:00 - 16:30
VMCAI
Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic
16:30 - 17:00
VMCAI
Matching multiplications in Bit-Vector formulas
17:00 - 17:30
Mon 16 Jan
Displayed time zone:
Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
change
Room
9:00
15
30
45
10:00
15
30
45
11:00
15
30
45
12:00
15
30
45
13:00
15
30
45
14:00
15
30
45
15:00
15
30
45
16:00
15
30
45
17:00
15
30
45
Amphitheater 44
VMCAI
Verified Concurrent Code: Tricks of the Trade
09:00 - 10:00
VMCAI
Sound Bit-Precise Numerical Domains
10:30 - 11:00
VMCAI
Efficient Elimination of Redundancies in Polyhedra using Raytracing
11:00 - 11:30
VMCAI
Finding Relevant Templates via the Principal Component Analysis
11:30 - 12:00
VMCAI
Effective Bug Finding in C Programs with Shape and Effect Abstraction
14:00 - 14:30
VMCAI
Reduction of Workflow Nets for Generalised Soundness Verification
14:30 - 15:00
VMCAI
Dynamic Reductions for Model Checking Concurrent Software.
15:00 - 15:30
VMCAI
Block-wise abstract interpretation by combining abstract domains with SMT
16:00 - 16:30
VMCAI
IC3 - Flipping the E in ICE
16:30 - 17:00
VMCAI
Counterexample Validation and Interpolation-Based Refinement for Forest ...
17:00 - 17:30
Tue 17 Jan
Displayed time zone:
Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
change
Room
9:00
15
30
45
10:00
15
30
45
11:00
15
30
45
12:00
15
30
45
13:00
15
30
45
14:00
15
30
45
15:00
15
30
45
16:00
15
30
45
17:00
15
30
45
Amphitheater 44
VMCAI
Verification of Cancer Programs
09:00 - 10:00
VMCAI
Reachability for dynamic parametric processes
10:30 - 11:00
VMCAI
Synthesizing Non-Vacuous Systems
11:00 - 11:30
VMCAI
Solving Nonlinear Integer Arithmetic with MCSat
11:30 - 12:00
VMCAI
Complete Abstractions and Subclassical Modal Logics
14:00 - 14:30
VMCAI
Structuring Abstract Interpreters through State and Value Abstractions
14:30 - 15:00
VMCAI
Conjunctive Abstract Interpretation using Paramodulation
15:00 - 15:30
VMCAI
Using Abstract Interpretation to Correct Synchronization Faults
16:00 - 16:30
VMCAI
Detecting All High-Level Dataraces in an RTOS Kernel.
16:30 - 17:00
VMCAI
Precise Thread-Modular Abstract Interpretation of Concurrent Programs u ...
17:00 - 17:30
Wed 18 Jan
Displayed time zone:
Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
change
Room
10:00
15
30
45
11:00
15
30
45
12:00
15
30
45
13:00
15
30
45
14:00
15
30
45
15:00
15
30
45
16:00
15
30
45
17:00
15
30
45
Amphitheater 44
POPL
Ogre and Pythia, An invariance proof method for weak consistency models
10:30 - 10:55
POPL
A Posteriori Environment Analysis with Pushdown Delta CFA
10:55 - 11:20
POPL
Semantic-Directed Clumping of Disjunctive Abstract States
11:20 - 11:45
POPL
Fast Polyhedra Abstract Domain
11:45 - 12:10
POPL
Beginner's Luck: A Language for Property-Based Generators
14:20 - 14:45
POPL
Exact Bayesian Inference by Symbolic Disintegration
14:45 - 15:10
POPL
Stochastic Invariants for Probabilistic Termination
15:10 - 15:35
POPL
Coupling proofs are probabilistic product programs
15:35 - 16:00
POPL
Monadic second-order logic on finite sequences
16:30 - 16:55
POPL
On the Relationship Between Higher-Order Recursion Schemes and Higher-O ...
16:55 - 17:20
POPL
Coming to Terms with Quantified Reasoning
17:20 - 17:45
Thu 19 Jan
Displayed time zone:
Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
change
Room
10:00
15
30
45
11:00
15
30
45
12:00
15
30
45
13:00
15
30
45
14:00
15
30
45
15:00
15
30
45
16:00
15
30
45
17:00
15
30
45
Amphitheater 44
POPL
Relational Cost Analysis
10:30 - 10:55
POPL
Contract-based Resource Verification for Higher-order Functions with Me ...
10:55 - 11:20
POPL
Context-sensitive data dependence analysis via Linear Conjunctive Langu ...
11:20 - 11:45
POPL
Towards Automatic Resource Bound Analysis for OCaml
11:45 - 12:10
POPL
Mixed-size Concurrency: ARM, POWER, C/C++11, and SC
14:20 - 14:45
POPL
Dynamic Race Detection For C++11
14:45 - 15:10
POPL
Serializability for Eventual Consistency: Criterion, Analysis and Appli ...
15:10 - 15:35
POPL
Thread Modularity at Many Levels: a Pearl in Compositional Verification
15:35 - 16:00
POPL
A Semantic Account of Metric Preservation
16:30 - 16:55
POPL
Cantor Meets Scott: Semantic Foundations for Probabilistic Networks
16:55 - 17:20
Fri 20 Jan
Displayed time zone:
Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
change
Room
10:00
15
30
45
11:00
15
30
45
12:00
15
30
45
13:00
15
30
45
14:00
15
30
45
15:00
15
30
45
16:00
15
30
45
17:00
15
30
45
Amphitheater 44
POPL
Component-Based Synthesis for Complex APIs
10:30 - 10:55
POPL
Learning nominal automata
10:55 - 11:20
POPL
On Verifying Causal Consistency
11:20 - 11:45
POPL
Complexity Verification Using Guided Theorem Enumeration
11:45 - 12:10
POPL
Parallel Functional Arrays
14:20 - 14:45
POPL
A Short Counterexample Property for Safety and Liveness Verification of ...
14:45 - 15:10
POPL
Analyzing divergence in bisimulation semantics
15:10 - 15:35
POPL
Fencing off Go: Liveness and Safety for Channel-Based Programming
15:35 - 16:00
POPL
Invariants of Quantum Programs: Characterisations and Generation
16:30 - 16:55
POPL
The Geometry of Parallelism. Classical, Probabilistic, and Quantum Effects
16:55 - 17:20
POPL
QWIRE: A Core Language for Quantum Circuits
17:20 - 17:45
Sat 21 Jan
Displayed time zone:
Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
change
Room
8:00
15
30
45
9:00
15
30
45
10:00
15
30
45
11:00
15
30
45
12:00
15
30
45
13:00
15
30
45
14:00
15
30
45
15:00
15
30
45
16:00
15
30
45
17:00
15
30
45
18:00
15
30
45
Amphitheater 44
N40AI
Opening
08:45 - 09:00
N40AI
Abstract Interpretation in Absint
09:00 - 09:30
N40AI
Abstract Interpretation in Facebook
09:30 - 10:00
N40AI
Abstract Interpretation in Amazon
10:30 - 11:00
N40AI
Abstract Interpretation at Galois
11:00 - 11:30
N40AI
Systems biology
11:30 - 12:00
N40AI
Security
14:00 - 14:30
N40AI
Big Code
14:30 - 15:00
N40AI
Program synthesis
15:00 - 15:30
N40AI
System verification
16:00 - 16:30
N40AI
Keynote: the Next 40 years of Abstract Interpretation
16:30 - 17:45
N40AI
Concrete Cheese and Wine
17:45 - 18:30
x
Sat 23 Nov 11:09