bluuebunny/crossref_metadata_2025_split huggingface dataset:
A physics‐informed machine learning prediction for thermal analysis in a convective‐radiative concave fin with periodic boundary conditions
Authors: Kumar Chandan , Srilatha Pudhari , Karthik Kalachar , Somashekar Channaiah , Nagaraja Kallur Venkat , Varun Kumar Ravikumar Shashikala , Shah Nehad Ali 
Published: April 2024

AbstractThe present research is focused on the inspection of unsteady heat dissipation through a radiative‐convective concave profiled fin along with the periodic boundary conditions. Additionally, the long‐short‐term memory machine learning (LSTM‐ML) approach is used in this study to examine the periodic fluctuation in the temperature of the fin. The current research is devoted to solving the highly non‐linear equation using a physics‐informed neural network (PINN) approach. Using the proper dimensionless terms, the associated fin problem is transformed into a non‐dimensional system, and the resulting partial differential equation (PDE) is then numerically solved using the finite difference method (FDM). Using the data‐driven LSTM‐ML technique, the time‐dependent periodic heat transmission in the concave fin is also examined. The impact of various factors on the temperature profile of the concave extended surface is explained, and the results are visually displayed. The temperature distribution in the concave fin diminishes as the convection‐conduction parameter and radiation‐conduction parameter rise. As the amplitude and thermal conductivity parameters improve, so does the temperature of the concave fin. Furthermore, it is demonstrated that although LSTM‐ML and PINN closely matched the FDM findings during the training domain, only PINN with designed characteristics has the potential to predict accurately beyond the trained region by capturing the physics of the problem.
Stochastic Window Mean-Payoff Games
Authors: Doyen Laurent , Gaba Pranshu , Guha Shibashis 
Published: April 2024

AbstractStochastic two-player games model systems with an environment that is both adversarial and stochastic. The environment is modeled by a player ($$\text {Player}~{2}$$Player2) who tries to prevent the system ($$\text {Player}~{1}$$Player1) from achieving its objective. We consider finitary versions of the traditional mean-payoff objective, replacing the long-run average of the payoffs by payoff average computed over a finite sliding window. Two variants have been considered: in one variant, the maximum window length is fixed and given, while in the other, it is not fixed but is required to be bounded. For both variants, we present complexity bounds and algorithmic solutions for computing strategies for$$\text {Player}~{1}$$Player1to ensure that the objective is satisfied with positive probability, with probability 1, or with probability at least p, regardless of the strategy of$$\text {Player}~{2}$$Player2. The solution crucially relies on a reduction to the special case of non-stochastic two-player games. We give a general characterization of prefix-independent objectives for which this reduction holds. The memory requirement for both players in stochastic games is also the same as in non-stochastic games by our reduction. Moreover, for non-stochastic games, we improve upon the upper bound for the memory requirement of$$\text {Player}~{1}$$Player1and upon the lower bound for the memory requirement of$$\text {Player}~{2}$$Player2.
Parity Games on Temporal Graphs
Authors: Austin Pete , Bose Sougata , Totzke Patrick 
Published: April 2024

AbstractTemporal graphs are a popular modelling mechanism for dynamic complex systems that extend ordinary graphs with discrete time. Simply put, time progresses one unit per step and the availability of edges can change with time.We consider the complexity of solving$$\omega $$ω-regular games played on temporal graphs where the edge availability is ultimately periodic and fixed a priori.We show that solving parity games on temporal graphs is decidable in$$\textsf{PSPACE}$$PSPACE, only assuming the edge predicate itself is in$$\textsf{PSPACE}$$PSPACE. A matching lower bound already holds for what we callpunctualreachability games on static graphs, where one player wants to reach the target at a given, binary encoded, point in time. We further study syntactic restrictions that imply more efficient procedures. In particular, if the edge predicate is in and is monotonically increasing for one player and decreasing for the other, then the complexity of solving games is only polynomially increased compared to static graphs.
Pareto Curves for Compositionally Model Checking String Diagrams of MDPs
Authors: Watanabe Kazuki , van der Vegt Marck , Hasuo Ichiro , Rot Jurriaan , Junges Sebastian 
Published: April 2024

AbstractComputing schedulers that optimize reachability probabilities in MDPs is a standard verification task. To address scalability concerns, we focus on MDPs that are compositionally described in a high-level description formalism. In particular, this paper considersstring diagrams, which specify an algebraic, sequential composition of subMDPs. Towards their compositional verification, the key challenge is to locally optimize schedulers on subMDPs without considering their context in the string diagram. This paper proposes to consider the schedulers in a subMDP which form aPareto curveon a combination of local objectives. While considering all such schedulers is intractable, it gives rise to a highly efficient sound approximation algorithm. The prototype on top of the model checker Storm demonstrates the scalability of this approach.
Learning Explainable and Better Performing Representations of POMDP Strategies
Authors: Bork Alexander , Chakraborty Debraj , Grover Kush , Křetínský Jan , Mohr Stefanie 
Published: April 2024

AbstractStrategies for partially observable Markov decision processes (POMDP) typically require memory. One way to represent this memory is via automata. We present a method to learn an automaton representation of a strategy using a modification of the $$L^*$$

L
∗

-algorithm. Compared to the tabular representation of a strategy, the resulting automaton is dramatically smaller and thus also more explainable. Moreover, in the learning process, our heuristics may even improve the strategy’s performance. We compare our approach to an existing approach that synthesizes an automaton directly from the POMDP, thereby solving it. Our experiments show that our approach can lead to significant improvements in the size and quality of the resulting strategy representations.
Forward and Backward Constrained Bisimulations for Quantum Circuits
Authors: Jiménez-Pastor A. , Larsen K. G. , Tribastone M. , Tschaikowski M. 
Published: April 2024

AbstractEfficient methods for the simulation of quantum circuits on classic computers are crucial for their analysis due to the exponential growth of the problem size with the number of qubits. Here we study lumping methods based on bisimulation, an established class of techniques that has been proven successful for (classic) stochastic and deterministic systems such as Markov chains and ordinary differential equations. Forward constrained bisimulation yields a lower-dimensional model which exactly preserves quantum measurements projected on a linear subspace of interest. Backward constrained bisimulation gives a reduction that is valid on a subspace containing the circuit input, from which the circuit result can be fully recovered. We provide an algorithm to compute the constraint bisimulations yielding coarsest reductions in both cases, using a duality result relating the two notions. As applications, we provide theoretical bounds on the size of the reduced state space for well-known quantum algorithms for search, optimization, and factorization. Using a prototype implementation, we report significant reductions on a set of benchmarks. Furthermore, we show that constraint bisimulation complements state-of-the-art methods for the simulation of quantum circuits based on decision diagrams.
Enhancing GenMC’s Usability and Performance
Authors: Kokologiannakis Michalis , Majumdar Rupak , Vafeiadis Viktor 
Published: April 2024

AbstractGenMC is a state-of-the-art stateless model checker that can verify safety properties of concurrent C/C++ programs under a wide range of memory consistency models, such as SC, TSO, RC11, and IMM.In this paper, we improve the performance and usability of GenMC: we provide a probabilistic estimate of the expected verification cost, we automate the porting of new memory models, and employ caching and other data structure optimizations to improve the tool’s performance.
Provable Preimage Under-Approximation for Neural Networks
Authors: Zhang Xiyue , Wang Benjie , Kwiatkowska Marta 
Published: April 2024

AbstractNeural network verification mainly focuses on local robustness properties, which can be checked by bounding the image (set of outputs) of a given input set. However, often it is important to know whether a given property holds globally for the input domain, and if not then for what proportion of the input the property is true. To analyze such properties requires computing preimage abstractions of neural networks. In this work, we propose an efficient anytime algorithm for generating symbolic under-approximations of the preimage of any polyhedron output set for neural networks. Our algorithm combines a novel technique for cheaply computing polytope preimage under-approximations using linear relaxation, with a carefully-designed refinement procedure that iteratively partitions the input region into subregions using input and ReLU splitting in order to improve the approximation. Empirically, we validate the efficacy of our method across a range of domains, including a high-dimensional MNIST classification task beyond the reach of existing preimage computation methods. Finally, as use cases, we showcase the application to quantitative verification and robustness analysis. We present a sound and complete algorithm for the former, which exploits our disjoint union of polytopes representation to provide formal guarantees. For the latter, we find that our method can provide useful quantitative information even when standard verifiers cannot verify a robustness property.
OxiDD
Authors: Husung Nils , Dubslaff Clemens , Hermanns Holger , Köhl Maximilian A. 
Published: April 2024

AbstractDecision diagrams (DDs) are an important data structure in computer science with applications ranging from circuit design and verification to machine learning. Most prominently, binary DDs are commonly used to succinctly represent Boolean functions. Due to the practical importance of DDs, there is an ongoing quest for high-performance software libraries supporting the construction and manipulation of DDs. With OxiDD, we present a new framework for DDs that focuses on safety, concurrency, and modularity. Following a highly modular design we implement OxiDD in Rust, which facilitates the integration of various kinds of DDs such as MTBDDs, ZBDDs, and TDDs, all within safe code also in a concurrent setting. Already in its initial release, OxiDD does not compromise performance, which we show to be on par with or even better than established highly optimized DD libraries.
State of the Art in Software Verification and Witness Validation: SV-COMP 2024
Authors: Beyer Dirk 
Published: April 2024

AbstractThe 13th edition of the Competition on Software Verification (SV-COMP 2024) was the largest competition of its kind so far: A total of 76 tools for verification and witness validation were compared. The competition evaluated 59 verification systems and 17 validation systems from 34 teams from 12 countries. This yields a good overview of the state of the art in tools for software verification. The competition was executed on a benchmark set with 30 300 verification tasks for C programs and 587 . verification tasks for Java programs. The specifications again included reachability, memory safety, overflows, and termination. This year was the second time that the competition had an extra competition track on witness validation. We introduced a new witness format 2.0, and a new scoring schema for the validation track. All meta data about the verification and validation tools are available in the FM-Tools repository.
EmergenTheta: Verification Beyond Abstraction Refinement (Competition Contribution)
Authors: Bajczi Levente , Szekeres Dániel , Mondok Milán , Ádám Zsófia , Somorjai Márk , Telbisz Csanád , Dobos-Kovács Mihály , Molnár Vince 
Published: April 2024

AbstractThetais a model checking framework conventionally based on abstraction refinement techniques. While abstraction is useful for a large number of verification problems, the over-reliance on the technique led toThetabeing unable to meaningfully adapt. Identifying this problem in previous years of SV-COMP has led us to createEmergenTheta, a sandbox for the new approaches we wantThetato support. By differentiating between mature and emerging techniques, we can experiment more freely without hurting the reliability of the overall framework. In this paper we detail the development route toEmergenTheta, and its first debut on SV-COMP’24 in the ReachSafety category.
Mopsa-C: Improved Verification for C Programs, Simple Validation of Correctness Witnesses (Competition Contribution)
Authors: Monat Raphaël , Milanese Marco , Parolini Francesco , Boillot Jérôme , Ouadjaout Abdelraouf , Miné Antoine 
Published: April 2024

AbstractWe present advances we brought to Mopsa for SV-Comp 2024. We significantly improved the precision of our verifier in the presence of dynamic memory allocation, library calls such as , -based loops, and integer abstractions. We introduced a witness validator for correctness witnesses. Thanks to these improvements, Mopsa won SV-Comp’sSoftwareSystemscategory by a large margin, scoring 2.5 times more points than the silver medalist, Bubaak-SpLit.
Ultimate Automizer and the Abstraction of Bitwise Operations
Authors: Schüssele Frank , Bentele Manuel , Dietsch Daniel , Heizmann Matthias , Jiang Xinyu , Klumpp Dominik , Podelski Andreas 
Published: April 2024

AbstractThe verification ofUltimate Automizerworks on an SMT-LIB-based model of a C program. If we choose an SMT-LIB theory of (mathematical) integers, the translation is not precise, because we overapproximate bitwise operations. In this paper we present a translation for bitwise operations that improves the precision of this overapproximation.
$${\textsc {HaliVer}}$$: Deductive Verification and Scheduling Languages Join Forces
Authors: van den Haak Lars B. , Wijs Anton , Huisman Marieke , van den Brand Mark 
Published: April 2024

AbstractThe HaliVer tool integrates deductive verification into the popular scheduling language Halide, used for image processing pipelines and array computations. HaliVer uses VerCors, a separation logic-based verifier, to verify the correctness of (1) the Halide algorithms and (2) the optimised parallel code produced by Halide when an optimisation schedule is applied to an algorithm. This allows proving complex, optimised code correct while reducing the effort to provide the required verification annotations. For both approaches, the same specification is used. We evaluated the tool on several optimised programs generated from characteristic Halide algorithms, using all but one of the essential scheduling directives available in Halide. Without annotation effort, HaliVer proves memory safety in almost all programs. With annotations HaliVer, additionally, proves functional correctness properties. We show that the approach is viable and reduces the manual annotation effort by an order of magnitude.
Most General Winning Secure Equilibria Synthesis in Graph Games
Authors: Nayak Satya Prakash , Schmuck Anne-Kathrin 
Published: April 2024

AbstractThis paper considers the problem of co-synthesis in k-player games over a finite graph where each player has an individual $$\omega $$
ω
-regular specification $$\phi _i$$

ϕ
i

. In this context, a secure equilibrium (SE) is a Nash equilibrium w.r.t. the lexicographically ordered objectives of each player to first satisfy their own specification, and second, to falsify other players’ specifications. A winning secure equilibrium (WSE) is an SE strategy profile $$(\pi _i)_{i\in [1;k]}$$

(

π
i

)

i
∈
[
1
;
k
]

that ensures the specification $$\phi :=\bigwedge _{i\in [1;k]}\phi _i$$

ϕ
:
=

⋀

i
∈
[
1
;
k
]

ϕ
i

if no player deviates from their strategy $$\pi _i$$

π
i

. Distributed implementations generated from a WSE make components act rationally by ensuring that a deviation from the WSE strategy profile is immediately punished by a retaliating strategy that makes the involved players lose.In this paper, we move from deviation punishment in WSE-based implementations to a distributed, assume-guarantee based realization of WSE. This shift is obtained by generalizing WSE from strategy profiles to specification profiles$$(\varphi _i)_{i\in [1;k]}$$

(

φ
i

)

i
∈
[
1
;
k
]

with $$\bigwedge _{i\in [1;k]}\varphi _i = \phi $$

⋀

i
∈
[
1
;
k
]

φ
i

=
ϕ

, which we call most general winning secure equilibria (GWSE). Such GWSE have the property that each player can individually pick a strategy $$\pi _i$$

π
i

winning for $$\varphi _i$$

φ
i

(against all other players) and all resulting strategy profiles $$(\pi _i)_{i\in [1;k]}$$

(

π
i

)

i
∈
[
1
;
k
]

are guaranteed to be a WSE. The obtained flexibility in players’ strategy choices can be utilized for robustness and adaptability of local implementations.Concretely, our contribution is three-fold: (1) we formalize GWSE for k-player games over finite graphs, where each player has an $$\omega $$
ω
-regular specification $$\phi _i$$

ϕ
i

; (2) we devise an iterative semi-algorithm for GWSE synthesis in such games, and (3) obtain an exponential-time algorithm for GWSE synthesis with parity specifications $$\phi _i$$

ϕ
i

.
Scoped Effects as Parameterized Algebraic Theories
Authors: Lindley Sam , Matache Cristina , Moss Sean , Staton Sam , Wu Nicolas , Yang Zhixuan 
Published: April 2024

AbstractNotions of computation can be modelled by monads. Algebraic effects offer a characterization of monads in terms of algebraic operations and equational axioms, where operations are basic programming features, such as reading or updating the state, and axioms specify observably equivalent expressions. However, many useful programming features depend on additional mechanisms such as delimited scopes or dynamically allocated resources. Such mechanisms can be supported via extensions to algebraic effects including scoped effects and parameterized algebraic theories. We present a fresh perspective on scoped effects by translation into a variation of parameterized algebraic theories. The translation enables a new approach to equational reasoning for scoped effects and gives rise to an alternative characterization of monads in terms of generators and equations involving both scoped and algebraic operations. We demonstrate the power of our fresh perspective by way of equational characterizations of several known models of scoped effects.
The Session Abstract Machine
Authors: Caires Luís , Toninho Bernardo 
Published: April 2024

AbstractWe build on a fine-grained analysis of session-based interaction as provided by the linear logic typing disciplines to introduce the SAM, an abstract machine for mechanically executing session-typed processes. A remarkable feature of the SAM’s design is its ability to naturally segregate and coordinate sequential with concurrent session behaviours. In particular, implicitly sequential parts of session programs may be efficiently executed by deterministic sequential application of SAM transitions, amenable to compilation, and without concurrent synchronisation mechanisms. We provide an intuitive discussion of the SAM structure and its underlying design, and state and prove its correctness for executing programs in a session calculus corresponding to full classical linear logic$$\textsf{CLL}$$CLL. We also discuss extensions and applications of the SAM to the execution of linear and session-based programming languages.
Specifying and Verifying Persistent Libraries
Authors: Stefanesco Léo , Raad Azalea , Vafeiadis Viktor 
Published: April 2024

AbstractWe present a general framework for specifying and verifying persistent libraries, that is, libraries of data structures that provide some persistency guarantees upon a failure of the machine they are executing on. Our framework enables modular reasoning about the correctness of individual libraries (horizontal and vertical compositionality) and is general enough to encompass all existing persistent library specifications ranging from hardware architectural specifications to correctness conditions such as durable linearizability. As case studies, we specify the and libraries, verify their implementations over "Image missing", and use them to build higher-level durably linearizable libraries, all within our framework. We also specify and verify a persistent transaction library that highlights some of the technical challenges which are specific to persistent memory compared to weak memory and how they are handled by our framework.
Hyperproperty Verification as CHC Satisfiability
Authors: Itzhaky Shachar , Shoham Sharon , Vizel Yakir 
Published: April 2024

AbstractHyperproperties specify the behavior of a system across multiple executions, and are an important extension of regular temporal properties. So far, such properties have resisted comprehensive treatment by software model-checking approaches such as IC3/PDR, due to the need to find not only an inductive invariant but also a total alignment of different executions that facilitates simpler inductive invariants.We show how this treatment is achieved via a reduction from the verification problem of $$\forall ^*\exists ^*$$

∀
∗

∃
∗

hyperproperties to Constrained Horn Clauses (CHCs). Our starting point is a set of universally quantified formulas in first-order logic (modulo theories) that encode the verification of $$\forall ^*\exists ^*$$

∀
∗

∃
∗

hyperproperties over infinite-state transition systems. The first-order encoding uses uninterpreted predicates to capture the (1) witness function for existential quantification over traces, (2) alignment of executions, and (3) corresponding inductive invariant. Such an encoding was previously proposed for k-safety properties. Unfortunately, finding a satisfying model for the resulting first-order formulas is beyond reach for modern first-order satisfiability solvers. Previous works tackled this obstacle by developing specialized solvers for the aforementioned first-order formulas. In contrast, we show that the same problems can be encoded as CHCs and solved by existing CHC solvers. CHC solvers take advantage of the unique structure of CHC formulas and handle the combination of quantifiers with theories and uninterpreted predicates more efficiently.Our key technical contribution is a logical transformation of the aforementioned sets of first-order formulas to equi-satisfiable sets of CHCs. The transformation to CHCs is sound and complete, and applying it to the first-order formulas that encode verification of hyperproperties leads to a CHC encoding of these problems. We implemented the CHC encoding in a prototype tool and show that, using existing CHC solvers for solving the CHCs, the approach already outperforms state-of-the-art tools for hyperproperty verification by orders of magnitude.