1,721,088 research outputs found
A Structural Approach to Reasoning with Quantified Boolean Formulas
No full textIn this paper we approach the problem of reason-
ing with quantified Boolean formulas (QBFs) by
combining search and resolution, and by switch-
ing between them according to structural proper-
ties of QBFs. We provide empirical evidence that
QBFs which cannot be solved by search or resolu-
tion alone, can be solved by combining them, and
that our approach makes a proof-of-concept imple-
mentation competitive with current QBF solvers
A Multi-engine Solver for Quantified Boolean Formulas
No full textn this paper we study the problem of yielding robust performances
from current state-of-the-art solvers for quantified Boolean formulas (QBFs).
Building on top of existing QBF solvers, we implement a new multi-engine solver
which can inductively learn its solver selection strategy. Experimental results con-
firm that our solver is always more robust than each single engine, that it is stable
with respect to various perturbations, and that such results can be partially ex-
plained by a handful of features playing a crucial role in our solver
Verification Of Data-Intensive Embedded Systems
No full textVerification of embedded software relying on black-box hardware is challenging whenever precise specifications of the underlying systems are incomplete or not available. Learning structured hardware models is a powerful enabler of verification in these cases, but it
can be inefficient when the system to be learned is data-intensive rather than control-intensive. We contribute a methodology to attack this problem based on a specific class of automata which are well suited to model systems wherein data paths are known to be decoupled from control paths. We show the effectiveness of our approach by combining learning and verification to assess the correctness of embedded programs relying on FIFO register circuitry to control an elevator system
NeVer: a tool for artificial neural networks verification
No full textThe adoption of Artificial Neural Networks (ANNs) in safety-related ap-
plications is often avoided because it is difficult to rule out possible misbehaviors with
traditional analytical or probabilistic techniques. In this paper we present NeVer, our
tool for checking safety of ANNs. NeVer encodes the problem of verifying safety of
ANNs into the problem of satisfying corresponding Boolean combinations of linear
arithmetic constraints. We describe the main verification algorithm and the structure
of NeVer. We present also empirical results confirming the effectiveness of NeVer
on realistic case studies
An Empirical study of QBF encodings: from treewidth estimation to useful preprocessing
No full textFrom an empirical point of view, the hardness of quantified Boolean formulas (QBFs), can be characterized by the (in)ability of current state-of-the-art QBF solvers to decide about the truth of formulas given limited computational resources. In this paper, we start from the problem of computing empirical hardness markers, i.e., features that can discriminate between hard and easy QBFs, and we end up showing that such markers can be useful to improve our understanding of QBF preprocessors. In particular, considering the connection between classes of tractable QBFs and the treewidth of associated graphs, we show that (an approximation of) treewidth is indeed a marker of empirical hardness and it is the only parameter which succeeds consistently in being so, even considering several other purely syntactic candidates which have been successfully employed to characterize QBFs in other contexts. We also show that treewidth approximations can be useful to describe the effect of QBF preprocessors, in that some QBF solvers benefit from a preprocessing phase when it reduces the treewidth of their input. Our experiments suggest that structural simplifications reducing treewidth are a potential enabler for the solution of hard QBF encodings
Challenging SMT solvers to verify neural networks
No full textIn recent years, Satisfiability Modulo Theory (SMT) solvers are becoming increasingly popular in the Computer Aided Verification and Reasoning community. Used natively or as back-engines, they are accumulating a record of success stories and, as witnessed by the annual SMT competition, their performances and capacity are also increasing steadily. Introduced in previous contributions of ours, a new application domain providing an outstanding challenge for SMT solvers is represented by verification of Multi-Layer Perceptrons (MLPs) a widely-adopted kind of artificial neural network. In this paper we present an extensive evaluation of the current state-of-the-art SMT solvers and assess their potential in the promising domain of MLP verification
A Self-adaptive multi-engine solver for quantified Boolean formulas
No full textIn this paper we study the problem of engineering a robust solver for quantified Boolean formulas (QBFs), i.e., a tool that can efficiently solve formulas across different problem domains without the need for domain-specific tuning. The paper presents two main empirical results along this line of research. Our first result is the development of a multi-engine solver, i.e., a tool that selects among its reasoning engines the one which is more likely to yield optimal results. In particular, we show that syntactic QBF features can be correlated to the performances of existing QBF engines across a variety of domains. We also show how a multi-engine solver can be obtained by carefully picking state-of-the-art QBF solvers as basic engines, and by harnessing inductive reasoning techniques to learn engine-selection policies. Our second result is the improvement of our multi-engine solver with the capability of updating the learned policies when they fail to give good predictions. In this way the solver becomes also self-adaptive, i.e., able to adjust its internal models when the usage scenario changes substantially. The rewarding results obtained in our experiments show that our solver AQME--Adaptive QBF Multi-Engine--can be more robust and efficient than state-of-the-art single-engine solvers, even when it is confronted with previously uncharted formulas and competitors
- …
