bluuebunny/crossref_metadata_2025 huggingface dataset:
Slug, a Stress-Induced Transcription Factor, Stimulates Herpes Simplex Virus 1 Replication and Transactivates a
cis
-Regulatory Module within the VP16 Promoter
Authors: Santos Vanessa Claire , Ostler Jeffery B. , Harrison Kelly S. , Jones Clinton
Published: April 2023

Herpes simplex virus 1 (HSV-1) establishes lifelong latency in several types of neurons. Periodically cellular stressors trigger reactivation from latency.
Reconstitution and Mutagenesis of Avian Infectious Laryngotracheitis Virus from Cosmid and Yeast Centromeric Plasmid Clones
Authors: Spatz Stephen , García Maricarmen , Fuchs Walter , Loncoman Carlos , Volkening Jeremy , Ross Teresa , Riblet Sylva , Kim Taejoong , Likens Nathan , Mettenleiter Thomas
Published: April 2023

Infectious laryngotracheitis virus (ILTV) is an important pathogen of chicken with morbidity of 100% and mortality rates as high as 70%. Factoring in decreased production, mortality, vaccination, and medication, a single outbreak can cost producers over a million dollars.
Corynebacteria of the
diphtheriae
Species Complex in Companion Animals: Clinical and Microbiological Characterization of 64 Cases from France
Authors: Museux Kristina , Arcari Gabriele , Rodrigo Guido , Hennart Melanie , Badell Edgar , Toubiana Julie , Brisse Sylvain
Published: April 2023

We report on the occurrence and clinical and microbiological characteristics of infections caused by members of the CdSC in companion animals. This is the first study based on the systematic analysis of a very large animal cohort (18,308 samples), which provides data on the frequency of CdSC isolates in various types of clinical samples from animals.
SARS-CoV-2 Inhibits NRF2-Mediated Antioxidant Responses in Airway Epithelial Cells and in the Lung of a Murine Model of Infection
Authors: Qu Yue , Haas de Mello Aline , Morris Dorothea R. , Jones-Hall Yava L. , Ivanciuc Teodora , Sattler Rachel A. , Paessler Slobodan , Menachery Vineet D. , Garofalo Roberto P. , Casola Antonella
Published: April 2023

The antioxidant defense system plays a major function in protecting the organism against oxidative damage caused by free radicals. COVID-19 patients often present with biochemical characteristics of uncontrolled pro-oxidative responses in the respiratory tract.
Hot orogenesis in the Paleoproterozoic: Insights from granitic gneiss domes within the Jiao-Liao-Ji belt, North China craton
Authors: Zhang Jian , Yang Chengwei , Zhao Lifu , Zhang Cheng , Yang Hongxiang , Lu Tianjiao , Feng Jia , Hao Ran , Chen Xiaoyu , Liu Junlai
Published: April 2023

As a part of the Columbia supercontinent, the North China craton is an ideal object for studying the evolution of supercontinent assembly and the mechanism of orogenesis in the Paleoproterozoic. The Jiao-Liao-Ji belt, located in the eastern part of the North China craton, provides important clues for our understanding of Paleoproterozoic orogenic processes. A series of Paleoproterozoic granitic gneiss domes is preserved in the Liaodong segment of the Jiao-Liao-Ji belt. These domes are cored by the Liaoji granitic gneisses (emplaced at 2250−2150 Ma) and mantled by metamorphosed volcanic-sedimentary rocks (deposited at 2200−1940 Ma). Combining multiple lines of evidence from mesostructures and microstructures, kinematics, magnetic fabrics, and crystallographic fabrics, we suggest that the granitic gneiss domes reflect inhomogeneous shearing of the middle to lower crust during Paleoproterozoic orogenic processes. Intensive layer-paralleling shearing characterized subhorizontal flow during nearly E-W−oriented compression. As a hot orogen formed in the Paleoproterozoic, the orogenic deformation in the Jiao-Liao-Ji belt was characterized by extensive doming due to dominant subhorizontal flow and subsidiary vertical flow in the middle to lower crust.
Emergent patterns in global health diplomacy: a network analysis of the resolutions adopted by the World Health Assembly from 1948 to 2022
Authors: Wernli Didier , Falcone Jean-Luc , Davidshofer Stephan , Lee Kelley , Chopard Bastien , Levrat Nicolas
Published: April 2023

From a complexity perspective on governance, multilateral diplomacy is based on interactions between people, ideas, norms, policies and institutions. This article uses a computer-assisted methodology to better understand governance systems as a network of norms. All World Health Assembly (WHA) resolutions that were available from 1948 to 2022 were collected from the WHO Institutional Repository for Information Sharing (IRIS) database. Regular expressions were used to identify how resolutions cite other resolutions and the resulting relationships were analysed as a normative network. The findings show that WHA resolutions constitute a complex network of interconnected global health issues. This network is characterised by several community patterns. While chain-like patterns are associated with specific diseases programmes, radial patterns are characteristic of highly important procedural decisions that member states reaffirm in similar situations. Finally, densely connected communities correspond to contested topics and emergencies. While these emergent patterns suggest the relevance of using network analysis to understand global health norms in international organisations, we reflect on how this computational approach can be extended to provide new understandings of how multilateral governance systems work, and to address some important contemporary questions about the effects of regime complexity on global health diplomacy.
Learning needs and perceived barriers and facilitators to end-of-life care: a survey of front-line nurses on acute medical wards
Authors: Reid Julie C , Hoad Neala , Willison Kathleen , Hanmiah Rajendar , Brandt Vegas Daniel , Mitri Mino , Boyle Anne , Weatherston Amanda , Lohin Susan , McInnes Deborah , Rudkowski Jill C , Joyner Michelle , Cook Deborah J
Published: April 2023

Objectives

Caring for dying hospitalised patients is a healthcare priority. Our objective was to understand the learning needs of front-line nurses on the general internal medicine (GIM) hospital wards, and perceived barriers to, and facilitators of, optimal end-of-life care.

Methods

We developed an 85-item survey informed by the Theoretical Domains Framework and Capability–Opportunity–Motivation–Behaviour system. We included demographics and two main domains (knowledge and practice; delivering end-of-life care) with seven subsections. Nurses from four GIM wards and the nursing resource team completed this survey. We analysed and compared results overall, by Capability, Opportunity, and Motivation, and by survey domain. We considered items with median scores <4/7 barriers. We conducted an a priori subgroup analysis based on duration of practice (≤5 and >5 years).

Results

Our response rate was 60.5% (144/238). 51% had been practising for >5 years; most respondents were female (93.1%). Nurses had similar scores on the knowledge (mean 76.0%; SD 11.6%) and delivering care (mean 74.5% (8.6%)) domains. Scores for items associated with Capability were higher than those associated with Opportunity (median (first, third quartiles) 78.6% (67.9%, 87.5%) vs 73.9% (66.0%, 81.8%); p=0.04). Nurses practising >5 years had significantly higher scores on all analyses. Barriers included engaging with families having strong emotional reactions, managing goals of care conflicts between patients and families, and staffing challenges on the ward. Additional requested resources included formal training, information binders and more staff. Opportunities for consideration include formalised on-the-job training, access to comprehensive information, including symptom management at the end of life, and debriefing sessions.

Conclusions

Front-line nurses reported an interest in learning more about end-of-life care and identified important barriers that are feasible to address. These results will inform specific knowledge translation strategies to build capacity among bedside nurses to enhance end-of-life care practices for dying patients on GIM wards.
RGESolver: a C++ library to perform renormalization group evolution in the Standard Model Effective Theory
Authors: Di Noi Stefano , Silvestrini Luca
Published: April 2023

Renormalization group evolution above the electroweak scale is a crucial ingredient in the phenomenology of the Standard Model Effective Theory. The open-source  library performs the evolution at leading order for dimension-six operators in the most general flavour scenario (assuming lepton and baryon number conservation). Given its efficiency, can be used to include the effects of renormalization group evolution in extensive phenomenological analyses in the framework of the Standard Model Effective Theory.
Undecidably semilocalizable metric measure spaces
Authors: De Pauw Thierry
Published: April 2023

We characterize measure spaces such that the canonical map [Formula: see text] is surjective. In case of [Formula: see text]-dimensional Hausdorff measure on a complete separable metric space [Formula: see text], we give two equivalent conditions. We give examples of [Formula: see text] and [Formula: see text] so that whether these conditions are met is undecidable in ZFC, including one with [Formula: see text] equals the Hausdorff dimension of [Formula: see text].
Accelerating Fuzzing through Prefix-Guided Execution
Authors: Li Shaohua , Su Zhendong
Published: April 2023

Coverage-guided fuzzing is one of the most effective approaches for discovering software defects and vulnerabilities. It executes all mutated tests from seed inputs to expose coverage-increasing tests. However, executing all mutated tests incurs significant performance penalties---most of the mutated tests are discarded because they do not increase code coverage. Thus, determining if a test increases code coverage without actually executing it is beneficial, but a paradoxical challenge. In this paper, we introduce the notion of prefix-guided execution (PGE) to tackle this challenge. PGE leverages two key observations: (1) Only a tiny fraction of the mutated tests increase coverage, thus requiring full execution; and (2) whether a test increases coverage may be accurately inferred from its partial execution. PGE monitors the execution of a test and applies early termination when the execution prefix indicates that the test is unlikely to increase coverage.

To demonstrate the potential of PGE, we implement a prototype on top of AFL++, which we call AFL++-PGE. We evaluate AFL++-PGE on MAGMA, a ground-truth benchmark set that consists of 21 programs from nine popular real-world projects. Our results show that, after 48 hours of fuzzing, AFL++-PGE finds more bugs, discovers bugs faster, and achieves higher coverage.
Prefix-guided execution is general and can benefit the AFL-based family of fuzzers.
Solving Conditional Linear Recurrences for Program Verification: The Periodic Case
Authors: Wang Chenglin , Lin Fangzhen
Published: April 2023

In program verification, one method for reasoning about loops is to convert them into sets of recurrences, and
then try to solve these recurrences by computing their closed-form solutions.
While there are solvers for computing closed-form solutions to these recurrences,
their capabilities are limited when the recurrences have
conditional expressions, which arise when the body of a loop contains
conditional statements.
In this paper, we take a step towards solving these recurrences. Specifically, we consider what we call
conditional linear recurrences and show that given such a recurrence and an initial value, if the
index sequence generated by the recurrence on the initial value is what we call ultimately periodic,
then it has a closed-form solution. However, checking whether such a sequence is
ultimately periodic is undecidable so we propose a heuristic "generate and verify" algorithm for
checking the ultimate periodicity of the sequence and computing closed-form solutions at the same time.
We implemented a solver based on this algorithm, and
our experiments show that a straightforward program verifier based on our solver and using the SMT solver Z3
is effective in verifying properties of many benchmark programs that contain conditional statements in their loops,
and compares favorably to other recurrence-based verification tools. Finally, we also consider extending
our results to computing closed-form solutions of recurrences with unknown initial values.
Hybrid Multiparty Session Types: Compositionality for Protocol Specification through Endpoint Projection
Authors: Gheri Lorenzo , Yoshida Nobuko
Published: April 2023

Multiparty session types (MPST) are a specification and verification framework for distributed message-passing systems. The communication protocol of the system is specified as a
global type
, from which a collection of
local types
(local process implementations) is obtained by
endpoint projection
. A global type is a single disciplining entity for the whole system, specified by
one designer
that has full knowledge of the communication protocol. On the other hand, distributed systems are often described in terms of their
components
: a different designer is in charge of providing a subprotocol for each component. The problem of modular specification of global protocols has been addressed in the literature, but the state of the art focuses only on dual input/output compatibility. Our work overcomes this limitation. We propose the first MPST theory of
multiparty compositionality for distributed protocol specification
that is semantics-preserving, allows the composition of two or more components, and retains full MPST expressiveness. We introduce
hybrid types
for describing subprotocols interacting with each other, define a novel
compatibility relation
, explicitly describe an algorithm for composing multiple subprotocols into a
well-formed global type
, and prove that compositionality preserves projection, thus retaining semantic guarantees, such as liveness and deadlock freedom. Finally, we test our work against real-world case studies and we smoothly extend our novel compatibility to MPST with delegation and explicit connections.
Enabling Bounded Verification of Doubly-Unbounded Distributed Agreement-Based Systems via Bounded Regions
Authors: Wagner Christopher , Jaber Nouraldin , Samanta Roopsha
Published: April 2023

The ubiquity of distributed agreement protocols, such as consensus, has galvanized interest in verification of such protocols
as well as
applications built on top of them. The complexity and unboundedness of such systems, however, makes their verification onerous in general, and, particularly prohibitive for full automation. An exciting, recent breakthrough reveals that, through careful modeling, it becomes possible to reduce verification of interesting distributed agreement-based (DAB) systems, that are unbounded in the number of processes, to model checking of small, finite-state systems. It is an open question if such reductions are also possible for DAB systems that are
doubly-unbounded
, in particular, DAB systems that additionally have unbounded data domains. We answer this question in the affirmative in this work thereby broadening the class of DAB systems which can be automatically and efficiently verified. We present a novel reduction which leverages
value symmetry
and a new notion of
data saturation
to reduce verification of doubly-unbounded DAB systems to model checking of small, finite-state systems. We develop a tool, Venus, that can efficiently verify sophisticated DAB system models such as the arbitration mechanism for a consortium blockchain, a distributed register, and a simple key-value store.
Verus: Verifying Rust Programs using Linear Ghost Types
Authors: Lattuada Andrea , Hance Travis , Cho Chanhee , Brun Matthias , Subasinghe Isitha , Zhou Yi , Howell Jon , Parno Bryan , Hawblitzel Chris
Published: April 2023

The Rust programming language provides a powerful type system that checks linearity and borrowing, allowing code to safely manipulate memory without garbage collection and making Rust ideal for developing low-level, high-assurance systems. For such systems, formal verification can be useful to prove functional correctness properties beyond type safety. This paper presents Verus, an SMT-based tool for formally verifying Rust programs.
With Verus, programmers express proofs and specifications using the Rust language, allowing proofs to take advantage of Rust's linear types and borrow checking. We show how this allows proofs to manipulate linearly typed permissions that let Rust code safely manipulate memory, pointers, and concurrent resources. Verus organizes proofs and specifications using a novel mode system that distinguishes specifications, which are not checked for linearity and borrowing, from executable code and proofs, which are checked for linearity and borrowing.
We formalize Verus' linearity, borrowing, and modes in a small lambda calculus, for which we prove type safety and termination of specifications and proofs. We demonstrate Verus on a series of examples, including pointer-manipulating code (an xor-based doubly linked list), code with interior mutability, and concurrent code.
Compositional Security Definitions for Higher-Order Where Declassification
Authors: Menz Jan , Hirsch Andrew K. , Li Peixuan , Garg Deepak
Published: April 2023

To ensure programs do not leak private data, we often want to be able to provide formal guarantees ensuring such data is handled correctly. Often, we cannot keep such data secret entirely; instead programmers specify how private data may bedeclassified. While security definitions for declassification exist, they mostly do not handle higher-order programs. In fact, in the higher-order setting no compositional security definition exists for intensional information-flow properties such aswheredeclassification, which allows declassification in specific parts of a program. We use logical relations to build a model (and thus security definition) of where declassification. The key insight required for our model is that we must stop enforcing indistinguishability once arelevant declassificationhas occurred. We show that the resulting security definition provides more security than the most related previous definition, which is for the lower-order setting.
Deep Learning Robustness Verification for Few-Pixel Attacks
Authors: Shapira Yuval , Avneri Eran , Drachsler-Cohen Dana
Published: April 2023

While successful, neural networks have been shown to be vulnerable to adversarial example attacks. In
L
0
adversarial attacks, also known as few-pixel attacks, the attacker picks
t
pixels from the image and arbitrarily perturbs them. To understand the robustness level of a network to these attacks, it is required to check the robustness of the network to perturbations of every set of
t
pixels. Since the number of sets is exponentially large, existing robustness verifiers, which can reason about a single set of pixels at a time, are impractical for
L
0
robustness verification. We introduce Calzone, an
L
0
robustness verifier for neural networks. To the best of our knowledge, Calzone is the first to provide a sound and complete analysis for
L
0
adversarial attacks. Calzone builds on the following observation: if a classifier is robust to any perturbation of a set of
k
pixels, for
k
>
t
, then it is robust to any perturbation of its subsets of size
t
. Thus, to reduce the verification time, Calzone predicts the largest
k
that can be proven robust, via dynamic programming and sampling. It then relies on covering designs to compute a covering of the image with sets of size
k
. For each set in the covering, Calzone submits its corresponding box neighborhood to an existing
L
∞
robustness verifier. If a set’s neighborhood is not robust, Calzone repeats this process and covers this set with sets of size
k
′<
k
. We evaluate Calzone on several datasets and networks, for
t
≤ 5. Typically, Calzone verifies
L
0
robustness within few minutes. On our most challenging instances (e.g.,
t
=5), Calzone completes within few hours. We compare to a MILP baseline and show that it does not scale already for
t
=3.
Proof Automation for Linearizability in Separation Logic
Authors: Mulder Ike , Krebbers Robbert
Published: April 2023

Recent advances in concurrent separation logic enabled the formal verification of increasingly sophisticated fine-grained (
i.e.
, lock-free) concurrent programs. For such programs, the golden standard of correctness is
linearizability
, which expresses that concurrent executions always behave as some valid sequence of sequential executions. Compositional approaches to linearizability (such as contextual refinement and logical atomicity) make it possible to prove linearizability of whole programs or compound data structures (
e.g.
, a ticket lock) using proofs of linearizability of their individual components (
e.g.
, a counter). While powerful, these approaches are also laborious—state-of-the-art tools such as Iris, FCSL, and Voila all require a form of interactive proof.

This paper develops proof automation for contextual refinement and logical atomicity in Iris. The key ingredient of our proof automation is a collection of proof rules whose application is directed by both the program and the logical state. This gives rise to effective proof search strategies that can prove linearizability of simple examples fully automatically. For more complex examples, we ensure the proof automation cooperates well with interactive proof tactics by minimizing the use of backtracking.

We implement our proof automation in Coq by extending and generalizing Diaframe, a proof automation extension for Iris. While the old version (Diaframe 1.0) was limited to ordinary Hoare triples, the new version (Diaframe 2.0) is extensible in its support for program verification styles: our proof search strategies for contextual refinement and logical atomicity are implemented as modules for Diaframe 2.0. We evaluate our proof automation on a set of existing benchmarks and novel proofs, showing that it provides significant reduction of proof work for both approaches to linearizability.
Regular Expression Matching using Bit Vector Automata
Authors: Le Glaunec Alexis , Kong Lingkun , Mamouras Konstantinos
Published: April 2023

Regular expressions (regexes) are ubiquitous in modern software. There is a variety of implementation techniques for regex matching, which can be roughly categorized as (1) relying on backtracking search, or (2) being based on finite-state automata. The implementations that use backtracking are often chosen due to their ability to support advanced pattern-matching constructs. Unfortunately, they are known to suffer from severe performance problems. For some regular expressions, the running time for matching can be exponential in the size of the input text. In order to provide stronger guarantees of matching efficiency, automata-based regex matching is the preferred choice. However, even these regex engines may exhibit severe performance degradation for some patterns. The main reason for this is that regexes used in practice are not exclusively built from the classical regular constructs, i.e., concatenation, nondeterministic choice and Kleene's star. They involve additional constructs that provide succinctness and convenience of expression. The most common such construct is bounded repetition (also called counting), which describes the repetition of the pattern a fixed number of times.

In this paper, we propose a new algorithm for the efficient matching of regular expressions that involve bounded repetition. Our algorithms are based on a new model of automata, which we call nondeterministic bit vector automata (NBVA). This model is chosen to be expressively equivalent to nondeterministic counter automata with bounded counters, a very natural model for expressing patterns with bounded repetition. We show that there is a class of regular expressions with bounded repetition that can be matched in time that is independent from the repetition bounds. Our algorithms are general enough to cover the vast majority of challenging bounded repetitions that arise in practice. We provide an implementation of our approach in a regex engine, which we call BVA-Scan. We compare BVA-Scan against state-of-the-art regex engines on several real datasets.
Outcome Logic: A Unifying Foundation for Correctness and Incorrectness Reasoning
Authors: Zilberstein Noam , Dreyer Derek , Silva Alexandra
Published: April 2023

Program logics for bug-finding (such as the recently introduced Incorrectness Logic) have framed correctness and incorrectness as dual concepts requiring different logical foundations. In this paper, we argue that a single unified theory can be used for both correctness and incorrectness reasoning. We present Outcome Logic (OL), a novel generalization of Hoare Logic that is both
monadic
(to capture computational effects) and
monoidal
(to reason about outcomes and reachability). OL expresses true positive bugs, while retaining
correctness
reasoning abilities as well. To formalize the applicability of OL to both correctness and incorrectness, we prove that any false OL specification can be disproven in OL itself. We also use our framework to reason about new types of incorrectness in nondeterministic and probabilistic programs. Given these advances, we advocate for OL as a new foundational theory of correctness and incorrectness.
Aliasing Limits on Translating C to Safe Rust
Authors: Emre Mehmet , Boyland Peter , Parekh Aesha , Schroeder Ryan , Dewey Kyle , Hardekopf Ben
Published: April 2023

The Rust language was created to provide safe low-level systems programming. There is both industrial and academic interest in the problem of (semi-)automatically translating C code to Rust in order to exploit Rust's safety guarantees. We study the effectiveness and limitations of existing techniques for automatically translating unsafe raw pointers (in Rust programs translated from C) into safe Rust references via ownership and lifetime inference. Our novel evaluation methodology enables our study to extend beyond prior studies, and to discover new information contradicting the conclusions of prior studies. We find that existing translation methods are severely limited by a lack of precision in the Rust compiler's safety checker, causing many safe pointer manipulations to be labeled as potentially unsafe. Leveraging this information, we propose methods for improving translation, based on encoding the results of a more precise analysis in a manner that is understandable to an unmodified Rust compiler. We implement one of our proposed methods, increasing the number of pointers that can be translated to safe Rust references by 75% over the baseline (from 12% to 21% of all pointers).
Live Pattern Matching with Typed Holes
Authors: Yuan Yongwei , Guest Scott , Griffis Eric , Potter Hannah , Moon David , Omar Cyrus
Published: April 2023

Several modern programming systems, including GHC Haskell, Agda, Idris, and Hazel, support
typed holes
. Assigning static and, to varying degree, dynamic meaning to programs with holes allows program editors and other tools to offer meaningful feedback and assistance throughout editing, i.e. in a
live
manner. Prior work, however, has considered only holes appearing in expressions and types. This paper considers, from type theoretic and logical first principles, the problem of typed pattern holes. We confront two main difficulties, (1) statically reasoning about exhaustiveness and irredundancy when patterns are not fully known, and (2) live evaluation of expressions containing both pattern and expression holes. In both cases, this requires reasoning conservatively about all possible hole fillings. We develop a typed lambda calculus, Peanut, where reasoning about exhaustiveness and redundancy is mapped to the problem of deriving first order entailments. We equip Peanut with an operational semantics in the style of Hazelnut Live that allows us to evaluate around holes in both expressions and patterns. We mechanize the metatheory of Peanut in Agda and formalize a procedure capable of deciding the necessary entailments. Finally, we scale up and implement these mechanisms within Hazel, a programming environment for a dialect of Elm that automatically inserts holes during editing to provide static and dynamic feedback to the programmer in a maximally live manner, i.e. for every possible editor state. Hazel is the first maximally live environment for a general-purpose functional language.
Pushing the Limit of 1-Minimality of Language-Agnostic Program Reduction
Authors: Xu Zhenyang , Tian Yongqiang , Zhang Mengxiao , Zhao Gaosen , Jiang Yu , Sun Chengnian
Published: April 2023

Program reduction has demonstrated its usefulness in facilitating debugging language implementations in practice, by minimizing bug-triggering programs. There are two categories of program reducers: language-agnostic program reducers (AGRs) and language-specific program reducers (SPRs). AGRs, such as HDD and Perses, are generally applicable to various languages; SPRs are specifically designed for one language with meticulous thoughts and significant engineering efforts, e.g., C-Reduce for reducing C/C++ programs.

Program reduction is an NP-complete problem: finding the globally minimal program is usually infeasible. Thus all existing program reducers resort to producing 1-minimal results, a special type of local minima. However, 1-minimality can still be large and contain excessive bug-irrelevant program elements. This is especially the case for AGR-produced results because of the generic reduction algorithms used in AGRs. An SPR often yields smaller results than AGRs for the language for which the SPR has customized reduction algorithms. But SPRs are not language-agnostic, and implementing a new SPR for a different language requires significant engineering efforts.

This paper proposes Vulcan, a language-agnostic framework to further minimize AGRs-produced results by exploiting the formal syntax of the language to perform aggressive program transformations, in hope of creating reduction opportunities for other reduction algorithms to progress or even directly deleting bugirrelevant elements from the results. Our key insights are two-fold. First, the program transformations in all existing program reducers including SPRs are not diverse enough, which traps these program reducers early in 1-minimality. Second, compared with the original program, the results of AGRs are much smaller, and time-wise it is affordable to perform diverse program transformations that change programs but do not necessarily reduce the sizes of the programs directly. Within the Vulcan framework, we proposed three simple examples of fine-grained program transformations to demonstrate that Vulcan can indeed further push the 1-minimality of AGRs. By performing these program transformations, a 1-minimal program might become a non-1-minimal one that can be further reduced later.

Our extensive evaluations on multilingual benchmarks including C, Rust and SMT-LIBv2 programs strongly demonstrate the effectiveness and generality of Vulcan. Vulcan outperforms the state-of-the-art language-agnostic program reducer Perses in size in all benchmarks: On average, the result of Vulcan contains 33.55%, 21.61%, and 31.34% fewer tokens than that of Perses on C, Rust, and SMT-LIBv2 subjects respectively. Vulcan can produce even smaller results if more reduction time is allocated. Moreover, for the C programs that are reduced by C-Reduce, Vulcan is even able to further minimize them by 10.07%.
Exact Recursive Probabilistic Programming
Authors: Chiang David , McDonald Colin , Shan Chung-chieh
Published: April 2023

Recursive calls over recursive data are useful for generating probability distributions, and probabilistic programming allows computations over these distributions to be expressed in a modular and intuitive way. Exact inference is also useful, but unfortunately, existing probabilistic programming languages do not perform exact inference on recursive calls over recursive data, forcing programmers to code many applications manually. We introduce a probabilistic language in which a wide variety of recursion can be expressed naturally, and inference carried out exactly. For instance, probabilistic pushdown automata and their generalizations are easy to express, and polynomial-time parsing algorithms for them are derived automatically. We eliminate recursive data types using program transformations related to defunctionalization and refunctionalization. These transformations are assured correct by a linear type system, and a successful choice of transformations, if there is one, is guaranteed to be found by a greedy algorithm.
Lower Bounds for Possibly Divergent Probabilistic Programs
Authors: Feng Shenghua , Chen Mingshuai , Su Han , Kaminski Benjamin Lucien , Katoen Joost-Pieter , Zhan Naijun
Published: April 2023

We present a new proof rule for verifying lower bounds on quantities of probabilistic programs. Our proof rule is not confined to almost-surely terminating programs -- as is the case for existing rules -- and can be used to establish non-trivial lower bounds on, e.g., termination probabilities and expected values, for possibly divergent probabilistic loops, e.g., the well-known three-dimensional random walk on a lattice.
Algebro-geometric Algorithms for Template-Based Synthesis of Polynomial Programs
Authors: Goharshady Amir Kafshdar , Hitarth S. , Mohammadi Fatemeh , Motwani Harshit Jitendra
Published: April 2023

Template-based synthesis, also known as sketching, is a localized approach to program synthesis in which the programmer provides not only a specification, but also a high-level "sketch" of the program. The sketch is basically a partial program that models the general intuition of the programmer, while leaving the low-level details as unimplemented "holes". The role of the synthesis engine is then to fill in these holes such that the completed program satisfies the desired specification. In this work, we focus on template-based synthesis of polynomial imperative programs with real variables, i.e. imperative programs in which all expressions appearing in assignments, conditions and guards are polynomials over program variables. While this problem can be solved in a sound and complete manner by a reduction to the first-order theory of the reals, the resulting formulas will contain a quantifier alternation and are extremely hard for modern SMT solvers, even when considering toy programs with a handful of lines. Moreover, the classical algorithms for quantifier elimination are notoriously unscalable and not at all applicable to this use-case.

In contrast, our main contribution is an algorithm, based on several well-known theorems in polyhedral and real algebraic geometry, namely Putinar's Positivstellensatz, the Real Nullstellensatz, Handelman's Theorem and Farkas' Lemma, which sidesteps the quantifier elimination difficulty and reduces the problem directly to Quadratic Programming (QP). Alternatively, one can view our algorithm as an efficient way of eliminating quantifiers in the particular formulas that appear in the synthesis problem. The resulting QP instances can then be handled quite easily by SMT solvers. Notably, our reduction to QP is sound and semi-complete, i.e. it is complete if polynomials of a sufficiently high degree are used in the templates. Thus, we provide the first method for sketching-based synthesis of polynomial programs that does not sacrifice completeness, while being scalable enough to handle meaningful programs. Finally, we provide experimental results over a variety of examples from the literature.
Randomized Testing of Byzantine Fault Tolerant Algorithms
Authors: Winter Levin N. , Buse Florena , de Graaf Daan , von Gleissenthall Klaus , Kulahcioglu Ozkan Burcu
Published: April 2023

Byzantine fault-tolerant algorithms promise agreement on a correct value, even if a subset of processes can deviate from the algorithm arbitrarily. While these algorithms provide strong guarantees in theory, in practice, protocol bugs and implementation mistakes may still cause them to go wrong. This paper introduces ByzzFuzz, a simple yet effective method for automatically finding errors in implementations of Byzantine fault-tolerant algorithms through randomized testing. ByzzFuzz detects fault-tolerance bugs by injecting randomly generated network and process faults into their executions. To navigate the space of possible process faults, ByzzFuzz introduces small-scope message mutations which mutate the contents of the protocol messages by applying small changes to the original message either in value (e.g., by incrementing the round number) or in time (e.g., by repeating a proposal value from a previous message). We find that small-scope mutations, combined with insights from the testing and fuzzing literature, are effective at uncovering protocol logic and implementation bugs in real-world fault-tolerant systems.

We implemented ByzzFuzz and applied it to test the production implementations of two popular blockchain systems, Tendermint and Ripple, and an implementation of the seminal PBFT protocol. ByzzFuzz detected several bugs in the implementation of PBFT, a potential liveness violation in Tendermint, and materialized two theoretically described vulnerabilities in Ripple’s XRP Ledger Consensus Algorithm. Moreover, we discovered a previously unknown fault-tolerance bug in the production implementation of Ripple, which is confirmed by the developers and fixed.
Verification-Preserving Inlining in Automatic Separation Logic Verifiers
Authors: Dardinier Thibault , Parthasarathy Gaurav , Müller Peter
Published: April 2023

Bounded verification has proved useful to detect bugs and to increase confidence in the correctness of a program. In contrast to unbounded verification, reasoning about calls via (bounded) inlining and about loops via (bounded) unrolling does not require method specifications and loop invariants and, therefore, reduces the annotation overhead to the bare minimum, namely specifications of the properties to be verified. For verifiers based on traditional program logics, verification is preserved by inlining (and unrolling): successful unbounded verification of a program w.r.t. some annotation implies successful verification of the inlined program. That is, any error detected in the inlined program reveals a true error in the original program. However, this essential property might not hold for automatic separation logic verifiers such as Caper, GRASShopper, RefinedC, Steel, VeriFast, and verifiers based on Viper. In this setting, inlining generally changes the resources owned by method executions, which may affect automatic proof search algorithms and introduce spurious errors.
In this paper, we present the first technique for verification-preserving inlining in automatic separation logic verifiers. We identify a semantic condition on programs and prove in Isabelle/HOL that it ensures verification-preserving inlining for state-of-the-art automatic separation logic verifiers. We also prove a dual result: successful verification of the inlined program ensures that there are method and loop annotations that enable the verification of the original program for bounded executions. To check our semantic condition automatically, we present two approximations that can be checked syntactically and with a program verifier, respectively. We implement these checks in Viper and demonstrate that they are effective for non-trivial examples from different verifiers.
Improving Oracle-Guided Inductive Synthesis by Efficient Question Selection
Authors: Ji Ruyi , Kong Chaozhe , Xiong Yingfei , Hu Zhenjiang
Published: April 2023

Oracle-guided inductive synthesis (OGIS) is a widely-used framework to apply program synthesis techniques in practice. The question selection problem aims at reducing the number of iterations in OGIS by selecting a proper input for each OGIS iteration. Theoretically, a question selector can generally improve the performance of OGIS solvers on both interactive and non-interactive tasks if it is not only effective for reducing iterations but also efficient. However, all existing effective question selectors fail in satisfying the requirement of efficiency. To ensure effectiveness, they convert the question selection problem into an optimization one, which is difficult to solve within a short time.

In this paper, we propose a novel question selector, named
LearnSy
.
LearnSy
is both efficient and effective and thus achieves general improvement for OGIS solvers for the first time. Since we notice that the optimization tasks in previous studies are difficult because of the complex behavior of operators, we estimate these behaviors in
LearnSy
as simple random events. Subsequently, we provide theoretical results for the precision of this estimation and design an efficient algorithm for its calculation.

According to our evaluation, when dealing with interactive tasks,
LearnSy
can offer competitive performance compared to existing selectors while being more efficient and more general. Moreover, when working on non-interactive tasks,
LearnSy
can generally reduce the time cost of existing CEGIS solvers by up to 43.0%.
Back to Direct Style: Typed and Tight
Authors: Müller Marius , Schuster Philipp , Brachthäuser Jonathan Immanuel , Ostermann Klaus
Published: April 2023

Translating programs into continuation-passing style is a well-studied
tool to explicitly deal with the control structure of programs. This is
useful, for example, for compilation.
In a typed setting, there also is a logical interpretation of such a translation
as an embedding of classical logic into intuitionistic logic.
A naturally arising question is whether there is an inverse translation
back to direct style. The answer to this question depends on how the
continuation-passing translation is defined and on the domain of the inverse translation.
In general, translating programs from continuation-passing style back to direct
style requires the use of control operators to account for the use of
continuations in non-trivial ways.

We present two languages, one in direct style and one in continuation-passing
style. Both languages are typed and equipped with an abstract machine semantics.
Moreover, both languages allow for non-trivial control flow.
We further present a translation to continuation-passing style and a translation
back to direct style. We show that both translations are type-preserving and
also preserve semantics in a very precise way giving an operational
correspondence between the two languages.
Moreover, we show that the compositions of the translations are well-behaved.
In particular, they are syntactic one-sided inverses on the full language and full
syntactic inverses when restricted to trivial control flow.
Fluent APIs in Functional Languages
Authors: Roth Ori , Gil Yossi
Published: April 2023

Fluent API is an object-oriented pattern for elegant APIs and embedded DSLs.
A smart fluent API can enforce the API protocol or DSL syntax at compile time.
Since fluent API implementations typically rely on overloading function names, they are hard to realize in functional programming languages.
This work shows how functional fluent APIs can be implemented in the absence of name overloading, by relying on parametric polymorphism and Hindley-Milner type inference.
The implementation supports fluent API protocols in the regular- and deterministic context-free language classes, and even beyond.
GNN-based Multi-bit Flip-flop Clustering and Post-clustering Design Optimization for Energy-efficient 3D ICs
Authors: Vanna-Iampikul Pruek , Lu Yi-Chen , Shim Da Eun , Lim Sung Kyu
Published: April 2023

In high-performance three-dimensional Integrated Circuits (3D ICs), clock networks consume a large portion of the full-chip power. However, no previous 3D IC work has ever optimized 3D clock networks for both power and performance simultaneously, which results in sub-optimal 3D designs. To overcome this issue, in this article, we propose a GNN-based flip-flop clustering algorithm that merges single-bit flip-flops into multi-bit flip-flops in an unsupervised manner, which jointly optimizes the power and performance metrics of clock networks. Moreover, we integrate our algorithm into the state-of-the-art 3D physical design flow and verify the integration, which leads to a better 3D full-chip design. Experimental results on eight industrial benchmarks demonstrate that the algorithm achieves improvements up to 18% in total power and 8.2% in performance over the state-of-the-art 3D flow.
From Surplus and Scarcity toward Abundance: Understanding the Use of ICT in Food Resource Sharing Practices
Authors: Engelbutzeder Philip , Randell Dave , Landwehr Marvin , Aal Konstantin , Stevens Gunnar , Wulf Volker
Published: April 2023

Food practices have become an important context for questions around sustainability. Within HCI, sustainable HCI and human-food-interaction have developed as a response. We argue, nevertheless, that food practices as a social activity remain relatively under-examined, and further that sustainable food practices hinge on communal activity. We present the results of action-oriented research with a grassroots movement committed to sustainable food practices at a local, communal level, thereby demonstrating the role of ICT in making food resource sharing a viable practice. We suggest that the current focus on food sharing might usefully be supplemented by attention to food resource sharing, an approach that aligns with a paradigm shift from surplus to abundance. We argue for a design that aims to encourage food resource sharing at a local level but that also has wider ramifications. These “glocal” endeavors recognize the complexity of prosumption practices and foster aspirations for “deep change” in food systems.
Privacy-preserving Decentralized Federated Learning over Time-varying Communication Graph
Authors: Lu Yang , Yu Zhengxin , Suri Neeraj
Published: April 2023

Establishing how a set of learners can provide privacy-preserving federated learning in a fully decentralized (peer-to-peer, no coordinator) manner is an open problem. We propose the first privacy-preserving consensus-based algorithm for the distributed learners to achieve decentralized global model aggregation in an environment of high mobility, where participating learners and the communication graph between them may vary during the learning process. In particular, whenever the communication graph changes, the Metropolis-Hastings method [
69
] is applied to update the weighted adjacency matrix based on the current communication topology. In addition, the Shamir’s secret sharing (SSS) scheme [
61
] is integrated to facilitate privacy in reaching consensus of the global model. The article establishes the correctness and privacy properties of the proposed algorithm. The computational efficiency is evaluated by a simulation built on a federated learning framework with a real-world dataset.
Effects of Chloride Ions on Passive Oxide Films Formed on Cr-Fe-Co-Ni(-Mo) Multi-Principal Element Alloy Surfaces
Authors: Wang Xueying , Mercier Dimitri , Zanna Sandrine , Seyeux Antoine , Perriere Loïc , Laurent-Brocq Mathilde , Guillot Ivan , Maurice Vincent , Marcus Philippe
Published: April 2023

The composition and stratification of the passive oxide films formed on three Cr-Fe-Co-Ni(-Mo) multi-principal element alloys by electrochemical anodic passivation in sulfuric acid electrolyte containing 0.2 and 4.7 M NaCl were investigated, combining X-ray photoelectron spectroscopy and time-of-flight secondary ion mass spectrometry surface analysis. The passive films show a bilayer structure similar to that formed in Cl−-free electrolyte with an inner layer mostly consisting of Cr oxide and an outer layer containing of Cr hydroxide, Ni hydroxide, Mo oxides, and Fe (hydr)oxide. The Mo-free alloy exhibits a thickening of the inner Cr oxide layer and the thinning of the outer layer in 0.2 M Cl−, whereas the two Mo-containing alloys do not show significant alteration even in 4.7 M Cl− evidencing their higher stability in Cl−-containing solutions. The chloride penetration is limited to the external part of the outer oxide layer, except in the most severe tested conditions where traces reach the inner barrier layer, and the chloride entry into the layer is strongly reduced after pre-passivation in Cl−-free solution. The results allow us to discuss the beneficial effects of pre-passivation in Cl−-free conditions and Mo addition providing these alloys enhanced resistance to passivity breakdown.