Experiences in Prolog-Based DFT Rule Checking. - Gianpiero Cabodi; Paolo Camurati; Paolo Prinetto (FJCC, 1986)

A functional approach to formal hardware verification: the MTI experience. - Dominique Borrione; Paolo Camurati; J. L. Paillet; Paolo Prinetto (ICCD, 1988)

Random testability analysis: comparing and evaluating existing approaches. - Paolo Camurati; Paolo Prinetto; Matteo Sonza Reorda (ICCD, 1988)

Formal Verification of Hardware Correctness: Introduction and Survey of Current Research. - Paolo Camurati; Paolo Prinetto (Computer, 1988)

ESTA: an expert system for DFT rule verification. - Paolo Camurati; Paolo Gianoglio; Renato Gianoglio; Paolo Prinetto (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1988)

Expressing logical and temporal conditions in simulation environments: TPDL*. - Gianpiero Cabodi; Paolo Camurati; Paolo Prinetto; Matteo Sonza Reorda (Microprocessing and Microprogramming, 1989)

Systolic array description in F2. - Paolo Camurati; Tiziana Margaria; Paolo Prinetto (Microprocessing and Microprogramming, 1989)

Knowledge-based systems as an aid to computer-aided repair. - Paolo Camurati; Marco Mezzalama; Paolo Prinetto (Microprocess. Microsystems, 1989)

The Use of Model Checking in ATPG for Sequential Circuits. - Paolo Camurati; Marco Gilli; Paolo Prinetto; Matteo Sonza Reorda (CAV, 1990)

Model Checking and Graph Theory in Sequential ATPG. - Paolo Camurati; Marco Gilli; Paolo Prinetto; Matteo Sonza Reorda (CAV (DIMACS/AMS volume), 1990)

Diagnosis oriented test pattern generation. - Paolo Camurati; Antonio Lioy; Paolo Prinetto; Matteo Sonza Reorda (EURO-DAC, 1990)

A diagnostic test pattern generation algorithm. - Paolo Camurati; Davide Medina; Paolo Prinetto; Matteo Sonza Reorda (ITC, 1990)

Exact probabilistic testability measures for multi-output circuits. - Paolo Camurati; Paolo Prinetto; Matteo Sonza Reorda (J. Electron. Test., 1990)

Assessing the diagnostic power of test pattern sets. - Paolo Camurati; Antonio Lioy; Paolo Prinetto; Matteo Sonza Reorda (Microprocessing and Microprogramming, 1990)

The OTTER environment for resolution-based proof of hardware correctness. - Paolo Camurati; Tiziana Margaria; Paolo Prinetto (Microprocessing and Microprogramming, 1990)

Resolution-based correctness proofs of synchronous circuits. - Paolo Camurati; Tiziana Margaria; Paolo Prinetto (EURO-DAC, 1991)

Proving finite state machines correct with an automaton-based method. - Paolo Camurati; Marco Gilli; Paolo Prinetto; Matteo Sonza Reorda (Great Lakes Symposium on VLSI, 1991)

TPDL: Extended Temporal Profile Description Language. - Gianpiero Cabodi; Paolo Camurati; Paolo Prinetto; Matteo Sonza Reorda (Softw. Pract. Exp., 1991)

A New Model for Improving symbolic Product Machine Traversal. - Gianpiero Cabodi; Paolo Camurati; Fulvio Corno; Silvano Gai; Paolo Prinetto; Matteo Sonza Reorda (DAC, 1992)

Cross-fertilizing FSM verification techniques and sequential diagnosis. - Gianpiero Cabodi; Paolo Camurati; Fulvio Corno; Paolo Prinetto; Matteo Sonza Reorda (EURO-DAC, 1992)

Sequential Circuit Diagnosis Based on Formal Verification Techniques. - Gianpiero Cabodi; Paolo Camurati; Fulvio Corno; Paolo Prinetto; Matteo Sonza Reorda (ITC, 1992)

A simulation-based approach to test pattern generation for synchronous sequential circuits. - Paolo Camurati; Fulvio Corno; Fulvio Prinetto; Matteo Sonza Reorda (VTS, 1992)

Advancements in Symbolic Traversal Technique. - Gianpiero Cabodi; Paolo Camurati (CHARME, 1993)

A Methodology for System-Level Design for Verifiability. - Paolo Camurati; Fulvio Corno; Paolo Prinetto (CHARME, 1993)

Exploiting Symbolic Traversal Techniques for Efficient Process Algebra Manipulation. - Paolo Camurati; Fulvio Corno; Paolo Prinetto (CHDL, 1993)

An efficient tool for system-level verification of behaviors and temporal properties. - Paolo Camurati; Fulvio Corno; Paolo Prinetto (EURO-DAC, 1993)

Exploiting Cofactoring for Efficient FSM Symbolic Traversal Based on the Transition Relation. - Gianpiero Cabodi; Paolo Camurati (ICCD, 1993)

An approach to sequential circuit diagnosis based on formal verification techniques. - Gianpiero Cabodi; Paolo Camurati; Fulvio Corno; Paolo Prinetto; Matteo Sonza Reorda (J. Electron. Test., 1993)

Auxiliary Variables for Extending Symbolic Traversal Techniques to Data Paths. - Gianpiero Cabodi; Paolo Camurati; Stefano Quer (DAC, 1994)

Symbolic exploration of large circuits with enhanced forward/backward traversals. - Gianpiero Cabodi; Paolo Camurati; Stefano Quer (EURO-DAC, 1994)

System-Level Modeling and Verification: a Comprehensive Design Methodology. - Paolo Camurati; Fulvio Corno; Paolo Prinetto; Catherine Bayol; Bernard Soulas (EDAC-ETC-EUROASIC, 1994)

Symbolic traversals of data paths with auxiliary variables. - Gianpiero Cabodi; Paolo Camurati; Stefano Quer (Great Lakes Symposium on VLSI, 1994)

Efficient State Space Pruning in Symbolic Backward Traversal. - Gianpiero Cabodi; Paolo Camurati; Stefano Quer (ICCD, 1994)

Detecting hard faults with combined approximate forward/backward symbolic techniques. - Gianpiero Cabodi; Paolo Camurati; Stefano Quer (ISCAS, 1994)

Full-Symbolic ATPG for Large Circuits. - Gianpiero Cabodi; Paolo Camurati; Stefano Quer (ITC, 1994)

A new functional fault model for system-level descriptions. - Paolo Camurati; Fulvio Corno; Michela Meo; Paolo Prinetto (VTS, 1994)

An industrial experience in the built-in self test of embedded RAMs. - Paolo Camurati; Paolo Prinetto; Matteo Sonza Reorda; Stefano Barbagallo; Andrea Burri; Davide Medina (VTS, 1994)

Transforming boolean relations by symbolic encoding. - Gianpiero Cabodi; Stefano Quer; Paolo Camurati (CHARME, 1995)

Computing subsets of equivalence classes for large FSMs. - Gianpiero Cabodi; Stefano Quer; Paolo Camurati (EURO-DAC, 1995)

Industrial BIST of Embedded RAMs. - Paolo Camurati; Paolo Prinetto; Matteo Sonza Reorda; Stefano Barbagallo; Andrea Burri; Davide Medina (IEEE Des. Test Comput., 1995)

Incremental re-encoding for symbolic traversal of product machines. - Gianpiero Cabodi; Paolo Camurati; Luciano Lavagno; Stefano Quer; Robert K. Brayton; Ellen Sentovich (EURO-DAC, 1996)

Decomposed symbolic forward traversals of large finite state machines. - Stefano Quer; Gianpiero Cabodi; Paolo Camurati (EURO-DAC, 1996)

Improved reachability analysis of large finite state machines. - Gianpiero Cabodi; Paolo Camurati; Stefano Quer (ICCAD, 1996)

Enhancing FSM Traversal by Temporary Re-Encoding. - Gianpiero Cabodi; Luciano Lavagno; Enrico Macii; Massimo Poncino; Stefano Quer; Paolo Camurati; Ellen Sentovich (ICCD, 1996)

A parallel approach to symbolic traversal based on set partitioning. - Gianpiero Cabodi; Paolo Camurati; Antonio Lioy; Massimo Poncino; Stefano Quer (CHARME, 1997)

Disjunctive Partitioning and Partial Iterative Squaring: An Effective Approach for Symbolic Traversal of Large Circuits. - Gianpiero Cabodi; Paolo Camurati; Luciano Lavagno; Stefano Quer (DAC, 1997)

Verification and synthesis of counters based on symbolic techniques. - Gianpiero Cabodi; Paolo Camurati; Luciano Lavagno; Stefano Quer (ED&TC, 1997)

Symbolic FSM traversals based on the transition relation. - Gianpiero Cabodi; Paolo Camurati (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1997)

The General Product Machine: a New Model for Symbolic FSM Traversal. - Gianpiero Cabodi; Paolo Camurati; Fulvio Corno; Paolo Prinetto; Matteo Sonza Reorda (Formal Methods Syst. Des., 1998)

Memory Optimization in Function and Set Manipulation with BDDs. - Gianpiero Cabodi; Stefano Quer; Paolo Camurati (Softw. Pract. Exp., 1998)

Auxiliary variables for BDD-based representation and manipulation of Boolean functions. - Gianpiero Cabodi; Paolo Camurati; Stefano Quer (ACM Trans. Design Autom. Electr. Syst., 1998)

Improving Symbolic Traversals by Means of Activity Profiles. - Gianpiero Cabodi; Paolo Camurati; Stefano Quer (DAC, 1999)

Computing Timed Transition Relations for Sequential Cycle-Based Simulation. - Gianpiero Cabodi; Paolo Camurati; Claudio Passerone; Stefano Quer (DATE, 1999)

Improving the efficiency of BDD-based operators by means of partitioning. - Gianpiero Cabodi; Paolo Camurati; Stefano Quer (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1999)

Verification of Similar FSMs by Mixing Incremental Re-encoding, Reachability Analysis, and Combinational Checks. - Stefano Quer; Gianpiero Cabodi; Paolo Camurati; Luciano Lavagno; Ellen Sentovich; Robert K. Brayton (Formal Methods Syst. Des., 2000)

Symbolic forward/backward traversals of large finite state machines. - Gianpiero Cabodi; Paolo Camurati; Stefano Quer (J. Syst. Archit., 2000)

Improving symbolic reachability analysis by means of activityprofiles. - Gianpiero Cabodi; Paolo Camurati; Stefano Quer (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2000)

Biasing symbolic search by means of dynamic activity profiles. - Gianpiero Cabodi; Paolo Camurati; Stefano Quer (DATE, 2001)

Reachability analysis of large circuits using disjunctive partitioning and partial iterative squaring. - Gianpiero Cabodi; Paolo Camurati; Stefano Quer (J. Syst. Archit., 2001)

Can BDDs compete with SAT solvers on bounded model checking? - Gianpiero Cabodi; Paolo Camurati; Stefano Quer (DAC, 2002)

Dynamic Scheduling and Clustering in Symbolic Image Computation. - Gianpiero Cabodi; Paolo Camurati; Stefano Quer (DATE, 2002)

Trading-Off SAT Search and Variable Quantifications for Effective Unbounded Model Checking. - Gianpiero Cabodi; Paolo Camurati; Luz Amanda Garcia; Marco Murciano; Sergio Nocco; Stefano Quer (FMCAD, 2008)

Automated abstraction by incremental refinement in interpolant-based model checking. - Gianpiero Cabodi; Paolo Camurati; Marco Murciano (ICCAD, 2008)

Speeding up model checking by exploiting explicit and hidden verification constraints. - Gianpiero Cabodi; Paolo Camurati; Luz Amanda Garcia; Marco Murciano; Sergio Nocco; Stefano Quer (DATE, 2009)

A 7/2-Approximation Algorithm for the Maximum Duo-Preservation String Mapping Problem. - Nicolas Boria; Gianpiero Cabodi; Paolo Camurati; Marco Palena; Paolo Pasini; Stefano Quer (CPM, 2016)

Reducing interpolant circuit size by ad-hoc logic synthesis and SAT-based weakening. - Gianpiero Cabodi; Paolo Camurati; Marco Palena; Paolo Pasini; Danilo Vendraminetto (FMCAD, 2016)

Secure Path Verification. - Gianpiero Cabodi; Paolo Camurati; Sebastiano F. Finocchiaro; Carmelo Loiacono; Francesco Savarese; Danilo Vendraminetto (IVSW, 2016)

A Greedy Approach to Answer Reachability Queries on DAGs. - Nicolas Boria; Gianpiero Cabodi; Paolo Camurati; Marco Palena; Paolo Pasini; Stefano Quer (CoRR, 2016)

A graph-labeling approach for efficient cone-of-influence computation in model-checking problems with multiple properties. - Gianpiero Cabodi; Paolo Camurati; Stefano Quer (Softw. Pract. Exp., 2016)

Interpolation-Based Learning as a Mean to Speed-Up Bounded Model Checking (Short Paper). - Gianpiero Cabodi; Paolo Camurati; Marco Palena; Paolo Pasini; Danilo Vendraminetto (SEFM, 2017)

Embedded Systems Secure Path Verification at the Hardware/Software Interface. - Gianpiero Cabodi; Paolo Camurati; Sebastiano F. Finocchiaro; Francesco Savarese; Danilo Vendraminetto (IEEE Des. Test, 2017)

SAT solver management strategies in IC3: an experimental approach. - Gianpiero Cabodi; Paolo Camurati; Alan Mishchenko; Marco Palena; Paolo Pasini (Formal Methods Syst. Des., 2017)

To split or to group: from divide-and-conquer to sub-task sharing for verifying multiple properties in model checking. - Gianpiero Cabodi; Paolo Camurati; Carmelo Loiacono; Marco Palena; Paolo Pasini; Denis Patti; Stefano Quer (Int. J. Softw. Tools Technol. Transf., 2018)

Model Checking Speculation-Dependent Security Properties: Abstracting and Reducing Processor Models for Sound and Complete Verification. - Gianpiero Cabodi; Paolo Camurati; Fabrizio F. Finocchiaro; Danilo Vendraminetto (C2SI, 2019)

KPIs for Optimal Location of charging stations for Electric Vehicles: the Biella case-study. - Edoardo Fadda; Daniele Manerba; Roberto Tadei; Paolo Camurati; Gianpiero Cabodi (FedCSIS, 2019)

Logic Synthesis for Interpolant Circuit Compaction. - Gianpiero Cabodi; Paolo Camurati; Marco Palena; Paolo Pasini; Danilo Vendraminetto (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2019)

Reducing Interpolant Circuit Size Through SAT-Based Weakening. - Gianpiero Cabodi; Paolo Camurati; Marco Palena; Paolo Pasini; Danilo Vendraminetto (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2020)

Optimizing Binary Decision Diagrams for Interpretable Machine Learning Classification. - Gianpiero Cabodi; Paolo E. Camurati; Alexey Ignatiev; João Marques-Silva 001; Marco Palena; Paolo Pasini (DATE, 2021)

Interpolation with guided refinement: revisiting incrementality in SAT-based unbounded model checking. - Gianpiero Cabodi; Paolo E. Camurati; Marco Palena; Paolo Pasini (Formal Methods Syst. Des., 2022)

Improving Bounded Model Checking Exploiting Interpolation-Based Learning and Strengthening. - Gianpiero Cabodi; Paolo E. Camurati; Marco Palena; Paolo Pasini (IEEE Access, 2024)

Hardware Model Checking Algorithms and Techniques. - Gianpiero Cabodi; Paolo E. Camurati; Marco Palena; Paolo Pasini (Algorithms, 2024)

Optimizing Binary Decision Diagrams for Interpretable Machine Learning Classification. - Gianpiero Cabodi; Paolo E. Camurati; João Marques-Silva 001; Marco Palena; Paolo Pasini (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2024)

A Theorem Prover Based Approach for SAT-Based Model Checking Certification. - Giulia Sindoni; Paolo Pasini; Gianpiero Cabodi; Paolo E. Camurati; Alberto Griggio; Marco Palena; Marco Roveri; Stefano Tonetta (CADE, 2025)