2,069 papers · page 6 of 104
Abstract The design of computer microarchitectures is a challenging task, involving a trade-off between efficiency and security. In the literature, two concerns which are affected by the details of the microarchitecture – formal assembly semantics, and vulnerability discovery and…
Abstract This paper presents a modular approach to verifying the vector module of PETSc, a widely used library in scientific computing, using the CIVL model checker. Our approach relies on the creation of stub functions, which serve a dual purpose of specifying the intended behav…
Abstract Deep Neural Networks (DNNs) are increasingly deployed in critical applications, where ensuring their safety and robustness is paramount. We present $$_\text {CAV25}$$ CAV 25 , a high-performance DNN verification tool that uses the DPLL(T) framework and supports a wide-ra…
Abstract We consider the use of commutativity-based reduction for the algorithmic verification of concurrent programs. In existing work, the commutativity relation used for the reduction is mostly fixed statically. In this paper, we propose a demand-driven approach to compute the…
Abstract Viper is a verification infrastructure that facilitates the development of automated verifiers based on separation logic. Viper consists of the Viper intermediate language and two backend verifiers based on symbolic execution and verification condition generation, respec…
Abstract Programs that manipulate tree-shaped data structures often require complex, specialized proofs that are difficult to generalize and automate. This paper introduces a unified, foundational approach to verifying such programs. Central to our approach is the knitted-tree en…
Abstract Despite its prevalence, probabilistic bisimilarity suffers from a lack of robustness under minuscule perturbations of the transition probabilities. This can lead to discontinuities in the probabilistic bisimilarity distance function, undermining its reliability in practi…
Abstract In 2015, LearnLib, the open-source framework for active automata learning, received the prestigious CAV artifact award. This paper presents the advancements made since then, highlighting significant additions to LearnLib, including state-of-the-art algorithms, novel lear…
Abstract Certification was made mandatory for the first time in the latest hardware model checking competition. In this case study, we investigate the trade-offs of requiring certificates for both passing and failing properties in the competition. Our evaluation shows that partic…
Abstract We present a compositional approach to controller synthesis of discrete event system controllers with linear temporal logic (LTL) goals. We exploit the modular structure of the plant to be controlled, given as a set of labelled transition systems (LTS), to mitigate state…
Abstract Markov decision processes model systems subject to nondeterministic and probabilistic uncertainty. A plethora of verification techniques addresses variations of reachability properties, such as: Is there a scheduler resolving the nondeterminism such that the probability …
Abstract We present PyCaliper : a Python-embedded framework to formulate, verify, and auto-synthesize specifications for hardware designs at the register transfer level (RTL). By being Python-embedded, PyCaliper is easy to use and benefits from object-oriented principles and Pyth…
Abstract Automated program verifiers such as Dafny, F $$^{\star}$$ ⋆ , Verus, and Viper are now routinely used to verify real-world software. Unfortunately, the performance of the SMT solvers employed by these tools is not always able to keep up with the increasing size and compl…
Abstract We report on the development of an optimized and verified decision procedure for orthologic equalities and inequalities. This decision procedure is quadratic-time and is used as a sound, efficient and predictable approximation to classical propositional logic in automate…
Abstract This paper presents , a new intermediate verification language and deductive verification tool that provides inbuilt support for concurrency reasoning. ’s meta-theory is based on the higher-order concurrent separation logic Iris, incorporating core features such as user-…
Abstract The Model Constructing Satisfiability (MCSat) approach to Satisfiability Modulo Theories (SMT) has demonstrated strong performance when handling complex theories such as nonlinear arithmetic. Despite being in development for over a decade, there has been limited research…
Abstract The synthesis of infinite-state reactive systems from temporal logic specifications or infinite-state games has attracted significant attention in recent years, leading to the emergence of novel solving techniques. Most approaches are accompanied by an implementation sho…
Abstract We present the first supermartingale certificate for quantitative $$\omega $$ ω -regular properties of discrete-time infinite-state stochastic systems. Our certificate is defined on the product of the stochastic system and a limit-deterministic Büchi automaton that speci…
Abstract With the explosion in popularity of the Rust programming language, a wealth of tools have recently been developed to analyze, verify, and test Rust programs. Alas, the Rust ecosystem remains relatively young, meaning that every one of these tools has had to re-implement …
Abstract Active automata learning from membership and equivalence queries is a foundational problem with numerous applications. We propose a novel variant of the active automata learning problem: actively learn finite automata using preference queries —i.e., queries about the rel…