Search events for 'all'
Proving False in Object Oriented Verification Programs by Exploiting Non-Termination
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. …
Applicative Intersection Types
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 Probabilistic Risk Assessment of a Nuclear Power Plant
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 …
MetaCoq as a tool to prevent future unsoundness in Coq
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 …
Interleaved 2D Notation for Concatenative Programming
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 …
Domain-Specific Visual Language for Data Engineering Quality
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 …
Toward a dynamic language toolkit
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 …
RHLE: Modular Deductive Verification of Relational ∀∃ Properties
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 2D Compositional Programming
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 …
Characterizing functions mappable over GADTs
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 …
Proving Memory Access Violations in Isabelle/HOL
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 …
A Calculus with Recursive Types, Record Concatenation and Subtyping
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 and Text Editor Integration in the Croquet Microverse 3D Collaborative Construction System
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 …
Type System for Four Delimited Control Operators
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 …
Generic Solution-Space Sampling for Multi-domain Product Lines
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. …
Automated Synthesis of Asynchronizations
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 …
Freon: An Open Web Native Language Workbench
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 …
Principles of Staged Static+Dynamic Partial Analysis
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 …
Gradual Grammars: Syntax in Levels and Locales
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 …
Data Types as a More Ergonomic Frontend for Grammar-Guided Genetic Programming
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 …
Fast and incremental computation of weak control closure
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 …
Lang-n-Prove: A DSL for Language Proofs
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 …
Partial Parsing for Structured Editors
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 …
From Coverage Computation to Fault Localization: A Generic Framework for Domain-Specific Languages
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 …
Language-parametric static semantic code completion
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 …
Synthesizing fine-grained synchronization protocols for implicit monitors
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 …
A Language Based on Two Relations between Symbols
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 …
Portals: An Extension of Dataflow Streaming for Stateful Serverless
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 …
Foundationally Sound Annotation Verifier via Control Flow Splitting
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 …
Grammar-based testing for little languages: an experience report with student compilers
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 …
Provably Correct Smart Contracts: An Approach using DeepSEA
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 …
Automatic Grammar Repair
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 …
Symbolic Execution for Randomized Programs
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 …
Conferences & Остраннeние: Shortchanging Topos and Ourselves
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 …
Effects, capabilities, and boxes: from scope-based reasoning to type-based reasoning and back
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 …
Digital Crochet: Toward a Visual Language for Pattern Description
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 …
CAAT: Consistency as a Theory
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 …
Scalable Linear Invariant Generation with Farkas’ Lemma
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 …
Can Guided Decomposition Help End-Users Write Larger Block-Based Programs? A Mobile Robot Experiment
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 …
Proof transfer for fast certification of multiple approximate neural networks
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 …
Revisiting Iso-Recursive Subtyping
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 …
Tower: Data Structures in Quantum Superposition
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 …
Evaluating the Quality of Student-Written Software Tests with Curated Mutation Analysis
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 …
Applying cognitive principles to model-finding output: the positive value of negative information
OOPSLA People: Tristan Dyer, Tim Nelson, Kathi Fisler, Shriram Krishnamurthi
… , and whether all instances must actually satisfy the input constraints. Using both …
C to checked C by 3c
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 …
Compositional Verification of Smart Contracts Through Communication Abstraction
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 …
Neurosymbolic Repair for Low-Code Formula Languages
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 …
Compositional Virtual Timelines: Verifying Dynamic-Priority Partitions with Algorithmic Temporal Isolation
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. …
Concurrent Size
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 …
Modular Verification of Op-Based CRDTs in Separation Logic
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 …
Competitive Debugging: Toward Contests Promoting Debugging as a Skill
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 …
Le Temps des Cerises: Efficient Temporal Stack Safety on Capability Machines using Directed Capabilities
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 …
Elipmoc: advanced decompilation of Ethereum smart contracts
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 …
Plausible sealing for gradual parametricity
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 …
Compilation of Dynamic Sparse Tensor Algebra
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 …
Highly Illogical, Kirk: Spotting Type Mismatches in the Large Despite Broken Contracts, Unsound Types, and Too Many Linters
OOPSLA People: Joshua Hoeflich, Robert Bruce Findler, Manuel Serrano
… of the language can be surprisingly important. Best of all, it also revealed a few …
Fractional Resources in Unbounded Separation Logic
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 …
Taming Transitive Redundancy for Context-Free Language Reachability
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 …
Sources of Unsoundness in Verification (Unsound)
Workshops People: Jan Bessai, Marco Servetto
… this would be greatly beneficial not only because it will help all of us to iron out …
Software Profession Dimensions of Diversity, Equity, and Inclusion
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 …