bluuebunny/crossref_metadata_2025 huggingface dataset:
Reliance on science: Worldwide front‐page patent citations to scientific articles
Authors: Marx Matt , Fuegi Aaron
Published: April 2020

Research summary

To what extent do firms rely on basic science in their R&D efforts? Several scholars have sought to answer this and related questions, but progress has been impeded by the difficulty of matching unstructured references in patents to published papers. We introduce an open‐access dataset of references from the front pages of patents granted worldwide to scientific papers published since 1800. Each patent‐paper linkage is assigned a confidence score, which is characterized in a random sample by false negatives versus false positives. All matches are available for download at http://relianceonscience.org. We outline several avenues for strategy research enabled by these new data.

Managerial summary

To what extent do firms rely on basic science in their R&D efforts? Several scholars have sought to answer this and related questions, but progress has been impeded by the difficulty of matching unstructured references in patents to published papers. We introduce an open‐access dataset of references from the front pages of patents granted worldwide to scientific papers published since 1800. Each patent‐paper linkage is assigned a confidence score, and we check a random sample of these confidence scores by hand in order to estimate both coverage (i.e., of the matches we should have found, what percentage did we find) and accuracy (i.e., of the matches we found, what percentage are correct). We outline several avenues for strategy research enabled by these new data.
Preparation of open‐tubular CEC column bonded with 6‐O‐monotosyl‐deoxy‐β‐cyclodextrin and its application in the enantioseparation of several related benzimidazoles
Authors: Fan Shitong , Guan Jin , Yan Feng , Zhang Dongxiang , Shi Shuang , Wang Silin
Published: April 2020

A new chiral open‐tubular capillary electrochromatography column was prepared with 6‐O‐monotosyl‐deoxy‐β‐cyclodextrin as staionary phase by covalent immobilization on inner wall of a fused‐silica capillary. Preparation procedure of the open‐tubular column was investigated and resulting surface morphology was determined using scanning electron microscopy. Moreover, the enantiomeric separation performance of open‐tubular capillary electrochromatography column was evaluated by using several related benzimidazoles as model analytes, including pantoprazole, tenatoprazole, omeprazole, and lansoprazole. The primary factors affecting its separation efficiency, such as type, concentration, and pH of buffer, applied voltage were optimized. In the optimum conditions, the enantiomers of four analytes revealed high resolutions of 5.75–8.83. The relative standard deviation values for the migrated times and resolutions of the model analyte representing intraday, interday, and column‐to‐column were less than 1.8 and 1.3%, respectively. The chiral open‐tubular capillary electrochromatography column still had satisfactory separation performance after continuous use for 72 h or intermittent use for 3 months.
Trace-Relating Compiler Correctness and Secure Compilation
Authors: Abate Carmine , Blanco Roberto , Ciobâcă Ștefan , Durier Adrien , Garg Deepak , Hrițcu Cătălin , Patrignani Marco , Tanter Éric , Thibault Jérémy
Published: April 2020

Compiler correctness is, in its simplest form, defined as the inclusion of the set of traces of the compiled program into the set of traces of the original program, which is equivalent to the preservation of all trace properties. Here traces collect, for instance, the externally observable events of each execution. This definition requires, however, the set of traces of the source and target languages to be exactly the same, which is not the case when the languages are far apart or when observations are fine-grained. To overcome this issue, we study a generalized compiler correctness definition, which uses source and target traces drawn from potentially different sets and connected by an arbitrary relation. We set out to understand what guarantees this generalized compiler correctness definition gives us when instantiated with a non-trivial relation on traces. When this trace relation is not equality, it is no longer possible to preserve the trace properties of the source program unchanged. Instead, we provide a generic characterization of the target trace property ensured by correctly compiling a program that satisfies a given source property, and dually, of the source trace property one is required to show in order to obtain a certain target property for the compiled code. We show that this view on compiler correctness can naturally account for undefined behavior, resource exhaustion, different source and target values, side-channels, and various abstraction mismatches. Finally, we show that the same generalization also applies to many secure compilation definitions, which characterize the protection of a compiled program against linked adversarial code.
Exploring Type-Level Bisimilarity towards More Expressive Multiparty Session Types
Authors: Jongmans Sung-Shik , Yoshida Nobuko
Published: April 2020

A key open problem with multiparty session types (MPST) concerns their expressiveness: current MPST have inflexible choice, no existential quantification over participants, and limited parallel composition. This precludes many real protocols to be represented by MPST. To overcome these bottlenecks of MPST, we explore a new technique using weak bisimilarity between global types and endpoint types, which guarantees deadlock-freedom and absence of protocol violations. Based on a process algebraic framework, we present well-formed conditions for global types that guarantee weak bisimilarity between a global type and its endpoint types and prove their check is decidable. Our main practical result, obtained through benchmarks, is that our well-formedness conditions can be checked orders of magnitude faster than directly checking weak bisimilarity using a state-of-the-art model checker.
Aneris: A Mechanised Logic for Modular Reasoning about Distributed Systems
Authors: Krogh-Jespersen Morten , Timany Amin , Ohlenbusch Marit Edna , Gregersen Simon Oddershede , Birkedal Lars
Published: April 2020

Building network-connected programs and distributed systems is a powerful way to provide scalability and availability in a digital, always-connected era. However, with great power comes great complexity. Reasoning about distributed systems is well-known to be difficult. In this paper we present , a novel framework based on separation logic supporting modular, node-local reasoning about concurrent and distributed systems. The logic is higher-order, concurrent, with higher-order store and network sockets, and is fully mechanized in the Coq proof assistant. We use our framework to verify an implementation of a load balancer that uses multi-threading to distribute load amongst multiple servers and an implementation of the two-phase-commit protocol with a replicated logging service as a client. The two examples certify that is well-suited for both horizontal and vertical modular reasoning.
Semantic Foundations for Deterministic Dataflow and Stream Processing
Authors: Mamouras Konstantinos
Published: April 2020

We propose a denotational semantic framework for deterministic dataflow and stream processing that encompasses a variety of existing streaming models. Our proposal is based on the idea that data streams, stream transformations, and stream-processing programs should be classified using types. The type of a data stream is captured formally by a monoid, an algebraic structure with a distinguished binary operation and a unit. The elements of a monoid model the finite fragments of a stream, the binary operation represents the concatenation of stream fragments, and the unit is the empty fragment. Stream transformations are modeled using monotone functions on streams, which we call stream transductions. These functions can be implemented using abstract machines with a potentially infinite state space, which we call stream transducers. This abstract typed framework of stream transductions and transducers can be used to (1) verify the correctness of streaming computations, that is, that an implementation adheres to the desired behavior, (2) prove the soundness of optimizing transformations, e.g. for parallelization and distribution, and (3) inform the design of programming models and query languages for stream processing. In particular, we show that several useful combinators can be supported by the full class of stream transductions and transducers: serial composition, parallel composition, and feedback composition.
RustHorn: CHC-Based Verification for Rust Programs
Authors: Matsushita Yusuke , Tsukada Takeshi , Kobayashi Naoki
Published: April 2020

Reduction to the satisfiablility problem for constrained Horn clauses (CHCs) is a widely studied approach to automated program verification. The current CHC-based methods for pointer-manipulating programs, however, are not very scalable. This paper proposes a novel translation of pointer-manipulating Rust programs into CHCs, which clears away pointers and heaps by leveraging ownership. We formalize the translation for a simplified core of Rust and prove its correctness. We have implemented a prototype verifier for a subset of Rust and confirmed the effectiveness of our method.
A First-Order Logic with Frames
Authors: Murali Adithya , Peña Lucas , Löding Christof , Madhusudan P.
Published: April 2020

We propose a novel logic, called Frame Logic (FL), that extends first-order logic (with recursive definitions) using a construct $$\textit{Sp}(\cdot )$$

Sp
(
·
)

that captures the implicit supports of formulas— the precise subset of the universe upon which their meaning depends. Using such supports, we formulate proof rules that facilitate frame reasoning elegantly when the underlying model undergoes change. We show that the logic is expressive by capturing several data-structures and also exhibit a translation from a precise fragment of separation logic to frame logic. Finally, we design a program logic based on frame logic for reasoning with programs that dynamically update heaps that facilitates local specifications and frame reasoning. This program logic consists of both localized proof rules as well as rules that derive the weakest tightest preconditions in FL.
Solving Program Sketches with Large Integer Values
Authors: Pan Rong , Hu Qinheping , Singh Rishabh , D’Antoni Loris
Published: April 2020

Program sketching is a program synthesis paradigm in which the programmer provides a partial program with holes and assertions. The goal of the synthesizer is to automatically find integer values for the holes so that the resulting program satisfies the assertions. The most popular sketching tool, Sketch, can efficiently solve complex program sketches, but uses an integer encoding that often performs poorly if the sketched program manipulates large integer values. In this paper, we propose a new solving technique that allows Sketch to handle large integer values while retaining its integer encoding. Our technique uses a result from number theory, the Chinese Remainder Theorem, to rewrite program sketches to only track the remainders of certain variable values with respect to several prime numbers. We prove that our transformation is sound and the encoding of the resulting programs are exponentially more succinct than existing Sketch encodings. We evaluate our technique on a variety of benchmarks manipulating large integer values. Our technique provides speedups against both existing Sketch solvers and can solve benchmarks that existing Sketch solvers cannot handle.
Higher-Ranked Annotation Polymorphic Dependency Analysis
Authors: Thorand Fabian , Hage Jurriaan
Published: April 2020

The precision of a static analysis can be improved by increasing the context-sensitivity of the analysis. In a type-based formulation of static analysis for functional languages this can be achieved by, e.g., introducing let-polyvariance or subtyping. In this paper we go one step further by defining a higher-ranked polyvariant type system so that even properties of lambda-bound identifiers can be generalized over. We do this for dependency analysis, a generic analysis that can be instantiated to a range of different analyses that in this way all can profit.

We prove that our analysis is sound with respect to a call-by-name semantics and that it satisfies a so-called noninterference property. We provide a type reconstruction algorithm that we have proven to be terminating, and sound and complete with respect to its declarative specification. Our principled description can serve as a blueprint for making other analyses higher-ranked.
ConSORT: Context- and Flow-Sensitive Ownership Refinement Types for Imperative Programs
Authors: Toman John , Siqi Ren , Suenaga Kohei , Igarashi Atsushi , Kobayashi Naoki
Published: April 2020

We present ConSORT, a type system for safety verification in the presence of mutability and aliasing. Mutability requires strong updates to model changing invariants during program execution, but aliasing between pointers makes it difficult to determine which invariants must be updated in response to mutation. Our type system addresses this difficulty with a novel combination of refinement types and fractional ownership types. Fractional ownership types provide flow-sensitive and precise aliasing information for reference variables. ConSORT interprets this ownership information to soundly handle strong updates of potentially aliased references. We have proved ConSORT sound and implemented a prototype, fully automated inference tool. We evaluated our tool and found it verifies non-trivial programs including data structure implementations.
Higher-Order Spreadsheets with Spilled Arrays
Authors: Williams Jack , Joharizadeh Nima , Gordon Andrew D. , Sarkar Advait
Published: April 2020

We develop a theory for two recently-proposed spreadsheet mechanisms: gridlets allow for abstraction and reuse in spreadsheets, and build on spilled arrays, where an array value spills out of one cell into nearby cells. We present the first formal calculus of spreadsheets with spilled arrays. Since spilled arrays may collide, the semantics of spilling is an iterative process to determine which arrays spill successfully and which do not. Our first theorem is that this process converges deterministically. To model gridlets, we propose the grid calculus, a higher-order extension of our calculus of spilled arrays with primitives to treat spreadsheets as values. We define a semantics of gridlets as formulas in the grid calculus. Our second theorem shows the correctness of a remarkably direct encoding of the Abadi and Cardelli object calculus into the grid calculus. This result is the first rigorous analogy between spreadsheets and objects; it substantiates the intuition that gridlets are an object-oriented counterpart to functional programming extensions to spreadsheets, such as sheet-defined functions.
Concise Read-Only Specifications for Better Synthesis of Programs with Pointers
Authors: Costea Andreea , Zhu Amy , Polikarpova Nadia , Sergey Ilya
Published: April 2020

In program synthesis there is a well-known trade-off between concise and strong specifications: if a specification is too verbose, it might be harder to write than the program; if it is too weak, the synthesised program might not match the user’s intent. In this work we explore the use of annotations for restricting memory access permissions in program synthesis, and show that they can make specifications much stronger while remaining surprisingly concise. Specifically, we enhance Synthetic Separation Logic (SSL), a framework for synthesis of heap-manipulating programs, with the logical mechanism of read-only borrows.

We observe that this minimalistic and conservative SSL extension benefits the synthesis in several ways, making it more (a) expressive (stronger correctness guarantees are achieved with a modest annotation overhead), (b) effective (it produces more concise and easier-to-read programs), (c) efficient (faster synthesis), and (d) robust (synthesis efficiency is less affected by the choice of the search heuristic). We explain the intuition and provide formal treatment for read-only borrows. We substantiate the claims (a)–(d) by describing our quantitative evaluation of the borrowing-aware synthesis implementation on a series of standard benchmark specifications for various heap-manipulating programs.
Liberate Abstract Garbage Collection from the Stack by Decomposing the Heap
Authors: Germane Kimball , Adams Michael D.
Published: April 2020

Abstract garbage collection and the use of pushdown systems each enhance the precision of control-flow analysis (CFA). However, their respective needs conflict: abstract garbage collection requires the stack but pushdown systems obscure it. Though several existing techniques address this conflict, none take full advantage of the underlying interplay. In this paper, we dissolve this conflict with a technique which exploits the precision of pushdown systems to decompose the heap across the continuation.This technique liberates abstract garbage collection from the stack, increasing its effectiveness and the compositionality of its host analysis. We generalize our approach to apply compositional treatment to abstract timestamps which induces the context abstraction of m-CFA, an abstraction more precise than k-CFA’s for many common programming patterns.
SMT-Friendly Formalization of the Solidity Memory Model
Authors: Hajdu Ákos , Jovanović Dejan
Published: April 2020

Solidity is the dominant programming language for Ethereum smart contracts. This paper presents a high-level formalization of the Solidity language with a focus on the memory model. The presented formalization covers all features of the language related to managing state and memory. In addition, the formalization we provide is effective: all but few features can be encoded in the quantifier-free fragment of standard SMT theories. This enables precise and efficient reasoning about the state of smart contracts written in Solidity. The formalization is implemented in the SOLC-VERIFY verifier and we provide an extensive set of tests that covers the breadth of the required semantics. We also provide an evaluation on the test set that validates the semantics and shows the novelty of the approach compared to other Solidity-level contract analysis tools.
Constructing Infinitary Quotient-Inductive Types
Authors: Fiore Marcelo P. , Pitts Andrew M. , Steenkamp S. C.
Published: April 2020

This paper introduces an expressive class of quotient-inductive types, called QW-types. We show that in dependent type theory with uniqueness of identity proofs, even the infinitary case of QW-types can be encoded using the combination of inductive-inductive definitions involving strictly positive occurrences of Hofmann-style quotient types, and Abel’s size types. The latter, which provide a convenient constructive abstraction of what classically would be accomplished with transfinite ordinals, are used to prove termination of the recursive definitions of the elimination and computation properties of our encoding of QW-types. The development is formalized using the Agda theorem prover.
Relative Full Completeness for Bicategorical Cartesian Closed Structure
Authors: Fiore Marcelo , Saville Philip
Published: April 2020

The glueing construction, defined as a certain comma category, is an important tool for reasoning about type theories, logics, and programming languages. Here we extend the construction to accommodate ‘2-dimensional theories’ of types, terms between types, and rewrites between terms. Taking bicategories as the semantic framework for such systems, we define the glueing bicategory and establish a bicategorical version of the well-known construction of cartesian closed structure on a glueing category. As an application, we show that free finite-product bicategories are fully complete relative to free cartesian closed bicategories, thereby establishing that the higher-order equational theory of rewriting in the simply-typed lambda calculus is a conservative extension of the algebraic equational theory of rewriting in the fragment with finite products only.
A Duality Theoretic View on Limits of Finite Structures
Authors: Gehrke Mai , Jakl Tomáš , Reggio Luca
Published: April 2020

A systematic theory of structural limits for finite models has been developed by Nešetřil and Ossona de Mendez. It is based on the insight that the collection of finite structures can be embedded, via a map they call the Stone pairing, in a space of measures, where the desired limits can be computed. We show that a closely related but finer grained space of measures arises — via Stone-Priestley duality and the notion of types from model theory — by enriching the expressive power of first-order logic with certain “probabilistic operators”. We provide a sound and complete calculus for this extended logic and expose the functorial nature of this construction.

The consequences are two-fold. On the one hand, we identify the logical gist of the theory of structural limits. On the other hand, our construction shows that the duality-theoretic variant of the Stone pairing captures the adding of a layer of quantifiers, thus making a strong link to recent work on semiring quantifiers in logic on words. In the process, we identify the model theoretic notion of types as the unifying concept behind this link. These results contribute to bridging the strands of logic in computer science which focus on semantics and on more algorithmic and complexity related areas, respectively.
Concurrent Kleene Algebra with Observations: From Hypotheses to Completeness
Authors: Kappé Tobias , Brunet Paul , Silva Alexandra , Wagemaker Jana , Zanasi Fabio
Published: April 2020

Concurrent Kleene Algebra (CKA) extends basic Kleene algebra with a parallel composition operator, which enables reasoning about concurrent programs. However, CKA fundamentally missestests, which are needed to model standard programming constructs such as conditionals and$$\mathsf {while}$$while-loops. It turns out that integrating tests in CKA is subtle, due to their interaction with parallelism. In this paper we provide a solution in the form of Concurrent Kleene Algebra with Observations (CKAO). Our main contribution is a completeness theorem for CKAO. Our result resorts on a more general study of CKA “with hypotheses”, of which CKAO turns out to be an instance: this analysis is of independent interest, as it can be applied to extensions of CKA other than CKAO.
An Axiomatic Approach to Reversible Computation
Authors: Lanese Ivan , Phillips Iain , Ulidowski Irek
Published: April 2020

Undoing computations of a concurrent system is beneficial in many situations, e.g., in reversible debugging of multi-threaded programs and in recovery from errors due to optimistic execution in parallel discrete event simulation. A number of approaches have been proposed for how to reverse formal models of concurrent computation including process calculi such as CCS, languages like Erlang, prime event structures and occurrence nets. However it has not been settled what properties a reversible system should enjoy, nor how the various properties that have been suggested, such as the parabolic lemma and the causal-consistency property, are related. We contribute to a solution to these issues by using a generic labelled transition system equipped with a relation capturing whether transitions are independent to explore the implications between these properties. In particular, we show how they are derivable from a set of axioms. Our intention is that when establishing properties of some formalism it will be easier to verify the axioms rather than proving properties such as the parabolic lemma directly. We also introduce two new notions related to causal consistent reversibility, namely causal safety and causal liveness, and show that they are derivable from our axioms.
Ambiguity, Weakness, and Regularity in Probabilistic Büchi Automata
Authors: Löding Christof , Pirogov Anton
Published: April 2020

Probabilistic Büchi automata are a natural generalization of PFA to infinite words, but have been studied in-depth only rather recently and many interesting questions are still open. PBA are known to accept, in general, a class of languages that goes beyond the regular languages. In this work we extend the known classes of restricted PBA which are still regular, strongly relying on notions concerning ambiguity in classical $$\omega $$
ω
-automata. Furthermore, we investigate the expressivity of the not yet considered but natural class of weak PBA, and we also show that the regularity problem for weak PBA is undecidable.
Local Local Reasoning: A BI-Hyperdoctrine for Full Ground Store
Authors: Polzer Miriam , Goncharov Sergey
Published: April 2020

Modelling and reasoning about dynamic memory allocation is one of the well-established strands of theoretical computer science, which is particularly well-known as a source of notorious challenges in semantics, reasoning, and proof theory. We capitalize on recent progress on categorical semantics offull ground store, in terms of afull ground store monad, to build a corresponding semantics of a higher order logic over the corresponding programs. Our main result is a construction of an(intuitionistic) BI-hyperdoctrine, which is arguably the semantic core of higher order logic over local store. Although we have made an extensive use of the existing generic tools, certain principled changes had to be made to enable the desired construction: while the original monad works over total heaps (to disable dangling pointers), our version involves partial heaps (heaplets) to enable compositional reasoning using separating conjunction. Another remarkable feature of our construction is that, in contrast to the existing generic approaches, our BI-algebra does not directly stem from an internal categorical partial commutative monoid.
Timed Negotiations
Authors: Akshay S. , Genest Blaise , Hélouët Loïc , Mital Sharvik
Published: April 2020

Negotiations were introduced in [6] as a model for concurrent systems with multiparty decisions. What is very appealing with negotiations is that it is one of the very few non-trivial concurrent models where several interesting problems, such as soundness, i.e. absence of deadlocks, can be solved in PTIME [3]. In this paper, we introduce the model of timed negotiations and consider the problem of computing the minimum and the maximum execution times of a negotiation. The latter can be solved using the algorithm of [10] computing costs in negotiations, but surprisingly minimum execution time cannot.

This paper proposes new algorithms to compute both minimum and maximum execution time, that work in much more general classes of negotiations than [10], that only considered sound and deterministic negotiations. Further, we uncover the precise complexities of these questions, ranging from PTIME to$$\varDelta _2^P$$Δ2P-complete. In particular, we show that computing the minimum execution time is more complex than computing the maximum execution time in most classes of negotiations we consider.
Learning Weighted Automata over Principal Ideal Domains
Authors: van Heerdt Gerco , Kupke Clemens , Rot Jurriaan , Silva Alexandra
Published: April 2020

In this paper, we study active learning algorithms for weighted automata over a semiring. We show that a variant of Angluin’s seminal $$\mathtt {L}^{\!\star }$$

L

⋆

algorithm works when the semiring is a principal ideal domain, but not for general semirings such as the natural numbers.
Controlling a Random Population
Authors: Colcombet Thomas , Fijalkow Nathanaël , Ohlmann Pierre
Published: April 2020

Bertrand et al. introduced a model of parameterised systems, where each agent is represented by a finite state system, and studied the following control problem: for any number of agents, does there exist a controller able to bring all agents to a target state? They showed that the problem is decidable andEXPTIME-complete in the adversarial setting, and posed as an open problem the stochastic setting, where the agent is represented by a Markov decision process. In this paper, we show that the stochastic control problem is decidable. Our solution makes significant uses of well quasi orders, of the max-flow min-cut theorem, and of the theory of regular cost functions.
Decomposing Probabilistic Lambda-Calculi
Authors: Dal Lago Ugo , Guerrieri Giulio , Heijltjes Willem
Published: April 2020

A notion of probabilistic lambda-calculus usually comes with a prescribed reduction strategy, typically call-by-name or call-by-value, as the calculus is non-confluent and these strategies yield different results. This is a break with one of the main advantages of lambda-calculus: confluence, which means results are independent from the choice of strategy. We present a probabilistic lambda-calculus where the probabilistic operator is decomposed into two syntactic constructs: a generator, which represents a probabilistic event; and a consumer, which acts on the term depending on a given event. The resulting calculus, the Probabilistic Event Lambda-Calculus, is confluent, and interprets the call-by-name and call-by-value strategies through different interpretations of the probabilistic operator into our generator and consumer constructs. We present two notions of reduction, one via fine-grained local rewrite steps, and one by generation and consumption of probabilistic events. Simple types for the calculus are essentially standard, and they convey strong normalization. We demonstrate how we can encode call-by-name and call-by-value probabilistic evaluation.
On the k-synchronizability of Systems
Authors: Di Giusto Cinzia , Laversa Laetitia , Lozes Etienne
Published: April 2020

We study k-synchronizability: a system is k-synchronizable if any of its executions, up to reordering causally independent actions, can be divided into a succession of k-bounded interaction phases. We show two results (both for mailbox and peer-to-peer automata): first, the reachability problem is decidable for k-synchronizable systems; second, the membership problem (whether a given system is k-synchronizable) is decidable as well. Our proofs fix several important issues in previous attempts to prove these two results for mailbox automata.
What’s Decidable About Program Verification Modulo Axioms?
Authors: Mathur Umang , Madhusudan P. , Viswanathan Mahesh
Published: April 2020

We consider the decidability of the verification problem of programs modulo axioms — automatically verifying whether programs satisfy their assertions, when the function and relation symbols are interpreted as arbitrary functions and relations that satisfy a set of first-order axioms. Though verification of uninterpreted programs (with no axioms) is already undecidable, a recent work introduced a subclass of coherent uninterpreted programs, and showed that they admit decidable verification [26]. We undertake a systematic study of various natural axioms for relations and functions, and study the decidability of the coherent verification problem. Axioms include relations being reflexive, symmetric, transitive, or total order relations, functions restricted to being associative, idempotent or commutative, and combinations of such axioms as well. Our comprehensive results unearth a rich landscape that shows that though several axiom classes admit decidability for coherent programs, coherence is not a panacea as several others continue to be undecidable.
Fold/Unfold Transformations for Fixpoint Logic
Authors: Kobayashi Naoki , Fedyukovich Grigory , Gupta Aarti
Published: April 2020

Fixpoint logics have recently been drawing attention as common foundations for automated program verification. We formalize fold/unfold transformations for fixpoint logic formulas and show how they can be used to enhance a recent fixpoint-logic approach to automated program verification, including automated verification of relational and temporal properties. We have implemented the transformations in a tool and confirmed its effectiveness through experiments.
Verifying OpenJDK’s LinkedList using KeY
Authors: Hiep Hans-Dieter A. , Maathuis Olaf , Bian Jinting , de Boer Frank S. , van Eekelen Marko , de Gouw Stijn
Published: April 2020

As a particular case study of the formal verification of state-of-the-art, real software, we discuss the specification and verification of a corrected version of the implementation of a linked list as provided by the Java Collection framework.
Endicheck: Dynamic Analysis for Detecting Endianness Bugs
Authors: Kápl Roman , Parízek Pavel
Published: April 2020

Computers store numbers in two mutually incompatible ways: little-endian or big-endian. They differ in the order of bytes within representation of numbers. This ordering is called endianness. When two computer systems, programs or devices communicate, they must agree on which endianness to use, in order to avoid misinterpretation of numeric data values.

We present Endicheck, a dynamic analysis tool for detecting endianness bugs, which is based on the popular Valgrind framework. It helps developers to find those code locations in their program where they forgot to swap bytes properly. Endicheck requires less source code annotations than existing tools, such as Sparse used by Linux kernel developers, and it can also detect potential bugs that would only manifest if the given program was run on computer with an opposite endianness. Our approach has been evaluated and validated on the Radeon SI Linux OpenGL driver, which is known to contain endianness-related bugs, and on several open-source programs. Results of experiments show that Endicheck can successfully identify many endianness-related bugs and provide useful diagnostic messages together with the source code locations of respective bugs.
Describing and Simulating Concurrent Quantum Systems
Authors: Bornat Richard , Boender Jaap , Kammueller Florian , Poly Guillaume , Nagarajan Rajagopal
Published: April 2020

We present a programming language for describing and analysing concurrent quantum systems. We have an interpreter for programs in the language, using a symbolic rather than a numeric calculator, and we give its performance on examples from quantum communication and cryptography.
Verifying Quantum Communication Protocols with Ground Bisimulation
Authors: Qin Xudong , Deng Yuxin , Du Wenjie
Published: April 2020

One important application of quantum process algebras is to formally verify quantum communication protocols. With a suitable notion of behavioural equivalence and a decision method, one can determine if an implementation of a protocol is consistent with its specification. Ground bisimulation is a convenient behavioural equivalence for quantum processes because of its associated coinduction proof technique. We exploit this technique to design and implement two on-the-fly algorithms for the strong and weak versions of ground bisimulation to check if two given processes in quantum CCS are equivalent. We then develop a tool that can verify interesting quantum protocols such as the BB84 quantum key distribution scheme.
Advances in Automatic Software Verification: SV-COMP 2020
Authors: Beyer Dirk
Published: April 2020

This report describes the 2020 Competition on Software Verification (SV-COMP), the 9$$^{\text {th}}$$edition of a series of comparative evaluations of fully automatic software verifiers for C and Java programs. The competition provides a snapshot of the current state of the art in the area, and has a strong focus on replicability of its results. The competition was based on 11 052 verification tasks for C programs and 416 verification tasks for Java programs. Each verification task consisted of a program and a property (reachability, memory safety, overflows, termination). SV-COMP 2020 had 28 participating verification systems from 11 countries.
2LS: Heap Analysis and Memory Safety
Authors: Malík Viktor , Schrammel Peter , Vojnar Tomáš
Published: April 2020

2LS is a framework for analysis of sequential C programs based on the CPROVER infrastructure and template-based synthesis techniques for checking both safety and termination. The paper presents the main improvements done in 2LS since 2018, which concern mainly the way 2LS handles dynamically allocated objects and structures as well as combinations of abstract domains.
JDart: Dynamic Symbolic Execution for Java Bytecode (Competition Contribution)
Authors: Mues Malte , Howar Falk
Published: April 2020

JDart performs dynamic symbolic execution of Java programs: it executes programs with concrete inputs while recording symbolic constraints on executed program paths. A constraint solver is then used for generating new concrete values from recorded constraints that drive execution along previously unexplored paths. JDart is built on top of the Java PathFinder software model checker and uses the JConstraints library for the integration of constraint solvers.
Map2Check: Using Symbolic Execution and Fuzzing
Authors: Rocha Herbert , Menezes Rafael , Cordeiro Lucas C. , Barreto Raimundo
Published: April 2020

Map2Check is a software verification tool that combines fuzzing, symbolic execution, and inductive invariants. It automatically checks safety properties in C programs by adopting source code instrumentation to monitor data (e.g., memory pointers) from the program’s executions using LLVM compiler infrastructure. For SV-COMP 2020, we extended Map2Check to exploit an iterative deepening approach using LibFuzzer and Klee to check for safety properties. We also use Crab-LLVM to infer program invariants based on reachability analysis. Experimental results show that Map2Check can handle a wide variety of safety properties in several intricate verification tasks from SV-COMP 2020.
Deciding the Bisimilarity of Context-Free Session Types
Authors: Almeida Bernardo , Mordido Andreia , Vasconcelos Vasco T.
Published: April 2020

We present an algorithm to decide the equivalence of context-free session types, practical to the point of being incorporated in a compiler. We prove its soundness and completeness. We further evaluate its behaviour in practice. In the process, we introduce an algorithm to decide the bisimilarity of simple grammars.
PredatorHP Revamped (Not Only) for Interval-Sized Memory Regions and Memory Reallocation (Competition Contribution)
Authors: Peringer Petr , Šoková Veronika , Vojnar Tomáš
Published: April 2020

This paper concentrates on improvements of the PredatorHP shape analyzer in the past two years, including, e.g., improved handling of interval-sized memory regions or new support of memory reallocation. The paper characterizes PredatorHP’s participation in SV-COMP 2020, pointing out its strengths and weakness and the way they were influenced by the latest changes in the tool.
Symbiotic 7: Integration of Predator and More
Authors: Chalupa Marek , Jašek Tomáš , Tomovič Lukáš , Hruška Martin , Šoková Veronika , Ayaziová Paulína , Strejček Jan , Vojnar Tomáš
Published: April 2020

Symbiotic  7 brings improvements in all parts of the tool. In particular, we integrated the advanced shape analysis implemented in Predator to our instrumentation process for memory safety checking. Further, we extended our slicer to correctly handle non-terminating programs. This new slicing is applied in termination analysis, where we also added instrumentation for detection of simple cycles in the program state space. The witness generation process changed as well.
Ultimate Taipan with Symbolic Interpretation and Fluid Abstractions
Authors: Dietsch Daniel , Heizmann Matthias , Nutz Alexander , Schätzle Claus , Schüssele Frank
Published: April 2020

Ultimate Taipan is a software model checker that combines trace abstraction with abstract interpretation on path programs. In this year’s version, we replaced our abstract interpretation engine and now use a combination of multiple abstraction functions, fixpoint computation, algebraic program analysis, and SMT solving. Our new approach will allow us to integrate new techniques more easily.
Highly Automated Formal Proofs over Memory Usage of Assembly Code
Authors: Verbeek Freek , Bockenek Joshua A. , Ravindran Binoy
Published: April 2020

We present a methodology for generating a characterization of the memory used by an assembly program, as well as a formal proof that the assembly is bounded to the generated memory regions. A formal proof of memory usage is required for compositional reasoning over assembly programs. Moreover, it can be used to prove low-level security properties, such as integrity of the return address of a function. Our verification method is based on interactive theorem proving, but provides automation by generating pre- and postconditions, invariants, control-flow, and assumptions on memory layout. As a case study, three binaries of the Xen hypervisor are disassembled. These binaries are the result of a complex build-chain compiling production code, and contain various complex and nested loops, large and compound data structures, and functions with over 100 basic blocks. The methodology has been successfully applied to 251 functions, covering 12,252 assembly instructions.
GASOL: Gas Analysis and Optimization for Ethereum Smart Contracts
Authors: Albert Elvira , Correas Jesús , Gordillo Pablo , Román-Díez Guillermo , Rubio Albert
Published: April 2020

We present the main concepts, components, and usage of Gasol, a Gas AnalysiS and Optimization tooL for Ethereum smart contracts. Gasol offers a wide variety of cost models that allow inferring the gas consumption associated to selected types of EVM instructions and/or inferring the number of times that such types of bytecode instructions are executed. Among others, we have cost models to measure only storage opcodes, to measure a selected family of gas-consumption opcodes following the Ethereum’s classification, to estimate the cost of a selected program line, etc. After choosing the desired cost model and the function of interest, Gasol returns to the user an upper bound of the cost for this function. As the gas consumption is often dominated by the instructions that access the storage, Gasol uses the gas analysis to detect under-optimized storage patterns, and includes an (optional) automatic optimization of the selected function. Our tool can be used within an Eclipse plugin for which displays the gas and instructions bounds and, when applicable, the gas-optimized function.
A case report of cholinesterase inhibitor poisoning: cholinesterase activities and analytical methods for diagnosis and clinical decision making
Authors: Amend N. , Langgartner J. , Siegert M. , Kranawetvogl T. , Koller M. , John H. , Pflügler C. , Mögele-Schmid C. , Worek F. , Thiermann H. , Wille T.
Published: April 2020

Suicidal ingestion of organophosphorus (OP) or carbamate (CM) compounds challenges health care systems worldwide, particularly in Southeast Asia. The diagnosis and treatment of OP or CM poisoning is traditionally based on the clinical appearance of the typical cholinergic toxidrome, e.g. miosis, salivation and bradycardia. Yet, clinical signs might be inconclusive or even misleading. A current case report highlights the importance of enzymatic assays to provide rapid information and support clinicians in diagnosis and rational clinical decision making. Furthermore, the differentiation between OP and CM poisoning seems important, as an oxime therapy will most probably not provide benefit in CM poisoning, but—as every pharmaceutical product—it might result in adverse effects. The early identification of the causing agent and the amount taken up in the body are helpful in planning of the therapeutic regimen including experimental strategies, e.g. the use of human blood products to facilitate scavenging of the toxic agent. Furthermore, the analysis of biotransformation products and antidote levels provides additional insights into the pathophysiology of OP or CM poisoning. In conclusion, cholinesterase activities and modern analytical methods help to provide a more effective treatment and a thorough understanding of individual cases of OP or CM poisoning.
Perihelion Librations in the Secular Three-Body Problem
Authors: Pinzari Gabriella
Published: April 2020

A normal form theory for non-quasiperiodic systems is combined with the special properties of the partially averaged Newtonian potential pointed out in Pinzari (Celest Mech Dyn Astron 131(5):22, 2019) to prove, in the averaged, planar three-body problem, the existence of a plenty of motions where, periodically, the perihelion of the inner body affords librations about one equilibrium position and its ellipse squeezes to a segment before reversing its direction and again decreasing its eccentricity (perihelion librations).
Analyse des Stellenwertes von „eLearning“ in der Augenheilkunde und Evaluierung einer „eLearning-App“
Authors: Grabowski E. , Alten F. , Termühlen J. , Heiduschka P. , Brücher V. , Eter N. , Clemens C. R.
Published: April 2020

Hintergrund

Ziel der Studie war die Analyse des Stellenwertes von „eLearning“ im Lern- und Fortbildungsverhalten von Augenärzten in Deutschland sowie die Bewertung der Akzeptanz einer neuen „eLearning“-Anwendersoftware (App).

Material und Methoden

Ophthalmologische Weiterbildungsassistenten und Fachärzte wurden im Rahmen von Fortbildungsveranstaltungen mittels eines Fragebogens nach ihren Fortbildungsaktivitäten befragt. Des Weiteren erfolgte nach Vorstellung und Anwendung einer „eLearning-App“ eine strukturierte Bewertung.

Ergebnisse

Es nahmen 149 Augenärzte an der Befragung teil. Während der überwiegende Teil der Kollegen (74,3 %) analoge Fachzeitschriften wöchentlich oder monatlich zur Weiterbildung nutzt, verwenden 45,9 % der Augenärzte digitale Printmedien (Bücher, Zeitschriften, Artikel) sowie 46,5 % Fachbücher in gedruckter Form. Lediglich 35 % der Befragten bilden sich über Online-Fortbildungsplattformen, z. B. digitale Kurse (CME-Kurse) oder Portale zum Abrufen aufgezeichneter Vorträge, fort. Die Nutzung der angebotenen „eLearning-App“ ging insgesamt mit einer positiven Akzeptanz einher; 91,7 % der befragten Kollegen würden diese Form der interaktiven Lernvermittlung weiterempfehlen.

Diskussion

Trotz fortschreitender Digitalisierung in allen Lebensbereichen nimmt „eLearning“ als Lernmedium in der ophthalmologischen Fort- und Weiterbildung weiterhin einen geringen Stellenwert ein. Interessanterweise ergab die Bewertung der App-Nutzer eine hohe Benutzerakzeptanz, unabhängig von Alter oder Arbeitsbereich.
Fine wine or sour grapes? A systematic review and meta-analysis of the impact of red wine polyphenols on vascular health
Authors: Weaver Samuel R. , Rendeiro Catarina , McGettrick Helen M. , Philp Andrew , Lucas Samuel J. E.
Published: April 2020

Purpose

Red wine polyphenols (RWP) are plant-based molecules that have been extensively studied in relation to their protective effects on vascular health in both animals and humans. The aim of this review was to quantify and compare the efficacy of RWP and pure resveratrol on outcomes measures of vascular health and function in both animals and humans.

Methods

Comprehensive database searches were carried out through PubMed, Web of Science and OVID for randomised, placebo-controlled studies in both animals and humans. Meta-analyses were carried out on acute and chronic studies of RWP in humans, alongside sub-group analysis where possible. Risk-of-bias assessment was carried out for all included studies based on randomisation, allocation, blinding, outcome data reporting, and other biases.

Results

48 animal and 37 human studies were included in data extraction following screening. Significant improvements in measures of blood pressure and vascular function following RWP were seen in 84% and 100% of animal studies, respectively. Human studies indicated significant improvements in systolic blood pressure overall (− 2.6 mmHg, 95% CI: [− 4.8, − 0.4]), with a greater improvement in pure-resveratrol studies alone (− 3.7 mmHg, 95% CI: [− 7.3, − 0.0]). No significant effects of RWP were seen in diastolic blood pressure or flow-mediated dilation (FMD) of the brachial artery.

Conclusion

RWP have the potential to improve vascular health in at risk human populations, particularly in regard to lowering systolic blood pressure; however, such benefits are not as prevalent as those observed in animal models.