Amphitheater 44 - VMCAI 2017

VenueParis Jussieu

Room nameAmphitheater 44

Floor0

Capacity240

Room InformationNo extra information available

Program

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, ViennaSelect other time zone

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 programSpecify 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 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 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 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 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 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 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 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 Christian Ferdinand AbsInt
09:30 30m Talk		Abstract Interpretation in Facebook N40AI Francesco Logozzo Facebook

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


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

Room information: Amphitheater 44

Program Display Configuration

Sun 15 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Mon 16 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Tue 17 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Wed 18 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Thu 19 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Fri 20 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Sat 21 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Sun 15 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

VMCAI

VMCAI

VMCAI

VMCAI

Mon 16 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

VMCAI

VMCAI

VMCAI

VMCAI

Tue 17 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

VMCAI

VMCAI

VMCAI

VMCAI

Wed 18 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

POPL

POPL

POPL

Thu 19 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

POPL

POPL

POPL

Fri 20 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

POPL

POPL

POPL

Sat 21 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

N40AI

N40AI

N40AI

N40AI

N40AI

Sun 15 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Mon 16 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Tue 17 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Wed 18 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Thu 19 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Fri 20 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Sat 21 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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