Issue
DARTS, Volume 8, Issue 2
Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022)
-
Part of:
Volume:
DARTS, Volume 8 (ECOOP 2022)
Conference: European Conference on Object-Oriented Programming (ECOOP)
Journal: Dagstuhl Artifacts Series (DARTS)
Publication Details
- published at: 2022-06-23
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- DBLP: db/journals/darts/darts8
Access Numbers
- Detailed Access Statistics available here
-
Total Document Accesses (updated on a weekly basis):
0PDF Downloads
Documents
No documents found matching your filter selection.
Document
Front Matter
Front Matter - ECOOP 2022 Artifacts, Table of Contents, Preface, Artifact Evaluation Committee
Abstract
Front Matter - ECOOP 2022 Artifacts, Table of Contents, Preface, Artifact Evaluation Committee
Cite as
Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022). Dagstuhl Artifacts Series (DARTS), Volume 8, Issue 2, pp. 0:i-0:xii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@Article{gorla_et_al:DARTS.8.2.0,
author = {Gorla, Alessandra and Winter, Stefan},
title = {{Front Matter - ECOOP 2022 Artifacts, Table of Contents, Preface, Artifact Evaluation Committee}},
pages = {0:i--0:xii},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2022},
volume = {8},
number = {2},
editor = {Gorla, Alessandra and Winter, Stefan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DARTS.8.2.0},
URN = {urn:nbn:de:0030-drops-161982},
doi = {10.4230/DARTS.8.2.0},
annote = {Keywords: Front Matter - ECOOP 2022 Artifacts, Table of Contents, Preface, Artifact Evaluation Committee}
}
Document
Artifact
How to Take the Inverse of a Type (Artifact)
Abstract
In functional programming, regular types are a subset of algebraic data types formed from products and sums with their respective units. One can view regular types as forming a commutative semiring but where the usual axioms are isomorphisms rather than equalities. In the pearl, we show that regular types in a linear setting permit a useful notion of multiplicative inverse, allowing us to ‘divide’ one type by another. We begin with an exploration of the properties and applications of this construction, and this artifact includes examples in Haskell demonstrating its relevance to various topics from the literature including program calculation, Laurent polynomials, and derivatives of data types. Some examples from the paper require a richer setting than Haskell can offer; the artifact replays the first set of examples in Granule, while also presenting additional examples demonstrating further algebraic structure through linear functions that incorporate local side effects.
Cite as
Daniel Marshall and Dominic Orchard. How to Take the Inverse of a Type (Artifact). In Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022). Dagstuhl Artifacts Series (DARTS), Volume 8, Issue 2, pp. 1:1-1:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@Article{marshall_et_al:DARTS.8.2.1,
author = {Marshall, Daniel and Orchard, Dominic},
title = {{How to Take the Inverse of a Type (Artifact)}},
pages = {1:1--1:3},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2022},
volume = {8},
number = {2},
editor = {Marshall, Daniel and Orchard, Dominic},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DARTS.8.2.1},
URN = {urn:nbn:de:0030-drops-161991},
doi = {10.4230/DARTS.8.2.1},
annote = {Keywords: linear types, regular types, algebra of programming, derivatives}
}
Document
Artifact
Defining Corecursive Functions in Coq Using Approximations (Artifact)
Abstract
This is the formalization in the Coq proof assistant of the related conference article shown below.
Cite as
Vlad Rusu and David Nowak. Defining Corecursive Functions in Coq Using Approximations (Artifact). In Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022). Dagstuhl Artifacts Series (DARTS), Volume 8, Issue 2, pp. 2:1-2:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@Article{rusu_et_al:DARTS.8.2.2,
author = {Rusu, Vlad and Nowak, David},
title = {{Defining Corecursive Functions in Coq Using Approximations (Artifact)}},
pages = {2:1--2:2},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2022},
volume = {8},
number = {2},
editor = {Rusu, Vlad and Nowak, David},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DARTS.8.2.2},
URN = {urn:nbn:de:0030-drops-162001},
doi = {10.4230/DARTS.8.2.2},
annote = {Keywords: corecursive function, productiveness, approximation, Coq proof assistant.}
}
Document
Artifact
Compiling Volatile Correctly in Java (Artifact)
Abstract
The compilation scheme for Volatile accesses in the OpenJDK 9 HotSpot Java Virtual Machine has a major problem that persists despite a recent bug report and a long discussion. One of the suggested fixes is to let Java compile Volatile accesses in the same way as C/C++11. However, we show that this approach is invalid for Java. Indeed, we show a set of optimizations that is valid for C/C++11 but invalid for Java, while the compilation scheme is similar. We prove the correctness of the compilation scheme to Power and x86 and a suite of valid optimizations in Java. Our proofs are based on a language model that we validate by proving key properties such as the DRF-SC theorem and by running litmus tests via our implementation of Java in Herd7.
Cite as
Shuyang Liu, John Bender, and Jens Palsberg. Compiling Volatile Correctly in Java (Artifact). In Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022). Dagstuhl Artifacts Series (DARTS), Volume 8, Issue 2, pp. 3:1-3:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@Article{liu_et_al:DARTS.8.2.3,
author = {Liu, Shuyang and Bender, John and Palsberg, Jens},
title = {{Compiling Volatile Correctly in Java (Artifact)}},
pages = {3:1--3:2},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2022},
volume = {8},
number = {2},
editor = {Liu, Shuyang and Bender, John and Palsberg, Jens},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DARTS.8.2.3},
URN = {urn:nbn:de:0030-drops-162018},
doi = {10.4230/DARTS.8.2.3},
annote = {Keywords: formal semantics, concurrency, compilation}
}
Document
Artifact
Direct Foundations for Compositional Programming (Artifact)
Abstract
Our companion paper proposes a new formulation of the 𝖥_{i}^{+} calculus with disjoint polymorphism and a merge operator based on Type-Directed Operational Semantics. The artifact contains Coq formalization of the 𝖥_{i}^{+} calculus and our new implementation of the CP language, which demonstrates the new 𝖥_{i}^{+} can serve as the direct foundation for Compositional Programming.
Cite as
Andong Fan, Xuejing Huang, Han Xu, Yaozhu Sun, and Bruno C. d. S. Oliveira. Direct Foundations for Compositional Programming (Artifact). In Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022). Dagstuhl Artifacts Series (DARTS), Volume 8, Issue 2, pp. 4:1-4:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@Article{fan_et_al:DARTS.8.2.4,
author = {Fan, Andong and Huang, Xuejing and Xu, Han and Sun, Yaozhu and Oliveira, Bruno C. d. S.},
title = {{Direct Foundations for Compositional Programming (Artifact)}},
pages = {4:1--4:3},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2022},
volume = {8},
number = {2},
editor = {Fan, Andong and Huang, Xuejing and Xu, Han and Sun, Yaozhu and Oliveira, Bruno C. d. S.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DARTS.8.2.4},
URN = {urn:nbn:de:0030-drops-162020},
doi = {10.4230/DARTS.8.2.4},
annote = {Keywords: Intersection types, disjoint polymorphism, operational semantics}
}
Document
Artifact
Elementary Type Inference (Artifact)
Abstract
This artifact contains the Appendix of the paper, proofs of theorems declared in the paper, and a sample implementation of the type inference algorithm. The proof contains 3 main results: soundness, completness and decidability of the type-inference algorithm. Moreover, there are several proofs about the declarative system and also a soundness/completeness proof between stable subtyping and a syntax-directed specification.
Cite as
Jinxu Zhao and Bruno C. d. S. Oliveira. Elementary Type Inference (Artifact). In Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022). Dagstuhl Artifacts Series (DARTS), Volume 8, Issue 2, pp. 5:1-5:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@Article{zhao_et_al:DARTS.8.2.5,
author = {Zhao, Jinxu and Oliveira, Bruno C. d. S.},
title = {{Elementary Type Inference (Artifact)}},
pages = {5:1--5:2},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2022},
volume = {8},
number = {2},
editor = {Zhao, Jinxu and Oliveira, Bruno C. d. S.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DARTS.8.2.5},
URN = {urn:nbn:de:0030-drops-162036},
doi = {10.4230/DARTS.8.2.5},
annote = {Keywords: Type Inference}
}
Document
Artifact
Qilin: A New Framework for Supporting Fine-Grained Context-Sensitivity in Java Pointer Analysis (Artifact)
Abstract
Existing whole-program context-sensitive pointer analysis frameworks for Java, which were open-sourced over one decade ago, were designed and implemented to support only method-level context-sensitivity (where all the variables/objects in a method are qualified by a common context abstraction representing a context under which the method is analyzed). We introduce Qilin as a generalized (modern) alternative, which will be open-sourced soon on GitHub, to support the current research trend on exploring fine-grained context-sensitivity (including variable-level context-sensitivity where different variables/objects in a method can be analyzed under different context abstractions at the variable level), precisely, efficiently, and modularly. To meet these four design goals, Qilin is developed as an imperative framework (implemented in Java) consisting of a fine-grained pointer analysis kernel with parameterized context-sensitivity that supports on-the-fly call graph construction and exception analysis, solved iteratively based on a new carefully-crafted incremental worklist-based constraint solver, on top of its handlers for complex Java features.
We have evaluated Qilin extensively using a set of 12 representative Java programs (popularly used in the literature). For method-level context-sensitive analyses, we compare Qilin with Doop (a declarative framework that defines the state-of-the-art), Qilin yields logically the same precision but more efficiently (e.g., 2.4x faster for four typical baselines considered, on average). For fine-grained context-sensitive analyses (which are not currently supported by open-source Java pointer analysis frameworks such as Doop), we show that Qilin allows seven recent approaches to be instantiated effectively in our parameterized framework, requiring additionally only an average of 50 LOC each.
Cite as
Dongjie He, Jingbo Lu, and Jingling Xue. Qilin: A New Framework for Supporting Fine-Grained Context-Sensitivity in Java Pointer Analysis (Artifact). In Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022). Dagstuhl Artifacts Series (DARTS), Volume 8, Issue 2, pp. 6:1-6:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@Article{he_et_al:DARTS.8.2.6,
author = {He, Dongjie and Lu, Jingbo and Xue, Jingling},
title = {{Qilin: A New Framework for Supporting Fine-Grained Context-Sensitivity in Java Pointer Analysis (Artifact)}},
pages = {6:1--6:3},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2022},
volume = {8},
number = {2},
editor = {He, Dongjie and Lu, Jingbo and Xue, Jingling},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DARTS.8.2.6},
URN = {urn:nbn:de:0030-drops-162040},
doi = {10.4230/DARTS.8.2.6},
annote = {Keywords: Pointer Analysis, Fine-Grained Context Sensitivity}
}
Document
Artifact
Automatic Root Cause Quantification for Missing Edges in JavaScript Call Graphs (Artifact)
Abstract
Building sound and precise static call graphs for real-world JavaScript applications poses an enormous challenge, due to many hard-to-analyze language features. Further, the relative importance of these features may vary depending on the call graph algorithm being used and the class of applications being analyzed. In this paper, we present a technique to automatically quantify the relative importance of different root causes of call graph unsoundness for a set of target applications. The technique works by identifying the dynamic function data flows relevant to each call edge missed by the static analysis, correctly handling cases with multiple root causes and inter-dependent calls. We apply our approach to perform a detailed study of the recall of a state-of-the-art call graph construction technique on a set of framework-based web applications. The study yielded a number of useful insights. We found that while dynamic property accesses were the most common root cause of missed edges across the benchmarks, other root causes varied in importance depending on the benchmark, potentially useful information for an analysis designer. Further, with our approach, we could quickly identify and fix a recall issue in the call graph builder we studied, and also quickly assess whether a recent analysis technique for Node.js-based applications would be helpful for browser-based code. All of our code and data is publicly available, and many components of our technique can be re-used to facilitate future studies.
Cite as
Madhurima Chakraborty, Renzo Olivares, Manu Sridharan, and Behnaz Hassanshahi. Automatic Root Cause Quantification for Missing Edges in JavaScript Call Graphs (Artifact). In Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022). Dagstuhl Artifacts Series (DARTS), Volume 8, Issue 2, pp. 7:1-7:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@Article{chakraborty_et_al:DARTS.8.2.7,
author = {Chakraborty, Madhurima and Olivares, Renzo and Sridharan, Manu and Hassanshahi, Behnaz},
title = {{Automatic Root Cause Quantification for Missing Edges in JavaScript Call Graphs (Artifact)}},
pages = {7:1--7:5},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2022},
volume = {8},
number = {2},
editor = {Chakraborty, Madhurima and Olivares, Renzo and Sridharan, Manu and Hassanshahi, Behnaz},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DARTS.8.2.7},
URN = {urn:nbn:de:0030-drops-162052},
doi = {10.4230/DARTS.8.2.7},
annote = {Keywords: JavaScript, call graph construction, static program analysis}
}
Document
Artifact
Functional Programming for Distributed Systems with XC (Artifact)
Abstract
In the paper "Functional programming for distributed systems with XC" we present XC, a programming language to develop the collective behaviour of homogeneous distributed systems while abstracting over concurrency, asynchronous execution, message loss, and device failures. The paper describes the design of XC, formalizes a core calculus for it, and shows that XC can effectively capture the logic of several distributed protocols and applications including gossiping, distributed summarization, information flows over self-healing communication structures, and self-organizing behaviours. Then, it discusses implementation, in a Scala and a C++ embedded domain-specific language (DSL), and provides evaluation through a case study in a smart city scenario, called SmartC. The reusable artifact described in this paper contains precisely those software projects: the Scala DSL, referred to as XC/Scala; the C++ DSL, referred to as XC/C++; and the SmartC implementation in both DSLs.
Cite as
Giorgio Audrito, Roberto Casadei, Ferruccio Damiani, Guido Salvaneschi, and Mirko Viroli. Functional Programming for Distributed Systems with XC (Artifact). In Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022). Dagstuhl Artifacts Series (DARTS), Volume 8, Issue 2, pp. 8:1-8:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@Article{audrito_et_al:DARTS.8.2.8,
author = {Audrito, Giorgio and Casadei, Roberto and Damiani, Ferruccio and Salvaneschi, Guido and Viroli, Mirko},
title = {{Functional Programming for Distributed Systems with XC (Artifact)}},
pages = {8:1--8:4},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2022},
volume = {8},
number = {2},
editor = {Audrito, Giorgio and Casadei, Roberto and Damiani, Ferruccio and Salvaneschi, Guido and Viroli, Mirko},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DARTS.8.2.8},
URN = {urn:nbn:de:0030-drops-162068},
doi = {10.4230/DARTS.8.2.8},
annote = {Keywords: Distributed programming, Field Calculi, Scala DSL, C++ DSL}
}
Document
Artifact
Stay Safe Under Panic: Affine Rust Programming with Multiparty Session Types (Artifact)
Abstract
This artifact contains a version of MultiCrusty, a Rust library designed for writing and checking communication protocols following the Affine Multiparty Session Types theory introduced in our ECOOP'22 paper. MultiCrusty can work, and should be used, with Scribble [Yoshida et al., 2014] and kMC [{Julien} {Lange} and {Nobuko} {Yoshida}, 2019]: with the former tool, users can write correct global protocols and project them onto local Rust types defined within MultiCrusty, this approach is qualified as top-down; while the latter tool allows to check local Rust types written by users, this approach is qualified as bottom-up. Our artifact contains those three tools, their respective source files, as well as the different examples and benchmarks introduced in our paper, all together within a Docker image.
Cite as
Nicolas Lagaillardie, Rumyana Neykova, and Nobuko Yoshida. Stay Safe Under Panic: Affine Rust Programming with Multiparty Session Types (Artifact). In Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022). Dagstuhl Artifacts Series (DARTS), Volume 8, Issue 2, pp. 9:1-9:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@Article{lagaillardie_et_al:DARTS.8.2.9,
author = {Lagaillardie, Nicolas and Neykova, Rumyana and Yoshida, Nobuko},
title = {{Stay Safe Under Panic: Affine Rust Programming with Multiparty Session Types (Artifact)}},
pages = {9:1--9:16},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2022},
volume = {8},
number = {2},
editor = {Lagaillardie, Nicolas and Neykova, Rumyana and Yoshida, Nobuko},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DARTS.8.2.9},
URN = {urn:nbn:de:0030-drops-162075},
doi = {10.4230/DARTS.8.2.9},
annote = {Keywords: Rust language, affine multiparty session types, failures, cancellation}
}
Document
Artifact
Verified Compilation and Optimization of Floating-Point Programs in CakeML (Artifact)
Abstract
Verified compilers such as CompCert and CakeML have become increasingly realistic over the last few years, but their support for floating-point arithmetic has thus far been limited. In particular, they lack the "fast-math-style" optimizations that unverified mainstream compilers perform. Supporting such optimizations in the setting of verified compilers is challenging because these optimizations, for the most part, do not preserve the IEEE-754 floating-point semantics. However, IEEE-754 floating-point numbers are finite approximations of the real numbers, and we argue that any compiler correctness result for fast-math optimizations should appeal to a real-valued semantics rather than the rigid IEEE-754 floating-point numbers.
This document describes the artifact for RealCake, an extension of CakeML that achieves end-to-end correctness results for fast-math-style optimized compilation of floating-point arithmetic. This result is achieved by giving CakeML a flexible floating-point semantics and integrating an external proof-producing accuracy analysis. RealCake’s end-to-end theorems relate the I/O behavior of the original source program under real-number semantics to the observable I/O behavior of the compiler generated and fast-math-optimized machine code.
Cite as
Heiko Becker, Robert Rabe, Eva Darulova, Magnus O. Myreen, Zachary Tatlock, Ramana Kumar, Yong Kiam Tan, and Anthony Fox. Verified Compilation and Optimization of Floating-Point Programs in CakeML (Artifact). In Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022). Dagstuhl Artifacts Series (DARTS), Volume 8, Issue 2, pp. 10:1-10:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@Article{becker_et_al:DARTS.8.2.10,
author = {Becker, Heiko and Rabe, Robert and Darulova, Eva and Myreen, Magnus O. and Tatlock, Zachary and Kumar, Ramana and Tan, Yong Kiam and Fox, Anthony},
title = {{Verified Compilation and Optimization of Floating-Point Programs in CakeML (Artifact)}},
pages = {10:1--10:2},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2022},
volume = {8},
number = {2},
editor = {Becker, Heiko and Rabe, Robert and Darulova, Eva and Myreen, Magnus O. and Tatlock, Zachary and Kumar, Ramana and Tan, Yong Kiam and Fox, Anthony},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DARTS.8.2.10},
URN = {urn:nbn:de:0030-drops-162086},
doi = {10.4230/DARTS.8.2.10},
annote = {Keywords: compiler verification, compiler optimization, floating-point arithmetic}
}
Document
Artifact
Low-Level Bi-Abduction (Artifact)
Abstract
Broom is a new static analyzer for C written in OCaml. Broom primarily aims at open programs, i.e., fragments of programs, with dynamic pointer-linked data structures - in particular, various kinds of lists - that employ advanced low-level pointer operations. It is based on separation logic and the principle of bi-abductive reasoning. The artifact is a VirtualBox image of a Linux machine with Ubuntu 20.04 operating system. It contains source code and binary of the Broom tool, benchmarks, and scripts for running our and the competing tools we compare to.
Cite as
Lukáš Holík, Petr Peringer, Adam Rogalewicz, Veronika Šoková, Tomáš Vojnar, and Florian Zuleger. Low-Level Bi-Abduction (Artifact). In Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022). Dagstuhl Artifacts Series (DARTS), Volume 8, Issue 2, pp. 11:1-11:6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@Article{holik_et_al:DARTS.8.2.11,
author = {Hol{\'\i}k, Luk\'{a}\v{s} and Peringer, Petr and Rogalewicz, Adam and \v{S}okov\'{a}, Veronika and Vojnar, Tom\'{a}\v{s} and Zuleger, Florian},
title = {{Low-Level Bi-Abduction (Artifact)}},
pages = {11:1--11:6},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2022},
volume = {8},
number = {2},
editor = {Hol{\'\i}k, Luk\'{a}\v{s} and Peringer, Petr and Rogalewicz, Adam and \v{S}okov\'{a}, Veronika and Vojnar, Tom\'{a}\v{s} and Zuleger, Florian},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DARTS.8.2.11},
URN = {urn:nbn:de:0030-drops-162092},
doi = {10.4230/DARTS.8.2.11},
annote = {Keywords: programs with dynamic linked data structures, programs with pointers, low-level pointer operations, static analysis, shape analysis, separation logic, bi-abduction}
}
Document
Artifact
REST: Integrating Term Rewriting with Program Verification (Artifact)
Abstract
This artifact contains code for REST, a novel term rewriting technique for theorem proving that uses online termination checking and can be integrated with existing program verifiers. The artifact includes the REST library as well as a version of Liquid Haskell extended with REST. In addition, it includes the scripts that were used to generate the tables in the paper’s evaluation section. Also included is a docker image containing a development environment for REST (and the Liquid Haskell extension).
Cite as
Zachary Grannan, Niki Vazou, Eva Darulova, and Alexander J. Summers. REST: Integrating Term Rewriting with Program Verification (Artifact). In Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022). Dagstuhl Artifacts Series (DARTS), Volume 8, Issue 2, pp. 12:1-12:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@Article{grannan_et_al:DARTS.8.2.12,
author = {Grannan, Zachary and Vazou, Niki and Darulova, Eva and Summers, Alexander J.},
title = {{REST: Integrating Term Rewriting with Program Verification (Artifact)}},
pages = {12:1--12:2},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2022},
volume = {8},
number = {2},
editor = {Grannan, Zachary and Vazou, Niki and Darulova, Eva and Summers, Alexander J.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DARTS.8.2.12},
URN = {urn:nbn:de:0030-drops-162105},
doi = {10.4230/DARTS.8.2.12},
annote = {Keywords: term rewriting, program verification, theorem proving}
}
Document
Artifact
A Deterministic Memory Allocator for Dynamic Symbolic Execution (Artifact)
Abstract
KDAlloc is a deterministic memory allocator for Dynamic Symbolic Execution. This artifact provides the allocator itself, integrated into the KLEE symbolic execution engine and the evaluation thereof.
Cite as
Daniel Schemmel, Julian Büning, Frank Busse, Martin Nowack, and Cristian Cadar. A Deterministic Memory Allocator for Dynamic Symbolic Execution (Artifact). In Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022). Dagstuhl Artifacts Series (DARTS), Volume 8, Issue 2, pp. 13:1-13:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@Article{schemmel_et_al:DARTS.8.2.13,
author = {Schemmel, Daniel and B\"{u}ning, Julian and Busse, Frank and Nowack, Martin and Cadar, Cristian},
title = {{A Deterministic Memory Allocator for Dynamic Symbolic Execution (Artifact)}},
pages = {13:1--13:2},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2022},
volume = {8},
number = {2},
editor = {Schemmel, Daniel and B\"{u}ning, Julian and Busse, Frank and Nowack, Martin and Cadar, Cristian},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DARTS.8.2.13},
URN = {urn:nbn:de:0030-drops-162110},
doi = {10.4230/DARTS.8.2.13},
annote = {Keywords: memory allocation, dynamic symbolic execution}
}
Document
Artifact
Ferrite: A Judgmental Embedding of Session Types in Rust (Artifact)
Abstract
This artifact provides a VirtualBox image containing the snapshots of source code for Ferrite and Servo at the time the main paper was published.
Cite as
Ruo Fei Chen, Stephanie Balzer, and Bernardo Toninho. Ferrite: A Judgmental Embedding of Session Types in Rust (Artifact). In Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022). Dagstuhl Artifacts Series (DARTS), Volume 8, Issue 2, pp. 14:1-14:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@Article{chen_et_al:DARTS.8.2.14,
author = {Chen, Ruo Fei and Balzer, Stephanie and Toninho, Bernardo},
title = {{Ferrite: A Judgmental Embedding of Session Types in Rust (Artifact)}},
pages = {14:1--14:2},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2022},
volume = {8},
number = {2},
editor = {Chen, Ruo Fei and Balzer, Stephanie and Toninho, Bernardo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DARTS.8.2.14},
URN = {urn:nbn:de:0030-drops-162125},
doi = {10.4230/DARTS.8.2.14},
annote = {Keywords: Session Types, Rust, DSL}
}
Document
Artifact
A Self-Dual Distillation of Session Types: Mechanized Proofs (Artifact)
Abstract
This is the artifact description for the paper "A Self-Dual Distillation of Session Types". The artifact consists of mechanized proofs of the theorems listed in the paper, in the Coq proof assistant.
Cite as
Jules Jacobs. A Self-Dual Distillation of Session Types: Mechanized Proofs (Artifact). In Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022). Dagstuhl Artifacts Series (DARTS), Volume 8, Issue 2, pp. 15:1-15:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@Article{jacobs:DARTS.8.2.15,
author = {Jacobs, Jules},
title = {{A Self-Dual Distillation of Session Types: Mechanized Proofs (Artifact)}},
pages = {15:1--15:2},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2022},
volume = {8},
number = {2},
editor = {Jacobs, Jules},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DARTS.8.2.15},
URN = {urn:nbn:de:0030-drops-162137},
doi = {10.4230/DARTS.8.2.15},
annote = {Keywords: Linear types, concurrency, lambda calculus, session types}
}
Document
Artifact
Prisma: A Tierless Language for Enforcing Contract-Client Protocols in Decentralized Applications (Artifact)
Abstract
Decentralized applications (dApps) consist of smart contracts that run on blockchains and clients that model collaborating parties. dApps are used to model financial and legal business functionality. Today, contracts and clients are written as separate programs - in different programming languages - communicating via send and receive operations. This makes distributed program flow awkward to express and reason about, increasing the potential for mismatches in the client-contract interface, which can be exploited by malicious clients, potentially leading to huge financial losses. In this paper, we present Prisma, a language for tierless decentralized applications, where the contract and its clients are defined in one unit. Pairs of send and receive actions that “belong together” are encapsulated into a single direct-style operation, which is executed differently by sending and receiving parties. This enables expressing distributed program flow via standard control flow and renders mismatching communication impossible. We prove formally that our compiler preserves program behavior in presence of an attacker controlling the client code. We systematically compare Prisma with mainstream and advanced programming models for dApps and provide empirical evidence for its expressiveness and performance.
Cite as
David Richter, David Kretzler, Pascal Weisenburger, Guido Salvaneschi, Sebastian Faust, and Mira Mezini. Prisma: A Tierless Language for Enforcing Contract-Client Protocols in Decentralized Applications (Artifact). In Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022). Dagstuhl Artifacts Series (DARTS), Volume 8, Issue 2, pp. 16:1-16:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@Article{richter_et_al:DARTS.8.2.16,
author = {Richter, David and Kretzler, David and Weisenburger, Pascal and Salvaneschi, Guido and Faust, Sebastian and Mezini, Mira},
title = {{Prisma: A Tierless Language for Enforcing Contract-Client Protocols in Decentralized Applications (Artifact)}},
pages = {16:1--16:3},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2022},
volume = {8},
number = {2},
editor = {Richter, David and Kretzler, David and Weisenburger, Pascal and Salvaneschi, Guido and Faust, Sebastian and Mezini, Mira},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DARTS.8.2.16},
URN = {urn:nbn:de:0030-drops-162149},
doi = {10.4230/DARTS.8.2.16},
annote = {Keywords: Domain Specific Languages, Smart Contracts, Scala}
}
Document
Artifact
Union Types with Disjoint Switches (Artifact)
Abstract
This artifact contains the mechanical formalization of the calculi associated with the paper Union Types with Disjoint Switches. All of the metatheory has been formalized in Coq theorem prover. We provide a docker image as well the code archive.
The paper studies a union calculus ({λ_{u}}). Primary idea of {λ_{u}} calculus is a type based disjoint switch construct for the elimination of union types. We also study several extensions of the {λ_{u}} calculus including intersection types, distributive subtyping, nominal types, parametric polymorphism and an extension for the empty types.
Cite as
Baber Rehman, Xuejing Huang, Ningning Xie, and Bruno C. d. S. Oliveira. Union Types with Disjoint Switches (Artifact). In Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022). Dagstuhl Artifacts Series (DARTS), Volume 8, Issue 2, pp. 17:1-17:6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@Article{rehman_et_al:DARTS.8.2.17,
author = {Rehman, Baber and Huang, Xuejing and Xie, Ningning and Oliveira, Bruno C. d. S.},
title = {{Union Types with Disjoint Switches (Artifact)}},
pages = {17:1--17:6},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2022},
volume = {8},
number = {2},
editor = {Rehman, Baber and Huang, Xuejing and Xie, Ningning and Oliveira, Bruno C. d. S.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DARTS.8.2.17},
URN = {urn:nbn:de:0030-drops-162150},
doi = {10.4230/DARTS.8.2.17},
annote = {Keywords: Union types, switch expression, disjointness, intersection types}
}
Document
Artifact
Global Type Inference for Featherweight Generic Java - Prototype Implementation (Artifact)
Abstract
We implemented a prototype of the type inference algorithm described in the paper "Global Type Inference for Featherweight Generic Java". Our type inference algorithm for Featherweight Generic Java (GFJ) is able to calculate the missing types in a Typeless Featherweight Generic Java (FGJ-GT) program. Inserting those types generates a valid GFJ program. We demonstrate this with a prototype implementation. The prototype is a web application which accepts GFJ-GT programs as input and shows the respective GFJ program after the type inference.
Cite as
Andreas Stadelmeier, Martin Plümicke, and Peter Thiemann. Global Type Inference for Featherweight Generic Java - Prototype Implementation (Artifact). In Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022). Dagstuhl Artifacts Series (DARTS), Volume 8, Issue 2, pp. 18:1-18:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@Article{stadelmeier_et_al:DARTS.8.2.18,
author = {Stadelmeier, Andreas and Pl\"{u}micke, Martin and Thiemann, Peter},
title = {{Global Type Inference for Featherweight Generic Java - Prototype Implementation (Artifact)}},
pages = {18:1--18:4},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2022},
volume = {8},
number = {2},
editor = {Stadelmeier, Andreas and Pl\"{u}micke, Martin and Thiemann, Peter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DARTS.8.2.18},
URN = {urn:nbn:de:0030-drops-162165},
doi = {10.4230/DARTS.8.2.18},
annote = {Keywords: type inference, Java, subtyping, generics}
}
Document
Artifact
API Generation for Multiparty Session Types, Revisited and Revised Using Scala 3 (Artifact)
Abstract
Construction and analysis of distributed systems is difficult. Multiparty session types (MPST) constitute a method to make it easier. The idea is to use type checking to statically prove deadlock freedom and protocol compliance of communicating processes. In practice, the premier approach to apply the MPST method in combination with mainstream programming languages has been based on API generation. With this artifact, and the companion paper, we revisit and revise this approach.
Regarding our "revisitation", using Scala 3, we present the existing API generation approach, which is based on deterministic finite automata (DFA), in terms of both the existing states-as-classes encoding of DFAs as APIs, and a new states-as-type-parameters encoding; the latter leverages match types in Scala 3. Regarding our "revision", also using Scala 3, we present a new API generation approach that is based on sets of pomsets instead of DFAs; it crucially leverages match types, too. Our fresh perspective allows us to avoid two forms of combinatorial explosion resulting from implementing concurrent subprotocols in the DFA-based approach. We implement our approach in a new API generation tool, called Pompset. This artifact contains Pompset.
Cite as
Guillermina Cledou, Luc Edixhoven, Sung-Shik Jongmans, and José Proença. API Generation for Multiparty Session Types, Revisited and Revised Using Scala 3 (Artifact). In Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022). Dagstuhl Artifacts Series (DARTS), Volume 8, Issue 2, pp. 19:1-19:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@Article{cledou_et_al:DARTS.8.2.19,
author = {Cledou, Guillermina and Edixhoven, Luc and Jongmans, Sung-Shik and Proen\c{c}a, Jos\'{e}},
title = {{API Generation for Multiparty Session Types, Revisited and Revised Using Scala 3 (Artifact)}},
pages = {19:1--19:4},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2022},
volume = {8},
number = {2},
editor = {Cledou, Guillermina and Edixhoven, Luc and Jongmans, Sung-Shik and Proen\c{c}a, Jos\'{e}},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DARTS.8.2.19},
URN = {urn:nbn:de:0030-drops-162171},
doi = {10.4230/DARTS.8.2.19},
annote = {Keywords: Concurrency, pomsets (partially ordered multisets), match types, Scala 3}
}
Document
Artifact
Concolic Execution for WebAssembly (Artifact)
Abstract
This artifact contains the implementation of WASP, a symbolic execution engine for Wasm, and WASP-C, a symbolic execution framework for testing C programs built using WASP . WASP works directly on Wasm code and was built on top of a standard-compliant Wasm reference implementation [Andreas Haas et al., 2017]. WASP was thoroughly evaluated: it was used to symbolically test a generic data-structure library and the Amazon Encryption SDK for C, demonstrating that it can find bugs and generate high-coverage testing inputs for real-world C applications; WASP was further tested against the Test-Comp benchmark, obtaining results comparable to well-established symbolic execution and testing tools for C.
Cite as
Filipe Marques, José Fragoso Santos, Nuno Santos, and Pedro Adão. Concolic Execution for WebAssembly (Artifact). In Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022). Dagstuhl Artifacts Series (DARTS), Volume 8, Issue 2, pp. 20:1-20:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@Article{marques_et_al:DARTS.8.2.20,
author = {Marques, Filipe and Fragoso Santos, Jos\'{e} and Santos, Nuno and Ad\~{a}o, Pedro},
title = {{Concolic Execution for WebAssembly (Artifact)}},
pages = {20:1--20:3},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2022},
volume = {8},
number = {2},
editor = {Marques, Filipe and Fragoso Santos, Jos\'{e} and Santos, Nuno and Ad\~{a}o, Pedro},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DARTS.8.2.20},
URN = {urn:nbn:de:0030-drops-162181},
doi = {10.4230/DARTS.8.2.20},
annote = {Keywords: Concolic Testing, WebAssembly, Test-Generation, Testing C Programs}
}
Document
Artifact
Design-by-Contract for Flexible Multiparty Session Protocols (Artifact)
Abstract
We introduce CAScr, the first implementation of Scribble (http://www.scribble.org, https://nuscr.dev/) that relies on choreography automata, for deadlock-free distributed programming. CAScr supports the main theoretical results and constructions in the related article. CAScr takes the popular top-down approach to system development, based on choreographic models, following the original methodology of Scribble and multiparty session types. The top-down approach enables correctness-by-construction: a developer provides a global description for the whole communication protocol; by projecting the global protocol, APIs are generated from local CFSMs, which ensure the safe implementation of each participant. The theory of choreography automata in the related article guarantees deadlock freedom for the distributed implementation of flexible global protocols. We target web development, supporting in particular the TypeScript programming language.
Cite as
Lorenzo Gheri, Ivan Lanese, Neil Sayers, Emilio Tuosto, and Nobuko Yoshida. Design-by-Contract for Flexible Multiparty Session Protocols (Artifact). In Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022). Dagstuhl Artifacts Series (DARTS), Volume 8, Issue 2, pp. 21:1-21:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@Article{gheri_et_al:DARTS.8.2.21,
author = {Gheri, Lorenzo and Lanese, Ivan and Sayers, Neil and Tuosto, Emilio and Yoshida, Nobuko},
title = {{Design-by-Contract for Flexible Multiparty Session Protocols (Artifact)}},
pages = {21:1--21:5},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2022},
volume = {8},
number = {2},
editor = {Gheri, Lorenzo and Lanese, Ivan and Sayers, Neil and Tuosto, Emilio and Yoshida, Nobuko},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DARTS.8.2.21},
URN = {urn:nbn:de:0030-drops-162196},
doi = {10.4230/DARTS.8.2.21},
annote = {Keywords: Choreography automata, design by contract, deadlock freedom, Communicating Finite State Machines, TypeScript programming}
}
Document
Artifact
Accumulation Analysis (Artifact)
Abstract
This artifact contains the data and analysis supporting the literature survey in section 4 of [Kellogg et al., 2022]. In our literature survey, we examined 187 papers from the literature that mention "typestate" and analyzed the typestate specifications they contained to determine whether or not they are accumulation typestate specifications.
Our purpose in doing this literature survey was to determine whether typestate FSMs were accumulation or not. However, we believe that the collection of typestate automata in typestates.pdf might be useful to anyone interested in the sort of typestate automata that appear in the literature. If we had had access to such a collection (gathered for a different purpose), our classification of whether these typestate automata were accumulation would have been much simpler. Anyone interested in properties of typestate automata can re-use our work.
Cite as
Martin Kellogg, Narges Shadab, Manu Sridharan, and Michael D. Ernst. Accumulation Analysis (Artifact). In Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022). Dagstuhl Artifacts Series (DARTS), Volume 8, Issue 2, pp. 22:1-22:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@Article{kellogg_et_al:DARTS.8.2.22,
author = {Kellogg, Martin and Shadab, Narges and Sridharan, Manu and Ernst, Michael D.},
title = {{Accumulation Analysis (Artifact)}},
pages = {22:1--22:3},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2022},
volume = {8},
number = {2},
editor = {Kellogg, Martin and Shadab, Narges and Sridharan, Manu and Ernst, Michael D.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DARTS.8.2.22},
URN = {urn:nbn:de:0030-drops-162209},
doi = {10.4230/DARTS.8.2.22},
annote = {Keywords: Typestate, finite-state property}
}
Document
Artifact
JavaScript Sealed Classes (Artifact)
Abstract
In this work, we study the JavaScript Sealed Classes, which differ from regular classes in a few ways that allow ahead-of-time (AoT) compilers to implement them more efficiently. Sealed classes are compatible with the rest of the language so that they can be combined with all other structures, including regular classes, and can be gradually integrated into existing code bases.
We present the design of the sealed classes and study their implementation in the hopc AoT compiler. We present an in-depth analysis of the speed of sealed classes compared to regular classes. To do so, we assembled a new suite of benchmarks that focuses on the efficiency of the class implementations. On this suite, we found that sealed classes provide an average speedup of 19%. The more classes and methods programs use, the greater the speedup. For the most favorable test that uses them intensively, we measured a speedup of 56%.
Cite as
Manuel Serrano. JavaScript Sealed Classes (Artifact). In Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022). Dagstuhl Artifacts Series (DARTS), Volume 8, Issue 2, pp. 23:1-23:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@Article{serrano:DARTS.8.2.23,
author = {Serrano, Manuel},
title = {{JavaScript Sealed Classes (Artifact)}},
pages = {23:1--23:4},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2022},
volume = {8},
number = {2},
editor = {Serrano, Manuel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DARTS.8.2.23},
URN = {urn:nbn:de:0030-drops-162212},
doi = {10.4230/DARTS.8.2.23},
annote = {Keywords: JavaScript, Compiler, Dynamic Languages, Classes, Inline caches}
}
Document
Artifact
PEDroid: Automatically Extracting Patches from Android App Updates (Artifact)
Abstract
We propose an approach to automatically identify and extract patches from updated Android apps by comparing the updated versions and their predecessors. PEDroid, a prototype patch extraction tool against Android apps, consists of two phases: differential analysis and patch identification. We evaluated it with a set of popular open-source apps to demonstrate its effectiveness. PEDroid achieves a recall of 92% in differential analysis and successfully identifies 28 of 36 patches in patch identification. We also provide specific guidance on reproducing the experimental results.
Cite as
Hehao Li, Yizhuo Wang, Yiwei Zhang, Juanru Li, and Dawu Gu. PEDroid: Automatically Extracting Patches from Android App Updates (Artifact). In Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022). Dagstuhl Artifacts Series (DARTS), Volume 8, Issue 2, pp. 24:1-24:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@Article{li_et_al:DARTS.8.2.24,
author = {Li, Hehao and Wang, Yizhuo and Zhang, Yiwei and Li, Juanru and Gu, Dawu},
title = {{PEDroid: Automatically Extracting Patches from Android App Updates (Artifact)}},
pages = {24:1--24:2},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2022},
volume = {8},
number = {2},
editor = {Li, Hehao and Wang, Yizhuo and Zhang, Yiwei and Li, Juanru and Gu, Dawu},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DARTS.8.2.24},
URN = {urn:nbn:de:0030-drops-162229},
doi = {10.4230/DARTS.8.2.24},
annote = {Keywords: Diffing, Patch Identification, Android App Analysis, App Evolution}
}
Document
Artifact
Synchron - An API and Runtime for Embedded Systems (Artifact)
Abstract
Programming embedded applications involves writing concurrent, event-driven and timing-aware programs. Traditionally, such programs are written in machine-oriented programming languages like C or Assembly. We present an alternative by introducing Synchron, an API that offers high-level abstractions to the programmer while supporting the low-level infrastructure in an associated runtime system and one-time-effort drivers.
Embedded systems applications exhibit the general characteristics of being (i) concurrent, (ii) I/O-bound and (iii) timing-aware. To address each of these concerns, the Synchron API consists of three components - (1) a Concurrent ML (CML) inspired message-passing concurrency model, (2) a message-passing-based I/O interface that translates between low-level interrupt based and memory-mapped peripherals, and (3) a timing operator, syncT, that marries CML’s sync operator with timing windows inspired from the TinyTimber kernel.
We implement the Synchron API as the bytecode instructions of a virtual machine called SynchronVM. SynchronVM hosts a Caml-inspired functional language as its frontend language, and the backend of the VM supports the STM32F4 and NRF52 microcontrollers, with RAM in the order of hundreds of kilobytes. We illustrate the expressiveness of the Synchron API by showing examples of expressing state machines commonly found in embedded systems. The timing functionality is demonstrated through a music programming exercise. Finally, we provide benchmarks on the response time, jitter rates, memory, and power usage of the SynchronVM.
Cite as
Abhiroop Sarkar and Bo Joel Svensson. Synchron - An API and Runtime for Embedded Systems (Artifact). In Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022). Dagstuhl Artifacts Series (DARTS), Volume 8, Issue 2, pp. 25:1-25:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@Article{sarkar_et_al:DARTS.8.2.25,
author = {Sarkar, Abhiroop and Svensson, Bo Joel},
title = {{Synchron - An API and Runtime for Embedded Systems (Artifact)}},
pages = {25:1--25:2},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2022},
volume = {8},
number = {2},
editor = {Sarkar, Abhiroop and Svensson, Bo Joel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DARTS.8.2.25},
URN = {urn:nbn:de:0030-drops-162238},
doi = {10.4230/DARTS.8.2.25},
annote = {Keywords: real-time, concurrency, functional programming, runtime, virtual machine}
}
Document
Artifact
What If We Don't Pop the Stack? The Return of 2nd-Class Values (Artifact)
Abstract
The main paper presents λ^{1/2}_{↩}, a type system and operational semantics with 2nd-class values and delayed stack reclamation. This artifact contains a compiler implementation of the calculus in Scala Native, the code for the case studies shown in the paper, and code for reproducing the evaluation.
Cite as
Anxhelo Xhebraj, Oliver Bračevac, Guannan Wei, and Tiark Rompf. What If We Don't Pop the Stack? The Return of 2nd-Class Values (Artifact). In Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022). Dagstuhl Artifacts Series (DARTS), Volume 8, Issue 2, pp. 26:1-26:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@Article{xhebraj_et_al:DARTS.8.2.26,
author = {Xhebraj, Anxhelo and Bra\v{c}evac, Oliver and Wei, Guannan and Rompf, Tiark},
title = {{What If We Don't Pop the Stack? The Return of 2nd-Class Values (Artifact)}},
pages = {26:1--26:2},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2022},
volume = {8},
number = {2},
editor = {Xhebraj, Anxhelo and Bra\v{c}evac, Oliver and Wei, Guannan and Rompf, Tiark},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DARTS.8.2.26},
URN = {urn:nbn:de:0030-drops-162247},
doi = {10.4230/DARTS.8.2.26},
annote = {Keywords: Call stack, closures, stack allocation, memory management, 2nd-class values, capabilities, effects}
}