bluuebunny/crossref_metadata_2025_split huggingface dataset:
Combining Semilattices and Semimodules
Authors: Bonchi Filippo , Santamaria Alessio 
Published: March 2021

AbstractWe describe the canonical weak distributive law $$\delta :\mathcal S\mathcal P\rightarrow \mathcal P\mathcal S$$

δ
:
S
P
→
P
S

of the powerset monad $$\mathcal P$$
P
over the S-left-semimodule monad $$\mathcal S$$
S
, for a class of semirings S. We show that the composition of $$\mathcal P$$
P
with $$\mathcal S$$
S
by means of such $$\delta $$
δ
yields almost the monad of convex subsets previously introduced by Jacobs: the only difference consists in the absence in Jacobs’s monad of the empty convex set. We provide a handy characterisation of the canonical weak lifting of $$\mathcal P$$
P
to $$\mathbb {EM}(\mathcal S)$$

EM
(
S
)

as well as an algebraic theory for the resulting composed monad. Finally, we restrict the composed monad to finitely generated convex subsets and we show that it is presented by an algebraic theory combining semimodules and semilattices with bottom, which are the algebras for the finite powerset monad $$\mathcal P_f$$

P
f

.
Deductive Stability Proofs for Ordinary Differential Equations
Authors: Tan Yong Kiam , Platzer André 
Published: March 2021

AbstractStability is required for real world controlled systems as it ensures that those systems can tolerate small, real world perturbations around their desired operating states. This paper shows how stability for continuous systems modeled by ordinary differential equations (ODEs) can be formally verified in differential dynamic logic (). The key insight is to specify ODE stability by suitably nesting the dynamic modalities of with first-order logic quantifiers. Elucidating the logical structure of stability properties in this way has three key benefits: i) it provides a flexible means of formally specifying various stability properties of interest, ii) it yields rigorous proofs of those stability properties from ’s axioms with ’s ODE safety and liveness proof principles, and iii) it enables formal analysis of the relationships between various stability properties which, in turn, inform proofs of those properties. These benefits are put into practice through an implementation of stability proofs for several examples in KeYmaera X, a hybrid systems theorem prover based on .
Deductive Verification of Floating-Point Java Programs in KeY
Authors: Abbasi Rosa , Schiffl Jonas , Darulova Eva , Ulbrich Mattias , Ahrendt Wolfgang 
Published: March 2021

AbstractDeductive verification has been successful in verifying interesting properties of real-world programs. One notable gap is the limited support for floating-point reasoning. This is unfortunate, as floating-point arithmetic is particularly unintuitive to reason about due to rounding as well as the presence of the special values infinity and ‘Not a Number’ (NaN). In this paper, we present the first floating-point support in a deductive verification tool for the Java programming language. Our support in the KeY verifier handles arithmetic via floating-point decision procedures inside SMT solvers and transcendental functions via axiomatization. We evaluate this integration on new benchmarks, and show that this approach is powerful enough to prove the absence of floating-point special values—often a prerequisite for further reasoning about numerical computations—as well as certain functional properties for realistic benchmarks.
Helmholtz: A Verifier for Tezos Smart Contracts Based on Refinement Types
Authors: Nishida Yuki , Saito Hiromasa , Chen Ran , Kawata Akira , Furuse Jun , Suenaga Kohei , Igarashi Atsushi 
Published: March 2021

AbstractA smart contract is a program executed on a blockchain, based on which many cryptocurrencies are implemented, and is being used for automating transactions. Due to the large amount of money that smart contracts deal with, there is a surging demand for a method that can statically and formally verify them.This tool paper describes our type-based static verification tool Helmholtz for Michelson, which is a statically typed stack-based language for writing smart contracts that are executed on the blockchain platform Tezos. Helmholtz is designed on top of our extension of Michelson’s type system with refinement types. Helmholtz takes a Michelson program annotated with a user-defined specification written in the form of a refinement type as input; it then typechecks the program against the specification based on the refinement type system, discharging the generated verification conditions with the SMT solver Z3. We briefly introduce our refinement type system for the core calculus Mini-Michelson of Michelson, which incorporates the characteristic features such as compound datatypes (e.g., lists and pairs), higher-order functions, and invocation of another contract. Helmholtz successfully verifies several practical Michelson programs, including one that transfers money to an account and that checks a digital signature.
AMulet 2.0 for Verifying Multiplier Circuits
Authors: Kaufmann Daniela , Biere Armin 
Published: March 2021

AbstractAMulet 2.0 is a fully automatic tool for the verification of integer multipliers using computer algebra. Our tool models multiplier circuits given as and-inverter graphs as a set of polynomials and applies preprocessing techniques based on elimination theory of Gröbner bases. Finally it uses a polynomial reduction algorithm to verify the correctness of the given circuit. AMulet 2.0 is a re-factorization and improved re-implementation of our previous multiplier verification tool AMulet 1.0.
A Web Interface for Petri Nets with Transits and Petri Games
Authors: Gieseking Manuel , Hecking-Harbusch Jesko , Yanich Ann 
Published: March 2021

AbstractDeveloping algorithms for distributed systems is an error-prone task. Formal models like Petri nets with transits and Petri games can prevent errors when developing such algorithms. Petri nets with transits allow us to follow the data flow between components in a distributed system. They can be model checked against specifications in LTL on both the local data flow and the global behavior. Petri games allow the synthesis of local controllers for distributed systems from safety specifications. Modeling problems in these formalisms requires defining extended Petri nets which can be cumbersome when performed textually.In this paper, we present a web interface (The web interface is deployed at http://adam.informatik.uni-oldenburg.de.) that allows an intuitive, visual definition of Petri nets with transits and Petri games. The corresponding model checking and synthesis problems are solved directly on a server. In the interface, implementations, counterexamples, and all intermediate steps can be analyzed and simulated. Stepwise simulations and interactive state space generation support the user in detecting modeling errors.
Dartagnan: Leveraging Compiler Optimizations and the Price of Precision (Competition Contribution)
Authors: Ponce-de-León Hernán , Haas Thomas , Meyer Roland 
Published: March 2021

AbstractWe describe the new features of the bounded model checkerDartagnanforSV-COMP’21. We participate, for the first time, in theReachSafetycategory on the verification of sequential programs. In some of these verification tasks, bugs only show up after many loop iterations, which is a challenge for bounded model checking. We address the challenge by simplifying the structure of the input program while preserving its semantics. For simplification, we leverage common compiler optimizations, which we get for free by using LLVM. Yet, there is a price to pay. Compiler optimizations may introduce bitwise operations, which require bit-precise reasoning. We evaluated an SMT encoding based on the theory of integers + bit conversions against one based on the theory of bit-vectors and found that the latter yields better performance. Compared to the unoptimized version ofDartagnan, the combination of compiler optimizations and bit-vectors yields a speed-up of an order of magnitude on average.
Towards String Support in JayHorn (Competition Contribution)
Authors: Shamakhi Ali , Hojjat Hossein , Rümmer Philipp 
Published: March 2021

Abstractis a Horn clause-based model checker for Java programs that has been competing at SV-COMP since 2019. An ongoing research and implementation effort is to add support for data-type to . Since current Horn solvers do not support strings natively, we consider a representation of (unbounded) strings using algebraic data-types, more precisely as lists. This paper discusses Horn clause encodings of different string operations, and presents preliminary results.
VeriAbs: A Tool for Scalable Verification by Abstraction (Competition Contribution)
Authors: Darke Priyanka , Agrawal Sakshi , Venkatesh R. 
Published: March 2021

AbstractVeriAbs is a strategy selection-based reachability verifier for C programs. The selection of a suitable strategy is from a pre-defined set of strategies and by taking into account the syntax and semantics of the code to be verified. This year we present VeriAbs version 1.4.1 in which a novel preprocessor to strategy selection is introduced. The preprocessor checks for the feasibility of performing a lightweight slicing of the input code using function call graph and variable reference information. By this if the program is found to besliceable, sub-programs or slices are generated, and the known strategy selection algorithm of VeriAbs is applied to each slice. The verification results of each slice are then composed to derive that of the entire program. This compositional verification has improved the scalability of VeriAbs and presented in this paper.
Certifying Proofs in the First-Order Theory of Rewriting
Authors: Mitterwallner Fabian , Lochmann Alexander , Middeldorp Aart , Felgenhauer Bertram 
Published: March 2021

AbstractThe first-order theory of rewriting is a decidable theory for linear variable-separated rewrite systems. The decision procedure is based on tree automata techniques and recently we completed a formalization in the Isabelle proof assistant. In this paper we present a certificate language that enables the output of software tools implementing the decision procedure to be formally verified. To show the feasibility of this approach, we present , a reincarnation of the decision tool with certifiable output, and the formally verified certifier .
Do Judge a Test by its Cover
Authors: Goldstein Harrison , Hughes John , Lampropoulos Leonidas , Pierce Benjamin C. 
Published: March 2021

AbstractProperty-based testing uses randomly generated inputs to validate high-level program specifications. It can be shockingly effective at finding bugs, but it often requires generating a very large number of inputs to do so. In this paper, we apply ideas from combinatorial testing, a powerful and widely studied testing methodology, to modify the distributions of our random generators so as to find bugs with fewer tests. The key concept is combinatorial coverage, which measures the degree to which a given set of tests exercises every possible choice of values for every small combination of input features.In its “classical” form, combinatorial coverage only applies to programs whose inputs have a very particular shape—essentially, a Cartesian product of finite sets. We generalize combinatorial coverage to the richer world of algebraic data types by formalizing a class of sparse test descriptions based on regular tree expressions. This new definition of coverage inspires a novel combinatorial thinning algorithm for improving the coverage of random test generators, requiring many fewer tests to catch bugs. We evaluate this algorithm on two case studies, a typed evaluator for System F terms and a Haskell compiler, showing significant improvements in both.
Correctness of Sequential Monte Carlo Inference for Probabilistic Programming Languages
Authors: Lundén Daniel , Borgström Johannes , Broman David 
Published: March 2021

AbstractProbabilistic programming is an approach to reasoning under uncertainty by encoding inference problems as programs. In order to solve these inference problems, probabilistic programming languages (PPLs) employ different inference algorithms, such as sequential Monte Carlo (SMC), Markov chain Monte Carlo (MCMC), or variational methods. Existing research on such algorithms mainly concerns their implementation and efficiency, rather than the correctness of the algorithms themselves when applied in the context of expressive PPLs. To remedy this, we give a correctness proof for SMC methods in the context of an expressive PPL calculus, representative of popular PPLs such as WebPPL, Anglican, and Birch. Previous work have studied correctness of MCMC using an operational semantics, and correctness of SMC and MCMC in a denotational setting without term recursion. However, for SMC inference—one of the most commonly used algorithms in PPLs as of today—no formal correctness proof exists in an operational setting. In particular, an open question is if the resample locations in a probabilistic program affects the correctness of SMC. We solve this fundamental problem, and make four novel contributions: (i) we extend an untyped PPL lambda calculus and operational semantics to include explicit resample terms, expressing synchronization points in SMC inference; (ii) we prove, for the first time, that subject to mild restrictions, any placement of the explicit resample terms is valid for a generic form of SMC inference; (iii) as a result of (ii), our calculus benefits from classic results from the SMC literature: a law of large numbers and an unbiased estimate of the model evidence; and (iv) we formalize the bootstrap particle filter for the calculus and discuss how our results can be further extended to other SMC algorithms.
Bayesian strategies: probabilistic programs as generalised graphical models
Authors: Paquet Hugo 
Published: March 2021

AbstractWe introduce Bayesian strategies, a new interpretation of probabilistic programs in game semantics. This interpretation can be seen as a refinement of Bayesian networks.Bayesian strategies are based on a new form of event structure, with two causal dependency relations respectively modelling control flow and data flow. This gives a graphical representation for probabilistic programs which resembles the concrete representations used in modern implementations of probabilistic programming.From a theoretical viewpoint, Bayesian strategies provide a rich setting for denotational semantics. To demonstrate this we give a model for a general higher-order programming language with recursion, conditional statements, and primitives for sampling from continuous distributions and trace re-weighting. This is significant because Bayesian networks do not easily support higher-order functions or conditionals.
Query Lifting
Authors: Ricciotti Wilmer , Cheney James 
Published: March 2021

AbstractLanguage-integrated query based on comprehension syntax is a powerful technique for safe database programming, and provides a basis for advanced techniques such as query shredding or query flattening that allow efficient programming with complex nested collections. However, the foundations of these techniques are lacking: although SQL, the most widely-used database query language, supports heterogeneous queries that mix set and multiset semantics, these important capabilities are not supported by known correctness results or implementations that assume homogeneous collections. In this paper we study language-integrated query for a heterogeneous query language $$\mathcal {NRC}_{\lambda }( Set,Bag )$$

NRC
λ

(
S
e
t
,
B
a
g
)

that combines set and multiset constructs. We show how to normalize and translate queries to SQL, and develop a novel approach to querying heterogeneous nested collections, based on the insight that “local” query subexpressions that calculate nested subcollections can be “lifted” to the top level analogously to lambda-lifting for local function definitions.
Nested Session Types
Authors: Das Ankush , DeYoung Henry , Mordido Andreia , Pfenning Frank 
Published: March 2021

AbstractSession types statically describe communication protocols between concurrent message-passing processes. Unfortunately, parametric polymorphism even in its restricted prenex form is not fully understood in the context of session types. In this paper, we present the metatheory of session types extended with prenex polymorphism and, as a result, nested recursive datatypes. Remarkably, we prove that type equality is decidable by exhibiting a reduction to trace equivalence of deterministic first-order grammars. Recognizing the high theoretical complexity of the latter, we also propose a novel type equality algorithm and prove its soundness. We observe that the algorithm is surprisingly efficient and, despite its incompleteness, sufficient for all our examples. We have implemented our ideas by extending the Rast programming language with nested session types. We conclude with several examples illustrating the expressivity of our enhanced type system.
Tree-level S-matrix of superstring field theory with homotopy algebra structure
Authors: Kunitomo Hiroshi 
Published: March 2021

Abstract
We show that the tree-level S-matrices of the superstring field theories based on the homotopy-algebra structure agree with those obtained in the first-quantized formulation. The proof is given in detail for the heterotic string field theory. The extensions to the type II and open superstring field theories are straightforward.
Constructing Carrollian CFTs
Authors: Gupta Nishant , Suryanarayana Nemani V. 
Published: March 2021

Abstract
We construct classical theories for scalar fields in arbitrary Carroll spacetimes that are invariant under Carrollian diffeomorphisms and Weyl transformations. When the local symmetries are gauge fixed these theories become Carrollian conformal field theories. We show that generically there are at least two types of such theories: one in which only time derivatives of the fields appear and the other in which both space and time derivatives appear. A classification of such scalar field theories in three (and higher) dimensions up to two derivative order is provided. We show that only a special case of our theories arises in the ultra-relativistic limit of a covariant parent theory.
Suppressing blow-up by gradient-dependent flux limitation in a planar Keller–Segel–Navier–Stokes system
Authors: Winkler Michael 
Published: March 2021

AbstractThe flux-limited Keller–Segel–Navier–Stokes system $$\begin{aligned} \left\{ \begin{array}{lcl} n_t + u\cdot \nabla n &{}=&{} \Delta n - \nabla \cdot \Big ( n f(|\nabla c|^2) \nabla c\Big ), \\ c_t + u\cdot \nabla c &{}=&{} \Delta c - c + n, \\ u_t + (u\cdot \nabla ) u &{}=&{} \Delta u + \nabla P + n\nabla \Phi , \qquad \nabla \cdot u=0, \end{array} \right. \qquad \qquad (\star ) \end{aligned}$$

n
t

+
u
·
∇
n

=

Δ
n
-
∇
·

(

n
f
(
|
∇
c

|
2

)
∇
c

)

,

c
t

+
u
·
∇
c

=

Δ
c
-
c
+
n
,

u
t

+

(
u
·
∇
)

u

=

Δ
u
+
∇
P
+
n
∇
Φ
,

∇
·
u
=
0
,

(
⋆
)

is considered in a smoothly bounded domain $$\Omega \subset {\mathbb {R}}^2$$

Ω
⊂

R

2

. It is shown that whenever the suitably smooth function f models any asymptotically algebraic-type saturation of cross-diffusive fluxes in the sense that $$\begin{aligned} |f(\xi )| \le K_f\cdot (\xi +1)^{-\frac{\alpha }{2}} \end{aligned}$$

|
f

(
ξ
)

|

≤

K
f

·

(
ξ
+
1
)

-

α
2

holds for all $$\xi \ge 0$$

ξ
≥
0

with some $$K_f>0$$

K
f

>
0

and $$\alpha >0$$

α
>
0

, for any all reasonably regular initial data a corresponding no-flux/no-flux/Dirichlet problem admits a globally defined classical solution which is bounded, inter alia, in $$L^\infty (\Omega \times (0,\infty ))$$

L
∞

(
Ω
×

(
0
,
∞
)

)

with respect to all its components. By extending a corresponding result known for a fluid-free counterpart of ($$\star $$
⋆
), this confirms that with regard to the possible emergence of blow-up phenomena, the choice $$f\equiv const.$$

f
≡
c
o
n
s
t
.

retains some criticality also in the presence of fluid interaction.
Brain hemodynamic response in Examiner–Examinee dyads during spatial short-term memory task: an fNIRS study
Authors: Panico Francesco , De Marco Stefania , Sagliano Laura , D’Olimpio Francesca , Grossi Dario , Trojano Luigi 
Published: March 2021

AbstractThe Corsi Block-Tapping test (CBT) is a measure of spatial working memory (WM) in clinical practice, requiring an examinee to reproduce sequences of cubes tapped by an examiner. CBT implies complementary behaviors in the examiners and the examinees, as they have to attend a precise turn taking. Previous studies demonstrated that the Prefrontal Cortex (PFC) is activated during CBT, but scarce evidence is available on the neural correlates of CBT in the real setting. We assessed PFC activity in dyads of examiner–examinee participants while completing the real version of CBT, during conditions of increasing and exceeding workload. This procedure allowed to investigate whether brain activity in the dyads is coordinated. Results in the examinees showed that PFC activity was higher when the workload approached or reached participants’ spatial WM span, and lower during workload conditions that were largely below or above their span. Interestingly, findings in the examiners paralleled the ones in the examinees, as examiners’ brain activity increased and decreased in a similar way as the examinees’ one. In the examiners, higher left-hemisphere activity was observed suggesting the likely activation of non-spatial WM processes. Data support a bell-shaped relationship between cognitive load and brain activity, and provide original insights on the cognitive processes activated in the examiner during CBT.
Bimanual coordination associated with left- and right-hand dominance: testing the limb assignment and limb dominance hypothesis
Authors: Panzer Stefan , Kennedy Deanna , Leinen Peter , Pfeifer Christina , Shea Charles 
Published: March 2021

AbstractIn an experiment conducted by Kennedy et al. (Exp Brain Res 233:181–195, 2016), dominant right-handed individuals were required to produce a rhythm of isometric forces in a 2:1 or 1:2 bimanual coordination pattern. In the 2:1 pattern, the left limb performed the faster rhythm, while in the 1:2 pattern, the right limb produced the faster pattern. In the 1:2 pattern, interference occurred in the limb which had to produce the slower rhythm of forces. However, in the 2:1 condition, interference occurred in both limbs. The conclusion was that interference was not only influenced by movement frequency, but also influenced by limb dominance. The present experiment was designed to replicate these findings in dynamic bimanual 1:2 and 2:1 tasks where performers had to move one wrist faster than the other, and to determine the influence of limb dominance. Dominant left-handed (N = 10; LQ = − 89.81) and dominant right-handed (N = 14; LQ = 91.25) participants were required to perform a 2:1 and a 1:2 coordination pattern using Lissajous feedback. The harmonicity value was calculated to quantify the interference in the trial-time series. The analysis demonstrated that regardless of limb dominance, harmonicity was always lower in the slower moving limb than in the faster moving limb. The present results indicated that for dominant left- and dominant right-handers the faster moving limb influenced the slower moving limb. This is in accordance with the assumption that movement frequency has a higher impact on limb control in bimanual 2:1 and 1:2 coordination tasks than handedness.