You're viewing the program in a time zone which is different from your device's time zone - change time zone

Sun 7 Jan
Times are displayed in time zone: Tijuana, Baja California change

09:00 - 10:00
Invited Talk by Ranjit JhalaVMCAI at Watercourt
Chair(s): Isil DilligUT Austin
09:00
60m
Talk
Reasoning about Functions
VMCAI
Ranjit JhalaUniversity of California, San Diego
10:30 - 12:00
SynthesisVMCAI at Watercourt
Chair(s): K. Rustan M. LeinoAmazon
10:30
30m
Talk
Abstraction-Based Interaction Model for Synthesis
VMCAI
Hila Peleg, Shachar ItzhakyTechnion, Israel, Sharon ShohamTel Aviv university
11:00
30m
Talk
A Framework for Computer-Aided Design of Educational Domain Models
VMCAI
Eric ButlerUniversity of Washington, Emina TorlakUniversity of Washington, Zoran PopovicUniversity of Washington
11:30
30m
Talk
Generating Tests by Example
VMCAI
Hila Peleg, Dan RasinTechnion – Israel Institute of Technology, Eran YahavTechnion
14:00 - 15:30
VerificationVMCAI at Watercourt
Chair(s): Jeffrey S. FosterUniversity of Maryland, College Park
14:00
30m
Talk
Gradual Program Verification
VMCAI
Johannes BaderMicrosoft, Jonathan AldrichCarnegie Mellon University, Éric TanterUniversity of Chile
14:30
30m
Talk
A Logical System for Modular Information Flow Verification
VMCAI
Adi PrabawaNational University of Singapore, Mahmudul Faisal Al AmeenNational University of Singapore, Benedict LeeNational University of Singapore, Wei-Ngan ChinNational University of Singapore
15:00
30m
Talk
P5: Planner-less Proofs of Probabilistic Parameterized Protocols
VMCAI
16:00 - 17:30
SecurityVMCAI at Watercourt
Chair(s): Francesco RanzatoUniversity of Padova
16:00
30m
Talk
Code Obfuscation Against Abstract Model Checking Attacks
VMCAI
Roberto BruniDipartimento di Informatica, Universita' di Pisa, Roberto GiacobazziUniversity of Verona and IMDEA Software Institute, Roberta GoriDipartimento di Informatica, Universita' di Pisa
16:30
30m
Talk
Scalable Approximation of Quantitative Information Flow in Programs
VMCAI
Fabrizio BiondiCentraleSupelec Rennes, Mike EnescuINRIA, Annelie HeuserCNRS/IRISA, Axel Legay, Kuldeep S. MeelNational University of Singapore, Jean QuilbeufINRIA
17:00
30m
Talk
Abstract Code Injection - A Semantic Approach Based on Abstract Non-Interference
VMCAI
Samuele BuroUniversità degli Studi di Verona, Isabella MastroeniUniversity of Verona, Italy

Mon 8 Jan
Times are displayed in time zone: Tijuana, Baja California change

09:00 - 10:30
Equational reasoning for probabilistic programmingTutorialFest at Bradbury
09:00
90m
Talk
Equational reasoning for probabilistic programming.
TutorialFest
A: Chung-chieh ShanIndiana University, USA
Media Attached
09:00 - 10:30
Programming and Reasoning with Infinite Data in IsabelleTutorialFest at Hershey
09:00
90m
Talk
Programming and Reasoning with Infinite Data in Isabelle/HOL.
TutorialFest
A: Mathias FleuryMPI-INF, A: Andreas Lochbihler, A: Andrei PopescuMiddlesex University, London
Media Attached
09:00 - 10:00
Invited Talk by René ThiemannCPP at Museum A
Chair(s): June AndronickData61,CSIRO (formerly NICTA) and UNSW
09:00
60m
Talk
Efficient Certification of Complexity Proofs: Formalizing the Perron–Frobenius Theorem (Invited Talk Paper)
CPP
Jose Divasón, Sebastiaan Joosten, Ondřej KunčarTechnische Universität München, Germany, René ThiemannUniversity of Innsbruck, Akihisa Yamada
DOI
09:00 - 10:30
Message-Passing Concurrency and Substructural LogicsTutorialFest at Museum B
09:00
90m
Talk
Message-Passing Concurrency and Substructural Logics
TutorialFest
Frank PfenningCarnegie Mellon University, USA
Media Attached
09:00 - 10:00
Invited Talk by Kenneth L. McMillanVMCAI at Watercourt
Chair(s): Lenore Zuck
09:00
60m
Talk
How to Stay Decidable
VMCAI
Kenneth L. McMillanMicrosoft Research
09:00 - 10:30
Code ObfuscationTutorialFest at Widney
09:00
90m
Talk
Code Obfuscation - A Hacking view on program analysis and understanding.
TutorialFest
A: Roberto GiacobazziUniversity of Verona and IMDEA Software Institute
Media Attached
10:30 - 12:00
Session 1-1PEPM at Crocker
Chair(s): Hsiang-Shang ‘Josh’ KoNational Institute of Informatics, Japan
10:30
60m
Talk
Developments in Property-Based Testing (Invited Talk)
PEPM
Jan MidtgaardUniversity of Southern Denmark
DOI
11:30
30m
Talk
Selective CPS Transformation for Shift and Reset
PEPM
Kenichi AsaiOchanomizu University, Chihiro UeharaOchanomizu University
DOI
10:30 - 12:00
Verifying Programs and SystemsCPP at Museum A
Chair(s): Natarajan ShankarSRI International, USA
10:30
30m
Talk
Total Haskell is Reasonable Coq
CPP
Antal Spector-Zabusky, Joachim BreitnerUniversity of Pennsylvania, Christine RizkallahUniversity of Pennsylvania, USA, Stephanie WeirichUniversity of Pennsylvania, USA
DOI
11:00
30m
Talk
A Formal Proof in Coq of a Control Function for the Inverted Pendulum
CPP
Damien RouhlingUniversity of Côte d'Azur, France
DOI
11:30
30m
Talk
Completeness and Decidability of Converse PDL in the Constructive Type Theory of Coq
CPP
Christian DoczkalCNRS, France, Joachim BardSaarland University, Germany
DOI
10:30 - 12:00
Abstract InterpretationVMCAI at Watercourt
Chair(s): Patrick Cousot
10:30
30m
Talk
On Constructivity of Galois Connections
VMCAI
Francesco RanzatoUniversity of Padova
11:00
30m
Talk
An Abstract Interpretation Framework for the Round-Off Error Analysis of Floating-Point Programs
VMCAI
Laura TitoloNational Institute of Aerospace, USA, Marco A. FeliuNational Institute of Aerospace, Mariano MoscatoNational Institute of Aerospace, Cesar MunozNASA
11:30
30m
Talk
Modular Analysis of Executables using On-Demand Heyting Completion
VMCAI
Julian KranzTechnical University of Munich, Axel SimonGoogle
11:00 - 12:00
Equational reasoning for probabilistic programmingTutorialFest at Bradbury
11:00
60m
Talk
Equational reasoning for probabilistic programming.
TutorialFest
A: Chung-chieh ShanIndiana University, USA
Media Attached
11:00 - 12:00
Programming and Reasoning with Infinite Data in IsabelleTutorialFest at Hershey
11:00
60m
Talk
Programming and Reasoning with Infinite Data in Isabelle/HOL.
TutorialFest
A: Mathias FleuryMPI-INF, A: Andreas Lochbihler, A: Andrei PopescuMiddlesex University, London
Media Attached
11:00 - 12:00
Message-Passing Concurrency and Substructural LogicsTutorialFest at Museum B
11:00
60m
Talk
Message-Passing Concurrency and Substructural Logics
TutorialFest
Frank PfenningCarnegie Mellon University, USA
Media Attached
11:00 - 12:00
Code ObfuscationTutorialFest at Widney
11:00
60m
Talk
Code Obfuscation - A Hacking view on program analysis and understanding.
TutorialFest
A: Roberto GiacobazziUniversity of Verona and IMDEA Software Institute
Media Attached
13:30 - 15:30
Verified ApplicationsCPP at Museum A
Chair(s): K. Rustan M. LeinoAmazon
13:30
30m
Talk
Mechanising and Verifying the WebAssembly Specification
CPP
Conrad WattUniversity of Cambridge, UK
DOI
14:00
30m
Talk
Towards Verifying Ethereum Smart Contract Bytecode in Isabelle/HOL
CPP
Sidney AmaniUNSW, Australia, Myriam BégelENS Paris-Saclay, France, Maksym Bortin, Mark StaplesCSIRO, Australia
DOI
14:30
30m
Talk
Mechanising Blockchain Consensus
CPP
George PîrleaUniversity College London, Ilya SergeyUniversity College London
DOI Pre-print
15:00
30m
Talk
Formal Microeconomic Foundations and the First Welfare Theorem
CPP
Cezary KaliszykUniversity of Innsbruck, Julian ParsertUniversity of Innsbruck, Austria
13:30 - 14:30
Opening & Invited Talk IPADL at Rose
13:30
30m
Day opening
Opening
PADL
14:00
30m
Talk
INVITED TALK: ``Safe'' Languages Require Sequential Consistency
PADL
I: Todd MillsteinUniversity of California, Los Angeles
14:00 - 15:30
Computational Higher Type TheoryTutorialFest at Bradbury
14:00
90m
Talk
Computational Higher Type Theory
TutorialFest
A: Robert HarperCarnegie Mellon University, A: Carlo AngiuliCarnegie Mellon University
Media Attached
14:00 - 15:30
Session 1-2PEPM at Crocker
Chair(s): Kenichi AsaiOchanomizu University
14:00
30m
Talk
A Guess-and-Assume Approach to Loop Fusion for Program Verification
PEPM
Akifumi ImanishiKyoto University, Kohei SuenagaGraduate School of Informatics, Kyoto University, Atsushi IgarashiKyoto University, Japan
DOI
14:30
30m
Talk
Gradually Typed Symbolic Expressions
PEPM
David BromanKTH Royal Institute of Technology, Jeremy G. SiekIndiana University, USA
DOI
15:00
30m
Talk
On the Cost of Type-Tag Soundness
PEPM
Ben GreenmanNortheastern University, Zeina MigeedUniversity of California, Los Angeles
DOI
14:00 - 15:30
Introduction to Algebraic Program analysisTutorialFest at Hershey
14:00
90m
Talk
Introduction to Algebraic Program analysis.
TutorialFest
Zachary KincaidPrinceton University, Thomas RepsUniversity of Wisconsin - Madison and GrammaTech, Inc.
Media Attached
14:00 - 15:30
Iris - A Higher-Order Concurrent Separation LogicTutorialFest at Museum B
14:00
90m
Talk
Iris - A Modular Foundation for Higher-Order Concurrent Separation Logic.
TutorialFest
Jacques-Henri JourdanCNRS, LRI, Université Paris-Sud, A: Robbert KrebbersDelft University of Technology
Media Attached
14:00 - 15:30
PotpourriVMCAI at Watercourt
Chair(s): Wei-Ngan ChinNational University of Singapore
14:00
30m
Talk
Revisiting MITL to Fix Decision Procedures
VMCAI
Nima RoohiUniversity of Pennsylvania, Mahesh ViswanathanUniversity of Illinois at Urbana-Champaign
14:30
30m
Talk
On abstraction and compositionality for weak-memory linearisability
VMCAI
Brijesh DongolBrunel University London, Radha JagadeesanDePaul University, James RielyDePaul University, Alasdair ArmstrongBrunel University
15:00
30m
Talk
Automatic Verification of RMA Programs via Abstraction Extrapolation
VMCAI
Cedric BaumannETH Zurich, Andrei Marian DanETH Zurich, Yuri MeshmanIMDEA, Torsten HoeflerETH Zurich, Martin VechevETH Zürich
14:00 - 15:30
One Weird Trick: Relational Interpreters for Program SynthesisTutorialFest at Widney
14:00
90m
Talk
One Weird Trick: Relational Interpreters for Program Synthesis.
TutorialFest
A: William E. ByrdUniversity of Alabama at Birmingham, USA, Gregory Rosenblattn.n., n.n.
Media Attached
14:30 - 15:30
Prolog and OptimizationsPADL at Rose
14:30
30m
Talk
Exploiting Term Hiding to Reduce Run-time Checking Overhead
PADL
A: Nataliia StulovaIMDEA Software Institute and T.U. of Madrid (UPM), A: José MoralesIMDEA Software Institute, A: Manuel HermenegildoIMDEA Software Institute and T.U. of Madrid (UPM)
15:00
30m
Talk
On k-colored Lambda Terms and their Skeletons
PADL
I: Paul TarauUniversity of North Texas
16:00 - 17:00
Computational Higher Type TheoryTutorialFest at Bradbury
16:00
60m
Talk
Computational Higher Type Theory
TutorialFest
A: Robert HarperCarnegie Mellon University, A: Carlo AngiuliCarnegie Mellon University
Media Attached
16:00 - 17:30
Session 1-3PEPM at Crocker
Chair(s): Frank PfenningCarnegie Mellon University, USA
16:00
60m
Talk
The Simple Essence of Automatic Differentiation (Invited Talk)
PEPM
Conal ElliottTarget, USA
Pre-print
16:00 - 17:00
Introduction to Algebraic Program analysisTutorialFest at Hershey
16:00
60m
Talk
Introduction to Algebraic Program analysis.
TutorialFest
Zachary KincaidPrinceton University, Thomas RepsUniversity of Wisconsin - Madison and GrammaTech, Inc.
Media Attached
16:00 - 18:00
Proof Methods and LibrariesCPP at Museum A
Chair(s): René ThiemannUniversity of Innsbruck
16:00
30m
Talk
Triangulating Context Lemmas
CPP
Craig McLaughlinThe University of Edinburgh, James McKinna, Ian StarkThe University of Edinburgh
DOI
16:30
30m
Talk
Adapting Proof Automation to Adapt Proofs
CPP
Talia RingerUniversity of Washington, Nathaniel YazdaniUniversity of Washington, Seattle, John LeoHalfaya Research, Dan GrossmanUniversity of Washington
DOI
17:00
30m
Talk
A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations
CPP
Niklas GrimmVienna University of Technology, Austria, Kenji MaillardInria Paris and ENS Paris, Cédric FournetMicrosoft Research, Cătălin HriţcuInria Paris, Matteo MaffeiSaarland University, Jonathan ProtzenkoMicrosoft Research, n.n., Tahina RamananandroMicrosoft Research, n.n., Aseem RastogiMicrosoft Research, Nikhil SwamyMicrosoft Research, Santiago Zanella-BéguelinMicrosoft Research, n.n.
DOI
17:30
30m
Talk
Formal Proof of Polynomial-Time Complexity with Quasi-Interpretations
CPP
Hugo FéréeUniversity of Kent, UK, Samuel HymUniversity of Lille, France, Micaela Mayero, Jean-Yves MoyenUniversity of Copenhagen, Denmark, David NowakCNRS, France
DOI
16:00 - 17:00
Iris - A Higher-Order Concurrent Separation LogicTutorialFest at Museum B
16:00
60m
Talk
Iris - A Modular Foundation for Higher-Order Concurrent Separation Logic.
TutorialFest
Jacques-Henri JourdanCNRS, LRI, Université Paris-Sud, A: Robbert KrebbersDelft University of Technology
Media Attached
16:00 - 17:30
Invited Tutorial by Mayur NaikVMCAI at Watercourt
Chair(s): Jens PalsbergUniversity of California, Los Angeles (UCLA)
16:00
90m
Talk
Maximum Satisfiability in Program Analysis: Applications and Techniques
VMCAI
Mayur NaikUniversity of Pennsylvania, Xujie SiUniversity of Pennsylvania, Xin ZhangMassachusetts Institute of Technology, USA, Radu GrigoreUniversity of Kent
16:00 - 17:00
One Weird Trick: Relational Interpreters for Program SynthesisTutorialFest at Widney
16:00
60m
Talk
One Weird Trick: Relational Interpreters for Program Synthesis.
TutorialFest
A: William E. ByrdUniversity of Alabama at Birmingham, USA, Gregory Rosenblattn.n., n.n.
Media Attached
18:00 - 22:00
VMCAI BanquetVMCAI at Watercourt
18:00
4h
Dinner
Banquet
VMCAI
18:15 - 20:15
CPP ReceptionCPP at Museum A
18:15
2h
Social Event
CPP Reception
CPP

Tue 9 Jan
Times are displayed in time zone: Tijuana, Baja California change

09:00 - 10:00
SESSION I (invited talk) PPS at Bradbury
Chair(s): Andrew D. GordonMicrosoft Research and University of Edinburgh
09:00
60m
Talk
Software is eating the world, but ML is going to eat software
PPS
09:00 - 10:00
Invited Talk by Brigitte PientkaCPP at Museum A
Chair(s): Amy FeltyUniversity of Ottawa
09:00
60m
Talk
POPLMark Reloaded: Mechanizing Logical Relations Proofs (Invited Talk)
CPP
Brigitte PientkaMcGill University
DOI
09:00 - 10:00
Invited Talk by Azadeh FarzanVMCAI at Watercourt
Chair(s): Isil DilligUT Austin
09:00
60m
Talk
Rethinking Compositionality for Concurrent Program Proofs
VMCAI
Azadeh FarzanUniversity of Toronto
10:00 - 10:30
POSTER SESSION (14 posters - not talks) PPS at Bradbury
10:00
2m
Talk
Probabilistic Programming for Robotics
PPS
Nils NappSUNY at Buffalo, Marco GaboardiUniversity at Buffalo, SUNY
10:02
2m
Talk
Game Semantics for Probabilistic Programs
PPS
C.-H. Luke OngUniversity of Oxford, Matthijs VákárUniversity of Oxford
10:04
2m
Talk
Interactive Writing and Debugging of Bayesian Probabilistic Programs
PPS
Javier Burroni, Arjun GuhaUniversity of Massachusetts, Amherst, David JensenUniversity of Massachusetts Amherst
Pre-print
10:06
2m
Talk
Deep Amortized Inference for Probabilistic Programs using Adversarial Compilation
PPS
10:08
2m
Talk
Comparing the speed of probabilistic processes
PPS
Mathias Ruggaard PedersenAalborg University, Nathanaël FijalkowAlan Turing Institute, Giorgio BacciAalborg University, Kim LarsenAalborg University, Radu MardareAalborg University
10:10
2m
Talk
Using Reinforcement Learning for Probabilistic Program Inference
PPS
Avi PfefferCharles River Analytics
10:12
2m
Talk
TensorFlow Distributions
PPS
Link to publication Pre-print
10:15
2m
Talk
Constructive probabilistic semantics with non-spatial locales
PPS
Benjamin ShermanMassachusetts Institute of Technology, USA, Jared TramontanoMassachusetts Institute of Technology, Michael CarbinMIT
Pre-print
10:17
2m
Talk
Using probabilistic programs as proposals
PPS
Marco Cusumano-TownerMIT-CSAIL, Vikash MansinghkaMassachusetts Institute of Technology
10:19
2m
Talk
Probabilistic Program Equivalence for NetKAT
PPS
Steffen SmolkaCornell University, David KahnCornell University, Praveen KumarCornell University, Nate FosterCornell University, Dexter Kozen, Alexandra SilvaUniversity College London
Link to publication File Attached
10:21
2m
Talk
Reasoning about Divergences via Span-liftings
PPS
Tetsuya SatoUniversity at Buffalo, SUNY, USA
10:23
2m
Talk
Probabilistic Models for Assured Position, Navigation and Timing
PPS
Andres Molina-MarkhamThe MITRE Corporation
10:25
2m
Talk
The Support Method of Computing Expectations
PPS
Avi PfefferCharles River Analytics
10:27
2m
Talk
Combining static and dynamic optimizations using closed-form solutions
PPS
Daniel LundénKTH Royal Institute of Technology, David BromanKTH Royal Institute of Technology, Lawrence M. MurrayUppsala University
10:30 - 12:00
SESSION II (3 talks) PPS at Bradbury
Chair(s): Erik Meijer
10:30
30m
Talk
The semantic structure of quasi-Borel spaces: algebra, logic, and recursion
PPS
Chris HeunenUniversity of Edinburgh, Ohad KammarUniversity of Oxford, Sean K. MossUniversity of Cambridge, Adam ŚcibiorUniversity of Cambridge and MPI Tuebingen, Sam StatonUniversity of Oxford, Matthijs VákárUniversity of Oxford, Hongseok YangUniversity of Oxford
11:00
30m
Talk
Stable, measurable functions and probabilistic programs
PPS
Michele PaganiUniversity Paris Diderot, Thomas EhrhardCNRS and University Paris Diderot, Christine TassonUniversity Paris Diderot
11:30
30m
Talk
Formal Methods For Probabilistic Programming
PPS
Daniel SelsamStanford University
10:30 - 12:00
Session 2-1PEPM at Crocker
Chair(s): Fritz HengleinDIKU, Denmark
10:30
60m
Talk
Challenges in the Design and Compilation of Programming Languages for Exascale Machines (Invited Talk)
PEPM
Alex AikenStanford University
11:30
30m
Talk
Checking Cryptographic API Usage with Composable Annotations (Short Paper)
PEPM
Duncan MitchellRoyal Holloway, University of London, L. Thomas van BinsbergenRoyal Holloway University of London, Blake Loring, Johannes KinderRoyal Holloway, University of London
DOI
10:30 - 12:00
Morning Session 2NetPL at Hershey
10:30
30m
Talk
Very Large Scale Network Verification
NetPL
Andrey RybalchenkoMicrosoft Research
11:00
60m
Other
Working Groups
NetPL
10:30 - 12:00
Trusted Verification Frameworks and SystemsCPP at Museum A
Chair(s): Zhong ShaoYale University
10:30
30m
Talk
A Verified SAT Solver with Watched Literals Using Imperative HOL
CPP
Mathias FleuryMPI-INF, Jasmin BlanchetteVrije Universiteit Amsterdam, Peter LammichTechnische Universität München
DOI
11:00
30m
Talk
Œuf: Minimizing the Coq Extraction TCB
CPP
Eric MullenUniversity of Washington, Stuart PernsteinerUniversity of Washington, USA, James R. WilcoxUniversity of Washington, Zachary TatlockUniversity of Washington, Seattle, Dan GrossmanUniversity of Washington
DOI
11:30
30m
Talk
Proofs in Conflict-Driven Theory Combination
CPP
Maria Paola BonacinaUniversity of Verona, Italy, Stéphane Graham-LengrandCNRS, France, Natarajan ShankarSRI International, USA
DOI
10:30 - 12:00
Panel IPLMW at Museum B
10:30
90m
Talk
Panel I: Technical Trends in Programming Languages Research
PLMW
Aws AlbarghouthiUniversity of Wisconsin-Madison, Constantin EneaUniversité Paris Diderot, David WalkerPrinceton University, Andrew C. MyersCornell University
10:30 - 12:00
Functional ProgrammingPADL at Rose
10:30
30m
Talk
Hygienic Source-Code Generation Using Functors
PADL
A: Karl CraryCarnegie Mellon University
11:00
30m
Talk
Snaarkl: Somewhat Practical, Pretty Much Declarative Verifiable Computing in Haskell
PADL
A: Gordon StewartOhio University, A: Samuel Merten, A: Logan Leland
11:30
30m
Talk
Rewriting High-Level Spreadsheet Structures into Higher-Order Functional Programs
PADL
A: Florian BiermannIT University of Copenhagen, Wensheng DouInstitute of Software, Chinese Academy of Sciences, China, A: Peter SestoftIT University of Copenhagen
13:30 - 15:30
Afternoon Session 1NetPL at Hershey
14:00
30m
Other
Working Groups Debrief
NetPL
14:30
30m
Talk
Safety Verification of Stateful Networks
NetPL
Sharon ShohamTel Aviv university
15:00
30m
Talk
Understand and verify your network using Header Space Analysis
NetPL
Peyman KazemianForward Networks
13:30 - 15:30
Type Theory, Set Theory, and Formalized MathematicsCPP at Museum A
Chair(s): Thorsten AltenkirchUniversity of Nottingham
13:30
30m
Talk
Finite Sets in Homotopy Type Theory
CPP
Dan FruminRadboud University, Herman GeuversRadboud University Nijmegen, Netherlands, Léon GondelmanLRI, Université Paris-Sud, Niels van der WeideRadboud University Nijmegen, Netherlands
DOI
14:00
30m
Talk
Generic Derivation of Induction for Impredicative Encodings in Cedille
CPP
Denis FirsovUniversity of Iowa, USA, Aaron StumpUniversity of Iowa, USA
DOI
14:30
30m
Talk
Large Model Constructions for Second-Order ZF in Dependent Type Theory
CPP
Dominik KirstSaarland University, Gert SmolkaSaarland University
DOI
15:00
30m
Talk
A Constructive Formalisation of Semi-algebraic Sets and Functions
CPP
14:00 - 15:30
SESSION III (invited tutorial + 1 talk) PPS at Bradbury
Chair(s): Cameron FreerRemine and Borelian
14:00
60m
Talk
Deep Probabilistic Programming: TensorFlow Distributions and Edward
PPS
15:00
30m
Talk
More support for symbolic disintegration
PPS
Praveen NarayananIndiana University, USA, Chung-chieh ShanIndiana University, USA
14:00 - 15:30
Session 2-2PEPM at Crocker
Chair(s): Kohei SuenagaGraduate School of Informatics, Kyoto University
14:00
30m
Talk
Partially Static Data as Free Extension of Algebras (Short Paper)
PEPM
Jeremy YallopUniversity of Cambridge, UK, Tamara von GlehnUniversity of Cambridge, Ohad KammarUniversity of Oxford
Pre-print
14:30
30m
Talk
Program Generation for ML Modules (Short Paper)
PEPM
Takahisa WatanabeUniversity of Tsukuba, Japan, Yukiyoshi KameyamaUniversity of Tsukuba, Japan
DOI
15:00
30m
Talk
Recursive Programs in Normal Form (Short Paper)
PEPM
Barry JayUniversity of Technology Sydney
DOI
14:00 - 15:30
Types and AnalysisVMCAI at Watercourt
Chair(s): Tachio TerauchiWaseda University
14:00
30m
Talk
From Shapes to Amortized Complexity
VMCAI
Tomas FiedorVUT Brno, Lukáš HolíkBrno University of Technology, Adam RogalewiczBrno University of Technology , Moritz SinnSt. Polten University of Applied Sciences, Tomáš VojnarBrno University of Technology, Florian ZulegerTU Vienna
14:30
30m
Talk
Invariant Generation for Multi-Path Loops with Polynomial Assignments
VMCAI
Andreas HumenbergerVienna University of Technology, Maximilian JaroschekVienna University of Technology, Laura KovacsChalmers University of Technology
15:00
30m
Talk
Refinement Types for Ruby
VMCAI
Milod Kazerounian, Niki VazouUniversity of Maryland, Austin BourgerieUniversity of Maryland, Jeffrey S. FosterUniversity of Maryland, College Park, Emina TorlakUniversity of Washington
16:00 - 18:00
SESSION IV (4 talks) PPS at Bradbury
Chair(s): Rif A. SaurousGoogle
16:00
30m
Talk
Auxiliary variables in Probabilistic Programs
PPS
16:30
30m
Talk
Probabilistic Program Inference With Abstractions
PPS
Steven HoltzenUniversity of California, Los Angeles, Guy Van den BroeckUniversity of California, Los Angeles, Todd MillsteinUniversity of California, Los Angeles
Pre-print
17:00
30m
Talk
SlicStan: Improving Probabilistic Programming using Information Flow Analysis
PPS
Maria I. GorinovaThe University of Edinburgh, Andrew D. GordonMicrosoft Research and University of Edinburgh, Charles SuttonUniversity of Edinburgh
Pre-print
17:30
30m
Talk
Contextual Equivalence for a Probabilistic Language with Continuous Random Variables and Recursion
PPS
Mitchell WandNortheastern University, USA, Theophilos GiannakopoulosBAE Systems, Inc., Andrew CobbNortheastern University, Ryan CulpepperNortheastern University
16:00 - 17:30
Session 2-3PEPM at Crocker
Chair(s): Barry JayUniversity of Technology Sydney
16:00
10m
Talk
Towards Language-independent Code Synthesis (Poster/Demo Talk)
PEPM
Jan BessaiTechnical University Dortmund, Boris DüdderUniversity of Copenhagen, George HeinemanWorcester Polytechnic Institute, Jakob RehofTechnical University Dortmund
File Attached
16:10
10m
Talk
Dataflow Metaprogramming (Poster/Demo Talk)
PEPM
Dominic Duggan, Jianhua YaoStevens Institute of Technology
16:20
10m
Talk
An Approach to Generating Text-Based IDEs with Syntax Completion (Poster/Demo Talk)
PEPM
Isao SasanoShibaura Institute of Technology
16:30
10m
Talk
Modular Macros (Poster/Demo Talk)
PEPM
Olivier Nicole, Leo WhiteJane Street, Jeremy YallopUniversity of Cambridge, UK
File Attached
16:40
10m
Talk
Equations: From Clauses to Splittings to Functions (Poster/Demo Talk)
PEPM
File Attached
16:50
40m
Other
Posters/Demos
PEPM
16:00 - 18:00
Afternoon Session 2NetPL at Hershey
16:00
30m
Talk
P4: A Language for Data Plane Programming
NetPL
Calin CascavalBarefoot Networks
16:30
30m
Talk
A Vision for Network Design Automation
NetPL
17:00
30m
Other
Panel
NetPL
Nate FosterCornell University, David WalkerPrinceton University, Barath RaghavanICSI, Jonathan SmithDARPA
17:30
30m
Day closing
Wrap Up
NetPL
Marco CaniniKAUST, Nate FosterCornell University, Todd MillsteinUniversity of California, Los Angeles
16:00 - 18:00
Formalizing Meta-TheoryCPP at Museum A
Chair(s): Brigitte PientkaMcGill University
16:00
30m
Talk
HOpi in Coq
CPP
Sergueï LengletUniversity of Lorraine, France, Alan SchmittInria
DOI
16:30
30m
Talk
A Coq Formalization of Normalization by Evaluation for Martin-Löf Type Theory
CPP
Paweł WieczorekUniversity of Wrocław, Dariusz BiernackiUniversity of Wrocław
DOI
17:00
30m
Talk
A Two-Level Logic Perspective on (Simultaneous) Substitutions
CPP
Kaustuv ChaudhuriInria, France
DOI
17:30
30m
Talk
Binder Aware Recursion over Well-Scoped de Bruijn Syntax
CPP
Jonas Kaiser, Steven Schäfer, Kathrin StarkSaarland University, Germany
DOI
16:00 - 18:00
Panel IIPLMW at Museum B
16:00
30m
Talk
Work-Life Balance?
PLMW
Andrew C. MyersCornell University
File Attached
16:30
90m
Talk
Panel II: Life in Grad School (and Beyond)
PLMW
Azadeh FarzanUniversity of Toronto, Zachary TatlockUniversity of Washington, Seattle, Thomas BallMicrosoft Research, Jennifer PaykinUniversity of Pennsylvania
16:00 - 18:00
Best Papers PADL at Rose
16:00
30m
Talk
Probabilistic Functional Logic Programming
PADL
A: Sandra DylusUniversity of Kiel, Germany, A: Jan ChristiansenFlensburg University of Applied Sciences, Germany, A: Finn TeegenUniversity of Kiel, Germany
16:30
30m
Talk
Optimizing Answer Set Computation via Heuristic-Based Decomposition
PADL
A: Francesco CalimeriUniversity of Calabria, A: Davide Fuscà, A: Simona Perri, A: Jessica Zangari
17:00
30m
Day closing
Closing
PADL
16:00 - 17:30
Model CheckingVMCAI at Watercourt
Chair(s): Kenneth L. McMillanMicrosoft Research
16:00
30m
Talk
Learning to Complement Büchi Automata
VMCAI
Yong LiInstitute of Software, Chinese Academy of Sciences, Andrea TurriniState Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Lijun ZhangInstitute of Software, Chinese Academy of Sciences, Sven ScheweUniversity of Liverpool
16:30
30m
Talk
Selfless Interpolation for Infinite-State Model Checking
VMCAI
Tanja SchindlerUniversity of Freiburg, Dejan JovanovićSRI International
17:00
30m
Talk
Parameterized Model Checking of Synchronous Distributed Algorithms by Abstraction
VMCAI
Benjamin AminofVienna University of Technology, Sasha RubinUniversity of Naples Federico II, Ilina StoilkovskaVienna University of Technology , Josef WidderTU Wien, Florian ZulegerTU Vienna

Wed 10 Jan
Times are displayed in time zone: Tijuana, Baja California change

08:30 - 10:00
Awards & Keynote-IResearch Papers at Bunker Hill / Watercourt
Chair(s): Ranjit JhalaUniversity of California, San Diego
08:30
5m
Day opening
Welcome to POPL 2018
Research Papers
G: Ranjit JhalaUniversity of California, San Diego, P: Andrew C. MyersCornell University
08:35
10m
Awards
SIGPLAN Awards
Research Papers
Satnam SinghX, the moonshot factory
08:45
60m
Talk
Milner Award Lecture: The Type Soundness Theorem That You Really Want to Prove (and Now You Can)
Research Papers
09:45
20m
Talk
Lightning Overview - Day 1
Research Papers
10:30 - 12:10
StringsResearch Papers at Bunker Hill
Chair(s): Zachary TatlockUniversity of Washington, Seattle
10:30
25m
Talk
Synthesizing Bijective Lenses
Research Papers
Anders MiltnerPrinceton University, Kathleen FisherTufts University, Benjamin C. PierceUniversity of Pennsylvania, David WalkerPrinceton University, Steve ZdancewicUniversity of Pennsylvania
10:55
25m
Talk
WebRelate: Integrating Web Data with Spreadsheets using Examples
Research Papers
Jeevana Priya InalaMIT, Rishabh SinghMicrosoft Research
11:20
25m
Talk
What's Decidable About String Constraints with ReplaceAll Function?
Research Papers
Taolue ChenBirkbeck, University of London, Yan ChenState Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences & University of Chinese Academy of Sciences, Matthew HagueRoyal Holloway, University of London, Anthony Widjaja LinOxford University, Zhilin WuState Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences
11:45
25m
Talk
String Constraints with Concatenation and Transducers Solved Efficiently
Research Papers
Lukáš HolíkBrno University of Technology, Anthony Widjaja LinOxford University, Petr JankůBrno University of Technology, Philipp RuemmerUppsala University, Tomáš VojnarBrno University of Technology
10:30 - 12:10
Types and EffectsResearch Papers at Watercourt
Chair(s): Neel KrishnaswamiComputer Laboratory, University of Cambridge
10:30
25m
Talk
Linear Haskell: practical linearity in a higher-order polymorphic language
Research Papers
Jean-Philippe BernardyUniversity of Gothenburg, Mathieu BoespflugTweag I/O, Ryan R. NewtonIndiana University, Simon Peyton JonesMicrosoft Research, Arnaud SpiwackTweag I/O
Pre-print File Attached
10:55
25m
Talk
Polyadic Approximations, Fibrations and Intersection Types
Research Papers
11:20
25m
Talk
Handling fibred algebraic effects
Research Papers
Danel AhmanInria Paris
11:45
25m
Talk
Handle with Care: Relational Interpretation of Algebraic Effects and Handlers
Research Papers
Dariusz BiernackiUniversity of Wrocław, Maciej PirógUniversity of Wrocław, Piotr PolesiukUniversity of Wrocław, Filip SieczkowskiUniversity of Wrocław
12:10 - 13:40
Wednesday LunchResearch Papers at Lunch Room
12:10
90m
Lunch
Wednesday Lunch
Research Papers
13:40 - 15:20
Verification IResearch Papers at Bunker Hill
Chair(s): Zhong ShaoYale University
13:40
25m
Talk
Automated Lemma Synthesis in Symbolic-Heap Separation Logic
Research Papers
Quang-Trung TaNational University of Singapore, Ton Chanh LeNational University of Singapore, Siau-Cheng KhooNational University of Singapore, Wei-Ngan ChinNational University of Singapore
14:05
25m
Talk
Foundations for Natural Proofs and Quantifier Instantiation
Research Papers
Christof LödingRWTH Aachen University, P. MadhusudanUniversity of Illinois at Urbana-Champaign, Lucas PeñaUniversity of Illinois at Urbana-Champaign
14:30
25m
Talk
Higher-Order Constrained Horn Clauses for Verification
Research Papers
Toby Cathcart BurnUniversity of Oxford, C.-H. Luke OngUniversity of Oxford, Steven RamsayUniversity of Bristol
14:55
25m
Talk
Relatively Complete Refinement Type System for Verification of Higher-Order Non-Deterministic Programs
Research Papers
Hiroshi UnnoUniversity of Tsukuba, Yuki SatakeUniversity of Tsukuba, Tachio TerauchiWaseda University
13:40 - 15:20
Interpretation and EvaluationResearch Papers at Watercourt
Chair(s): Atsushi IgarashiKyoto University, Japan
13:40
25m
Talk
Unifying Analytic and Statically-Typed Quasiquotes
Research Papers
Lionel ParreauxEPFL, Antoine VoizardUniversity of Pennsylvannia, Amir ShaikhhaEPFL, Christoph E. KochEPFL
Pre-print
14:05
25m
Talk
Jones-Optimal Partial Evaluation by Specialization-Safe Normalization
Research Papers
Matt BrownUCLA, Jens PalsbergUniversity of California, Los Angeles (UCLA)
14:30
25m
Talk
Migrating Gradual Types
Research Papers
John Peter CamporaULL Lafayette, Sheng ChenUniversity of Louisiana at Lafayette, Martin ErwigOregon State University, Eric WalkingshawOregon State University
14:55
25m
Talk
Intrinsically-Typed Definitional Interpreters for Imperative Languages
Research Papers
Casper Bach PoulsenDelft University of Technology, Arjen RouvoetDelft University of Technology, Andrew TolmachPortland State University, Robbert KrebbersDelft University of Technology, Eelco VisserDelft University of Technology
DOI Pre-print
15:50 - 17:30
Memory and ConcurrencyResearch Papers at Bunker Hill
Chair(s): Azadeh FarzanUniversity of Toronto
15:50
25m
Talk
Effective Stateless Model Checking for C/C++ Concurrency
Research Papers
Michalis KokologiannakisNational Technical University of Athens, Greece, Ori LahavTel Aviv University, Israel, Konstantinos (Kostis) Sagonas, Viktor VafeiadisMPI-SWS, Germany
16:15
25m
Talk
Transactions in Relaxed Memory Architectures
Research Papers
Brijesh DongolBrunel University London, Radha JagadeesanDePaul University, James RielyDePaul University
Link to publication DOI Pre-print Media Attached
16:40
25m
Talk
Simplifying ARM Concurrency: Multicopy-Atomic Axiomatic and Operational Models for ARMv8
Research Papers
Christopher PulteUniversity of Cambridge, Shaked FlurUniversity of Cambridge, Will DeaconARM Ltd., Jon FrenchUniversity of Cambridge, Susmit SarkarUniversity of St. Andrews, Peter SewellUniversity of Cambridge
17:05
25m
Talk
Progress of Concurrent Objects with Partial Methods
Research Papers
Hongjin LiangUniversity of Science and Technology of China, Xinyu FengUniversity of Science and Technology of China
15:50 - 17:30
TypesResearch Papers at Watercourt
Chair(s): Thorsten AltenkirchUniversity of Nottingham
15:50
25m
Talk
A Principled approach to Ornamentation in ML
Research Papers
16:15
25m
Talk
Type-Preserving CPS Translation of Σ and Π Types is Not Not Possible
Research Papers
William J. BowmanNortheastern University, USA, Youyou CongOchanomizu University, Japan, Nick RiouxNortheastern University, USA, Amal AhmedNortheastern University, USA
Link to publication DOI Pre-print
16:40
25m
Talk
Safety and Conservativity of Definitions in HOL and Isabelle/HOL
Research Papers
Ondřej KunčarTechnische Universität München, Germany, Andrei PopescuMiddlesex University, London
17:05
25m
Talk
Univalent Higher Categories via Complete Semi-Segal Types
Research Papers
Paolo CapriottiUniversity of Nottingham, Nicolai KrausUniversity of Nottingham
19:00 - 22:00
POPL BanquetResearch Papers at MOCA
19:00
3h
Dinner
POPL Banquet
Research Papers

Thu 11 Jan
Times are displayed in time zone: Tijuana, Baja California change

08:30 - 10:00
Keynote-IIResearch Papers at Bunker Hill / Watercourt
Chair(s): Andrew C. MyersCornell University
08:30
60m
Talk
Some Principles of Differential Programming Languages
Research Papers
Gordon PlotkinUniversity of Edinburgh, UK
09:30
30m
Talk
Lightning Overview - Day 2
Research Papers
10:30 - 12:10
ConsistencyResearch Papers at Bunker Hill
Chair(s): Xinyu FengUniversity of Science and Technology of China
10:30
25m
Talk
Sound, Complete, and Tractable Linearizability Monitoring for Concurrent Collections
Research Papers
Michael EmmiNokia Bell Labs, Constantin EneaUniversité Paris Diderot
10:55
25m
Talk
Reducing Liveness to Safety in First-Order Logic
Research Papers
Oded PadonTel Aviv University, Jochen HoenickeUniversität Freiburg, Giuliano LosaUniversity of California at Los Angeles, USA, Andreas PodelskiUniversity of Freiburg, Germany, Mooly SagivTel Aviv University, Sharon ShohamTel Aviv university
11:20
25m
Talk
Alone Together: Compositional Reasoning and Inference for Weak Isolation
Research Papers
Gowtham KakiPurdue University, Kartik NagarPurdue University, Mahsa NajafzadehPurdue University, Suresh JagannathanPurdue University
11:45
25m
Talk
Programming and Proving with Distributed Protocols
Research Papers
Ilya SergeyUniversity College London, James R. WilcoxUniversity of Washington, Zachary TatlockUniversity of Washington, Seattle
DOI Pre-print
10:30 - 12:10
Program Analysis IResearch Papers at Watercourt
Chair(s): Tachio TerauchiWaseda University
10:30
25m
Talk
Inference of Static Semantics for Incomplete C Programs
Research Papers
Pre-print
10:55
25m
Talk
Optimal Dyck Reachability for Data-dependence and Alias Analysis
Research Papers
11:20
25m
Talk
Data-centric Dynamic Partial Order Reduction
Research Papers
Marek ChalupaMasaryk University, Krishnendu ChatterjeeIST Austria, Andreas PavlogiannisIST Austria, Kapil VaidyaIIT Bombay, Nishant SinhaIBM Research
11:45
25m
Talk
Analytical Modeling of Cache Behavior for Affine Programs
Research Papers
Wenlei BaoOhio State University, Sriram KrishnamoorthyPacific Northwest National Laboratories, Louis-Noël PouchetColorado State University, P. SadayappanOhio State University
12:10 - 13:40
Thursday LunchResearch Papers at Lunch Room
12:10
90m
Lunch
Thursday Lunch
Research Papers
13:40 - 15:20
TerminationResearch Papers at Bunker Hill
Chair(s): Constantin EneaUniversité Paris Diderot
13:40
25m
Talk
A new proof rule for almost-sure termination
Research Papers
Annabelle McIverMacquarie University, Carroll MorganUniversity of New South Wales; Data 61, Benjamin Lucien KaminskiRWTH Aachen University; University College London, Joost-Pieter KatoenRWTH Aachen University
14:05
25m
Talk
Lexicographic Ranking Supermartingales: An Efficient Approach to Termination of Probabilistic Programs
Research Papers
Sheshansh AgrawalIIT Bombay, Krishnendu ChatterjeeIST Austria, Petr NovotnyIST Austria
14:30
25m
Talk
Algorithmic Analysis of Termination Problems for Quantum Programs
Research Papers
Yangjia LiInstitute of Software, Chinese Academy of Sciences, Mingsheng YingUniversity of Technology Sydney
14:55
25m
Talk
Monadic refinements for relational cost analysis
Research Papers
Ivan RadicekTU Vienna, Gilles BartheIMDEA Software Institute, Marco GaboardiUniversity at Buffalo, SUNY, Deepak GargMax Planck Institute for Software Systems, Florian ZulegerTU Vienna
13:40 - 15:20
Outside the boxResearch Papers at Watercourt
Chair(s): Lars BirkedalAarhus University
13:40
25m
Talk
Go with the Flow: Compositional Abstractions for Concurrent Data Structures
Research Papers
Siddharth KrishnaNew York University, Dennis ShashaNew York University, Thomas WiesNew York University
14:05
25m
Talk
Parametricity versus the Universal Type
Research Papers
Dominique DevrieseKU Leuven, Marco PatrignaniSaarland University, CISPA, Frank PiessensKU Leuven
14:30
25m
Talk
Linearity in Higher-Order Recursion Schemes
Research Papers
Pierre ClairambaultCNRS & ENS Lyon, Charles GrelloisINRIA Sophia Antipolis & Aix-Marseille Université, Andrzej MurawskiUniversity of Oxford
14:55
25m
Talk
Symbolic Types for Lenient Symbolic Execution
Research Papers
Stephen ChangNortheastern University, Alex KnauthNortheastern University, Emina TorlakUniversity of Washington
15:50 - 16:40
Language DesignResearch Papers at Bunker Hill
Chair(s): Zachary TatlockUniversity of Washington, Seattle
15:50
25m
Talk
An Axiomatic Basis for Bidirectional Programming
Research Papers
Hsiang-Shang ‘Josh’ KoNational Institute of Informatics, Japan, Zhenjiang HuNational Institute of Informatics
Link to publication DOI Pre-print Media Attached File Attached
16:15
25m
Talk
Simplicitly: Foundations and Applications of Implicit Function Types
Research Papers
Martin OderskyEPFL, Switzerland, Olivier BlanvillainEPFL, Fengyun LiuEPFL, Switzerland, Aggelos BiboudisEcole Polytechnique Federale de Lausanne, Heather MillerEcole Polytechnique Federale de Lausanne, Sandro StuckiEPFL
15:50 - 16:40
Dependent TypesResearch Papers at Watercourt
Chair(s): Karl CraryCarnegie Mellon University
15:50
25m
Talk
Up-to Techniques Using Sized Types
Research Papers
Nils Anders DanielssonUniversity of Gothenburg, Chalmers University of Technology
16:15
25m
Talk
Decidability of Conversion for Type Theory in Type Theory
Research Papers
Andreas AbelGothenburg University, Joakim ÖhmanIMDEA Software Institute, Andrea VezzosiChalmers University of Technology
17:00 - 18:00
Business MeetingResearch Papers at Bunker Hill / Watercourt
Chair(s): Andrew C. MyersCornell University, Ranjit JhalaUniversity of California, San Diego
17:00
20m
Talk
Chairs' Report
Research Papers
P: Andrew C. MyersCornell University, G: Ranjit JhalaUniversity of California, San Diego
17:20
10m
Talk
POPL 2019 Preview
Research Papers
G: Fritz HengleinDIKU, Denmark, P: Stephanie WeirichUniversity of Pennsylvania, USA
17:30
30m
Talk
SIGPLAN Town Hall
Research Papers
Michael HicksUniversity of Maryland, College Park, Benjamin C. PierceUniversity of Pennsylvania
18:15 - 20:15
POPL Poster SessionResearch Papers at SRC
18:15
2h
Other
POPL Poster Session
Research Papers
18:30 - 20:30
18:30
7m
Talk
A Decidable Logic for Tree Data-Structures with Measurements
Student Research Competition
18:37
7m
Talk
Combining Control Operators and Dependent Types
Student Research Competition
Youyou CongOchanomizu University, Japan
18:44
7m
Talk
Comparing Liquid Haskell and Coq: Evaluating the Great Expectations of “A Tale of Two Provers”
Student Research Competition
18:51
7m
Talk
Comparison among three program verification techniques in Dependent Haskell, Liquid Haskell and F*
Student Research Competition
Xinyue ZhangBryn Mawr College, USA, Rachel Xu
18:58
7m
Talk
Finite Maps At The Type Level
Student Research Competition
Divesh OtwaniHaverford College
19:05
7m
Talk
Formal Models Underlying Blockchain Technology
Student Research Competition
Haochen XieNagoya University
19:12
7m
Talk
Generating Information-Flow Control Mechanisms from Programming Language Specifications
Student Research Competition
Andrew BedfordLaval University
19:19
7m
Talk
How to Make Your Programs Very Safe: A Review of Practical Applications of Dependent Types
Student Research Competition
19:26
7m
Talk
Modelling Microcontroller Hardware using Typestate
Student Research Competition
Rudi HornUniversity of Edinburgh
19:33
7m
Talk
Program Synthesis with Neural Oracles
Student Research Competition
19:40
7m
Talk
Propositional Dynamic Logic for Higher-Order Functional Programs
Student Research Competition
Yuki SatakeUniversity of Tsukuba
19:47
7m
Talk
Relational Cost Analysis with State
Student Research Competition
Weihao QuUniversity at Buffalo, SUNY
19:54
7m
Talk
Robust Example-based Synthesis
Student Research Competition
20:01
7m
Talk
Simplifying incremental code with IODyn
Student Research Competition
Kyle HeadleyUniversity of Colorado Boulder
20:08
7m
Talk
Software Fault Isolation for Robust Compilation
Student Research Competition
Ana Nora EvansUniversity of Virginia, USA
20:15
7m
Talk
Synchronous Proofs for Asynchronous Programs
Student Research Competition
Bernhard KraglIST Austria
20:22
7m
Talk
Type-Driven Gradual Security with References
Student Research Competition
Matías ToroUniversity of Chile

Fri 12 Jan
Times are displayed in time zone: Tijuana, Baja California change

08:30 - 10:00
Keynote-IIIResearch Papers at Bunker Hill / Watercourt
Chair(s): Andrew C. MyersCornell University
08:30
60m
Talk
Formal Methods and the Law
Research Papers
S: Sarah LawskyNorthwestern University
09:30
30m
Talk
Lightning Overview - Day 3
Research Papers
10:30 - 12:10
Testing and VerificationResearch Papers at Bunker Hill
Chair(s): Santosh NagarakatteRutgers University, USA
10:30
25m
Talk
Generating Good Generators for Inductive Relations
Research Papers
Leonidas LampropoulosUniversity of Pennsylvania, Zoe ParaskevopoulouPrinceton University, Benjamin C. PierceUniversity of Pennsylvania
10:55
25m
Talk
Why is Random Testing Effective for Partition Tolerance Bugs?
Research Papers
11:20
25m
Talk
On Automatically Proving the Correctness of math.h Implementations
Research Papers
Wonyeol LeeStanford University, Rahul SharmaMicrosoft Research, Alex AikenStanford University
11:45
25m
Talk
Online Detection of Effectively Callback Free Objects with Applications to Smart Contracts
Research Papers
Shelly GrossmanTel Aviv University, Ittai AbrahamVMWare Research, Guy Golan-GuetaVMWare Research, Yan MichalevskyStanford University, Noam RinetzkyTel Aviv University, Mooly SagivTel Aviv University, Yoni ZoharTel Aviv University
10:30 - 12:00
Finalist PresentationsStudent Research Competition at SRC
10:30
15m
Talk
Graduate Finalist 1
Student Research Competition
10:45
15m
Talk
Graduate Finalist 2
Student Research Competition
11:00
15m
Talk
Graduate Finalist 3
Student Research Competition
11:15
15m
Talk
Undergraduate Finalist 1
Student Research Competition
11:30
15m
Talk
Undergraduate Finalist 2
Student Research Competition
11:45
15m
Talk
Undergraduate Finalist 3
Student Research Competition
10:30 - 12:10
Dynamic LanguagesResearch Papers at Watercourt
Chair(s): Jean YangCarnegie Mellon University
10:30
25m
Talk
Correctness of Speculative Optimizations with Dynamic Deoptimization
Research Papers
Olivier FlückigerNortheastern University, USA, Gabriel SchererNortheastern University, USA, Ming-Ho YeeNortheastern University, USA, Aviral GoelNortheastern University, Amal AhmedNortheastern University, USA, Jan VitekNortheastern University
DOI Pre-print
10:55
25m
Talk
JaVerT: JavaScript Verification Toolchain
Research Papers
José Fragoso SantosImperial College London, Petar MaksimovićImperial College London, Daiva NaudžiūnienėImperial College London, Thomas WoodImperial College London, Philippa GardnerImperial College London
11:20
25m
Talk
Soft Contract Verification for Higher-order Stateful Programs
Research Papers
Phúc C. NguyễnUniversity of Maryland, Thomas GilrayUniversity of Maryland, Sam Tobin-HochstadtIndiana University, David Van HornUniversity of Maryland
11:45
25m
Talk
Collapsing Towers of Interpreters
Research Papers
Nada AminUniversity of Cambridge, Tiark RompfPurdue University
12:10 - 13:30
12:10
80m
Lunch
Friday Lunch
Research Papers
13:30 - 15:20
Program Analysis IIResearch Papers at Bunker Hill
Chair(s): Isil DilligUT Austin
13:30
10m
Awards
SRC Awards
Research Papers
Benjamin DelawarePurdue University
13:30
22m
Talk
Refinement Reflection: Complete Verification with SMT
Research Papers
Niki VazouUniversity of Maryland, Anish TondwalkarUCSD, Vikraman Choudhury, Ryan ScottIndiana University, Ryan R. NewtonIndiana University, Philip WadlerUniversity of Edinburgh, UK, Ranjit JhalaUniversity of California, San Diego
14:05
25m
Talk
Non-Linear Reasoning For Invariant Synthesis
Research Papers
Zachary KincaidPrinceton University, John CyphertUniversity of Wisconsin - Madison, Jason BreckUniversity of Wisconsin - Madison, Thomas RepsUniversity of Wisconsin - Madison and GrammaTech, Inc.
14:30
25m
Talk
A Practical Construction for Decomposing Numerical Abstract Domains
Research Papers
14:55
25m
Talk
Verifying Equivalence of Database-Driven Applications
Research Papers
Yuepeng WangUniversity of Texas at Austin, Isil DilligUT Austin, Shuvendu LahiriMicrosoft Research, William CookUniversity of Texas at Austin
13:40 - 15:20
ProbabilityResearch Papers at Watercourt
Chair(s): Lars BirkedalAarhus University
13:40
25m
Talk
Proving expected sensitivity of probabilistic programs
Research Papers
Gilles BartheIMDEA Software Institute, Thomas EspitauUniversite Pierre et Marie Curie, Benjamin GregoireINRIA, Justin HsuUniversity College London, Pierre-Yves StrubEcole Polytechnique
14:05
25m
Talk
Synthesizing Coupling Proofs of Differential Privacy
Research Papers
Aws AlbarghouthiUniversity of Wisconsin-Madison, Justin HsuUniversity College London
14:30
25m
Talk
Measurable cones and stable, measurable functions
Research Papers
Thomas EhrhardCNRS and University Paris Diderot, Michele PaganiUniversity Paris Diderot, Christine TassonUniversity Paris Diderot
14:55
25m
Talk
Denotational validation of higher-order Bayesian inference
Research Papers
Adam ŚcibiorUniversity of Cambridge and MPI Tuebingen, Ohad KammarUniversity of Oxford, Matthijs VákárUniversity of Oxford, Sam StatonUniversity of Oxford, Hongseok YangUniversity of Oxford, Yufei CaiUniversity of Tuebingen, Klaus OstermannUniversity of Tuebingen, Sean K. MossUniversity of Cambridge, Chris HeunenUniversity of Edinburgh, Zoubin GhahramaniUniversity of Cambridge
15:50 - 17:05
SynthesisResearch Papers at Bunker Hill
Chair(s): Nadia PolikarpovaUniversity of California, San Diego
15:50
25m
Talk
Strategy Synthesis for Linear Arithmetic Games
Research Papers
Azadeh FarzanUniversity of Toronto, Zachary KincaidPrinceton University
16:15
25m
Talk
Bonsai: Synthesis-Based Reasoning for Type Systems
Research Papers
Kartik ChandraStanford University, Rastislav BodikUniversity of Washington
16:40
25m
Talk
Program Synthesis using Abstraction Refinement
Research Papers
Xinyu WangUT Austin, Isil DilligUT Austin, Rishabh SinghMicrosoft Research
15:50 - 17:05
Types for StateResearch Papers at Watercourt
Chair(s): Neel KrishnaswamiComputer Laboratory, University of Cambridge
15:50
25m
Talk
A Logical Relation for Monadic Encapsulation of State: Proving contextual equivalences in the presence of runST
Research Papers
Amin Timanyimec-Distrinet KU-Leuven, Leo StefanescoENS Lyon, Morten Krogh-JespersenAarhus University, Lars BirkedalAarhus University
16:15
25m
Talk
Recalling a Witness: Foundations and Applications of Monotonic State
Research Papers
Danel AhmanInria Paris, Cédric FournetMicrosoft Research, Cătălin HriţcuInria Paris, Kenji MaillardInria Paris and ENS Paris, Aseem RastogiMicrosoft Research, Nikhil SwamyMicrosoft Research
Pre-print
16:40
25m
Talk
RustBelt: Securing the Foundations of the Rust Programming Language
Research Papers
Ralf JungMPI-SWS, Jacques-Henri JourdanCNRS, LRI, Université Paris-Sud, Robbert KrebbersDelft University of Technology, Derek DreyerMPI-SWS

Sat 13 Jan
Times are displayed in time zone: Tijuana, Baja California change

09:00 - 10:00
Welcome and Invited TalkPriSC at Hershey
Chair(s): Cătălin HriţcuInria Paris
09:00
10m
Talk
PriSC Welcome
PriSC
File Attached
09:10
50m
Talk
Challenges For Compiler-backed Security: From Sanitizer to Mitigation (Invited Talk)
PriSC
Mathias PayerPurdue University
File Attached
09:00 - 10:00
KeynoteCoqPL at Watercourt A
Chair(s): Yves BertotINRIA
09:00
60m
Talk
CoqHammer: Strong Automation for Program Verification
CoqPL
Lukasz CzajkaUniversity of Innsbruck, Cezary KaliszykUniversity of Innsbruck
File Attached
10:30 - 12:00
10:30
30m
Talk
Synthesizing Program-Specific Static Analyses
Off the Beaten Track
Colin GordonDrexel University
File Attached
11:00
30m
Talk
On quantifying the degree of unsoundness of static analyses
Off the Beaten Track
File Attached
11:30
30m
Talk
Explaining Type Errors
Off the Beaten Track
Brent YorgeyHendrix College, Richard A. EisenbergBryn Mawr College, USA, Harley D. Eades IIIAugusta University
File Attached
10:30 - 12:10
Tactics and Proof EngineeringCoqPL at Watercourt A
Chair(s): Benjamin DelawarePurdue University
10:30
25m
Talk
A “destruct” Tactic for Mtac2
CoqPL
Jan-Oliver KaiserMPI-SWS, Beta ZilianiFAMAF, UNC and CONICET
File Attached
10:55
25m
Talk
Typed Template Coq
CoqPL
Simon Boulier, Matthieu SozeauInria, Nicolas TabareauInria, France, Abhishek AnandCornell University
File Attached
11:20
25m
Talk
Elpi: an extension language for Coq
CoqPL
File Attached
11:45
25m
Talk
Coqatoo: Generating Natural Language Versions of Coq Proofs
CoqPL
Andrew BedfordLaval University
File Attached
13:30 - 15:30
Session 2Off the Beaten Track at Crocker
Chair(s): William E. ByrdUniversity of Alabama at Birmingham, USA
13:30
30m
Lunch
Lunch (12pm-2pm)
Off the Beaten Track
14:00
30m
Talk
SweetPea: A Language for Designing Experiments
Off the Beaten Track
Annie CherkaevUniversity of Utah, Sebastian MusslickPrinceton University, Jonathan CohenPrinceton University, Vivek SrikumarUniversity of Utah, Matthew FlattUniversity of Utah
File Attached
14:30
30m
Talk
Extensible Semantics for Fluidics
Off the Beaten Track
Max WillseyUniversity of Washington, Jared RoeschUniversity of Washington, USA
File Attached
15:00
30m
Talk
Towards Proof Synthesis by Neural Machine Translation
Off the Beaten Track
Taro SekiyamaIBM Research, Japan, Akifumi ImanishiKyoto University, Kohei SuenagaGraduate School of Informatics, Kyoto University
File Attached
13:30 - 15:30
Session 2PriSC at Hershey
Chair(s): David NaumannStevens Institute of Technology
13:30
30m
Talk
Building Secure SGX Enclaves using F*, C/C++ and X64
PriSC
File Attached
14:00
30m
Talk
Robust Hyperproperty Preservation for Secure Compilation
PriSC
Deepak GargMax Planck Institute for Software Systems, Cătălin HriţcuInria Paris, Marco PatrignaniSaarland University, CISPA, Marco Stronati, David SwaseyMPI-SWS
Pre-print File Attached
14:30
30m
Talk
Formally Secure Compilation of Unsafe Low-Level Components
PriSC
Guglielmo FachiniInria Paris, Cătălin HriţcuInria Paris, Marco Stronati, Ana Nora EvansUniversity of Virginia, USA, Théo Laurent, Arthur Azevedo de AmorimCarnegie Mellon University, USA, Benjamin C. PierceUniversity of Pennsylvania, Andrew TolmachPortland State University
Pre-print File Attached
15:00
30m
Talk
Secure Compilation in a Production Environment
PriSC
File Attached
14:00 - 14:50
PL MetatheoryCoqPL at Watercourt A
Chair(s): Steve ZdancewicUniversity of Pennsylvania
14:00
25m
Talk
Locally Nameless at Scale
CoqPL
Stephanie WeirichUniversity of Pennsylvania, USA, Antoine VoizardUniversity of Pennsylvannia, Anastasiya Kravchuk-Kirilyuk University of Pennsylvania
File Attached
14:25
25m
Talk
A Coq Formalisation of a Core of R
CoqPL
File Attached
14:50 - 15:30
Coq developers talk & panelCoqPL at Watercourt A
14:50
40m
Talk
Session with the Coq Development Team
CoqPL
File Attached
16:00 - 18:00
16:00
30m
Talk
Back to the Future with Denotational Semantics
Off the Beaten Track
Jeremy G. SiekIndiana University, USA
File Attached
16:30
30m
Talk
Climbing Up the Semantic Tower — at Runtime
Off the Beaten Track
File Attached
17:00
30m
Talk
Towards A Systems Approach To Distributed Programming
Off the Beaten Track
Christopher MeiklejohnUniversité catholique de Louvain, Peter Van RoyUniversité catholique de Louvain
File Attached
17:30
30m
Day closing
Discussion and business meeting
Off the Beaten Track
16:00 - 18:05
Semantics and SynthesisCoqPL at Watercourt A
Chair(s): Ilya SergeyUniversity College London
16:00
25m
Talk
Phantom Types for Quantum Programs
CoqPL
Robert RandUniversity of Pennsylvania, Jennifer PaykinUniversity of Pennsylvania, Steve ZdancewicUniversity of Pennsylvania
File Attached
16:25
25m
Talk
Revisiting Parametricity: Inductives and Uniformity of Propositions
CoqPL
Abhishek AnandCornell University, Greg MorrisettCornell University
File Attached
16:50
25m
Talk
Towards Context-Aware Data Refinement
CoqPL
Paul KrogmeierPurdue University, Steven KiddPurdue University, Benjamin DelawarePurdue University
File Attached
17:15
25m
Talk
Mechanizing the Construction and Rewriting of Proper Functions in Coq
CoqPL
Edwin WestbrookGalois, Inc.
File Attached
17:40
25m
Talk
A calculus for logical refinements in separation logic
CoqPL
Dan FruminRadboud University, Robbert KrebbersDelft University of Technology
File Attached

Sun 7 Jan
Times are displayed in time zone: Tijuana, Baja California change

Room9:003010:003011:003012:003013:003014:003015:003016:003017:0030
Watercourt

Mon 8 Jan
Times are displayed in time zone: Tijuana, Baja California change

Mon 8 Jan
Times are displayed in time zone: Tijuana, Baja California change

Room9:0015304510:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:0015304518:0015304519:0015304520:0015304521:00153045
Bradbury
Crocker
Hershey
Hershey
Museum A
CPP
CPP Reception
18:15 - 20:15
Museum B
Rose
PADL
Opening
13:30 - 14:00
Watercourt
VMCAI
Banquet
18:00 - 22:00
Widney

Tue 9 Jan
Times are displayed in time zone: Tijuana, Baja California change

Room9:0015304510:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:00153045
Bradbury
Crocker
PEPM
Posters/Demos
16:50 - 17:30
Hershey
NetPL
Working Groups
11:00 - 12:00
NetPL
Panel
17:00 - 17:30
NetPL
Wrap Up
17:30 - 18:00
Museum A
CPP
HOpi in Coq
16:00 - 16:30
Museum B
PLMW
Dafny Overview
14:00 - 14:30
Rose
PADL
Closing
17:00 - 17:30
Watercourt

Wed 10 Jan
Times are displayed in time zone: Tijuana, Baja California change

Room8:001530459:0015304510:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:0015304518:0015304519:0015304520:0015304521:00153045
Bunker Hill
Bunker Hill / Watercourt
Lunch Room
MOCA
Watercourt

Thu 11 Jan
Times are displayed in time zone: Tijuana, Baja California change

Room8:001530459:0015304510:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:0015304518:0015304519:0015304520:00153045
Bunker Hill
Bunker Hill / Watercourt
Lunch Room
SRC
Watercourt

Fri 12 Jan
Times are displayed in time zone: Tijuana, Baja California change

Room8:001530459:0015304510:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:00153045
Bunker Hill
Bunker Hill / Watercourt
Lunch Room
SRC
Watercourt

Sat 13 Jan
Times are displayed in time zone: Tijuana, Baja California change

Room9:0015304510:0015304511:0015304512:0015304513:0015304514:00