bluuebunny/crossref_metadata_2025_split huggingface dataset:
Early Verification of Legal Compliance via Bounded Satisfiability Checking
Authors: Feng Nick , Marsso Lina , Sabetzadeh Mehrdad , Chechik Marsha 
Published: July 2023

AbstractLegal properties involve reasoning about data values and time. Metric first-order temporal logic (MFOTL) provides a rich formalism for specifying legal properties. While MFOTL has been successfully used for verifying legal properties over operational systems via runtime monitoring, no solution exists for MFOTL-based verification in early-stage system development captured by requirements. Given a legal property and system requirements, both formalized in MFOTL, the compliance of the property can be verified on the requirements via satisfiability checking. In this paper, we propose a practical, sound, and complete (within a given bound) satisfiability checking approach for MFOTL. The approach, based on satisfiability modulo theories (SMT), employs a counterexample-guided strategy to incrementally search for a satisfying solution. We implemented our approach using the Z3 SMT solver and evaluated it on five case studies spanning the healthcare, business administration, banking and aviation domains. Our results indicate that our approach can efficiently determine whether legal properties of interest are met, or generate counterexamples that lead to compliance violations.
Formula Normalizations in Verification
Authors: Guilloud Simon , Bucev Mario , Milovančević Dragana , Kunčak Viktor 
Published: July 2023

AbstractWe apply and evaluate polynomial-time algorithms to compute two different normal forms of propositional formulas arising in verification. One of the normal form algorithms is presented for the first time. The algorithms compute normal forms and solve the word problem for two different subtheories of Boolean algebra: orthocomplemented bisemilattice (OCBSL) and ortholattice (OL). Equality of normal forms decides the word problem and is a sufficient (but not necessary) check for equivalence of propositional formulas. Our first contribution is a quadratic-time OL normal form algorithm, which induces a coarser equivalence than the OCBSL normal form and is thus a more precise approximation of propositional equivalence. The algorithm is efficient even when the input formula is represented as a directed acyclic graph. Our second contribution is the evaluation of OCBSL and OL normal forms as part of a verification condition cache of the Stainless verifier for Scala. The results show that both normalization algorithms substantially increase the cache hit ratio and improve the ability to prove verification conditions by simplification alone. To gain further insights, we also compare the algorithms on hardware circuit benchmarks, showing that normalization reduces circuit size and works well in the presence of sharing.
Automated Tail Bound Analysis for Probabilistic Recurrence Relations
Authors: Sun Yican , Fu Hongfei , Chatterjee Krishnendu , Goharshady Amir Kafshdar 
Published: July 2023

AbstractProbabilistic recurrence relations (PRRs) are a standard formalism for describing the runtime of a randomized algorithm. Given a PRR and a time limit $$\kappa $$
κ
, we consider the tail probability $$\Pr [T \ge \kappa ]$$

Pr
[
T
≥
κ
]

, i.e., the probability that the randomized runtime T of the PRR exceeds $$\kappa $$
κ
. Our focus is the formal analysis of tail bounds that aims at finding a tight asymptotic upper bound $$u \ge \Pr [T\ge \kappa ]$$

u
≥
Pr
[
T
≥
κ
]

. To address this problem, the classical and most well-known approach is the cookbook method by Karp (JACM 1994), while other approaches are mostly limited to deriving tail bounds of specific PRRs via involved custom analysis.
In this work, we propose a novel approach for deriving the common exponentially-decreasing tail bounds for PRRs whose preprocessing time and random passed sizes observe discrete or (piecewise) uniform distribution and whose recursive call is either a single procedure call or a divide-and-conquer. We first establish a theoretical approach via Markov’s inequality, and then instantiate the theoretical approach with a template-based algorithmic approach via a refined treatment of exponentiation. Experimental evaluation shows that our algorithmic approach is capable of deriving tail bounds that are (i) asymptotically tighter than Karp’s method, (ii) match the best-known manually-derived asymptotic tail bound for QuickSelect, and (iii) is only slightly worse (with a $$\log \log n$$

log
log
n

factor) than the manually-proven optimal asymptotic tail bound for QuickSort. Moreover, our algorithmic approach handles all examples (including realistic PRRs such as QuickSort, QuickSelect, DiameterComputation, etc.) in less than 0.1 s, showing that our approach is efficient in practice.
Kratos2: An SMT-Based Model Checker for Imperative Programs
Authors: Griggio Alberto , Jonáš Martin 
Published: July 2023

AbstractThis paper describes , a tool for the verification of imperative programs. operates on an intermediate verification language called , with a formally-specified semantics based on smt, allowing the specification of both reachability and liveness properties. It integrates several state-of-the-art verification engines based on sat and smt. Moreover, it provides additional functionalities such as a flexible Python api, a customizable C front-end, generation of counterexamples, support for simulation and symbolic execution, and translation into multiple low-level verification formalisms. Our experimental analysis shows that is competitive with state-of-the-art software verifiers on a large range of programs. Thanks to its flexibility, has already been used in various industrial projects and academic publications, both as a verification back-end and as a benchmark generator.
Making $$\textsf {IP}=\textsf {PSPACE}$$ Practical: Efficient Interactive Protocols for BDD Algorithms
Authors: Couillard Eszter , Czerner Philipp , Esparza Javier , Majumdar Rupak 
Published: July 2023

AbstractWe show that interactive protocols between a prover and a verifier, a well-known tool of complexity theory, can be used in practice to certify the correctness of automated reasoning tools.Theoretically, interactive protocols exist for all $$\textsf {PSPACE}$$
PSPACE
problems. The verifier of a protocol checks the prover’s answer to a problem instance in probabilistic polynomial time, with polynomially many bits of communication, and with exponentially small probability of error. (The prover may need exponential time.) Existing interactive protocols are not used in practice because their provers use naive algorithms, inefficient even for small instances, that are incompatible with practical implementations of automated reasoning.We bridge the gap between theory and practice by means of an interactive protocol whose prover uses BDDs. We consider the problem of counting the number of assignments to a QBF instance ($$\#\text {CP}$$

#
CP

), which has a natural BDD-based algorithm. We give an interactive protocol for $$\#\text {CP}$$

#
CP

whose prover is implemented on top of an extended BDD library. The prover has only a linear overhead in computation time over the natural algorithm.We have implemented our protocol in $$\textsf {blic}$$
blic
, a certifying tool for $$\#\text {CP}$$

#
CP

. Experiments on standard QBF benchmarks show that is competitive with state-of-the-art QBF-solvers. The run time of the verifier is negligible. While loss of absolute certainty can be concerning, the error probability in our experiments is at most $$10^{-10}$$

10

-
10

and reduces to $$10^{-10k}$$

10

-
10
k

by repeating the verification k times.
R2U2 Version 3.0: Re-Imagining a Toolchain for Specification, Resource Estimation, and Optimized Observer Generation for Runtime Verification in Hardware and Software
Authors: Johannsen Chris , Jones Phillip , Kempa Brian , Rozier Kristin Yvonne , Zhang Pei 
Published: July 2023

AbstractR2U2 is a modular runtime verification framework capable of monitoring sets of specifications in real time and in resource-constrained environments. Such environments demand that a runtime monitor be fast, easily integratable, accessible to domain experts, and have predictable resource requirements. Version 3.0 adds new features to R2U2 and its associated suite of tools that meet these needs including a new front-end compiler that accepts a custom specification language, a GUI for resource estimation, and improvements to R2U2’s internal architecture.
Efficient Sensitivity Analysis for Parametric Robust Markov Chains
Authors: Badings Thom , Junges Sebastian , Marandi Ahmadreza , Topcu Ufuk , Jansen Nils 
Published: July 2023

AbstractWe provide a novel method for sensitivity analysis of parametric robust Markov chains. These models incorporate parameters and sets of probability distributions to alleviate the often unrealistic assumption that precise probabilities are available. We measure sensitivity in terms of partial derivatives with respect to the uncertain transition probabilities regarding measures such as the expected reward. As our main contribution, we present an efficient method to compute these partial derivatives. To scale our approach to models with thousands of parameters, we present an extension of this method that selects the subset ofkparameters with the highest partial derivative. Our methods are based on linear programming and differentiating these programs around a given value for the parameters. The experiments show the applicability of our approach on models with over a million states and thousands of parameters. Moreover, we embed the results within an iterative learning scheme that profits from having access to a dedicated sensitivity analysis.
MDPs as Distribution Transformers: Affine Invariant Synthesis for Safety Objectives
Authors: Akshay S. , Chatterjee Krishnendu , Meggendorfer Tobias , Žikelić Đorđe 
Published: July 2023

AbstractMarkov decision processes can be viewed as transformers of probability distributions. While this view is useful from a practical standpoint to reason about trajectories of distributions, basic reachability and safety problems are known to be computationally intractable (i.e., Skolem-hard) to solve in such models. Further, we show that even for simple examples of MDPs, strategies for safety objectives over distributions can require infinite memory and randomization.In light of this, we present a novel overapproximation approach to synthesize strategies in an MDP, such that a safety objective over the distributions is met. More precisely, we develop a new framework for template-based synthesis of certificates as affine distributional and inductive invariants for safety objectives in MDPs. We provide two algorithms within this framework. One can only synthesize memoryless strategies, but has relative completeness guarantees, while the other can synthesize general strategies. The runtime complexity of both algorithms is in PSPACE. We implement these algorithms and show that they can solve several non-trivial examples.
Search and Explore: Symbiotic Policy Synthesis in POMDPs
Authors: Andriushchenko Roman , Bork Alexander , Češka Milan , Junges Sebastian , Katoen Joost-Pieter , Macák Filip 
Published: July 2023

AbstractThis paper marries two state-of-the-art controller synthesis methods for partially observable Markov decision processes (POMDPs), a prominent model in sequential decision making under uncertainty. A central issue is to find a POMDP controller—that solely decides based on the observations seen so far—to achieve a total expected reward objective. As finding optimal controllers is undecidable, we concentrate on synthesising good finite-state controllers (FSCs). We do so by tightly integrating two modern, orthogonal methods for POMDP controller synthesis: a belief-based and an inductive approach. The former method obtains an FSC from a finite fragment of the so-called belief MDP, an MDP that keeps track of the probabilities of equally observable POMDP states. The latter is an inductive search technique over a set of FSCs, e.g., controllers with a fixed memory size. The key result of this paper is a symbiotic anytime algorithm that tightly integrates both approaches such that each profits from the controllers constructed by the other. Experimental results indicate a substantial improvement in the value of the controllers while significantly reducing the synthesis time and memory footprint.
AutoQ: An Automata-Based Quantum Circuit Verifier
Authors: Chen Yu-Fang , Chung Kai-Min , Lengál Ondřej , Lin Jyun-Ao , Tsai Wei-Lun 
Published: July 2023

AbstractWe present a specification language and a fully automated tool named AutoQ for verifying quantum circuits symbolically. The tool implements the automata-based algorithm from [14] and extends it with the capabilities for symbolic reasoning. The extension allows to specify relational properties, i.e., relationships between states before and after executing a circuit. We present a number of use cases where we used AutoQ to fully automatically verify crucial properties of several quantum circuits, which have, to the best of our knowledge, so far been proved only with human help.
Bounded Verification for Finite-Field-Blasting
Authors: Ozdemir Alex , Wahby Riad S. , Brown Fraser , Barrett Clark 
Published: July 2023

AbstractZero Knowledge Proofs (ZKPs) are cryptographic protocols by which a prover convinces a verifier of the truth of a statement without revealing any other information. Typically, statements are expressed in a high-level language and then compiled to a low-level representation on which the ZKP operates. Thus,a bug in a ZKP compiler can compromise the statement that the ZK proof is supposed to establish.This paper takes a step towards ZKP compiler correctness by partially verifying afield-blastingcompiler pass, a pass that translates Boolean and bit-vector logic into equivalent operations in a finite field. First, we define correctness for field-blasters and ZKP compilers more generally. Next, we describe the specific field-blaster using a set of encoding rules and define verification conditions for individual rules. Finally, we connect the rules and the correctness definition by showing that if our verification conditions hold, the field-blaster is correct. We have implemented our approach in the CirC ZKP compiler and have proved bounded versions of the corresponding verification conditions. We show that our partially verified field-blaster does not hurt the performance of the compiler or its output; we also report on four bugs uncovered during verification.
Local gradient theory of dielectrics incorporating polarization inertia and flexodynamic effect
Authors: Hrytsyna Olha , Tokovyy Yuriy , Hrytsyna Maryan 
Published: July 2023

AbstractA higher-grade theory of non-ferromagnetic thermo-elastic dielectrics which incorporates the local mass displacement, the heat flux gradient, polarization inertia, and flexodynamic effects is developed. The process of local mass displacement is associated with changes in material microstructure. Using the fundamental principles of continuum mechanics, electrodynamics, and non-equilibrium thermodynamics, the gradient-type constitutive equations are derived. Due to accounting for the polarization inertia, the rheological constitutive equation for the polarization vector is obtained. In the balance equation of linear momentum, an additional term with the second time derivative of the polarization vector appears in comparison with the classical theory. This term controls the influence of the dynamic flexoelectric effect on the mechanical motion of dielectric solids. The propagation of a plane harmonic wave is analyzed within the context of the developed theory. It is shown that the theory allows for capturing the experimentally observed phenomenon of high-frequency dispersion of a longitudinal elastic wave. The theory may be useful for modeling coupled processes in nanodielectrics and heterogeneous polarized systems.
Control of nonlinear bulk deformation and large shear strain on first-order phase transformation kinetics
Authors: Utkin Ivan , Khakimova Liudmila , Schmalholz Stefan Markus , Podladchikov Yury 
Published: July 2023

AbstractPhase transformations play a key role in numerous coupled natural processes, and they are important for many industrial applications. However, the kinetics of phase transformations in coupled chemo-mechanical systems undergoing large mechanical deformations still needs to be better quantified. Here, we study the phase transformation kinetics of a two-phase binary mixture using the diffuse interface approach. We couple a Cahn–Hilliard type model with a mechanical model for a compressible viscous flow. The bulk compressibility is a nonlinear function of the pressure, and the shear viscosity is a nonlinear function of the concentration. The mechanical coupling is achieved by employing a pressure-dependent mechanical mixing term in the equation for the Gibbs energy. We derive a dimensionless system of equations which we solve numerically with a pseudo-transient method using conservative finite differences for discretization. We perform numerical simulations in 1D and 2D model setups considering far-field simple shear and pure shear. For a chemo-mechanically coupled system, we show that the velocity of the phase boundary is a linear function of the degree of metastability and, hence, confirm the hypothesis of “normal growth.” A stronger mechanical coupling and a larger volumetric effect of the chemical reaction result in lower phase boundary velocities. The 2D results show a significant impact of the mechanical coupling and the far-field deformation on the orientation and kinetics of the phase transformations. Under far-field simple shear and pure shear in 2D, the phase transformations generate string-like patterns. The orientation of these patterns is controlled by the applied far-field deformation and orientations differ by 45 degrees between simple shear and pure shear.
Ball-end micro-milling of material measures: wear behavior in field use
Authors: Klauer-Dobrowolski Katja , Eifler Matthias , Kirsch Benjamin , Seewig Jörg , Aurich Jan C. 
Published: July 2023

AbstractMicro-milling
is a precise method for micro-structuring component surfaces. When complex or free-form structures like material measures are to be manufactured, ball-end milling tools are particularly suitable. In preliminary studies by the authors, areal material measures for the calibration of optical topography measuring instruments were manufactured via micro-milling. The demands on the surface quality of the material measures are extremely high. Therefore, worn tools must not be used if the wear has a direct effect on the resulting topography of the manufactured material measures. At the same time, the micro-milling tools used are very costly and should therefore be used as long as possible. A comprehensive experimental study was carried out on the wear behavior of different ball-end micro-milling tools for the specific use case of areal material measures. In the investigations, brass CuZn39Pb3 was machined and different areal material measures were manufactured. The tool life dependent wear was determined and critical wear was identified.
Disease activity and disease-related factors are drivers of patient global assessment in rheumatoid arthritis: a real-life cross-sectional study
Authors: Suardi Ilaria , Posio Cristina , Luconi Ester , Boracchi Patrizia , Caporali Roberto , Ingegnoli Francesca 
Published: July 2023

AbstractDespite that the Patient Global Assessment (PGA) is widely used for measuring Rheumatoid Arthritis (RA) disease activity to define the remission state of the disease, the primary contributors influencing patients’ ratings are still debated. This study aims to determine which clinical, sociodemographic and lifestyle-related contextual factors might be key drivers of PGA in RA. This single-center cross-sectional study recruited 393 consecutive adult RA patients. Median age 60 years, females 306 (77.9%). Data related to disease activity were assessed by using Simplified Disease Activity Index (SDAI), severity by Health Assessment Questionnaire (HAQ), and impact by RA Impact of Disease (RAID). Sociodemographic/lifestyle features were collected. Disease remission was calculated using Boolean-based criteria 1.0 and 2.0. Quantile regression models were used for univariate and multivariate analysis. The remission rate progressively increased from 15% by using SDAI with a Boolean 1.0-based definition to 43.5% using a Boolean 2.0-based remission. Among factors related to disease activity, the use of low-dose corticosteroids, the RAID items pain and sleep difficulties were predictive for worse PGA scores (p = 0.01). Among factors related to disease severity HAQ score and RAID total were independent factors associated with higher median PGA (p = 0.02 and p < 0.001). RAID’s physical well-being was related to PGA scores (p = 0.01). An increasing trend in PGA was observed in longstanding diseases (> 15 years). Our results confirmed that there is no unambiguous interpretation of the PGA score. It is a measure related to some disease activity parameters, but it is also influenced by contextual factors related to disease severity and impact. These data highlighted that PGA should have a broad interpretation, thus supporting the proposal of a dual targets (biological and impact) approach to obtain a more accurate estimate of disease activity.
Magnetic Resonance Velocimetry for porous media: sources and reduction of measurement errors for improved accuracy
Authors: Ricke Adrian , Sadeghi Mehrdad , Dreher Wolfgang 
Published: July 2023

AbstractNuclear Magnetic Resonance (NMR) is a powerful tool for noninvasively investigating static and dynamic properties of fluids inside complex and opaque structures. Thus, Magnetic Resonance Velocimetry (MRV) allows for the in situ analysis of the local flow velocity of fluids. Such an analysis characterises mass transport properties and helps to validate or improve numerical predictions for porous media. The benefit of such validations is lowered by several problems worsening the measurement accuracy. This publication addresses systematic errors and the influence of noise, which may reduce the accuracy of MRV measurements. Techniques are described to minimise or correct displacement and phase errors. A new multi-echo MRV-sequence is proposed as a compromise between Velocity-to-Noise Ratio (VNR), total measurement time, spatial resolution and displacement errors. For improved VNR, a dual-VENC encoding scheme was used and repetition time $$T_{\text{R}}$$

T
R

was optimised. As an example, the proposed MRV sequence was used to measure the three-directional flow velocity of water in an Open Cell Foam (OCF) with 10 pores per inch with three-dimensional isotropic spatial resolution.