VenueOmni Hotel
Room nameBunker Hill
Floor0
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

Conference Day
Wed 10 Jan

Displayed time zone: Tijuana, Baja California change

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
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
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

Conference Day
Thu 11 Jan

Displayed time zone: Tijuana, Baja California change

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
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 NovotnýIST 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
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

Conference Day
Fri 12 Jan

Displayed time zone: Tijuana, Baja California change

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
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
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

Conference Day
Wed 10 Jan

Displayed time zone: Tijuana, Baja California change

Conference Day
Thu 11 Jan

Displayed time zone: Tijuana, Baja California change

Conference Day
Fri 12 Jan

Displayed time zone: Tijuana, Baja California change