2,069 papers · page 3 of 104
Abstract Workflow nets are a variant of Petri nets used for modelling business processes. Central decision problems are soundness problems, one popular variant called generalised soundness. These problems intuitively ask whether initiated processes can be finalised. We introduce …
Abstract We introduce the tool $$^{\textsf {\small 2.0}}$$ 2 . 0 , the first highly efficient push-button bounded model checker (BMC) for hyperproperties. HyperQB takes as input a model in NuSMV or Verilog and a formula expressed in the temporal logics HyperLTL or A-HLTL. The cor…
Abstract In many verification tasks, system models do not correspond to the focused and idealized models that appear in research literature. In practice, models usually contain components and execution paths that are irrelevant to the property being verified or have only a limite…
Abstract Operating a network is a daunting task. Operating one at a global scale, with stringent service objectives and requirements to be available during maintenance and failures, is even more so. At Google, we operate such a network. This paper details our experience applying …
Abstract Synthesizing a reactive system from specifications given in linear temporal logic (LTL) is a classical problem, finding its applications in safety-critical systems design. These systems are typically represented using either Mealy machines or AIGER circuits. We present t…
Abstract Agents in cyber-physical systems are increasingly entrusted with safety-critical tasks. Ensuring the safety of these agents often requires localizing their pose for subsequent actions. Pose estimates can, e.g., be obtained from various combinations of lidar sensors, came…
Abstract A DFA separates two disjoint languages $$L_1$$ L 1 and $$L_2$$ L 2 if it accepts every word in $$L_1$$ L 1 and rejects every word in $$L_2$$ L 2 . Algorithms for active learning of small separating DFAs have many applications, e.g. for learning network invariants, learni…
Abstract P4 is a domain-specific language for programming protocol-independent packet processors, where packet parsers describe how incoming bit-streams are structured into headers and fields. Building on work by Doenges et al. (2022), we present Octopus , a tool that translates …
Abstract Several extensions of Datalog perform probabilistic inference by allowing users to annotate input facts and rules with probabilities. While extremely useful in many domains (e.g., quantitative program analysis), existing systems typically do not support incremental infer…
Abstract We reexamine the problem of verifying Markov chains with respect to step-bounded reachability probabilities. Prevailing approaches rely on encoding the state-transition matrix using either explicit or symbolic representations. While these approaches are effective for spa…
Abstract Ensuring ancilla safety is a critical correctness requirement for quantum compilation, since ancilla qubits are routinely introduced to implement complex operations with fewer gates and reduced depth. However, formally verifying this property is computationally hard due …
Abstract Formal verification of Semantic Segmentation Networks is challenging due to high-dimensional output spaces and cumulative over-approximation errors in deep architectures. Existing verification methods based on specific Star-set reachability suffer from either exponential…
Abstract Formal verification of transformers has become increasingly important due to their widespread deployment in safety-critical applications. Compared to classic neural networks, the inferences of transformers involve highly complex computations, such as dot products in self…
Abstract is a tool to automatically infer complexity bounds and prove termination of (possibly recursive) integer programs. To this end, implements an alternating modular inference of upper runtime and size bounds for program parts. In particular, uses a portfolio of different te…
Abstract Emerson-Lei automata, which allow arbitrary Boolean combinations of $$\texttt{Fin}$$ Fin and $$\texttt{Inf}$$ Inf acceptance conditions, provide a unifying framework for $$\omega $$ ω -automata but pose significant challenges for determinization. The previous best algori…
Abstract A hard real-time system cannot miss any deadline. A weakly-hard real-time system, on the contrary, is designed to tolerate a specific number of deadline misses. For instance, the $$\texttt {{\textbf {AnyMiss}}}\,(2, 300)$$ AnyMiss ( 2 , 300 ) weakly-hard constraint stipu…
Abstract We present , a versatile, open-source Python library for quantum circuit analysis. reduces various simulation, verification, and synthesis tasks to weighted model counting (#SAT). It supports universal quantum circuits and a wide variety of gates. provides multiple encod…
Abstract Component-based synthesis (CBS) aims to generate loop-free programs from a set of libraries whose methods are annotated with specifications and whose output must satisfy a set of logical constraints, expressed as a query. The effectiveness of a CBS algorithm critically d…
Abstract Decision tree ensembles (DTE) are a popular model for a wide range of AI classification tasks, used in multiple safety critical domains, and hence verifying properties on these models has been an active topic of study over the last decade. One such verification question …
Abstract The TLA $$^+$$ + language has been widely used, both in academia and industry, to specify and reason about distributed systems. This paper presents Apalache , an efficient and flexible symbolic model checker for TLA $$^+$$ + . Apalache ’s engine is based on bounded model…