bluuebunny/crossref_metadata_2025_split huggingface dataset:
Gender gap in tenure and promotion: Evidence from the economics Ph.D. class of 2008
Authors: Chen Jihui , Liu Qihong , Kim Myongjin 
Published: March 2022

AbstractThis study examines early career outcomes (i.e., tenure and promotion) of the Economics Ph.D. class of 2008. We find that female economists are less likely (by up to 15.8%) to have received tenure and promotion 8 years post‐graduation compared to males in the same cohort. The gender gap becomes more pronounced (e.g., 36.5% less likely to receive tenure/promotion) among individuals of foreign origins working in the United States. In addition, we find a similar gender bias regarding whether an individual remains on tenure‐track positions since the initial job placement in 2008. Adding to the literature, our analysis sheds light on the gender gap in the Economics profession from a broad international perspective.
Type‐2 Diabetes and Identification of Major Genetic Determinants of Glycemic Index in Rice – A Review
Authors: John Deepa , Sureshkumar S. , Raman Maya 
Published: March 2022

AbstractRice consumers of different parts of the world always face the risk of diabetes and related health complications. Dietary intervention is the best adapted measure to maintain blood glucose levels and manage the diseases in rice consuming populations. The glycemic index of rice varieties is negatively correlated to the amylose content. Research studies have proven that the consumption of rice varieties with low glycemic index has beneficial effects in controlling diabetes. The genetic basis for the diversity observed for amylose content in different rice varieties is well elucidated. Waxy gene (Wx) is known to encode Granule–Bound Starch Synthase I (GBSS I) enzyme, which determines the amylose content in rice. Different allelic variations of Wx gene exist, which can be correlated to varying amylose content in rice. The PCR‐based markers for detecting single nucleotide polymorphism mutation at Wx locus provides a cost‐effective alternative to genotype rice varieties. This review outlines the anti‐diabetic properties of rice and strategies to identify rice varieties with a low glycemic index at the molecular level. The molecular basis of the glycemic index allows breeders to successfully identify rice germplasms with low glycemic index and engineer rice varieties with high grain yield and low glycemic index.
DyNetKAT: An Algebra of Dynamic Networks
Authors: Caltais Georgiana , Hojjat Hossein , Mousavi Mohammad Reza , Tunç Hünkar Can 
Published: March 2022

AbstractWe introduce a formal language for specifying dynamic updates for Software Defined Networks. Our language builds upon Network Kleene Algebra with Tests (NetKAT) and adds constructs for synchronisations and multi-packet behaviour to capture the interaction between the control- and data-plane in dynamic updates. We provide a sound and ground-complete axiomatisation of our language. We exploit the equational theory and provide an efficient method for reasoning about safety properties. We implement our equational theory in DyNetiKAT – a tool prototype, based on the Maude Rewriting Logic and the NetKAT tool, and apply it to a case study. We show that we can analyse the case study for networks with hundreds of switches using our tool prototype.
Quantifier elimination for counting extensions of Presburger arithmetic
Authors: Chistikov Dmitry , Haase Christoph , Mansutti Alessio 
Published: March 2022

AbstractWe give a new quantifier elimination procedure for Presburger arithmetic extended with a unary counting quantifier $$\exists ^{= x} y\, \mathrm {\Phi }$$

∃

=
x

y

Φ

that binds to the variable $$x$$
x
the number of different $$y$$
y
satisfying $$\mathrm {\Phi }$$
Φ
. While our procedure runs in non-elementary time in general, we show that it yields nearly optimal elementary complexity results for expressive counting extensions of Presburger arithmetic, such as the threshold counting quantifier $$\exists ^{\ge c} y\, \mathrm {\Phi }$$

∃

≥
c

y

Φ

that requires that the number of different y satisfying $$\mathrm {\Phi }$$
Φ
be at least $$c\in \mathbb {N}$$

c
∈
N

, where c can succinctly be defined by a Presburger formula. Our results are cast in terms of what we call the monadically-guarded fragment of Presburger arithmetic with unary counting quantifiers, for which we develop a 2ExpSpace decision procedure.
Sweedler Theory of Monads
Authors: McDermott Dylan , Rivas Exequiel , Uustalu Tarmo 
Published: March 2022

AbstractMonad-comonad interaction laws are a mathematical concept for describing communication protocols between effectful computations and coeffectful environments in the paradigm where notions of effectful computation are modelled by monads and notions of coeffectful environment by comonads. We show that monad-comonad interaction laws are an instance of measuring maps from Sweedler theory for duoidal categories whereby the final interacting comonad for a monad and a residual monad arises as the Sweedler hom and the initial residual monad for a monad and an interacting comonad as the Sweedler copower. We then combine this with a (co)algebraic characterization of monad-comonad interaction laws to derive descriptions of the Sweedler hom and the Sweedler copower in terms of their coalgebras resp. algebras.
Model Checking Temporal Properties of Recursive Probabilistic Programs
Authors: Winkler Tobias , Gehnen Christina , Katoen Joost-Pieter 
Published: March 2022

AbstractProbabilistic pushdown automata (pPDA) are a standard operational model for programming languages involving discrete random choices, procedures, and returns. Temporal properties are useful for gaining insight into the chronological order of events during program execution. Existing approaches in the literature have focused mostly on $$\omega $$
ω
-regular and LTL properties. In this paper, we study the model checking problem of pPDA against $$\omega $$
ω
-visibly pushdown languages that can be described by specification logics such as CaRet and are strictly more expressive than $$\omega $$
ω
-regular properties. With these logical formulae, it is possible to specify properties that explicitly take the structured computations arising from procedural programs into account. For example, CaRet is able to match procedure calls with their corresponding future returns, and thus allows to express fundamental program properties like total and partial correctness.
Graphical Piecewise-Linear Algebra
Authors: Boisseau Guillaume , Piedeleu Robin 
Published: March 2022

AbstractGraphical (Linear) Algebra is a family of diagrammatic languages allowing to reason about different kinds of subsets of vector spaces compositionally. It has been used to model various application domains, from signal-flow graphs to Petri nets and electrical circuits. In this paper, we introduce to the family its most expressive member to date: Graphical Piecewise-Linear Algebra, a new language to specify piecewise-linear subsets of vector spaces.Like the previous members of the family, it comes with a complete axiomatisation, which means it can be used to reason about the corresponding semantic domain purely equationally, forgetting the set-theoretic interpretation. We show completeness using a single axiom on top of Graphical Polyhedral Algebra, and show that this extension is the smallest that can capture a variety of relevant constructs.Finally, we showcase its use by modelling the behaviour of stateless electronic circuits of ideal elements, a domain that had remained outside the remit of previous diagrammatic languages.
Token Games and History-Deterministic Quantitative Automata
Authors: Boker Udi , Lehtinen Karoliina 
Published: March 2022

AbstractA nondeterministic automaton is history-deterministic if its nondeterminism can be resolved by only considering the prefix of the word read so far. Due to their good compositional properties, history-deterministic automata are useful in solving games and synthesis problems. Deciding whether a given nondeterministic automaton is history-deterministic (the problem) is generally a difficult task, which might involve an exponential procedure, or even be undecidable, for example for pushdown automata.Token gamesprovide aPTimesolution to the problem of Büchi and coBüchi automata, and it is conjectured that 2-token games characterise for all$$\omega $$ω-regular automata. We extend token games to the quantitative setting and analyze their potential to help deciding for quantitative automata. In particular, we show that 1-token games characterise for all quantitative (and Boolean) automata on finite words, as well as discounted-sum ($${\mathsf {DSum}}$$DSum) automata on infinite words, and that 2-token games characterise of$${\mathsf {LimInf}}$$LimInfand$${\mathsf {LimSup}}$$LimSupautomata. Using these characterisations, we provide solutions to the problem of$${\mathsf {Inf}}$$Infand$${\mathsf {Sup}}$$Supautomata on finite words inPTime, for$${\mathsf {DSum}}$$DSumautomata on finite and infinite words inNP$$\cap $$∩co-NP, for$${\mathsf {LimSup}}$$LimSupautomata in quasipolynomial time, and for$${\mathsf {LimInf}}$$LimInfautomata in exponential time, where the latter two are only polynomial for automata with a logarithmic number of weights.
Abstraction for Crash-Resilient Objects
Authors: Khyzha Artem , Lahav Ori 
Published: March 2022

AbstractWe study abstraction for crash-resilient concurrent objects using non-volatile memory (NVM). We develop a library-correctness criterion that is sound for ensuring contextual refinement in this setting, thus allowing clients to reason about library behaviors in terms of their abstract specifications, and library developers to verify their implementations against the specifications abstracting away from particular client programs. As a semantic foundation we employ a recent NVM model, called Persistent Sequential Consistency, and extend its language and operational semantics with useful specification constructs. The proposed correctness criterion accounts for NVM-related interactions between client and library code due to explicit persist instructions, and for calling policies enforced by libraries. We illustrate our approach on two implementations and specifications of simple persistent objects with different prototypical durability guarantees. Our results provide the first approach to formal compositional reasoning under NVM.
Static Race Detection for Periodic Programs
Authors: Suresh Varsha P , Pai Rekha , D’Souza Deepak , D’Souza Meenakshi , Chakrabarti Sujit Kumar 
Published: March 2022

AbstractWe consider the problem of statically detecting data races in periodic real-time programs that use locks, and run on a single processor platform. We propose a technique based on a small set of rules that exploits the priority, periodicity, locking, and timing information of tasks in the program. One of the key requirements is a response time analysis for such programs, and we propose an algorithm to compute this for the case of non-nested locks. We have implemented our analysis for real-time programs written in C in a tool called PePRacer and evaluated its performance on a small set of benchmarks from the literature.
Probabilistic Total Store Ordering
Authors: Abdulla Parosh Aziz , Atig Mohamed Faouzi , Agarwal Raj Aryan , Godbole Adwait , S. Krishna 
Published: March 2022

AbstractWe present Probabilistic Total Store Ordering (PTSO) – a probabilistic extension of the classical TSO semantics. For a given (finite-state) program, the operational semantics of PTSO induces an infinite-state Markov chain. We resolve the inherent non-determinism due to process schedulings and memory updates according to given probability distributions. We provide a comprehensive set of results showing the decidability of several properties for PTSO, namely (i) Almost-Sure (Repeated) Reachability: whether a run, starting from a given initial configuration, almost surely visits (resp. almost surely repeatedly visits) a given set of target configurations. (ii) Almost-Never (Repeated) Reachability: whether a run from the initial configuration, almost never visits (resp. almost never repeatedly visits) the target. (iii) Approximate Quantitative (Repeated) Reachability: to approximate, up to an arbitrary degree of precision, the measure of runs that start from the initial configuration and (repeatedly) visit the target. (iv) Expected Average Cost: to approximate, up to an arbitrary degree of precision, the expected average cost of a run from the initial configuration to the target. We derive our results through a nontrivial combination of results from the classical theory of (infinite-state) Markov chains, the theories of decisive and eager Markov chains, specific techniques from combinatorics, as well as, decidability and complexity results for the classical (non-probabilistic) TSO semantics. As far as we know, this is the first work that considers probabilistic verification of programs running on weak memory models.
A Dependent Dependency Calculus
Authors: Choudhury Pritam , Eades Harley , Weirich Stephanie 
Published: March 2022

AbstractOver twenty years ago, Abadi et al. established the Dependency Core Calculus (DCC) as a general purpose framework for analyzing dependency in typed programming languages. Since then, dependency analysis has shown many practical benefits to language design: its results can help users and compilers enforce security constraints, eliminate dead code, among other applications. In this work, we present a Dependent Dependency Calculus (DDC), which extends this general idea to the setting of a dependently-typed language. We use this calculus to track both run-time and compile-time irrelevance, enabling faster type-checking and program execution.
Structured Handling of Scoped Effects
Authors: Yang Zhixuan , Paviotti Marco , Wu Nicolas , van den Berg Birthe , Schrijvers Tom 
Published: March 2022

AbstractAlgebraic effects offer a versatile framework that covers a wide variety of effects. However, the family of operations that delimit scopes are not algebraic and are usually modelled as handlers, thus preventing them from being used freely in conjunction with algebraic operations. Although proposals for scoped operations exist, they are either ad-hoc and unprincipled, or too inconvenient for practical programming. This paper provides the best of both worlds: a theoretically-founded model of scoped effects that is convenient for implementation and reasoning. Our new model is based on an adjunction between a locally finitely presentable category and a category of functorial algebras. Using comparison functors between adjunctions, we show that our new model, an existing indexed model, and a third approach that simulates scoped operations in terms of algebraic ones have equal expressivity for handling scoped operations. We consider our new model to be the sweet spot between ease of implementation and structuredness. Additionally, our approach automatically induces fusion laws of handlers of scoped effects, which are useful for reasoning and optimisation.
Information-flow Interfaces
Authors: Bartocci Ezio , Ferrère Thomas , Henzinger Thomas A. , Nickovic Dejan , da Costa Ana Oliveira 
Published: March 2022

AbstractContract-based design is a promising methodology for taming the complexity of developing sophisticated systems. A formal contract distinguishes between assumptions, which are constraints that the designer of a component puts on the environments in which the component can be used safely, and guarantees, which are promises that the designer asks from the team that implements the component. A theory of formal contracts can be formalized as an interface theory, which supports the composition and refinement of both assumptions and guarantees.Although there is a rich landscape of contract-based design methods that address functional and extra-functional properties, we present the first interface theory that is designed for ensuring system-wide security properties. Our framework provides a refinement relation and a composition operation that support both incremental design and independent implementability. We develop our theory for both stateless and stateful interfaces. We illustrate the applicability of our framework with an example inspired from the automotive domain.
AequeVox: Automated Fairness Testing of Speech Recognition Systems
Authors: Rajan Sai Sathiesh , Udeshi Sakshi , Chattopadhyay Sudipta 
Published: March 2022

AbstractAutomatic Speech Recognition (ASR) systems have become ubiquitous. They can be found in a variety of form factors and are increasingly important in our daily lives. As such, ensuring that these systems are equitable to different subgroups of the population is crucial. In this paper, we introduce,AequeVox, an automated testing framework for evaluating the fairness of ASR systems.AequeVoxsimulates different environments to assess the effectiveness of ASR systems for different populations. In addition, we investigate whether the chosen simulations are comprehensible to humans. We further propose a fault localization technique capable of identifying words that are not robust to these varying environments. Both components ofAequeVoxare able to operate in the absence of ground truth data.We evaluateAequeVoxon speech from four different datasets using three different commercial ASRs. Our experiments reveal that non-native English, female and Nigerian English speakers generate109%,528.5%and156.9%more errors, on average than native English, male and UK Midlands speakers, respectively. Our user study also reveals that 82.9% of the simulations (employed through speech transformations) had a comprehensibility rating above seven (out of ten), with the lowest rating being 6.78. This further validates the fairness violations discovered byAequeVox. Finally, we show that the non-robust words, as predicted by the fault localization technique embodied inAequeVox, show223.8%more errors than the predicted robust words across all ASRs.
Semantic Clone Detection via Probabilistic Software Modeling
Authors: Thaller Hannes , Linsbauer Lukas , Egyed Alexander 
Published: March 2022

AbstractSemantic clone detection is the process of finding program elements with similar or equal runtime behavior. For example, detecting the semantic equality between the recursive and iterative implementation of the factorial computation. Semantic clone detection is the de facto technical boundary of clone detectors. In recent years, this boundary has been tested using interesting new approaches. This article contributes a semantic clone detection approach that detects clones which have 0 % syntactic similarity. We present Semantic Clone Detection via Probabilistic Software Modeling (SCD-PSM) as a stable and precise solution to semantic clone detection. PSM builds a probabilistic model of a program that is capable of evaluating and generating runtime data. SCD-PSM leverages this model and its model elements for finding behaviorally equal model elements. This behavioral equality is then generalized to semantic equality of the original program elements. It uses the likelihood between model elements as a distance metric. Then, it employs the likelihood ratio significance test to decide whether this distance is significant, given a pre-specified and controllable false-positive rate. The output of SCD-PSM are pairs of program elements (i.e., methods), their distance, and a decision on whether they are clones or not. SCD-PSM yields excellent results with a Matthews Correlation Coefficient greater than 0.9. These results are obtained on classical semantic clone detection problems such as detecting recursive and iterative versions of an algorithm, but also on complex problems used in coding competitions.
VeriFuzz: Good Seeds for Fuzzing (Competition Contribution)
Authors: Metta Ravindra , Medicherla Raveendra Kumar , Karmarkar Hrishikesh 
Published: March 2022

AbstractWe present VeriFuzz 1.2 with two new enhancements: (1) unroll the given program to a short depth and use BMC to produceincompletetest inputs, which are extended intocompleteinputs, and (2) if BMC fails for this short unrolling, automatically identify the reason and rerun BMC with a corresponding remedial strategy.
Construction of Verifier Combinations Based on Off-the-Shelf Verifiers
Authors: Beyer Dirk , Kanav Sudeep , Richter Cedric 
Published: March 2022

AbstractSoftware verifiers have different strengths and weaknesses, depending on properties of the verification task. It is well-known that combinations of verifiers via portfolio and selection approaches can help to combine the strengths. In this paper, we investigate (a) how to easily compose such combinations fromexisting, ‘off-the-shelf’ verification tools without changing them and (b) how much performance improvement easy combinations can yield, regarding the effectiveness (number of solved problems) and efficiency (consumed resources). First, we contribute a method to systematically and conveniently construct verifier combinations from existing tools, using the composition frameworkCoVeriTeam. We consider sequential portfolios, parallel portfolios, and algorithm selections. Second, we perform a large experiment on 8 883 verification tasks to show that combinations can improve the verification resultswithoutadditional computational resources. All combinations are constructed from off-the-shelf verifiers, that is, we use them as published. The result of our work suggests that users of verification tools can achieve a significant improvement at a negligible cost (only configure our composition scripts).
Quantitative Program Sketching using Lifted Static Analysis
Authors: Dimovski Aleksandar S. 
Published: March 2022

AbstractWe present a novel approach for resolving numerical program sketches under Boolean and quantitative objectives. The input is a program sketch, which represents a partial program with missing numerical parameters (holes). The aim is to automatically synthesize values for the parameters, such that the resulting complete program satisfies: a Boolean (qualitative) specification given in the form of assertions; and a quantitative specification that estimates the number of execution steps to termination and which the synthesizer is expected to optimize.To address the above quantitative sketching problem, we encode a program sketch as a program family (a.k.a. software product line) and analyze it by the specifically designed lifted analysis algorithms based on abstract interpretation. In particular, we use a combination of forward (numerical) and backward (termination) lifted analysis of program families to find the variants (family members) that satisfy all assertions, and moreover are optimal with respect to the given quantitative objective. Such obtained variants represent “correct & optimal” sketch realizations.We present a prototype implementation of our approach within the FamilySketcher tool for resolving C sketches with numerical types. We have evaluated our approach on a set of benchmarks, and experimental results confirm the effectiveness of our approach.