Interpolant-based model checking has been shown to be effective on large verification instances, as it efficiently combines automated abstraction and reachability fixed-point checks. On the other hand, methods based on variable quantification have proved their ability to remove free inputs, thus projecting the search space over state variables. In this paper, we propose an integrated approach which combines the abstraction power of interpolation with techniques that rely on and-inverter graph (AIG) and/or binary decision diagram (BDD) representations of states, directly supporting variable quantification and fixed-point checks. The underlying idea of this combination is to adopt AIG or BDD-based quantifications to limit and restrict the search space and the complexity of the interpolant-based approach. The exploited strategies, most of which are individually well known, are integrated with a new flavor, specifically designed to improve their effectiveness on difficult verification instances. Experimental results, specifically oriented to hard-to-solve verification problems, show the robustness of our approach.

The design of complex embedded systems deployed in safety-critical or mission-critical applications mandates the availability of methods to validate the system dependability across the whole design flow. In this article we introduce a fault injection approach, based on loadable kernel modules and running under the Linux operating system, which can be adopted as soon as a running prototype of the systems is available. Moreover, for the purpose of decoupling dependability analysis from hardware availability, we also propose the adoption of hardware virtualization. Extensive experimental results show that statistical analysis made on top of virtual prototypes are in good agreement with the information disclosed by fault detection trends of real platforms, even under real-time constraints.

Hardware synthesis is the process by which system-level, Register Transfer (RT)-level, or behavioral descriptions can be turned into real implementations, in terms of logic gates. Scheduling is one of the most time-consuming steps in the overall design flow, and may become much more complex when performing hardware synthesis from high-level specifications. Exploiting a single scheduling strategy on very large designs is often reductive and potentially inadequate. Furthermore, finding the “best” single candidate among all possible scheduling algorithms is practically infeasible. In this article we introduce a hybrid scheduling approach that is a preliminary step towards a comprehensive solution not yet provided by industrial or by academic solutions. Our method relies on an abstract symbolic representation of data flow nodes (operations) bound to control flow paths: it produces a more realistic lower bound during the prescheduling resource estimation step and speeds up slower but accurate heuristic scheduling techniques, thus achieving a globally improved result.

Constraints represent a key component of state-of-the-art verification tools based on compositional approaches and assume-guarantee reasoning. In recent years, most of the research efforts on verification constraints have focused on defining formats and techniques to encode, or to synthesize, constraints starting from the specification of the design. In this paper, we analyze the impact of constraints on the performance of model checking tools, and we discuss how to effectively exploit them. We also introduce an approach to explicitly derive verification constraints hidden in the design and/or in the property under verification. Such constraints may simply come from true design constraints, embedded within the properties, or may be generated in the general effort to reduce or partition the state space. Experimental results show that, in both cases, we can reap benefits for the overall verification process in several hard-to-solve designs, where we obtain speed-ups of more than one order of magnitude.

Interpolant-based model checking has been shown effective on large verification instances, as it efficiently combines automated abstraction and fixed-point checks. On the other hand, methods based on variable quantification have proved their ability to remove free inputs, thus projecting the search space over state variables. In this paper we propose an integrated approach combining the abstraction power of interpolation with techniques relying on AIG and/or BDD representations of states, supporting variable quantification and fixed-point checks. The underlying idea of this combination is to adopt AIG- or BDD-based quantifications to limit and restrict the search space (and the complexity) of the interpolant-based approach. The exploited strategies, individually well-known, are integrated with a new flavor, specifically designed to improve their effectiveness on large verification instances. Experimental results, oriented to hard-to-solve verification problems, show the robustness of our approach.

This paper addresses the field of unbounded model checking (UMC) based on SAT engines, where Craig interpolants have recently gained wide acceptance as an automated abstraction technique. We start from the observation that interpolants can be quite effective on large verification instances. As they operate on SAT-generated refutation proofs, interpolants are very good at automatically abstract facts that are not significant for proofs. In this work, we push forward the new idea of generating abstractions without resorting to SAT proofs, and to accept (reject) abstractions whenever they (do not) fulfill given adequacy constraints. We propose an integrated approach smoothly combining the capabilities of interpolation with abstraction and over-approximation techniques, that do not directly derive from SAT refutation proofs. The driving idea of this combination is to incrementally generate, by refinement, an abstract (over-approximate) image, built up from equivalences, implications, ternary and localization abstraction, then (eventually) from SAT refutation proofs. Experimental results, derived from the verification of hard problems, show the robustness of our approach.

SAT--based Unbounded Model Checking based on Craig Interpolants is often able to overcome BDDs and other SAT--based techniques on large verification instances. Based on refutation proofs generated by SAT solvers, interpolants provide compact circuit representations of state sets, as they abstract away several nonrelevant details of the proofs. We propose three main contributions, aimed at controlling interpolant size and traversal depth. First of all, we introduce interpolant--based dynamic abstraction to reduce the support of computed interpolants. Subsequently, we propose new advances in interpolant compaction by redundancy removal. Finally, we introduce interpolant computation exploiting circuit quantification, instead of SAT refutation proofs. These techniques heavily rely on an effective application of the incremental SAT paradigm. The experimental results proposed in this paper are specifically oriented to prove properties, rather than disproving them, i.e., they target complete verification instead of simply hunting bugs. They show how this methodology is able to stretch the applicability of interpolant--based Model Checking to larger and deeper verification instances.

This paper addresses SAT-based Unbounded Model Checking based on Craig Interpolants. This recently introduced methodology is often able to outperform BDDs and other SAT-based techniques on large verification instances. Based on refutation proofs generated by SAT solvers, interpolants provide compact circuit representations of state sets, and abstract away several details non relevant for proofs. We propose three main contributions, aimed at controlling interpolant size and traversal depth. First of all, we introduce interpolant-based dynamic abstraction to reduce the support of the computed interpolant. Second, we propose new advances in interpolant compaction by redundancy removal. Both techniques rely on an effective application of the incremental SAT paradigm. Finally, we also introduce interpolant computation exploiting circuit quantification, instead of SAT refutation proofs. Experimental results are specifically oriented to prove properties, rather than disproving them (bug hunting). They show how the methodology is able to extend the applicability of interpolant based Model Checking to larger and deeper verification instances.