POPL 2017
Sun 15 - Sat 21 January 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
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

09:00 - 10:00
Invited talk 1VMCAI at Amphitheater 44
Chair(s): David MonniauxCNRS, VERIMAG
09:00
60m
Talk
Detecting Strict Aliasing Violations in the Wild
VMCAI
Pascal CuoqTrust-in-Soft
File Attached
10:30 - 12:00
Program AnalysisVMCAI at Amphitheater 44
Chair(s): Boris YakobowskiCEA - LIST
10:30
30m
Talk
Partitioned Memory Models for Program Analysis.
VMCAI
Wei WangGoogle, Inc., Clark BarrettStanford University, Thomas WiesNew York University
File Attached
11:00
30m
Talk
Property Directed Reachability for Proving Absence of Concurrent Modification Errors
VMCAI
Asya FrumkinTel Aviv University, Yotam M. Y. FeldmanTel Aviv University, Ondřej LhotákUniversity of Waterloo, Canada, Oded PadonTel Aviv University, Mooly SagivTel Aviv University, Sharon ShohamTel Aviv university
File Attached
11:30
30m
Talk
Stabilizing Floating-Point Programs using Provenance Analysis
VMCAI
Yijia GuNortheastern University, Thomas WahlNortheastern University
16:00 - 17:30
Decision proceduresVMCAI at Amphitheater 44
Chair(s): Andreas PodelskiUniversity of Freiburg, Germany
16:00
30m
Talk
Synthesising Strategy Improvement and Recursive Algorithms for Solving 2.5 Player Parity Games
VMCAI
Ernst Moritz HahnState Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Sven ScheweUniversity of Liverpool, Andrea TurriniState Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Lijun ZhangInstitute 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 ReynoldsEPFL, Radu IosifVERIMAG, CNRS, Université Grenoble-Alpes, Cristina SerbanVERIMAG, CNRS, Université Grenoble-Alpes
File Attached
17:00
30m
Talk
Matching multiplications in Bit-Vector formulas
VMCAI
Supratik ChakrabortyIIT Bombay, Ashutosh Gupta, Rahul JainTata Institute of Fundamental Research
File Attached

Mon 16 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

09:00 - 10:00
Invited talk 2VMCAI at Amphitheater 44
Chair(s): Ahmed BouajjaniIRIF, Université Paris Diderot
09:00
60m
Talk
Verified Concurrent Code: Tricks of the Trade
VMCAI
A: Ernie CohenAmazon Web Services
10:30 - 12:00
Numerical domainsVMCAI at Amphitheater 44
Chair(s): Laure GonnordUniversity of Lyon & LIP, France
10:30
30m
Talk
Sound Bit-Precise Numerical Domains
VMCAI
Tushar SharmaUniversity of Wisconsin - Madison, USA, Thomas RepsUniversity 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 SeladjiUniversity of Tlemcen
File Attached
14:00 - 15:30
Model-checking and bug findingVMCAI at Amphitheater 44
Chair(s): Andreas PodelskiUniversity of Freiburg, Germany
14:00
30m
Talk
Effective Bug Finding in C Programs with Shape and Effect Abstraction
VMCAI
Iago AbalIT University of Copenhagen, Claus BrabrandIT University of Copenhagen, Denmark, Andrzej WąsowskiIT University of Copenhagen, Denmark
14:30
30m
Talk
Reduction of Workflow Nets for Generalised Soundness Verification
VMCAI
Hadrien BrideFemto-ST / Université de Franche-Comté, Olga KouchnarenkoFemto-ST / Université de Franche-Comté, Fabien PeureuxFemto-ST / Université de Franche-Comté + Smartesting S&S
Media Attached
15:00
30m
Talk
Dynamic Reductions for Model Checking Concurrent Software.
VMCAI
Henning GüntherTechnische Universität Wien, Alfons LaarmanVienna University of Technology, Ana SokolovaUniversity of Salzburg, Georg WeissenbacherTechnische Universität Wien
File Attached
16:00 - 17:30
Symbolic analysis and invariant synthesisVMCAI at Amphitheater 44
Chair(s): Constantin EneaLIAFA, 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 GurfinkelUniversity of Waterloo, Sharon ShohamTel Aviv university, Sharad MalikPrinceton University
17:00
30m
Talk
Counterexample Validation and Interpolation-Based Refinement for Forest Automata
VMCAI
Lukáš Holík, Martin HruskaBrno University of Technology , Ondřej LengálBrno University of Technology , Adam RogalewiczBrno University of Technology , Tomáš VojnarBrno University of Technology

Tue 17 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

09:00 - 10:00
Invited talk 3VMCAI at Amphitheater 44
Chair(s): Andreas PodelskiUniversity of Freiburg, Germany
09:00
60m
Talk
Verification of Cancer Programs
VMCAI
Jasmin FisherMicrosoft Research
10:30 - 12:00
Model Checking and SynthesisVMCAI at Amphitheater 44
Chair(s): Ahmed BouajjaniIRIF, Université Paris Diderot
10:30
30m
Talk
Reachability for dynamic parametric processes
VMCAI
Anca MuschollUniversité de Bordeaux / LaBRI, Helmut SeidlTechnische Universität München, Igor WalukiewiczCNRS, LaBRI
11:00
30m
Talk
Synthesizing Non-Vacuous Systems
VMCAI
Roderick BloemInstitute of Software Technology, Graz University of Technology , Hana Chockler, Masoud EbrahimiInstitute of Applied Information Processing and Communications, Graz University of Technology, Ofer StrichmanTechnion
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 GiacobazziUniversity of Verona, Italy
14:00
30m
Talk
Complete Abstractions and Subclassical Modal Logics
VMCAI
Vijay D'SilvaGoogle, Marcelo SousaUniversity of Oxford
14:30
30m
Talk
Structuring Abstract Interpreters through State and Value Abstractions
VMCAI
David BühlerCEA LIST, Boris YakobowskiCEA - LIST, Sandrine BlazyUniversity of Rennes 1, France
Media Attached
15:00
30m
Talk
Conjunctive Abstract Interpretation using Paramodulation
VMCAI
Mooly SagivTel Aviv University, A: Or OzeriTel Aviv university, Oded PadonTel Aviv University, Noam RinetzkyTel Aviv University
Media Attached
16:00 - 17:30
Concurrency 2VMCAI at Amphitheater 44
Chair(s): David MonniauxCNRS, VERIMAG
16:00
30m
Talk
Using Abstract Interpretation to Correct Synchronization Faults
VMCAI
Pietro FerraraIBM Research, Omer TrippIBM Thomas J. Watson Research Center, Peng LiuPurdue University, Eric KoskinenYale University
16:30
30m
Talk
Detecting All High-Level Dataraces in an RTOS Kernel.
VMCAI
Suvam MukherjeeIndian Institute of Science, Arunkumar SIndian 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 MonatEcole Normale Supérieure de Lyon, Antoine MinéUPMC, France

Wed 18 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

10:30 - 12:10
Abstract InterpretationPOPL at Amphitheater 44
Chair(s): Isabella MastroeniUniversity of Verona, Italy
10:30
25m
Talk
Ogre and Pythia, An invariance proof method for weak consistency models
POPL
Jade AlglaveUniversity College London, Patrick CousotNew York University
10:55
25m
Talk
A Posteriori Environment Analysis with Pushdown Delta CFA
POPL
Kimball GermaneUniversity of Utah, Matthew MightUniversity of Utah; Harvard Medical School; The White House
11:20
25m
Talk
Semantic-Directed Clumping of Disjunctive Abstract States
POPL
Huisong LiINRIA/CNRS/ENS/PSL*, François BérengerINRIA/CNRS/ENS/PSL*, Bor-Yuh Evan ChangUniversity of Colorado Boulder, Xavier RivalINRIA/CNRS/ENS Paris
11:45
25m
Talk
Fast Polyhedra Abstract Domain
POPL
Gagandeep SinghETH Zurich, Switzerland, Markus PüschelETH Zurich, Martin VechevETH Zurich
14:20 - 16:00
Probabilistic ProgrammingPOPL at Amphitheater 44
Chair(s): Marco GaboardiSUNY Buffalo, USA
14:20
25m
Talk
Beginner's Luck: A Language for Property-Based Generators
POPL
Leonidas LampropoulosUniversity of Pennsylvania, Diane Gallois-WongInria Paris, ENS Paris, Cătălin HriţcuInria Paris, John HughesChalmers University of Technology, Benjamin C. PierceUniversity of Pennsylvania, Li-yao XiaENS Paris
Pre-print
14:45
25m
Talk
Exact Bayesian Inference by Symbolic Disintegration
POPL
Chung-chieh ShanIndiana University, USA, Norman Ramsey
Pre-print
15:10
25m
Talk
Stochastic Invariants for Probabilistic Termination
POPL
Krishnendu ChatterjeeIST Austria, Petr NovotnyIST Austria, Djordje ZikelicUniversity of Cambridge
15:35
25m
Talk
Coupling proofs are probabilistic product programs
POPL
16:30 - 17:45
LogicPOPL at Amphitheater 44
Chair(s): Alexandra SilvaUniversity College London
16:30
25m
Talk
Monadic second-order logic on finite sequences
POPL
Loris D'AntoniUniversity of Wisconsin–Madison, Margus VeanesMicrosoft Research
16:55
25m
Talk
On the Relationship Between Higher-Order Recursion Schemes and Higher-Order Fixpoint Logic
POPL
Naoki KobayashiUniversity of Tokyo, Japan, Etienne LozesENS Cachan, Florian BruseUniversity of Kassel
17:20
25m
Talk
Coming to Terms with Quantified Reasoning
POPL
Simon RobillardChalmers University of Technology, Andrei VoronkovUniversity of Manchester, Laura KovacsChalmers University of Technology

Thu 19 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

10:30 - 12:10
Program AnalysisPOPL at Amphitheater 44
Chair(s): Francesco LogozzoFacebook
10:30
25m
Talk
Relational Cost Analysis
POPL
Ezgi ÇiçekMPI-SWS, Germany, Gilles BartheIMDEA, Marco GaboardiSUNY Buffalo, USA, Deepak GargMPI-SWS, Germany, Jan HoffmannCarnegie Mellon University
10:55
25m
Talk
Contract-based Resource Verification for Higher-order Functions with Memoization
POPL
Ravichandhran MadhavanEPFL, Sumith KulalIIT Bombay, Viktor KunčakEPFL, Switzerland
11:20
25m
Talk
Context-sensitive data dependence analysis via Linear Conjunctive Language Reachability
POPL
Qirun ZhangUniversity of California, Davis, Zhendong SuUniversity of California, Davis
11:45
25m
Talk
Towards Automatic Resource Bound Analysis for OCaml
POPL
Jan HoffmannCarnegie Mellon University, Ankush DasCarnegie Mellon University, Shu-chun WengYale University
14:20 - 16:00
Concurrency 2POPL at Amphitheater 44
Chair(s): Nobuko YoshidaImperial College London, UK
14:20
25m
Talk
Mixed-size Concurrency: ARM, POWER, C/C++11, and SC
POPL
Shaked FlurUniversity of Cambridge, Susmit SarkarUniversity of St. Andrews, UK, Christopher PulteUniversity of Cambridge, Kyndylan NienhuisUniversity of Cambridge, Luc MarangetINRIA Rocquencourt, Kathryn E. GrayUniversity of Cambridge, Ali SezginUniversity of Cambridge, Mark BattyUniversity of Kent, Peter SewellUniversity of Cambridge
14:45
25m
Talk
Dynamic Race Detection For C++11
POPL
Christopher LidburyImperial College London, Alastair DonaldsonImperial College London
15:10
25m
Talk
Serializability for Eventual Consistency: Criterion, Analysis and Applications
POPL
Lucas BrutschyETH Zurich, Dimitar DimitrovETH Zurich, Switzerland, Peter MüllerETH Zurich, Martin VechevETH Zurich
Pre-print
15:35
25m
Talk
Thread Modularity at Many Levels: a Pearl in Compositional Verification
POPL
Jochen HoenickeUniversität Freiburg, Rupak MajumdarMPI-SWS, Andreas PodelskiUniversity of Freiburg, Germany
16:30 - 17:20
Semantic FoundationsPOPL at Amphitheater 44
Chair(s): Lars BirkedalAarhus University
16:30
25m
Talk
A Semantic Account of Metric Preservation
POPL
Arthur Azevedo de AmorimUniversity of Pennsylvania, USA, Ikram CheriguiENS Paris, Marco GaboardiSUNY Buffalo, USA, Justin Hsu, Shin-ya KatsumataKyoto University
16:55
25m
Talk
Cantor Meets Scott: Semantic Foundations for Probabilistic Networks
POPL
Steffen SmolkaCornell University, Praveen KumarCornell University, Nate FosterCornell University, Dexter KozenCornell University, Alexandra SilvaUniversity College London
DOI File Attached

Fri 20 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

10:30 - 12:10
Verification and SynthesisPOPL at Amphitheater 44
Chair(s): Benjamin DelawarePurdue University
10:30
25m
Talk
Component-Based Synthesis for Complex APIs
POPL
Yu FengUniversity of Texas at Austin, USA, Ruben Martins, Yuepeng WangUniversity of Texas at Austin, Isil DilligUT Austin, Thomas RepsUniversity of Wisconsin - Madison and Grammatech Inc.
10:55
25m
Talk
Learning nominal automata
POPL
Joshua MoermanRadboud University, Matteo SammartinoUniversity College London, Alexandra SilvaUniversity College London, Bartek KlinUniversity of Warsaw, Michał SzynwelskiUniversity of Warsaw
11:20
25m
Talk
On Verifying Causal Consistency
POPL
Ahmed BouajjaniIRIF, Université Paris Diderot, Constantin EneaLIAFA, Université Paris Diderot, Rachid Guerraoui, Jad HamzaLIAFA, Université Paris Diderot
11:45
25m
Talk
Complexity Verification Using Guided Theorem Enumeration
POPL
Akhilesh SrikanthGeorgia Institute of Technology, Burak SahinGeorgia Institute of Technology, William Harris
14:20 - 16:00
Concurrency 3POPL at Amphitheater 44
Chair(s): Adam ChlipalaMIT
14:20
25m
Talk
Parallel Functional Arrays
POPL
Ananya Kumar, Guy E. BlellochCarnegie Mellon University, Robert Harper
14:45
25m
Talk
A Short Counterexample Property for Safety and Liveness Verification of Fault-tolerant Distributed Algorithms
POPL
Igor KonnovTU Wien, Marijana LazićTU Wien, Helmut VeithTU Wien, Josef WidderTU Wien
DOI Pre-print
15:10
25m
Talk
Analyzing divergence in bisimulation semantics
POPL
Xinxin LiuInstitute of software, Chinese academy of sciences, Tingting Yu, Wenhui ZhangInstitute of software, Chinese academy of sciences
15:35
25m
Talk
Fencing off Go: Liveness and Safety for Channel-Based Programming
POPL
Julien LangeImperial College London, Nicholas NgImperial College London, Bernardo ToninhoImperial College London, Nobuko YoshidaImperial College London, UK
Pre-print
16:30 - 17:45
QuantumPOPL at Amphitheater 44
Chair(s): Michele PaganiIRIF, Université Paris Diderot
16:30
25m
Talk
Invariants of Quantum Programs: Characterisations and Generation
POPL
Mingsheng YingUniversity of Technology Sydney, Australia, Shenggang YingUniversity of Technology Sydney, Australia, Xiaodi WuUniversity of Oregon, USA
16:55
25m
Talk
The Geometry of Parallelism. Classical, Probabilistic, and Quantum Effects
POPL
Ugo Dal LagoUniversity of Bologna, France, Claudia Faggian, Benoit ValironLRI, CentraleSupelec, Univ. Paris Saclay, Akira YoshimizuUniv.Tokyo
17:20
25m
Talk
QWIRE: A Core Language for Quantum Circuits
POPL
Jennifer Paykin, Robert RandUniversity of Pennsylvania, Steve ZdancewicUniversity of Pennsylvania

Sat 21 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

08:45 - 09:00
OpeningN40AI at Amphitheater 44
Chair(s): Roberto GiacobazziUniversity 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 FeretINRIA Paris
10:30
30m
Talk
Abstract Interpretation in Amazon
N40AI
11:00
30m
Talk
Abstract Interpretation at Galois
N40AI
Aaron TombGalois, Inc.
11:30
30m
Talk
Systems biology
N40AI
Vincent DanosENS Paris/CNRS
14:00 - 15:30
Security, Big Code and Synthesis N40AI at Amphitheater 44
Chair(s): Xavier RivalINRIA/CNRS/ENS Paris
14:00
30m
Talk
Security
N40AI
Michael HicksUniversity of Maryland at College Park, USA
14:30
30m
Talk
Big Code
N40AI
Bor-Yuh Evan ChangUniversity of Colorado Boulder
15:00
30m
Talk
Program synthesis
N40AI
Eran YahavTechnion
16:00 - 18:30
System Verification and Patrick Cousot's KeynoteN40AI at Amphitheater 44
Chair(s): Francesco RanzatoUniversity of Padova
16:00
30m
Talk
System verification
N40AI
Arie GurfinkelUniversity of Waterloo
16:30
75m
Talk
Keynote: the Next 40 years of Abstract Interpretation
N40AI
Patrick CousotNew York University
17:45
45m
Social Event
Concrete Cheese and Wine
N40AI

Sun 15 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

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

Mon 16 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Tue 17 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Wed 18 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

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

Thu 19 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

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

Fri 20 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

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

Sat 21 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Sat 21 Jan
Times are displayed in 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