bluuebunny/crossref_metadata_2025 huggingface dataset:
Mapping a data-flow programming model onto heterogeneous platforms
Authors: Sbîrlea Alina , Zou Yi , Budimlíc Zoran , Cong Jason , Sarkar Vivek
Published: April 2020

In this paper we explore mapping of a high-level macro data-flow programming model called Concurrent Collections (CnC) onto heterogeneous platforms in order to achieve high performance and low energy consumption while preserving the ease of use of data-flow programming. Modern computing platforms are becoming increasingly heterogeneous in order to improve energy efficiency. This trend is clearly seen across a diverse spectrum of platforms, from small-scale embedded SOCs to large-scale super-computers. However, programming these heterogeneous platforms poses a serious challenge for application developers. We have designed a software flow for converting high-level CnC programs to the Habanero-C language. CnC programs have a clear separation between the application description, the implementation of each of the application components and the abstraction of hardware platform, making it an excellent programming model for domain experts. Domain experts can later employ the help of a tuning expert (either a compiler or a person) to tune their applications with minimal effort. We also extend the Habanero-C runtime system to support work-stealing across heterogeneous computing devices and introduce task affinity for these heterogeneous components to allow users to fine tune the runtime scheduling decisions. We demonstrate a working example that maps a pipeline of medical image-processing algorithms onto a prototype heterogeneous platform that includes CPUs, GPUs and FPGAs. For the medical imaging domain, where obtaining fast and accurate results is a critical step in diagnosis and treatment of patients, we show that our model offers up to 17.72X speedup and an estimated usage of 0.52X of the power used by CPUs alone, when using accelerators (GPUs and FPGAs) and CPUs.
Efficient soft error protection for commodity embedded microprocessors using profile information
Authors: Khudia Daya Shanker , Wright Griffin , Mahlke Scott
Published: April 2020

Successive generations of processors use smaller transistors in the quest to make more powerful computing systems. It has been previously studied that smaller transistors make processors more susceptible to soft errors (transient faults caused by high energy particle strikes). Such errors can result in unexpected behavior and incorrect results. With smaller and cheaper transistors becoming pervasive in mainstream computing, it is necessary to protect these devices against soft errors; an increasing rate of faults necessitates the protection of applications running on commodity processors against soft errors. The existing methods of protecting against such faults generally have high area or performance overheads and thus are not directly applicable in the embedded design space. In order to protect against soft errors, the detection of these errors is a necessary first step so that a recovery can be triggered.

To solve the problem of detecting soft errors cheaply, we propose a profiling-based software-only application analysis and transformation solution. The goal is to develop a low cost solution which can be deployed for off-the-shelf embedded processors. The solution works by intelligently duplicating instructions that are likely to affect the program output, and comparing results between original and duplicated instructions. The intelligence of our solution is garnered through the use of control flow, memory dependence, and value profiling to understand and exploit the common-case behavior of applications. Our solution is able to achieve 92% fault coverage with a 20% instruction overhead. This represents a 41% lower performance overhead than the best prior approaches with approximately the same fault coverage.
Compiler-assisted preferred caching for embedded systems with STT-RAM based hybrid cache
Authors: Li Qingan , Zhao Mengying , Xue Chun Jason , He Yanxiang
Published: April 2020

As technology scales down, energy consumption is becoming a big problem for traditional SRAM-based cache hierarchies. The emerging Spin-Torque Transfer RAM (STT-RAM) is a promising replacement for large on-chip cache due to its ultra low leakage power and high storage density. However, write operations on STT-RAM suffer from considerably higher energy consumption and longer latency than SRAM. Hybrid cache consisting of both SRAM and STT-RAM has been proposed recently for both performance and energy efficiency. Most management strategies for hybrid caches employ migration-based techniques to dynamically move write-intensive data from STT-RAM to SRAM. These techniques lead to extra overheads. In this paper, we propose a compiler-assisted approach, preferred caching, to significantly reduce the migration overhead by giving migration-intensive memory blocks the preference for the SRAM part of the hybrid cache. Furthermore, a data assignment technique is proposed to improve the efficiency of preferred caching. The reduction of migration overhead can in turn improve the performance and energy efficiency of STT-RAM based hybrid cache. The experimental results show that, with the proposed techniques, on average, the number of migrations is reduced by 21.3%, the total latency is reduced by 8.0% and the total dynamic energy is reduced by 10.8%.
"Smart" design space sampling to predict Pareto-optimal solutions
Authors: Zuluaga Marcela , Krause Andreas , Milder Peter , Püschel Markus
Published: April 2020

Many high-level synthesis tools offer degrees of freedom in mapping high-level specifications to Register-Transfer Level descriptions. These choices do not affect the functional behavior but span a design space of different cost-performance tradeoffs. In this paper we present a novel machine learning-based approach that efficiently determines the Pareto-optimal designs while only sampling and synthesizing a fraction of the design space. The approach combines three key components: (1) A regression model based on Gaussian processes to predict area and throughput based on synthesis training data. (2) A "smart" sampling strategy, GP-PUCB, to iteratively refine the model by carefully selecting the next design to synthesize to maximize progress. (3) A stopping criterion based on assessing the accuracy of the model without access to complete synthesis data. We demonstrate the effectiveness of our approach using IP generators for discrete Fourier transforms and sorting networks. However, our algorithm is not specific to this application and can be applied to a wide range of Pareto front prediction problems.
Symbolic consistency checking of OpenMp parallel programs
Authors: Yu Fang , Yang Shun-Ching , Wang Farn , Chen Guan-Cheng , Chan Che-Chang
Published: April 2020

We present a symbolic approach for checking consistency of OpenMP parallel programs. A parallel program is consistent if it yields the same result as its sequential version despite the execution order among threads. We find race conditions of an OpenMP parallel program, construct the formal model of its raced segments under relaxed memory models, and perform guided symbolic simulation to search consistency violations. The simulation terminates when (1) a witness has been found (the program is inconsistent), or (2) all reachable states have been explored (the program is consistent). We have developed the tool Pathg by incorporating Omega library to solve race constraints and Red symbolic simulator to perform guided search. We show that Pathg can prove consistency of programs, identify races that modern OpenMP checkers failed to report, and find inconsistency witnesses effectively against benchmarks from the OpenMP Source Code Repository and the NAS Parallel benchmark suite.
Developing verified programs with Dafny
Authors: Leino K. Rustan M.
Published: April 2020

Reasoning about programs is a fundamental skill that every software engineer needs. This tutorial provides participants an opportunity to get hands-on experience with Dafny, a tool that can help develop this skill.

Dafny is a programming language and state-of-the-art program verifier. The language is type-safe and sequential, and it includes common imperative features, dynamic object allocation, and inductive datatypes. It also includes specification constructs like pre- and postconditions, which let a programmer record the intended behavior of the program along with the executable code that is supposed to cause that behavior. Because the Dafny verifier runs continuously in the background, the consistency of a program and its specifications is always enforced.

In this tutorial, I give a taste of how to use Dafny in program development. This includes an overview of Dafny, basics of writing specifications, how to debug verification attempts, and how to formulate and prove lemmas. Dafny has been used to verify a number of challenging algorithms, including Schorr-Waite graph marking, Floyd's ``tortoise and hare'' cycle-detection algorithm, and snapshotable trees with iterators. Dafny is also being used in teaching, with over 100,000 program-verification attempts submitted to the online version of the tool. Dafny was a popular choice in the VSTTE 2012 program verification competition, where two of the Dafny teams were among the competition's 6 medalists. Its open-source implementation has also been used as a foundation for other verification tools. More information is found from the Dafny project page, http://research.microsoft.com/dafny and in the references below. Binary downloads and sources are available from http://dafny.codeplex.com. The tool can also be run on the web at http://rise4fun.com/dafny, where there is an online version of the tutorial.
Service-oriented architecture (SOA) concepts and implementations
Authors: Sward Ricky E. , Boleng Jeff
Published: April 2020

This tutorial explains how to implement a Service-Oriented Architecture (SOA) for reliable systems using an Enterprise Service Bus (ESB) and the Ada Web Server (AWS). The first part of the tutorial describes terms of Service-Oriented Architectures (SOA) including service, service registry, service provider, service consumer, Service Oriented Architecture Protocol (SOAP), and Web Service Description Language (WSDL). This tutorial also presents principles of SOA including loose coupling, encapsulation, composability of web services, and statelessness of web services. The tutorial also covers the benefits of SOA and organizations that are supporting SOA infrastructure. The second part of the tutorial covers the Enterprise Service Bus (ESB) including definitions, capabilities, benefits and drawbacks. The tutorial discusses the difference between SOA and an ESB, as well as some of the commercially available ESB solutions on the market. The Mule ESB is explored in more detail and several examples are given. In the third part, the tutorial covers the Ada Web Server (AWS) built using the Ada programming language. The tutorial covers the capabilities of AWS and explains how to build and install AWS. The tutorial explains how to build an AWS server and include the server in an Ada application. The tutorial demonstrates how to build a call back function in AWS and build a response to a SOAP message. Finally, the tutorial explains how to connect an AWS server to an ESB endpoint. AWS is a key component to building a SOA for a reliable system. This capability allows the developer to expose services in a high-integrity system using the Ada and SPARK programming languages.
Keynote presentation
Authors: Liskov Barbara
Published: April 2020

Turing provided the basis for modern computer science. However there is a huge gap between a Turing machine and the kinds of applications we use today. This gap is bridged by software, and designing and implementing large programs is a difficult task. The main way we have of keeping the complexity of software under control is to make use of abstraction and modularity. This talk will discuss how abstraction and modularity are used in the design of large programs, and how these concepts are supported in modern programming languages. It will also discuss what support is needed going forward,
A formal foundation for dynamic delta-oriented software product lines
Authors: Damiani Ferruccio , Padovani Luca , Schaefer Ina
Published: April 2020

Delta-oriented programming (DOP) is a flexible approach for implementing software product lines (SPLs). DOP SPLs are implemented by a code base (a set of delta modules encapsulating changes to object-oriented programs) and a product line declaration (providing the connection of the delta modules with the product features). In this paper, we extend DOP by the capability to switch the implemented product configuration at runtime and present a formal foundation for dynamic DOP. A dynamic DOP SPL is a DOP SPL with a dynamic reconfiguration graph that specifies how to switch between different feature configurations. Dynamic DOP supports (unanticipated) software evolution such that at runtime, the product line declaration, the code base and the dynamic reconfiguration graph can be changed in any (unanticipated) way that preserves the currently running product. The type system of our dynamic DOP core calculus ensures that the dynamic reconfigurations lead to type safe products and do not cause runtime type errors.
Family-based deductive verification of software product lines
Authors: Thüm Thomas , Schaefer Ina , Apel Sven , Hentschel Martin
Published: April 2020

A software product line is a set of similar software products that share a common code base. While software product lines can be implemented efficiently using feature-oriented programming, verifying each product individually does not scale, especially if human effort is required (e.g., as in interactive theorem proving). We present a family-based approach of deductive verification to prove the correctness of a software product line efficiently. We illustrate and evaluate our approach for software product lines written in a feature-oriented dialect of Java and specified using the Java Modeling Language. We show that the theorem prover KeY can be used off-the-shelf for this task, without any modifications. Compared to the individual verification of each product, our approach reduces the verification time needed for our case study by more than 85%.
Pushouts in software architecture design
Authors: Riché T. L. , Gonçalves R. , Marker B. , Batory D.
Published: April 2020

A classical approach to program derivation is to progressively extend a simple specification and then incrementally refine it to an implementation. We claim this approach is hard or impractical when reverse engineering legacy software architectures. We present a case study that shows
optimizations
and
pushouts
---in addition to refinements and extensions---are essential for practical stepwise development of complex software architectures.
Faster program adaptation through reward attribution inference
Authors: Bauer Tim , Erwig Martin , Fern Alan , Pinto Jervis
Published: April 2020

In the adaptation-based programming (ABP) paradigm, programs may contain variable parts (function calls, parameter values, etc.) that can be take a number of different values. Programs also contain reward statements with which a programmer can provide feedback about how well a program is performing with respect to achieving its goals (for example, achieving a high score on some scale). By repeatedly running the program, a machine learning component will, guided by the rewards, gradually adjust the automatic choices made in the variable program parts so that they converge toward an optimal strategy.

ABP is a method for semi-automatic program generation in which the choices and rewards offered by programmers allow standard machine-learning techniques to explore a design space defined by the programmer to find an optimal instance of a program template. ABP effectively provides a DSL that allows non-machine-learning experts to exploit machine learning to generate self-optimizing programs.

Unfortunately, in many cases the placement and structuring of choices and rewards can have a detrimental effect on how an optimal solution to a program-generation problem can be found. To address this problem, we have developed a dataflow analysis that computes influence tracks of choices and rewards. This information can be exploited by an augmented machine-learning technique to ignore misleading rewards and to generally attribute rewards better to the choices that have actually influenced them. Moreover, this technique allows us to detect errors in the adaptive program that might arise out of program maintenance. Our evaluation shows that the dataflow analysis can lead to improvements in performance.
A calculus for modeling and implementing variation
Authors: Walkingshaw Eric , Erwig Martin
Published: April 2020

We present a formal calculus for modeling and implementing variation in software. It unifies the compositional and annotative approaches to feature implementation and supports the development of abstractions that can be used to directly relate feature models to their implementation. Since the compositional and annotative approaches are complementary, the calculus enables implementers to use the best combination of tools for the job and focus on inherent feature interactions, rather than those introduced by biases in the representation. The calculus also supports the abstraction of recurring variational patterns and provides a metaprogramming platform for organizing variation in artifacts.
Evaluation of monocular depth cues on a high-dynamic-range display for visualization
Authors: Easa Haider K. , Mantiuk Rafał K. , Lim Ik Soo
Published: April 2020

The aim of this work is to identify the depth cues that provide intuitive depth-ordering when used to visualize abstract data. In particular we focus on the depth cues that are effective on a high-dynamic-range (HDR) display: contrast and brightness. In an experiment participants were shown a visualization of the volume layers at different depths with a single isolated monocular cue as the only indication of depth. The observers were asked to identify which slice of the volume appears to be closer. The results show that brightness, contrast and relative size are the most effective monocular depth cues for providing an intuitive depth ordering.
L24
Authors: Stanley-Marbell Phillip
Published: April 2020

Networks of sensors must process large amounts of intermittently-available data in situ. This motivates the investigation of means for achieving high performance when required, but ultra-low-power dissipation when idle. One approach to this challenge is the use of embedded multiprocessor systems, leading to trade-offs between parallelism, performance, energy efficiency, and cost. To evaluate these trade-offs and to gain insight for future system designs, this article presents the design, implementation, and evaluation of a miniature, energy-scalable, 24-processor module,
L24
, for use in embedded sensor systems.

Analytic results and empirical evidence motivating such embedded multiprocessors is provided, and a parallel fixed-point fast Fourier transform implementation is presented. This application is used as a challenging but realistic evaluator of the presented hardware platform. Through a combination of hardware measurements, instruction-level microarchitectural simulation, and analytic modeling, it is demonstrated that the platform provides idle power dissipation over an order of magnitude lower than systems employing a monolithic processor of equivalent performance, while dynamic power dissipation remains competitive.

Taking into account both application computation and interprocessor communication demands, it is shown that there may exist an optimum operating voltage that minimizes either time-to-solution, energy usage, or the energy-delay product. This optimum operating point is formulated analytically, calibrated with system measurements, and evaluated for the hardware platform and application presented.
Software thread integration for instruction-level parallelism
Authors: So Won , Dean Alexander G.
Published: April 2020

Multimedia applications require a significantly higher level of performance than previous workloads of embedded systems. They have driven digital signal processor (DSP) makers to adopt high-performance architectures like VLIW (Very-Long Instruction Word). Despite many efforts to exploit instruction-level parallelism (ILP) in the application, the speed is a fraction of what it could be, limited by the difficulty of finding enough independent instructions to keep all of the processor's functional units busy.

This article proposes Software Thread Integration (STI) for instruction-level parallelism. STI is a software technique for interleaving multiple threads of control into a single implicitly multithreaded one. We use STI to improve the performance on ILP processors by merging parallel procedures into one, increasing the compiler's scope and hence allowing it to create a more efficient instruction schedule. Assuming the parallel procedures are given, we define a methodology for finding the best performing integrated procedure with a minimum compilation time.

We quantitatively estimate the performance impact of integration, allowing various integration scenarios to be compared and ranked via profitability analysis. During integration of threads, different ILP-improving code transformations are selectively applied according to the control structure and the ILP characteristics of the code, driven by interactions with software pipelining. The estimated profitability is verified and corrected by an iterative compilation approach, compensating for possible estimation inaccuracy. Our modeling methods combined with limited compilation quickly find the best integration scenario without requiring exhaustive integration.
Splittable pseudorandom number generators using cryptographic hashing
Authors: Claessen Koen , Pałka Michał H.
Published: April 2020

We propose a new splittable pseudorandom number generator (PRNG) based on a cryptographic hash function. Splittable PRNGs, in contrast to linear PRNGs, allow the creation of two (seemingly) independent generators from a given random number generator. Splittable PRNGs are very useful for structuring purely functional programs, as they avoid the need for threading around state. We show that the currently known and used splittable PRNGs are either not efficient enough, have inherent flaws, or lack formal arguments about their randomness. In contrast, our proposed generator can be implemented efficiently, and comes with a formal statements and proofs that quantify how 'random' the results are that are generated. The provided proofs give strong randomness guarantees under assumptions commonly made in cryptography.
Probabilistic relational verification for cryptographic implementations
Authors: Barthe Gilles , Fournet Cédric , Grégoire Benjamin , Strub Pierre-Yves , Swamy Nikhil , Zanella-Béguelin Santiago
Published: April 2020

Relational program logics have been used for mechanizing formal proofs of various cryptographic constructions. With an eye towards scaling these successes towards end-to-end security proofs for implementations of distributed systems, we present RF*, a relational extension of F*, a general-purpose higher-order stateful programming language with a verification system based on refinement types. The distinguishing feature of F* is a relational Hoare logic for a higher-order, stateful, probabilistic language. Through careful language design, we adapt the F* typechecker to generate both classic and relational verification conditions, and to automatically discharge their proofs using an SMT solver. Thus, we are able to benefit from the existing features of F*, including its abstraction facilities for modular reasoning about program fragments. We evaluate RF* experimentally by programming a series of cryptographic constructions and protocols, and by verifying their security properties, ranging from information flow to unlinkability, integrity, and privacy. Moreover, we validate the design of RF* by formalizing in Coq a core probabilistic λ calculus and a relational refinement type system and proving the soundness of the latter against a denotational semantics of the probabilistic lambda λ calculus.
A relationally parametric model of dependent type theory
Authors: Atkey Robert , Ghani Neil , Johann Patricia
Published: April 2020

Reynolds' theory of relational parametricity captures the invariance of polymorphically typed programs under change of data representation. Reynolds' original work exploited the typing discipline of the polymorphically typed lambda-calculus System F, but there is now considerable interest in extending relational parametricity to type systems that are richer and more expressive than that of System F.

This paper constructs parametric models of predicative and impredicative dependent type theory. The significance of our models is twofold. Firstly, in the impredicative variant we are able to deduce the existence of initial algebras for all
indexed=
functors. To our knowledge, ours is the first account of parametricity for dependent types that is able to lift the useful deduction of the existence of initial algebras in parametric models of System F to the dependently typed setting. Secondly, our models offer conceptual clarity by uniformly expressing relational parametricity for dependent types in terms of reflexive graphs, which allows us to unify the interpretations of types and kinds, instead of taking the relational interpretation of types as a primitive notion. Expressing our model in terms of reflexive graphs ensures that it has canonical choices for the interpretations of the standard type constructors of dependent type theory, except for the interpretation of the universe of small types, where we formulate a refined interpretation tailored for relational parametricity. Moreover, our reflexive graph model opens the door to generalisations of relational parametricity, for example to higher-dimensional relational parametricity.
Modular reasoning about heap paths via effectively propositional formulas
Authors: Itzhaky Shachar , Banerjee Anindya , Immerman Neil , Lahav Ori , Nanevski Aleksandar , Sagiv Mooly
Published: April 2020

First order logic with transitive closure, and separation logic enable elegant interactive verification of heap-manipulating programs. However, undecidabilty results and high asymptotic complexity of checking validity preclude complete automatic verification of such programs, even when loop invariants and procedure contracts are specified as formulas in these logics. This paper tackles the problem of procedure-modular verification of reachability properties of heap-manipulating programs using efficient decision procedures that are complete: that is, a SAT solver must generate a counterexample whenever a program does not satisfy its specification. By (a) requiring each procedure modifies a fixed set of heap partitions and creates a bounded amount of heap sharing, and (b) restricting program contracts and loop invariants to use only deterministic paths in the heap, we show that heap reachability updates can be described in a simple manner. The restrictions force program specifications and verification conditions to lie within a fragment of first-order logic with transitive closure that is reducible to effectively propositional logic, and hence facilitate sound, complete and efficient verification. We implemented a tool atop Z3 and report on preliminary experiments that establish the correctness of several programs that manipulate linked data structures.
Symbolic optimization with SMT solvers
Authors: Li Yi , Albarghouthi Aws , Kincaid Zachary , Gurfinkel Arie , Chechik Marsha
Published: April 2020

The rise in efficiency of Satisfiability Modulo Theories (SMT) solvers has created numerous uses for them in software verification, program synthesis, functional programming, refinement types, etc. In all of these applications, SMT solvers are used for generating satisfying assignments (e.g., a witness for a bug) or proving unsatisfiability/validity(e.g., proving that a subtyping relation holds). We are often interested in finding not just an arbitrary satisfying assignment, but one that optimizes (minimizes/maximizes) certain criteria. For example, we might be interested in detecting program executions that maximize energy usage (performance bugs), or synthesizing short programs that do not make expensive API calls. Unfortunately, none of the available SMT solvers offer such optimization capabilities.

In this paper, we present SYMBA, an efficient SMT-based optimization algorithm for
objective functions
in the theory of linear real arithmetic (LRA). Given a formula φ and an objective function
t
, SYMBA finds a satisfying assignment of φthat maximizes the value of
t
. SYMBA utilizes efficient SMT solvers as black boxes. As a result, it is easy to implement and it directly benefits from future advances in SMT solvers. Moreover, SYMBA can optimize a set of objective functions, reusing information between them to speed up the analysis. We have implemented SYMBA and evaluated it on a large number of optimization benchmarks drawn from program analysis tasks. Our results indicate the power and efficiency of SYMBA in comparison with competing approaches, and highlight the importance of its multi-objective-function feature.
Consistency analysis of decision-making programs
Authors: Chaudhuri Swarat , Farzan Azadeh , Kincaid Zachary
Published: April 2020

Applications in many areas of computing make discrete decisions under
uncertainty
, for reasons such as limited numerical precision in calculations and errors in sensor-derived inputs. As a result, individual decisions made by such programs may be nondeterministic, and lead to contradictory decisions at different points of an execution. This means that an otherwise correct program may execute along paths, that it would not follow under its ideal semantics, violating essential program invariants on the way. A program is said to be
consistent
if it does not suffer from this problem despite uncertainty in decisions.

In this paper, we present a sound, automatic program analysis for verifying that a program is consistent in this sense. Our analysis proves that each decision made along a program execution is consistent with the decisions made earlier in the execution. The proof is done by generating an invariant that abstracts the set of all decisions made along executions that end at a program location
l
, then verifying, using a fixpoint constraint-solver, that no contradiction can be derived when these decisions are combined with new decisions made at
l
.

We evaluate our analysis on a collection of programs implementing algorithms in
computational geometry
. Consistency is known to be a critical, frequently-violated, and thoroughly studied correctness property in geometry, but ours is the first attempt at automated verification of consistency of geometric algorithms. Our benchmark suite consists of implementations of convex hull computation, triangulation, and point location algorithms. On almost all examples that are not consistent (with two exceptions), our analysis is able to verify consistency within a few minutes.
NetKAT
Authors: Anderson Carolyn Jane , Foster Nate , Guha Arjun , Jeannin Jean-Baptiste , Kozen Dexter , Schlesinger Cole , Walker David
Published: April 2020

Recent years have seen growing interest in high-level languages for programming networks. But the design of these languages has been largely ad hoc, driven more by the needs of applications and the capabilities of network hardware than by foundational principles. The lack of a semantic foundation has left language designers with little guidance in determining how to incorporate new features, and programmers without a means to reason precisely about their code.

This paper presents NetKAT, a new network programming language that is based on a solid mathematical foundation and comes equipped with a sound and complete equational theory. We describe the design of NetKAT, including primitives for filtering, modifying, and transmitting packets; union and sequential composition operators; and a Kleene star operator that iterates programs. We show that NetKAT is an instance of a canonical and well-studied mathematical structure called a Kleene algebra with tests (KAT) and prove that its equational theory is sound and complete with respect to its denotational semantics. Finally, we present practical applications of the equational theory including syntactic techniques for checking reachability, proving non-interference properties that ensure isolation between programs, and establishing the correctness of compilation algorithms.
Counter-factual typing for debugging type errors
Authors: Chen Sheng , Erwig Martin
Published: April 2020

Changing a program in response to a type error plays an important part in modern software development. However, the generation of good type error messages remains a problem for highly expressive type systems. Existing approaches often suffer from a lack of precision in locating errors and proposing remedies. Specifically, they either fail to locate the source of the type error consistently, or they report too many potential error locations. Moreover, the change suggestions offered are often incorrect. This makes the debugging process tedious and ineffective.

We present an approach to the problem of type debugging that is based on generating and filtering a comprehensive set of type-change suggestions. Specifically, we generate all (program-structure-preserving) type changes that can possibly fix the type error. These suggestions will be ranked and presented to the programmer in an iterative fashion. In some cases we also produce suggestions to change the program. In most situations, this strategy delivers the correct change suggestions quickly, and at the same time never misses any rare suggestions. The computation of the potentially huge set of type-change suggestions is efficient since it is based on a variational type inference algorithm that type checks a program with variations only once, efficiently reusing type information for shared parts.

We have evaluated our method and compared it with previous approaches. Based on a large set of examples drawn from the literature, we have found that our method outperforms other approaches and provides a viable alternative.
Sound compilation of reals
Authors: Darulova Eva , Kuncak Viktor
Published: April 2020

Writing accurate numerical software is hard because of many sources of unavoidable uncertainties, including finite numerical precision of implementations. We present a programming model where the user writes a program in a real-valued implementation and specification language that explicitly includes different types of uncertainties. We then present a compilation algorithm that generates a finite-precision implementation that is guaranteed to meet the desired precision with respect to real numbers. Our compilation performs a number of verification steps for different candidate precisions. It generates verification conditions that treat all sources of uncertainties in a unified way and encode reasoning about finite-precision roundoff errors into reasoning about real numbers. Such verification conditions can be used as a standardized format for verifying the precision and the correctness of numerical programs. Due to their non-linear nature, precise reasoning about these verification conditions remains difficult and cannot be handled using state-of-the art SMT solvers alone. We therefore propose a new procedure that combines exact SMT solving over reals with approximate and sound affine and interval arithmetic. We show that this approach overcomes scalability limitations of SMT solvers while providing improved precision over affine and interval arithmetic. Our implementation gives promising results on several numerical models, including dynamical systems, transcendental functions, and controller implementations.
Battery transition systems
Authors: Boker Udi , Henzinger Thomas A. , Radhakrishna Arjun
Published: April 2020

The analysis of the energy consumption of software is an important goal for quantitative formal methods. Current methods, using weighted transition systems or energy games, model the energy source as an ideal resource whose status is characterized by one number, namely the amount of remaining energy. Real batteries, however, exhibit behaviors that can deviate substantially from an ideal energy resource. Based on a discretization of a standard continuous battery model, we introduce {\em battery transition systems}. In this model, a battery is viewed as consisting of two parts -- the available-charge tank and the bound-charge tank. Any charge or discharge is applied to the available-charge tank. Over time, the energy from each tank diffuses to the other tank.

Battery transition systems are infinite state systems that, being not well-structured, fall into no decidable class that is known to us. Nonetheless, we are able to prove that the $\omega$-regular model-checking problem is decidable for battery transition systems. We also present a case study on the verification of control programs for energy-constrained semi-autonomous robots.
Backpack
Authors: Kilpatrick Scott , Dreyer Derek , Peyton Jones Simon , Marlow Simon
Published: April 2020

Module systems like that of Haskell permit only a weak form of modularity in which module implementations depend directly on other implementations and must be processed in dependency order. Module systems like that of ML, on the other hand, permit a stronger form of modularity in which explicit interfaces express assumptions about dependencies, and each module can be typechecked and reasoned about independently.

In this paper, we present Backpack, a new language for building separately-typecheckable *packages* on top of a weak module system like Haskell's. The design of Backpack is inspired by the MixML module calculus of Rossberg and Dreyer, but differs significantly in detail. Like MixML, Backpack supports explicit interfaces and recursive linking. Unlike MixML, Backpack supports a more flexible applicative semantics of instantiation. Moreover, its design is motivated less by foundational concerns and more by the practical concern of integration into Haskell, which has led us to advocate simplicity---in both the syntax and semantics of Backpack---over raw expressive power. The semantics of Backpack packages is defined by elaboration to sets of Haskell modules and binary interface files, thus showing how Backpack maintains interoperability with Haskell while extending it with separate typechecking. Lastly, although Backpack is geared toward integration into Haskell, its design and semantics are largely agnostic with respect to the details of the underlying core language.
Complexity column
Authors: Immerman Neil
Published: April 2020

I am pleased to announce that I will be editing a quarterly column on Logic and Complexity for the SIGLOG newsletter. The topic of logic and complexity is quite broad: computational complexity is a central issue for most areas in logic and computer science. While checking if a program has a certain property, or more generally if a statement is true, is typically undecidable, as a community we have made great progress in developing algorithms and building tools that perform these tasks in many useful cases. Similarly we have shown that many key problems are complete for a wide range of complexity classes.
On linear recurrence sequences and loop termination
Authors: Ouaknine Joël , Worrell James
Published: April 2020

A sequence of real numbers is said to be
positive
if all terms are positive, and
ultimately positive
if all but finitely many terms are positive. In this article we survey recent progress on long-standing open problems concerning deciding the positivity and ultimate positivity of integer linear recurrence sequences. We briefly discuss some of the many contexts in which these problems arise, and relate them to the well-known Skolem Problem, which asks whether a given linear recurrence sequence has a zero term. We also highlight some of the mathematical techniques that have been used to obtain decision procedures for these problems, pointing out obstacles to further progress.

In the second half of this survey we move on to closely related questions concerning the termination of linear while loops. This is a well-studied subject in software verification and by now there is rich toolkit of techniques to prove termination in practice. However the decidability of termination for some of the most basic types of loop remains open. Here again we discuss recent progress and remaining open problems.
Semantics column
Authors: Mislove Michael
Published: April 2020

This quarter's column is by ALEXANDRA SILVA, who works on coalgebras, among other things. Alexandra provides us with an introduction to coalgebras and their role in computational models, and uses them to analyze a fascinating illustrative example: Brzozowski's Algorithm, which takes as input a finite state automaton, and as if by magic, produces the minimal automaton accepting the same language. Unraveling this algorithm and revealing its underlying mechanism is a lovely example of coalgebras at work, and indeed, the results that Alexandra describes have been the topic of an invited lecture at LICS [Panangaden 2013].
Conference reports
Authors: Pérez Jorge A.
Published: April 2020

It will be my pleasure to edit the column on conference reports in the SIGLOG newsletter. A distinguishing aspect of computer science with respect to other areas is the prominent role that conferences, workshops, and professional meetings play in scientific dissemination and interaction. Conferences closely related to SIGLOG are highly reputed venues in the field. These include the ACM-IEEE Symposium on Logic in Computer Science (LICS), the EACSL Conference on Computer Science Logic (CSL), the International Colloquium on Automata, Languages and Programming (ICALP), but also several others. Moreover, well-established conferences frequently host co-located satellite events which bear witness to the vitality of our community by addressing recent advances and trends. Given the impact and visibility that these scientific meetings have, it is only natural that the SIGLOG newsletter includes reports on them.
An improved homomorphism preservation theorem from lower bounds in circuit complexity
Authors: Rossman Benjamin
Published: April 2020

Previous work of the author [Rossman 2008a] showed that the Homomorphism Preservation Theorem of classical model theory remains valid when its statement is restricted to finite structures. In this paper, we give a new proof of this result via a reduction to lower bounds in circuit complexity, specifically on the AC
0
formula size of the colored subgraph isomorphism problem. Formally, we show the following: if a first-order sentence Φ of quantifier-rank
k
is preserved under homomorphisms on finite structures, then it is equivalent on finite structures to an existential-positive sentence Ψ of quantifier-rank
k

O
(1)

. Quantitatively, this improves the result of [Rossman 2008a], where the upper bound on the quantifier-rank of Ψ is a non-elementary function of
k.
Provenance analysis for FOL model checking
Authors: Tannen Val
Published: April 2020

This article is a recasting in the realm of logic of some of the work I have done on
provenance for database transformations
in collaboration with a number of wonderful people (see Acknowledgments).
Engineering Multi-Agent Systems
Authors: Mascardi Viviana , Weyns Danny , Ricci Alessandro , Earle Clara Benac , Casals Arthur , Challenger Moharram , Chopra Amit , Ciortea Andrei , Dennis Louise A. , Díaz Álvaro Fernández , El Fallah-Seghrouchni Amal , Ferrando Angelo , Fredlund Lars-Åke , Giunchiglia Eleonora , Guessoum Zahia , Günay Akin , Hindriks Koen , Iglesias Carlos A. , Logan Brian , Kampik Timotheus , Kardas Geylani , Koeman Vincent J. , Larsen John Bruntse , Mayer Simon , Méndez Tasio , Nieves Juan Carlos , Seidita Valeria , Teze Baris Tekin , Varga László Z. , Winikoff Michael
Published: April 2020

The continuous integration of software-intensive systems together with the ever-increasing computing power offer a breeding ground for intelligent agents and multi-agent systems (MAS) more than ever before. Over the past two decades, a wide variety of languages, models, techniques and methodologies have been proposed to engineer agents and MAS. Despite this substantial body of knowledge and expertise, the systematic engineering of large-scale and open MAS still poses many challenges. Researchers and engineers still face fundamental questions regarding theories, architectures, languages, processes, and platforms for designing, implementing, running, maintaining, and evolving MAS. This paper reports on the results of the 6th International Workshop on Engineering Multi-Agent Systems (EMAS 2018, 14th-15th of July, 2018, Stockholm, Sweden), where participants discussed the issues above focusing on the state of affairs and the road ahead for researchers and engineers in this area.
Mucins and the Microbiome
Authors: Hansson Gunnar C.
Published: April 2020

Generating the barriers that protect our inner surfaces from bacteria and other challenges requires large glycoproteins called mucins. These come in two types, gel-forming and transmembrane, all characterized by large, highly O-glycosylated mucin domains that are diversely decorated by Golgi glycosyltransferases to become extended rodlike structures. The general functions of mucins on internal epithelial surfaces are to wash away microorganisms and, even more importantly, to build protective barriers. The latter function is most evident in the large intestine, where the inner mucus layer separates the numerous commensal bacteria from the epithelial cells. The host's conversion of MUC2 to the outer mucus layer allows bacteria to degrade the mucin glycans and recover the energy content that is then shared with the host. The molecular nature of the mucins is complex, and how they construct the extracellular complex glycocalyx and mucus is poorly understood and a future biochemical challenge.
Operando Identification of Liquid Intermediates in Lithium–Sulfur Batteries via Transmission UV–vis Spectroscopy
Authors: He Qi , Freiberg Anna T. S. , Patel Manu U. M. , Qian Simon , Gasteiger Hubert A.
Published: April 2020

Lithium-sulfur (Li-S) batteries are facing various challenges with regards to performance and durability, and further improvements require a better understanding of the fundamental working mechanisms, including an identification of the reaction intermediates in an operating Li-S battery. In this study, we present an operando transmission UV–vis spectro-electrochemical cell design that employs a conventional sulfur/carbon composite electrode, propose a comprehensive peak assignment for polysulfides in DOL:DME-based electrolyte, and finally identify the liquid intermediates in the discharging process of an operating Li-S cell. Here, we propose for the first time a meta-stable polysulfide species (S3
2−) that is present at substantial concentrations during the 2nd discharge plateau in a Li-S battery. We identify the S3
2− species that are the reduction product of S4
2−, as deducted from the analysis of the obtained operando UV–vis spectra along with the transferred charge, and confirmed by rotating ring disk electrode measurements for the reduction of a solution with a nominal Li2S4 stoichiometry. Furthermore, our operando results provide insight into the potential-dependent stability of different S-species and the rate-limiting (electro)chemical steps during discharging. Finally, we propose a viable reaction pathway of how S8 is electrochemically reduced to Li2S2/Li2S based on our operando results as well as that reported in the literature.