Symmetry in finite model finding problems of many-sorted first-order logic (MSFOL) can be exploited to reduce the number of interpretations considered during search, thereby improving solver performance for tools such as the Alloy Analyzer. We present a framework to soundly compose static symmetry breaking schemes for many-sorted finite model finding. Then, we introduce and prove the correctness of three static symmetry breaking schemes for MSFOL: 1) one for functions with distinct sorts in the domain and range; 2) one for functions where the range sort appears in the domain; and 3) one for predicates. We provide a novel presentation of sort inference in the context of symmetry breaking that yields a new mathematical link between sorts and symmetries. We empirically investigate how our symmetry breaking approaches affect solving performance.

We motivate and present a proposal for how to represent the syntax of behavioural models written in extended finite-state machine languages with hierarchical states (e.g., the Statecharts family) in SMT-LIB. By including the state structure explicitly in the SMT-LIB model, our goal is to facilitate effective automated deductive reasoning, which can exploit the structure found in the state hierarchy. We present a novel method that combines deep and shallow encoding techniques to describe models that have both state hierarchy and use the rich datatypes found in SMT-LIB. Our representation permits varying semantics to be chosen for the syntax recognizing the rich variety of semantics that exist for this family of modelling languages. We hope that discussion of these representation issues will facilitate model sharing for investigation of analysis techniques.

Temporal logic model checking of infinite state systems without the use of iteration or abstraction is usually considered beyond the realm of first-order logic (FOL) reasoners because of the need for a fixpoint computation. In this paper, we show that it is possible to reduce model checking of a finite or infinite Kripke structure that is expressed in FOL to a validity problem in FOL for a fragment of computational tree logic (CTL), which we call CTL-live. CTL-live includes the CTL connectives that are traditionally used to express liveness properties. Our reduction can form the basis for methods that use FOL reasoning techniques directly to accomplish model checking of CTL-live properties without the need for fixpoint operators, transitive closure, abstraction, or induction.

The ability to create and analyze abstract models is an important step in conquering software complexity. In this paper, we show that it is practical to verify dynamic properties of infinite state models expressed in a subset of CTL directly using an SMT solver without iteration, abstraction, or human intervention. We call this subset CTL-Live and it consists of the operators of CTL expressible using the least fixed point operator of the mu-calculus, which are commonly considered liveness properties (e.g., AF, AU). We show that using this method the verification of an infinite state model can sometimes complete more quickly than verifying a finite version of the model. We also examine modelling techniques to represent abstract models in first-order logic that facilitate this form of model checking.

Avestan is a declarative modelling language compatible with SMT-LIB. SMT-LIB is an standard input language that is supported by the state-of-the-art satisfiability modulo theory solvers (SMT solvers). The recent advances in SMT solvers have introduced them as efficient analysis tools; as a result, they are becoming more popular in the verification and certification of digital products. SMT-LIB was designed to be machine readable rather than human readable. In this paper, we present Avestan, a declarative modelling language that is intended to be analyzed by SMT solvers and readable by humans. An Avestan model is translated to an SMT-LIB model so that it can be analyzed by different SMT solvers. Avestan has relational constructs that are heavily inspired by Alloy; we added these constructs to increase the readability of an Avestan model.

Models are created and changed throughout the development process of software systems. The cost of repairing the errors that are due to mistakes in models is very high. In this research, we address this problem by developing model checking techniques that can be applied to abstract models that guide designers throughout the evolution of models and systems. Abstract models are declarative, expressed as a set of constraints, and this declarative aspect is the main challenge in model checking them. Our main idea for solving this problem is to express the model checking problem as a constraint solving problem. This approach enables designers to use current state-of-the-art constraint solvers for analysis. We have implemented this idea for Alloy models and we are further extending it for automatic model repairing. To achieve scalability, we have developed BDD-based methods for analysis of declarative models and we are studying model checking methods that are based on satisfiability modulo theories. We plan to extend these methods to infinite state space models.

We show how static properties of declarative models can be efficiently analyzed in a symbolic model checker; in particular, we use Cadence SMV to analyze Alloy models by translating Alloy to SMV. The computational paths of the SMV models represent interpretations of the Alloy models. The produced SMV model satisfies its LTL specifications if and only if the original Alloy model is inconsistent with respect to its finite scopes; counterexamples produced by the model checker are valid instances of the Alloy model. Our experiments show that the translation of many frequently used constructs of Alloy to SMV results in optimized models such that their analysis in SMV is much faster than in the Alloy Analyzer. Model checking is faster than SAT solving for static problems when an interpretation can be eliminated by early decisions in the model checking search.