Issue
DARTS, Volume 3, Issue 2
Special Issue of the 31st European Conference on Object-Oriented Programming (ECOOP 2017)
-
Part of:
Volume:
DARTS, Volume 3 (ECOOP 2017)
Conference: European Conference on Object-Oriented Programming (ECOOP)
Journal: Dagstuhl Artifacts Series (DARTS)
Editors
Publication Details
- published at: 2017-06-20
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- DBLP: db/journals/darts/darts3
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 - ECOOP 2017 Artifacts, Table of Contents, Preface, Artifact Evaluation Committee
Abstract
Front Matter - ECOOP 2017 Artifacts, Table of Contents, Preface, Artifact Evaluation Committee
Cite as
Special Issue of the 31st European Conference on Object-Oriented Programming (ECOOP 2017). Dagstuhl Artifacts Series (DARTS), Volume 3, Issue 2, pp. 0:i-0:xii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@Article{haller_et_al:DARTS.3.2.0,
author = {Haller, Philipp and Pradel, Michael and van der Storm, Tijs},
title = {{ Front Matter - ECOOP 2017 Artifacts, Table of Contents, Preface, Artifact Evaluation Committee}},
pages = {0:i--0:xii},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2017},
volume = {3},
number = {2},
editor = {Haller, Philipp and Pradel, Michael and van der Storm, Tijs},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.3.2.0},
URN = {urn:nbn:de:0030-drops-72813},
doi = {10.4230/DARTS.3.2.0},
annote = {Keywords: Front Matter - ECOOP 2017 Artifacts, Table of Contents, Preface, Artifact Evaluation Committee}
}
Document
IceDust 2: Derived Bidirectional Relations and Calculation Strategy Composition (Artifact)
Abstract
This artifact is based on IceDust2, a data modeling language with derived values. The provided package is designed to support the claims of the companion paper: in particular, it allows users to compile and run IceDust2 specifications. Instructions for building the IceDust2 compiler from source in Spoofax are also provided.
Cite as
Daco C. Harkes and Eelco Visser. IceDust 2: Derived Bidirectional Relations and Calculation Strategy Composition (Artifact). In Special Issue of the 31st European Conference on Object-Oriented Programming (ECOOP 2017). Dagstuhl Artifacts Series (DARTS), Volume 3, Issue 2, pp. 1:1-1:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@Article{harkes_et_al:DARTS.3.2.1,
author = {Harkes, Daco C. and Visser, Eelco},
title = {{IceDust 2: Derived Bidirectional Relations and Calculation Strategy Composition (Artifact)}},
pages = {1:1--1:2},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2017},
volume = {3},
number = {2},
editor = {Harkes, Daco C. and Visser, Eelco},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.3.2.1},
URN = {urn:nbn:de:0030-drops-72826},
doi = {10.4230/DARTS.3.2.1},
annote = {Keywords: incremental computing, data modeling, domain specific language}
}
Document
A Capability-Based Module System for Authority Control (Artifact)
Abstract
This artifact is intended to demonstrate the module system of the Wyvern programming language and consists of a Linux virtual machine with a snapshot of the Wyvern programming language's codebase. The Wyvern codebase contains a test suite that corresponds to the code examples in the paper accompanying the artifact. In addition, the artifact contains a document describing how to compile and run Wyvern programs.
Cite as
Darya Melicher, Yangqingwei Shi, Alex Potanin, and Jonathan Aldrich. A Capability-Based Module System for Authority Control (Artifact). In Special Issue of the 31st European Conference on Object-Oriented Programming (ECOOP 2017). Dagstuhl Artifacts Series (DARTS), Volume 3, Issue 2, pp. 2:1-2:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@Article{melicher_et_al:DARTS.3.2.2,
author = {Melicher, Darya and Shi, Yangqingwei and Potanin, Alex and Aldrich, Jonathan},
title = {{A Capability-Based Module System for Authority Control (Artifact)}},
pages = {2:1--2:2},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2017},
volume = {3},
number = {2},
editor = {Melicher, Darya and Shi, Yangqingwei and Potanin, Alex and Aldrich, Jonathan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.3.2.2},
URN = {urn:nbn:de:0030-drops-72838},
doi = {10.4230/DARTS.3.2.2},
annote = {Keywords: language-based security, capabilities, authority, modules}
}
Document
A Linear Decomposition of Multiparty Sessions for Safe Distributed Programming (Artifact)
Abstract
This artifact contains a version of the Scribble tool that, given a protocol specification with multiple participants, can generate Scala APIs for implementing each participant in a type-safe, protocol-abiding way. Crucially, the API generation leverages a decomposition of the multiparty protocol into type-safe peer-to-peer interactions between pairs of participants; and this, in turn, allows to implement the API internals on top of the existing lchannels library for type-safe binary session programming. As a result, several technically challenging aspects in the implementation of multiparty sessions are solved "for free", at the underlying binary level. This includes distributed multiparty session delegation: this artifact implements it for the first time.
Cite as
Alceste Scalas, Ornela Dardha, Raymond Hu, and Nobuko Yoshida. A Linear Decomposition of Multiparty Sessions for Safe Distributed Programming (Artifact). In Special Issue of the 31st European Conference on Object-Oriented Programming (ECOOP 2017). Dagstuhl Artifacts Series (DARTS), Volume 3, Issue 2, pp. 3:1-3:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@Article{scalas_et_al:DARTS.3.2.3,
author = {Scalas, Alceste and Dardha, Ornela and Hu, Raymond and Yoshida, Nobuko},
title = {{A Linear Decomposition of Multiparty Sessions for Safe Distributed Programming (Artifact)}},
pages = {3:1--3:3},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2017},
volume = {3},
number = {2},
editor = {Scalas, Alceste and Dardha, Ornela and Hu, Raymond and Yoshida, Nobuko},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.3.2.3},
URN = {urn:nbn:de:0030-drops-72847},
doi = {10.4230/DARTS.3.2.3},
annote = {Keywords: process calculi, session types, concurrent programming, Scala}
}
Document
Concurrent Data Structures Linked in Time (Artifact)
Abstract
This artifact provides the full mechanization in FCSL of the
developments in the companion paper, "Concurrent Data Structures
Linked in Time". In the latter, we propose a new method, based on a
separation-style logic, for reasoning about concurrent objects with
such linearization points. We embrace the dynamic nature of
linearization points, and encode it as part of the data structure's
auxiliary state, so that it can be dynamically modified in
place by auxiliary code, as needed when some appropriate run-time
event occurs. We illustrate the method by verifying (mechanically in
FCSL) an intricate optimal snapshot algorithm due to Jayanti, as well
as some clients.
FCSL is the first completely formalized framework for mechanized
verification of full functional correctness of fine-grained concurrent
programs. It is implemented as an embedded domain-specific language
(DSL) in the dependently-typed language of the Coq proof assistant,
and is powerful enough to reason about programming features such as
higher-order functions and local thread spawning. By incorporating a
uniform concurrency model, based on state-transition systems and
partial commutative monoids, FCSL makes it possible to build proofs
about concurrent libraries in a thread-local, compositional way, thus
facilitating scalability and reuse: libraries are verified just once,
and their specifications are used ubiquitously in client-side
reasoning.
Cite as
Germán Andrés Delbianco, Ilya Sergey, Aleksandar Nanevski, and Anindya Banerjee. Concurrent Data Structures Linked in Time (Artifact). In Special Issue of the 31st European Conference on Object-Oriented Programming (ECOOP 2017). Dagstuhl Artifacts Series (DARTS), Volume 3, Issue 2, pp. 4:1-4:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@Article{delbianco_et_al:DARTS.3.2.4,
author = {Delbianco, Germ\'{a}n Andr\'{e}s and Sergey, Ilya and Nanevski, Aleksandar and Banerjee, Anindya},
title = {{Concurrent Data Structures Linked in Time (Artifact)}},
pages = {4:1--4:4},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2017},
volume = {3},
number = {2},
editor = {Delbianco, Germ\'{a}n Andr\'{e}s and Sergey, Ilya and Nanevski, Aleksandar and Banerjee, Anindya},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.3.2.4},
URN = {urn:nbn:de:0030-drops-72850},
doi = {10.4230/DARTS.3.2.4},
annote = {Keywords: separation logic, linearization Points, concurrent snapshots, FCSL}
}
Document
Towards Strong Normalization for Dependent Object Types (DOT) (Artifact)
Abstract
This artifact provides the fully mechanized proof of strong normalization for D_{<:} , a variant of (Dependent Object Types) DOT (Rompf & Amin, 2016) that excludes recursive functions and recursive types. The intersection type and recursive self type are further integrated, moving towards DOT. The key proof idea follows the method of Girard (Girard, 1972) and Tait (Tait, 1967).
Cite as
Fei Wang and Tiark Rompf. Towards Strong Normalization for Dependent Object Types (DOT) (Artifact). In Special Issue of the 31st European Conference on Object-Oriented Programming (ECOOP 2017). Dagstuhl Artifacts Series (DARTS), Volume 3, Issue 2, pp. 5:1-5:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@Article{wang_et_al:DARTS.3.2.5,
author = {Wang, Fei and Rompf, Tiark},
title = {{Towards Strong Normalization for Dependent Object Types (DOT) (Artifact)}},
pages = {5:1--5:3},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2017},
volume = {3},
number = {2},
editor = {Wang, Fei and Rompf, Tiark},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.3.2.5},
URN = {urn:nbn:de:0030-drops-72869},
doi = {10.4230/DARTS.3.2.5},
annote = {Keywords: Scala, DOT, strong normalization, logical relations, recursive types}
}
Document
Contracts in the Wild: A Study of Java Programs (Artifact)
Abstract
This artefact contains a dataset of open-source programs obtained from the Maven Central Repository and scripts that first extract contracts from these programs and then perform several analyses on the contracts extracted. The extraction and analysis is fully automated and directly produces the tables presented in the accompanying paper.
The results show how contracts are used in real-world program, and how their usage changes between versions and within inheritance hierarchies.
Cite as
Jens Dietrich, David J. Pearce, Kamil Jezek, and Premek Brada. Contracts in the Wild: A Study of Java Programs (Artifact). In Special Issue of the 31st European Conference on Object-Oriented Programming (ECOOP 2017). Dagstuhl Artifacts Series (DARTS), Volume 3, Issue 2, pp. 6:1-6:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@Article{dietrich_et_al:DARTS.3.2.6,
author = {Dietrich, Jens and Pearce, David J. and Jezek, Kamil and Brada, Premek},
title = {{Contracts in the Wild: A Study of Java Programs (Artifact)}},
pages = {6:1--6:4},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2017},
volume = {3},
number = {2},
editor = {Dietrich, Jens and Pearce, David J. and Jezek, Kamil and Brada, Premek},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.3.2.6},
URN = {urn:nbn:de:0030-drops-72871},
doi = {10.4230/DARTS.3.2.6},
annote = {Keywords: verification, design-by-contract, assertions, preconditions, postconditions, runtime checking, java, input validation}
}
Document
Parallelizing Julia with a Non-Invasive DSL (Artifact)
Abstract
This artifact is based on ParallelAccelerator, an embedded domain-specific language (DSL) and compiler for speeding up compute-intensive Julia programs. In particular, Julia code that makes heavy use of aggregate array operations is a good candidate for speeding up with ParallelAccelerator. ParallelAccelerator is a non-invasive DSL that makes as few changes to the host programming model as possible.
Cite as
Todd A. Anderson, Hai Liu, Lindsey Kuper, Ehsan Totoni, Jan Vitek, and Tatiana Shpeisman. Parallelizing Julia with a Non-Invasive DSL (Artifact). In Special Issue of the 31st European Conference on Object-Oriented Programming (ECOOP 2017). Dagstuhl Artifacts Series (DARTS), Volume 3, Issue 2, pp. 7:1-7:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@Article{anderson_et_al:DARTS.3.2.7,
author = {Anderson, Todd A. and Liu, Hai and Kuper, Lindsey and Totoni, Ehsan and Vitek, Jan and Shpeisman, Tatiana},
title = {{Parallelizing Julia with a Non-Invasive DSL (Artifact)}},
pages = {7:1--7:2},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2017},
volume = {3},
number = {2},
editor = {Anderson, Todd A. and Liu, Hai and Kuper, Lindsey and Totoni, Ehsan and Vitek, Jan and Shpeisman, Tatiana},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.3.2.7},
URN = {urn:nbn:de:0030-drops-72888},
doi = {10.4230/DARTS.3.2.7},
annote = {Keywords: parallelism, scientific computing, domain-specific languages, Julia}
}
Document
Mixed Messages: Measuring Conformance and Non-Interference in TypeScript (Artifact)
Abstract
In the paper Mixed Messages: Measuring Conformance and Non-Interference in TypeScript we present our experiences of evaluating gradual typing using our tool TypeScript TPD. The tool, based on the polymorphic blame calculus, monitors JavaScript libraries and TypeScript clients against the corresponding TypeScript definition. Our experiments yield two conclusions. First, TypeScript definitions are prone to error. Second, there are serious technical concerns with the use of the JavaScript proxy mechanism for enforcing contracts. This artifact includes all the libraries we tested, their definition files, and the source code of our tool. From this, all libraries can be wrapped and tested to reproduce the log data that formed our conclusion. All conformance errors and examples of interference are documented, and can be verified against the generated logs.
Cite as
Jack Williams, J. Garrett Morris, Philip Wadler, and Jakub Zalewski. Mixed Messages: Measuring Conformance and Non-Interference in TypeScript (Artifact). In Special Issue of the 31st European Conference on Object-Oriented Programming (ECOOP 2017). Dagstuhl Artifacts Series (DARTS), Volume 3, Issue 2, pp. 8:1-8:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@Article{williams_et_al:DARTS.3.2.8,
author = {Williams, Jack and Morris, J. Garrett and Wadler, Philip and Zalewski, Jakub},
title = {{Mixed Messages: Measuring Conformance and Non-Interference in TypeScript (Artifact)}},
pages = {8:1--8:2},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2017},
volume = {3},
number = {2},
editor = {Williams, Jack and Morris, J. Garrett and Wadler, Philip and Zalewski, Jakub},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.3.2.8},
URN = {urn:nbn:de:0030-drops-72899},
doi = {10.4230/DARTS.3.2.8},
annote = {Keywords: gradual typing, TypeScript, JavaScript, proxies}
}
Document
Type Abstraction for Relaxed Noninterference (Artifact)
Abstract
This artifact is a web interpreter for the ObSec language defined in the companion paper. ObSec is a simple object-oriented language that supports type-based declassification. Type-base declassification exploits the familiar notion of type abstraction to support expressive declassification policies in a simple and expressive manner.
Cite as
Raimil Cruz, Tamara Rezk, Bernard Serpette, and Éric Tanter. Type Abstraction for Relaxed Noninterference (Artifact). In Special Issue of the 31st European Conference on Object-Oriented Programming (ECOOP 2017). Dagstuhl Artifacts Series (DARTS), Volume 3, Issue 2, pp. 9:1-9:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@Article{cruz_et_al:DARTS.3.2.9,
author = {Cruz, Raimil and Rezk, Tamara and Serpette, Bernard and Tanter, \'{E}ric},
title = {{Type Abstraction for Relaxed Noninterference (Artifact)}},
pages = {9:1--9:2},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2017},
volume = {3},
number = {2},
editor = {Cruz, Raimil and Rezk, Tamara and Serpette, Bernard and Tanter, \'{E}ric},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.3.2.9},
URN = {urn:nbn:de:0030-drops-72902},
doi = {10.4230/DARTS.3.2.9},
annote = {Keywords: type abstraction, relaxed noninterference, information flow control}
}
Document
EVF: An Extensible and Expressive Visitor Framework for Programming Language Reuse (Artifact)
Abstract
This artifact is based on EVF, an extensible and expressive Java visitor framework. EVF aims at reducing the effort involved in creation and reuse of programming languages. EVF an annotation processor that automatically generate boilerplate ASTs and AST for a given an Object Algebra interface. This artifact contains source code of the case study on "Types and Programming Languages", illustrating how effective EVF is in modularizing programming languages. There is also a microbenchmark in the artifact that shows that EVF has reasonable performance with respect to traditional visitors.
Cite as
Weixin Zhang and Bruno C. d. S. Oliveira. EVF: An Extensible and Expressive Visitor Framework for Programming Language Reuse (Artifact). In Special Issue of the 31st European Conference on Object-Oriented Programming (ECOOP 2017). Dagstuhl Artifacts Series (DARTS), Volume 3, Issue 2, pp. 10:1-10:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@Article{zhang_et_al:DARTS.3.2.10,
author = {Zhang, Weixin and Oliveira, Bruno C. d. S.},
title = {{EVF: An Extensible and Expressive Visitor Framework for Programming Language Reuse (Artifact)}},
pages = {10:1--10:2},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2017},
volume = {3},
number = {2},
editor = {Zhang, Weixin and Oliveira, Bruno C. d. S.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.3.2.10},
URN = {urn:nbn:de:0030-drops-72918},
doi = {10.4230/DARTS.3.2.10},
annote = {Keywords: visitor pattern, object algebras, modularity, domain-specific languages}
}
Document
Mailbox Abstractions for Static Analysis of Actor Programs (Artifact)
Abstract
This artifact is based on Scala-AM, a static analysis framework relying on the Abstracting Abstract Machines approach. This version of the framework is extended to support actor-based programs, written in a variant of Scheme. The sound static analysis is performed in order to verify the absence of errors in actor-based program, and to compute upper bounds on actor's mailboxes. We developed several mailbox abstractions with which the static analysis can be run, and evaluate the precision of the technique with these mailbox abstractions. This artifact contains documentation on how to use analysis and on how to reproduce the results presented in the companion paper.
Cite as
Quentin Stiévenart, Jens Nicolay, Wolfgang De Meuter, and Coen De Roover. Mailbox Abstractions for Static Analysis of Actor Programs (Artifact). In Special Issue of the 31st European Conference on Object-Oriented Programming (ECOOP 2017). Dagstuhl Artifacts Series (DARTS), Volume 3, Issue 2, pp. 11:1-11:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@Article{stievenart_et_al:DARTS.3.2.11,
author = {Sti\'{e}venart, Quentin and Nicolay, Jens and De Meuter, Wolfgang and De Roover, Coen},
title = {{Mailbox Abstractions for Static Analysis of Actor Programs (Artifact)}},
pages = {11:1--11:2},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2017},
volume = {3},
number = {2},
editor = {Sti\'{e}venart, Quentin and Nicolay, Jens and De Meuter, Wolfgang and De Roover, Coen},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.3.2.11},
URN = {urn:nbn:de:0030-drops-72920},
doi = {10.4230/DARTS.3.2.11},
annote = {Keywords: static analysis, abstraction, abstract interpretation, actors, mailbox}
}
Document
Data Exploration through Dot-driven Development (Artifact)
Abstract
This artifact presents The Gamma, a simple programming environment for data exploration that uses member access as the primary mechanism for constructing queries. The artifact consists of two parts. The user facing web-based component allows users to explore a simple dataset of Olympic medal winners while a back-end service provides the data and evaluates queries executed by the user.
The purpose of the artifact is to illustrate the pivot type provider, which provides a simple way for constructing queries in a object-based programming language equipped with member access. The pivot type provider can be use to construct new queries from code or using the user interface, but it also encourages the user to modify existing code.
Cite as
Tomas Petricek. Data Exploration through Dot-driven Development (Artifact). In Special Issue of the 31st European Conference on Object-Oriented Programming (ECOOP 2017). Dagstuhl Artifacts Series (DARTS), Volume 3, Issue 2, pp. 12:1-12:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@Article{petricek:DARTS.3.2.12,
author = {Petricek, Tomas},
title = {{Data Exploration through Dot-driven Development (Artifact)}},
pages = {12:1--12:2},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2017},
volume = {3},
number = {2},
editor = {Petricek, Tomas},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.3.2.12},
URN = {urn:nbn:de:0030-drops-72936},
doi = {10.4230/DARTS.3.2.12},
annote = {Keywords: data science, type providers, pivot tables, aggregation}
}
Document
Evil Pickles: DoS Attacks Based on Object-Graph Engineering (Artifact)
Abstract
This artefact demonstrates the effects of the serialisation vulnerabilities described in the companion paper. It is composed of three components: scripts, including source code, for Java, Ruby and C# serialisation-vulnerabilities, two case studies that demonstrate attacks based on the vulnerabilities, and a contracts-based mitigation strategy for serialisation-based attacks on Java applications. The artefact allows users to witness how the serialisation-based vulnerabilities result in behavior that can be used in security attacks. It also supports the repeatability of the case study experiments and the benchmark for the mitigation measures proposed in the paper. Instructions for running the tasks are provided along with a description of the artefact setup.
Cite as
Jens Dietrich, Kamil Jezek, Shawn Rasheed, Amjed Tahir, and Alex Potanin. Evil Pickles: DoS Attacks Based on Object-Graph Engineering (Artifact). In Special Issue of the 31st European Conference on Object-Oriented Programming (ECOOP 2017). Dagstuhl Artifacts Series (DARTS), Volume 3, Issue 2, pp. 13:1-13:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@Article{dietrich_et_al:DARTS.3.2.13,
author = {Dietrich, Jens and Jezek, Kamil and Rasheed, Shawn and Tahir, Amjed and Potanin, Alex},
title = {{Evil Pickles: DoS Attacks Based on Object-Graph Engineering (Artifact)}},
pages = {13:1--13:3},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2017},
volume = {3},
number = {2},
editor = {Dietrich, Jens and Jezek, Kamil and Rasheed, Shawn and Tahir, Amjed and Potanin, Alex},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.3.2.13},
URN = {urn:nbn:de:0030-drops-72944},
doi = {10.4230/DARTS.3.2.13},
annote = {Keywords: serialisation, denial of service, degradation of service, Java, C#, JavaScript, Ruby, vulnerabilities, library design, collection libraries}
}
Document
Interprocedural Specialization of Higher-Order Dynamic Languages Without Static Analysis (Artifact)
Abstract
This artifact is based on LC, a research oriented JIT compiler for Scheme. The compiler is extended to allow interprocedural, type based, code specialization using the technique and its implementation presented in the paper. Because the technique is directly implemented in LC, the package contains the build of the compiler used for our experiments. To support repeatability, the artifact allows the user to easily extract the data presented in the paper such as the number of executed type checks or the generated code size. The user can repeat the experiments using a set of standard benchmarks as well as its own programs. Instructions for building the compiler from scratch are also provided.
Cite as
Baptiste Saleil and Marc Feeley. Interprocedural Specialization of Higher-Order Dynamic Languages Without Static Analysis (Artifact). In Special Issue of the 31st European Conference on Object-Oriented Programming (ECOOP 2017). Dagstuhl Artifacts Series (DARTS), Volume 3, Issue 2, pp. 14:1-14:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@Article{saleil_et_al:DARTS.3.2.14,
author = {Saleil, Baptiste and Feeley, Marc},
title = {{Interprocedural Specialization of Higher-Order Dynamic Languages Without Static Analysis (Artifact)}},
pages = {14:1--14:2},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2017},
volume = {3},
number = {2},
editor = {Saleil, Baptiste and Feeley, Marc},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.3.2.14},
URN = {urn:nbn:de:0030-drops-72952},
doi = {10.4230/DARTS.3.2.14},
annote = {Keywords: just-in-time compilation, interprocedural optimization, dynamic language, higher-order function, scheme}
}
Document
Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris (Artifact)
Abstract
This artifact provides the soundness proofs for the encodings in Iris the RSL and GPS logics, as well as the verification for all standard examples known to be verifiable in those logics. All of these proofs are formalized in Coq, which is the main content of this artifact. The formalization is provided in a virtual machine for the convenience of testing, but can also be built from source.
Cite as
Jan-Oliver Kaiser, Hoang-Hai Dang, Derek Dreyer, Ori Lahav, and Viktor Vafeiadis. Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris (Artifact). In Special Issue of the 31st European Conference on Object-Oriented Programming (ECOOP 2017). Dagstuhl Artifacts Series (DARTS), Volume 3, Issue 2, pp. 15:1-15:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@Article{kaiser_et_al:DARTS.3.2.15,
author = {Kaiser, Jan-Oliver and Dang, Hoang-Hai and Dreyer, Derek and Lahav, Ori and Vafeiadis, Viktor},
title = {{Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris (Artifact)}},
pages = {15:1--15:2},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2017},
volume = {3},
number = {2},
editor = {Kaiser, Jan-Oliver and Dang, Hoang-Hai and Dreyer, Derek and Lahav, Ori and Vafeiadis, Viktor},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.3.2.15},
URN = {urn:nbn:de:0030-drops-72966},
doi = {10.4230/DARTS.3.2.15},
annote = {Keywords: weak memory models, release-acquire, concurrency, separation logic}
}
Document
Proactive Synthesis of Recursive Tree-to-String Functions from Examples (Artifact)
Abstract
This artifact, named Prosy, is an interactive command-line tool for synthesizing recursive tree-to-string functions (e.g. pretty-printers) from examples. Specifically, Prosy takes as input a Scala file containing a hierarchy of abstract and case classes, and synthesizes the printing function after interacting with the user. Prosy first pro-actively generates a finite set of trees such that their string representations uniquely determine the function to synthesize. While asking the output for each example, Prosy prunes away questions when it can infer their answers from previous answers. In the companion paper, we prove that this pruning allows Prosy not to require that the user provides answers to the entire set of questions, which is of size O(n^3) where n is the size of the input file, but only to a reasonably small subset of size O(n). Furthermore, Prosy guides the interaction by providing suggestions whenever it can.
Cite as
Mikaël Mayer, Jad Hamza, and Viktor Kuncak. Proactive Synthesis of Recursive Tree-to-String Functions from Examples (Artifact). In Special Issue of the 31st European Conference on Object-Oriented Programming (ECOOP 2017). Dagstuhl Artifacts Series (DARTS), Volume 3, Issue 2, pp. 16:1-16:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@Article{mayer_et_al:DARTS.3.2.16,
author = {Mayer, Mika\"{e}l and Hamza, Jad and Kuncak, Viktor},
title = {{Proactive Synthesis of Recursive Tree-to-String Functions from Examples (Artifact)}},
pages = {16:1--16:2},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2017},
volume = {3},
number = {2},
editor = {Mayer, Mika\"{e}l and Hamza, Jad and Kuncak, Viktor},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.3.2.16},
URN = {urn:nbn:de:0030-drops-72970},
doi = {10.4230/DARTS.3.2.16},
annote = {Keywords: programming by example, active learning, program synthesis}
}