Powered by
2016 ACM SIGPLAN International Conference on Systems, Programming, Languages and Applications: Software for Humanity (SPLASH Companion 2016),
October 30 – November 4, 2016,
Amsterdam, Netherlands
Doctoral Symposium
Dedicated Support for Analyses and Optimizations in Language Workbenches
Tamás Szabó
(itemis, Germany; Delft University of Technology, Netherlands)
Language workbenches are widely used to implement domain-specific languages (DSLs) and their accompanying integrated development environments (IDEs). They help to define the abstract syntax, concrete syntax(es), type system, and transformations for the languages. However, there are other language aspects, specifically program analyses and optimizations, that are also crucial to a language implementation, but state-of-the-art language workbenches has only limited support for them. The high implementation effort for these language aspects is justifiable for a general-purpose language (GPL), but is not justifiable for DSLs because of their different development economies.
To this end, I conduct research on dedicated support for analyses and optimizations for DSLs in language workbenches. My main goal is to develop declarative meta-languages that help to define static program analyses and that capture and automate patterns and techniques of optimizations. The research directions are directly driven by industrial need, and upon successful completion, the results would be applied in projects centered around DSLs for high-performance computing (HPC), insurance, and concurrent embedded systems.
@InProceedings{SPLASH Companion16p3,
author = {Tamás Szabó},
title = {Dedicated Support for Analyses and Optimizations in Language Workbenches},
booktitle = {Proc.\ SPLASH Companion},
publisher = {ACM},
pages = {3--5},
doi = {},
year = {2016},
}
Integrating Concerns with Development Environments
Ján Juhár
(Technical University of Košice, Slovakia)
Program comprehension is an essential process in programming and many researchers report that it tends to take up to a half of a programmers' time during their work with a source code. Integrated development environments (IDEs) facilitate this process but there still are only restricted possibilities for narrowing the gap between concerns of a problem domain and a source code that implements them. In our work we utilize projectional properties of modern IDEs to make them able to process concern-related metadata and to provide customizable code projections. These projections preserve the original code structure while they show it from an alternative perspective regarding the contained concerns. We plan to evaluate the effect such code projections will have on program comprehension tasks.
@InProceedings{SPLASH Companion16p6,
author = {Ján Juhár},
title = {Integrating Concerns with Development Environments},
booktitle = {Proc.\ SPLASH Companion},
publisher = {ACM},
pages = {6--8},
doi = {},
year = {2016},
}
Language Support for Verifiable SDNs
Matthias Eichholz
(TU Darmstadt, Germany)
Programming languages for Software-Defined Networks (SDNs) provide higher abstractions on top of hardware-based APIs like OpenFlow.
Researchers started to develop SDN programming languages based on mathematical foundations, which makes these languages amenable to verification and allows network administrators to answer questions about correctness of their policies, reachability within the network and performance of the network.
However, these languages are only able to capture a limited set of properties and lack support for fully automated verification.
In this paper we first highlight different issues of existing programming languages enabling network verification for SDNs and describe ongoing research on a new SDN language that tackles the aforementioned issues.
@InProceedings{SPLASH Companion16p9,
author = {Matthias Eichholz},
title = {Language Support for Verifiable SDNs},
booktitle = {Proc.\ SPLASH Companion},
publisher = {ACM},
pages = {9--11},
doi = {},
year = {2016},
}
VeriTaS: Verification of Type System Specifications: Mechanizing Domain Knowledge about Progress and Preservation Proofs
Sylvia Grewe
(TU Darmstadt, Germany)
Developing a type system with a soundness proof is hard. The VeriTaS project aims at simplifying the development of sound type systems through automation of soundness proofs and through automated derivation of efficient type checkers from sound type system specifications.
Within the VertiTaS project, I focus on developing an interface for the verification of progress and preservation proofs which shall automate standard parts of such proofs. To achieve this, I propose to identify recurring proof strategies in progress and preservation proofs from the literature, to develop a format for abstractly representing these proof strategies, and to mechanize them by connecting them to existing theorem provers.
@InProceedings{SPLASH Companion16p12,
author = {Sylvia Grewe},
title = {VeriTaS: Verification of Type System Specifications: Mechanizing Domain Knowledge about Progress and Preservation Proofs},
booktitle = {Proc.\ SPLASH Companion},
publisher = {ACM},
pages = {12--14},
doi = {},
year = {2016},
}
Scaling Testing of Refactoring Engines
Melina Mongiovi
(Federal University of Campina Grande, Brazil)
Refactoring engines may have overly weak conditions, overly strong conditions, and transformation issues related to the refactoring definitions. We find that 86% of the test suites of Eclipse and JRRT are concerned to those kinds of bugs. However, the engines still have them. Researchers have proposed a number of techniques for testing refactoring engines. Nevertheless, they may have limitations related to the program generator, time consumption, kinds of bugs, automation, and debugging. We propose and implement a technique to scale testing of refactoring engines. We improve expressiveness of a program generator and use a technique to skip some test inputs to improve performance. Moreover, we propose new oracles to detect behavioral changes using change impact analysis, overly strong conditions using mutation testing, and transformation issues. We evaluate our technique in 28 refactoring implementations of Java (Eclipse and JRRT) and C (Eclipse) and find 119 bugs. The technique reduces the time in 96% using skips while missing only 6% of the bugs. Using the new oracle to identify overly strong conditions, it detects more bugs and facilitates the debugging activity different from previous works. Finally, we evaluate refactoring implementations of Eclipse and JRRT using the input programs of their refactoring test suites and find a number of bugs not detected by the developers.
@InProceedings{SPLASH Companion16p15,
author = {Melina Mongiovi},
title = {Scaling Testing of Refactoring Engines},
booktitle = {Proc.\ SPLASH Companion},
publisher = {ACM},
pages = {15--17},
doi = {},
year = {2016},
}
Multitier Reactive Abstractions
Pascal Weisenburger
(TU Darmstadt, Germany)
Distributed applications are traditionally developed using separate modules for each component in the distributed system, which can even be written in different programming languages. Those modules react on events such as user input, which are produced by other modules, and may in turn produce new events to be handled by different modules. Thus, most distributed applications are reactive in nature. Distributed event-based data flow makes it is hard to reason about the system and therefore makes the development of distributed systems challenging.
In this paper, we present language abstractions for distributed reactive programming easing the development of such applications and supporting various distributed architectures.
@InProceedings{SPLASH Companion16p18,
author = {Pascal Weisenburger},
title = {Multitier Reactive Abstractions},
booktitle = {Proc.\ SPLASH Companion},
publisher = {ACM},
pages = {18--20},
doi = {},
year = {2016},
}
Spray: Programming with a Persistent Distributed Heap
Marco Grandi
(University of Pisa, Italy)
Persistence and distribution are two important aspects in distributed applications that are commonly managed explicitly and separately. This paper introduces Spray, a programming paradigm for distributed applications that combines these two concepts in one abstraction: a persistent distributed heap.
@InProceedings{SPLASH Companion16p21,
author = {Marco Grandi},
title = {Spray: Programming with a Persistent Distributed Heap},
booktitle = {Proc.\ SPLASH Companion},
publisher = {ACM},
pages = {21--23},
doi = {},
year = {2016},
}
Towards Practical Release-Level Dynamic Software Updating on Stock Java: Evaluating an Efficient and Safely Programmable Java Dynamic Updating System
Martin Alexander Neumann
(KIT, Germany)
Towards more usable dynamic software updating on stock Java, we propose (1) a programming model that transformation code can be statically type-checked against, also featuring type-safe execution of transformation code; (2) an efficient checkpointable eager state transformation approach that avoids hazards of deadlocks and data-races when transformation code is executed, also allowing to seamlessly abort an update if any exception occurs; and (3) a programming approach based on assertions to abort dynamic updates if assumptions of transformation code are not met. We implement the three aspects in a dynamic updating system to study their performance and usability.
@InProceedings{SPLASH Companion16p24,
author = {Martin Alexander Neumann},
title = {Towards Practical Release-Level Dynamic Software Updating on Stock Java: Evaluating an Efficient and Safely Programmable Java Dynamic Updating System},
booktitle = {Proc.\ SPLASH Companion},
publisher = {ACM},
pages = {24--26},
doi = {},
year = {2016},
}
proc time: 0.99