bluuebunny/crossref_metadata_2025 huggingface dataset:
Memory safety in C by abstract interpretation
Authors: Jones Joseph , Wasson James , Brown Sean , Poulsen Seth , Aldous Peter , Mercer Eric
Published: January 2019

Pointer arithmetic is a core feature of the C programming language and C program analysis is impossible without an understanding of its effects. Many program analyses opt to be unsound in the presence of pointer arithmetic or preserve soundness at the cost of precision. However, the number of operations that can be performed on pointers is actually quite small. As was observed by Might et al., these few operations can be precisely modeled with a simplified Peano arithmetic. This paper presents an interpreter that uses a memory model based on this arithmetic. It desugars C programs to a simple imperative language using standard semantics-preserving techniques to simplify the interpretation. The result is a prototype analysis that reasons precisely about memory safety in full C programs without programmer annotations.
Multi-Directional navigation method for optimized consumption of user generated content through semantic mapping of features derived from the user generated content
Authors: Jain Ajay , Soni Sachin
Published: January 2019

Gone are the days when a buyer used to depend solely on the product marketing team to know what's good about a product or product features. With the advent of social media, product purchase has become democratic with product buyers, product users are vocal about reporting back their experience about the product. According to Forrester, "buyers will spend more time on web pages that have social content than those that don't" and "user-generated content has significant influence on a buyer's purchase decision." The research doesn't lie- User Generated Content (termed as UGC) is more effective at driving purchase intent and brand loyalty than any other media. To create engaging, authentic customer experiences, companies should weave UGC throughout their owned websites, showcasing the voices that consumers trust the most: their own.
Report of the 1st International Workshop on Context-aware Autonomous and Smart Architectures (CASA@ECSA 2017)
Authors: Raibulet Claudia , Fugini Mariagrazia , Drira Khalil , Pelliccione Patrizio , Gerostathopoulos Ilias , Prehofer Christian , Moessner Klaus
Published: January 2019

The 2017 1st International Workshop on Context-aware, Autonomous and Smart Architectures (CASA 2017) was held in conjunction with the 11th European Conference on Software Architecture (ECSA 2017), on September, 12th, 2017 in Canterbury, United Kingdom. The goal of this one-day workshop was to bring together researchers and practitioners from academic environment and from the industry to share their solutions, ideas, visions, and doubts in the design of software architectures for context-aware, autonomous, and smart solutions. The workshop focused on architectural aspects offering a complementary vision of such solutions with respect to the available application- and user-oriented perspectives on context-awareness, autonomy, and smartness. Furthermore, the workshop aimed to enable discussions, partnerships, and collaborations among the software engineers interested in these solutions.
The Effect of Software Warranties on Cybersecurity
Authors: van der Linden Dirk , Rashid Awais
Published: January 2019

This workshop focused on bringing software developers and legal professionals together to understand the shared challenges they face in promoting the development of secure software on the one hand, and software at all, on the other hand. This report sum- marizes current scienti c research on the topics and challenges discussed in the workshop breakout sessions. The insights from the workshop highlight a number of interesting directions for fur- ther research on the interplay between software warranties and cybersecurity.
Higher inductive types in cubical computational type theory
Authors: Cavallo Evan , Harper Robert
Published: January 2019

Homotopy type theory proposes
higher inductive types
(HITs) as a means of defining and reasoning about inductively-generated objects with higher-dimensional structure. As with the univalence axiom, however, homotopy type theory does not specify the computational behavior of HITs. Computational interpretations have now been provided for univalence and specific HITs by way of cubical type theories, which use a judgmental infrastructure of dimension variables. We extend the cartesian cubical computational type theory introduced by Angiuli et al. with a schema for indexed cubical inductive types (CITs), an adaptation of higher inductive types to the cubical setting. In doing so, we isolate the canonical values of a cubical inductive type and prove a canonicity theorem with respect to these values.
Bisimulation as path type for guarded recursive types
Authors: Møgelberg Rasmus Ejlers , Veltri Niccolò
Published: January 2019

In type theory, coinductive types are used to represent processes, and are thus crucial for the formal verification of non-terminating reactive programs in proof assistants based on type theory, such as Coq and Agda. Currently, programming and reasoning about coinductive types is difficult for two reasons: The need for recursive definitions to be productive, and the lack of coincidence of the built-in identity types and the important notion of bisimilarity.

Guarded recursion in the sense of Nakano has recently been suggested as a possible approach to dealing with the problem of productivity, allowing this to be encoded in types. Indeed, coinductive types can be encoded using a combination of guarded recursion and universal quantification over clocks. This paper studies the notion of bisimilarity for guarded recursive types in Ticked Cubical Type Theory, an extension of Cubical Type Theory with guarded recursion. We prove that, for any functor, an abstract, category theoretic notion of bisimilarity for the final guarded coalgebra is equivalent (in the sense of homotopy type theory) to path equality (the primitive notion of equality in cubical type theory). As a worked example we study a guarded notion of labelled transition systems, and show that, as a special case of the general theorem, path equality coincides with an adaptation of the usual notion of bisimulation for processes. In particular, this implies that guarded recursion can be used to give simple equational reasoning proofs of bisimilarity. This work should be seen as a step towards obtaining bisimilarity as path equality for coinductive types using the encodings mentioned above.
Fully abstract module compilation
Authors: Crary Karl
Published: January 2019

We give a translation suitable for compilation of modern module calculi supporting sealing, generativity, translucent signatures, applicative functors, higher-order functors and/or first-class modules. Ours is the first module-compilation translation with a dynamic correctness theorem. The theorem states that the translation produces target terms that are contextually equivalent to the source, in an appropriate sense. A corollary of the theorem is that the translation is fully abstract. Consequently, the translation preserves all abstraction present in the source. In passing, we also show that modules are a definitional extension of the underlying core language. All of our proofs are formalized in Coq.
Polymorphic symmetric multiple dispatch with variance
Authors: Park Gyunghee , Hong Jaemin , Steele Jr. Guy L. , Ryu Sukyoung
Published: January 2019

Many object-oriented languages provide method overloading, which allows multiple method declarations with the same name. For a given method invocation, in order to choose what method declaration to invoke, multiple dispatch considers the run-time types of the arguments. While multiple dispatch can support binary methods (such as mathematical operators) intuitively and consistently, it is difficult to guarantee that calls will be neither ambiguous nor undefined at run time, especially in the presence of expressive language features such as multiple inheritance and parametric polymorphism. Previous efforts have formalized languages that include such features by using overloading rules that guarantee a unique and type-sound resolution of each overloaded method call; in many cases, such rules resolve ambiguity by treating the arguments asymmetrically. Here we present the first formal specification of a strongly typed object-oriented language with symmetric multiple dispatch, multiple inheritance, and parametric polymorphism with variance. We define both a static (type- checking) semantics and a dynamic (dispatching) semantics and prove the type soundness of the language, thus demonstrating that our novel dynamic dispatch algorithm is consistent with the static semantics. Details of our dynamic dispatch algorithm address certain technical challenges that arise from structural asymmetries inherent in object-oriented languages (e.g., classes typically declare ancestors explicitly but not descendants).
Abstracting extensible data types: or, rows by any other name
Authors: Morris J. Garrett , McKinna James
Published: January 2019

We present a novel typed language for extensible data types, generalizing and abstracting existing systems of row types and row polymorphism. Extensible data types are a powerful addition to traditional functional programming languages, capturing ideas from OOP-like record extension and polymorphism to modular compositional interpreters. We introduce row theories, a monoidal generalization of row types, giving a general account of record concatenation and projection (dually, variant injection and branching). We realize them via qualified types, abstracting the interpretation of records and variants over different row theories. Our approach naturally types terms untypable in other systems of extensible data types, while maintaining strong metatheoretic properties, such as coherence and principal types. Evidence for type qualifiers has computational content, determining the implementation of record and variant operations; we demonstrate this in giving a modular translation from our calculus, instantiated with various row theories, to polymorphic λ-calculus.
Gradual parametricity, revisited
Authors: Toro Matías , Labrada Elizabeth , Tanter Éric
Published: January 2019

Bringing the benefits of gradual typing to a language with parametric polymorphism like System F, while preserving relational parametricity, has proven extremely challenging: first attempts were formulated a decade ago, and several designs were recently proposed. Among other issues, these proposals can however signal parametricity errors in unexpected situations, and improperly handle type instantiations when imprecise types are involved. These observations further suggest that existing polymorphic cast calculi are not well suited for supporting a gradual counterpart of System F. Consequently, we revisit the challenge of designing a gradual language with explicit parametric polymorphism, exploring the extent to which the Abstracting Gradual Typing methodology helps us derive such a language, GSF. We present the design and metatheory of GSF, and provide a reference implementation. In addition to avoiding the uncovered semantic issues, GSF satisfies all the expected properties of a gradual parametric language, save for one property: the dynamic gradual guarantee, which was left as conjecture in all prior work, is here proven to be simply incompatible with parametricity. We nevertheless establish a weaker property that allows us to disprove several claims about gradual free theorems, clarifying the kind of reasoning supported by gradual parametricity.
Categorical combinatorics of scheduling and synchronization in game semantics
Authors: Mellies Paul-André
Published: January 2019

Game semantics is the art of interpreting types as games and programs as strategies interacting in space and time with their environment. In order to reflect the interactive behavior of programs, strategies are required to follow specific scheduling policies. Typically, in the case of a purely sequential programming language, the program (Player) and its environment (Opponent) will play one after the other, in a strictly alternating way. On the other hand, in the case of a concurrent language, Player and Opponent will be allowed to play several moves in a row, in a non-alternating way. In both cases, the scheduling policy is designed very carefully in order to ensure that the strategies synchronize properly and compose well when plugged together. A longstanding conceptual problem has been to understand when and why a given scheduling policy works and is compositional in that sense. In this paper, we exhibit a number of simple and fundamental combinatorial structures which ensure that a given scheduling policy encoded as synchronization template defines a symmetric monoidal closed (and in fact star-autonomous) bicategory of games, strategies and simulations. To that purpose, we choose to work at a very general level, and illustrate our method by constructing two template game models of linear logic with different flavors (alternating and non-alternating) using the same categorical combinatorics, performed in the category of small categories. As a whole, the paper may be seen as a hymn in praise of synchronization, building on the notion of synchronization algebra in process calculi and adapting it smoothly to programming language semantics, using a combination of ideas at the converging point of game semantics and of categorical algebra.
Fixpoint games on continuous lattices
Authors: Baldan Paolo , König Barbara , Mika-Michalski Christina , Padoan Tommaso
Published: January 2019

Many analysis and verifications tasks, such as static program analyses and model-checking for temporal logics, reduce to the solution of systems of equations over suitable lattices. Inspired by recent work on lattice-theoretic progress measures, we develop a game-theoretical approach to the solution of systems of monotone equations over lattices, where for each single equation either the least or greatest solution is taken. A simple parity game, referred to as fixpoint game, is defined that provides a correct and complete characterisation of the solution of systems of equations over continuous lattices, a quite general class of lattices widely used in semantics. For powerset lattices the fixpoint game is intimately connected with classical parity games for µ-calculus model-checking, whose solution can exploit as a key tool Jurdziński’s small progress measures. We show how the notion of progress measure can be naturally generalised to fixpoint games over continuous lattices and we prove the existence of small progress measures. Our results lead to a constructive formulation of progress measures as (least) fixpoints. We refine this characterisation by introducing the notion of selection that allows one to constrain the plays in the parity game, enabling an effective (and possibly efficient) solution of the game, and thus of the associated verification problem. We also propose a logic for specifying the moves of the existential player that can be used to systematically derive simplified equations for efficiently computing progress measures. We discuss potential applications to the model-checking of latticed µ-calculi.
Exceptional asynchronous session types: session types without tiers
Authors: Fowler Simon , Lindley Sam , Morris J. Garrett , Decova Sára
Published: January 2019

Session types statically guarantee that communication complies with a protocol. However, most accounts of session typing do not account for failure, which means they are of limited use in real applications---especially distributed applications---where failure is pervasive.

We present the first formal integration of asynchronous session types with exception handling in a functional programming language. We define a core calculus which satisfies preservation and progress properties, is deadlock free, confluent, and terminating.

We provide the first implementation of session types with exception handling for a fully-fledged functional programming language, by extending the Links web programming language; our implementation draws on existing work on effect handlers. We illustrate our approach through a running example of two-factor authentication, and a larger example of a session-based chat application where communication occurs over session-typed channels and disconnections are handled gracefully.
Quantitative robustness analysis of quantum programs
Authors: Hung Shih-Han , Hietala Kesha , Zhu Shaopeng , Ying Mingsheng , Hicks Michael , Wu Xiaodi
Published: January 2019

Quantum computation is a topic of significant recent interest, with practical advances coming from both research and industry. A major challenge in quantum programming is dealing with errors (quantum noise) during execution. Because quantum resources (e.g., qubits) are scarce, classical error correction techniques applied at the level of the architecture are currently cost-prohibitive. But while this reality means that quantum programs are almost certain to have errors, there as yet exists no principled means to reason about erroneous behavior. This paper attempts to fill this gap by developing a semantics for erroneous quantum while-programs, as well as a logic for reasoning about them. This logic permits proving a property we have identified, called є-robustness, which characterizes possible “distance” between an ideal program and an erroneous one. We have proved the logic sound, and showed its utility on several case studies, notably: (1) analyzing the robustness of noisy versions of the quantum Bernoulli factory (QBF) and quantum walk (QW); (2) demonstrating the (in)effectiveness of different error correction schemes on single-qubit errors; and (3) analyzing the robustness of a fault-tolerant version of QBF.
A domain theory for statistical probabilistic programming
Authors: Vákár Matthijs , Kammar Ohad , Staton Sam
Published: January 2019

We give an adequate denotational semantics for languages with recursive higher-order types, continuous probability distributions, and soft constraints. These are expressive languages for building Bayesian models of the kinds used in computational statistics and machine learning. Among them are untyped languages, similar to Church and WebPPL, because our semantics allows recursive mixed-variance datatypes. Our semantics justifies important program equivalences including commutativity.

Our new semantic model is based on `quasi-Borel predomains'. These are a mixture of chain-complete partial orders (cpos) and quasi-Borel spaces. Quasi-Borel spaces are a recent model of probability theory that focuses on sets of admissible random elements. Probability is traditionally treated in cpo models using probabilistic powerdomains, but these are not known to be commutative on any class of cpos with higher order functions. By contrast, quasi-Borel predomains do support both a commutative probabilistic powerdomain and higher-order functions. As we show, quasi-Borel predomains form both a model of Fiore's axiomatic domain theory and a model of Kock's synthetic measure theory.
Bayesian synthesis of probabilistic programs for automatic data modeling
Authors: Saad Feras A. , Cusumano-Towner Marco F. , Schaechtle Ulrich , Rinard Martin C. , Mansinghka Vikash K.
Published: January 2019

We present new techniques for automatically constructing probabilistic programs for data analysis, interpretation, and prediction. These techniques work with probabilistic domain-specific data modeling languages that capture key properties of a broad class of data generating processes, using Bayesian inference to synthesize probabilistic programs in these modeling languages given observed data. We provide a precise formulation of Bayesian synthesis for automatic data modeling that identifies sufficient conditions for the resulting synthesis procedure to be sound. We also derive a general class of synthesis algorithms for domain-specific languages specified by probabilistic context-free grammars and establish the soundness of our approach for these languages. We apply the techniques to automatically synthesize probabilistic programs for time series data and multivariate tabular data. We show how to analyze the structure of the synthesized programs to compute, for key qualitative properties of interest, the probability that the underlying data generating process exhibits each of these properties. Second, we translate probabilistic programs in the domain-specific language into probabilistic programs in Venture, a general-purpose probabilistic programming system. The translated Venture programs are then executed to obtain predictions of new time series data and new multivariate data records. Experimental results show that our techniques can accurately infer qualitative structure in multiple real-world data sets and outperform standard data analysis methods in forecasting and predicting new data.
code2vec: learning distributed representations of code
Authors: Alon Uri , Zilberstein Meital , Levy Omer , Yahav Eran
Published: January 2019

We present a neural model for representing snippets of code as continuous distributed vectors (``code embeddings''). The main idea is to represent a code snippet as a single fixed-length code vector, which can be used to predict semantic properties of the snippet. To this end, code is first decomposed to a collection of paths in its abstract syntax tree. Then, the network learns the atomic representation of each path while simultaneously learning how to aggregate a set of them.

We demonstrate the effectiveness of our approach by using it to predict a method's name from the vector representation of its body. We evaluate our approach by training a model on a dataset of 12M methods. We show that code vectors trained on this dataset can predict method names from files that were unobserved during training. Furthermore, we show that our model learns useful method name vectors that capture semantic similarities, combinations, and analogies.

A comparison of our approach to previous techniques over the same dataset shows an improvement of more than 75%, making it the first to successfully predict method names based on a large, cross-project corpus. Our trained model, visualizations and vector similarities are available as an interactive online demo at http://code2vec.org. The code, data and trained models are available at https://github.com/tech-srl/code2vec.
An abstract domain for certifying neural networks
Authors: Singh Gagandeep , Gehr Timon , Püschel Markus , Vechev Martin
Published: January 2019

We present a novel method for scalable and precise certification of deep neural networks. The key technical insight behind our approach is a new abstract domain which combines floating point polyhedra with intervals and is equipped with abstract transformers specifically tailored to the setting of neural networks. Concretely, we introduce new transformers for affine transforms, the rectified linear unit (ReLU), sigmoid, tanh, and maxpool functions.

We implemented our method in a system called DeepPoly and evaluated it extensively on a range of datasets, neural architectures (including defended networks), and specifications. Our experimental results indicate that DeepPoly is more precise than prior work while scaling to large networks.

We also show how to combine DeepPoly with a form of abstraction refinement based on trace partitioning. This enables us to prove, for the first time, the robustness of the network when the input image is subjected to complex perturbations such as rotations that employ linear interpolation.
A²I: abstract² interpretation
Authors: Cousot Patrick , Giacobazzi Roberto , Ranzato Francesco
Published: January 2019

The fundamental idea of Abstract
2
Interpretation (A
2
I), also called meta-abstract interpretation, is to apply abstract interpretation to abstract interpretation-based static program analyses. A
2
I is generally meant to use abstract interpretation to analyse properties of program analysers. A
2
I can be either offline or online. Offline A
2
I is performed either before the program analysis, such as variable packing used by the Astrée program analyser, or after the program analysis, such as in alarm diagnosis. Online A
2
I is performed during the program analysis, such as Venet’s cofibred domains or Halbwachs et al.’s and Singh et al.’s variable partitioning techniques for fast polyhedra/numerical abstract domains. We formalize offline and online meta-abstract interpretation and illustrate this notion with the design of widenings and the decomposition of relational abstract domains to speed-up program analyses. This shows how novel static analyses can be extracted as meta-abstract interpretations to design efficient and precise program analysis algorithms.
Concerto: a framework for combined concrete and abstract interpretation
Authors: Toman John , Grossman Dan
Published: January 2019

Abstract interpretation promises sound but computable static summarization of program behavior. However, modern software engineering practices pose significant challenges to this vision, specifically the extensive use of frameworks and complex libraries. Frameworks heavily use reflection, metaprogramming, and multiple layers of abstraction, all of which confound even state-of-the-art abstract interpreters. Sound but conservative analysis of frameworks is impractically imprecise, and unsoundly ignoring reflection and metaprogramming is untenable given the prevalence of these features. Manually modeling framework behaviors offers excellent precision, at the cost of immense effort by the tool designer.

To overcome the above difficulties, we present Concerto, a system for analyzing framework-based applications by soundly combining concrete and abstract interpretation. Concerto analyzes framework implementations using concrete interpretation, and application code using abstract interpretation. This technique is possible in practice as framework implementations typically follow a single path of execution when provided a concrete, application-specific configuration file which is often available at analysis time. Concerto exploits this configuration information to precisely resolve reflection and other metaprogramming idioms during concrete execution. In contrast, application code may have infinitely many paths of execution, so Concerto switches to abstract interpretation to analyze application code. Concerto is an analysis framework, and can be instantiated with any abstract interpretation that satisfies a small set of preconditions. In addition, unlike manual modeling, Concerto is not specialized to any specific framework implementation. We have formalized our approach and proved several important properties including soundness and termination. In addition, we have implemented an initial proof of concept prototype of Concerto for a subset of Java, and found that our combined interpretation significantly improves analysis precision and performance.
Skeletal semantics and their interpretations
Authors: Bodin Martin , Gardner Philippa , Jensen Thomas , Schmitt Alan
Published: January 2019

The development of mechanised language specification based on structured operational semantics, with applications to verified compilers and sound program analysis, requires huge effort. General theory and frameworks have been proposed to help with this effort. However, none of this work provides a systematic way of developing concrete and abstract semantics, connected together by a general consistency result. We introduce a
skeletal semantics
of a language, where each skeleton describes the complete semantic behaviour of a language construct. We define a general notion of
interpretation
, which provides a systematic and language-independent way of deriving semantic judgements from the skeletal semantics. We explore four generic interpretations: a simple well-formedness interpretation; a concrete interpretation; an abstract interpretation; and a constraint generator for flow-sensitive analysis. We prove general
consistency results
between interpretations, depending only on simple language-dependent lemmas. We illustrate our ideas using a simple While language.
Refinement of path expressions for static analysis
Authors: Cyphert John , Breck Jason , Kincaid Zachary , Reps Thomas
Published: January 2019

Algebraic program analyses compute information about a program’s behavior by first (a) computing a valid
path expression
—i.e., a regular expression that recognizes all feasible execution paths (and usually more)—and then (b) interpreting the path expression in a semantic algebra that defines the analysis. There are an infinite number of different regular expressions that qualify as valid path expressions, which raises the question “
Which one should we choose?
” While any choice yields a sound result, for many analyses the choice can have a drastic effect on the precision of the results obtained. This paper investigates the following two questions: (1)
What does it mean for one valid path expression to be “better” than another
? (2)
Can we compute a valid path expression that is “better,” and if so, how
? We show that it is not satisfactory to compare two path expressions
E
1
and
E
2
solely by means of the
languages that they generate
. Counter to one’s intuition, it is possible for
L
(
E
2
) ⊊
L
(
E
1
), yet for
E
2
to produce a
less-precise
analysis result than
E
1
—and thus we would not want to perform the transformation
E
1
→
E
2
. However, the exclusion of paths so as to analyze a smaller language of paths is exactly the refinement criterion used by some prior methods.

In this paper, we develop an algorithm that takes as input a valid path expression
E
, and returns a valid path expression
E
′ that is guaranteed to yield analysis results that are at least as good as those obtained using
E
. While the algorithm sometimes returns
E
itself, it typically does not: (i) we prove a
no-degradation result
for the algorithm’s base case—for transforming a leaf loop (i.e., a most-deeply-nested loop); (ii) at a non-leaf loop
L
, the algorithm treats each loop
L
′ in the body of
L
as an indivisible atom, and applies the leaf-loop algorithm to
L
; the no-degradation result carries over to (ii), as well. Our experiments show that the technique has a substantial impact: the loop-refinement algorithm allows the implementation of Compositional Recurrence Analysis to prove over 25% more assertions for a collection of challenging loop micro-benchmarks.
Decidable verification of uninterpreted programs
Authors: Mathur Umang , Madhusudan P. , Viswanathan Mahesh
Published: January 2019

We study the problem of completely automatically verifying uninterpreted programs—programs that work over arbitrary data models that provide an interpretation for the constants, functions and relations the program uses. The verification problem asks whether a given program satisfies a postcondition written using quantifier-free formulas with equality on the final state, with no loop invariants, contracts, etc. being provided. We show that this problem is undecidable in general. The main contribution of this paper is a subclass of programs, called
coherent programs
that admits decidable verification, and can be decided in Pspace. We then extend this class of programs to classes of programs that are
k
-coherent, where
k
∈ ℕ, obtained by (automatically) adding
k
ghost variables and assignments that make them coherent. We also extend the decidability result to programs with recursive function calls and prove several undecidability results that show why our restrictions to obtain decidability seem necessary.
Modular quantitative monitoring
Authors: Alur Rajeev , Mamouras Konstantinos , Stanford Caleb
Published: January 2019

In real-time decision making and runtime monitoring applications, declarative languages are commonly used as they facilitate modular high-level specifications with the compiler guaranteeing evaluation over data streams in an efficient and incremental manner. We introduce the model of
Data Transducers
to allow
modular
compilation of queries over streaming data. A data transducer maintains a finite set of data variables and processes a sequence of tagged data values by updating its variables using an allowed set of operations. The model allows unambiguous nondeterminism, exponentially succinct control, and combining values from parallel threads of computation. The semantics of the model immediately suggests an efficient streaming algorithm for evaluation. The expressiveness of data transducers coincides with
streamable regular transductions
, a robust and streamable class of functions characterized by MSO-definable string-to-DAG transformations with no backward edges. We show that the novel features of data transducers, unlike previously studied transducers, make them as succinct as traditional imperative code for processing data streams, but the structuring of the transition function permits modular compilation. In particular, we show that operations such as parallel composition, union, prefix-sum, and quantitative analogs of combinators for unambiguous parsing, can be implemented by natural and succinct constructions on data transducers. To illustrate the benefits of such modularity in compilation, we define a new language for quantitative monitoring, QRE-Past, that integrates features of past-time temporal logic and quantitative regular expressions. While this combination allows a natural specification of a cardiac arrhythmia detection algorithm in QRE-Past, compilation of QRE-Past specifications into efficient monitors comes for free thanks to succinct constructions on data transducers.
Fast and exact analysis for LRU caches
Authors: Touzeau Valentin , Maïza Claire , Monniaux David , Reineke Jan
Published: January 2019

For applications in worst-case execution time analysis and in security, it is desirable to statically classify memory accesses into those that result in cache hits, and those that result in cache misses. Among cache replacement policies, the least recently used (LRU) policy has been studied the most and is considered to be the most predictable.

The state-of-the-art in LRU cache analysis presents a tradeoff between precision and analysis efficiency: The classical approach to analyzing programs running on LRU caches, an abstract interpretation based on a range abstraction, is very fast but can be imprecise. An exact analysis was recently presented, but, as a last resort, it calls a model checker, which is expensive.

In this paper, we develop an analysis based on abstract interpretation that comes close to the efficiency of the classical approach, while achieving exact classification of all memory accesses as the model-checking approach. Compared with the model-checking approach we observe speedups of several orders of magnitude. As a secondary contribution we show that LRU cache analysis problems are in general NP-complete.
Closed forms for numerical loops
Authors: Kincaid Zachary , Breck Jason , Cyphert John , Reps Thomas
Published: January 2019

This paper investigates the problem of reasoning about non-linear behavior of simple numerical loops. Our approach builds on classical techniques for analyzing the behavior of linear dynamical systems. It is well-known that a closed-form representation of the behavior of a linear dynamical system can always be expressed using algebraic numbers, but this approach can create formulas that present an obstacle for automated-reasoning tools. This paper characterizes when linear loops have closed forms in simpler theories that are more amenable to automated reasoning. The algorithms for computing closed forms described in the paper avoid the use of algebraic numbers, and produce closed forms expressed using polynomials and exponentials over rational numbers. We show that the logic for expressing closed forms is decidable, yielding decision procedures for verifying safety and termination of a class of numerical loops over rational numbers. We also show that the procedure for computing closed forms for this class of numerical loops can be used to over-approximate the behavior of arbitrary numerical programs (with unrestricted control flow, non-deterministic assignments, and recursive procedures).
Iron: managing obligations in higher-order concurrent separation logic
Authors: Bizjak Aleš , Gratzer Daniel , Krebbers Robbert , Birkedal Lars
Published: January 2019

Precise management of resources and the obligations they impose, such as the need to dispose of memory, close locks, and release file handles, is hard---especially in the presence of concurrency, when some resources are shared, and different threads operate on them concurrently. We present Iron, a novel higher-order concurrent separation logic that allows for precise reasoning about resources that are transferable among dynamically allocated threads. In particular, Iron can be used to show the correctness of challenging examples, where the reclamation of memory is delegated to a forked-off thread. We show soundness of Iron by means of a model of Iron, defined on top of the Iris base logic, and we use this model to prove that memory resources are accounted for precisely and not leaked. We have formalized all of the developments in the Coq proof assistant.
On library correctness under weak memory consistency: specifying and verifying concurrent libraries under declarative consistency models
Authors: Raad Azalea , Doko Marko , Rožić Lovro , Lahav Ori , Vafeiadis Viktor
Published: January 2019

Concurrent libraries are the building blocks for concurrency. They encompass a range of abstractions (locks, exchangers, stacks, queues, sets) built in a layered fashion: more advanced libraries are built out of simpler ones. While there has been a lot of work on verifying such libraries in a sequentially consistent (SC) environment, little is known about how to specify and verify them under weak memory consistency (WMC).

We propose a general declarative framework that allows us to specify concurrent libraries declaratively, and to verify library implementations against their specifications compositionally. Our framework is sufficient to encode standard models such as SC, (R)C11 and TSO. Additionally, we specify several concurrent libraries, including mutual exclusion locks, reader-writer locks, exchangers, queues, stacks and sets. We then use our framework to verify multiple weakly consistent implementations of locks, exchangers, queues and stacks.
Bridging the gap between programming languages and hardware weak memory models
Authors: Podkopaev Anton , Lahav Ori , Vafeiadis Viktor
Published: January 2019

We develop a new intermediate weak memory model, IMM, as a way of modularizing the proofs of correctness of compilation from concurrent programming languages with weak memory consistency semantics to mainstream multi-core architectures, such as POWER and ARM. We use IMM to prove the correctness of compilation from the promising semantics of Kang et al. to POWER (thereby correcting and improving their result) and ARMv7, as well as to the recently revised ARMv8 model. Our results are mechanized in Coq, and to the best of our knowledge, these are the first machine-verified compilation correctness results for models that are weaker than x86-TSO.
CT-wasm: type-driven secure cryptography for the web ecosystem
Authors: Watt Conrad , Renner John , Popescu Natalie , Cauligi Sunjay , Stefan Deian
Published: January 2019

A significant amount of both client and server-side cryptography is implemented in JavaScript. Despite widespread concerns about its security, no other language has been able to match the convenience that comes from its ubiquitous support on the "web ecosystem" - the wide variety of technologies that collectively underpins the modern World Wide Web. With the introduction of the new WebAssembly bytecode language (Wasm) into the web ecosystem, we have a unique opportunity to advance a principled alternative to existing JavaScript cryptography use cases which does not compromise this convenience.

We present Constant-Time WebAssembly (CT-Wasm), a type-driven, strict extension to WebAssembly which facilitates the verifiably secure implementation of cryptographic algorithms. CT-Wasm's type system ensures that code written in CT-Wasm is both information flow secure and resistant to timing side channel attacks; like base Wasm, these guarantees are verifiable in linear time. Building on an existing Wasm mechanization, we mechanize the full CT-Wasm specification, prove soundness of the extended type system, implement a verified type checker, and give several proofs of the language's security properties.

We provide two implementations of CT-Wasm: an OCaml reference interpreter and a native implementation for Node.js and Chromium that extends Google's V8 engine. We also implement a CT-Wasm to Wasm rewrite tool that allows developers to reap the benefits of CT-Wasm's type system today, while developing cryptographic algorithms for base Wasm environments. We evaluate the language, our implementations, and supporting tools by porting several cryptographic primitives - Salsa20, SHA-256, and TEA - and the full TweetNaCl library. We find that CT-Wasm is fast, expressive, and generates code that we experimentally measure to be constant-time.
Genetic improvement events in 2018
Authors: Danglot Benjamin , An Gabin
Published: January 2019

Genetic improvement uses optimisation and machine learning techniques, particularly heuristic search and evolutionary algorithms, to improve existing software. The main application is automatic bug fixing, where reducing or eliminating buggy behaviour improves a program. Other applications involve automatically producing a better program that runs faster, uses less memory, uses less energy, or runs on a different type of computer.

This article summarise two international events exclusively devoted to this topic in 2018.
Smarcal1 and Zranb3 Protect Replication Forks from Myc-Induced DNA Replication Stress
Authors: Puccetti Matthew V. , Adams Clare M. , Kushinsky Saul , Eischen Christine M.
Published: January 2019

The cellular DNA replication stress response functions to stabilize DNA replication forks and inhibits genome instability and tumorigenesis induced by oncogenes. However, the specific proteins required for resolving oncogenic stress remain poorly understood. Here we report that Smarcal1 and Zranb3, closely related replication fork–remodeling proteins, have nonredundant functions in resolving Myc-induced DNA replication stress. In Myc-overexpressing primary cells, significant differences in replication fork stalling, collapse, and DNA damage were detected between cells deficient in Smarcal1 or Zranb3, leading to changes in proliferation and apoptosis. These differences were also reflected in Myc-induced lymphoma development; haploinsufficiency of Smarcal1 resulted in accelerated lymphomagenesis, whereas haploinsufficiency of Zranb3 inhibited lymphoma development. Complete loss of either protein resulted in disparate survival outcomes. Our results reveal that endogenous replication stress from Myc in primary cells requires both alleles of Smarcal1 and Zranb3 and demonstrate the requirement of both proteins to stabilize replication forks upon Myc dysregulation in a nonredundant manner.

Significance:

Smarcal1 and Zranb3 are essential, but nonredundant, for responding to DNA replication stress and stabilizing replication forks following Myc overexpression.

See related commentary by Sotiriou and Halazonetis, p. 1297
SUV39H1 Represses the Expression of Cytotoxic T-Lymphocyte Effector Genes to Promote Colon Tumor Immune Evasion
Authors: Lu Chunwan , Yang Dafeng , Klement John D. , Oh Il Kyu , Savage Natasha M. , Waller Jennifer L. , Colby Aaron H. , Grinstaff Mark W. , Oberlies Nicholas H. , Pearce Cedric J. , Xie Zhiliang , Kulp Samuel K. , Coss Christopher C. , Phelps Mitch A. , Albers Thomas , Lebedyeva Iryna O. , Liu Kebin
Published: January 2019

Despite the presence of CTLs in the tumor microenvironment, the majority of immunogenic human colon cancer does not respond to immune checkpoint inhibitor immunotherapy, and microsatellite instable (MSI) tumors are not naturally eliminated. The molecular mechanism underlying the inactivity of tumor-infiltrating CTLs is unknown. We report here that CTLs were present in both MSI and microsatellite stable colon tumors. The expression of the H3K9me3-specific histone methyltransferase SUV39H1 was significantly elevated in human colon carcinoma compared with normal colon tissues. Using a mouse colon carcinoma model, we further determined that tumor-infiltrating CTLs in the colon tumor microenvironment have high expression of SUV39H1. To target SUV39H1 in the tumor microenvironment, a virtual chemical library was screened on the basis of the SET (suppressor of variegation 3–9, enhancer of zeste and trithorax) domain structure of the human SUV39H1 protein. Functional enzymatic activity assays identified a small molecule that inhibits SUV39H1 enzymatic activity. On the basis of the structure of this small molecule, we modified it and chemically synthesized a small molecule, termed F5446, which has an EC50 of 0.496 μmol/L for SUV39H1 enzymatic activity. H3K9me3 was enriched in the promoters of GZMB, PRF1, FASLG, and IFNG in quiescent T cells. F5446 inhibited H3K9me3, thereby upregulating expression of these effectors in tumor-infiltrating CTLs and suppressing colon carcinoma growth in a CD8+ CTL-dependent manner in vivo. Our data indicate that SUV39H1 represses CTL effector gene expression and, in doing so, confers colon cancer immune escape.
Effectiveness and Adverse Events of Early Laparoscopic Therapy versus Conservative Treatment for Tubo-Ovarian or Pelvic Abscess: A Single-Center Retrospective Cohort Study
Authors: Chu Lei , Ma Hanbo , Liang Junhua , Li Li , Shen Aiqun , Wang Jianjun , Li Huaifang , Tong Xiaowen
Published: January 2019

Background/Aim: We aimed to assess the value of early laparoscopic therapy in management of tubo-ovarian abscess (TOA) or pelvic abscess. Methods: This was a retrospective study of all consecutive patients who were initially diagnosed with TOA or pelvic abscess at the local hospital between January 2010 and December 2014. The risks of operation and recurrence were analyzed using logistic analyses. Results: The durations of body temperature > 38.0°C (p = 0.001) and hospitalization (p < 0.001) were longer in the conventional group versus the early laparoscopy group. In the conventional group, 15 (50%) patients finally underwent laparoscopic exploration. The abscess size in the late laparoscopic group was significantly larger than the successful antibiotic treatment group (6.3 ± 1.5 vs. 4.9 ± 1.2 cm, p = 0.010). Abscess > 5.5 cm was independently associated with antibiotic failure (OR 4.571; 95% CI 1.612–12.962). Compared with late laparoscopy, early laparoscopy was associated with a shorter operation time (p = 0.037), less blood loss (p = 0.035), and shorter durations of body temperature > 38.0°C (p < 0.001) and hospitalization (p < 0.001). The cost was the lowest in the patients successfully treated conservatively. Conclusion: Early laparoscopic treatment is associated with shorter time of fever resolution, shorter hospitalization, and less blood loss compared with conventional treatment for TOA or pelvic abscess.