Write a Blog >>
VenueHilton St. Petersburg Bayfront
Room nameGrand Bay North
Floor0
Additional informationThere is no additional information of this room available.
Program

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

Wed 20 Jan
Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change

10:30 - 12:10: Track 1: Algorithmic VerificationResearch Papers at Grand Bay North
Chair(s): Arie GurfinkelCarnegie Mellon University
10:30 - 10:55
Talk
Temporal Verification of Higher-order Functional Programs
Research Papers
Akihiro Murase, Tachio TerauchiJAIST, Naoki KobayashiUniversity of Tokyo, Ryosuke SatoUniversity of Tokyo, Hiroshi UnnoUniversity of Tsukuba
10:55 - 11:20
Talk
Scaling Network Verification using Symmetry and Surgery
Research Papers
Gordon Plotkin, Nikolaj BjørnerMicrosoft Research, Nuno P. LopesMicrosoft Research, Andrey RybalchenkoMicrosoft Research, George VargheseMicrosoft Research
11:20 - 11:45
Talk
Model Checking for Symbolic-Heap Separation Logic with Inductive Predicates
Research Papers
11:45 - 12:10
Talk
Reducing Crash Recoverability to Reachability
Research Papers
Eric KoskinenYale University, Junfeng YangColumbia University
14:20 - 16:00: Track 1: Decision ProceduresResearch Papers at Grand Bay North
Chair(s): Loris D'AntoniUniversity of Pennsylvania
14:20 - 14:45
Talk
Query-Guided Maximum Satisfiability
Research Papers
Xin ZhangGeorgia Tech, Ravi MangalGeorgia Institute of Technology, Aditya NoriMicrosoft Research, UK, Mayur NaikGeorgia Tech
File Attached
14:45 - 15:10
Talk
String Solving with Word Equations and Transducers: Decidability and Applications to Detecting Mutation XSS
Research Papers
Anthony Widjaja LinYale-NUS College, Singapore, Pablo BarceloUniversity of Chile, Chile
Media Attached
15:10 - 15:35
Talk
Symbolic Computation of Differential Equivalences
Research Papers
Luca CardelliMicrosoft Research and University of Oxford, Mirco TribastoneIMT Institute for Advanced Studies Lucca, Italy, Max TschaikowskiIMT Institute for Advanced Studies Lucca, Italy, Andrea VandinIMT Institute for Advanced Studies Lucca, Italy
Media Attached
15:35 - 16:00
Talk
Unboundedness and Downward Closures of Higher-Order Pushdown Automata
Research Papers
Matthew HagueRoyal Holloway University of London, UK, Jonathan KochemsDepartment of Computer Science, University of Oxford, C.-H. Luke OngUniversity of Oxford, UK
Media Attached
16:30 - 17:45: Track 1: Language DesignResearch Papers at Grand Bay North
Chair(s): David WalkerPrinceton University
16:30 - 16:55
Talk
Dependent Types and Multi-Monadic Effects in F*
Research Papers
Nikhil SwamyMicrosoft Research, Cătălin HriţcuINRIA Paris, Chantal KellerMSR-INRIA, Aseem RastogiUniversity of Maryland, College Park, Antoine Delignat-LavaudINRIA, Simon ForestENS, Karthikeyan BhargavanINRIA, Cédric FournetMicrosoft Research, Pierre-Yves StrubIMDEA Software Institute, Markulf KohlweissMicrosoft Research, Jean-Karim ZinzindohouéINRIA, Santiago Zanella-BéguelinMicrosoft Research
Pre-print Media Attached
16:55 - 17:20
Talk
Fabular: Regression Formulas as Probabilistic Programming
Research Papers
Johannes BorgströmUppsala University, Andrew D. GordonMicrosoft Research and University of Edinburgh, Long OuyangStanford University, Claudio RussoMicrosoft Research, Adam ŚcibiorUniversity of Cambridge, Marcin SzymczakUniversity of Edinburgh
Media Attached
17:20 - 17:45
Talk
Kleenex: Compiling Nondeterministic Transducers to Deterministic Streaming Transducers
Research Papers
Bjørn Bugge GrathwohlDIKU, University of Copenhagen, Fritz HengleinDIKU, Denmark, Ulrik Terp RasmussenDIKU, University of Copenhagen, Kristoffer Aalund SøholmJobindex, Denmark, Sebastian Paaske TørholmJobindex, Denmark
Media Attached

Thu 21 Jan
Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change

10:30 - 12:10: Track 1: Foundations of distributed systemsResearch Papers at Grand Bay North
Chair(s): Mooly SagivTel Aviv University
10:30 - 10:55
Talk
Certified Causally Consistent Distributed Key-Value Stores
Research Papers
Media Attached
10:55 - 11:20
Talk
'Cause I'm Strong Enough: Reasoning about Consistency Choices in Distributed Systems
Research Papers
Alexey GotsmanIMDEA, Hongseok YangUniversity of Oxford, UK, Carla FerreiraUniversidade Nova Lisboa, Mahsa NajafzadehUPMC & INRIA, Marc ShapiroInria & LIP6
Media Attached
11:20 - 11:45
Talk
A Program Logic for Concurrent Objects under Fair Scheduling
Research Papers
Hongjin LiangUniversity of Science and Technology of China, Xinyu FengUniversity of Science and Technology of China
Media Attached
11:45 - 12:10
Talk
PSync: a partially synchronous language for fault-tolerant distributed algorithms
Research Papers
Cezara DrăgoiINRIA, ENS, CNRS, Thomas A. HenzingerIST Austria, Damien ZuffereyMIT
Link to publication DOI Pre-print Media Attached File Attached
14:20 - 16:00: Track 1: Learning and verificationResearch Papers at Grand Bay North
Chair(s): David MonniauxCNRS, VERIMAG
14:20 - 14:45
Talk
Combining Static Analysis with Probabilistic Models to Enable Market-Scale Analysis
Research Papers
Damien OcteauUniversity of Wisconsin and Pennsylvania State University, Somesh JhaUniversity of Wisconsin, Madison, Matthew DeringPennsylvania State University, Patrick McDanielPennsylvania State University, Alexandre BartelTechnical University Darmstadt, Hongyu LiRice University, Jacques KleinUniversity of Luxembourg, Yves Le TraonUniversity of Luxembourg
Media Attached
14:45 - 15:10
Talk
Abstraction Refinement Guided by a Learnt Probabilistic Model
Research Papers
Radu GrigoreUniversity of Oxford, Hongseok YangUniversity of Oxford, UK
Media Attached
15:10 - 15:35
Talk
Learning Invariants using Decision Trees and Implication Counterexamples
Research Papers
Pranav GargUniversity of Illinois at Urbana-Champaign, Daniel NeiderUniversity of Illinois at Urbana-Champaign, P. MadhusudanUniversity of Illinois at Urbana-Champaign, Dan RothUniversity of Illinois at Urbana-Champaign
Media Attached
15:35 - 16:00
Talk
Symbolic Abstract Data Type Inference
Research Papers
Michael EmmiIMDEA Software Institute, Constantin EneaLIAFA, Université Paris Diderot
Media Attached
16:30 - 17:45: Track 1: OptimizationResearch Papers at Grand Bay North
Chair(s): Mayur NaikGeorgia Tech
16:30 - 16:55
Talk
SMO: An Integrated Approach to Intra-Array and Inter-Array Storage Optimization
Research Papers
Somashekaracharya G BhaskaracharyaIndian Institute of Science and National Instruments, Uday BondhugulaIndian Institute of Science, Albert CohenINRIA
Media Attached File Attached
16:55 - 17:20
Talk
PolyCheck: Dynamic Verification of Iteration Space Transformations on Affine Programs
Research Papers
Wenlei Bao, Sriram KrishnamoorthyPacific Northwest National Laboratories, Louis-Noël PouchetOhio State University, Fabrice RastelloINRIA, France, P. SadayappanOhio State University
Media Attached
17:20 - 17:45
Talk
Printing Floating-Point Numbers: A Faster, Always Correct Method
Research Papers
Marc AndryscoUniversity of California, San Diego, Ranjit JhalaUniversity of California, San Diego, Sorin LernerUniversity of California, San Diego
Media Attached
18:00 - 19:00: SIGPLAN Awards; Program Chair's Report; and SIGPLAN Business MeetingResearch Papers at Grand Bay North
Chair(s): Michael HicksUniversity of Maryland at College Park, USA

Fri 22 Jan
Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change

10:30 - 12:10: Track 1: Program Design and AnalysisResearch Papers at Grand Bay North
Chair(s): Manu SridharanSamsung Research America
10:30 - 10:55
Talk
Newtonian Program Analysis via Tensor Product
Research Papers
Thomas RepsUniversity of Wisconsin - Madison and Grammatech Inc., Emma TuretskyCS Dept., Univ. of Wisconsin-Madison, Prathmesh PrabhuGoogle
Media Attached
10:55 - 11:20
Talk
Casper: An Efficient Approach to Call Trace Collection
Research Papers
Rongxin WuDepartment of Computer Science and Engineering, The Hong Kong University of Science and Technology, Xiao XiaoThe Hong Kong University of Science and Technology, Shing-Chi CheungDepartment of Computer Science and Engineering, The Hong Kong University of Science and Technology, Hongyu ZhangMicrosoft Research, Charles ZhangHKUST
Media Attached
11:20 - 11:45
Talk
Pushdown Control-flow Analysis for Free
Research Papers
Thomas GilrayUniversity of Utah, Steven Lyde, Michael D. AdamsUniversity of Utah, Matthew MightUniversity of Utah, USA, David Van HornUniversity of Maryland, College Park
Pre-print Media Attached
11:45 - 12:10
Talk
Binding as Sets of Scopes
Research Papers
Matthew FlattUniversity of Utah
Pre-print Media Attached
14:20 - 16:00: Track 1: SynthesisResearch Papers at Grand Bay North
Chair(s): Roberto GiacobazziUniversity of Verona, Italy
14:20 - 14:45
Talk
Learning Programs from Noisy Data
Research Papers
Veselin RaychevETH Zurich, Pavol BielikETH Zurich, Switzerland, Martin VechevETH Zurich, Andreas KrauseETH Zurich
Link to publication DOI Pre-print Media Attached File Attached
14:45 - 15:10
Talk
Optimizing Synthesis with Metasketches
Research Papers
James BornholtUniversity of Washington, Emina TorlakUniversity of Washington, Dan GrossmanUniversity of Washington, USA, Luis CezeUniversity of Washington, USA
Pre-print Media Attached
15:10 - 15:35
Talk
Maximal Specification Synthesis
Research Papers
Aws AlbarghouthiUniversity of Wisconsin–Madison, Isil DilligUniversity of Texas, Austin, Arie GurfinkelCarnegie Mellon University
Pre-print Media Attached
15:35 - 16:00
Talk
Example-Directed Synthesis: A Type-Theoretic Interpretation
Research Papers
Jonathan FranklePrinceton University, Peter-Michael OseraGrinnell College, David WalkerPrinceton University, Steve ZdancewicUniversity of Pennsylvania
Pre-print Media Attached File Attached

Wed 20 Jan
Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change

Fri 22 Jan
Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change