Search Results

As a new programming paradigm, deep neural networks (DNNs) have been increasingly deployed in practice, but the lack of robustness hinders their applications in safety-critical domains. While there are techniques for verifying DNNs with formal guarantees, ...

Minimal trap spaces (MTSs) capture subspaces in which the Boolean dynamics is trapped, whatever the update mode. They correspond to the attractors of the most permissive mode. Due to their versatility, the computation of MTSs has recently gained ...$$

Bounded model checking (BMC) is well-known to be undecidable even for simple hybrid systems. Existing work targeted for a wide class of non-linear hybrid systems reduces the BMC problem to the satisfiability problem of an satisfiability modulo theory ...

The verification of safety-critical software systems is an algorithmically complex task, which often utilizes SMT (Satisfiability Modulo Theory) solvers for computing abstractions and refinements. It follows that the performance of SMT solvers impacts ...

Deep Reinforcement Learning (DRL) has demonstrated its strength in developing intelligent systems. These systems shall be formally guaranteed to be trustworthy when applied to safety-critical domains, which is typically achieved by formal ...

Given a set of uninterpreted programs to be verified, the trace abstraction-based verification method can be used to solve them once at a time. The verification of different programs is independent of each other. However, the individual ...

Abstract interpretation is a sound-by-construction method for program verification: any erroneous program will raise some alarm. However, the verification of correct programs may yield false-alarms, namely it may be incomplete. Ideally, one would like ...

Techniques for software verification are typically realized as cohesive units of software with tightly coupled components. This makes it difficult to re-use components, and the potential for workload distribution is limited. Innovations in software ...

With the improvement of hardware and algorithms, the main challenge of software model checking has shifted from pure algorithmic performance toward supporting a wider set of input programs. Successful toolchains tackle the problem of parsing a wide ...

The verification of uninterpreted programs is undecidable in general. This paper proposes to employ counterexample-guided abstraction refinement (CEGAR) framework for verifying uninterpreted programs. Different from the existing interpolant-based ...

Due to the state-space explosion problem, efficient verification of real-world programs in large scale is still a big challenge. Particularly, thread alternation makes the verification of concurrent programs much more difficult since it aggravates this ...

In recent years, expansion-based techniques have been shown to be very powerful in theory and practice for solving quantified Boolean formulas (QBF), the extension of propositional formulas with existential and universal quantifiers over Boolean ...$$

Reachability analysis of dynamical models is a relevant problem that has seen much progress in the last decades, however with clear limitations pertaining to the nature of the dynamics and the soundness of the results. This article focuses on ...

A generic register automaton is a finite automaton equipped with variables (which may be viewed as counters or, more generally, registers) ranging over infinite data domains. A trace of a generic register automaton is an alternating sequence of ...

Automated formal verification is often based on the Counterexample-Guided Abstraction Refinement (CEGAR) approach. Many variants of CEGAR have been developed over the years as different problem domains usually require different strategies for ...

Verification of multitasking embedded software requires taking into account its underlying operating system w.r.t. its scheduling policy and handling of task priorities in order to achieve a higher degree of accuracy. However, such comprehensive ...

We propose and evaluate a new CNF encoding based on Zykov’s tree for computing the chromatic number of a graph. Zykov algorithms are branch-and-bound procedures, that branch on pairings of vertices that express whether or not two non-adjacent ...

This paper introduces a new, fully automated model-based approach for effective testing of Android apps. Different from existing model-based approaches that guide testing with a static GUI model (i.e., the model does not evolve its abstraction during ...

Block summarization is an efficient technique in software verification to decompose a verification problem into separate tasks and to avoid repeated exploration of reusable parts of a program. In order to benefit from abstraction at the same time, ...

The complexity of designing and verifying large-scale systems requires abstract models. Consistently and systematically deriving a more concrete model from an abstract model with regard to verification of its behavior against certain properties is an ...