bluuebunny/crossref_metadata_2025 huggingface dataset:
A modular cost analysis for probabilistic programs
Authors: Avanzini Martin , Moser Georg , Schaper Michael
Published: November 2020

We present a novel methodology for the automated resource analysis of non-deterministic, probabilistic imperative programs, which gives rise to a
modular approach
. Program fragments are analysed in full independence. Moreover, the established results allow us to incorporate sampling from
dynamic distributions
, making our analysis applicable to a wider class of examples, for example the
Coupon Collector’s problem
.

We have implemented our contributions in the tool , exploiting a constraint-solver over iterative refineable cost functions facilitated by off-the-shelf SMT solvers. We provide ample experimental evidence of the prototype’s algorithmic power. Our experiments show that our tool runs typically at least one
order of magnitude faster
than comparable tools. On more involved examples, it may even be the case that execution times of seconds become milliseconds. At the same time we retain the precision of existing tools.

The extensions in applicability and the greater efficiency of our prototype, yield scalability of sorts. This effects into a wider class of examples, whose expected cost analysis can be thus be performed fully automatically.
Sound garbage collection for C using pointer provenance
Authors: Banerjee Subarno , Devecsery David , Chen Peter M. , Narayanasamy Satish
Published: November 2020

Garbage collection (GC) support for unmanaged languages can reduce programming burden in reasoning about liveness of dynamic objects. It also avoids temporal memory safety violations and memory leaks.
Sound
GC for weakly-typed languages such as C/C++, however, remains an unsolved problem. Current value-based GC solutions examine values of memory locations to discover the pointers, and the objects they point to. The approach is inherently unsound in the presence of arbitrary type casts and pointer manipulations, which are legal in C/C++. Such language features are regularly used, especially in low-level systems code.

In this paper, we propose Dynamic Pointer Provenance Tracking to realize sound GC. We observe that pointers cannot be created out-of-thin-air, and they must have provenance to at least one valid allocation. Therefore, by tracking pointer provenance from the source (e.g., malloc) through both explicit data-flow and implicit control-flow, our GC has sound and precise information to compute the set of all reachable objects at any program state. We discuss several static analysis optimizations, that can be employed during compilation aided with profiling, to significantly reduce the overhead of dynamic provenance tracking from nearly 8× to 16% for well-behaved programs that adhere to the C standards. Pointer provenance based sound GC invocation is also 13% faster and reclaims 6% more memory on average, compared to an unsound value-based GC.
Dataflow-based pruning for speeding up superoptimization
Authors: Mukherjee Manasij , Kant Pranav , Liu Zhengyang , Regehr John
Published: November 2020

Superoptimization is a compilation strategy that uses search to improve code quality, rather than relying on a canned sequence of transformations, as traditional optimizing compilers do. This search can be seen as a program synthesis problem: from unoptimized code serving as a specification, the synthesis procedure attempts to create a more efficient implementation. An important family of synthesis algorithms works by enumerating candidates and then successively checking if each refines the specification, using an SMT solver. The contribution of this paper is a pruning technique which reduces the enumerative search space using fast dataflow-based techniques to discard synthesis candidates that contain symbolic constants and uninstantiated instructions. We demonstrate the effectiveness of this technique by improving the runtime of an enumerative synthesis procedure in the Souper superoptimizer for the LLVM intermediate representation. The techniques presented in this paper eliminate 65% of the solver calls made by Souper, making it 2.32x faster (14.54 hours vs 33.76 hours baseline, on a large multicore) at solving all 269,113 synthesis problems that Souper encounters when optimizing the C and C++ programs from SPEC CPU 2017.
Learning graph-based heuristics for pointer analysis without handcrafting application-specific features
Authors: Jeon Minseok , Lee Myungho , Oh Hakjoo
Published: November 2020

We present Graphick, a new technique for automatically learning graph-based heuristics for pointer analysis. Striking a balance between precision and scalability of pointer analysis requires designing good analysis heuristics. For example, because applying context sensitivity to all methods in a real-world program is impractical, pointer analysis typically uses a heuristic to employ context sensitivity only when it is necessary. Past research has shown that exploiting the program's graph structure is a promising way of developing cost-effective analysis heuristics, promoting the recent trend of ``graph-based heuristics'' that work on the graph representations of programs obtained from a pre-analysis. Although promising, manually developing such heuristics remains challenging, requiring a great deal of expertise and laborious effort. In this paper, we aim to reduce this burden by learning graph-based heuristics automatically, in particular without hand-crafted application-specific features. To do so, we present a feature language to describe graph structures and an algorithm for learning analysis heuristics within the language. We implemented Graphick on top of Doop and used it to learn graph-based heuristics for object sensitivity and heap abstraction. The evaluation results show that our approach is general and can generate high-quality heuristics. For both instances, the learned heuristics are as competitive as the existing state-of-the-art heuristics designed manually by analysis experts.
Shiftry: RNN inference in 2KB of RAM
Authors: Kumar Aayan , Seshadri Vivek , Sharma Rahul
Published: November 2020

Traditionally, IoT devices send collected sensor data to an intelligent cloud where machine learning (ML) inference happens. However, this course is rapidly changing and there is a recent trend to run ML on the edge IoT devices themselves. An intelligent edge is attractive because it saves network round trip (efficiency) and keeps user data at the source (privacy). However, the IoT devices are much more resource constrained than the cloud, which makes running ML on them challenging. Specifically, consider Arduino Uno, a commonly used board, that has 2KB of RAM and 32KB of read-only Flash memory. Although recent breakthroughs in ML have created novel recurrent neural network (RNN) models that provide good accuracy with KB-sized models, deploying them on tiny devices with such hard memory requirements has remained elusive.

We provide, Shiftry, an automatic compiler from high-level floating-point ML models to fixed-point C-programs with 8-bit and 16-bit integers, which have significantly lower memory requirements. For this conversion, Shiftry uses a data-driven float-to-fixed procedure and a RAM management mechanism. These techniques enable us to provide first empirical evaluation of RNNs running on tiny edge devices. On simpler ML models that prior work could handle, Shiftry-generated code has lower latency and higher accuracy.
StreamQL: a query language for processing streaming time series
Authors: Kong Lingkun , Mamouras Konstantinos
Published: November 2020

Real-time data analysis applications increasingly rely on complex streaming computations over time-series data. We propose StreamQL, a language that facilitates the high-level specification of complex analyses over streaming time series. StreamQL is designed as an algebra of stream transformations and provides a collection of combinators for composing them. It integrates three language-based approaches for data stream processing: relational queries, dataflow composition, and temporal formalisms. The relational constructs are useful for specifying simple transformations, aggregations, and the partitioning of data into key-based groups or windows. The dataflow abstractions enable the modular description of a computation as a pipeline of stages or, more generally, as a directed graph of independent tasks. Finally, temporal constructs can be used to specify complex temporal patterns and time-varying computations. These constructs can be composed freely to describe complex streaming computations. We provide a formal denotational semantics for StreamQL using a class of monotone functions over streams. We have implemented StreamQL as a lightweight Java library, which we use to experimentally evaluate our approach. The experiments show that the throughput of our implementation is competitive compared to state-of-the-art streaming engines such as RxJava and Reactor.
Incremental predicate analysis for regression verification
Authors: Yu Qianshan , He Fei , Wang Bow-Yaw
Published: November 2020

Software products are evolving during their life cycles. Ideally, every revision need be formally verified to ensure software quality. Yet repeated formal verification requires significant computing resources. Verifying each and every revision can be very challenging. It is desirable to ameliorate regression verification for practical purposes. In this paper, we regard predicate analysis as a process of assertion annotation. Assertion annotations can be used as a certificate for the verification results. It is thus a waste of resources to throw them away after each verification. We propose to reuse the previously-yielded assertion annotation in regression verification. A light-weight impact-analysis technique is proposed to analyze the reusability of assertions. A novel assertion strengthening technique is furthermore developed to improve reusability of annotation. With these techniques, we present an incremental predicate analysis technique for regression verification. Correctness of our incremental technique is formally proved. We performed comprehensive experiments on revisions of Linux kernel device drivers. Our technique outperforms the state-of-the-art program verification tool CPAchecker by getting 2.8x speedup in total time and solving additional 393 tasks.
Inter-theory dependency analysis for SMT string solvers
Authors: Trinh Minh-Thai , Chu Duc-Hiep , Jaffar Joxan
Published: November 2020

Solvers in the framework of Satisfiability Modulo Theories (SMT) have been widely successful in practice. Recently there has been an increasing interest in solvers for string constraints to address security issues in web programming, for example. To be practically useful, the solvers need to support an expressive constraint language over unbounded strings, and in particular, over string lengths. Satisfiability checking for these formulas, especially in the SMT context, is very hard; it is generally undecidable for a rich fragment. In this paper, we propose a form of dependency analysis for a rich fragment of string constraints including high-level operations such as length, contains to deal with their inter-theory interaction so as to solve them more efficiently. We implement our dependency analysis in the string theory of the Z3 solver to obtain a new one, called S3N. Finally, we demonstrate the superior performance of S3N over state-of-the-art string solvers such as Z3str3, CVC4, S3P, and Z3 on several large industrial-strength benchmarks.
Pomsets with preconditions: a simple model of relaxed memory
Authors: Jagadeesan Radha , Jeffrey Alan , Riely James
Published: November 2020

Relaxed memory models must simultaneously achieve efficient implementability and thread-compositional reasoning. Is that why they have become so complicated? We argue that the answer is no: It is possible to achieve these goals by combining an idea from the 60s (preconditions) with an idea from the 80s (pomsets), at least for X64 and ARMv8. We show that the resulting model (1) supports compositional reasoning for temporal safety properties, (2) supports all expected sequential compiler optimizations, (3) satisfies the DRF-SC criterion, and (4) compiles to X64 and ARMv8 microprocessors without requiring extra fences on relaxed accesses.
CompCertELF: verified separate compilation of C programs into ELF object files
Authors: Wang Yuting , Xu Xiangzhe , Wilke Pierre , Shao Zhong
Published: November 2020

We present CompCertELF, the first extension to CompCert that supports verified compilation from C programs all the way to a standard binary file format, i.e., the ELF object format. Previous work on Stack-Aware CompCert provides a verified compilation chain from C programs to assembly programs with a realistic machine memory model. We build CompCertELF by modifying and extending this compilation chain with a verified assembler which further transforms assembly programs into ELF object files.

CompCert supports large-scale verification via verified separate compilation: C modules can be written and compiled separately, and then linked together to get a target program that refines the semantics of the program linked from the source modules. However, verified separate compilation in CompCert only works for compilation to assembly programs, not to object files. For the latter, the main difficulty is to bridge the two different views of linking: one for CompCert's programs that allows arbitrary shuffling of global definitions by linking and the other for object files that treats blocks of encoded definitions as indivisible units.

We propose a lightweight approach that solves the above problem without any modification to CompCert's framework for verified separate compilation: by introducing a notion of syntactical equivalence between programs and proving the commutativity between syntactical equivalence and the two different kinds of linking, we are able to transit from the more abstract linking operation in CompCert to the more concrete one for ELF object files. By applying this approach to CompCertELF, we obtain the first compiler that supports verified separate compilation of C programs into ELF object files.
A large-scale longitudinal study of flaky tests
Authors: Lam Wing , Winter Stefan , Wei Anjiang , Xie Tao , Marinov Darko , Bell Jonathan
Published: November 2020

Flaky tests are tests that can non-deterministically pass or fail for the same code version. These tests undermine regression testing efficiency, because developers cannot easily identify whether a test fails due to their recent changes or due to flakiness. Ideally, one would detect flaky tests right when flakiness is introduced, so that developers can then immediately remove the flakiness. Some software organizations, e.g., Mozilla and Netflix, run some tools—detectors—to detect flaky tests as soon as possible. However, detecting flaky tests is costly due to their inherent non-determinism, so even state-of-the-art detectors are often impractical to be used on all tests for each project change. To combat the high cost of applying detectors, these organizations typically run a detector solely on newly added or directly modified tests, i.e., not on unmodified tests or when other changes occur (including changes to the test suite, the code under test, and library dependencies). However, it is unclear how many flaky tests can be detected or missed by applying detectors in only these limited circumstances.

To better understand this problem, we conduct a large-scale longitudinal study of flaky tests to determine when flaky tests become flaky and what changes cause them to become flaky. We apply two state-of-theart detectors to 55 Java projects, identifying a total of 245 flaky tests that can be compiled and run in the code version where each test was added. We find that 75% of flaky tests (184 out of 245) are flaky when added, indicating substantial potential value for developers to run detectors specifically on newly added tests. However, running detectors solely on newly added tests would still miss detecting 25% of flaky tests. The percentage of flaky tests that can be detected does increase to 85% when detectors are run on newly added or directly modified tests. The remaining 15% of flaky tests become flaky due to other changes and can be detected only when detectors are always applied to all tests. Our study is the first to empirically evaluate when tests become flaky and to recommend guidelines for applying detectors in the future.
Digging for fold: synthesis-aided API discovery for Haskell
Authors: James Michael B. , Guo Zheng , Wang Ziteng , Doshi Shivani , Peleg Hila , Jhala Ranjit , Polikarpova Nadia
Published: November 2020

We present Hoogle+, a web-based API discovery tool for Haskell. A Hoogle+ user can specify a programming task using either a type, a set of input-output tests, or both. Given a specification, the tool returns a list of matching programs composed from functions in popular Haskell libraries, and annotated with automatically-generated examples of their behavior. These features of Hoogle+ are powered by three novel techniques. First, to enable efficient type-directed synthesis from tests only, we develop an algorithm that
infers likely type specifications from tests
. Second, to return high-quality programs even with ambiguous specifications, we develop a technique that automatically
eliminates meaningless and repetitive synthesis results
. Finally, we show how to extend this elimination technique to automatically
generate informative inputs
that can be used to demonstrate program behavior to the user. To evaluate the effectiveness of Hoogle+ compared with traditional API search techniques, we perform a user study with 30 participants of varying Haskell proficiency. The study shows that programmers equipped with Hoogle+ generally solve tasks faster and were able to solve 50% more tasks overall.
Resolution as intersection subtyping via Modus Ponens
Authors: Marntirosian Koar , Schrijvers Tom , Oliveira Bruno C. d. S. , Karachalias Georgios
Published: November 2020

Resolution and subtyping are two common mechanisms in programming languages. Resolution is used by features such as type classes or Scala-style implicits to synthesize values automatically from contextual type information. Subtyping is commonly used to automatically convert the type of a value into another compatible type. So far the two mechanisms have been considered independently of each other. This paper shows that, with a small extension, subtyping with intersection types can subsume resolution. This has three main consequences. Firstly, resolution does not need to be implemented as a separate mechanism. Secondly, the interaction between resolution and subtyping becomes apparent. Finally, the integration of resolution into subtyping enables first-class (implicit) environments. The extension that recovers the power of resolution via subtyping is the modus ponens rule of propositional logic. While it is easily added to declarative subtyping, significant care needs to be taken to retain desirable properties, such as transitivity and decidability of algorithmic subtyping, and coherence. To materialize these ideas we develop λiMP, a calculus that extends a iprevious calculus with disjoint intersection types, and develop its metatheory in the Coq theorem prover.
World age in Julia: optimizing method dispatch in the presence of eval
Authors: Belyakova Julia , Chung Benjamin , Gelinas Jack , Nash Jameson , Tate Ross , Vitek Jan
Published: November 2020

Dynamic programming languages face semantic and performance challenges in the presence of features, such as eval, that can inject new code into a running program. The Julia programming language introduces the novel concept of world age to insulate optimized code from one of the most disruptive side-effects of eval: changes to the definition of an existing function. This paper provides the first formal semantics of world age in a core calculus named juliette, and shows how world age enables compiler optimizations, such as inlining, in the presence of eval. While Julia also provides programmers with the means to bypass world age, we found that this mechanism is not used extensively: a static analysis of over 4,000 registered Julia packages shows that only 4-9% of packages bypass world age. This suggests that Julia's semantics aligns with programmer expectations.
ιDOT: a DOT calculus with object initialization
Authors: Kabir Ifaz , Li Yufeng , Lhoták Ondřej
Published: November 2020

The Dependent Object Types (DOT) calculus serves as a foundation of the Scala programming language, with a machine-verified soundness proof. However, Scala's type system has been shown to be unsound due to null references, which are used as default values of fields of objects before they have been initialized. This paper proposes ιDOT, an extension of DOT for ensuring safe initialization of objects. DOT was previously extended to κDOT with the addition of mutable fields and constructors. To κDOT, ιDOT adds an initialization effect system that statically prevents the possibility of reading a null reference from an uninitialized object. To design ιDOT, we have reformulated the Freedom Before Commitment object initialization scheme in terms of disjoint subheaps to make it easier to formalize in an effect system and prove sound. Soundness of ιDOT depends on the interplay of three systems of rules: a type system close to that of DOT, an effect system to ensure definite assignment of fields in each constructor, and an initialization system that tracks the initialization status of objects in a stack of subheaps. We have proven the overall system sound and verified the soundness proof using the Coq proof assistant.
Verifying replicated data types with typeclass refinements in Liquid Haskell
Authors: Liu Yiyun , Parker James , Redmond Patrick , Kuper Lindsey , Hicks Michael , Vazou Niki
Published: November 2020

This paper presents an extension to Liquid Haskell that facilitates stating and semi-automatically proving properties of typeclasses. Liquid Haskell augments Haskell with
refinement types
—our work allows such types to be attached to typeclass method declarations, and ensures that instance implementations respect these types. The engineering of this extension is a modular interaction between GHC, the Glasgow Haskell Compiler, and Liquid Haskell’s core proof infrastructure. The design sheds light on the interplay between modular proofs and typeclass resolution, which in Haskell is coherent by default (meaning that resolution always selects the same implementation for a particular instantiating type), but in other dependently typed languages is not.

We demonstrate the utility of our extension by using Liquid Haskell to modularly verify that 34 instances satisfy the laws of five standard typeclasses.

More substantially, we implement a framework for programming distributed applications based on
replicated data types
(RDTs). We define a typeclass whose Liquid Haskell type captures the mathematical properties RDTs should satisfy; prove in Liquid Haskell that these properties are sufficient to ensure that replicas’ states converge despite out-of-order update delivery; implement (and prove correct) several instances of our RDT typeclass; and use them to build two realistic applications, a multi-user calendar event planner and a collaborative text editor.
Unifying execution of imperative generators and declarative specifications
Authors: Nie Pengyu , Parovic Marinela , Zang Zhiqiang , Khurshid Sarfraz , Milicevic Aleksandar , Gligoric Milos
Published: November 2020

We present Deuterium---a framework for implementing Java methods as executable contracts. Deuterium introduces a novel, type-safe way to write method contracts entirely in Java, as a combination of imperative generators and declarative specifications (written in a first-order relational logic with transitive closure). Existing approaches are typically based on encoding both the specification and the program heap into a constraint language, and then using an off-the-shelf constraint solver---without any additional guidance---to search for a new program heap that satisfies the specification. Deuterium takes advantage of user-provided generators to prune the search space and reduce incurred overhead of constraint solving. Deuterium supports two ways of solving declarative constraints: SAT-based and search-based with in-memory state exploration. We evaluate our approach on a suite of data structures, established as a standard benchmark by prior work. Furthermore, we use random and sequence-based test generation to create a new benchmark designed to mimic realistic execution scenarios. Our results show that generators improve the performance of executable contracts and that in-memory state exploration is the algorithm of choice when heap sizes are small.
Regex matching with counting-set automata
Authors: Turoňová Lenka , Holík Lukáš , Lengál Ondřej , Saarikivi Olli , Veanes Margus , Vojnar Tomáš
Published: November 2020

We propose a solution to the problem of efficient matching regular expressions (regexes) with bounded repetition, such as (ab){1,100}, using deterministic automata. For this, we introduce novel
counting-set automata (CsAs)
, automata with registers that can hold sets of bounded integers and can be manipulated by a limited portfolio of constant-time operations. We present an algorithm that compiles a large sub-class of regexes to deterministic CsAs. This includes (1) a novel Antimirov-style translation of regexes with counting to
counting automata (CAs)
, nondeterministic automata with bounded counters, and (2) our main technical contribution, a determinization of CAs that outputs CsAs. The main advantage of this workflow is that
the size of the produced CsAs does not depend on the repetition bounds used in the regex
(while the size of the DFA is exponential to them). Our experimental results confirm that deterministic CsAs produced from practical regexes with repetition are indeed vastly smaller than the corresponding DFAs. More importantly, our prototype matcher based on CsA simulation handles practical regexes with repetition regardless of sizes of counter bounds. It easily copes with regexes with repetition where state-of-the-art matchers struggle.
Contextual dispatch for function specialization
Authors: Flückiger Olivier , Chari Guido , Yee Ming-Ho , Ječmen Jan , Hain Jakob , Vitek Jan
Published: November 2020

In order to generate efficient code, dynamic language compilers often need information, such as dynamic types, not readily available in the program source. Leveraging a mixture of static and dynamic information, these compilers speculate on the missing information. Within one compilation unit, they specialize the generated code to the previously observed behaviors, betting that past is prologue. When speculation fails, the execution must jump back to unoptimized code. In this paper, we propose an approach to further the specialization, by disentangling classes of behaviors into separate optimization units. With contextual dispatch, functions are versioned and each version is compiled under different assumptions. When a function is invoked, the implementation dispatches to a version optimized under assumptions matching the dynamic context of the call. As a proof-of-concept, we describe a compiler for the R language which uses this approach. Our implementation is, on average, 1.7× faster than the GNU R reference implementation. We evaluate contextual dispatch on a set of benchmarks and measure additional speedup, on top of traditional speculation with deoptimization techniques. In this setting contextual dispatch improves the performance of 18 out of 46 programs in our benchmark suite.
Counterexample-guided correlation algorithm for translation validation
Authors: Gupta Shubhani , Rose Abhishek , Bansal Sorav
Published: November 2020

Automatic translation validation across the unoptimized intermediate representation (IR) of the original source code and the optimized executable assembly code is a desirable capability, and has the potential to compete with existing approaches to verified compilation such as CompCert. A difficult subproblem is the automatic identification of the correlations across the transitions between the two programs' respective locations. We present a counterexample-guided algorithm to identify these correlations in a robust and scalable manner. Our algorithm has both theoretical and empirical advantages over prior work in this problem space.
Foundations of empirical memory consistency testing
Authors: Kirkham Jake , Sorensen Tyler , Tureci Esin , Martonosi Margaret
Published: November 2020

Modern memory consistency models are complex, and it is difficult to reason about the relaxed behaviors that current systems allow. Programming languages, such as C and OpenCL, offer a memory model interface that developers can use to safely write concurrent applications. This abstraction provides functional portability across any platform that implements the interface, regardless of differences in the underlying systems. This powerful abstraction hinges on the ability of the system to correctly implement the interface. Many techniques for memory consistency model validation use empirical testing, which has been effective at uncovering undocumented behaviors and even finding bugs in trusted compilation schemes. Memory model testing consists of small concurrent unit tests called “litmus tests”. In these tests, certain observations,
including potential bugs
, are exceedingly rare, as they may only be triggered by precise interleaving of system steps in a complex processor, which is probabilistic in nature. Thus, each test must be run many times in order to provide a high level of confidence in its coverage.

In this work, we rigorously investigate empirical memory model testing. In particular, we propose methodologies for navigating complex stressing routines and analyzing large numbers of testing observations. Using these insights, we can more efficiently tune stressing parameters, which can lead to higher confidence results at a faster rate. We emphasize the need for such approaches by performing a meta-study of prior work, which reveals results with low reproducibility and inefficient use of testing time.

Our investigation is presented alongside empirical data. We believe that OpenCL targeting GPUs is a pragmatic choice in this domain as there exists a variety of different platforms to test, from large HPC servers to power-efficient edge devices. The tests presented in the work span 3 GPUs from 3 different vendors. We show that our methodologies are applicable across the GPUs, despite significant variances in the results. Concretely, our results show: lossless speedups of more than 5× in tuning using data peeking; a definition of portable stressing parameters which loses only 12% efficiency when generalized across our domain; a priority order of litmus tests for tuning. We stress test a conformance test suite for the OpenCL 2.0 memory model and discover a bug in Intel’s compiler. Our methods are evaluated on the other two GPUs using mutation testing. We end with recommendations for official memory model conformance tests.
Just-in-time learning for bottom-up enumerative synthesis
Authors: Barke Shraddha , Peleg Hila , Polikarpova Nadia
Published: November 2020

A key challenge in program synthesis is the astronomical size of the search space the synthesizer has to explore. In response to this challenge, recent work proposed to guide synthesis using learned probabilistic models. Obtaining such a model, however, might be infeasible for a problem domain where no high-quality training data is available. In this work we introduce an alternative approach to guided program synthesis: instead of training a model ahead of time we show how to bootstrap one just in time, during synthesis, by learning from partial solutions encountered along the way. To make the best use of the model, we also propose a new program enumeration algorithm we dub guided bottom-up search, which extends the efficient bottom-up search with guidance from probabilistic models.

We implement this approach in a tool called Probe, which targets problems in the popular syntax-guided synthesis (SyGuS) format. We evaluate Probe on benchmarks from the literature and show that it achieves significant performance gains both over unguided bottom-up search and over a state-of-the-art probability-guided synthesizer, which had been trained on a corpus of existing solutions. Moreover, we show that these performance gains do not come at the cost of solution quality: programs generated by Probe are only slightly more verbose than the shortest solutions and perform no unnecessary case-splitting.
Gradual verification of recursive heap data structures
Authors: Wise Jenna , Bader Johannes , Wong Cameron , Aldrich Jonathan , Tanter Éric , Sunshine Joshua
Published: November 2020

Current static verification techniques do not provide good support for incrementality, making it difficult for developers to focus on specifying and verifying the properties and components that are most important. Dynamic verification approaches support incrementality, but cannot provide static guarantees. To bridge this gap, prior work proposed gradual verification, which supports incrementality by allowing every assertion to be complete, partial, or omitted, and provides sound verification that smoothly scales from dynamic to static checking. The prior approach to gradual verification, however, was limited to programs without recursive data structures. This paper extends gradual verification to programs that manipulate recursive, mutable data structures on the heap. We address several technical challenges, such as semantically connecting iso- and equi-recursive interpretations of abstract predicates, and supporting gradual verification of heap ownership. This work thus lays the foundation for future tools that work on realistic programs and support verification within an engineering process in which cost-benefit trade-offs can be made.
TacTok: semantics-aware proof synthesis
Authors: First Emily , Brun Yuriy , Guha Arjun
Published: November 2020

Formally verifying software correctness is a highly manual process. However, because verification proof scripts often share structure, it is possible to learn from existing proof scripts to fully automate some formal verification. The goal of this paper is to improve proof script synthesis and enable fully automating more verification. Interactive theorem provers, such as the Coq proof assistant, allow programmers to write partial proof scripts, observe the semantics of the proof state thus far, and then attempt more progress. Knowing the proof state semantics is a significant aid. Recent research has shown that the proof state can help predict the next step. In this paper, we present TacTok, the first technique that attempts to fully automate proof script synthesis by modeling proof scripts using both the partial proof script written thus far and the semantics of the proof state. Thus, TacTok more completely models the information the programmer has access to when writing proof scripts manually. We evaluate TacTok on a benchmark of 26 software projects in Coq, consisting of over 10 thousand theorems. We compare our approach to five tools. Two prior techniques, CoqHammer, the state-of-the-art proof synthesis technique, and ASTactic, a proof script synthesis technique that models proof state. And three new proof script synthesis technique we create ourselves, SeqOnly, which models only the partial proof script and the initial theorem being proven, and WeightedRandom and WeightedGreedy, which use metaheuristic search biased by frequencies of proof tactics in existing, successful proof scripts. We find that TacTok outperforms WeightedRandom and WeightedGreedy, and is complementary to CoqHammer and ASTactic: for 24 out of the 26 projects, TacTok can synthesize proof scripts for some theorems the prior tools cannot. Together with TacTok, 11.5% more theorems can be proven automatically than by CoqHammer alone, and 20.0% than by ASTactic alone. Compared to a combination of CoqHammer and ASTactic, TacTok can prove an additional 3.6% more theorems, proving 115 theorems no tool could previously prove. Overall, our experiments provide evidence that partial proof script and proof state semantics, together, provide useful information for proof script modeling, and that metaheuristic search is a promising direction for proof script synthesis. TacTok is open-source and we make public all our data and a replication package of our experiments.
Flow2Vec: value-flow-based precise code embedding
Authors: Sui Yulei , Cheng Xiao , Zhang Guanqin , Wang Haoyu
Published: November 2020

Code embedding, as an emerging paradigm for source code analysis, has attracted much attention over the past few years. It aims to represent code semantics through distributed vector representations, which can be used to support a variety of program analysis tasks (e.g., code summarization and semantic labeling). However, existing code embedding approaches are intraprocedural, alias-unaware and ignoring the asymmetric transitivity of directed graphs abstracted from source code, thus they are still ineffective in preserving the structural information of code.

This paper presents Flow2Vec, a new code embedding approach that precisely preserves interprocedural program dependence (a.k.a value-flows). By approximating the high-order proximity, i.e., the asymmetric transitivity of value-flows, Flow2Vec embeds control-flows and alias-aware data-flows of a program in a low-dimensional vector space. Our value-flow embedding is formulated as matrix multiplication to preserve context-sensitive transitivity through CFL reachability by filtering out infeasible value-flow paths. We have evaluated Flow2Vec using 32 popular open-source projects. Results from our experiments show that Flow2Vec successfully boosts the performance of two recent code embedding approaches codevec and codeseq for two client applications, i.e., code classification and code summarization. For code classification, Flow2Vec improves codevec with an average increase of 21.2%, 20.1% and 20.7% in precision, recall and F1, respectively. For code summarization, Flow2Vec outperforms codeseq by an average of 13.2%, 18.8% and 16.0% in precision, recall and F1, respectively.
Battery Day
Authors: Frazelle Jessie
Published: November 2020

Tesla held its first Battery Day on September 22, 2020. The Tesla team didn't just look at one angle but all the angles: cell design, manufacturing, vehicle integration, and materials. If Tesla were to achieve 400 watt-hours per kilogram, a zero-emissions jet just might be on the horizon.
Everything VPN is New Again
Authors: Crawshaw David
Published: November 2020

The VPN (virtual private network) is 24 years old. The concept was created for a radically different Internet from the one we know today. As the Internet grew and changed, so did VPN users and applications. The VPN had an awkward adolescence in the Internet of the 2000s, interacting poorly with other widely popular abstractions. In the past decade the Internet has changed again, and this new Internet offers new uses for VPNs. The development of a radically new protocol, WireGuard, provides a technology on which to build these new VPNs.
The GDF15-GFRAL Pathway in Health and Metabolic Disease: Friend or Foe?
Authors: Breit Samuel N. , Brown David A. , Tsai Vicky Wang-Wei
Published: November 2020

GDF15 is a cell activation and stress response cytokine of the glial cell line–derived neurotrophic factor family within the TGF-β superfamily. It acts through a recently identified orphan member of the GFRα family called GFRAL and signals through the Ret coreceptor. Cell stress and disease lead to elevated GDF15 serum levels, causing anorexia, weight loss, and alterations to metabolism, largely by actions on regions of the hindbrain. These changes restore homeostasis and, in the case of obesity, cause a reduction in adiposity. In some diseases, such as advanced cancer, serum GDF15 levels can rise by as much as 10–100-fold, leading to an anorexia-cachexia syndrome, which is often fatal. This review discusses how GDF15 regulates appetite and metabolism, the role it plays in resistance to obesity, and how this impacts diseases such as diabetes, nonalcoholic fatty liver disease, and anorexia-cachexia syndrome. It also discusses potential therapeutic applications of targeting the GDF15-GFRAL pathway and lastly suggests some potential unifying hypotheses for its biological role.
On Fixed Point Results in Controlled Metric Spaces
Authors: Ahmad Jamshaid , Al-Mazrooei Abdullah Eqal , Aydi Hassen , De la Sen Manuel
Published: November 2020

In this article, we introduce Reich type contractions and (

α
,
F

)-contractions in the class of controlled metric spaces and establish some new related fixed point theorems. Our results are generalizations of some known results of literature. Some examples and certain consequences are given to illustrate significance of presented results.
Clinical Features and Risk Factors of Active Tuberculosis in Patients with Behçet’s Disease
Authors: Liu Yaxu , Zhang Lifan , Zhou Ziyue , Sun Luxi , Zhou Baotong , Liu Xiaoqing , Zheng Wenjie
Published: November 2020

To investigate the clinical features and potential risk factors of active tuberculosis (ATB) in Behçet’s disease (BD), we conducted a case-control study on hospitalized BD patients in our institute from 2010 to 2019. BD patients with ATB were enrolled as the case group. The control group was selected by random number sampling from the remaining BD patients, including those with latent tuberculosis infection, previous tuberculosis, or without tuberculosis. Finally, we reviewed 386 BD patients and identified 21 (5.4%) ATB cases, including four (19.0%) microbiologically confirmed and 17 (81.0%) clinically diagnosed. We found that BD patients with ATB were more prone to have systemic symptoms (fever, night sweating, and unexplained weight loss) and/or symptoms related to the infection site. Multivariate logistic regression analysis revealed that

erythrocyte
 
sedimentation
 
rate
 

ESR

>
60

 mm/h (

OR
=
13.710

, 95% CI (1.101, 170.702)), increased IgG (

OR
=
1.226

, 95% CI (1.001, 1.502)), and positive T-SPOT.TB (

OR
=
7.793

, 95% CI (1.312, 48.464), for 24-200 SFC/106PBMC;

OR
=
17.705

95% CI (2.503, 125.260), for >200 SFC/106PBMC) were potential risk factors for ATB in BD patients. Our study suggested that when BD patients have systemic symptoms with significantly elevated TB-SPOT, the diagnosis of ATB should be considered.
Short‐Term Cigarette Smoking in Rats Impairs Physical Capacity and Induces Cardiac Remodeling
Authors: Bocalini Danilo Sales , da Silva Luiz Rafael , Silva Kleiton Augusto Santos , Serra Andrey Jorge , Avila Renata Andrade , Leopoldo André Soares , Lima-Leopoldo Ana Paula , da Cunha Márcia Regina Holanda , Tucci Paulo Jose F. , dos Santos Leonardo
Published: November 2020

Despite the strong evidence on the cardiac and renal damages after chronic exposure to cigarette smoke, there is a paucity of data on its short‐term effects. The study evaluated the short‐term effects of cigarette smoking on left ventricular (LV) remodeling, in vitro myocardial and renal function. Female Wistar rats were randomized to control (C) and cigarette smoking rats for eight weeks. Physical capacity was assessed using an adapted model of exhaustive swim; left ventricle (LV) morphology and function were also evaluated. Renal function was assessed by creatinine clearance and urine protein. The in vitro myocardial performance was analyzed in isolated papillary muscles. Rats exhibited reduced physical capacity after short‐term cigarette smoking. Although there was no change on LV function, reduced chamber diameter was found in the smoking group associated with an increased LV wall thickness. There was augmented cardiac mass compared to C that was confirmed by increased cardiomyocyte nucleus volume, but in vitro myocardial performance and renal function were unchanged. A short‐term cigarette smoking induces cardiac remodeling without abnormalities in function. The smoking group still preserved renal function and in vitro myocardial performance. However, the reduced physical capacity may suggest an impairment of the cardiac reserve.
Analysis of Rotary Vibration of Rigid Friction Pipe Pile in Unsaturated Soil
Authors: Zhao Fu-yao , Xiang Peng
Published: November 2020

Based on the mixture theory and previous work, the governing equation of the rotary vibration of rigid friction pipe pile in unsaturated soil is established. The analytical solution of this equation can be used to analyze the displacements and the complex stiffness of rotary vibration. The results show that the contribution to stiffness is as follows: solid < liquid < gas; and the contribution to rotational impedance is as follows: solid > liquid > gas. In addition, when the fluid permeability coefficient decreases, the stiffness decreases and the rotational impedance increases, but the influence is not obvious (especially the gas permeability coefficient). Four different kinds of degradation problems are also presented. Relevant conclusions can provide reference for engineering application.
The Preventive Effects of Asparagus officinalis Extract on Sodium Selenite‐Induced Cataractogenesis in Experimental Animal Models
Authors: Azadbakht Momammad , Asghari Mohammad , Nowroozpoor Dailami Kiumars , Davoodi Ali , Ahmadi Amirhossein
Published: November 2020

Background and Objectives. Cataract is the leading cause of blindness worldwide. Although surgery is now considered the most successful cure, the development of alternative treatments is needed due to postsurgical complications. Oxidative stress in the lens is considered to be the most crucial factor in the formation of cataracts. Therefore, the effects of the hydroalcoholic extract of Asparagus officinalis L, a traditional antioxidative plant, on cataract formation of sodium selenite were evaluated. Materials and Methods. Neonatal rats received a single dose of sodium selenite as an intraperitoneal injection (30 μmol/kg) on day 10 postnatal to induce cataract. Animals were then posttreated with various oral solutions of A. officinalis extract at 200 mg/kg or 400 mg/kg once daily on days 10–16 postnatal. Cataract was evaluated by slit‐lamp, and lens opacification was analyzed in each group 24 hours after the last treatment at day seven postadministration of the extracts or vehicle. The total protein concentration of lenses, glutathione reductase activity as the glutathione antioxidant capacity, and malondialdehyde content as a marker of lipid peroxidation were further assessed in removed rat lenses on day 30 postnatal. Results. All lenses in the healthy and control plant groups were clear. Sodium selenite significantly increased cataract grade (2.8 ± 0.2) when compared to the healthy group (p = 0.001). However, cataract grades were decreased considerably as 1.9 ± 0.72 and 1.5 ± 0.85 in groups that received 200 mg/kg and 400 mg/kg oral extract of A. officinalis, respectively. A. officinalis extract also restored all abnormalities of biochemical markers induced by sodium selenite. Conclusion. Our data suggest that A. officinalis could be a promising candidate as a safe alternative treatment in cataracts upon further clinical trials. This effect is probably associated with the antioxidant activity of A. officinalis.