Abstract In the field of formal verification, certifying proofs serve as compelling evidence to demonstrate the correctness of a model within a deductive system. These proofs can be automatically generated as a by-product of the verification process and are key artifacts for high-assurance systems. Their significance lies in their ability to be independently verified by proof checkers, which provides a more convenient approach than certifying the tools that generate them. Modern model checking algorithms adopt deductive methods and usually generate proofs in terms of inductive invariants, assuming that these apply to the original system under verification. Model checkers, though, often make use of a range of complex pre-processing simplifications and transformations to ease the verification process, which add another layer of complexity to the generation of proofs. In this paper, we present a novel approach for certifying model checking results exploiting a theorem prover and a theory of temporal deductive rules that can support various kinds of transformations and simplification of the original circuit. We implemented and experimentally evaluated our contribution on invariants generated using two state-of-the-art model checkers, nuXmv and PdTRAV, and by defining a set of rules within a theorem prover, to validate each certificate.

Machine learning (ML) is ever more frequently used as a tool to aid decision-making. The need to understand the decisions made by ML algorithms has sparked a renewed interest in explainable ML models. A number of known models are often regarded as interpretable by human decision-makers with varying degrees of difficulty. The size of such models plays a crucial role in determining how easily they can be understood by a human. In this paper1 we propose the use of Binary Decision Diagrams (BDDs) as an interpretable ML model. BDDs can be deemed as interpretable as decision trees (DTs) while offering a often more compact representation due to node sharing. Fixed variable ordering also allows for more concise explanations. We propose a SAT-based approach for learning optimal BDDs that exhibit perfect accuracy on training data. We also explore heuristic methods for computing sub-optimal BDDs, in order to improve scalability.

Motivated by the need to understand the behaviour of complex machine learning (ML) models, there has been recent interest in learning optimal (or sub-optimal) decision trees (DTs). This interest is explained by the fact that DTs are widely regarded as interpretable by human decision makers. An alternative to DTs are Binary Decision Diagrams (BDDs), which can be deemed interpretable. Compared to DTs, and despite a fixed variable order, BDDs offer the advantage of more compact representations in practice, due to node sharing. Moreover, there is also extensive experience in the efficient manipulation of BDDs. Our work proposes preliminary inroads in two main directions: (a) proposing a SAT-based model for computing a decision tree as the smallest Reduced Ordered Binary Decision Diagram, consistent with given training data; and (b) exploring heuristic approaches for deriving sub-optimal (i.e., not minimal) ROBDDs, in order to improve the scalability of the proposed technique. The heuristic approach is related to recent work on using BDDs for classification. Whereas previous works addressed size reduction by general logic synthesis techniques, our work adds the contribution of generalized cofactors, that are a well-known compaction technique specific to BDDs, once a care (or equivalently a don't care) set is given. Preliminary experimental results are also provided, proposing a direct comparison between optimal and sub-optimal solutions, as well as an evaluation of the impact of the proposed size reduction steps.

We address the problem of reducing the size of Craig's interpolants (ITPs) used in SAT-based model checking. Whereas it is well known that ITPs are highly redundant, their compaction is typically tackled by reducing the proof graph and/or by exploiting standard logic synthesis techniques. Furthermore, strengthening and weakening have been studied as options to control ITP quality. In this paper,1 we propose an SAT-based ITP weakening/strengthening technique, for ITP compaction, where the UNSAT core extracted from an additional SAT query is used to obtain a gate-level abstraction of the ITP. The abstraction introduces fresh new variables at gate cuts that must be quantified out in order to obtain a valid ITP. We show how to efficiently quantify them out, by working on a negation normal form representation of the circuit. This paper includes an experimental evaluation, showing the benefits of the proposed approach, on a set of benchmark ITPs arising from hardware model checking problems.

We address the problem of reducing the size of Craig's interpolants used in SAT-based model checking. Craig's interpolants are AND-OR circuits, generated by post-processing refutation proofs of SAT solvers. Being highly redundant, their compaction is typically tackled by reducing the proof graph and/or by exploiting standard logic synthesis techniques. In this paper, we propose a set of ad-hoc logic synthesis functions that, revisiting known logic synthesis approaches, specifically address speed and scalability. Though general and not restricted to interpolants, these techniques target the main sources of redundancy in combinational circuits. This paper includes an experimental evaluation, showing the benefits of the proposed techniques, on a set of benchmark interpolants arising from hardware model checking problems.

Modern devices often include several embedded instruments, such as BIST interfaces, sensors, calibration facilities. New standards, such as IEEE Std 1687, provide vehicles to access these instruments. In approaches based on reconfigurable scan networks (RSNs), instruments are coupled with scan registers, connected into chains and interleaved with reconfigurable modules. Such modules embed reconfigurable multiplexers that permit a selective access to different parts of the chain. A similar scenario is also supported by IEEE Std 1149.1-2013. The test of permanent faults affecting an RSN requires to shift test vectors throughout a certain number of network configurations. This paper presents some methodologies to select the list of configurations that perform the complete test of the reconfigurable modules of the RSN. In particular, one method is presented that, by construction, can be proved to be able to apply the test in the minimum amount of clock cycles. Other methods are sub-optimal in terms of test application time (TAT), but scale well on large circuits. In order to provide a comparison between the proposed methods, experimental results on some benchmark RSNs are provided.

Modern devices often include several embedded instruments, such as BISTs, sensors, and other analog components. New standards, such as IEEE Std. 1687, provide vehicles to access these instruments. In approaches based on reconfigurable scan networks, instruments are coupled with scan registers, connected into chains and interleaved with reconfigurable multiplexers, permitting a selective access to different parts of the chain. A similar scenario is also supported by IEEE Std. 1149.1-2013, where a test data register can be constructed as a chain of multiple segments, some of which can be excluded or mutually selected. The test of permanent faults affecting a reconfigurable scan network requires to shift test patterns throughout a certain number of network configurations. This paper presents a method to select the list of configurations needed to apply the complete test set in the minimum amount of clock cycles. The method is based on a graph representation ofthe problem. Experimental results on some benchmark networks are provided, together with a comparison with other approaches based on heuristics. The provided results can be effectively usedto evaluate the test time of sub-optimal approaches.

This paper presents a simple 7/2-approximation algorithm for the Maximum Duo-Preservation String Mapping (MPSM) problem. This problem is complementary to the classical and well studied min common string partition problem (MCSP), that computes the minimal edit distance between two strings when the only operation allowed is to shift blocks of characters. The algorithm improves on the previously best-known 4-approximation algorithm by computing a simple local optimum.

We address the problem of reducing the size of Craig interpolants used in SAT-based Model Checking. Craig interpolants are AND-OR circuits, generated by post-processing refutation proofs of SAT solvers. Whereas it is well known that interpolants are highly redundant, their compaction is typically tackled by reducing the proof graph and/or by exploiting standard logic synthesis techniques. Furthermore, strengthening and weakening have been studied as an option to control interpolant quality. In this paper we propose two interpolant compaction techniques: (1) A set of ad-hoc logic synthesis functions that, revisiting known logic synthesis approaches, specifically address speed and scalability. Though general and not restricted to interpolants, these techniques target the main sources of redundancy in interpolant circuits. (2) An interpolant weakening technique, where the UNSAT core extracted from an additional SAT query is used to obtain a gate-level abstraction of the interpolant. The abstraction introduces fresh new variables at gate cuts that must be quantified out in order to obtain a valid interpolant. We show how to efficiently quantify them out, by working on an NNF representation of the circuit. The paper includes an experimental evaluation, showing the benefits of the proposed techniques, on a set of benchmark interpolants arising from both hardware and software model checking problems.

This paper addresses model checking based on SAT solvers and Craig interpolants. We tackle major scalability problems of state-of-the-art interpolation-based approaches, and we achieve two main results: (1) a novel model checking algorithm; (2) a new and flexible way to handle an incremental representation of (over-approximated) forward reachable states. The new model checking algorithm (IGR: Interpolation with Guided Refinement), partially takes inspiration from IC3 and interpolation sequences. It bases its robustness and scalability on incremental refinement of state sets, and guided unwinding/simplification of transition relation unrollings. State sets, the central data structure of our algorithm, are incrementally refined, and they represent a valuable information to be shared among related problems, either in concurrent or sequential (multiple-engine or multiple property) execution schemes. We provide experimental data, showing that IGR extends the capability of a state-of-the-art model checker, with a specific focus on hard-to-prove properties.

This paper introduces a new technique for a fast computation of the Cone-Of-Influence (COI) of multiple properties. It specifically addresses frameworks where multiple properties belongs to the same model, and they partially or fully share their COI. In order to avoid multiple repeated visits of the same circuit sub-graph representation, it proposes a new algorithm, which performs a single topological visit of the variable dependency graph. It also studies mutual relationships among different properties, based on the overlapping of their COIs. It finally considers state variable scoring, based on their own COIs and/or their appearance in multiple COIs, as a new statistic for variable sorting and grouping/clustering in various Model Checking algorithms. Preliminary results show the advantages, and potential applications of these ideas.