bluuebunny/crossref_metadata_2025_split huggingface dataset:
State of the Art of Sustainable Development of Railway Nodes: The High Speed Rail (HSR)
Authors: Panuccio Paola 
Published: July 2024

AbstractHigh Speed Rail (HSR) is a new mode of transport and has a significant impact on the territory. The urban plan, in respect of the technical standards set by the rules, does not provide any indication for the inclusion of an important node in the territory, such as a station of an HSR line. Even the Sustainable Urban Mobility Plans (SUMPs) designed for metropolitan areas, in their strategic choices, often do not give indications on the HSR. It therefore happens that the territories are distorted by the effects caused by the location of such an important infrastructural node. Furthermore, the stations of the HSR are designed by “archi-star” architects who give a significant formal and visual mark on the territory. The paper underlines the importance of HSR through the analysis of two case studies, the effects that HSR cause on the territory. The first case of the Mediopadana High Speed Rail station in Reggio Emilia analyses the impact caused on a moderately anthropized territory. The second case of the High Speed Rail station of Naples Afragola analyses the impact caused on a highly anthropized territory. The analysis of these two projects concludes with considerations regarding the opportunity of an integrated urban and transport planning.
The MoXI Model Exchange Tool Suite
Authors: Johannsen Chris , Nukala Karthik , Dureja Rohit , Irfan Ahmed , Shankar Natarajan , Tinelli Cesare , Vardi Moshe Y. , Rozier Kristin Yvonne 
Published: July 2024

AbstractWe release the first tool suite implementingMoXI(Model eXchange Interlingua), an intermediate language for symbolic model checking designed to be an international research-community standard and developed by a widespread collaboration under a National Science Foundation (NSF) CISE Community Research Infrastructure initiative. Although we focus here on hardware verification, theMoXIlanguage is useful for software model checking and verification of infinite-state systems in general.MoXIbuilds on elements of SMT-LIB 2; it is easy to add new theories and operators. Our contributions include: (1) introducing the first tool suite of automated translators into and out of the new model-checking intermediate language; (2) composing an initial example benchmark set enabling the model-checking research community to build future translations; (3) compiling details for utilizing, extending, and improving upon our tool suite, including usage characteristics and initial performance data. Experimental evaluations demonstrate that compiling SMV-language models throughMoXIto perform symbolic model checking with the tools from the last Hardware Model Checking Competition performs competitively with model checking directly vianuXmv.
End-to-End Mechanized Proof of a JIT-Accelerated eBPF Virtual Machine for IoT
Authors: Yuan Shenghao , Besson Frédéric , Talpin Jean-Pierre 
Published: July 2024

AbstractModern operating systems have adopted Berkeley Packet Filters (BPF) as a mechanism to extend kernel functionalities dynamically, e.g., Linux’s eBPF or RIOT’s rBPF. The just-in-time (JIT) compilation of eBPF introduced in Linux eBPF for performance has however led to numerous critical issues. Instead, RIOT’s rBPF uses a slower but memory-isolating interpreter (a virtual machine) which implements a defensive semantics of BPF; and therefore trades performance for security. To increase performance without sacrificing security, this paper presents a fully verified JIT implementation for RIOT’s rBPF, consisting of: i/ an end-to-end refinement workflow to both proving the JIT correct from an abstract specification and by deriving a verified concrete C implementation; ii/ a symbolic CompCert interpreter for executing binary code; iii/ a verified JIT compiler for rBPF; iv/ a verified hybrid rBPF virtual machine. Our core contribution is, to the best of our knowledge, the first and fully verified rBPF JIT compiler with correctness guarantees from high-level specification to low-level implementation. Benchmarks on microcontrollers hosting the RIOT operating system demonstrate significant performance improvements over the existing implementations of rBPF, even in worst-case application scenarios.
A Framework for Debugging Automated Program Verification Proofs via Proof Actions
Authors: Cho Chanhee , Zhou Yi , Bosamiya Jay , Parno Bryan 
Published: July 2024

AbstractMany program verification tools provide automation via SMT solvers, allowing them to automatically discharge many proofs. However, when a proof fails, it can be hard to understand why it failed or how to fix it. The main feedback the developer receives is simply the verification result (i.e., success or failure), with no visibility into the solver’s internal state. To assist developers using such tools, we introduce ProofPlumber, a novel and extensible proof-action framework for understanding and debugging proof failures. Proof actions act on the developer’s source-level proofs (e.g., assertions and lemmas) to determine why they failed and potentially suggest remedies. We evaluate ProofPlumber by writing a collection of proof actions that capture common proof debugging practices. We produce 17 proof actions, each only 29–177 lines of code.
SMT-Based Symbolic Model-Checking for Operator Precedence Languages
Authors: Chiari Michele , Geatti Luca , Gigante Nicola , Pradella Matteo 
Published: July 2024

AbstractOperator Precedence Languages (OPL) have been recently identified as a suitable formalism for model checking recursive procedural programs, thanks to their ability of modeling the program stack. OPL requirements can be expressed in thePrecedence Oriented Temporal Logic(), which features modalities to reason on the natural matching between function calls and returns, exceptions, and other advanced programming constructs that previous approaches, such as Visibly Pushdown Languages, cannot model effectively. Existing approaches for model checking of have been designed following the explicit-state, automata-based approach, a feature that severely limits their scalability. In this paper, we give the first symbolic, SMT-based approach for model checking properties. While previous approaches construct the automaton for both the formula and the model of the program, we encode them into a (sequence of) SMT formulas. The search of a trace of the model witnessing a violation of the formula is then carried out by an SMT-solver, in a Bounded Model Checking fashion. We carried out an experimental evaluation, which shows the effectiveness of the proposed solution.
On Polynomial Expressions with C-Finite Recurrences in Loops with Nested Nondeterministic Branches
Authors: Wang Chenglin , Lin Fangzhen 
Published: July 2024

AbstractLoops are inductive constructs, which make them difficult to analyze and verify in general. One approach is to represent the inductive behaviors of the program variables in a loop by recurrences and try to solve them for closed-form solutions. These solutions can then be used to generate invariants or directly fed into an SMT-based verifier. One problem with this approach is that if a loop contains nondeterministic choices or complex operations such as non-linear assignments, then recurrences for program variables may not exist or may have no closed-form solutions. In such cases, an alternative is to generate recurrences for expressions, and there has been recent work along this line. In this paper, we further work in this direction and propose a template-based method for extracting polynomial expressions that satisfy some c-finite recurrences. While in general there are possibly infinitely many such polynomials for a given loop, we show that the desired polynomials form a finite union of vector spaces. We propose an algorithm for computing the bases of the vector spaces, and identify two cases where the bases can be computed efficiently. To demonstrate the usefulness of our results, we implemented a prototype system based on one of the special cases, and integrated it into an SMT-based verifier. Our experimental results show that the new verifier can now verify programs with non-linear properties.
Hevm, a Fast Symbolic Execution Framework for EVM Bytecode
Authors: Dxo  , Soos Mate , Paraskevopoulou Zoe , Lundfall Martin , Brockman Mikael 
Published: July 2024

AbstractWe present , a symbolic execution engine for the EVM. can prove safety properties for EVM bytecode or verify semantic equivalence between two bytecode objects. It exposes a user-friendly API in Solidity that allows end-users to define symbolic tests using almost the same syntax as they would for their usual unit tests. We evaluate our framework against state-of-the-art tools, using a comprehensive set of benchmarks. Our empirical findings demonstrate that outperforms its counterparts, effectively solving a greater number of problems within competitive time frames.
SolTG: A CHC-Based Solidity Test Case Generator
Authors: Britikov Konstantin , Zlatkin Ilia , Fedyukovich Grigory , Alt Leonardo , Sharygina Natasha 
Published: July 2024

AbstractAchieving high test coverage is important when developing blockchain smart contracts, but it could be challenging without automated reasoning tools. In this paper, we present SolTG, an automated test case generator for Solidity based on constrained Horn clauses (CHC). SolTG exhaustively enumerates symbolic path constraints from the contract’s CHC representation and makes calls to the Satisfiability Modulo Theories (SMT) solver to find input values under which the contract exhibits the corresponding behavior. Test cases synthesized by SolTG have the form of a sequence of function calls over concrete values of input parameters which lead to a specific execution scenario. The tool supports multiple Solidity-specific features and is capable of exhibiting a high coverage for industrial-grade Solidity code. We present a detailed architecture of SolTG based on the existing translation of smart contracts into a CHC representation. We also present the experimental results for test generation on the regression and industrial benchmarks.
Distributed SMT Solving Based on Dynamic Variable-Level Partitioning
Authors: Zhao Mengyu , Cai Shaowei , Qian Yuhang 
Published: July 2024

AbstractSatisfiability Modulo Theories on arithmetic theories have significant applications in many important domains. Previous efforts have been mainly devoted to improving the techniques and heuristics in sequential SMT solvers. With the development of computing resources, a promising direction to boost performance is parallel and even distributed SMT solving. We explore this potential in a divide-and-conquer view and propose a novel dynamic parallel framework with variable-level partitioning. To the best of our knowledge, this is the first attempt to perform variable-level partitioning for arithmetic theories. Moreover, we enhance the interval constraint propagation algorithm, coordinate it with Boolean propagation, and integrate it into our variable-level partitioning strategy. Our partitioning algorithm effectively capitalizes on propagation information, enabling efficient formula simplification and search space pruning. We apply our method to three state-of-the-art SMT solvers, namely CVC5, OpenSMT2, and Z3, resulting in efficient parallel SMT solvers. Experiments are carried out on benchmarks of linear and non-linear arithmetic over both real and integer variables, and our variable-level partitioning method shows substantial improvements over previous partitioning strategies and is particularly good at non-linear theories.
Quantified Linear Arithmetic Satisfiability via Fine-Grained Strategy Improvement
Authors: Murphy Charlie , Kincaid Zachary 
Published: July 2024

AbstractChecking satisfiability of formulae in the theory of linear arithmetic has far reaching applications, including program verification and synthesis. Many satisfiability solvers excel at proving and disproving satisfiability of quantifier-free linear arithmetic formulas and have recently begun to support quantified formulas. Beyond simply checking satisfiability of formulas, fine-grained strategies for satisfiability games enables solving additional program verification and synthesis tasks. Quantified satisfiability games are played between two players—SAT and UNSAT—who take turns instantiating quantifiers and choosing branches of boolean connectives to evaluate the given formula. A winning strategy for SAT (resp. UNSAT) determines the choices of SAT (resp. UNSAT) as a function of UNSAT ’s (resp. SAT ’s) choices such that the given formula evaluates to true (resp. false) no matter what choices UNSAT (resp. SAT) may make. As we are interested in both checking satisfiability and synthesizing winning strategies, we must avoid conversion to normal-forms that alter the game semantics of the formula (e.g. prenex normal form). We present fine-grained strategy improvement and strategy synthesis, the first technique capable of synthesizing winning fine-grained strategies for linear arithmetic satisfiability games, which may be used in higher-level applications. We experimentally evaluate our technique and find it performs favorably compared with state-of-the-art solvers.
Formally Certified Approximate Model Counting
Authors: Tan Yong Kiam , Yang Jiong , Soos Mate , Myreen Magnus O. , Meel Kuldeep S. 
Published: July 2024

AbstractApproximate model counting is the task of approximating the number of solutions to an input Boolean formula. The state-of-the-art approximate model counter for formulas in conjunctive normal form (CNF), $$\textsf{ApproxMC}$$
ApproxMC
, provides a scalable means of obtaining model counts with probably approximately correct (PAC)-style guarantees. Nevertheless, the validity of $$\textsf{ApproxMC}$$
ApproxMC
’s approximation relies on a careful theoretical analysis of its randomized algorithm and the correctness of its highly optimized implementation, especially the latter’s stateful interactions with an incremental CNF satisfiability solver capable of natively handling parity (XOR) constraints.We present the first certification framework for approximate model counting with formally verified guarantees on the quality of its output approximation. Our approach combines: (i) a static, once-off, formal proof of the algorithm’s PAC guarantee in the Isabelle/HOL proof assistant; and (ii) dynamic, per-run, verification of $$\textsf{ApproxMC}$$
ApproxMC
’s calls to an external CNF-XOR solver using proof certificates. We detail our general approach to establish a rigorous connection between these two parts of the verification, including our blueprint for turning the formalized, randomized algorithm into a verified proof checker, and our design of proof certificates for both $$\textsf{ApproxMC}$$
ApproxMC
and its internal CNF-XOR solving steps. Experimentally, we show that certificate generation adds little overhead to an approximate counter implementation, and that our certificate checker is able to fully certify $$84.7\%$$

84.7
%

of instances with generated certificates when given the same time and memory limits as the counter.
LTL Learning on GPUs
Authors: Valizadeh Mojtaba , Fijalkow Nathanaël , Berger Martin 
Published: July 2024

AbstractLinear temporal logic (LTL) is widely used in industrial verification. LTL formulae can be learned from traces. Scaling LTL formula learning is an open problem. We implement the first GPU-based LTL learner using a novel form of enumerative program synthesis. The learner is sound and complete. Our benchmarks indicate that it handles traces at least 2048 times more numerous, and on average at least 46 times faster than existing state-of-the-art learners. This is achieved with, among others, a branch-free implementation of LTL that has $$O(\log n)$$

O
(
log
n
)

time complexity, where n is trace length, while previous implementations are $$O(n^2)$$

O
(

n
2

)

or worse (assuming bitwise boolean operations and shifts by powers of 2 have unit costs—a realistic assumption on modern processors).
Optimization-Based Model Checking and Trace Synthesis for Complex STL Specifications
Authors: Sato Sota , An Jie , Zhang Zhenya , Hasuo Ichiro 
Published: July 2024

AbstractTechniques of light-weight formal methods, such as monitoring and falsification, are attracting attention for quality assurance of cyber-physical systems. The techniques require formal specs, however, and writing right specs is still a practical challenge. Commonly one relies ontrace synthesis—i.e. automatic generation of a signal that satisfies a given spec—to examine the meaning of a spec. In this work, motivated by 1) complex STL specs from an automotive safety standard and 2) the struggle of existing tools in their trace synthesis, we introduce a novel trace synthesis algorithm for STL specs. It combines the use of MILP (inspired by works on controller synthesis) and avariable-interval encodingof STL semantics (previously studied for SMT-based STL model checking). The algorithm solves model checking, too, as the dual of trace synthesis. Our experiments show that only ours has realistic performance needed for the interactive examination of STL specs by trace synthesis.
Inner-Approximate Reachability Computation via Zonotopic Boundary Analysis
Authors: Ren Dejin , Liang Zhen , Wu Chenyu , Ding Jianqiang , Wu Taoran , Xue Bai 
Published: July 2024

AbstractInner-approximate reachability analysis involves calculating subsets of reachable sets, known as inner-approximations. This analysis is crucial in the fields of dynamic systems analysis and control theory as it provides a reliable estimation of the set of states that a system can reach from given initial states at a specific time instant. In this paper, we study the inner-approximate reachability analysis problem based on the set-boundary reachability method for systems modelled by ordinary differential equations, in which the computed inner-approximations are represented with zonotopes. The set-boundary reachability method computes an inner-approximation by excluding states reached from the initial set’s boundary. The effectiveness of this method is highly dependent on the efficient extraction of the exact boundary of the initial set. To address this, we propose methods leveraging boundary and tiling matrices that can efficiently extract and refine the exact boundary of the initial set represented by zonotopes. Additionally, we enhance the exclusion strategy by contracting the outer-approximations in a flexible way, which allows for the computation of less conservative inner-approximations. To evaluate the proposed method, we compare it with state-of-the-art methods against a series of benchmarks. The numerical results demonstrate that our method is not only efficient but also accurate in computing inner-approximations.
Scenario-Based Flexible Modeling and Scalable Falsification for Reconfigurable CPSs
Authors: Wang Jiawan , Liu Wenxia , Zhang Muzimiao , Wei Jiaqi , Shi Yuhui , Bu Lei , Li Xuandong 
Published: July 2024

AbstractCyber-physical systems (CPSs) are used in many safety-critical areas, making it crucial to ensure their safety. However, with CPSs increasingly dynamically deployed and reconfigured during runtime, their safety analysis becomes challenging. For one thing, reconfigurable CPSs usually consist of multiple agents dynamically connected during runtime. Their highly dynamic system topologies are too intricate for traditional modeling languages, which, in turn, hinders formal analysis. For another, due to the growing size and uncertainty of reconfigurable CPSs, their system models can be huge and even unavailable at design time. This calls for runtime analysis approaches with better scalability and efficiency. To address these challenges, we propose a scenario-based hierarchical modeling language for reconfigurable CPS. It provides template models for agent inherent features, together with an instantiation mechanism to activate single agent’s runtime behavior, communication configurations for multiple agents’ connected behaviors, and scenario task configurations for their dynamic topologies. We also present a path-oriented falsification approach to falsify system requirements. It employs classification-model-based optimization to explore search space effectively and cut unnecessary system simulations and robustness calculations for efficiency. Our modeling and falsification are implemented in a tool called . Experiments have shown that it can largely reduce modeling time and improve modeling accuracy, and perform scalable CPS falsification with high success rates in seconds.
Probabilistic Access Policies with Automated Reasoning Support
Authors: Zhu Shaowei , Zhang Yunbo 
Published: July 2024

AbstractExisting access policy languages like Cedar equipped with SMT-based automated reasoning capabilities are effective in providing formal guarantees about the policies. However, this scheme only supports access control based on deterministic information. Observing that certain information useful for access control can be described by random variables, we are motivated to develop a new paradigm of access control in which access policies contain rules about uncertainty, or more precisely, probabilities of random events. To compute these probabilities, we rely on probabilistic programming languages. Additionally, we show that the probabilistic part of these policies can be encoded in linear real arithmetic, which enables practical automated reasoning tasks such as proving relative permissiveness between policies. We demonstrate the advantages of the proposed probabilistic policies over the existing paradigm through two case studies on real-world datasets with a prototype implementation.
Dynamic Programming for Symbolic Boolean Realizability and Synthesis
Authors: Lin Yi , Martinelli Tabajara Lucas , Vardi Moshe Y. 
Published: July 2024

AbstractInspired by recent progress in dynamic programming approaches for weighted model counting, we investigate a dynamic-programming approach in the context of boolean realizability and synthesis, which takes a conjunctive-normal-form boolean formula over input and output variables, and aims at synthesizing witness functions for the output variables in terms of the inputs. We show how graded project-join trees, obtained via tree decomposition, can be used to compute a BDD representing the realizability set for the input formulas in a bottom-up order. We then show how the intermediate BDDs generated during realizability checking phase can be applied to synthesizing the witness functions in a top-down manner. An experimental evaluation of a solver – DPSynth – based on these ideas demonstrates that our approach for Boolean realizabilty and synthesis has superior time and space performance over a heuristics-based approach using same symbolic representations. We discuss the advantage on scalability of the new approach, and also investigate our findings on the performance of the DP framework.