Sources of Unsoundness in Verification When: Tue 6 Dec 2022 13:30 - 13:50 People: Jaymon Furniss

… We looked at three different verifiers for object-oriented program veri fication, Gobra, KeY, and Dafny. We show that all three can be made to prove false … much difficulty and that this is possibly common throughout all OO verifiers. …

APLAS When: Mon 5 Dec 2022 16:00 - 16:30 People: Xu Xue, Bruno C. d. S. Oliveira, Ningning Xie

… }. Nevertheless no previous calculus supports all those features at once. In this paper … all the features, and is proven to be type sound. However, the semantics … of overloading are forbidden, but all other features are supported. The main challenge …

Formal Techniques for Safety-Critical Systems When: Wed 7 Dec 2022 16:00 - 16:30 People: Mohamed Abdelghany, Sofiene Tahar

… ) dependability modeling techniques are typically used to associate all possible … formally determine all possible classes of accident events that can occur …

Sources of Unsoundness in Verification When: Tue 6 Dec 2022 11:15 - 12:00 People: Yannick Forster

… all aspects of Coq’s type theory in MetaCoq. In the future, we hope …

Programming Abstractions and Interactive Notations, Tools, and Environments When: Mon 5 Dec 2022 11:45 - 12:00 People: Michael Homer

… stack to identify where values are produced and consumed. All …

Programming Abstractions and Interactive Notations, Tools, and Environments When: Mon 5 Dec 2022 11:15 - 11:30 People: Alexis De Meo, Michael Homer

… and their implications for all parties, eliminating repetition while increasing …

Virtual Machines and Language Implementations When: Mon 5 Dec 2022 11:35 - 12:00 People: Dave Mason

… -Oriented languages. By sharing, all could benefit from each others’ research …

APLAS When: Mon 5 Dec 2022 13:30 - 14:00 People: Robert Dickerson, Qianchuan Ye, Michael K. Zhang, Benjamin Delaware

… that \emph{all} runs of a collection of programs do not violate a specified …

Live Programming When: Tue 6 Dec 2022 16:10 - 16:30 People: Michael Homer

… We present an approach to live programming in a two-dimensional grid of functions where all intermediate values are always visible and tangible. Arguments are chosen through selecting values, and indicated by layout, so all interaction …

APLAS When: Mon 5 Dec 2022 15:30 - 16:00 People: Patricia Johann, Pierre Cagne

… It is well-known that GADTs do not admit standard map functions of the kind supported by ADTs and nested types. In addition, standard map functions are insufficient to distribute their data-changing argument functions over all …

Formal Techniques for Safety-Critical Systems When: Wed 7 Dec 2022 14:00 - 14:30 People: Sharar Ahmadi, Brijesh Dongol, Matt Griffin

… generate a set of programs covering all possible
cases in which an assembly-level …

APLAS When: Mon 5 Dec 2022 16:30 - 17:00 People: Yaoda Zhou, Bruno C. d. S. Oliveira, Andong Fan

… of our disjointness definition. All the proofs are mechanized in the Coq theorem …

Live Programming When: Tue 6 Dec 2022 14:10 - 14:30 People: Yoshiki Ohshima, Aran Lunzer, Vanessa Freudenberg, Brian Upton, David Smith

… . On each change of the application code, you need to load a new build onto all …

GPCE When: Tue 6 Dec 2022 15:52 - 16:15 People: Chiaki Ishio, Kenichi Asai

… for all the four control operators. Following Danvy and Filinski’s approach, we … and that the calculus with all the four control operators is terminating. Furthermore, we show …

GPCE When: Wed 7 Dec 2022 14:37 - 15:00 People: Marc Hentze, Tobias Pett, Chico Sundermann, Sebastian Krieter, Thomas Thüm, Ina Schaefer

… all potential error sources missed by problem-space sampling. …

SAS When: Tue 6 Dec 2022 16:00 - 16:30 People: Sidi Mohamed Beillahi, Ahmed Bouajjani, Constantin Enea, Shuvendu K. Lahiri

… introducing data races. We investigate the delay complexity of enumerating all data race …

SLE 2022 When: Tue 6 Dec 2022 11:42 - 11:57 People: Jos Warmer, Anneke Kleppe

… to be the one tool that can meet all these requirements. Instead the architecture …

SAS When: Wed 7 Dec 2022 11:00 - 11:30 People: Aditya Anand, Manas Thakur

… transform a general whole-program analysis (that resolves dependencies across all … partial analysis that addresses all these points, based on the classic theory …

SLE 2022 When: Wed 7 Dec 2022 14:10 - 14:34 People: Tijs van der Storm, Felienne Hermans

… Programming language implementations are often one-size-fits-all. Irrespective … a single, canonical syntax for all language users. Whereas professional software developers might be willing to learn a programming language all in one go, this might …

GPCE When: Wed 7 Dec 2022 10:52 - 11:15 People: Guilherme Espada, Leon Ingelse, Paulo Canelas, Pedro Barbosa, Alcides Fonseca

… while using the host language type-system to take advantage of all the existing …

SAS When: Wed 7 Dec 2022 11:30 - 12:00 People: Abu Naser Masud

… of 31.03 in all benchmarks and a maximum speedup of 35.29 than the best state …

SLE 2022 When: Wed 7 Dec 2022 15:30 - 15:54 People: Matteo Cimini

… the type safety of all these languages, when the correct code for substitution lemmas …

SLE 2022 When: Tue 6 Dec 2022 10:54 - 11:18 People: Tom Beckmann, Patrick Rein, Toni Mattis, Robert Hirschfeld

… Creating structured editors, which maintain a valid syntax tree at all times rather than allowing to edit program text, is typically a time consuming task. Recent work has investigated the use of existing general-purpose language grammars …

SLE 2022 When: Tue 6 Dec 2022 14:35 - 14:59 People: Faezeh Khorram, Erwan Bousse, Antonio Garmendia, Jean-Marie Mottu, Gerson Sunyé, Manuel Wimmer

… meaningful coverage matrices for all investigated DSLs and models. The applied fault …

OOPSLA When: Sat 10 Dec 2022 11:30 - 12:00 People: Daniel A. A. Pelsmaeker, Hendrik van Antwerpen, Casper Bach Poulsen, Eelco Visser

… . It should be complete, such that it proposes all valid fragments so that code completion can be used to construct all programs. To realize soundness and completeness …

OOPSLA When: Fri 9 Dec 2022 11:30 - 12:00 People: Kostas Ferles, Benjamin Sepanski, Rahul Krishnan, James Bornholt, Işıl Dillig

… A monitor is a widely-used concurrent programming abstraction that encapsulates all shared state between threads. Monitors can be classified as being either … monitors from an implicit specification, but prior work does not exploit all …

Onward! Papers When: Fri 9 Dec 2022 13:30 - 14:00 People: Agustín Rafael Martínez

… We present a language with all the power of abstraction and the simplicity of two fundamental relations: substitution and categorization. With a graphic symbol representing each one of them, we created a playful visual programming …

Onward! Papers When: Sat 10 Dec 2022 11:30 - 12:00 People: Jonas Spenger, Paris Carbone, Philipp Haller

… introduce all programming model invariants and the corresponding system methods used …

Student Research Competition When: Mon 5 Dec 2022 18:00 - 20:00Wed 7 Dec 2022 18:30 - 18:45 People: Litao Zhou

… of the rich assertion language, not all reduced proof goals can be automatically …

COVID Time Papers In Person When: Mon 5 Dec 2022 14:00 - 14:30 People: Phillip van Heerden, Moeketsi Raselimo, Konstantinos (Kostis) Sagonas, Bernd Fischer

… ) all test suites constructed systematically following different grammar … suites performs as well or better than the instructor’s test suite in all aspects … of triggered semantic errors and detected failures and crashes. Moreover, all failing …

Posters When: Mon 5 Dec 2022 18:00 - 20:00 People: Daniel Britten, Vilhelm Sjöberg, Steve Reeves

… not relying on a central authority. All that is required to be trusted beyond …

COVID Time Papers In Person When: Mon 5 Dec 2022 13:30 - 14:00 People: Moeketsi Raselimo, Bernd Fischer

… We describe the first approach to automatically repair bugs in context-free grammars: given a grammar that fails some tests in a given test suite, we iteratively and gradually transform the grammar until it passes all tests. Our core idea …

OOPSLA When: Fri 9 Dec 2022 16:00 - 16:30 People: Zachary Susag, Sumit Lahiri, Justin Hsu, Subhajit Roy

… quantify over all possible inputs. Our technique augments standard symbolic …

Onward! Essays When: Thu 8 Dec 2022 11:10 - 11:50 People: Richard P. Gabriel, Jenny Quillien

… about conference design of all types. Cutting access to these deeper physical …

OOPSLA When: Fri 9 Dec 2022 15:30 - 16:00 People: Jonathan Immanuel Brachthäuser, Philipp Schuster, Edward Lee, Aleksander Boruch-Gruszecki

… that capabilities and effects can be reconciled harmoniously. By assuming that all functions …

Onward! Papers When: Fri 9 Dec 2022 11:30 - 12:00 People: Klara Seitz, Patrick Rein, Jens Lincke, Robert Hirschfeld

… or ambiguous instructions after all.

We propose a first visual, domain-specific …

OOPSLA When: Sat 10 Dec 2022 11:00 - 11:30 People: Thomas Haas, Roland Meyer, Hernán Ponce de León

… We propose a family of logical theories for capturing an abstract notion of consistency and show how to build a generic and efficient theory solver that works for all members in the family.
The theories can be used to model the influence …

V-OOPSLA When: Wed 30 Nov 2022 21:15 - 21:30 People: Hongming Liu, Hongfei Fu, zhiyong yu, Jiaxin Song, Guoqiang Li

… to a parallel processing that divides the invariant-generation task for all program … the execution time for all program locations.
Hence, our approach constitutes …

OOPSLA When: Sat 10 Dec 2022 10:30 - 11:00 People: Nico Ritschel, Felipe Fronchetti, Reid Holmes, Ronald Garcia, David C. Shepherd

… functions, but does not require decomposition. We found that while almost all users … decomposition strategy fits all domains, we believe that similar domain-specific sub …

OOPSLA When: Sat 10 Dec 2022 11:30 - 12:00 People: Shubham Ugare, Gagandeep Singh, Sasa Misailovic

… for the robustness verification of neural networks, a major limitation of almost all state …, and the robustness of all the networks needs to be verified efficiently.

We present FANC …

COVID Time Papers In Person When: Fri 9 Dec 2022 11:30 - 12:00 People: Yaoda Zhou, Bruno C. d. S. Oliveira, Jinxu Zhao

… that two recursive types are subtypes if all their finite unfoldings … involving recursive types. All results are mechanically formalized in the Coq …

OOPSLA When: Fri 9 Dec 2022 14:00 - 14:30 People: Charles Yuan, Michael Carbin

… all recursion using classical parameters as is necessary for a program …. We provide the first executable implementation of sets that satisfies all three …

SPLASH-E When: Mon 5 Dec 2022 16:00 - 16:30 People: Braxton Hall, Elisa Baniassad

… ' suites over all generated clones.

We employed Mutation Analysis to assess …

OOPSLA People: Tristan Dyer, Tim Nelson, Kathi Fisler, Shriram Krishnamurthi

… , and whether all instances must actually satisfy the input constraints. Using both …

OOPSLA When: Thu 8 Dec 2022 10:30 - 11:00 People: Aravind Machiry, John Kastner, Matt McCutchen, Aaron Eline, Kyle Headley, MIchael Hicks

… necessarily all at once, so that safety retrofitting can be incremental. This paper …

COVID Time Papers In Person When: Wed 7 Dec 2022 15:30 - 16:00 People: Scott Wesley, Maria Christakis, Jorge A. Navas, Richard Trefler, Valentin Wüstholz, Arie Gurfinkel

… Solidity smart contracts are programs that manage up to 2^160 users on a blockchain. Verifying a smart contract relative to all users is intractable due to state explosion. Existing solutions either restrict the number of users to under …

V-OOPSLA When: Wed 30 Nov 2022 22:00 - 22:15 People: Rohan Bavishi, Harshit Joshi, José Pablo Cambronero, Anna Fariha, Sumit Gulwani, Vu Le, Ivan Radiček, Ashish Tiwari

… all baselines. We release these benchmarks to encourage subsequent work in low …

OOPSLA When: Fri 9 Dec 2022 16:00 - 16:30 People: Mengqi Liu, Zhong Shao, Hao Chen, Man-Ki Yoon, Jung-Eun Kim

… . All the proofs are mechanized in Coq. …

OOPSLA When: Sat 10 Dec 2022 14:00 - 14:30 People: Gal Sela, Erez Petrank

… structure to count the elements, or acquiring one global lock in all update …

V-OOPSLA When: Wed 30 Nov 2022 04:30 - 04:45 People: Abel Nieto, Léon Gondelman, Alban Reynaud, Amin Timany, Lars Birkedal

… Operation-based Conflict-free Replicated Data Types (op-based CRDTs) are a family of distributed data structures where all operations are designed to commute, so that replica states eventually converge.
Additionally, op-based CRDTs …

Onward! Papers When: Sat 10 Dec 2022 11:00 - 11:30 People: Patrick Rein, Tom Beckmann, Leonard Geier, Toni Mattis, Robert Hirschfeld

… approaches, and that the format was enjoyable and engaging for all participants.
We …

OOPSLA When: Fri 9 Dec 2022 10:30 - 11:00 People: Aina Linn Georges, Alix Trieu, Lars Birkedal

… and frame lifetimes to a base capability machine. All results have been mechanized …

OOPSLA When: Fri 9 Dec 2022 11:00 - 11:30 People: Neville Grech, Sifis Lagouvardos, Ilias Tsatiris, Yannis Smaragdakis

… improves over all notable past decompilers, including its predecessor, Gigahorse …

OOPSLA When: Fri 9 Dec 2022 11:00 - 11:30 People: Elizabeth Labrada, Matías Toro, Éric Tanter, Dominique Devriese

… that are not subject to graduality guarantees. Furthermore, all current proposals rely …

OOPSLA When: Thu 8 Dec 2022 15:30 - 16:00 People: Stephen Chou, Saman Amarasinghe

… , including all the ones named above as well as many more. We then describe how, given …

OOPSLA People: Joshua Hoeflich, Robert Bruce Findler, Manuel Serrano

… of the language can be surprisingly important. Best of all, it also revealed a few …

OOPSLA When: Fri 9 Dec 2022 14:00 - 14:30 People: Thibault Dardinier, Peter Müller, Alexander J. Summers

… whether distributivity and combinability hold for all assertions …

V-OOPSLA When: Wed 30 Nov 2022 21:00 - 21:15 People: Yuxiang Lei, Yulei Sui, Shuo Ding, Qirun Zhang

… .

This paper proposes a scalable yet precision-preserving approach to all …

Workshops People: Jan Bessai, Marco Servetto

… this would be greatly beneficial not only because it will help all of us to iron out …

Panels When: Fri 9 Dec 2022 10:30 - 12:00 People: Steven D. Fraser, Dennis Mancl, Alex Sloley, Sally Sloley, Kelly Blincoe, Stéphanie Camaréna, Tanya Johnson, Geoff Kaufman, Mahsa McCauley, Sheng-Ying Pao

… principles and their adoption remain relevant to all. This Systems, Programming …