NuSMT

What is NuSMT?

NuSMT is a verification tool that combines the strengths of BDDs (Binary Decision Diagrams) and SMT (Satisfiability Modulo Theory) solvers. The name 'NuSMT' is derived from the verification engines it is composed of: NuSMV model checker and MathSAT SMT solver. BDD based quantification is known to be efficient and it forms the heart of many modern model checking engines. NuSMT is an extension to the most widely used open-source model checker NuSMV. The newer verification engines - SMT solvers quite aptly referred to as a "disruptive technology" enables us to handle richer theories. NuSMT uses MathSAT SMT solver.

What is new in NuSMT?

Traditionally CEGAR loop is implemented using SAT solvers. Although efficient SAT solvers are available, one has to encode the verification problem into a SAT problem in order to use them. Further, richer theories, that are predominant in for example hybrid systems, can not be encoded. In NuSMT we use SMT solvers, which can deal with richer theories, thereby avoiding the need to encode our verification problem into theory of Booleans. We perform a tight integration of a well known model checker with an efficient SMT solver to get the best of both worlds - scalability of SMT solvers with respect to SAT solvers, and the efficiency of BDD based techniques, and carve out a CEGAR framework, that enables effective, efficient and scalable formal verification. We evaluated NuSMT on several examples of hybrid systems and found the results to be encouraging. The material mentioned in the 'Publications' section describes the techniques employed in NuSMT in greater detail.

Predicate Abstraction & CEGAR

Predicate Abstraction is a kind of abstraction technique wherein the concrete model is abstracted with respect to a given set of predicates. Predicates are relations over the variables of the concrete program. The abstract model is constructed by keep- ing track of certain predicates either provided by the user, or in more sophisticated techniques discovered automatically by the iterative process itself. Each such predicate is represented by a Boolean variable in the abstract model. We refer to the mapping from the concrete space to the abstract (Boolean) space as abstraction function and we also assume a dual function - concretization function, mapping the abstract states to sets of concrete states. The abstract system may not be complete with respect to the properties, and hence it might have to be refined by adding more information to the initial abstract model. This pro- cess of refinement can also be automated and in most tools employing predicate abstraction technique, several iterations of refinement is not uncommon. Predicate abstraction of ANSI-C programs integrated with counterexample guided abstraction refinement was introduced by Ball and Rajamani. This lead to the success of this approach in industrial scale examples, namely the SLAM project at Microsoft Research. The project succeeded in veri- fying properties of Windows device drivers. Consequently, there became available many tools based on abstraction refinement framework. Some of the popular ones include BLAST, SLAM, VCEGAR, Copper (in ComfoRT), etc.

The abstraction generated by predicate abstraction techniques are usually much simpler than the concrete model and can be readily subject to model checking. Since the abstract model is composed of Boolean variables and transitions over them, model checking is much more effective over the abstract model. If a property is true of the abstract model, it is also true of the concrete model. If a property does not hold, the model checker generates a counterexample. A counterexample is a sequence of transitions from an initial abstract state and ending in an abstract state that violates the property. Note that because of loss of some information due to abstraction, this counterexample may not be a real counterexample, but just an artifact of the abstraction process. The counterexample is analyzed to check if it is real, by simulating it on the concrete model. This phase is called Simulation. This is performed by mapping back the states in the abstract counterexample trace to the concrete model, to see if the behaviour represented by the abstract counterexample is feasible in the actual concrete model. If simulation succeeds, then the counterexample is real, and the concrete model has a corresponding path leading to an error state. If simulation fails, then the counterexample is said to be a spurious counterexample. The abstraction has to be refined in order to eliminate the spurious behaviour of the model. The refinement phase consists of analyzing the spurious counterexample in order to figure out more details in order to refine the abstract model. This iterative process of abstraction, model checking, simulation and refinement are carried out till the property is proved or a real counterexample encountered. This process is hence known as CEGAR - Counterexample Guided Abstraction Refinement.

Publications

In case you need any clarifications, details or if you have any suggestions, comments or feedback, you are welcome to contact the author at



kalyan@lri.fr