ABSTRACT. In this paper, we consider the problem of model checking fair transition systems expressed symbolically in the framework of Satisfiability Modulo Theories. This problem, referred to as Verification Modulo Theories, is tackled by combining two key elements from the legacy of Ed Clarke: SAT-based verification and abstraction refinement. We show how fundamental SAT-based algorithms have been lifted to deal with the extended expressiveness with a tight integration of abstraction within a CEGAR loop. In turn, the case of nonlinear theories is based on a CEGAR loop over the linear case. These two elements have also deeply impacted the development of the NuSMV model checker, born from a joint project between FBK and CMU, and its successor nuXmv, whose core integrates SMT-based techniques for VMT.

(Presentation-only submission. This journal paper appeared in Formal Methods in Systems Design, Volume 60, pages 452–481, (2022), special issue in memory of Edmund M. Clarke)

ABSTRACT. The SMT (Satisfiability Modulo Theories) theory of arrays is well established and widely used, various decision procedures and extensions have been developed for it. However, recent works suggest that it is more efficient to develop tailored reasoning for some theories, such as sequences and strings, rather than reasoning over them through axiomatization over the theory of arrays. In this paper, we are interested in reasoning over n-indexed sequences as they are found in some programming languages such as Ada. We propose an SMT theory of n-indexed sequences, and we explore different ways to represent and reason over n-indexed sequences using existing theories, as well as tailored calculi for the theory.

ABSTRACT. In the last few years there have been rapid developments in SMT solving for finite fields. These include new decision procedures, new implementations of SMT theory solvers, and new software verifiers that rely on SMT solving for finite fields. To support interoperability in this emerging ecosystem, we propose the SMT-LIB theory of finite field arithmetic (FFA). The theory defines a canonical representation of finite field elements as well as definitions of operations and predicates on finite field elements.

For the most up-to-date version of our proposal, find it on arXiv at http://arxiv.org/abs/2407.21169.

ABSTRACT. SMT solving for higher order logic has been around for a few years and many challenges remain to tackle. In this talk, I will present an assessment of the current state of research in higher-order SMT and focus on the challenge of quantifier instantiation, following a conflict-based approach inspired from first-order logic.

ABSTRACT. The process of developing civil aircraft and their related systems includes multiple phases of Preliminary Safety Assessment (PSA). An objective of PSA is to link the classification of failure conditions and effects (produced in the functional hazard analysis phases) to appropriate safety requirements for elements in the aircraft architecture. A complete and correct preliminary safety assessment phase avoids potentially costly revisions to the design late in the design process. Hence, automated ways to support PSA are an important challenge in modern aircraft design. A modern approach to conducting PSAs is via the use of abstract propagation models, that are basically hyper-graphs where arcs model the dependency among components, e.g. how the degradation of one component may lead to the degraded or failed operation of another. Such models are used for computing failure propagations: the fault of a component may have multiple ramifications within the system, causing the malfunction of several interconnected components. A central aspect of this problem is that of identifying the minimal fault combinations, also referred to as minimal cut sets, that cause overall failures. In this paper we propose an expressive framework to model failure propagation, catering for multiple levels of degradation as well as cyclic and nondeterministic dependencies. We define a formal sequential semantics, and present an efficient SMT-based method for the analysis of failure propagation, able to enumerate cut sets that are minimal with respect to the order between levels of degradation. In contrast with the state of the art, the proposed approach is provably more expressive, and dramatically outperforms other systems when a comparison is possible.

ABSTRACT. Satisfiability Modulo Theory (SMT) solvers have significantly advanced automated reasoning due to their effectiveness in solving problems across various fields. With the advancement in SMT solvers, there is growing interest in exploring capabilities beyond mere satisfiability, similar to the progression observed in Boolean satisfiability solvers that expanded into counting and sampling. In this study, we investigate the following question: Can we extend a modern SMT solver with modern CNF model counters and CNF samplers to be efficient in solving the problems of counting and sampling over bit-vectors?

The main contribution of this work is the development of an efficient approximate model counter along with the first efficient almost-uniform and uniform-like samplers for the theory of bit-vectors. Our tool csb converts the bit-vector formula into a CNF formula using bit-blasting techniques before applying CNF model counters or samplers to perform counting or sampling. Our tool enhances the popular SMT solver STP with an approximate model counter ApproxMC, an almost-uniform sampler UniGen, and a uniform-like sampler CMSGen. Our experiments demonstrate significant performance improvements over existing methods.

Given the various techniques developed for model counters, bit-blasting, and preprocessing over the last decades, there are multiple ways to combine these components to construct our bit-vector model counter. To determine the most effective integration approach, we curated a set of bit-vector benchmarks from four distinct bit-vector counting problems to identify the best combinations and experiment with all possible combinations of the counter. Our empirical analysis underscores the effectiveness of a tightly integrated system combining bit-blasting, preprocessing, and CNF counters and samplers.

ABSTRACT. Dolmen provides tools to parse, type, and validate input files used in automated deduction, and in particular problems from the SMT-LIB. This work adds to Dolmen the ability to export in SMT-LIB format any problem that it successfully parsed and typed. More than just printing term, this work includes the ability for Dolmen to compute the minimal SMT-LIB logic needed for a set of statements, so that problems from other languages can be given an adequate logic when being exported to SMT-LIB format. This also means that Dolmen can now be used to compute the minimal logic of an arbitrary SMT-LIB problem.