bluuebunny/crossref_metadata_2025 huggingface dataset:
Model-driven engineering and run-time model-usage in service robotics
Authors: Steck Andreas , Lotz Alex , Schlegel Christian
Published: April 2020

The development of service robots has gained more and more attention over the last years. A major challenge on the way towards industrial-strength service robotic systems is to make the step from code-driven to model-driven engineering. In this work we propose to put models into the focus of the whole life-cycle of robotic systems covering design-time as well as run-time. We describe how to explicate parameters, properties and resource information in the models at design-time and how to take these information into account by the run-time system of the robot to support its decision making process. We underpin our work by an exhaustive real-world example which is completely developed with our tools.
Reflection in direct style
Authors: Asai Kenichi
Published: April 2020

A reflective language enables us to access, inspect, and/or modify the language semantics from within the same language framework. Although the degree of semantics exposure differs from one language to another, the most powerful approach, referred to as the behavioral reflection, exposes the entire language semantics (or the language interpreter) that defines behavior of user programs for user inspection/modification. In this paper, we deal with the behavioral reflection in the context of a functional language Scheme. In particular, we show how to construct a reflective interpreter where user programs are interpreted by the tower of metacircular interpreters and have the ability to change any parts of the interpreters during execution. Its distinctive feature compared to the previous work is that the metalevel interpreters observed by users are written in direct style. Based on the past attempt of the present author, the current work solves the level-shifting anomaly by defunctionalizing and inspecting the top of the continuation frames. The resulting system enables us to freely go up and down the levels and access/modify the direct-style metalevel interpreter. This is in contrast to the previous system where metalevel interpreters were written in continuation-passing style (CPS) and only CPS functions could be exposed to users for modification.
Firepile
Authors: Nystrom Nathaniel , White Derek , Das Kishen
Published: April 2020

Recent advances have enabled GPUs to be used as general-purpose parallel processors on commodity hardware for little cost. However, the ability to program these devices has not kept up with their performance. The programming model for GPUs has a number of restrictions that make it difficult to program. For example, software running on the GPU cannot perform dynamic memory allocation, requiring the programmer to pre-allocate all memory the GPU might use. To achieve good performance, GPU programmers must also be aware of how data is moved between host and GPU memory and between the different levels of the GPU memory hierarchy.

We describe Firepile, a library for GPU programming in Scala. The library enables a subset of Scala to be executed on the GPU. Code trees can be created from run-time function values, which can then be analyzed and transformed to generate GPU code. A key property of this mechanism is that it is modular: unlike with other meta-programming constructs, the use of code trees need not be exposed in the library interface. Code trees are general and can be used by library writers in other application domains. Our experiments show Firepile users can achieve performance comparable to C code targeted to the GPU with shorter, simpler, and easier-to-understand code.
Declaratively defining domain-specific language debuggers
Authors: Lindeman Ricky T. , Kats Lennart C.L. , Visser Eelco
Published: April 2020

Tool support is vital to the effectiveness of domain-specific languages. With language workbenches, domain-specific languages and their tool support can be generated from a combined, high-level specification. This paper shows how such a specification can be extended to describe a debugger for a language. To realize this, we introduce a meta-language for coordinating the debugger that abstracts over the complexity of writing a debugger by hand. We describe the implementation of a language-parametric infrastructure for debuggers that can be instantiated based on this specification. The approach is implemented in the Spoofax language workbench and validated through realistic case studies with the Stratego transformation language and the WebDSL web programming language.
Growing a language environment with editor libraries
Authors: Erdweg Sebastian , Kats Lennart C.L. , Rendel Tillmann , Kästner Christian , Ostermann Klaus , Visser Eelco
Published: April 2020

Large software projects consist of code written in a multitude of different (possibly domain-specific) languages, which are often deeply interspersed even in single files. While many proposals exist on how to integrate languages semantically and syntactically, the question of how to support this scenario in integrated development environments (IDEs) remains open: How can standard IDE services, such as syntax highlighting, outlining, or reference resolving, be provided in an extensible and compositional way, such that an open mix of languages is supported in a single file?

Based on our library-based syntactic extension language for Java, SugarJ, we propose to make IDEs extensible by organizing editor services in
editor libraries
. Editor libraries are libraries written in the object language, SugarJ, and hence activated and composed through regular import statements on a file-by-file basis. We have implemented an IDE for editor libraries on top of SugarJ and the Eclipse-based Spoofax language workbench. We have validated editor libraries by evolving this IDE into a fully-fledged and schema-aware XML editor as well as an extensible Latex editor, which we used for writing this paper.
A modular memory optimization for synchronous data-flow languages
Authors: Gérard Léonard , Guatto Adrien , Pasteur Cédric , Pouzet Marc
Published: April 2020

The generation of efficient sequential code for synchronous data-flow languages raises two intertwined issues: control and memory optimization. While the former has been extensively studied, for instance in the compilation of Lustre and Signal, the latter has only been addressed in a restricted manner. Yet, memory optimization becomes a pressing issue when arrays are added to such languages.

This article presents a two-level solution to the memory optimization problem. It combines a compile-time optimization algorithm, reminiscent of register allocation, paired with language annotations on the source given by the designer. Annotations express in-place modifications and control where allocation is performed. Moreover, they allow external functions performing
in-place
modifications to be safely imported. Soundness of annotations is guaranteed by a semilinear type system and additional scheduling constraints. A key feature is that annotations for well-typed programs do not change the semantics of the language: removing them may lead to less efficient code but will not alter the semantics.

The method has been implemented in a new compiler for a LUSTRE-like synchronous language extended with hierarchical automata and arrays. Experiments show that the proposed approach removes most of the unnecessary array copies, resulting in faster code that uses less memory.
An operational semantics for Simulink's simulation engine
Authors: Bouissou Olivier , Chapoutot Alexandre
Published: April 2020

The industrial tool Matlab/Simulink is widely used in the design of embedded systems. The main feature of this tool is its ability to model in a common formalism the software and its physical environment. This makes it very useful for validating the design of embedded software using numerical simulation. However, the formal verification of such models is still problematic as Simulink is a programming language for which no formal semantics exists. In this article, we present an operational semantics of a representative subset of Simulink which includes both continuous-time and discrete-time blocks. We believe that this work gives a better understanding of Simulink and it defines the foundations of a general framework to apply formal methods on Simulink's high level descriptions of embedded systems.
Leading-edge ada verification technologies
Authors: Kanig Johannes
Published: April 2020

We give a hands-on introduction to the tools GNATtest and GNATprove, both developed at AdaCore in the Hi-Lite research project. They allow to do verification of Ada 2012 contracts through testing and formal verification, and also allow a combination of the results of both tools.

The tutorial will contain a very short introduction to Ada 2012, and attendees will write a small example on which they can play with GNATtest to develop test cases, and GNATprove to do some formal verification.
Tutorial overview
Authors: Nilsen Kelvin
Published: April 2020

In spite of the high-level abstraction benefits of automatic tracing garbage collection, current prevailing sentiment within the safety certification community is that a simpler memory model is required for the most rigorous levels of software safety certification. Thus, the draft JSR-302 specification for safety critical Java relies on scope-based memory allocation rather than tracing garbage collection. The scoped memory model for JSR-302 is a simplification of the RTSJ model. JSR-302 enforces a strict hierarchy of scopes and distinguishes private scopes, which can be seen only by one thread, from mission scopes, which can be accessed by all the threads that comprise a mission, including threads running within inner-nested sub-missions. The hierarchical memory structure allows implementations to guarantee the absence of memory fragmentation for scope management, unlike the Real-Time Specification for Java from which the JSR-302 specification was derived.

In the absence of block structure, it is more difficult in Java to safely manage references to stack-allocated objects than in Ada. While the simplified hierarchical management of scoped memory that is part of JSR-302 addresses memory fragmentation concerns, it does not guarantee the absence of dangling pointers. As with the Real-Time Specification for Java, JSR-302 requires a run-time check to enforce that no reference assignment creates a relationship whereby an outer-nested object is allowed to point to an inner-nested object. This rule assures the absence of dangling pointers, but it introduces a different problem: every assignment to a reference field must be accompanied by a run-time check to validate the appropriate scope nesting relationship. This run-time check will throw a run-time exception if the assignment is deemed inappropriate.

The safety certification evidence for a given safety-critical Java program must therefore include an argument for every reference assignment that it will not cause the program to abort with a run-time exception. Furthermore, the certification evidence must prove that sufficient memory is available to reliably execute each safety-critical task in the system.

This tutorial provides an overview of dynamic memory management in Safety Critical Java and describes two annotation systems that have been designed to support static (compile-time) enforcement of memory safety properties. The first annotation system is described in an appendix to the draft JSR-302 standard. This relatively simple annotation system, which is not considered normative, serves to demonstrate that memory safety can be statically proven without requiring extensive annotations throughout existing library code. The second annotation system is the system implemented in Perc Pico. This annotation system, which is much richer than the draft JSR-302 annotation, has been in experimental use for over five years. During that time, tens of thousands of lines of experimental application code have been developed, with the experience motivating a variety of refinements to the original design.
Synchronization cannot be implemented as a library
Authors: Bosch Geert
Published: April 2020

Writing efficient programs for increasingly parallel computer architectures requires the use of hardware primitives, such as atomic read-modify-write instructions or transactional memory. While new libraries and language constructs are introduced to expose the new capabilities, we argue that they are implementation details best left hidden. High-level synchronization constructs, such as those provided by Java and Ada, are both sufficient and necessary for modern programming languages to take full advantage of today's and tomorrow's hardware. While defined in terms of mutual exclusion, we show that these constructs are general enough to allow an enhanced compiler to automatically generate the appropriate lock-free synchronization code for the target system. Language support for synchronization is necessary for efficient, reliable and portable programs.
Programming language life cycles
Authors: Steele Guy L.
Published: April 2020

New programming languages keep getting invented, and old languages (most of them) eventually die. Many languages are eventually reduced to, if anything, a single surviving slogan or idea. (Examples: COBOL = programs look like English; SNOBOL = pattern matching on strings.) How do ideas about what programmers want or need to do drive decisions made by language designers? We'll look at some of these ideas, and also at the origin, evolution, and possible destinations of certain ideas pursued during the development of the Fortress programming language, speculating on the forces that drive these life cycles.
Adapting ACATS for use with run-time checks suppressed
Authors: Eilers Dan R. , Koskinen Tero
Published: April 2020

A well-known issue with compiler conformance testing is that the tested environment may differ from the end user's environment, in ways that defy analysis. Possible differences include the host or target computer instruction set, the host or target computer operating system version, version differences in various components of the compilation system, and differences in compilation switch settings. Most of these differences can be eliminated by retesting in the end-user's actual environment. However, if the end user's environment includes compilation switches that suppress some or all of Ada's run-time checks, which we believe to be quite common, it is not currently feasible to re-run ACATS testing in that mode. That is because many ACATS tests rely on run-time checking, and those tests are not segregated or otherwise identified. We propose to remedy this difficulty by identifying such tests, so that the remaining tests can all be run and expected to pass with compilation flags that suppress some or all checks.
An inheritance system for structural & behavioral reuse in component-based software programming
Authors: Spacek Petr , Dony Christophe , Tibermacine Chouki , Fabresse Luc
Published: April 2020

In the context of Component-based Programming, which addresses the implementation stage of a component-based software engineering development process, this paper describes a specification and an operational integration of an inheritance system into a self-contained new component-based programming language named Compo. Our proposal completes and extends related works by making it possible to apply inheritance to the full description of components, i.e. both to structural (description of provisions and requirements, of component architecture) and behavioral (full implementations of services) parts in component descriptions. Inheritance in Compo is designed to be used in conjunction with composition to maximize reuse capabilities and expressive power. Compo implementation proposes a clear operational solution for inheritance and for achieving and testing substitutions.
Elastic images
Authors: Argelaguet Ferran , Jáuregui David Antonio Gómez , Marchal Maud , Lécuyer Anatole
Published: April 2020

We introduce the Elastic Images, a novel pseudo-haptic feedback technique which enables the perception of the local elasticity of images without the need of any haptic device. The proposed approach focus on whether visual feedback is able to induce a sensation of stiffness when the user interacts with an image using a standard mouse. The user, when clicking on a Elastic Image, is able to deform it locally according to its elastic properties. To reinforce the effect, we also propose the generation of procedural shadows and creases to simulate the compressibility of the image and several mouse cursors replacements to enhance pressure and stiffness perception. A psychophysical experiment was conducted to quantify this novel pseudo-haptic perception and determine its perceptual threshold (or its Just Noticeable Difference). The results showed that users were able to recognize up to eight different stiffness values with our proposed method and confirmed that it provides a perceivable and exploitable sensation of elasticity. The potential applications of the proposed approach range from pressure sensing in product catalogs and games, or its usage in graphical user interfaces for increasing the expressiveness of widgets.
Surface perception of planar abstractions
Authors: Mccrae James , Mitra Niloy J. , Singh Karan
Published: April 2020

Various algorithms have been proposed to create planar abstractions of 3D models, but there has been no systematic effort to evaluate the effectiveness of such abstractions in terms of perception of the abstracted surfaces. In this work, we perform a large crowd-sourced study involving approximately 70k samples to evaluate how well users can orient gauges on planar abstractions of commonly occurring models. We test four styles of planar abstractions against ground truth surface representations, and analyze the data to discover a wide variety of correlations between task error and measurements relating to surface-specific properties such as curvature, local thickness and medial axis distance, and abstraction-specific properties. We use these discovered correlations to create linear models to predict error in surface understanding at a given point, for both surface representations and planar abstractions. Our predictive models reveal the geometric causes most responsible for error, and we demonstrate their potential use to build upon existing planar abstraction techniques in order to improve perception of the abstracted surface.
Leveraging speculative architectures for runtime program validation
Authors: Santos Juan Carlos Martinez , Fei Yunsi
Published: April 2020

Program execution can be tampered with by malicious attackers through exploiting software vulnerabilities. Changing the program behavior by compromising control data and decision data has become the most serious threat in computer system security. Although several hardware approaches have been presented to validate program execution, they either incur great hardware overhead or introduce false alarms. We propose a new hardware-based approach by leveraging the existing speculative architectures for runtime program validation. The on-chip branch target buffer (BTB) is utilized as a cache of the legitimate control flow transfers stored in a secure memory region. In addition, the BTB is extended to store the correct program path information. At each indirect branch site, the BTB is used to validate the decision history of previous conditional branches and monitor the following execution path at runtime. Implementation of this approach is transparent to the upper operating system and programs. Thus, it is applicable to legacy code. Because of good code locality of the executable programs and effectiveness of branch prediction, the frequency of control-flow validations against the secure off-chip memory is low. Our experimental results show a negligible performance penalty and small storage overhead.
Thermal-aware memory mapping in 3D designs
Authors: Hsieh Ang-Chih , Hwang Tingting
Published: April 2020

DRAM is usually used as main memory for program execution. The thermal behavior of a memory block in a 3D SIP is affected not only by the power behavior but also the heat dissipating ability of that block. The power behavior of a block is related to the applications run on the system, while the heat dissipating ability is determined by the number of tier and the position the block locates. Therefore, a thermal-aware memory allocator should consider the following two points. First, the allocator should consider not only the power behavior of a logic block but also the physical location during memory mapping and second, the changing temperature of a physical block during execution of programs. In this article, we will propose a memory mapping algorithm taking into consideration these two points. Our technique can be classified as static thermal management to be applied to embedded software designs. Experiments show that for single-core systems, our method can reduce the temperature of memory system by 17.1°C, as compared to a straightforward mapping in the best case, and 13.3°C on average. For systems with four cores, the temperature reductions are 9.9°C and 11.6°C on average when L1 cache of each core is set to 4KB and 8KB, respectively.
Transport-layer-assisted routing for runtime thermal management of 3D NoC systems
Authors: Chao Chih-Hao , Chen Kun-Chih , Yin Tsu-Chu , Lin Shu-Yen , Wu An-Yeu (Andy)
Published: April 2020

To ensure thermal safety and to avoid performance degradation from temperature regulation in 3D NoC, we propose a new temperature-traffic control framework. The framework contains the vertical throttling-based runtime thermal management (VT-RTM) scheme and the transport-layer assisted routing (TLAR) scheme. VT-RTM scheme increases the cooling speed and maintains high availability. TLAR scheme sustains the throughput of the nonstationary irregular mesh network. In our experiments, VT-RTM scheme reduces cooling time by 84% and achieves 98% network availability; the overall performance impact is around 8% of traditional schemes. TLAR scheme reduces average latency by 35∼% and improves sustainable throughput by 76%
Understanding idiomatic traversals backwards and forwards
Authors: Bird Richard , Gibbons Jeremy , Mehner Stefan , Voigtländer Janis , Schrijvers Tom
Published: April 2020

We present new ways of reasoning about a particular class of effectful Haskell programs, namely those expressed as idiomatic traversals. Starting out with a specific problem about labelling and unlabelling binary trees, we extract a general inversion law, applicable to any monad, relating a traversal over the elements of an arbitrary traversable type to a traversal that goes in the opposite direction. This law can be invoked to show that, in a suitable sense, unlabelling is the inverse of labelling. The inversion law, as well as a number of other properties of idiomatic traversals, is a corollary of a more general theorem characterising traversable functors as finitary containers: an arbitrary traversable object can be decomposed uniquely into shape and contents, and traversal be understood in terms of those. Proof of the theorem involves the properties of traversal in a special idiom related to the free applicative functor.
Hasochism
Authors: Lindley Sam , McBride Conor
Published: April 2020

Haskell's type system has outgrown its Hindley-Milner roots to the extent that it now stretches to the basics of dependently typed programming. In this paper, we collate and classify techniques for programming with dependent types in Haskell, and contribute some new ones. In particular, through extended examples---merge-sort and rectangular tilings---we show how to exploit Haskell's constraint solver as a theorem prover, delivering code which, as Agda programmers, we envy. We explore the compromises involved in simulating variations on the theme of the dependent function space in an attempt to help programmers put dependent types to work, and to inform the evolving language design both of Haskell and of dependently typed languages more broadly.
An EDSL approach to high performance Haskell programming
Authors: Ankner Johan , Svenningsson Josef David
Published: April 2020

This paper argues for a new methodology for writing high performance Haskell programs by using Embedded Domain Specific Languages.

We exemplify the methodology by describing a complete library, meta-repa, which is a reimplementation of parts of the repa library. The paper describes the implementation of meta-repa and contrasts it with the standard approach to writing high performance libraries. We conclude that even though the embedded language approach has an initial cost of defining the language and some syntactic overhead it gives a more tailored programming model, stronger performance guarantees, better control over optimizations, simpler implementation of fusion and inlining and allows for moving type level programming down to value level programming in some cases. We also provide benchmarks showing that meta-repa is as fast, or faster, than repa.

Furthermore, meta-repa also includes push arrays and we demonstrate their usefulness for writing certain high performance kernels such as FFT.
CakeML
Authors: Kumar Ramana , Myreen Magnus O. , Norrish Michael , Owens Scott
Published: April 2020

We have developed and mechanically verified an ML system called CakeML, which supports a substantial subset of Standard ML. CakeML is implemented as an interactive read-eval-print loop (REPL) in x86-64 machine code. Our correctness theorem ensures that this REPL implementation prints only those results permitted by the semantics of CakeML. Our verification effort touches on a breadth of topics including lexing, parsing, type checking, incremental and dynamic compilation, garbage collection, arbitrary-precision arithmetic, and compiler bootstrapping.

Our contributions are twofold. The first is simply in building a system that is end-to-end verified, demonstrating that each piece of such a verification effort can in practice be composed with the others, and ensuring that none of the pieces rely on any over-simplifying assumptions. The second is developing novel approaches to some of the more challenging aspects of the verification. In particular, our formally verified compiler can bootstrap itself: we apply the verified compiler to itself to produce a verified machine-code implementation of the compiler. Additionally, our compiler proof handles diverging input programs with a lightweight approach based on logical timeout exceptions. The entire development was carried out in the HOL4 theorem prover.
Parametric effect monads and semantics of effect systems
Authors: Katsumata Shin-ya
Published: April 2020

We study fundamental properties of a generalisation of monad called
parametric effect monad
, and apply it to the interpretation of general effect systems whose effects have sequential composition operators. We show that parametric effect monads admit analogues of the structures and concepts that exist for monads, such as Kleisli triples, the state monad and the continuation monad, Plotkin and Power's algebraic operations, and the categorical ┬┬-lifting. We also show a systematic method to generate both effects and a parametric effect monad from a monad morphism. Finally, we introduce two effect systems with explicit and implicit subeffecting, and discuss their denotational semantics and the soundness of effect systems.
Minimization of symbolic automata
Authors: D'Antoni Loris , Veanes Margus
Published: April 2020

Symbolic Automata extend classical automata by using symbolic alphabets instead of finite ones. Most of the classical automata algorithms rely on the alphabet being finite, and generalizing them to the symbolic setting is not a trivial task. In this paper we study the problem of minimizing symbolic automata. We formally define and prove the basic properties of minimality in the symbolic setting, and lift classical minimization algorithms (Huffman-Moore's and Hopcroft's algorithms) to symbolic automata. While Hopcroft's algorithm is the fastest known algorithm for DFA minimization, we show how, in the presence of symbolic alphabets, it can incur an exponential blowup. To address this issue, we introduce a new algorithm that fully benefits from the symbolic representation of the alphabet and does not suffer from the exponential blowup. We provide comprehensive performance evaluation of all the algorithms over large benchmarks and against existing state-of-the-art implementations. The experiments show how the new symbolic algorithm is faster than previous implementations.
Authenticated data structures, generically
Authors: Miller Andrew , Hicks Michael , Katz Jonathan , Shi Elaine
Published: April 2020

An authenticated data structure (ADS) is a data structure whose operations can be carried out by an untrusted
prover
, the results of which a
verifier
can efficiently check as authentic. This is done by having the prover produce a compact proof that the verifier can check along with each operation's result. ADSs thus support outsourcing data maintenance and processing tasks to untrusted servers without loss of integrity. Past work on ADSs has focused on particular data structures (or limited classes of data structures), one at a time, often with support only for particular operations.

This paper presents a generic method, using a simple extension to a ML-like functional programming language we call λ• (lambda-auth), with which one can program authenticated operations over any data structure defined by standard type constructors, including recursive types, sums, and products. The programmer writes the data structure largely as usual and it is compiled to code to be run by the prover and verifier. Using a formalization of λ• we prove that all well-typed λ• programs result in code that is secure under the standard cryptographic assumption of collision-resistant hash functions. We have implemented λ• as an extension to the OCaml compiler, and have used it to produce authenticated versions of many interesting data structures including binary search trees, red-black+ trees, skip lists, and more. Performance experiments show that our approach is efficient, giving up little compared to the hand-optimized data structures developed previously.
Modular, higher-order cardinality analysis in theory and practice
Authors: Sergey Ilya , Vytiniotis Dimitrios , Peyton Jones Simon
Published: April 2020

Since the mid '80s, compiler writers for functional languages (especially lazy ones) have been writing papers about identifying and exploiting thunks and lambdas that are used only once. However it has proved difficult to achieve both power and simplicity in practice. We describe a new, modular analysis for a higher-order language, which is both simple and effective, and present measurements of its use in a full-scale, state of the art optimising compiler. The analysis finds many single-entry thunks and one-shot lambdas and enables a number of program optimisations.
From parametricity to conservation laws, via Noether's theorem
Authors: Atkey Robert
Published: April 2020

Invariance is of paramount importance in programming languages and in physics. In programming languages, John Reynolds' theory of relational parametricity demonstrates that parametric polymorphic programs are invariant under change of data representation, a property that yields "free" theorems about programs just from their types. In physics, Emmy Noether showed that if the action of a physical system is invariant under change of coordinates, then the physical system has a conserved quantity: a quantity that remains constant for all time. Knowledge of conserved quantities can reveal deep properties of physical systems. For example, the conservation of energy is by Noether's theorem a consequence of a system's invariance under time-shifting.

In this paper, we link Reynolds' relational parametricity with Noether's theorem for deriving conserved quantities. We propose an extension of System F$\omega$ with new kinds, types and term constants for writing programs that describe classical mechanical systems in terms of their Lagrangians. We show, by constructing a relationally parametric model of our extension of F$\omega$, that relational parametricity is enough to satisfy the hypotheses of Noether's theorem, and so to derive conserved quantities for free, directly from the polymorphic types of Lagrangians expressed in our system.
Toward general diagnosis of static errors
Authors: Zhang Danfeng , Myers Andrew C.
Published: April 2020

We introduce a general way to locate programmer mistakes that are detected by static analyses such as type checking. The program analysis is expressed in a constraint language in which mistakes result in unsatisfiable constraints. Given an unsatisfiable system of constraints, both satisfiable and unsatisfiable constraints are analyzed, to identify the program expressions most likely to be the cause of unsatisfiability. The likelihood of different error explanations is evaluated under the assumption that the programmer's code is mostly correct, so the simplest explanations are chosen, following Bayesian principles. For analyses that rely on programmer-stated assumptions, the diagnosis also identifies assumptions likely to have been omitted. The new error diagnosis approach has been implemented for two very different program analyses: type inference in OCaml and information flow checking in Jif. The effectiveness of the approach is evaluated using previously collected programs containing errors. The results show that when compared to existing compilers and other tools, the general technique identifies the location of programmer errors significantly more accurately.
A proof system for separation logic with magic wand
Authors: Lee Wonyeol , Park Sungwoo
Published: April 2020

Separation logic is an extension of Hoare logic which is acknowledged as an enabling technology for large-scale program verification. It features two new logical connectives, separating conjunction and separating implication, but most of the applications of separation logic have exploited only separating conjunction without considering separating implication. Nevertheless the power of separating implication has been well recognized and there is a growing interest in its use for program verification. This paper develops a proof system for full separation logic which supports not only separating conjunction but also separating implication. The proof system is developed in the style of sequent calculus and satisfies the admissibility of cut. The key challenge in the development is to devise a set of inference rules for manipulating heap structures that ensure the completeness of the proof system with respect to separation logic. We show that our proof of completeness directly translates to a proof search strategy.
A trusted mechanised JavaScript specification
Authors: Bodin Martin , Chargueraud Arthur , Filaretti Daniele , Gardner Philippa , Maffeis Sergio , Naudziuniene Daiva , Schmitt Alan , Smith Gareth
Published: April 2020

JavaScript is the most widely used web language for client-side applications. Whilst the development of JavaScript was initially just led by implementation, there is now increasing momentum behind the ECMA standardisation process. The time is ripe for a formal, mechanised specification of JavaScript, to clarify ambiguities in the ECMA standards, to serve as a trusted reference for high-level language compilation and JavaScript implementations, and to provide a platform for high-assurance proofs of language properties.

We present JSCert, a formalisation of the current ECMA standard in the Coq proof assistant, and JSRef, a reference interpreter for JavaScript extracted from Coq to OCaml. We give a Coq proof that JSRef is correct with respect to JSCert and assess JSRef using test262, the ECMA conformance test suite. Our methodology ensures that JSCert is a comparatively accurate formulation of the English standard, which will only improve as time goes on. We have demonstrated that modern techniques of mechanised specification can handle the complexity of JavaScript.
Combining proofs and programs in a dependently typed language
Authors: Casinghino Chris , Sjöberg Vilhelm , Weirich Stephanie
Published: April 2020

Most dependently-typed programming languages either require that all expressions terminate (e.g. Coq, Agda, and Epigram), or allow infinite loops but are inconsistent when viewed as logics (e.g. Haskell, ATS, Ωmega. Here, we combine these two approaches into a single dependently-typed core language. The language is composed of two fragments that share a common syntax and overlapping semantics: a logic that guarantees total correctness, and a call-by-value programming language that guarantees type safety but not termination. The two fragments may interact: logical expressions may be used as programs; the logic may soundly reason about potentially nonterminating programs; programs can require logical proofs as arguments; and "mobile" program values, including proofs computed at runtime, may be used as evidence by the logic. This language allows programmers to work with total and partial functions uniformly, providing a smooth path from functional programming to dependently-typed programming.
Profiling for laziness
Authors: Chang Stephen , Felleisen Matthias
Published: April 2020

While many programmers appreciate the benefits of lazy programming at an abstract level, determining which parts of a concrete program to evaluate lazily poses a significant challenge for most of them. Over the past thirty years, experts have published numerous papers on the problem, but developing this level of expertise requires a significant amount of experience.

We present a profiling-based technique that captures and automates this expertise for the insertion of laziness annotations into strict programs. To make this idea precise, we show how to equip a formal semantics with a metric that measures waste in an evaluation. Then we explain how to implement this metric as a dynamic profiling tool that suggests where to insert laziness into a program. Finally, we present evidence that our profiler's suggestions either match or improve on an expert's use of laziness in a range of real-world applications.
Sound input filter generation for integer overflow errors
Authors: Long Fan , Sidiroglou-Douskos Stelios , Kim Deokhwan , Rinard Martin
Published: April 2020

We present a system, SIFT, for generating input filters that nullify integer overflow errors associated with critical program sites such as memory allocation or block copy sites. SIFT uses a static pro- gram analysis to generate filters that discard inputs that may trigger integer overflow errors in the computations of the sizes of allocated memory blocks or the number of copied bytes in block copy operations. Unlike all previous techniques of which we are aware, SIFT is sound -- if an input passes the filter, it will not trigger an integer overflow error at any analyzed site. Our results show that SIFT successfully analyzes (and therefore generates sound input filters for) 56 out of 58 memory allocation and block memory copy sites in analyzed input processing modules from five applications (VLC, Dillo, Swfdec, Swftools, and GIMP). These nullified errors include six known integer overflow vulnerabilities. Our results also show that applying these filters to 62895 real-world inputs produces no false positives. The analysis and filter generation times are all less than a second.
Gradual typing embedded securely in JavaScript
Authors: Swamy Nikhil , Fournet Cedric , Rastogi Aseem , Bhargavan Karthikeyan , Chen Juan , Strub Pierre-Yves , Bierman Gavin
Published: April 2020

JavaScript's flexible semantics makes writing correct code hard and writing secure code extremely difficult. To address the former problem, various forms of gradual typing have been proposed, such as Closure and TypeScript. However, supporting all common programming idioms is not easy; for example, TypeScript deliberately gives up type soundness for programming convenience. In this paper, we propose a gradual type system and implementation techniques that provide important safety and security guarantees.

We present TS# , a gradual type system and source-to-source compiler for JavaScript. In contrast to prior gradual type systems, TS# features full runtime reflection over three kinds of types: (1) simple types for higher-order functions, recursive datatypes and dictionary-based extensible records; (2) the type any, for dynamically type-safe TS# expressions; and (3) the type un, for untrusted, potentially malicious JavaScript contexts in which TS# is embedded. After type-checking, the compiler instruments the program with various checks to ensure the type safety of TS# despite its interactions with arbitrary JavaScript contexts, which are free to use eval, stack walks, prototype customizations, and other offensive features. The proof of our main theorem employs a form of type-preserving compilation, wherein we prove all the runtime invariants of the translation of TS# to JavaScript by showing that translated programs are well-typed in JS# , a previously proposed dependently typed language for proving functional correctness of JavaScript programs.

We describe a prototype compiler, a secure runtime, and sample applications for TS#. Our examples illustrate how web security patterns that developers currently program in JavaScript (with much difficulty and still with dubious results) can instead be programmed naturally in TS#, retaining a flavor of idiomatic JavaScript, while providing strong safety guarantees by virtue of typing.
All about the with statement in JavaScript
Authors: Park Changhee , Lee Hongki , Ryu Sukyoung
Published: April 2020

The with statement in JavaScript makes static analysis of JavaScript applications difficult by introducing a new scope at run time and thus invalidating lexical scoping. Therefore, many static approaches to JavaScript program analysis and the strict mode of ECMAScript 5 simply disallow the with statement. To justify exclusion of the with statement, we should better understand the actual usage patterns of the with statement.

In this paper, we present the usage patterns of the with statement in real-world JavaScript applications currently used in the 898 most popular web sites. We investigate whether we can rewrite the with statements in each pattern to other statements not using the with statement. We show that we can rewrite all the static occurrences of the with statement that do not have any dynamic code generating functions. Even though the rewriting process is not applicable to any dynamically generated with statements, our results are still promising. Because all the static approaches that disallow the with statement also disallow dynamic code generation, such static approaches can allow the with statement using our rewriting process. We formally present our rewriting strategy, provide its implementation, and show its faithfulness using extensive testing. We believe that removing with statements will simplify JavaScript program analysis designs without considering dynamic scope introduction while imposing fewer syntactic restrictions.
Programming language techniques for differential privacy
Authors: Barthe Gilles , Gaboardi Marco , Hsu Justin , Pierce Benjamin
Published: April 2020

Differential privacy is rigorous framework for stating and enforcing privacy guarantees on computations over sensitive data. Informally, differential privacy ensures that the presence or absence of a single individual in a database has only a negligible statistical effect on the computation's result. Many specific algorithms have been proved differentially private, but manually checking that a given program is differentially private can be subtle, tedious, or both. This approach becomes unfeasible when larger programs are considered.
Semantics column
Authors: Mislove Michael
Published: April 2020

We begin 2017 with a column by Val Tannen on
provenance
. This notion originally arose in art and in archiving - in the former, it deals with the history of artwork, including the chain of custody; it's used to authenticate works of art, and to validate ownership. In archiving, provenance provides a history of how a collection came together, including which elements are closely associated with one another. This gives added information to aid future researchers who wish to use the collection.
Report on CWI lectures in honor of Adriaan van Wijngaarden
Authors: Pérez Jorge A.
Published: April 2020

CWI, the Dutch research institute for mathematics and computer science, organized the "CWI Lectures in honor of Adriaan van Wijngaarden" on November 3, 2016.
Automata column
Authors: Bojańczyk Mikołaj
Published: April 2020

This column is about minimising automata, which is one of the fundamental themes in automata theory. The classical result is that deterministic finite automata on finite words can be minimised. However minimisation (or more importantly, the existence of a unique canonical device) is also true in a very wide variety of other settings, including different types of inputs (words, infinite words, trees, etc.) as well as different types of outputs (yes/no values, numbers, or other words, etc.). In this column, Thomas Colcombet and Daniela Petrşan have a look at minimisation from an abstract (categorical) perspective, and establish what are the conditions needed for a model of automata to admit minimisation.
Verification column
Authors: Rungta Neha
Published: April 2020

The growing popularity of verification competitions such as VerifyThis Verification Competition and the Competition on Software Verification (SV-COMP), both, incentivize as well as reward tool developers. VerifyThis 2016 was held in Eindhoven colocated with the European Joint Conferences on Theory and Practice of Software (ETAPS) 2016. The competition presents challenges to evaluate a broad range of tools such as Danfy, KeY, VeriFast, CIVL, among others. The first article in the newsletter "CIVL Solutions to VerifyThis 2016 Challenges" by Stephen F. Siegel at University of Delaware presents the solutions to the challenges using The Concurrency Intermediate Verification Language (CIVL) verifier. CIVL supports of a variety of techniques based on symbolic execution and model checking to verify sequential and concurrent programs. The article presents an overview of the framework, a description of the challenges, and how CIVL performs on the benchmarks. The second article "Security by Compilation: An Automated Approach to Comprehensive Side-channel resistance" by Chao Wang from University of Southern California and Patrick Schaumont from Virginia Tech leverage formal verification and program synthesis to detect side challenge attacks on mobile devices. The approach is evaluated on implementations of MAC-Keccak, AES and other cryptographic algorithms. This article bridges the security and verification forums of the newsletter.
Summary of the International Conference on Software andSystem Processes (ICSSP 2018)
Authors: Kuhrmann Marco , O'Connor Rory V. , Houston Dan , Hebig Regina , Raffo David
Published: April 2020

The International Conference on Software and System Processes (ICSSP), continuing the success of Software Process Workshop (SPW), the Software Process Modeling and Simulation Workshop (ProSim) and the International Conference on Software Process (ICSP) conference series, has become the established premier event in the eld of software and systems engineering processes. It provides a leading forum for the exchange of research outcomes and industrial best-practices in process development from software and systems disciplines. ICSSP 2018 was held in Gothenburg, Sweden, 26-27 May 2018, co-located with the 40th International Conference on Software Engineering (ICSE). The theme of ICSSP 2018 was studying \Demands on Processes, Processes on Demand" by recognizing the demands on processes that include the need for both well-developed plans and incremental deliveries (agile and hybrid processes), utilization of increased automation (model-based engineering and DevOps), higher degrees of customer collaboration, comprehensive analysis of existing products for reuse (open source and COTS), and performance requirements of enterprise-level architectures. Papers presented at ICSSP discussed these issues across di erent domains, providing concepts, evidence, and experiences.