SPLASH 2022 (series) /
SPLASH 2022 Program
Filter Program
Dates
Rooms
Tracks
Badges
Your Program
Wed 30 NovDisplayed time zone: Auckland, Wellington change
Wed 30 Nov
Displayed time zone: Auckland, Wellington change
04:00 - 05:30 | Session 1V-OOPSLA at Virtual Airmeet Room Chair(s): Amal Ahmed Northeastern University, USA, Jan Vitek Northeastern University | ||
04:00 15mTalk | Generic Go to Go: Dictionary-Passing, Monomorphisation, and HybridPre-recorded V-OOPSLA Stephen Ellis Imperial College London, Shuofei Zhu Pennsylvania State University, Nobuko Yoshida University of Oxford, Linhai Song Pennsylvania State University DOI | ||
04:15 15mResearch paper | Coverage-guided tensor compiler fuzzing with joint IR-pass mutationPre-recorded V-OOPSLA Jiawei Liu University of Illinois at Urbana-Champaign, Yuxiang Wei Tongji University, Sen Yang Fudan University, Yinlin Deng University of Illinois at Urbana-Champaign, Lingming Zhang University of Illinois at Urbana-Champaign DOI | ||
04:30 15mTalk | Modular Verification of Op-Based CRDTs in Separation Logic V-OOPSLA Abel Nieto Aarhus University, Léon Gondelman Aarhus University, Alban Reynaud ENS Lyon, Amin Timany Aarhus University, Lars Birkedal Aarhus University DOI | ||
04:45 15mTalk | Monadic and Comonadic Aspects of Dependency Analysis V-OOPSLA Pritam Choudhury University of Pennsylvania DOI | ||
05:00 30mLive Q&A | Q&A for Session 1 V-OOPSLA | ||
21:00 - 22:45 | Session 2V-OOPSLA at Virtual Airmeet Room Chair(s): Sophia Drossopoulou Meta and Imperial College London | ||
21:00 15mTalk | Taming Transitive Redundancy for Context-Free Language ReachabilityPre-recorded V-OOPSLA Yuxiang Lei University of Technology Sydney, Yulei Sui University of New South Wales, Sydney, Shuo Ding Georgia Institute of Technology, Qirun Zhang Georgia Institute of Technology DOI | ||
21:15 15mTalk | Scalable Linear Invariant Generation with Farkas’ Lemma V-OOPSLA Hongming Liu Shanghai Jiao Tong University, Hongfei Fu Shanghai Jiao Tong University, zhiyong yu Shanghai Jiao Tong University, Jiaxin Song Shanghai Jiao Tong University, Guoqiang Li Shanghai Jiao Tong University DOI | ||
21:30 15mTalk | Consistency-Preserving Propagation for SMT Solving of Concurrent Program VerificationPre-recorded V-OOPSLA DOI | ||
21:45 15mTalk | Oracle-Free Repair Synthesis for Floating-Point ProgramsPre-recorded V-OOPSLA Daming Zou ETH Zurich, Yuchen Gu Peking University, Yuanfeng Shi Peking University, Mingzhe Wang Princeton University, Yingfei Xiong Peking University, Zhendong Su ETH Zurich DOI | ||
22:00 15mTalk | Neurosymbolic Repair for Low-Code Formula Languages V-OOPSLA Rohan Bavishi University of California at Berkeley, Harshit Joshi Microsoft, José Pablo Cambronero Microsoft, Anna Fariha Microsoft, Sumit Gulwani Microsoft, Vu Le Microsoft, Ivan Radiček Microsoft, Ashish Tiwari Microsoft DOI | ||
22:15 30mLive Q&A | Q&A for Session 2 V-OOPSLA | ||
Thu 1 DecDisplayed time zone: Auckland, Wellington change
Thu 1 Dec
Displayed time zone: Auckland, Wellington change
01:00 - 02:30 | |||
01:00 15mResearch paper | SHARP: fast incremental context-sensitive pointer analysis for JavaPre-recorded V-OOPSLA DOI | ||
01:15 15mTalk | Reasoning about Distributed Reconfigurable Systems V-OOPSLA Emma Ahrens RWTH Aachen University, Marius Bozga CNRS; Université Grenoble Alpes, Radu Iosif CNRS; Université Grenoble Alpes, Joost-Pieter Katoen RWTH Aachen University DOI | ||
01:30 15mTalk | Type-Directed Synthesis of Visualizations from Natural Language Queries V-OOPSLA Jocelyn (Qiaochu) Chen University of Texas at Austin, Shankara Pailoor University of Texas at Austin, Celeste Barnaby University of Texas at Austin, Abby Criswell University of Texas at Austin, Chenglong Wang Microsoft Research, Greg Durrett University of Texas at Austin, Işıl Dillig University of Texas at Austin DOI | ||
01:45 15mTalk | Model Checking for a Multi-Execution Memory Model V-OOPSLA DOI | ||
02:00 30mLive Q&A | Q&A for Session 3 V-OOPSLA | ||
Mon 5 DecDisplayed time zone: Auckland, Wellington change
Mon 5 Dec
Displayed time zone: Auckland, Wellington change
09:00 - 10:00 | Keynote 1SAS at AMRF Auditorium Chair(s): Gagandeep Singh University of Illinois at Urbana-Champaign, Caterina Urban Inria & École Normale Supérieure | Université PSL | ||
09:00 60mKeynote | Commercial-Grade Static Analyzers in DatalogIn PersonKeynote SAS Bernhard Scholz University of Sydney | ||
09:00 - 10:00 | |||
09:00 60mKeynote | Verification of Concurrent Programs under Release-Acquire ConcurrencyKeynoteVirtual APLAS Shankaranarayanan Krishna IIT Bombay, India | ||
09:00 - 10:00 | Morning 1SPLASH-E at Seminar Room G125 Chair(s): Molly Q Feldman Oberlin College The session is hybrid, with the first talk being in-person, and the second virtual. The physical venue G125 has video equipment for online presentation via airmeet. The SPLASH 2022 airmeet page is: https://tinyurl.com/splash2022virtual. Look for the SPLASH-E sessions there and bookmark them. For issues, use the airmeet chat if you are joining online, and look for the student volunteer Jiwon Park, if you in G125. | ||
09:00 30mTalk | Codehound: Helping Instructors Track Pedagogical Code Dependencies in Course MaterialsIn Person SPLASH-E DOI | ||
09:30 30mTalk | The Role of Abstraction in Introductory ProgrammingVirtual SPLASH-E Kezia Devathasan University of Victoria, Celina Berg University of Victoria, Daniela Damian University of Victoria DOI | ||
09:00 - 10:00 | |||
09:00 15mTalk | Creating Dynamic Prototypes from Web Page SketchesVirtual PAINT DOI | ||
09:15 15mTalk | Toward a VR-Native Live Programming EnvironmentVirtual PAINT Leonard Geier University of Potsdam; Hasso Plattner Institute, Clemens Tiedt University of Potsdam; Hasso Plattner Institute, Tom Beckmann University of Potsdam; Hasso Plattner Institute, Marcel Taeumel University of Potsdam; Hasso Plattner Institute, Robert Hirschfeld University of Potsdam; Hasso Plattner Institute DOI | ||
09:30 15mTalk | Suppose You Had Blocks within a NotebookVirtual PAINT Mauricio Verano Merino Vrije Universiteit Amsterdam, Juan Pablo Sáenz Politecnico di Torino, Ana María Díaz Castillo Teach for All DOI Pre-print | ||
09:45 15mTalk | Interaction vs. Abstraction: Managed Copy and PasteVirtual PAINT DOI Pre-print | ||
10:00 - 10:30 | |||
10:00 30mCoffee break | Coffee break Catering and Social Events | ||
10:30 - 12:00 | |||
10:30 30mTalk | Parameterized Recursive Refinement Types for Automated Program Verification SAS Ryoya Mukai The University of Tokyo, Naoki Kobayashi University of Tokyo, Japan, Ryosuke Sato University of Tokyo, Japan | ||
11:00 30mTalk | Efficient Modular SMT-Based Model Checking of Pointer ProgramsVirtual SAS Isabel Garcia-Contreras University of Waterloo, Arie Gurfinkel University of Waterloo, Jorge A. Navas Certora, inc. | ||
11:30 30mTalk | Case Study on Verification-Witness Validators: Where We Are and Where We Go SAS Link to publication DOI Media Attached | ||
10:30 - 12:00 | Semantics and AnalysisAPLAS at Seminar Room G007 Chair(s): Julian Mackay Victoria University of Wellington | ||
10:30 30mTalk | An Algebraic Theory for Shared-State Concurrency APLAS File Attached | ||
11:00 30mTalk | Decoupling the Ascending and Descending Phases in Abstract Interpretation APLAS Vincenzo Arceri University of Parma, Italy, Isabella Mastroeni University of Verona, Italy, Enea Zaffanella University of Parma, Italy | ||
11:30 30mTalk | Inferring Region Types via an Abstract Notion of Environment Transformation APLAS | ||
10:30 - 12:00 | |||
10:30 5mTalk | Welcome Notes VMIL Stefan Marr University of Kent | ||
10:35 30mTalk | Ease Virtual Machine Level Tooling with Language Level Ordinary Object PointersVirtual VMIL Pierre Misse-Chanabier University of Lille; Inria; CNRS; Centrale Lille; UMR 9189 CRIStAL, Théo Rogliano University of Lille; Inria; CNRS; Centrale Lille; UMR 9189 CRIStAL DOI | ||
11:05 30mTalk | Inlining-Benefit Prediction with Interprocedural Partial Escape AnalysisVirtual VMIL Matthew Edwin Weingarten ETH Zurich; Oracle Labs, Theodoros Theodoridis ETH Zurich, Aleksandar Prokopec Oracle Labs DOI | ||
11:35 25mTalk | Toward a dynamic language toolkit Virtual VMIL Dave Mason Toronto Metropolitan University (formerly Ryerson University) | ||
10:30 - 12:00 | Morning 2SPLASH-E at Seminar Room G125 Chair(s): Martin Henz National University of Singapore The session is hybrid, with the first talk being virtual (pre-recorded with live Q&A), and the second in-person. The physical venue G125 has video equipment for online presentation via airmeet. The SPLASH 2022 airmeet page is: https://tinyurl.com/splash2022virtual. Look for the SPLASH-E sessions there and bookmark them. For issues, use the airmeet chat if you are joining online, and look for the student volunteer Jiwon Park, if you in G125. | ||
10:30 30mTalk | Data Science Pedagogy to Support Industry, Governmental, and Research InitiativesPre-recorded SPLASH-E Kevin Dick Carleton University, Hoda Khalil Carleton University, Gabriel A. Wainer Carleton University DOI | ||
11:00 30mTalk | Crossing Learning Thresholds Progressively via Active LearningIn Person SPLASH-E DOI | ||
11:30 30mOther | Discussion SPLASH-E | ||
10:30 - 12:00 | |||
10:30 15mTalk | Integration testing can be reliable and low-effort in a projectional IDE through snapshots - DEMOVirtual PAINT Bastian Kruck itemis SECURE // Hasso Plattner Institute | ||
10:45 15mTalk | Towards a Python 3 IDE for Teaching Creative Programming PAINT Tristan Bunn Victoria University of Wellington, Craig Anslow Victoria University of Wellington, Karsten Lundqvist | ||
11:00 15mTalk | Conjecturing on a Fundamental Theorem of Computation and its Implications for a New Theory in Programmer Experience Design PAINT Gary Miller University of Technology Sydney | ||
11:15 15mTalk | Domain-Specific Visual Language for Data Engineering Quality PAINT DOI Pre-print | ||
11:30 15mTalk | Blocks, Blocks, and More Blocks-Based Programming PAINT Benjamin Selwyn-Smith Oracle Labs, Craig Anslow Victoria University of Wellington, Michael Homer Victoria University of Wellington DOI | ||
11:45 15mTalk | Interleaved 2D Notation for Concatenative Programming PAINT Michael Homer Victoria University of Wellington DOI Pre-print | ||
11:00 - 12:00 | SLE and GPCE PapersCOVID Time Papers In Person at Lecture Theatre 2 Chair(s): Andreea Costea School of Computing, National University Of Singapore | ||
11:00 30mTalk | FIDDLR: streamlining reuse with concern-specific modelling languages COVID Time Papers In Person Maximilian Schiedermeier McGill University, Jörg Kienzle McGill University, Canada, Bettina Kemme McGill University, Canada Link to publication DOI | ||
11:30 30mTalk | Manipulating GUI Structures Declaratively COVID Time Papers In Person Link to publication DOI | ||
12:00 - 13:30 | |||
12:00 90mLunch | Lunch Catering and Social Events | ||
13:30 - 15:00 | Numerical Static AnalysesSAS at AMRF Auditorium Chair(s): Isabella Mastroeni University of Verona, Italy | ||
13:30 30mTalk | CLEVEREST: Accelerating CEGAR-based Neural Network Verification via Adversarial AttacksVirtual SAS Zhe Zhao ShanghaiTech University, Yedi Zhang ShanghaiTech University, Guangke Chen ShanghaiTech University, Fu Song ShanghaiTech University, Taolue Chen Birkbeck University of London, Jiaxiang Liu Shenzhen University | ||
14:00 30mTalk | Boosting Robustness Verification of Semantic Feature Neighborhoods SAS | ||
14:30 30mTalk | Lifting Numeric Relational Domains to Algebraic Data Types SAS Santiago Bautista Univ Rennes, Inria, CNRS, IRISA, Thomas P. Jensen INRIA Rennes, Benoît Montagu Inria Pre-print File Attached | ||
13:30 - 14:30 | SLE papersCOVID Time Papers In Person at Lecture Theatre 2 Chair(s): Peter Thiemann University of Freiburg, Germany | ||
13:30 30mTalk | Automatic Grammar Repair COVID Time Papers In Person Moeketsi Raselimo Stellenbosch University, South Africa, Bernd Fischer Stellenbosch University, South Africa Link to publication DOI | ||
14:00 30mTalk | Grammar-based testing for little languages: an experience report with student compilers COVID Time Papers In Person Phillip van Heerden Stellenbosch University, Moeketsi Raselimo Stellenbosch University, South Africa, Konstantinos (Kostis) Sagonas Uppsala University and Nat. Tech. Univ. of Athens, Bernd Fischer Stellenbosch University, South Africa Link to publication DOI | ||
13:30 - 15:00 | Testing and VerificationAPLAS at Seminar Room G007 Chair(s): Jonathan Aldrich Carnegie Mellon University | ||
13:30 30mTalk | RHLE: Modular Deductive Verification of Relational ∀∃ Properties APLAS Robert Dickerson Purdue University, Qianchuan Ye Purdue University, Michael K. Zhang Purdue University, Benjamin Delaware Purdue University | ||
14:00 30mTalk | Automated Temporal Verification for Algebraic Effects APLAS Yahui Song National University of Singapore, Darius Foo National University of Singapore, Wei-Ngan Chin National University of Singapore | ||
14:30 30mTalk | Model-based Fault Classification for Automotive Software APLAS Mike Becker TU Braunschweig, Roland Meyer TU Braunschweig, Tobias Runge TU Braunschweig, Ina Schaefer KIT, Sören van der Wall PhD Student, Sebastian Wolff New York University | ||
13:30 - 15:00 | |||
13:30 60mKeynote | Virgil as a Systems Programming Language VMIL Ben L. Titzer Carnegie Mellon University | ||
14:30 30mTalk | Improving Vectorization Heuristics in a Dynamic Compiler with Machine Learning Models VMIL Raphael Mosaner JKU Linz, Gergö Barany Oracle Labs, David Leopoldseder Oracle Labs, Hanspeter Mössenböck JKU Linz DOI | ||
13:30 - 15:00 | Afternoon 1SPLASH-E at Seminar Room G125 Chair(s): Eli Tilevich Virginia Tech The session is hybrid, with the first talk being virtual, and the second in-person. The physical venue G125 has video equipment for online presentation via airmeet. The SPLASH 2022 airmeet page is: https://tinyurl.com/splash2022virtual. Look for the SPLASH-E sessions there and bookmark them. For issues, use the airmeet chat if you are joining online, and look for the student volunteer Wang Chengpeng, if you in G125. | ||
13:30 30mTalk | Team Harmony before, during, and after COVID-19Virtual SPLASH-E Noa Heyl University of British Columbia, Elisa Baniassad University of British Columbia, Oluwakemi Ola University of British Columbia DOI | ||
14:00 30mTalk | Expressions in Java: Essential, Prevalent, Neglected?In Person SPLASH-E DOI | ||
14:30 30mOther | Discussion SPLASH-E | ||
15:00 - 15:30 | |||
15:00 30mCoffee break | Coffee break Catering and Social Events | ||
15:30 - 17:00 | Keynote 2, Radhia Cousot Award, PC Chairs ReportSAS at AMRF Auditorium Chair(s): Gagandeep Singh University of Illinois at Urbana-Champaign, Caterina Urban Inria & École Normale Supérieure | Université PSL | ||
15:30 60mKeynote | Logical Reasoning in Reinforcement Learning: A Boon or Bane? KeynoteVirtual SAS Suguman Bansal Rice University, USA | ||
16:30 10mAwards | Radhia Cousot Award SAS Caterina Urban Inria & École Normale Supérieure | Université PSL, Gagandeep Singh University of Illinois at Urbana-Champaign | ||
16:40 20mDay closing | PC Chairs Report SAS Caterina Urban Inria & École Normale Supérieure | Université PSL, Gagandeep Singh University of Illinois at Urbana-Champaign | ||
15:30 - 17:30 | |||
15:30 30mTalk | Characterizing functions mappable over GADTs APLAS | ||
16:00 30mTalk | Applicative Intersection Types APLAS Xu Xue University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong, Ningning Xie University of Toronto | ||
16:30 30mTalk | A Calculus with Recursive Types, Record Concatenation and Subtyping APLAS Yaoda Zhou University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong, Andong Fan Hong Kong University of Science and Technology | ||
17:00 30mTalk | Novice Type Error Diagnosis with Natural Language Models APLAS Chuqin Geng McGill University, Haolin Ye McGill University, Yixuan Li McGill University, Tianyu Han McGill University, Brigitte Pientka McGill University, Xujie Si McGill University, Canada | ||
15:30 - 17:00 | |||
15:30 60mKeynote | MMTk and The Case for Modular VM Development VMIL Steve Blackburn Google and Australian National University | ||
16:30 30mTalk | Profile Guided Offline Optimization of Hidden Class Graphs for JavaScript VMs in Embedded Systems VMIL Tomoharu Ugawa University of Tokyo, Stefan Marr University of Kent, Richard Jones University of Kent DOI | ||
15:30 - 17:00 | Afternoon 2SPLASH-E at Seminar Room G125 Chair(s): Benjamin Lerner Northeastern University, United States Both talks in this session are given in-person. The physical venue G125 has video equipment for online participation via airmeet. The SPLASH 2022 airmeet page is: https://tinyurl.com/splash2022virtual. Look for the SPLASH-E sessions there and bookmark them. For issues, use the airmeet chat if you are joining online, and look for the student volunteer Jiwon Park, if you in G125. | ||
15:30 30mTalk | Mio: A Block-Based Environment for Program DesignIn Person SPLASH-E Junya Nose SoftBank, Youyou Cong Tokyo Institute of Technology, Hidehiko Masuhara Tokyo Institute of Technology DOI | ||
16:00 30mTalk | Evaluating the Quality of Student-Written Software Tests with Curated Mutation AnalysisIn Person SPLASH-E DOI | ||
16:30 30mOther | Discussion SPLASH-E | ||
18:00 - 20:00 | SPLASH PostersStudent Research Competition / Posters at Atrium Chair(s): Xujie Si McGill University, Canada, Caterina Urban Inria & École Normale Supérieure | Université PSL | ||
18:00 2hPoster | Simple Extensible Programming through Precisely-Typed Open Recursion Student Research Competition Andong Fan Hong Kong University of Science and Technology DOI | ||
18:00 2hPoster | CodeSpider: Automatic Code Querying with Multi-modal Conjunctive Query Synthesis Student Research Competition Chengpeng Wang Hong Kong University of Science and Technology DOI | ||
18:00 2hPoster | LoRe: Local-First Reactive Programming with Verified Safety Guarantees Student Research Competition Julian Haas TU Darmstadt DOI | ||
18:00 2hPoster | Qiwi: A Beginner Friendly Quantum Language Student Research Competition DOI | ||
18:00 2hPoster | Provably Correct Smart Contracts: An Approach using DeepSEA Posters DOI | ||
18:00 2hPoster | Tower: Data Structures in Quantum Superposition Posters Charles Yuan Massachusetts Institute of Technology, Michael Carbin Massachusetts Institute of Technology | ||
18:00 2hPoster | Using Mutations to Analyze Formal Specifications Student Research Competition Siraphob Phipathananunth Vanderbilt University DOI | ||
18:00 2hPoster | Competitive Debugging: Toward Contests Promoting Debugging as a Skill Posters Patrick Rein University of Potsdam; Hasso Plattner Institute, Tom Beckmann University of Potsdam; Hasso Plattner Institute, Leonard Geier University of Potsdam; Hasso Plattner Institute, Toni Mattis University of Potsdam; Hasso Plattner Institute, Robert Hirschfeld University of Potsdam; Hasso Plattner Institute | ||
18:00 2hPoster | Foundationally Sound Annotation Verifier via Control Flow Splitting Student Research Competition Litao Zhou Shanghai Jiao Tong University DOI | ||
18:00 2hPoster | Semi-symbolic Inference for Efficient Streaming Probabilistic Programming Posters Eric Atkinson Massachusetts Institute of Technology, Charles Yuan Massachusetts Institute of Technology, Guillaume Baudart Inria, Louis Mandel IBM Research, Michael Carbin Massachusetts Institute of Technology | ||
18:00 2hPoster | A Study of the Impact of Callbacks in Staged Static+Dynamic Partial Analysis Student Research Competition Aditya Anand IIT Mandi DOI | ||
18:00 2hPoster | Multiverse Notebook: A Notebook Environment for Safe and Efficient Exploration Posters DOI | ||
18:00 2hPoster | Katara: Synthesizing CRDTs with Verified Lifting Posters Shadaj Laddad University of California at Berkeley, Conor Power University of California at Berkeley, Mae Milano University of California at Berkeley, Alvin Cheung University of California at Berkeley, Joseph M. Hellerstein University of California at Berkeley | ||
18:00 2hPoster | Explicit Code Reuse Recommendation Posters DOI | ||
18:00 2hPoster | Automated Verification for Real-Time Systems using Implicit Clocks and an Extended Antimirov Algorithm Student Research Competition DOI | ||
18:00 2hPoster | Composing Linear Types and Separation Logic Proofs of Memory Safety Posters Pilar Selene Linares Arévalo University of Melbourne DOI | ||
18:00 2hPoster | ARENA: Enhancing Abstract Refinement for Neural Network Verification Student Research Competition Yuyi Zhong National University of Singapore, Quang-Trung Ta National University of Singapore, Siau-Cheng Khoo National University of Singapore DOI | ||
18:00 2hPoster | Termination of Recursive Functions by Lexicographic Orders of Linear Combinations Student Research Competition DOI | ||
Tue 6 DecDisplayed time zone: Auckland, Wellington change
Tue 6 Dec
Displayed time zone: Auckland, Wellington change
08:45 - 08:57 | SLE OpeningSLE at Seminar Room G007 Chair(s): Lola Burgueño University of Malaga, Walter Cazzola Università degli Studi di Milano | ||
08:45 12mDay opening | SLE Opening SLE Bernd Fischer Stellenbosch University, South Africa, Lola Burgueño University of Malaga, Walter Cazzola Università degli Studi di Milano | ||
09:00 - 10:00 | Keynote 3SAS at AMRF Auditorium Chair(s): Gagandeep Singh University of Illinois at Urbana-Champaign, Caterina Urban Inria & École Normale Supérieure | Université PSL | ||
09:00 60mKeynote | Towards Efficient Reasoning of Quantum ProgramsKeynote SAS Nengkun Yu Stony Brook University, USA | ||
09:00 - 10:00 | |||
09:00 15mDay opening | Welcome to Unsound Unsound | ||
09:15 45mTalk | What do we mean by "unsound"?Virtual Unsound Jan Bessai Independent | ||
09:00 - 10:00 | |||
09:00 5mOther | WelcomeIn Person Doctoral Symposium | ||
09:05 35mTalk | Researching with Undergraduates: a Curricular ApproachIn Person Doctoral Symposium | ||
09:40 20mOther | Elevator PitchesIn Person Doctoral Symposium | ||
10:00 - 10:30 | |||
10:00 30mCoffee break | Coffee break Catering and Social Events | ||
10:30 - 12:00 | |||
10:30 30mTalk | SecWasm: Information Flow Control for WebAssemblyVirtual SAS Iulia Bastys Chalmers University of Technology, Maximilian Algehed Chalmers University of Technology, Sweden, Alexander Sjösten TU Wien, Andrei Sabelfeld Chalmers University of Technology | ||
11:00 30mTalk | Adversarial Logic SAS Julien Vanegue Bloomberg | ||
11:30 30mTalk | Property-driven code obfuscations - Reinterpreting Jones-optimality in Abstract Interpretation SAS | ||
10:30 - 12:00 | Session 2. Language Workbenches and Programming EnvironmentsSLE at Seminar Room G007 Chair(s): Stefan Marr University of Kent | ||
10:30 24mTalk | Workbench for Creating Block-Based EnvironmentsResearch PaperIn Person SLE DOI Pre-print | ||
10:54 24mTalk | Partial Parsing for Structured EditorsVirtualResearch Paper SLE Tom Beckmann University of Potsdam; Hasso Plattner Institute, Patrick Rein University of Potsdam; Hasso Plattner Institute, Toni Mattis University of Potsdam; Hasso Plattner Institute, Robert Hirschfeld University of Potsdam; Hasso Plattner Institute DOI Pre-print | ||
11:18 24mTalk | A Language-Parametric Approach to Exploratory Programming EnvironmentsResearch PaperIn Person SLE L. Thomas van Binsbergen University of Amsterdam, Damian Frölich University of Amsterdam, Mauricio Verano Merino Vrije Universiteit Amsterdam, Joey Lai University of Amsterdam, Pierre Jeanjean Inria; University of Rennes; CNRS; IRISA, Tijs van der Storm CWI; University of Groningen, Benoit Combemale University of Rennes; Inria; CNRS; IRISA, Olivier Barais University of Rennes; Inria; CNRS; IRISA DOI Pre-print | ||
11:42 15mTalk | Freon: An Open Web Native Language WorkbenchTool PaperVirtual SLE DOI | ||
10:30 - 12:00 | Session 1PLMW at Seminar Room G080 Chair(s): Youyou Cong Tokyo Institute of Technology, James Tizard University of Auckland | ||
10:30 90mDay opening | Welcome to PLMW! PLMW | ||
10:30 - 12:00 | |||
10:30 45mTalk | How to trust a verified program?Virtual Unsound Wouter Swierstra Utrecht University, Netherlands | ||
11:15 45mTalk | MetaCoq as a tool to prevent future unsoundness in CoqVirtual Unsound Yannick Forster Inria | ||
10:30 - 12:00 | |||
10:30 30mTalk | Towards a Verified Cost Model for Call-by-Push-ValueIn Person Doctoral Symposium Zhuo Chen University of Melbourne DOI | ||
11:00 30mTalk | Formally Verified Resource Bounds through Implicit Computational ComplexityIn Person Doctoral Symposium Neea Rusch Augusta University DOI | ||
11:30 30mTalk | Proving Obliviousness of Probabilistic Algorithms with Formal VerificationIn Person Doctoral Symposium Pengbo Yan University of Melbourne DOI | ||
10:30 - 12:00 | Keynote, Talks I, and IntroductionsLIVE at Seminar Room LG004 Chair(s): Jun Kato National Institute of Advanced Industrial Science and Technology (AIST), Sam Lau University of California at San Diego | ||
10:30 60mKeynote | Searching for LifeIn-personKeynote LIVE Peter van Hardenberg Ink & Switch | ||
11:30 20mTalk | Potluck: dynamic documents as personal softwarePre-recorded LIVE | ||
11:50 10mSocial Event | Introductions LIVE | ||
12:00 - 13:30 | |||
13:30 - 15:00 | |||
13:30 30mTalk | Invariant Inference With Provable Complexity From the Monotone Theory SAS | ||
14:00 30mTalk | Local Completeness Logic on Kleene Algebra with Tests SAS Marco Milanese Dipartimento di Matematica, University of Padova, Italy, Francesco Ranzato University of Padova | ||
14:30 30mTalk | Deciding program properties via complete abstractions on bounded domains SAS Roberto Bruni University of Pisa, Roberta Gori University of Pisa, Nicolas Manini IMDEA Software Institute | ||
13:30 - 14:35 | GPCE KeynoteGPCE Keynote at Seminar Room G007 Chair(s): Bernhard Scholz The University of Sydney, Yukiyoshi Kameyama University of Tsukuba | ||
13:30 65mKeynote | Language Design meets Verifying CompilersIn PersonKeynote GPCE Keynote David J. Pearce ConsenSys DOI | ||
13:30 - 15:00 | Mentoring Session - TuesdayPLMW at Seminar Room G080 Chair(s): Youyou Cong Tokyo Institute of Technology, Molly Q Feldman Oberlin College, James Tizard University of Auckland, Lukasz Ziarek University at Buffalo | ||
13:30 90mSocial Event | Mentoring Sessions PLMW | ||
13:30 - 15:00 | |||
13:30 20mTalk | Proving False in Object Oriented Verification Programs by Exploiting Non-Termination Unsound | ||
13:50 45mTalk | The 4 horsemen of unsoundness in OO languages Unsound Marco Servetto Victoria University of Wellington | ||
14:35 25mPanel | Discussion Unsound Marco Servetto Victoria University of Wellington | ||
13:30 - 15:00 | |||
13:30 30mTalk | Verification of Programs with Concealed ComponentsIn Person Doctoral Symposium Sumit Lahiri IIT Kanpur DOI | ||
14:00 30mTalk | Verification of Hardware and Software with Fuzzing and ProofsIn Person Doctoral Symposium Sujit Kumar Muduli IIT Kanpur DOI | ||
14:30 30mTalk | Programming Support for Local-First Software: Enabling the Design of Privacy-Preserving Distributed Software without Relying on the CloudIn Person Doctoral Symposium Julian Haas TU Darmstadt DOI | ||
13:30 - 15:00 | Talks IILIVE at Seminar Room LG004 Chair(s): Jun Kato National Institute of Advanced Industrial Science and Technology (AIST), Sam Lau University of California at San Diego | ||
13:30 10mShort-paper | Docable: Towards a Live Learning EnvironmentVirtual LIVE | ||
13:40 10mShort-paper | System-Specific Interpreters Make Megasystems FriendlierIn-person LIVE Matthew Sotoudeh Stanford University Link to publication | ||
13:50 20mTalk | Tidyparse: Real-Time Context Free Error CorrectionIn-person LIVE Breandan Considine McGill University, Jin L.C. Guo McGill University, Xujie Si McGill University, Canada | ||
14:10 20mTalk | Live Programming and Text Editor Integration in the Croquet Microverse 3D Collaborative Construction SystemIn-person LIVE Yoshiki Ohshima Croquet Corporation, Shizuoka University, Aran Lunzer Croquet Corporation, Vanessa Freudenberg Croquet Corp, Brian Upton , David Smith | ||
14:30 20mShort-paper | Cascade: a Meta-Language for Change, Cause and EffectVirtual LIVE Riemer van Rozen CWI Pre-print | ||
14:35 - 15:00 | |||
14:35 24mTalk | From Coverage Computation to Fault Localization: A Generic Framework for Domain-Specific LanguagesVirtualResearch Paper SLE Faezeh Khorram IMT Atlantique; Nantes Université; École Centrale Nantes, Erwan Bousse IMT Atlantique; Nantes Université; École Centrale Nantes, Antonio Garmendia JKU Linz, Jean-Marie Mottu IMT Atlantique; Nantes Université; École Centrale Nantes, Gerson Sunyé IMT Atlantique; Nantes Université; École Centrale Nantes, Manuel Wimmer JKU Linz DOI Pre-print | ||
15:00 - 15:30 | |||
15:00 30mCoffee break | Coffee break Catering and Social Events | ||
15:30 - 17:00 | |||
15:30 30mTalk | Bootstrapping Library-Based Synthesis SAS | ||
16:00 30mTalk | Automated Synthesis of Asynchronizations SAS Sidi Mohamed Beillahi University of Toronto, Ahmed Bouajjani IRIF, Université Paris Diderot, Constantin Enea Ecole Polytechnique / LIX / CNRS, Shuvendu K. Lahiri Microsoft Research | ||
16:30 30mTalk | Solving Invariant Generation for Unsolvable Loops SAS Daneshvar Amrollahi Stanford University, Ezio Bartocci TU Wien, George Kenison TU Wien, Laura Kovács TU Wien, Marcel Moosbrugger TU Wien, Miroslav Stankovič TU Wien | ||
15:30 - 17:00 | |||
15:30 60mTalk | Managing Your Research, Your Advisor, Your PhD PLMW Amal Ahmed Northeastern University, USA | ||
15:30 - 17:00 | |||
15:30 22mTalk | Language-Integrated Query for Temporal DataIn Person GPCE Simon Fowler University of Glasgow, Vashti Galpin University of Edinburgh, James Cheney University of Edinburgh DOI | ||
15:52 22mTalk | Type System for Four Delimited Control OperatorsIn PersonBest Paper GPCE DOI | ||
16:15 22mTalk | SQL to Stream with S2S: An Automatic Benchmark Generator for the Java Stream APIIn PersonTool Demo GPCE DOI | ||
16:37 8mOther | PC Chair's Report GPCE Yukiyoshi Kameyama University of Tsukuba | ||
15:30 - 17:30 | |||
15:30 30mTalk | Modelling the Quantification of Technical DebtIn Person Doctoral Symposium Judith Perera University of Auckland DOI | ||
16:00 30mTalk | Towards Automated Updates of Software DependenciesIn Person Doctoral Symposium Dhanushka Jayasuriya University of Auckland DOI | ||
16:30 30mTalk | Grammar Inference for Ad Hoc ParsersIn Person Doctoral Symposium Michael Schröder TU Wien DOI Pre-print | ||
17:00 30mTalk | Program Synthesis for Artifacts beyond ProgramsIn Person Doctoral Symposium Pankaj Kumar Kalita IIT Kanpur DOI | ||
15:30 - 17:00 | Talks IIILIVE at Seminar Room LG004 Chair(s): Jun Kato National Institute of Advanced Industrial Science and Technology (AIST), Sam Lau University of California at San Diego | ||
15:30 10mShort-paper | Education-aware Interactive Machine Teaching: Training Autonomous Game AgentsVirtual LIVE Chunqi Zhao , I-Chao Shen , Tsukasa Fukusato The University of Tokyo, Jun Kato National Institute of Advanced Industrial Science and Technology (AIST), Takeo Igarashi The University of Tokyo | ||
15:40 10mShort-paper | Flowie, a Collaborative Projection EditorIn-person LIVE | ||
15:50 20mTalk | Meta-programmable functional notebooks with LivebookPre-recorded LIVE José Valim Dashbit | ||
16:10 20mTalk | Live 2D Compositional ProgrammingIn-person LIVE Michael Homer Victoria University of Wellington Link to publication | ||
16:30 20mTalk | Ampleforth: A Live Literate EditorVirtual LIVE Gilad Bracha F5 | ||
Wed 7 DecDisplayed time zone: Auckland, Wellington change
Wed 7 Dec
Displayed time zone: Auckland, Wellington change
09:00 - 10:00 | SLE KeynoteSLE Keynote / SLE at Seminar Room G007 Chair(s): Lola Burgueño University of Malaga, Walter Cazzola Università degli Studi di Milano | ||
09:00 60mKeynote | People do not want to learn a new language but a new libraryIn PersonKeynote SLE Keynote Shigeru Chiba University of Tokyo DOI | ||
09:00 - 10:00 | |||
09:00 60mKeynote | Abstractions and Execution Engines for Scalable & Consistent Cloud Applications: are we there yet?VirtualKeynote REBLS Asterios Katsifodimos TU Delft | ||
09:00 - 10:00 | |||
09:00 30mTalk | Program Synthesis Using Example PropagationVirtual HATRA Niek Mulleners Utrecht University, Johan Jeuring Utrecht University, Bastiaan Heeren Open University of the Netherlands, Netherlands Link to publication | ||
09:30 30mTalk | Some Problems with Properties: A Study on Property-Based Testing in IndustryVirtual HATRA Harrison Goldstein University of Pennsylvania, Joseph W. Cutler University of Pennsylvania, Adam Stein University of Pennsylvania, Benjamin C. Pierce University of Pennsylvania, Andrew Head University of Pennsylvania Link to publication | ||
09:00 - 10:00 | |||
09:00 60mKeynote | Cooperative Verification: Towards Reliable Safety-Critical Systems In Person FTSCS Dirk Beyer LMU Munich Link to publication DOI | ||
10:00 - 10:30 | |||
10:00 30mCoffee break | Coffee break Catering and Social Events | ||
10:30 - 12:00 | |||
10:30 30mTalk | Semantic Foundations for Cost Analysis of Pipeline-Optimized ProgramsVirtual SAS Solène Mirliaz ENS Rennes / IRISA / Inria, David Pichardie Meta, Gilles Barthe MPI-SP, Germany / IMDEA Software Institute, Spain, Adrien Koutsos INRIA Paris, Peter Schwabe Max Planck Institute for Security and Privacy | ||
11:00 30mTalk | Principles of Staged Static+Dynamic Partial Analysis SAS | ||
11:30 30mTalk | Fast and incremental computation of weak control closure SAS Abu Naser Masud Malardalen University | ||
10:30 - 12:00 | Session 6. Language Implementation, Debugging and OptimizationSLE at Seminar Room G007 Chair(s): Marco Servetto Victoria University of Wellington | ||
10:30 24mTalk | A Multi-target, Multi-paradigm DSL Compiler for Algorithmic Graph ProcessingVirtualResearch Paper SLE Houda Boukham Ecole Mohammadia d'Ingénieurs; Oracle Labs, Guido Wachsmuth Oracle Labs, Martijn Dwars Oracle Labs, Dalila Chiadmi Ecole Mohammadia d'Ingénieurs DOI | ||
10:54 24mTalk | Optimising First-Class Pattern MatchingResearch PaperIn Person SLE Jeff Smits Delft University of Technology, Toine Hartman Independent, Jesper Cockx Delft University of Technology DOI | ||
11:18 24mTalk | Specializing Scope Graph Resolution QueriesResearch PaperIn Person SLE Aron Zwaan Delft University of Technology DOI | ||
11:42 15mTalk | Reflection as a Tool to Debug ObjectsTool PaperVirtual SLE Steven Costiou INRIA Lille, Vincent Aranega Univ. Lille, CNRS, Inria, Centrale Lille, UMR 9189 - CRIStAL, Marcus Denker INRIA Lille DOI | ||
10:30 - 12:00 | Mentoring Session - WednesdayPLMW at Seminar Room G080 Chair(s): Youyou Cong Tokyo Institute of Technology, Molly Q Feldman Oberlin College, James Tizard University of Auckland, Lukasz Ziarek University at Buffalo | ||
10:30 90mSocial Event | Mentoring Sessions PLMW | ||
10:30 - 12:00 | |||
10:30 22mTalk | Incremental Processing of Structured Data in DatalogVirtual GPCE DOI | ||
10:52 22mTalk | Data Types as a More Ergonomic Frontend for Grammar-Guided Genetic ProgrammingVirtual GPCE Guilherme Espada University of Lisbon, Leon Ingelse University of Lisbon, Paulo Canelas University of Lisbon; Carnegie Mellon University, Pedro Barbosa University of Lisbon; Instituto de Medicina Molecular, Alcides Fonseca University of Lisbon DOI | ||
11:15 22mTalk | Deep Fusion for Efficient Nested Recursive ComputationsVirtual GPCE Amir Shaikhha University of Edinburgh DOI | ||
11:37 22mTalk | Composable Sequence Macros for Fast IterationVirtual GPCE Anna Bolotina Czech Technical University in Prague, Ryan Culpepper Czech Technical University in Prague DOI | ||
10:30 - 12:00 | |||
10:30 30mTalk | Towards Introducing Asynchronous Tasks to an FRP Language for Small-Scale Embedded Systems REBLS Akihiko Yokoyama Tokyo Institute of Technology, Sosuke Moriguchi Tokyo Institute of Technology, Takuo Watanabe Tokyo Institute of Technology DOI Pre-print | ||
11:00 30mTalk | Semantics of RxJSPre-recorded REBLS DOI | ||
11:30 30mTalk | About Combining Functional Reactive Programming and Replicated Data TypesPre-recorded REBLS File Attached | ||
10:30 - 12:00 | |||
10:30 30mTalk | Exploring the Verifiability of Code Generated by GitHub Copilot HATRA Dakota Wong University of Waterloo, Austin Kothig University of Waterloo, Patrick Lam University of Waterloo Link to publication | ||
11:00 30mTalk | Holbert: Reading, Writing, Proving and Learning in the Browser HATRA Link to publication Media Attached | ||
11:30 30mTalk | A Survey of Weak Reasoning Assistants HATRA Matthew Sotoudeh Stanford University Link to publication | ||
10:30 - 12:00 | |||
10:30 30mTalk | Rewriting Logic Semantics and Symbolic Analysis for Parametric Timed AutomataIn Person FTSCS Jaime Arias CNRS; LIPN; Université Sorbonne Paris Nord, Kyungmin Bae POSTECH, Carlos Olarte CNRS; LIPN; Université Sorbonne Paris Nord, Peter Ölveczky University of Oslo, Laure Petrucci CNRS; LIPN; Université Sorbonne Paris Nord, Fredrik Rømming University of Oslo DOI | ||
11:00 30mTalk | Q: A Sound Verification Framework for Statecharts and Their ImplementationsIn Person FTSCS Samuel D. Pollard Sandia National Laboratories, Robert C. Armstrong Sandia National Laboratories, Jon Aytac Sandia National Laboratories, John Bender Sandia National Laboratories, Geoffrey C. Hulette Sandia National Laboratories, Raheel S. Mahmood Sandia National Laboratories, Karla Morris Sandia National Laboratories, Blake C. Rawlings Sandia National Laboratories DOI | ||
11:30 30mTalk | strategFTO: Untimed Control for Timed OpacityIn Person FTSCS Étienne André Université Sorbonne Paris Nord; LIPN; CNRS, Shapagat Bolat Université de Lorraine; CNRS; Inria; LORIA, Engel Lefaucheux Université de Lorraine; CNRS; Inria; LORIA, Dylan Marinho Université de Lorraine; CNRS; Inria; LORIA DOI | ||
12:00 - 13:30 | |||
12:00 90mLunch | Lunch Catering and Social Events | ||
13:30 - 15:00 | |||
13:30 10mTalk | Chair's Welcome and Most Notable Paper Award DLS | ||
13:40 40mTalk | Invited Talk: A decade of Self-Optimizing Interpreters in GraalVMVirtual DLS Christian Wimmer Oracle Labs | ||
14:20 40mTalk | Invited Talk: Live Programming over TCP? Bringing Squeak/Smalltalk Liveness to Godot via React/SVirtual DLS Tom Beckmann University of Potsdam; Hasso Plattner Institute, Leonard Geier University of Potsdam; Hasso Plattner Institute, Robert Hirschfeld University of Potsdam; Hasso Plattner Institute | ||
13:30 - 15:00 | SAS Papers 1COVID Time Papers In Person at Lecture Theatre 2 Chair(s): Roberto Giacobazzi University of Verona | ||
13:30 30mTalk | Abstract Neural Networks COVID Time Papers In Person Link to publication DOI | ||
14:00 30mTalk | Reduced Products of Abstract Domains for Fairness Certification of Neural Networks COVID Time Papers In Person Denis Mazzucato INRIA & École Normale Supérieure, Caterina Urban Inria & École Normale Supérieure | Université PSL Link to publication DOI | ||
14:30 30mTalk | Static analysis of ReLU neural networks with tropical polyhedra COVID Time Papers In Person Eric Goubault Ecole Polytechnique, Sebastien Palumby Ecole Polytechnique, Sylvie Putot École Polytechnique, Louis Rustenholz Universidad Politécnica de Madrid (UPM) and IMDEA Software Institute, Sriram Sankaranarayanan University of Colorado, Boulder Link to publication DOI | ||
13:30 - 15:00 | Session 7. Grammars, Parsing and TheorySLE at Seminar Room G007 Chair(s): Marjan Mernik University of Maribor | ||
13:30 40mTalk | The Semantics of PluralsVirtualSLE Body of Knowledge SLE DOI | ||
14:10 24mTalk | Gradual Grammars: Syntax in Levels and LocalesVirtualResearch Paper SLE DOI Pre-print Media Attached | ||
14:34 24mTalk | Property Probes: Source Code Based Exploration of Program Analysis ResultsIncludes DemoResearch PaperIn Person SLE Anton Risberg Alaküla Lund University, Görel Hedin Lund University, Niklas Fors Lund University, Adrian Pop Linköping University DOI Media Attached File Attached | ||
13:30 - 15:00 | Session 3PLMW at Seminar Room G080 Chair(s): Youyou Cong Tokyo Institute of Technology, James Tizard University of Auckland | ||
13:30 90mPanel | PhD Life PanelPanel PLMW Chiaki Ishio Ochanomizu University, Kiran Gopinathan National University of Singapore, Mae Milano University of California at Berkeley | ||
13:30 - 15:00 | |||
13:30 22mTalk | Model-Driven IoT App Stores: Deploying Customizable Software Products to Heterogeneous DevicesIn Person GPCE Arvid Butting Software Engineering, RWTH Aachen University, Jörg Christian Kirchhof RWTH Aachen University, Anno Kleiss RWTH Aachen University, Judith Michael RWTH Aachen University, Radoslav Orlov RWTH Aachen University, Bernhard Rumpe RWTH Aachen University DOI Pre-print | ||
13:52 22mTalk | Language Support for Refactorability Decay PreventionIn Person GPCE DOI | ||
14:15 22mTalk | Preserving Consistency of Interrelated Models during View-Based Evolution of Variable SystemsVirtual GPCE Sofia Ananieva FZI Research Center for Information Technology, Thomas Kühn Karlsruhe Institute of Technology, Ralf Reussner KIT DOI | ||
14:37 23mTalk | Generic Solution-Space Sampling for Multi-domain Product LinesVirtual GPCE Marc Hentze Volkswagen, Tobias Pett TU Braunschweig, Chico Sundermann University of Ulm, Sebastian Krieter University of Ulm, Thomas Thüm University of Ulm, Ina Schaefer KIT DOI | ||
13:30 - 15:00 | |||
13:30 30mTalk | FLOREnce: A Hybrid Logic-Functional Reactive Programming Language REBLS Louise Van Verre Vrije Universiteit Brussel, Humberto Rodriguez Avila Vrije Universiteit Brussel, Jens Nicolay Vrije Universiteit Brussel, Wolfgang De Meuter Vrije Universiteit Brussel DOI | ||
14:00 30mTalk | Distributed Persistent Signals: Architecture and Implementation REBLS DOI | ||
14:30 30mTalk | Reactive Programming on the Bare Metal: A Formal Model for a Low-Level Reactive Virtual Machine REBLS Bjarno Oeyen Vrije Universiteit Brussel, Joeri De Koster Vrije Universiteit Brussel, Wolfgang De Meuter Vrije Universiteit Brussel DOI Pre-print | ||
13:30 - 15:00 | |||
13:30 30mTalk | Static Information Flow Control Made Simple HATRA Link to publication | ||
14:00 60mMeeting | Discussion HATRA Michael Coblenz University of California, San Diego, Jonathan Aldrich Carnegie Mellon University, Luke Church University of Cambridge | Lund University | Lark Systems | ||
13:30 - 15:00 | |||
13:30 30mTalk | Symbolic Reachability Analysis of Distributed Systems using Narrowing and Heuristic SearchIn Person FTSCS DOI | ||
14:00 30mTalk | Proving Memory Access Violations in Isabelle/HOLIn Person FTSCS Sharar Ahmadi University of Surrey, Brijesh Dongol University of Surrey, Matt Griffin University of Surrey DOI | ||
14:30 30mTalk | Bounded Model Checking of PLC ST Programs using Rewriting Modulo SMTIn Person FTSCS DOI | ||
15:00 - 15:30 | |||
15:00 30mCoffee break | Coffee break Catering and Social Events | ||
15:30 - 17:00 | |||
15:30 30mTalk | Execution vs. Parse-Based Language Servers: Tradeoffs and Opportunities for Language-Agnostic Tooling for Dynamic Languages DLS Stefan Marr University of Kent, Humphrey Burchell University of Kent, Fabio Niephaus Oracle Labs, Potsdam DOI Pre-print | ||
16:00 30mTalk | Who You Gonna Call: Analyzing the Run-time Call-Site Behavior of Ruby Applications DLS Sophie Kaleba University of Kent, Octave Larose University of Kent, Richard Jones University of Kent, Stefan Marr University of Kent DOI Pre-print | ||
16:30 30mTalk | Dynamic Pattern Matching with Python DLS Tobias Kohn University of Cambridge, UK, Guido van Rossum Python Software Foundation, Brandt Bucher Research Affiliates, LLC, Talin , Ivan Levkivskyi Dropbox Ireland DOI Pre-print | ||
15:30 - 17:00 | |||
15:30 30mTalk | Compositional Verification of Smart Contracts Through Communication Abstraction COVID Time Papers In Person Scott Wesley University of Waterloo, Canada, Maria Christakis MPI-SWS, Jorge A. Navas Certora, inc., Richard Trefler University of Waterloo, Canada, Valentin Wüstholz ConsenSys, Arie Gurfinkel University of Waterloo Link to publication DOI | ||
16:30 30mTalk | Interprocedural Shape Analysis Using Separation Logic-Based Transformer Summaries COVID Time Papers In Person Hugo Illous CEA & INRIA / ENS Paris, Matthieu Lemerre CEA LIST, France, Xavier Rival INRIA/CNRS/ENS Paris Link to publication DOI | ||
15:30 - 17:00 | Session 4PLMW at Seminar Room G080 Chair(s): Youyou Cong Tokyo Institute of Technology, James Tizard University of Auckland | ||
15:30 90mPanel | Post PhD Careers PanelPanel PLMW Jun Kato National Institute of Advanced Industrial Science and Technology (AIST), Lola Burgueño University of Malaga, Steve Blackburn Google and Australian National University, Tony Hosking Australian National University | ||
15:30 - 17:00 | |||
15:30 22mTalk | A Modern C++ Point of View of Programming in Image ProcessingVirtual GPCE Michaël ROYNARD EPITA Research Laboratory, Edwin Carlinet EPITA Research Laboratory, Thierry Géraud EPITA Research Laboratory DOI | ||
15:52 22mTalk | The Cost of Dynamism in Static Languages for Image ProcessingIn Person GPCE Baptiste Esteban EPITA Research Laboratory, Edwin Carlinet EPITA Research Laboratory, Guillaume Tochon EPITA Research Laboratory, Didier Verna EPITA Research Laboratory DOI | ||
16:15 22mTalk | A Model-Driven Generative Self Play-Based Toolchain for Developing Games and PlayersIn Person GPCE Evgeny Kusmenko RWTH Aachen University, Maximilian Münker RWTH Aachen University, Matthias Nadenau RWTH Aachen University, Bernhard Rumpe RWTH Aachen University DOI | ||
16:37 22mTalk | Dynamic Replanning of Multi-drone Missions using Dynamic Forward SlicingIn Person GPCE DOI | ||
15:30 - 17:30 | |||
15:30 30mTalk | Synchronous Programming and Refinement Types in Robotics: From Verification to ImplementationIn Person FTSCS Jiawei Chen University of Michigan at Ann Arbor, José Luiz Vargas de Mendonça University of Michigan at Ann Arbor, Shayan Jalili University of Michigan at Ann Arbor, Bereket Shimels Ayele Addis Ababa Institute of Technology, Bereket Ngussie Bekele Addis Ababa Institute of Technology, Zhemin Qu University of Michigan at Ann Arbor, Pranjal Sharma University of Michigan at Ann Arbor, Tigist Shiferaw Addis Ababa Institute of Technology, Yicheng Zhang University of Michigan at Ann Arbor, Jean-Baptiste Jeannin University of Michigan at Ann Arbor DOI | ||
16:00 30mTalk | Formal Probabilistic Risk Assessment of a Nuclear Power PlantVirtual FTSCS DOI | ||
16:30 30mTalk | Modelling a Blockchain for Smart Contract Verification using DeepSEAIn Person FTSCS DOI | ||
17:00 30mTalk | Towards a Formalization of the Active Corner Method for Collision Avoidance in PVSIn Person FTSCS | ||
16:58 - 17:10 | SLE ClosingSLE at Seminar Room G007 Chair(s): Lola Burgueño University of Malaga, Walter Cazzola Università degli Studi di Milano | ||
16:58 12mDay closing | SLE Closing SLE | ||
Thu 8 DecDisplayed time zone: Auckland, Wellington change
Thu 8 Dec
Displayed time zone: Auckland, Wellington change
08:45 - 09:00 | Opening and WelcomeOpening and Welcome at AMRF Auditorium Chair(s): Kelly Blincoe University of Auckland, Alex Potanin Australian National University | ||
09:00 - 10:00 | |||
09:00 60mKeynote | Myths and Mythconceptions: What does it mean to be a programming language, anyhow?Keynote Keynotes DOI | ||
10:00 - 10:30 | |||
10:00 30mCoffee break | Coffee break Catering and Social Events | ||
10:30 - 12:00 | |||
10:30 30mTalk | A Fast In-Place Interpreter for WebAssembly OOPSLA Ben L. Titzer Carnegie Mellon University DOI | ||
11:00 30mTalk | Optimal Heap Limits for Reducing Browser Memory Use OOPSLA Marisa Kirisame University of Utah, Pranav Shenoy University of Utah, Pavel Panchekha University of Utah DOI | ||
11:30 30mTalk | The Road Not Taken: Exploring Alias Analysis Based Optimizations Missed by the Compiler OOPSLA DOI | ||
10:30 - 12:00 | |||
10:30 30mResearch paper | Complexity-guided container replacement synthesis OOPSLA Chengpeng Wang Hong Kong University of Science and Technology, Peisen Yao Hong Kong University of Science and Technology, Wensheng Tang Hong Kong University of Science and Technology, Qingkai Shi Ant Group, Charles Zhang Hong Kong University of Science and Technology DOI | ||
11:00 30mTalk | Katara: Synthesizing CRDTs with Verified Lifting OOPSLA Shadaj Laddad University of California at Berkeley, Conor Power University of California at Berkeley, Mae Milano University of California at Berkeley, Alvin Cheung University of California at Berkeley, Joseph M. Hellerstein University of California at Berkeley DOI | ||
11:30 30mTalk | Specification-Guided Component-Based Synthesis from Effectful Libraries OOPSLA DOI | ||
10:30 - 12:00 | |||
10:30 30mResearch paper | C to checked C by 3c OOPSLA Aravind Machiry Purdue University, John Kastner Amazon, Matt McCutchen , Aaron Eline Amazon, Kyle Headley Amazon, MIchael Hicks Amazon DOI | ||
11:00 30mTalk | Solo: A Lightweight Static Analysis for Differential Privacy OOPSLA DOI | ||
11:30 30mTalk | MLstruct: Principal Type Inference in a Boolean Algebra of Structural Types OOPSLA Lionel Parreaux Hong Kong University of Science and Technology, Chun Yin Chau The Hong Kong University of Science and Technology DOI Pre-print Media Attached File Attached | ||
10:30 - 12:30 | Session 1Onward! Essays at Seminar Room G100 Chair(s): Jeremy Singer University of Glasgow We are aiming for 25 min talks with 15 min discussion, for each essay. We want to encourage questions, conversation, maybe even arguments! | ||
10:30 40mTalk | Relentless Repairability or Reckless Reuse: Whether or Not to Rebuild a Concern with Your Familiar Tools and MaterialsIn Person Onward! Essays Marcel Taeumel University of Potsdam; Hasso Plattner Institute, Robert Hirschfeld University of Potsdam; Hasso Plattner Institute Link to publication DOI Pre-print | ||
11:10 40mTalk | Conferences & Остраннeние: Shortchanging Topos and OurselvesVirtual Onward! Essays Link to publication DOI | ||
11:50 40mTalk | What Object-Oriented Programming Was Supposed to Be: Two Grumpy Old Guys’ Take on Object-Oriented ProgrammingIn Person Onward! Essays Link to publication DOI | ||
10:30 - 12:00 | ICFP and SASCOVID Time Papers In Person at Seminar Room LG004 Chair(s): Peter Thiemann University of Freiburg, Germany | ||
10:30 30mTalk | Composing and decomposing op-based CRDTs with semidirect products COVID Time Papers In Person Matthew Weidner Carnegie Mellon University, Heather Miller Carnegie Mellon University, USA, Christopher Meiklejohn Carnegie Mellon University Link to publication DOI | ||
11:00 30mTalk | Improving Thread-Modular Abstract Interpretation COVID Time Papers In Person Michael Schwarz Technische Universität München, Simmo Saan University of Tartu, Estonia, Helmut Seidl Technische Universität München, Kalmer Apinis University of Tartu, Estonia, Julian Erhard Technical University of Munich, Vesal Vojdani University of Tartu Link to publication DOI | ||
11:30 30mTalk | Static Analysis of Endian Portability by Abstract InterpretationVirtual COVID Time Papers In Person David Delmas Airbus & Sorbonne Université, Abdelraouf Ouadjaout Sorbonne Université, Antoine Miné Sorbonne Université Link to publication DOI | ||
12:00 - 13:30 | |||
12:00 90mLunch | Lunch Catering and Social Events | ||
13:45 - 14:00 | |||
13:45 15mAwards | SPLASH AwardsAwards Awards | ||
14:00 - 15:00 | |||
14:00 60mKeynote | The State Of Debugging in 2022KeynoteSupported by Google Keynotes DOI | ||
15:00 - 15:30 | |||
15:00 30mCoffee break | Coffee break Catering and Social Events | ||
15:30 - 17:00 | |||
15:30 30mTalk | A Bunch of Sessions: A Propositions-as-Sessions Interpretation of Bunched Implications in Channel-Based Concurrency OOPSLA Daniel Frumin University of Groningen, Emanuele D’Osualdo MPI-SWS, Bas van den Heuvel University of Groningen, Jorge A. Pérez University of Groningen DOI Pre-print | ||
16:00 30mTalk | A case for DOT: Theoretical Foundations for Objects with Pattern Matching and GADT-Style Reasoning OOPSLA Aleksander Boruch-Gruszecki EPFL, Radosław Waśko University of Warsaw, Yichen Xu Beijing University of Posts and Telecommunications, Lionel Parreaux Hong Kong University of Science and Technology DOI | ||
16:30 30mTalk | Coeffects for Sharing and Mutation OOPSLA Riccardo Bianchini University of Genoa, Francesco Dagnino University of Genoa, Paola Giannini University of Eastern Piedmont, Elena Zucca University of Genoa, Marco Servetto Victoria University of Wellington DOI | ||
15:30 - 17:00 | |||
15:30 30mTalk | Compilation of Dynamic Sparse Tensor Algebra OOPSLA Stephen Chou Massachusetts Institute of Technology, Saman Amarasinghe Massachusetts Institute of Technology DOI | ||
16:00 30mTalk | Incremental Type-Checking for Free: Using Scope Graphs to Derive Incremental Type-Checkers OOPSLA Aron Zwaan Delft University of Technology, Hendrik van Antwerpen Delft University of Technology, Eelco Visser Delft University of Technology DOI | ||
16:30 30mTalk | UniRec: A Unimodular-Like Framework for Nested Recursions and Loops OOPSLA Kirshanthan Sundararajah Purdue University, Charitha Saumya Purdue University, Milind Kulkarni Purdue University DOI | ||
15:30 - 17:00 | |||
15:30 30mTalk | Checking Equivalence in a Non-strict Language OOPSLA DOI | ||
16:00 30mTalk | Necessity Specifications for Robustness OOPSLA Julian Mackay Victoria University of Wellington, Susan Eisenbach Imperial College London, James Noble Research & Programming, Sophia Drossopoulou Meta and Imperial College London DOI | ||
16:30 30mResearch paper | Quantitative strongest post: a calculus for reasoning about the flow of quantitative information OOPSLA Linpeng Zhang University College London, Benjamin Lucien Kaminski Saarland University and University College London DOI | ||
15:30 - 17:00 | Session 2Onward! Essays at Seminar Room G100 Chair(s): Jonathan Aldrich Carnegie Mellon University We are aiming for 25 min talks with 15 min discussion, for each essay. We want to encourage questions, conversation, maybe even arguments! | ||
15:30 40mTalk | Ascending the Ladder to Self-Sustainability: Achieving Open Evolution in an Interactive Graphical SystemIncludes DemoIn Person Onward! Essays Link to publication DOI | ||
16:10 40mTalk | Bringing Together Configuration Research: Towards a Common GroundIn Person Onward! Essays Link to publication DOI Pre-print | ||
15:30 - 17:00 | ICFP PapersCOVID Time Papers In Person at Seminar Room LG004 Chair(s): Matthieu Lemerre CEA LIST, France | ||
15:30 30mTalk | Certifying the Synthesis of Heap-Manipulating Programs COVID Time Papers In Person Yasunari Watanabe Ahrefs Research, Kiran Gopinathan National University of Singapore, George Pîrlea National University of Singapore, Singapore, Nadia Polikarpova University of California at San Diego, Ilya Sergey National University of Singapore Link to publication DOI | ||
16:00 30mTalk | Kindly Bent to Free Us COVID Time Papers In Person Gabriel Radanne Inria, Hannes Saffrich University of Freiburg, Peter Thiemann University of Freiburg, Germany Link to publication DOI | ||
16:30 30mTalk | Stable relations and abstract interpretation of higher-order programs COVID Time Papers In Person Link to publication File Attached | ||
18:00 - 21:00 | |||
18:00 3hDinner | Dinner Catering and Social Events | ||
Fri 9 DecDisplayed time zone: Auckland, Wellington change
Fri 9 Dec
Displayed time zone: Auckland, Wellington change
09:00 - 10:00 | |||
09:00 60mKeynote | Improving the Quality of Creative Practices with Pattern LanguagesKeynote Keynotes DOI | ||
10:00 - 10:30 | |||
10:00 30mCoffee break | Coffee break Catering and Social Events | ||
10:30 - 12:00 | |||
10:30 30mTalk | A Study of Inline Assembly in Solidity Smart Contracts OOPSLA Stefanos Chaliasos Imperial College London, Arthur Gervais Imperial College London, Ben Livshits Imperial College London DOI | ||
11:00 30mResearch paper | Elipmoc: advanced decompilation of Ethereum smart contracts OOPSLA Neville Grech University of Malta, Sifis Lagouvardos University of Athens, Ilias Tsatiris University of Athens, Yannis Smaragdakis University of Athens DOI | ||
11:30 30mTalk | SigVM: Enabling Event-Driven Execution for Truly Decentralized Smart Contracts OOPSLA Zihan Zhao University of Toronto, Sidi Mohamed Beillahi University of Toronto, Ryan Song University of Toronto, Yuxi Cai University of Toronto, Andreas Veneris University of Toronto, Fan Long University of Toronto DOI | ||
10:30 - 12:00 | |||
10:30 30mTalk | Neural Architecture Search using Property Guided Synthesis OOPSLA Charles Jin Massachusetts Institute of Technology, Phitchaya Mangpo Phothilimthana Google Research, Sudip Roy Cohere.ai DOI | ||
11:00 30mTalk | Synthesizing Axiomatizations using Logic Learning OOPSLA Paul Krogmeier University of Illinois at Urbana-Champaign, Zhengyao Lin Carnegie Mellon University, Adithya Murali University of Illinois at Urbana-Champaign, P. Madhusudan University of Illinois at Urbana-Champaign DOI | ||
11:30 30mResearch paper | Synthesizing fine-grained synchronization protocols for implicit monitors OOPSLA Kostas Ferles Veridise Inc., Benjamin Sepanski The University of Texas at Austin, Rahul Krishnan University of Wisconsin-Madison, James Bornholt University of Texas at Austin, Işıl Dillig University of Texas at Austin DOI | ||
10:30 - 12:00 | |||
10:30 30mResearch paper | Le Temps des Cerises: Efficient Temporal Stack Safety on Capability Machines using Directed Capabilities OOPSLA DOI | ||
11:00 30mResearch paper | Plausible sealing for gradual parametricity OOPSLA Elizabeth Labrada University of Chile, Matías Toro University of Chile, Éric Tanter University of Chile, Dominique Devriese KU Leuven DOI | ||
11:30 30mResearch paper | Purity of an ST monad: full abstraction by semantically typed back-translation OOPSLA DOI | ||
10:30 - 12:00 | Future Programming Languages and Tools (1)Onward! Papers at Seminar Room G100 Chair(s): Jeremy Singer University of Glasgow | ||
10:30 30mTalk | Forest: Structural Code Editing with Multiple Cursors Onward! Papers DOI | ||
11:00 30mTalk | Bridging the Syntax-Semantics Gap of ProgrammingIncludes Demo Onward! Papers DOI | ||
11:30 30mTalk | Digital Crochet: Toward a Visual Language for Pattern DescriptionVirtual Onward! Papers Klara Seitz University of Potsdam; Hasso Plattner Institute, Patrick Rein University of Potsdam; Hasso Plattner Institute, Jens Lincke University of Potsdam; Hasso Plattner Institute, Robert Hirschfeld University of Potsdam; Hasso Plattner Institute DOI Pre-print | ||
10:30 - 12:00 | |||
10:30 90mPanel | Software Profession Dimensions of Diversity, Equity, and InclusionPanel Panels P: Steven D. Fraser Innoxec, R: Dennis Mancl MSWX Software Experts, C: Alex Sloley Agile Twist, C: Sally Sloley Visual Agile Management, P: Kelly Blincoe University of Auckland, P: Stéphanie Camaréna Source Transitions, P: Tanya Johnson Auror, P: Geoff Kaufman Carnegie Mellon University, P: Mahsa McCauley Auckland University of Technology, P: Sheng-Ying Pao National Tsing Hua University | ||
12:00 - 13:30 | |||
12:00 90mLunch | Lunch Catering and Social Events | ||
13:30 - 15:00 | Logic and Verification IOOPSLA at AMRF Auditorium Chair(s): Benjamin Lucien Kaminski Saarland University and University College London | ||
13:30 30mResearch paper | Finding real bugs in big programs with incorrectness logic OOPSLA Quang Loc Le University College London, Azalea Raad Imperial College London, Jules Villard Meta, Josh Berdine Meta, Derek Dreyer MPI-SWS, Peter W. O'Hearn Meta; University College London DOI | ||
14:00 30mTalk | Fractional Resources in Unbounded Separation Logic OOPSLA Thibault Dardinier ETH Zurich, Peter Müller ETH Zurich, Alexander J. Summers University of British Columbia DOI | ||
14:30 30mTalk | Proving Hypersafety Compositionally OOPSLA DOI Pre-print | ||
13:30 - 15:00 | |||
13:30 30mResearch paper | Bugs in Quantum computing platforms: an empirical study OOPSLA DOI | ||
14:00 30mTalk | Tower: Data Structures in Quantum Superposition OOPSLA Charles Yuan Massachusetts Institute of Technology, Michael Carbin Massachusetts Institute of Technology DOI | ||
14:30 30mTalk | Verified Compilation of Quantum Oracles OOPSLA Liyi Li University of Maryland, Finn Voichick University of Maryland, Kesha Hietala University of Maryland, Yuxiang Peng University of Maryland, Xiaodi Wu University of Maryland, Michael Hicks University of Maryland; Amazon DOI | ||
13:30 - 14:30 | |||
13:30 30mTalk | AnICA: Analyzing Inconsistencies in Microarchitectural Code Analyzers OOPSLA DOI | ||
14:00 30mTalk | Seq2Parse: Neurosymbolic Parse Error Repair OOPSLA Georgios Sakkas University of California at San Diego, Madeline Endres University of Michigan, Philip Guo University of California at San Diego, Westley Weimer University of Michigan, Ranjit Jhala University of California at San Diego DOI | ||
13:30 - 15:00 | Future Programming Languages and Tools (2)Onward! Papers at Seminar Room G100 Chair(s): Jeremy Singer University of Glasgow | ||
13:30 30mTalk | A Language Based on Two Relations between SymbolsIncludes Demo Onward! Papers Agustín Rafael Martínez University of Buenos Aires DOI Pre-print | ||
14:00 30mTalk | Exploring Task Equivalence for Software Engineering Practice Adaptation and Replacement Onward! Papers Diana Kirk University of Auckland DOI | ||
14:30 30mTalk | The Principles of the Flix Programming LanguageVirtual Onward! Papers Magnus Madsen Aarhus University DOI | ||
13:30 - 15:00 | Onward! Papers and EssaysCOVID Time Papers In Person at Seminar Room LG004 Chair(s): Matthew Sotoudeh Stanford University | ||
13:30 30mTalk | A Case Study in Language-Based Security: Building an I/O Library for Wyvern COVID Time Papers In Person Jennifer Fish Carnegie Mellon University, Darya Melicher Google, Jonathan Aldrich Carnegie Mellon University Link to publication DOI | ||
14:00 30mTalk | How (Not) To Write Java Pointer Analyses After 2020 COVID Time Papers In Person Manas Thakur IIT Bombay Link to publication DOI | ||
14:30 30mTalk | Putting the Semantics into Semantic Versioning COVID Time Papers In Person Patrick Lam University of Waterloo, Jens Dietrich Victoria University of Wellington, David J. Pearce ConsenSys Link to publication DOI | ||
15:00 - 15:30 | |||
15:00 30mCoffee break | Coffee break Catering and Social Events | ||
15:30 - 17:00 | |||
15:30 30mTalk | BFF: Foundational and Automated Verification of Bitfield-Manipulating Programs OOPSLA Fengmin Zhu MPI-SWS, Michael Sammler MPI-SWS, Rodolphe Lepigre MPI-SWS, Derek Dreyer MPI-SWS, Deepak Garg MPI-SWS DOI | ||
16:00 30mTalk | Compositional Virtual Timelines: Verifying Dynamic-Priority Partitions with Algorithmic Temporal Isolation OOPSLA Mengqi Liu Yale University, Zhong Shao Yale University, Hao Chen Yale University, Man-Ki Yoon Yale University, Jung-Eun Kim Yale University DOI | ||
16:30 30mResearch paper | Linear types for large-scale systems verification OOPSLA Jialin Li , Andrea Lattuada ETH Zurich, Yi Zhou Carnegie Mellon University, Jonathan Cameron Carnegie Mellon University, Jon Howell VMWare Research, Bryan Parno Carnegie Mellon University, USA, Chris Hawblitzel Microsoft Research DOI | ||
15:30 - 17:00 | |||
15:30 30mResearch paper | Effects, capabilities, and boxes: from scope-based reasoning to type-based reasoning and back OOPSLA Jonathan Immanuel Brachthäuser University of Tübingen, Philipp Schuster University of Tübingen, Edward Lee University of Waterloo, Aleksander Boruch-Gruszecki EPFL DOI | ||
16:00 30mTalk | First-class Names for Effect Handlers OOPSLA Ningning Xie University of Toronto, Youyou Cong Tokyo Institute of Technology, Kazuki Ikemori Tokyo Institute of Technology, Daan Leijen Microsoft Research DOI | ||
16:30 30mTalk | High-Level Effect Handlers in C++ OOPSLA Dan Ghica Huawei, Sam Lindley University of Edinburgh, Marcos Maronas Bravo Huawei, Maciej Piróg Huawei DOI | ||
15:30 - 17:00 | ProbabilisticOOPSLA at Seminar Room G007 Chair(s): Benjamin Lucien Kaminski Saarland University and University College London | ||
15:30 30mTalk | Semi-symbolic Inference for Efficient Streaming Probabilistic Programming OOPSLA Eric Atkinson Massachusetts Institute of Technology, Charles Yuan Massachusetts Institute of Technology, Guillaume Baudart Inria, Louis Mandel IBM Research, Michael Carbin Massachusetts Institute of Technology DOI | ||
16:00 30mTalk | Symbolic Execution for Randomized Programs OOPSLA Zachary Susag Cornell University, Sumit Lahiri IIT Kanpur, Justin Hsu Cornell University, Subhajit Roy IIT Kanpur DOI | ||
16:30 30mTalk | This Is the Moment for Probabilistic Loops OOPSLA DOI | ||
15:30 - 17:00 | Program Synthesis, Testing and AdaptationOnward! Papers at Seminar Room G100 Chair(s): Stefan Marr University of Kent | ||
15:30 30mTalk | Derivations with Holes for Concept-Based Program SynthesisIncludes Demo Onward! Papers João Costa Seco NOVA-LINCS; Nova University of Lisbon, Jonathan Aldrich Carnegie Mellon University, Luís Carvalho NOVA-LINCS; Nova University of Lisbon, Bernardo Toninho NOVA-LINCS; Nova University of Lisbon, Carla Ferreira NOVA-LINCS; Nova University of Lisbon DOI | ||
16:00 30mTalk | Intramorphic Testing: A New Approach to the Test Oracle Problem Onward! Papers DOI | ||
16:30 30mTalk | GOAL: Supporting General and Dynamic Adaptation in Computing SystemsVirtual Onward! Papers Ahsan Pervaiz University of Chicago, Yao Hsiang Yang Rice University, Adam Duracz Rice University, Ferenc Bartha Rice University, Ryuichi Sai Rice University, Connor Imes University of Chicago, Robert Cartwright Rice University, Krishna Palem Rice University, Shan Lu University of Chicago, Henry Hoffmann University of Chicago DOI | ||
Sat 10 DecDisplayed time zone: Auckland, Wellington change
Sat 10 Dec
Displayed time zone: Auckland, Wellington change
09:00 - 10:00 | |||
09:00 60mKeynote | (I Can't Get No) VerificationKeynote Keynotes DOI | ||
10:00 - 10:30 | |||
10:00 30mCoffee break | Coffee break Catering and Social Events | ||
10:30 - 12:00 | Logic and ConcurrencyOOPSLA at AMRF Auditorium Chair(s): Mohsen Lesani University of California at Riverside | ||
10:30 30mTalk | A Concurrent Program Logic with a Future and History OOPSLA DOI | ||
11:00 30mTalk | CAAT: Consistency as a Theory OOPSLA Thomas Haas TU Braunschweig, Roland Meyer TU Braunschweig, Hernán Ponce de León Huawei Dresden Research Center DOI | ||
11:30 30mTalk | Implementing and Verifying Release-Acquire Transactional Memory in C11 OOPSLA DOI | ||
10:30 - 12:00 | |||
10:30 30mTalk | Data-Driven Lemma Synthesis for Interactive Proofs OOPSLA Aishwarya Sivaraman University of California at Los Angeles, Alex Sanchez-Stern University of Massachusetts at Amherst, Bretton Chen University of California at Los Angeles, Sorin Lerner University of California at San Diego, Todd Millstein University of California at Los Angeles DOI | ||
11:00 30mTalk | Intrinsically-Typed Definitional Interpreters à la Carte OOPSLA Cas van der Rest Delft University of Technology, Casper Bach Poulsen Delft University of Technology, Arjen Rouvoet Delft University of Technology, Eelco Visser Delft University of Technology, Peter D. Mosses Swansea University and Delft University of Technology DOI | ||
11:30 30mResearch paper | Proof transfer for fast certification of multiple approximate neural networks OOPSLA Shubham Ugare University of Illinois at Urbana-Champaign, Gagandeep Singh University of Illinois at Urbana-Champaign, Sasa Misailovic University of Illinois at Urbana-Champaign DOI | ||
10:30 - 12:00 | |||
10:30 30mTalk | Can Guided Decomposition Help End-Users Write Larger Block-Based Programs? A Mobile Robot Experiment OOPSLA Nico Ritschel University of British Columbia, Felipe Fronchetti Virginia Commonwealth University, Reid Holmes University of British Columbia, Ronald Garcia University of British Columbia, David C. Shepherd Virginia Commonwealth University DOI | ||
11:00 30mTalk | Compositional Embeddings of Domain-Specific Languages OOPSLA Yaozhu Sun University of Hong Kong, Utkarsh Dhandhania University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong DOI Pre-print | ||
11:30 30mResearch paper | Language-parametric static semantic code completion OOPSLA Daniel A. A. Pelsmaeker Delft University of Technology, Netherlands, Hendrik van Antwerpen Delft University of Technology, Casper Bach Poulsen Delft University of Technology, Eelco Visser Delft University of Technology DOI | ||
10:30 - 12:00 | Program Comprehension Tools and TechniquesOnward! Papers at Seminar Room G100 Chair(s): James Noble Research & Programming | ||
10:30 30mTalk | Contextualized Programming Language DocumentationIncludes Demo Onward! Papers Hannah Potter University of Washington, Ardi Madadi University of Washington, René Just University of Washington, Cyrus Omar University of Michigan DOI | ||
11:00 30mTalk | Competitive Debugging: Toward Contests Promoting Debugging as a Skill Onward! Papers Patrick Rein University of Potsdam; Hasso Plattner Institute, Tom Beckmann University of Potsdam; Hasso Plattner Institute, Leonard Geier University of Potsdam; Hasso Plattner Institute, Toni Mattis University of Potsdam; Hasso Plattner Institute, Robert Hirschfeld University of Potsdam; Hasso Plattner Institute DOI Pre-print | ||
11:30 30mTalk | Portals: An Extension of Dataflow Streaming for Stateful Serverless Onward! Papers Jonas Spenger KTH Royal Institute of Technology, Paris Carbone RISE Research institutes of Sweden, Philipp Haller KTH DOI | ||
12:00 - 13:30 | |||
12:00 90mLunch | Lunch Catering and Social Events | ||
13:30 - 15:00 | Testing and MaintenanceOOPSLA at AMRF Auditorium Chair(s): Işıl Dillig University of Texas at Austin | ||
13:30 30mTalk | Overwatch: Learning Patterns in Code Edit Sequences OOPSLA Yuhao Zhang University of Wisconsin-Madison, Yasharth Bajpai Microsoft, Priyanshu Gupta Microsoft, Ameya Ketkar Uber, Miltiadis Allamanis Microsoft Research, Titus Barik Microsoft, Sumit Gulwani Microsoft, Arjun Radhakrishna Microsoft, Mohammad Raza Microsoft, Gustavo Soares Microsoft, Ashish Tiwari Microsoft DOI | ||
14:00 30mTalk | Satisfiability Modulo Fuzzing: A Synergistic Combination of SMT Solving and Fuzzing OOPSLA DOI | ||
14:30 30mTalk | Synthesizing Code Quality Rules from Examples OOPSLA DOI | ||
13:30 - 15:00 | |||
13:30 30mResearch paper | C4: verified transactional objects OOPSLA Mohsen Lesani University of California at Riverside, Li-yao Xia University of Pennsylvania, Anders Kaseorg Massachusetts Institute of Technology, Christian J. Bell MIT CSAIL, Adam Chlipala Massachusetts Institute of Technology, Benjamin C. Pierce University of Pennsylvania, Steve Zdancewic University of Pennsylvania DOI | ||
14:00 30mTalk | Concurrent Size OOPSLA DOI | ||
14:30 30mTalk | Veracity: Declarative Multicore Programming with Commutativity OOPSLA Adam Chen Stevens Institute of Technology, Parisa Fathololumi Stevens Institute of Technology, Eric Koskinen Stevens Institute of Technology, Jared Pincus Stevens Institute of Technology DOI | ||
13:30 - 15:00 | |||
13:30 30mResearch paper | On incorrectness logic for Quantum programs OOPSLA Peng Yan University of Technology Sydney, Hanru Jiang Yanqi Lake Beijing Institute of Mathematical Sciences and Applications, China, Nengkun Yu Stony Brook University, USA DOI | ||
14:00 30mResearch paper | Weighted programming: a programming paradigm for specifying mathematical models OOPSLA Kevin Batz RWTH Aachen University, Adrian Gallus RWTH Aachen University, Benjamin Lucien Kaminski Saarland University and University College London, Joost-Pieter Katoen RWTH Aachen University, Tobias Winkler RWTH Aachen University DOI | ||
14:30 30mTalk | Wildcards Need Witness Protection OOPSLA Kevin Bierhoff Google DOI | ||
13:30 - 15:00 | PLDI and POPL PapersCOVID Time Papers In Person at Seminar Room LG004 Chair(s): Joxan Jaffar National University of Singapore | ||
13:30 30mTalk | PMEvo: portable inference of port mappings for out-of-order processors by evolutionary optimization COVID Time Papers In Person Link to publication DOI | ||
14:00 30mTalk | Software Model-Checking as Cyclic-Proof Search COVID Time Papers In Person Link to publication DOI | ||
14:30 30mTalk | SolType: Refinement Types for Arithmetic Overflow in Solidity COVID Time Papers In Person Bryan Tan , Benjamin Mariano The University of Texas at Austin, Texas, USA, Shuvendu K. Lahiri Microsoft Research, Işıl Dillig University of Texas at Austin, Yu Feng University of California at Santa Barbara Link to publication DOI | ||
15:00 - 15:30 | |||
15:00 30mCoffee break | Coffee break Catering and Social Events | ||
15:30 - 17:00 | |||
15:30 30mResearch paper | Automated transpilation of imperative to functional code using neural-guided program synthesis OOPSLA Benjamin Mariano University of Texas at Austin, Yanju Chen University of California at Santa Barbara, Yu Feng University of California at Santa Barbara, Greg Durrett University of Texas at Austin, Işıl Dillig University of Texas at Austin DOI | ||
16:00 30mTalk | Synthesis-Powered Optimization of Smart Contracts via Data Type Refactoring OOPSLA Yanju Chen University of California at Santa Barbara, Yuepeng Wang Simon Fraser University, Maruth Goyal University of Texas at Austin, James Dong Stanford University, Yu Feng University of California at Santa Barbara, Işıl Dillig University of Texas at Austin DOI | ||
16:30 30mTalk | Synthesizing Abstract Transformers OOPSLA Pankaj Kumar Kalita IIT Kanpur, Sujit Kumar Muduli IIT Kanpur, Loris D'Antoni University of Wisconsin-Madison, Thomas Reps University of Wisconsin-Madison, Subhajit Roy IIT Kanpur DOI | ||
15:30 - 17:00 | PLDI PapersCOVID Time Papers In Person at Seminar Room LG004 Chair(s): Jonathan Aldrich Carnegie Mellon University | ||
15:30 30mTalk | Behavioral simulation for smart contracts COVID Time Papers In Person Sidi Mohamed Beillahi University of Toronto, Gabriela Ciocarlie University of Texas at San Antonio, Michael Emmi Amazon Web Services, Constantin Enea Ecole Polytechnique / LIX / CNRS Link to publication DOI | ||
16:00 30mTalk | Ethainter: A Smart Contract Security Analyzer for Composite Vulnerabilities COVID Time Papers In Person Lexi Brent International Computer Science Institute, USA / University of Sydney, Australia, Neville Grech University of Malta, Sifis Lagouvardos University of Athens, Bernhard Scholz The University of Sydney, Yannis Smaragdakis University of Athens Link to publication DOI | ||
16:30 30mTalk | Practical Smart Contract Sharding with Ownership and Commutativity Analysis COVID Time Papers In Person George Pîrlea National University of Singapore, Singapore, Amrit Kumar Zilliqa Research, Ilya Sergey National University of Singapore Link to publication DOI | ||
16:00 - 17:00 | |||
16:00 30mTalk | Indexing the Extended Dyck-CFL Reachability for Context-Sensitive Program AnalysisVirtual OOPSLA Qingkai Shi Ant Group, Yongchao WANG Hong Kong University of Science and Technology, Peisen Yao Hong Kong University of Science and Technology, Charles Zhang Hong Kong University of Science and Technology DOI | ||
16:30 30mTalk | The Essence of Online Data Processing OOPSLA DOI | ||