2,069 papers · page 2 of 104
Abstract We present a new Programming-by-Examples (PBE) approach to repairing regex-dependent string-manipulation programs. Our approach has the following key features: (1) the support for a wide range of functions including regex-dependent functions such as , , , list manipulati…
Abstract We generalize an efficient automata-based approach to string solving, the stabilization-based method behind the solver Z3-Noodler , to support relational constraints represented by finite-state transducers (useful for modeling constraints, etc.). We focus on efficient ha…
Abstract We introduce a formal modeling methodology to analyze quantum communication protocols in the tool Uppaal . Our approach encodes quantum states, operations, and measurements into Uppaal timed automata with data extensions and external function calls, enabling both exhaust…
Abstract This paper presents the first symbolic bounded model checking technique capable of verifying $$\forall ^+\exists ^+$$ ∀ + ∃ + -liveness hyperproperties (expressed in HyperLTL) over arbitrary (non-terminating) reactive systems. Previous bounded procedures for HyperLTL han…
Abstract SystemVerilog remains one of the most widely used languages for designing and verifying digital circuits. Despite its importance, the SystemVerilog standard suffers from ambiguities, which can lead to inconsistent implementations and portability challenges. Formal method…
Abstract Quantum circuit optimizers use rewrite rules from circuit equivalences, yet prior work has identified thousands of such identities, creating substantial challenges for their storage, management, and effective application. For many widely used unitary gate sets, including…
Abstract Syntactic obligations are a fragment of LTL formulas that translate to deterministic weak $$\omega $$ ω -automata (DWA). We show that syntactic obligations can be very efficiently converted to minimal DWA represented using multi-terminal binary decision diagrams (MTBDDs)…
Abstract We present Taco , a toolsuite for the development and automatic verification of fault-tolerant and threshold-based distributed algorithms. Our toolsuite implements three approaches for model checking threshold automata in different decidable fragments known from the lite…
Abstract The verification of reductions , representative subsets of interleavings, simplifies correctness proofs of parameterized concurrent programs. We introduce an expressive class of syntactic reductions, which we call natural reductions . Natural reductions are specified by …
Abstract We present an SMT-based active learning algorithm for nondeterministic weighted automata (WFAs) as a practical and robust alternative to Hankel/ $$\textsf{L}^\star $$ L ⋆ -style methods. Our algorithm is parametric in a given semiring and, if it terminates, guaranteed to…
Abstract Modern stream-based monitors collect detailed statistics of the runtime behavior of the system under observation. If the system runs in a privacy-sensitive context, this poses the risk of disclosing sensitive information. Differential privacy is the state-of-the-art appr…
Abstract We introduce a generic certificate format for verifying liveness properties in hardware model checking. The format relies purely on propositional predicates and does not involve explicit counters. Our certificates can be efficiently validated using a fixed number of SAT …
Abstract Machine Learning (ML) inference is shifting from using pre-developed static, CUDA C++, GPU kernel libraries to using MLIR-based graph compilers that perform advanced optimizations and generate custom kernels. This paradigm shift reimagines how we achieve ML inference in …
Abstract We present —a Dafny-style verifier for imperative programs embedded in the Lean proof assistant. Like Dafny, supports reasoning about effectful programs featuring mutable state, loops, and non-determinism. Unlike Dafny, seamlessly combines automated SMT-based proofs with…
Abstract In imperative and object-oriented languages, programmers often define relations such as equality or orderings between instances of structs or classes. These object relations must satisfy well-known algebraic properties, such as reflexivity, transitivity, etc. Violations …
Abstract Separation-logic proofs of heap-manipulating programs require careful accounting of objects and pointers in memory. On paper, these proofs are often accompanied by heap-memory diagrams that help authors and readers track the evolution of the program’s abstract state. How…
Abstract This paper introduces several techniques that improve the scalability of the deductive verification of data-level parallel programs working on arrays and matrices. First of all, we introduce a technique to rewrite expressions with (nested) quantifiers, so suitable trigge…
Abstract Reference counting bugs in Linux kernel drivers can lead to severe resource mismanagement and security vulnerabilities. We introduce DrvHorn , a novel automated tool to detect these bugs by reducing reference counting verification to an assertion checking problem leverag…
Abstract Shielding is a prominent model-based technique to ensure safety of autonomous agents. Classical shielding aims to ensure that nothing bad ever happens and comes with strong guarantees about safety and maximal permissiveness. However, shielding systems for probabilistic s…
Abstract Quantitative automata (QAs) extend finite-state automata on infinite words with weighted transitions to specify quantitative system properties. However, their finite weight sets rule out properties like average response time, where response times can be arbitrarily large…