2,069 papers · page 6 of 104
Robert J. Colvin, Roger C. Su
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…
Venkata Dhavala, Jan Hückelheim, Paul D. Hovland, Stephen F. Siegel
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…
Hai Duong, ThanhVu Nguyen, Matthew B. Dwyer
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…
Marcel Ebbinghaus, Dominik Klumpp, Andreas Podelski
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…
Marco Eilers, Malte Schwerhoff, Alexander J. Summers, Peter Müller
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…
Marco Faella, Gennaro Parlato
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…
Syyeda Zainab Fatmi, Stefan Kiefer, David Parker, Franck van Breugel
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…
Markus Frohme, Falk Howar, Bernhard Steffen
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…
Nils Froleyks, Emily Yu, Mathias Preiner, Armin Biere, Keijo Heljanko
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…
Hernán Gagliardi, Víctor A. Braberman, Sebastián Uchitel
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…
Lina Gerlach, Tobias Winkler, Erika Ábrahám, Borzoo Bonakdarpour, Sebastian Junges
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 …
Adwait Godbole, Brian Huffman, Fangfei Liu, Carlos V. Rozas, Sanjit A. Seshia
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…
Kiran Gopinathan, Dionysios Spiliopoulos, Vikram Goyal, Peter Müller, Markus Püschel, Ilya Sergey
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…
Simon Guilloud, Clément Pit-Claudel
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…
Ekanshdeep Gupta, Nisarg Patel, Thomas Wies
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-…
Thomas Hader, Ahmed Irfan, Stéphane Graham-Lengrand
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…
Philippe Heim, Rayna Dimitrova
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…
Thomas A. Henzinger, Kaushik Mallik, Pouya Sadeghi, Dorde Zikelic
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…
Son Ho, Guillaume Boisseau, Lucas Franceschino, Yoann Prak, Aymeric Fromherz, Jonathan Protzenko
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 …
Eric Hsiung, Joydeep Biswas, Swarat Chaudhuri
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…