SLE (Software Language Engineering) 2020

Link to Publication: http://design.cs.iastate.edu/splash20/gpce20/gpce20foreword-fm001-p.pdf

Best Paper Award

This paper is concerned with synthesizing programs based on black-box oracles: we are interested in the case where there exists an executable implementation of a component or library, but its internal structure is unknown. We are provided with just an API or function signature, and aim to synthesize a program with equivalent behavior.

To attack this problem, we detail Presyn: a program synthesizer designed for flexible interoperation with existing programs and compiler toolchains. Presyn uses high-level imperative control-flow structures and a pair of cooperating predictive models to efficiently narrow the space of potential programs. These models can be trained effectively on small corpora of synthesized examples.

We evaluate Presyn against five leading program synthesizers on a collection of 112 synthesis benchmarks collated from previous studies and real-world software libraries. We show that Presyn is able to synthesize a wider range of programs than each of them with less human input. We demonstrate the application of our approach to real-world code and software engineering problems with two case studies: accelerator library porting and detection of duplicated library reimplementations.

Link to Publication: http://design.cs.iastate.edu/splash20/gpce20/gpce20main-p2-p.pdf

Bruce Collie

University of Edinburgh

Jackson Woodruff

University of Edinburgh

Michael F. P. O'Boyle

University of Edinburgh

The Stratego language supports program transformation by means of term rewriting with programmable rewriting strategies. Stratego's traversal primitives support concise definition of generic tree traversals. Stratego is a dynamically typed language because its features cannot be captured fully by a static type system. While dynamic typing makes for a flexible programming model, it also leads to unintended type errors, code that is harder to maintain, and missed opportunities for optimization.

In this paper, we introduce a gradual type system for Stratego that combines the flexibility of dynamically typed generic programming, where needed, with the safety of statically declared and enforced types, where possible. To make sure that statically typed code cannot go wrong, all access to statically typed code from dynamically typed code is protected by dynamic type checks (casts). The type system is backwards compatible such that types can be introduced incrementally to existing Stratego programs. We formally define a type system for Core Gradual Stratego, discuss its implementation in a new type checker for Stratego, and present an evaluation of its impact on Stratego programs.

Link to Publication: http://design.cs.iastate.edu/splash20/sle20/sle20main-p4-p.pdf

Jeff Smits

Delft University of Technology, Netherlands

Netherlands

Eelco Visser

Delft University of Technology

Model-based development approaches, such as Model-Driven Engineering (MDE), heavily rely on the use of modelling languages to achieve and automate software development tasks. To enable the definition of model variants (e.g., supporting the compact description of system families),
one solution is to combine MDE with Software Product Lines. However, this is technically costly as it requires adapting many MDE artefacts associated to the modelling language – especially the meta-models and graphical environments.
To alleviate this situation, we propose a method for the automated injection of variability into graphical modelling languages. Given the meta-model and graphical environment of a particular language, our approach permits configuring the allowed model variability, and the graphical environment is automatically adapted to enable creating models with variability. Our solution is implemented atop the Eclipse Modeling Framework and Sirius, and synthesizes adapted graphical editors integrated with FeatureIDE.

Link to Publication: http://design.cs.iastate.edu/splash20/gpce20/gpce20main-p13-p.pdf

Antonio Garmendia

JKU Linz

Austria

Manuel Wimmer

JKU Linz

Austria

Esther Guerra

Autonomous University of Madrid

Elena Gómez-Martínez

Autonomous University of Madrid

Juan de Lara

Autonomous University of Madrid

Spain

Integrated Development Environments (IDEs) are indispensable companions to programming languages. They are increasingly turning towards Web-based infrastructure. The rise of a protocol such as the Language Server Protocol (LSP) that standardizes the separation between a language-agnostic IDE, and a language server that provides all language services (\emph{e.g.,} auto completion, compiler…) has allowed the emergence of high quality generic Web components to build the IDE part that runs in the browser. However, all language services require different computing capacities and response times to guarantee a user-friendly experience within the IDE. The monolithic distribution of all language services prevents to leverage on the available execution platforms (e.g., local platform, application server, cloud). In contrast with the current approaches that provide IDEs in the form of a monolithic client-server architecture, we explore in this paper the modularization of all language services to support their individual deployment and dynamic adaptation within an IDE. We evaluate the performance impact of the distribution of the language services across the available execution platforms on four EMF-based languages, and demonstrate the benefit of a custom distribution.

Link to Publication: http://design.cs.iastate.edu/splash20/sle20/sle20main-p91-p.pdf

Fabien Coulon

Obeo, France / University of Rennes, France / Inria, France / CNRS, France / IRISA, France

Alex Auvolat

University of Rennes, France / Inria, France / CNRS, France / IRISA, France

Benoit Combemale

University of Rennes, France / Inria, France / CNRS, France / IRISA, France

France

Yérom-David Bromberg

University of Rennes, France / Inria, France / CNRS, France / IRISA, France

François Taïani

University of Rennes, France / Inria, France / CNRS, France / IRISA, France

Olivier Barais

University of Rennes, France / Inria, France / CNRS, France / IRISA, France

Noël Plouzeau

University of Rennes, France / Inria, France / CNRS, France / IRISA, France

Software product lines are increasingly used to handle the growing demand of custom-tailored software variants. They provide systematic reuse of software paired with variability mechanisms in the code to implement whole product families rather than single software products. A common domain of application for product lines are safety-critical systems, which require behavioral correctness to avoid dangerous situations in-field. While most approaches concentrate on post-hoc verification for product lines, we argue that a stepwise approach to create correct programs may be beneficial for developers to manage the growing variability. Correctness-by-construction is such a stepwise approach to create programs using a set of small, tractable refinement rules that guarantee the correctness of the program with regard to its specification. In this paper, we propose the first approach to develop correct-by-construction software product lines using feature-oriented programming. First, we extend correctness-by-construction by two refinement rules for variation points in the code. Second, we give a proof for the soundness of the proposed rules. Third, we implement our technique in a tool called VarCorC and show the applicability of the tool by conducting two case studies.

Link to Publication: http://design.cs.iastate.edu/splash20/gpce20/gpce20main-p17-p.pdf

Tabea Bordis

TU Braunschweig

Tobias Runge

TU Braunschweig

Ina Schaefer

TU Braunschweig

Germany

Simulation is a key tool for researching complex system behaviour. Agent-based simulation has been applied across domains, such as biology, health, economics and urban sciences. However, engineering robust, efficient, maintainable, and reliable agent-based simulations is challenging. We present a vision for engineering agent simulations comprising a family of domain-specific modelling languages (DSMLs) that integrates core software engineering, validation and simulation experimentation. We relate the vision to examples of principled simulation, to show how the DSMLs would improve robustness, efficiency, and maintainability of simulations. Focusing on how to demonstrate the fitness for purpose of a simulator, the envisaged approach supports bi-directional transparency and traceability between the original domain understanding to the implementation, interpretation of results and evaluation of hypotheses.

Link to Publication: http://design.cs.iastate.edu/splash20/sle20/sle20main-p8-p.pdf

Steffen Zschaler

King's College London

United Kingdom

Fiona Polack

Keele University

Multi-stage programming (MSP) holds great promise, allowing the reliable generation of specialized, partially-evaluated
code with static type- and scope-safety guarantees. Yet, we
argue that MSP has not reached its full potential yet, as it has
been traditionally limited to generating expressions, and has
lacked principled facilities for generating modular programs
and data structures. In that sense, we argue that MSP has
been reserved for programming “in the small,” focused on
generating efficient kernels of computation on the scale of
single function bodies. We present a novel technique called
staged classes, which extends MSP with the ability to manipulate class definitions as first-class constructs. This lets
programmers use MSP “in the large,” on the level of applications, rather than mere functions. This way, applications
can be designed in an abstract and modular way without
runtime cost, as staged classes guarantee the removal of all
staging-time abstractions, resulting in the generation of efficient specialized modules and data structures. We describe
the design of a prototype relational database system in Scala,
which uses several stages of runtime compilation to maximize the efficiency of query execution and data storage. We
also show that staged classes can be used for defining type- and scope-safe implementations of type providers.

Link to Publication: http://design.cs.iastate.edu/splash20/gpce20/gpce20main-p32-p.pdf

Lionel Parreaux

EPFL

Switzerland

Amir Shaikhha

University of Edinburgh

Many techniques in software language engineering get their first validation by being prototyped to work on one particular language such as Java, Scala, Scheme, or ML, or a subset of such a language. Claims of their generalisability, as well as discussion on potential threats to their external validity, are often based on authors' ad hoc understanding of the world outside their usual comfort zone. To facilitate and simplify such discussions by providing a solid measurable ground, we propose a language called BabyCobol, which was specifically designed to contain features that turn processing legacy programming languages such as COBOL, FORTRAN, PL/I, REXX, CLIST, and 4GLs (fourth generation languages), into such a challenge. The language is minimal by design so that it can help to quickly find weaknesses in frameworks making them inapplicable to dealing with legacy software. However, applying new techniques of software language engineering and reverse engineering to such a small language will not be too tedious and overwhelming. BabyCobol was designed in collaboration with industrial compiler developers by systematically traversing features of several second, third and fourth generation languages to identify the core culprits in making development of compiler for legacy languages difficult.

Link to Publication: http://design.cs.iastate.edu/splash20/sle20/sle20main-p27-p.pdf

Vadim Zaytsev

University of Twente, Netherlands

Netherlands

Language-integrated query has attracted much attention from researchers and engineers. It enables one to write a database query with high-level abstractions, which makes it possible to compose, iterate, and reuse queries. An important issue in language-integrated query is the N+1 query problem, and Cheney et al. proposed a program-transformation approach to solve it for a core language of Microsoft’s LINQ. In our previous work, we extended their language to grouping (GROUP BY in SQL) and aggregate functions, and showed that any term can be transformed to a single SQL query. It still has a problem in that the resulting queries may be unnecessarily large and inefficient.

This paper solves the problem. Our key idea is re-organization of queries with nested control structures. While our previous work decomposes grouping into finer primitives before transformation, the new algorithm fuses nested control structures after transformation, while keeping the absence of nested data structures. Our algorithm also eliminates correlated subqueries as much as possible, to obtain better performance. We have conducted performance measurements, which shows that our new algorithm reduces the size of generated queries and improves the performance for several examples.

Link to Publication: http://design.cs.iastate.edu/splash20/gpce20/gpce20main-p30-p.pdf

Rui Okura

University of Tsukuba

Yukiyoshi Kameyama

University of Tsukuba

Japan

Reference attribute grammars (RAGs) have reached a level of maturity where they are supported by several tools, and have gained traction in both academic and industrial language tool development. However, despite a lot of accumulated knowledge of how to best develop RAGs in practice, there is limited support to guide practitioners.

In this paper, we address this issue by focusing on one RAG tool, JastAdd, and by defining principles and patterns for development of RAGs with this tool. We evaluate the proposed principles and patterns with an exploratory empirical study with 14 practitioners, with a mix of beginners and experienced users from both academia and industry. The results indicate that the principles and patterns capture the practice of developing JastAdd RAGs well, help practitioners to become aware of useful patterns, and provide a common language to more efficiently reason about the practice of developing JastAdd RAGs.

Link to Publication: http://design.cs.iastate.edu/splash20/sle20/sle20main-p32-p.pdf

Niklas Fors

Lund University

Emma Söderberg

Lund University

Sweden

Görel Hedin

Lund University

GUIs often contain structures that are incidental, not properly manipulatable through well-defined APIs. For example, modifying a list of items in a GUI's model may require extraneous bookkeeping operations in the view, such as adding and removing event handlers, and updating the menu structure. Observing GUIs in practice gives an indication that programmers may find it difficult or tedious to implement complete and convenient sets of operations for manipulating various structures: useful operations for adding, inserting, swapping, or reordering elements are often missing, inconsistent, or limited. This paper introduces a DSL for programming operations that manipulate such incidental structures. The programmer specifies structures via relations between elements, concretely by defining methods that unestablish and establish a relation. This gives the programmer an ability to describe structural transformations via rules that control which relations should hold before and after a rule is applied. The API for structure manipulation is generated from these rules. Our DSL can give an abstract view on ad-hoc structures, making it easier to provide the necessary set of operations for their convenient manipulation.

Link to Publication: http://design.cs.iastate.edu/splash20/gpce20/gpce20main-p11-p.pdf

Knut Anders Stokke

University of Bergen

Mikhail Barash

University of Bergen

Norway

Jaakko Järvi

University of Turku

Norway

Block-based programming systems employ a jigsaw metaphor to write programs.
They are popular in the domain of programming education (e.g., Scratch), but also used as a programming interface for end-users in other disciplines, such as arts, robotics, and configuration management.
In particular, block-based environments promise a convenient interface for Domain-Specific Languages (DSLs) for domain experts who might lack a traditional programming education.
However, building a block-based environment for a DSL from scratch requires significant effort.

This paper presents an approach to engineer block-based language interfaces by reusing existing language artifacts.
We present Kogi, a tool for deriving block-based environments from context-free grammars.
We identify and define the abstract structure for describing block-based environments.
Kogi transforms a context-free grammar into this structure, which then generates a block-based environment based on Google Blockly.
The approach is illustrated with four case studies, a DSL for state machines, Sonification Blocks (a DSL for sound synthesis), Pico (a simple programming language), and QL (a DSL for questionnaires).
The results show that usable block-based environments can be derived from context-free grammars, and with an order of magnitude reduction in effort.

Link to Publication: http://design.cs.iastate.edu/splash20/sle20/sle20main-p106-p.pdf

Mauricio Verano Merino

Technische Universiteit Eindhoven

Netherlands

Tijs van der Storm

CWI & University of Groningen, Netherlands

Netherlands

Satisfying real-time requirements in cyber-physical systemsis challenging as timing behaviour depends on the applica-tion software, the embedded hardware, as well as the exe-cution environment. This challenge is exacerbated as real-world, industrial systems often use unpredictable hardwareand software libraries or operating systems with timing haz-ards and proprietary device drivers. All these issues limitor entirely prevent the application of established real-timeanalysis techniques.

This paper describes PReGO, a partially generative method-ology for satisfying real-time requirements in industrial usecases developed without real-time techniques in mind. Weapply our methodology to a Search & Rescue applicationrunning on a fixed-wing drone with COTS components, in-cluding a NVIDIA Jetson board and a stock Ubuntu/Linux.We empirically evaluate the impact of each integration stepand demonstrate the effectiveness of our methodology inmeeting real-time application requirements in terms of dead-line misses and energy consumption.

Link to Publication: http://design.cs.iastate.edu/splash20/gpce20/gpce20main-p9-p.pdf

Benjamin Rouxel

University of Amsterdam

Ulrik Pagh Schultz

University of Southern Denmark

Benny Akesson

University of Amsterdam / TNO

Jesper Holst

Sky-Watch

Ole Jørgensen

Sky-Watch

Clemens Grelck

University of Amsterdam

Netherlands

We present a type system over language definitions that classifies parts of the operational semantics of a language in input, and
models a common language design organization.
The resulting typing discipline guarantees that the language at hand is automatically type sound.

Thanks to the use of types to model language design,
our type checker has a high-level view on the language being
analyzed and can report messages using the same jargon of language designers.

We have implemented our type system in the $\textsc{lang-n-check}$ tool, and we have applied it to derive the type soundness of several functional languages, including those with recursive types, polymorphism, exceptions, lists, sums, and several common types and operators.

Link to Publication: http://design.cs.iastate.edu/splash20/sle20/sle20main-p44-p.pdf

Matteo Cimini

University of Massachusetts at Lowell, USA

United States

Dale Miller

Inria, France / École Polytechnique, France

France

Jeremy G. Siek

Indiana University, USA

United States

Programmers declare variables to serve specific implementation purposes that we refer to as \emph{variable usage semantics (VUS)}. Understanding VUS is required for various software engineering tasks, including program comprehension, code audits, and vulnerability detection. To help programmers understand VUS, we present a new program analysis that infers a variable’s usage semantics from its textual and context information (e.g., symbolic name, type, scope, information flow). To support this analysis, we introduce VarSem, a domain-specific language, in which a variable’s semantic category is expressed as a set of declarative rules. VarSem’s execution determines which program variables belong to a given semantic category. VarSem translates high-level declarative rules into low-level program analysis techniques, including natural language processing and data flow, and provides a highly extensible architecture for specifying new rules and analysis techniques. We evaluate VarSem with eight real-world systems to identify their personally identifiable information variables. The evaluation results show that VarSem infers variable semantics with satisfying accuracy/precision and passable recall, thus potentially benefiting both software and security engineers.

Link to Publication: http://design.cs.iastate.edu/splash20/gpce20/gpce20main-p36-p.pdf

Yin Liu

Virginia Tech

Eli Tilevich

Virginia Tech

United States

We describe a monadification process for attribute grammars for more concisely written attribute equations, closer to the style of inference rules used in traditional typing and evaluation specifications. Inference rules specifying, for example, a typing relation typically consider only typable expressions, whereas well-defined attribute grammars explicitly determine attribute values for any term, including untypable ones. The monadification approach lets one represent, for example, types as monadic optional/maybe values, but write non-monadic equations over the value inside the monad that only specify the rules for a correct typing, leading to more concise specifications. The missing failure cases are handled by a rewriting that inserts monadic return, bind, and failure operations to produce a well-defined attribute grammar that handles untypable trees. Thus, one can think in terms of a type T and not the actual monadic type M(T). To formalize this notion, typing and evaluation relations are given for the original and rewritten equations. The rewriting is total, preserves types, and a correctness property relating values of original and rewritten equations is given. A prototype implementation illustrates the benefits with examples such as typing of the simply-typed lambda calculus with Booleans, evaluation of the same, and type inference in Caml Light.

Link to Publication: http://design.cs.iastate.edu/splash20/sle20/sle20main-p71-p.pdf

Dawn Michaelson

University of Minnesota

Eric Van Wyk

University of Minnesota, USA

United States

Object-oriented programming, functional programming, and metaprogramming each offer a unique axis of abstraction that enables modular code. Macros, a common technique for metaprogramming, capture ASTs as quotes to let users manipulate them in the host language. However, macros are often at odds with other programming techniques since they can only process code written at the call-site and cannot analyze code behind abstraction boundaries such as variables and methods. Furthermore, the quotes generated for macro expansion exist only at compile-time and cannot be passed around in user code. Multi-stage programming treats quotes as runtime values to address this problem, but introduces the cost of running the compiler when splicing quotes. This forces developers to choose between low runtime overhead and modularity. What if we could have the best of both worlds? We introduce fluid quotes, a new technique that uses dependent types to let users pass quotes through abstraction boundaries in runtime code while splicing them ahead-of-time. This technique enables new metaprogramming capabilities by eliminating the traditional requirement of co-locating parameter expressions with call-sites. Fluid quotes capture not only source code but also associated runtime context to ensure correctness. In addition, they can be composed into larger expressions without any macro code. We demonstrate the capabilities of fluid quotes through two specific applications: optimizing data processing pipelines and making language integrated queries more flexible.

Link to Publication: http://design.cs.iastate.edu/splash20/gpce20/gpce20main-p7-p.pdf

Shadaj Laddad

University of California at Berkeley

Koushik Sen

University of California at Berkeley

United States

This paper presents strategy attributes, a seamless integration of strategic term rewriting into attribute grammars. Strategy attributes are specified using rewrite rules with strategies that control their application. The rules can reference contextual information held in attributes on the trees being rewritten. This use of attributes leads to rewriting on decorated trees instead of undecorated terms. During rewriting, attributes are (lazily) computed on new trees to ensure they are correct with respect to their defining equations. Attributes and strategic rewriting can each be used where most appropriate, thus avoiding the cumbersome aspects of each.

Strategy attributes are essentially higher-order attributes for which the defining equations are automatically generated from the attributes' strategy expressions. They are thus compatible with other attribute grammar features such as reference attributes, forwarding, and attribute flow analyses for well-definedness. A conservative static analysis checks if a strategy is intended to always succeed or to be partial, thus simplifying its use and optimizing its translation. Strategy attributes are demonstrated in the optimization of a simple expression language, evaluation of the lambda calculus, and optimization of strategy attribute translations.

Link to Publication: http://design.cs.iastate.edu/splash20/sle20/sle20main-p75-p.pdf

Lucas Kramer

University of Minnesota

United States

Eric Van Wyk

University of Minnesota, USA

United States

Sriram Rajamani

Microsoft Research

India

Sriram Rajamani is Distinguished Scientist and Managing Director of Microsoft Research India. His research interests are in designing, building and analyzing computer systems in a principled manner. Over the years he has worked on various topics including Hardware and Software Verification, Type Systems, Language Design, Distributed Systems, Security and Privacy. His current research interest is in combining Program Synthesis and Machine Learning. Together with Tom Ball, he was awarded the CAV 2011 Award for “contributions to software model checking, specifically the development of the SLAM/SDV software model checker that successfully demonstrated computer-aided verification techniques on real programs.” Sriram was elected ACM Fellow in 2015 for contributions to software analysis and defect detection. Recently, Sriram has been elected Fellow of Indian National Academy of Engineering. Sriram has a PhD from UC Berkeley, MS from University of Virginia and BEng from College of Engineering, Guindy, all with specialization in Computer Science. Sriram was general chair for POPL 2015 in India, and was program Co-Chair for CAV 2005. He co-founded the Mysore Park Series, and the ISEC conference series in India. He serves on the CACM editorial board as co-chair for special regional sections, to bring computing innovations from around the world to CACM.

Please go to the breakrooms at Clowdr.

Please go to the breakrooms at Clowdr.

Please go to the breakrooms at Clowdr.

Application-level packet filtering is a technique for network access control in which an “application-level gateway” intercepts network packages at the application level (e.g., HTTP, FTP), scans them for security cooncerns and optionally logs, rewrites or discards them. Existing application-level filters express their filtering rules in general-purpose languages, which limits the correctness guarantees available for them.

We present the first declarative language for application-level network filtering, developed at Advenica AB. Our DSL uses security assertions to express properties that packets must have to be allowed through the network (e.g., “IMAP packet contains no executable attachment” or “SQL reply contains only explicitly permitted columns”), along with remedies that either reject or rewrite undesirable packets.

We have designed the language around the needs of network filter developers, with a focus on correctness: our language can statically verify several properties of filter programs, such as well-formedness of the outcome, confluence, and termination, with the help of an off-the-shelf SMT solver.

Our initial results show that the language is sufficiently expressive for a variety of network protocols, closely maps to the application domain, is usable by network filter engineers, and provides strong correctness guarantees.

Link to Publication: http://design.cs.iastate.edu/splash20/gpce20/gpce20main-p10-p.pdf

Hampus Balldin

Advenica

Christoph Reichenbach

Lund University

OCR engines aim to identify and extract text strings fromdocuments or images. While current efforts focus mostly inmainstream languages, there is little support for program-ming or domain-specific languages (DSLs). In this paper, wepresent our vision about the current state of OCR recognitionfor DSLs and its challenges. We discuss some strategies toimprove the OCR quality applied to DSL textual expressionsby leveraging DSL specifications and domain data. To bettersupport our ideas we present the preliminary results of anempirical study and outline a research roadmap.

Link to Publication: http://design.cs.iastate.edu/splash20/sle20/sle20main-p50-p.pdf

Jorge Perianez Pascual

University of Extremadura, Spain

Roberto Rodriguez-Echeverria

University of Extremadura, Spain

Loli Burgueño

Open University of Catalonia, Spain

Jordi Cabot

Open University of Catalonia, Spain

Software systems that share potentially sensitive data are subjected to laws, regulations, policies and/or contracts. The monitoring, control and enforcement processes applied to these systems are currently to a large extent manual, which we rather automate by embedding the processes as dedicated and adaptable software services in order to improve efficiency and effectiveness.
This approach requires such regulatory services to be closely aligned with a formal description of the relevant norms.

This paper presents eFLINT, a domain-specific language developed for formalizing norms. The theoretical foundations of the language are found in transition systems and in Hohfeld’s framework of legal fundamental conceptions. The language can be used to formalize norms from a large variety of sources. The resulting specifications are executable and support several forms of reasoning such as automatic case assessment, manual exploration and simulation. Moreover, the specifications can be used to develop regulatory services for several types of monitoring, control and enforcement. The language is explained through an example, formalizing articles 6(1)(a) and 16 of the General Data Protection Regulation (GDPR). A prototype implementation and formal definition of eFLINT are provided as supplementary material.

Link to Publication: http://design.cs.iastate.edu/splash20/gpce20/gpce20main-p14-p.pdf

L. Thomas van Binsbergen

CWI

Netherlands

Lu-Chi Liu

University of Amsterdam

Robert van Doesburg

Leibniz Institute / University of Amsterdam / TNO

Tom van Engers

Leibniz Institute / University of Amsterdam / TNO

Reducing the energy consumption of a complex, especially cyber-physical, system is a cross-cutting concern through the system layers, and typically requires long feedback loops between experts in several engineering disciplines. Having an immediate automatic estimation of the global system consumption at design-time would significantly accelerate this process, but cross-layer tools are missing in several domains.

Executable domain-specific modeling languages (xDSLs) can be used to design several layers of the system under development in an integrated view. By including the behavioral specification for software and physical components of the system, they are an effective source artifact for cross-layer energy estimation.

In this paper we propose EEL, a language for annotating xDSL primitives with energy-related properties, i.e. how their execution would contribute to the energy consumption on a specific runtime platform.
Given an xDSL, energy specialists create EEL models of that xDSL for each considered runtime platform.
The models are used at design time, to predict the energy consumption of the real systems.
This avoids the need of energetic analysis by deployment and measurement on all runtime platforms, that is slow and expensive.

We augment an existing language workbench for xDSLs with an editor for EEL models and a component that computes energy-consumption estimations during model editing.
The evaluation shows that EEL can be used to represent estimation models from literature, and provide useful predictions.

Link to Publication: http://design.cs.iastate.edu/splash20/sle20/sle20main-p12-p.pdf

Thibault Béziers la Fosse

IMT Atlantique, ICAM

France

Massimo Tisi

Jean-Marie Mottu

Université de Nantes, LS2N, IMT Atlantique

Gerson Sunyé

Université de Nantes, LS2N

Please go to the breakrooms at Clowdr.

AMA

The line between high-assurance and general-purpose software is increasingly blurred, as nowadays nearly any insecure or buggy software can have severe economic consequences. When developers release software, it is critical that there be as few defects (and vulnerabilities) as possible. To check the quality of their code, developers typically write and run test cases, and some may also use static analyses that inspect their code. Yet code is still released with bugs and critical vulnerabilities: testing can not prove the absence of defects, and static analyses often overwhelm developers with false positive reports, making them difficult for the average developer to use. I argue that new dynamic program analyses can act as a force multiplier for developers’ test suites: increasing the number of defects that tests can find without burdening developers with false positive reports. In this talk, I will describe some of my recent work building dynamic analysis systems for taint tracking and checkpointing of JVM-based systems, along with several examples of how these analyses can be integrated with developer-written tests to improve the reliability and fault finding power of those tests.

This talk is given by the recipient of the Dahl Nygaard Junior prize.

The AMA following this talk will be moderated by Gail Kaiser and Darko Marinov.

Jonathan Bell

Northeastern University

Jon is an Assistant Professor directing research in Software Engineering and Software Systems at Northeastern University. His research makes it easier for developers to create reliable and secure software by improving software testing and program analysis. Jon’s work on accelerating software testing has been recognized with an ACM SIGSOFT Distinguished Paper Award (ICSE ’14 – Unit Test Virtualization with VMVM), and was the basis for an industrial collaboration with Electric Cloud. His program analysis research has resulted in several widely adopted runtime systems for the JVM, including the Phosphor taint tracking system (OOPSLA ’14) and CROCHET checkpoint/rollback tool (ECOOP ’18). His research has been funded by the NSA and the NSF, and he is the recipient of the NSF CAREER award. At George Mason, Jon taught courses in distributed systems, web development, and program analysis. His teaching at GMU has been recognized with a departmental award. Jon serves on a variety of program committees and was recently co-chair of the PLDI 2020 Artifact Evaluation Committee. As part of his efforts to broaden the participation of underrepresented groups in computing, Jon co-organizes the PL/SE mentoring workshop at SPLASH (in 2017, 2018, 2019 and 2020).

• A Sparse Iteration Space Transformation Framework for Sparse Tensor Algebra. Ryan Senanayake, Changwan Hong, Ziheng Wang, Amalee Wilson, Stephen Chou, Shoaib Kamil, Saman Amarasinghe, and Fredrik Kjolstad

• Certified and Efficient Instruction Scheduling. Cyril Six, Sylvain Boulmé, and David Monniaux

• CompCertELF: Verified Separate Compilation of C Programs into ELF Object Files. Yuting Wang, Xiangzhe Xu, Pierre Wilke, and Zhong Shao

• Guided Linking: Dynamic Linking without the Costs. Sean Bartell, Will Dietz, and Vikram S. Adve

• Guiding Dynamic Programing via Structural Probability for Accelerating Programming by Example. Ruyi Ji, Yican Sun, Yingfei Xiong, and Zhenjiang Hu

• Incremental Predicate Analysis for Regression Verification. Qianshan Yu, Fei He, and Bow-Yaw Wang

• Learning Semantic Program Embeddings with Graph Interval Neural Network. Yu Wang, Ke Wang, Fengjuan Gao, and Linzhang Wang

• Macros for Domain-Specific Languages. Michael Ballantyne, Alexis King, and Matthias Felleisen

• Precise Inference of Expressive Units of Measurement Types. Tongtong Xiang, Jeff Y. Luo, and Werner Dietl

• Resolution as Intersection Subtyping via Modus Ponens. Koar Marntirosian, Tom Schrijvers, Bruno C. d. S. Oliveira, and Georgios Karachalias

• Revisiting Iso-Recursive Subtyping. Yaoda Zhou, Bruno C. d. S. Oliveira, and Jinxu Zhao

• SATUNE: Synthesizing Efficient SAT Encoders. Hamed Gorjiara, Harry Xu ,and Brian Demsky

• Scaling Exact Inference for Discrete Probabilistic Programs. Steven Holtzen and Guy Van den Broeck, and Todd Millstein

• Statically Verified Refinements for Multiparty Protocols. Fangyi Zhou, Francisco Ferreira, Raymond Hu, Rumyana Neykova, and Nobuko Yoshida

• StreamQL: A Query Language for Processing Streaming Time Series. Lingkun Kong and Konstantinos Mamouras

• Towards a Formal Foundation of Intermittent Computing. Milijana Surbatovich, Brandon Lucia, and Limin Jia

• Unifying Execution of Imperative Generators and Declarative Specifications. Pengyu Nie, Marinela Parovic, Zhiqiang Zang, Sarfraz Khurshid, Aleksandar Milicevic, and Milos Gligoric

Concurrent model synchronization is the task of restoring consistency between two correlated models after they have been changed concurrently and independently.
To determine whether such concurrent model changes conflict with each other and to resolve these conflicts taking domain- or user-specific preferences into account is highly challenging.
In this paper, we present a framework for concurrent model synchronization algorithms based on Triple Graph Grammars (TGGs).
TGGs specify the consistency of correlated models using grammar rules; these rules can be used to derive different consistency restoration operations.
Using TGGs, we infer a causal dependency relation for model elements that enables us to detect conflicts non-invasively.
Different kinds of conflicts are detected first and resolved by the subsequent conflict resolution process.
Users configure the overall synchronization process by orchestrating the application of consistency restoration fragments according to several conflict resolution strategies to achieve individual synchronization goals.
As proof of concept, we have implemented this framework in the model transformation tool eMoflon.
Our initial evaluation shows that the runtime of our presented approach scales with the size of model changes and conflicts, rather than model size.

Link to Publication: http://design.cs.iastate.edu/splash20/sle20/sle20main-p15-p.pdf

Lars Fritsche

TU Darmstadt, Germany

Jens Kosiol

University of Marburg, Germany

Adrian Möller

TU Darmstadt, Germany

Andy Schürr

TU Darmstadt, Germany

Gabriele Taentzer

University of Marburg, Germany

Germany

Language workbenches—tools to define software languages together with their IDEs—are designed to simplify language engineering and implementation: they free language engineers from many meticulous tasks, but oftentimes have a very steep learning curve even for experienced software professionals. With the assumption that meta-definitions are one of the key factors that hinder language engineering, we introduce an example-driven approach to language definition. We describe in this paper our vision of a web-based tool aimed at beginner language engineers, and list possible requirements for such a tool. A language is defined by giving examples of code written in it using illustrative syntax definition. These examples are then annotated to specify different concerns of language definition—abstract syntax, typing rules, validation rules, formatting rules, and dynamic semantics.

Link to Publication: http://design.cs.iastate.edu/splash20/sle20/sle20main-p80-p.pdf

Mikhail Barash

University of Bergen

Norway

Autonomous robots combine a variety of skills to form increasingly complex behaviors called missions. While the skills are often programmed at a relatively low level of abstraction, their coordination is architecturally separated and often expressed in higher-level languages or frameworks. Recently, the language of Behavior Trees gained attention among roboticists for this reason. Originally designed for computer games to model autonomous actors, Behavior Trees offer an extensible tree-based representation of missions. However, even though, several implementations of the language are in use, little is known about its usage and scope in the real world. How do behavior trees relate to traditional languages for describing behavior? How are behavior tree concepts used in applications? What are the benefits of using them?

We present a study of the key language concepts in Behavior Trees and their use in real-world robotic applications. We identify behavior tree languages and compare their semantics to the most well-known behavior modeling languages: state and activity diagrams. We mine open source repositories for robotics applications that use the language and analyze this usage. We find that Behavior Trees are a pragmatic language, not fully specified, allowing projects to extend it even for just one model. Behavior trees clearly resemble the models-at-runtime paradigm. We contribute a dataset of real-world behavior models, hoping to inspire the community to use and further develop this language, associated tools, and analysis techniques.

Link to Publication: http://design.cs.iastate.edu/splash20/sle20/sle20main-p74-p.pdf

Razan Ghzouli

Chalmers University of Technology & University of Gothenburg

Sweden

Thorsten Berger

Chalmers University of Technology, Sweden / University of Gothenburg, Sweden

Sweden

Einar Broch Johnsen

University of Oslo

Swaib Dragule

Chalmers | University of Gothenburg

Andrzej Wąsowski

IT University of Copenhagen, Denmark

Denmark

In collaboration scenarios, we often encounter situations in
which semantically interrelated models are changed concurrently.
Concurrent model synchronization denotes the task
of keeping these models consistent by propagating changes
between them. This is challenging as changes can contradict
each other and thus be in conflict. A problem with current
synchronisation approaches is that they are often nondeterministic,
i.e., the order in which changes are propagated
is essential for the result. Furthermore, a common limitation
is that the involved models must have been in a consistent
state at some point, and that the applied changes are at least
valid for the domain in which they were made. We propose
a hybrid approach based on Triple Graph Grammars (TGGs)
and Integer Linear Programming (ILP) to overcome these issues:
TGGs are a grammar-based means that supplies us with
a superset of possible synchronization solutions, forming a
search space from which an optimum solution incorporating
user-defined preferences can be chosen by ILP. Therefore, the
proposed method combines configurability by comprising
expert knowledge via TGGs with the flexible input handling
of search-based techniques: By accepting arbitrary graph
structures as input models, the approach is tolerant towards
errors induced during the modelling process, i.e., it can cope
with input models which do not conform to their metamodel
or which cannot be generated by the TGG at hand. The
approach is implemented in the model transformation tool
eMoflon and evaluated regarding scalability for growing
model sizes and an increasing number of changes.

Link to Publication: http://design.cs.iastate.edu/splash20/sle20/sle20main-p20-p.pdf

Nils Weidmann

Lars Fritsche

TU Darmstadt, Germany

Anthony Anjorin

Paderborn University, Germany

Please go to the breakrooms at Clowdr.

Test case generation from context-free grammars typically uses the grammar's production rules to directly construct words that cover specific sets of derivations. Here, we investigate test case generation by traversing graphs derived from the LR-automata corresponding to the grammars. We develop a new algorithm that generates positive test cases by covering all edges between pairs of directly connected states in a two-phase breadth-first path search. The algorithm iterates over all edges stemming from shift/reduce and reduce/reduce conflicts, using a technique similar to the stack duplication used in GLR parsing. We then extend our algorithm to generate negative (i.e., syntactically invalid) test cases, by applying different edge mutation operations during the extraction of test cases from paths.

Link to Publication: http://design.cs.iastate.edu/splash20/sle20/sle20main-p55-p.pdf

Christoff Rossouw

Stellenbosch University, South Africa

Bernd Fischer

Stellenbosch University, South Africa

South Africa

We report on our experience in using various grammar-based test suite
generation methods to test 61 single-pass compilers that undergraduate
students submitted for the practical project of a computer
architecture course.

We show that
(1) all test suites constructed systematically following different
grammar coverage criteria fall far behind the instructor's test suite
in achieved code coverage, in the number of triggered semantic errors,
and in detected failures and crashes;
(2) a medium-sized positive random test suite triggers more crashes
than the instructor's test suite, but achieves lower code coverage and
triggers fewer non-crashing errors;
and
(3) a combination of the systematic and random test suites performs
as well or better than the instructor's test suite in all aspects and
identifies errors or crashes in every single submission.

We then develop a light-weight extension of the basic grammar-based testing
framework to capture contextual constraints, by encoding scoping and
typing information as ``semantic mark-up tokens'' in the grammar rules.
These mark-up tokens are interpreted by a small generic core engine
when the tests are rendered, and tests with a
syntactic structure that cannot be completed into a valid program by
choosing appropriate identifiers are discarded.
%
We formalize individual error models by overwriting individual mark-up tokens,
and generate tests that are guaranteed to break specific contextual
properties of the language. We show that a fully automatically
generated random test suite with 15 error models achieves roughly the
same coverage as the instructor's test suite, and outperforms it in the
number of triggered semantic errors and detected failures and crashes.
Moreover, all failing tests indicate real errors, and we have
detected errors even in the instructor's reference implementation.

Link to Publication: http://design.cs.iastate.edu/splash20/sle20/sle20main-p85-p.pdf

Phillip van Heerden

Stellenbosch University

Moeketsi Raselimo

Stellenbosch University, South Africa

Konstantinos (Kostis) Sagonas

Uppsala University, Sweden

Sweden

Bernd Fischer

Stellenbosch University, South Africa

South Africa

We describe gtutr, an interactive feedback system designed to assist students in developing context-free grammars and corresponding ANTLR parsers.
It intelligently controls students' access to a large test suite for the target language. After each submission, gtutr analyzes any failing tests and uses the Needleman-Wunsch sequence alignment algorithm over the tests' rule traces to identify and eliminate similar failing tests. This reduces the redundancy in the feedback

given to the students and prevents them from being overloaded. gtutr uses simple gamification to encourage independent problem solving by students: it gives as little information as possible, and students need to prompt the system for further details such as failing tests similar to or different from already seen tests, or even for hints about rules that are the most likely to contain faults. It tracks the students' information requests and uses this to attenuate marks following an instructor-set penalty schema. The system also visualizes test outcomes over multiple submissions, helping students to keep track of the effects of their changes as their grammar development progresses.

Link to Publication: http://design.cs.iastate.edu/splash20/sle20/sle20main-p39-p.pdf

Chelsea Barraball

Stellenbosch University, South Africa

Moeketsi Raselimo

Stellenbosch University, South Africa

Bernd Fischer

Stellenbosch University, South Africa

South Africa

Swift is a modern general-purpose programming language, designed to be a replacement for C-based languages. Although primarily directed at development of applications for Apple's operating systems, Swift's adoption has been growing steadily in other domains, ranging from server-side services to machine learning. This success can be partly attributed to a rich type system that enables the design of safe, fast, and expressive programming interfaces. Unfortunately, this richness comes at the cost of complexity, setting a high entry barrier to exploit Swift's full potential. Furthermore, existing documentation typically only relies on examples, leaving new users with little help to build a deeper understanding of the underlying rules and mechanisms.

This paper aims to tackle this issue by laying out the foundations for a formal framework to reason about Swift's type system. We introduce Featherweight Swift, a minimal language stripped of all features not essential to describe its typing rules. Featherweight Swift features classes and protocol inheritance, supports retroactive modeling, and emulates Swift's overriding mechanisms. Yet its formalization fits on a few pages. We present Featherweight Swift's syntax and semantics. We then elaborate on the usability of our framework to reason about Swift's features, future extensions, and implementation by discussing a bug in Swift's compiler, discovered throughout the design of our calculus.

Link to Publication: http://design.cs.iastate.edu/splash20/sle20/sle20main-p56-p.pdf

Dimitri Racordon

University of Geneva, Switzerland

Switzerland

Didier Buchs

University of Geneva, Switzerland

Please go to the breakrooms at Clowdr.

Parsing Expression Grammars (PEGs) are a recognition-based formalism which allows to describe the syntactical and the lexical elements of a language. The main difference between Context-Free Grammars (CFGs) and PEGs relies on the interpretation of the choice operator: while the CFGs' unordered choice $e \mid e'$ is interpreted as the union of the languages recognized by $e$ and $e'$, the PEGs' prioritized choice $e / e'$ discards $e'$ if $e$ succeeds. Such subtle, but important difference, changes the language
recognized and yields more efficient parsing algorithms. This paper proposes a rewriting logic semantics for PEGs. We start
with a rewrite theory giving meaning to the usual constructs in PEGs. Later, we show that cuts, a mechanism for controlling backtracks in PEGs, finds also a natural representation in our framework.
We generalize such mechanism, allowing for both local and global cuts with a precise, unified and formal semantics. Hence, our work strives at better understanding and controlling backtracks in parsers for PEGs. The semantics we propose is executable and, besides being a parser with modest efficiency, it can be used as a playground to test different optimization ideas. More importantly, it is a mathematical tool that can be used for different analyses.

Link to Publication: http://design.cs.iastate.edu/splash20/sle20/sle20main-p78-p.pdf

Sergio Queiroz de Medeiros

Universidade Federal do Rio Grande do Norte

Brazil

Carlos Olarte

Federal University of Rio Grande do Norte, Brazil

Proof assistants like Coq, Lean, or HOL4 rely heavily on stateful meta-programs called scripts to assemble proofs. Unlike pen-and-paper proofs, proof scripts only describe the steps to take (induct on x, apply a theorem, …), not the states that these steps lead to; as a result, plain proof scripts are essentially incomprehensible without the assistance of an interactive user interface able to run the script and show the corresponding proof states.

Until now, the standard process to communicate a proof without forcing readers to execute its script was to manually copy-paste intermediate proof states into the script, as source code comments — a tedious and error-prone exercise. Additional prose (such as for a book or tutorial) was likewise embedded in comments, preserving executability at the cost of a mediocre text-editing experience.

This paper describes a new approach to the development and dissemination of literate proof scripts, with a focus on the Coq proof assistant. Specifically, we describe two contributions: a compiler that interleaves Coq's output with the original proof script to produce interactive webpages that are complete, self-contained presentations of Coq proofs; and a new literate programming toolkit that allows authors to switch seamlessly between prose- and code-oriented views of the same sources, by translating back and forth between reStructuredText documents and literate Coq source files. In combination, these tools offer a new way to write, communicate, and preserve proofs, combining the flexibility of procedural proof scripts and the intelligibility of declarative proofs.

Clément Pit-Claudel

MIT CSAIL

United States

I’m a PhD candidate at MIT, working in Adam Chlipala’s lab. My research focuses on proof assistants, extensible compilers, and programming languages; my broader interests include hardware design languages, optimization, databases, and type theory. I work on end-to-end verified compilation pipelines from high-level specifications to assembly language, verified compilers and fast simulation for rule-based hardware design languages with EHRs, and Coq tooling.
And I’m applying for faculty positions this year!

Please go to the breakrooms at Clowdr.

Please go to the breakrooms at Clowdr.

Please go to the breakrooms at Clowdr.

The reliability of software that has a Deep Neural Network (DNN) as a component is urgently important today given the increasing number of critical applications being deployed with DNNs. The need for reliability raises a need for rigorous testing of the safety and trustworthiness of these systems. In the last few years, there have been a number of research efforts focused on testing DNNs. However, the test generation techniques proposed so far lack a check to determine whether the test inputs they are generating are valid, and thus invalid inputs are produced. To illustrate this situation, we explored three recent DNN testing techniques. Using deep generative model based input validation, we show that all the three techniques generate significant number of invalid test inputs. We further analyzed the test coverage achieved by the test inputs generated by the DNN testing techniques and showed how invalid test inputs can falsely inflate test coverage metrics. To overcome the inclusion of invalid inputs in testing, we propose a technique to incorporate the valid input space of the DNN model under test in the test generation process. Our technique uses a deep generative model-based algorithm to generate only valid inputs. Results of our empirical studies show that our technique is effective in eliminating invalid tests and boosting the number of valid test inputs generated.

Link to Publication: http://design.cs.iastate.edu/splash20/splashcomp20/splashcomp20key-key2-p.pdf

Mary Lou Soffa

University of Virginia

Mary Lou Ehnot Soffa is the Owen R. Cheatham Professor of Sciences at the Computer Science Department at the University of Virginia. From 2004 to 2012, she served as the Department Chair at UVA.  From 1977 to 2004, she was a Professor of Computer Science at the University of Pittsburgh and also served as the Dean of Graduate Studies in the College of Arts and Sciences from 1991 to 1996. Her research interests include optimizing compilers, virtual execution environments, software testing, program analysis, software security,  and software systems for multi-core architectures.  She has published over 175 articles and  has directed 32 Ph.D. students to completion, half of whom are women.  Mary Lou is both  an IEEE Fellow and  an ACM Fellow. She  received the Anita Borg Technical Leadership Award, the Ken Kennedy Award and the Computing Research Association (CRA) Nico Habermann Award.

Please go to the breakrooms at Clowdr.

Please go to the breakrooms at Clowdr.

Please go to the breakrooms at Clowdr.

Please go to the breakrooms at Clowdr.

Please go to the breakrooms at Clowdr.