Write a Blog >>
VMCAI 2017
Sun 15 - Tue 17 January 2017
co-located with POPL 2017
VenueParis Jussieu
Room nameAmphitheater 44
Floor0
Capacity240
Room InformationNo extra information available
Program

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 1VMCAI 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 AnalysisVMCAI 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 1VMCAI 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
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 proceduresVMCAI 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 2VMCAI 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 domainsVMCAI 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
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 findingVMCAI 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 synthesisVMCAI 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
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 3VMCAI 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 SynthesisVMCAI 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 InterpretationVMCAI 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 2VMCAI 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 InterpretationPOPL 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 ProgrammingPOPL 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
LogicPOPL 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 AnalysisPOPL 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 2POPL 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 FoundationsPOPL 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 SynthesisPOPL 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 3POPL 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
QuantumPOPL 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
OpeningN40AI at Amphitheater 44
Chair(s): Roberto Giacobazzi University of Verona, Italy
08:45
15m
Day opening
Opening
N40AI

09:00 - 10:00
Industrial Panel 1N40AI at Amphitheater 44
Chair(s): Antoine Miné UPMC, France
09:00
30m
Talk
Abstract Interpretation in Absint
N40AI
09:30
30m
Talk
Abstract Interpretation in Facebook
N40AI
10:30 - 12:00
Industrial Panel 2 & Systems BiologyN40AI 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 KeynoteN40AI 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

Room9:003010:003011:003012:003013:003014:003015:003016:003017:0030
Amphitheater 44

Mon 16 Jan

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Tue 17 Jan

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Wed 18 Jan

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Room10:003011:003012:003013:003014:003015:003016:003017:0030
Amphitheater 44

Thu 19 Jan

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Room10:003011:003012:003013:003014:003015:003016:003017:0030
Amphitheater 44

Fri 20 Jan

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Room10:003011:003012:003013:003014:003015:003016:003017:0030
Amphitheater 44

Sat 21 Jan

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Sat 21 Jan

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Room8:001530459:0015304510:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:0015304518:00153045
Amphitheater 44
N40AI
Opening
08:45 - 09:00
N40AI
Security
14:00 - 14:30
N40AI
Big Code
14:30 - 15:00