Gianpiero Cabodi

Fabrizio F. Finocchiaro

Proceedings of the Codes, Cryptology and Information Security, 2019

2018

To split or to group: from divide-and-conquer to sub-task sharing for verifying multiple properties in model checking.

[BibT_eX]

[DOI]

Int. J. Softw. Tools Technol. Transf., 2018

2017

Efficient Complex High-Precision Computations on GPUs without Precision Loss.

[BibT_eX]

[DOI]

J. Circuits Syst. Comput., 2017

SAT solver management strategies in IC3: an experimental approach.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2017

Deep Classifiers-Based License Plate Detection, Localization and Recognition on GPU-Powered Mobile Platform.

[BibT_eX]

[DOI]

Syed Tahir Hussain Rizvi

Future Internet, 2017

Embedded Systems Secure Path Verification at the Hardware/Software Interface.

[BibT_eX]

[DOI]

Sebastiano F. Finocchiaro

Francesco Savarese

IEEE Des. Test, 2017

Interpolation-Based Learning as a Mean to Speed-Up Bounded Model Checking (Short Paper).

[BibT_eX]

[DOI]

Proceedings of the Software Engineering and Formal Methods - 15th International Conference, 2017

GPU-only unified ConvMM layer for neural classifiers.

[BibT_eX]

[DOI]

Syed Tahir Hussain Rizvi

Gianluca Francini

Proceedings of the 4th International Conference on Control, 2017

2016

A graph-labeling approach for efficient cone-of-influence computation in model-checking problems with multiple properties.

[BibT_eX]

[DOI]

Softw. Pract. Exp., 2016

A Greedy Approach to Answer Reachability Queries on DAGs.

[BibT_eX]

[DOI]

CoRR, 2016

Secure Path Verification.

[BibT_eX]

[DOI]

Sebastiano F. Finocchiaro

Carmelo Loiacono

Francesco Savarese

Proceedings of the 1st IEEE International Verification and Security Workshop, 2016

Scalable FPGA graph model to detect routing faults.

[BibT_eX]

[DOI]

Luca Sterpone

Sebastiano F. Finocchiaro

Carmelo Loiacono

Francesco Savarese

Boyang Du

Proceedings of the 22nd IEEE International Symposium on On-Line Testing and Robust System Design, 2016

Reducing interpolant circuit size by ad-hoc logic synthesis and SAT-based weakening.

[BibT_eX]

[DOI]

Proceedings of the 2016 Formal Methods in Computer-Aided Design, 2016

A 7/2-Approximation Algorithm for the Maximum Duo-Preservation String Mapping Problem.

[BibT_eX]

[DOI]

Proceedings of the 27th Annual Symposium on Combinatorial Pattern Matching, 2016

Gabor filter based image representation for object classification.

[BibT_eX]

[DOI]

Syed Tahir Hussain Rizvi

Pedro P. B. de Gusmao

Gianluca Francini

Proceedings of the International Conference on Control, 2016

2015

Optimization techniques for craig interpolant compaction in unbounded model checking.

[BibT_eX]

[DOI]

Carmelo Loiacono

Formal Methods Syst. Des., 2015

2014

Hardware Model Checking Competition 2014: An Analysis and Comparison of Solvers and Benchmarks.

[BibT_eX]

[DOI]

J. Satisf. Boolean Model. Comput., 2014

Interpolation with Guided Refinement: Revisiting incrementality in SAT-based unbounded model checking.

[BibT_eX]

[DOI]

Marco Palena

Paolo Pasini

Proceedings of the Formal Methods in Computer-Aided Design, 2014

Tightening BDD-based approximate reachability with SAT-based clause generalization<sup>∗</sup>.

[BibT_eX]

[DOI]

Proceedings of the Design, Automation & Test in Europe Conference & Exhibition, 2014

2013

Thread-based multi-engine model checking for multicore platforms.

[BibT_eX]

[DOI]

ACM Trans. Design Autom. Electr. Syst., 2013

Trading-off Incrementality and Dynamic Restart of Multiple Solvers in IC3.

[BibT_eX]

[DOI]

Marco Palena

Alan Mishchenko

Proceedings of the Second International Workshop on Design and Implementation of Formal Tools and Systems, 2013

2011

Benchmarking a model checker for algorithmic improvements and tuning for performance.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2011

Interpolation sequences revisited.

[BibT_eX]

[DOI]

Proceedings of the Design, Automation and Test in Europe, 2011

Optimized model checking of multiple properties.

[BibT_eX]

[DOI]

Proceedings of the Design, Automation and Test in Europe, 2011

2010

Speeding-up heuristic allocation, scheduling and binding with SAT-based abstraction/refinement techniques.

[BibT_eX]

[DOI]

ACM Trans. Design Autom. Electr. Syst., 2010

Boosting software fault injection for dependability analysis of real-time embedded applications.

[BibT_eX]

[DOI]

Marco Murciano

Massimo Violante

ACM Trans. Embed. Comput. Syst., 2010

Partitioning Interpolant-Based Verification for Effective Unbounded Model Checking.

[BibT_eX]

[DOI]

IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2010

Finding Multiple Equivalence-Preserving Transformations in Combinational Circuits through Incremental-SAT.

[BibT_eX]

[DOI]

J. Electron. Test., 2010

2009

Strengthening Model Checking Techniques With Inductive Invariants.

[BibT_eX]

[DOI]

IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2009

Exploiting incrementality in SAT-based search for multiple equivalence-preserving transformations in combinational circuits.

[BibT_eX]

[DOI]

Proceedings of the IEEE International High Level Design Validation and Test Workshop, 2009

Speeding up model checking by exploiting explicit and hidden verification constraints.

[BibT_eX]

[DOI]

Proceedings of the Design, Automation and Test in Europe, 2009

2008

Boosting interpolation with dynamic localized abstraction and redundancy removal.

[BibT_eX]

[DOI]

ACM Trans. Design Autom. Electr. Syst., 2008

Automated abstraction by incremental refinement in interpolant-based model checking.

[BibT_eX]

[DOI]

Marco Murciano

Proceedings of the 2008 International Conference on Computer-Aided Design, 2008

Trading-Off SAT Search and Variable Quantifications for Effective Unbounded Model Checking.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods in Computer-Aided Design, 2008

2007

A Compositional Approach for Equivalence Checking of Sequential Circuits with Unknown Reset State and Overlapping Partitions.

[BibT_eX]

[DOI]

Gabriel P. Bischoff

Karl S. Brace

Proceedings of the Computer Aided Systems Theory, 2007

Boosting the role of inductive invariants in model checking.

[BibT_eX]

[DOI]

Proceedings of the 2007 Design, Automation and Test in Europe Conference and Exposition, 2007

2006

BDD-Based Hardware Verification.

[BibT_eX]

[DOI]

Marco Murciano

Proceedings of the Formal Methods for Hardware Verification, 2006

Stepping forward with interpolants in unbounded model checking.

[BibT_eX]

[DOI]

Proceedings of the 2006 International Conference on Computer-Aided Design, 2006

2005

Are BDDs still alive within sequential verification?

[BibT_eX]

[DOI]

Int. J. Softw. Tools Technol. Transf., 2005

A BMC-based formulation for the scheduling problem of hardware systems.

[BibT_eX]

[DOI]

Int. J. Softw. Tools Technol. Transf., 2005

Circuit Based Quantification: Back to State Set Manipulation within Unbounded Model Checking.

[BibT_eX]

[DOI]

Proceedings of the 2005 Design, 2005

2004

Improving SAT-based Bounded Model Checking by Means of BDD-based Approximate Traversals.

[BibT_eX]

[DOI]

J. Univers. Comput. Sci., 2004

Exploiting Target Enlargement and Dynamic Abstraction within Mixed BDD and SAT Invariant Checking.

[BibT_eX]

[DOI]

Proceedings of the 2nd International Workshop on Bounded Model Checking, 2004

2003

A BMC-formulation for the scheduling problem in highly constrained hardware Systems.

[BibT_eX]

[DOI]

Proceedings of the First International Workshop on Bounded Model Checking, 2003

2002

A Symbolic Approach for the Combined Solution of Scheduling and Allocation.

[BibT_eX]

[DOI]

Proceedings of the 15th International Symposium on System Synthesis (ISSS 2002), 2002

Dynamic Scheduling and Clustering in Symbolic Image Computation.

[BibT_eX]

[DOI]

Proceedings of the 2002 Design, 2002

Can BDDs compete with SAT solvers on bounded model checking?

[BibT_eX]

[DOI]

Proceedings of the 39th Design Automation Conference, 2002

Mixing Forward and Backward Traversals in Guided-Prioritized BDD-Based Verification.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 14th International Conference, 2002

2001

Reachability analysis of large circuits using disjunctive partitioning and partial iterative squaring.

[BibT_eX]

[DOI]

J. Syst. Archit., 2001

Biasing symbolic search by means of dynamic activity profiles.

[BibT_eX]

[DOI]

Proceedings of the Conference on Design, Automation and Test in Europe, 2001

Meta-BDDs: A Decomposed Representation for Layered Symbolic Manipulation of Boolean Functions.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 13th International Conference, 2001

2000

Improving symbolic reachability analysis by means of activityprofiles.

[BibT_eX]

[DOI]

IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2000

Symbolic forward/backward traversals of large finite state machines.

[BibT_eX]

[DOI]

J. Syst. Archit., 2000

Verification of Similar FSMs by Mixing Incremental Re-encoding, Reachability Analysis, and Combinational Checks.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2000

Optimizing sequential verification by retiming transformations.

[BibT_eX]

[DOI]

Fabio Somenzi

Proceedings of the 37th Conference on Design Automation, 2000

1999

Improving the efficiency of BDD-based operators by means of partitioning.

[BibT_eX]

[DOI]

IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1999

Computing Timed Transition Relations for Sequential Cycle-Based Simulation.

[BibT_eX]

[DOI]

Proceedings of the 1999 Design, 1999

Improving Symbolic Traversals by Means of Activity Profiles.

[BibT_eX]

[DOI]

Proceedings of the 36th Conference on Design Automation, 1999

1998

Binary Decision Diagrams and the Multiple Variable Order Problem

[BibT_eX]

Universität Trier, Mathematik/Informatik, Forschungsbericht, 1998

Auxiliary variables for BDD-based representation and manipulation of Boolean functions.

[BibT_eX]

[DOI]

ACM Trans. Design Autom. Electr. Syst., 1998

Memory Optimization in Function and Set Manipulation with BDDs.

[BibT_eX]

[DOI]

Softw. Pract. Exp., 1998

The General Product Machine: a New Model for Symbolic FSM Traversal.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 1998

1997

Symbolic FSM traversals based on the transition relation.

[BibT_eX]

[DOI]

IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1997

Verification and synthesis of counters based on symbolic techniques.

[BibT_eX]

[DOI]

Proceedings of the European Design and Test Conference, 1997

Disjunctive Partitioning and Partial Iterative Squaring: An Effective Approach for Symbolic Traversal of Large Circuits.

[BibT_eX]

[DOI]

Proceedings of the 34st Conference on Design Automation, 1997

A parallel approach to symbolic traversal based on set partitioning.

[BibT_eX]

Proceedings of the Advances in Hardware Design and Verification, 1997

1996

Enhancing FSM Traversal by Temporary Re-Encoding.

[BibT_eX]

[DOI]

Proceedings of the 1996 International Conference on Computer Design (ICCD '96), 1996

Improved reachability analysis of large finite state machines.

[BibT_eX]

[DOI]

Proceedings of the 1996 IEEE/ACM International Conference on Computer-Aided Design, 1996

Decomposed symbolic forward traversals of large finite state machines.

[BibT_eX]

[DOI]

Proceedings of the conference on European design automation, 1996

Incremental re-encoding for symbolic traversal of product machines.

[BibT_eX]

[DOI]

Proceedings of the conference on European design automation, 1996

1995

Computing subsets of equivalence classes for large FSMs.

[BibT_eX]

[DOI]

Proceedings of the Proceedings EURO-DAC'95, 1995

Transforming boolean relations by symbolic encoding.

[BibT_eX]

[DOI]

Proceedings of the Correct Hardware Design and Verification Methods, 1995

1994

A BDD Package For A Massively Parallel SIMD Architecture.

[BibT_eX]

[DOI]

Proceedings of the Second Euromicro Workshop on Parallel and Distributed Processing, 1994

Full-Symbolic ATPG for Large Circuits.

[BibT_eX]

[DOI]

Proceedings of the Proceedings IEEE International Test Conference 1994, 1994

Detecting hard faults with combined approximate forward/backward symbolic techniques.

[BibT_eX]

[DOI]

Proceedings of the 1994 IEEE International Symposium on Circuits and Systems, ISCAS 1994, London, England, UK, May 30, 1994

Efficient State Space Pruning in Symbolic Backward Traversal.

[BibT_eX]

[DOI]

Proceedings of the Proceedings 1994 IEEE International Conference on Computer Design: VLSI in Computer & Processors, 1994

Symbolic traversals of data paths with auxiliary variables.

[BibT_eX]

[DOI]

Proceedings of the Fourth Great Lakes Symposium on Design Automation of High Performance VLSI Systems, 1994

Symbolic exploration of large circuits with enhanced forward/backward traversals.

[BibT_eX]

[DOI]

Proceedings of the Proceedings EURO-DAC'94, 1994

Auxiliary Variables for Extending Symbolic Traversal Techniques to Data Paths.

[BibT_eX]

[DOI]

Proceedings of the 31st Conference on Design Automation, 1994

1993

A Parallel System for Test Pattern Generation.

[BibT_eX]

[DOI]

Parallel Comput., 1993

An approach to sequential circuit diagnosis based on formal verification techniques.

[BibT_eX]

[DOI]

J. Electron. Test., 1993

Exploiting Cofactoring for Efficient FSM Symbolic Traversal Based on the Transition Relation.

[BibT_eX]

[DOI]

Proceedings of the Proceedings 1993 International Conference on Computer Design: VLSI in Computers & Processors, 1993

Advancements in Symbolic Traversal Technique.

[BibT_eX]

[DOI]

Proceedings of the Correct Hardware Design and Verification Methods, 1993

1992

Sequential Circuit Diagnosis Based on Formal Verification Techniques.

[BibT_eX]

[DOI]

Proceedings of the Proceedings IEEE International Test Conference 1992, 1992

Cross-fertilizing FSM verification techniques and sequential diagnosis.

[BibT_eX]

[DOI]

Proceedings of the conference on European design automation, 1992

A New Model for Improving symbolic Product Machine Traversal.

[BibT_eX]

[DOI]

Proceedings of the 29th Design Automation Conference, 1992

1991

TPDL: Extended Temporal Profile Description Language.

[BibT_eX]

[DOI]

Softw. Pract. Exp., 1991

A parallel system for test pattern generation.

[BibT_eX]

[DOI]

Proceedings of the Third IEEE Symposium on Parallel and Distributed Processing, 1991

Fast Differential Fault Simulation by Dynamic Fault Ordering.

[BibT_eX]

[DOI]

Silvano Gai

Matteo Sonza Reorda

Proceedings of the Proceedings 1991 IEEE International Conference on Computer Design: VLSI in Computer & Processors, 1991

1990

A transputer-based gate-level fault simulator.

[BibT_eX]

[DOI]

Silvano Gai

Matteo Sonza Reorda

Microprocessing and Microprogramming, 1990

1989

Expressing logical and temporal conditions in simulation environments: TPDL<sup>*</sup>.

[BibT_eX]

[DOI]

Microprocessing and Microprogramming, 1989

1988

Fault simulation in a multilevel environment: the MOZART approach.

[BibT_eX]

[DOI]

Proceedings of the Eighteenth International Symposium on Fault-Tolerant Computing, 1988

1986

Experiences in Prolog-Based DFT Rule Checking.

[BibT_eX]