Gianpiero Cabodi

105 papers A* 8A 18B 6C 10Journal 41Unranked 22

Year	Rank	Type	Title / Venue / Authors
2025	A	`conf`	A Theorem Prover Based Approach for SAT-Based Model Checking Certification. CADE Giulia Sindoni, Paolo Pasini, Gianpiero Cabodi, Paolo E. Camurati, Alberto Griggio, Marco Palena, Marco Roveri, Stefano Tonetta
2024	J	`jnl`	Hardware Model Checking Algorithms and Techniques. Algorithms Gianpiero Cabodi, Paolo E. Camurati, Marco Palena, Paolo Pasini
2024	J	`jnl`	Improving Bounded Model Checking Exploiting Interpolation-Based Learning and Strengthening. IEEE Access Gianpiero Cabodi, Paolo E. Camurati, Marco Palena, Paolo Pasini
2024	J	`jnl`	Optimizing Binary Decision Diagrams for Interpretable Machine Learning Classification. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. Gianpiero Cabodi, Paolo E. Camurati, João Marques-Silva, Marco Palena, Paolo Pasini
2022	J	`jnl`	Interpolation with guided refinement: revisiting incrementality in SAT-based unbounded model checking. Formal Methods Syst. Des. Gianpiero Cabodi, Paolo E. Camurati, Marco Palena, Paolo Pasini
2021	A	`conf`	Optimizing Binary Decision Diagrams for Interpretable Machine Learning Classification. DATE Gianpiero Cabodi, Paolo E. Camurati, Alexey Ignatiev, João Marques-Silva, Marco Palena, Paolo Pasini
2020	J	`jnl`	Reducing Interpolant Circuit Size Through SAT-Based Weakening. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. Gianpiero Cabodi, Paolo Camurati, Marco Palena, Paolo Pasini, Danilo Vendraminetto
2019	C	`conf`	KPIs for Optimal Location of charging stations for Electric Vehicles: the Biella case-study. FedCSIS Edoardo Fadda, Daniele Manerba, Roberto Tadei, Paolo Camurati, Gianpiero Cabodi
2019	J	`jnl`	Logic Synthesis for Interpolant Circuit Compaction. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. Gianpiero Cabodi, Paolo Camurati, Marco Palena, Paolo Pasini, Danilo Vendraminetto
2019	—	`conf`	Model Checking Speculation-Dependent Security Properties: Abstracting and Reducing Processor Models for Sound and Complete Verification. C2SI Gianpiero Cabodi, Paolo Camurati, Fabrizio F. Finocchiaro, Danilo Vendraminetto
2018	J	`jnl`	To split or to group: from divide-and-conquer to sub-task sharing for verifying multiple properties in model checking. Int. J. Softw. Tools Technol. Transf. Gianpiero Cabodi, Paolo Camurati, Carmelo Loiacono, Marco Palena, Paolo Pasini, Denis Patti, Stefano Quer
2017	J	`jnl`	Deep Classifiers-Based License Plate Detection, Localization and Recognition on GPU-Powered Mobile Platform. Future Internet Syed Tahir Hussain Rizvi, Denis Patti, Tomas Björklund, Gianpiero Cabodi, Gianluca Francini
2017	J	`jnl`	Efficient Complex High-Precision Computations on GPUs without Precision Loss. J. Circuits Syst. Comput. Gianpiero Cabodi, Alessandro Garbo, Carmelo Loiacono, Stefano Quer, Gianluca Francini
2017	J	`jnl`	Embedded Systems Secure Path Verification at the Hardware/Software Interface. IEEE Des. Test Gianpiero Cabodi, Paolo Camurati, Sebastiano F. Finocchiaro, Francesco Savarese, Danilo Vendraminetto
2017	C	`conf`	GPU-only unified ConvMM layer for neural classifiers. CoDIT Syed Tahir Hussain Rizvi, Gianpiero Cabodi, Gianluca Francini
2017	B	`conf`	Interpolation-Based Learning as a Mean to Speed-Up Bounded Model Checking (Short Paper). SEFM Gianpiero Cabodi, Paolo Camurati, Marco Palena, Paolo Pasini, Danilo Vendraminetto
2017	J	`jnl`	SAT solver management strategies in IC3: an experimental approach. Formal Methods Syst. Des. Gianpiero Cabodi, Paolo Camurati, Alan Mishchenko, Marco Palena, Paolo Pasini
2016	B	`conf`	A 7/2-Approximation Algorithm for the Maximum Duo-Preservation String Mapping Problem. CPM Nicolas Boria, Gianpiero Cabodi, Paolo Camurati, Marco Palena, Paolo Pasini, Stefano Quer
2016	J	`jnl`	A Greedy Approach to Answer Reachability Queries on DAGs. CoRR Nicolas Boria, Gianpiero Cabodi, Paolo Camurati, Marco Palena, Paolo Pasini, Stefano Quer
2016	J	`jnl`	A graph-labeling approach for efficient cone-of-influence computation in model-checking problems with multiple properties. Softw. Pract. Exp. Gianpiero Cabodi, Paolo Camurati, Stefano Quer
2016	C	`conf`	Gabor filter based image representation for object classification. CoDIT Syed Tahir Hussain Rizvi, Gianpiero Cabodi, Pedro P. B. de Gusmao, Gianluca Francini
2016	B	`conf`	Reducing interpolant circuit size by ad-hoc logic synthesis and SAT-based weakening. FMCAD Gianpiero Cabodi, Paolo Camurati, Marco Palena, Paolo Pasini, Danilo Vendraminetto
2016	C	`conf`	Scalable FPGA graph model to detect routing faults. IOLTS Luca Sterpone, Gianpiero Cabodi, Sebastiano F. Finocchiaro, Carmelo Loiacono, Francesco Savarese, Boyang Du
2016	—	`conf`	Secure Path Verification. IVSW Gianpiero Cabodi, Paolo Camurati, Sebastiano F. Finocchiaro, Carmelo Loiacono, Francesco Savarese, Danilo Vendraminetto
2015	J	`jnl`	Optimization techniques for craig interpolant compaction in unbounded model checking. Formal Methods Syst. Des. Gianpiero Cabodi, Carmelo Loiacono, Danilo Vendraminetto
2014	J	`jnl`	Hardware Model Checking Competition 2014: An Analysis and Comparison of Solvers and Benchmarks. J. Satisf. Boolean Model. Comput. Gianpiero Cabodi, Carmelo Loiacono, Marco Palena, Paolo Pasini, Denis Patti, Stefano Quer, Danilo Vendraminetto, Armin Biere, Keijo Heljanko
2014	B	`conf`	Interpolation with Guided Refinement: Revisiting incrementality in SAT-based unbounded model checking. FMCAD Gianpiero Cabodi, Marco Palena, Paolo Pasini
2014	A	`conf`	Tightening BDD-based approximate reachability with SAT-based clause generalization DATE Gianpiero Cabodi, Paolo Pasini, Stefano Quer, Danilo Vendraminetto
2013	A	`conf`	Optimization techniques for craig interpolant compaction in unbounded model checking. DATE Gianpiero Cabodi, Carmelo Loiacono, Danilo Vendraminetto
2013	J	`jnl`	Thread-based multi-engine model checking for multicore platforms. ACM Trans. Design Autom. Electr. Syst. Gianpiero Cabodi, Sergio Nocco, Stefano Quer
2013	—	`conf`	Trading-off Incrementality and Dynamic Restart of Multiple Solvers in IC3. DIFTS@FMCAD Marco Palena, Gianpiero Cabodi, Alan Mishchenko
2012	B	`ed.`	Formal Methods in Computer-Aided Design, FMCAD 2012, Cambridge, UK, October 22-25, 2012 FMCAD Gianpiero Cabodi, Satnam Singh
2011	J	`jnl`	Benchmarking a model checker for algorithmic improvements and tuning for performance. Formal Methods Syst. Des. Gianpiero Cabodi, Sergio Nocco, Stefano Quer
2011	A	`conf`	Interpolation sequences revisited. DATE Gianpiero Cabodi, Sergio Nocco, Stefano Quer
2011	A	`conf`	Optimized model checking of multiple properties. DATE Gianpiero Cabodi, Sergio Nocco
2010	J	`jnl`	Boosting software fault injection for dependability analysis of real-time embedded applications. ACM Trans. Embed. Comput. Syst. Gianpiero Cabodi, Marco Murciano, Massimo Violante
2010	J	`jnl`	Finding Multiple Equivalence-Preserving Transformations in Combinational Circuits through Incremental-SAT. J. Electron. Test. Gianpiero Cabodi, Leandro Dipietro, Marco Murciano, Sergio Nocco
2010	J	`jnl`	Partitioning Interpolant-Based Verification for Effective Unbounded Model Checking. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. Gianpiero Cabodi, Luz Amanda Garcia, Marco Murciano, Sergio Nocco, Stefano Quer
2010	J	`jnl`	Speeding-up heuristic allocation, scheduling and binding with SAT-based abstraction/refinement techniques. ACM Trans. Design Autom. Electr. Syst. Gianpiero Cabodi, Luciano Lavagno, Marco Murciano, Alex Kondratyev, Yosinori Watanabe
2009	—	`conf`	Exploiting incrementality in SAT-based search for multiple equivalence-preserving transformations in combinational circuits. HLDVT Gianpiero Cabodi, Leandro Dipietro, Marco Murciano, Sergio Nocco
2009	A	`conf`	Speeding up model checking by exploiting explicit and hidden verification constraints. DATE Gianpiero Cabodi, Paolo Camurati, Luz Amanda Garcia, Marco Murciano, Sergio Nocco, Stefano Quer
2009	J	`jnl`	Strengthening Model Checking Techniques With Inductive Invariants. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. Gianpiero Cabodi, Sergio Nocco, Stefano Quer
2008	A	`conf`	Automated abstraction by incremental refinement in interpolant-based model checking. ICCAD Gianpiero Cabodi, Paolo Camurati, Marco Murciano
2008	J	`jnl`	Boosting interpolation with dynamic localized abstraction and redundancy removal. ACM Trans. Design Autom. Electr. Syst. Gianpiero Cabodi, Marco Murciano, Sergio Nocco, Stefano Quer
2008	B	`conf`	Trading-Off SAT Search and Variable Quantifications for Effective Unbounded Model Checking. FMCAD Gianpiero Cabodi, Paolo Camurati, Luz Amanda Garcia, Marco Murciano, Sergio Nocco, Stefano Quer
2007	—	`conf`	A Compositional Approach for Equivalence Checking of Sequential Circuits with Unknown Reset State and Overlapping Partitions. EUROCAST Gabriel P. Bischoff, Karl S. Brace, Gianpiero Cabodi
2007	A	`conf`	Boosting the role of inductive invariants in model checking. DATE Gianpiero Cabodi, Sergio Nocco, Stefano Quer
2006	—	`conf`	BDD-Based Hardware Verification. SFM Gianpiero Cabodi, Marco Murciano
2006	A	`conf`	Stepping forward with interpolants in unbounded model checking. ICCAD Gianpiero Cabodi, Marco Murciano, Sergio Nocco, Stefano Quer
2005	J	`jnl`	A BMC-based formulation for the scheduling problem of hardware systems. Int. J. Softw. Tools Technol. Transf. Gianpiero Cabodi, Alex Kondratyev, Luciano Lavagno, Sergio Nocco, Stefano Quer, Yosinori Watanabe
2005	J	`jnl`	Are BDDs still alive within sequential verification? Int. J. Softw. Tools Technol. Transf. Gianpiero Cabodi, Sergio Nocco, Stefano Quer
2005	A	`conf`	Circuit Based Quantification: Back to State Set Manipulation within Unbounded Model Checking. DATE Gianpiero Cabodi, Marco Crivellari, Sergio Nocco, Stefano Quer
2004	—	`conf`	Exploiting Target Enlargement and Dynamic Abstraction within Mixed BDD and SAT Invariant Checking. BMC@CAV Gabriel P. Bischoff, Karl S. Brace, Gianpiero Cabodi, Sergio Nocco, Stefano Quer
2004	J	`jnl`	Improving SAT-based Bounded Model Checking by Means of BDD-based Approximate Traversals. J. Univers. Comput. Sci. Gianpiero Cabodi, Sergio Nocco, Stefano Quer
2003	—	`conf`	A BMC-formulation for the scheduling problem in highly constrained hardware Systems. BMC@CAV Gianpiero Cabodi, Sergio Nocco, Stefano Quer, Alex Kondratyev, Luciano Lavagno, Yosinori Watanabe
2003	A	`conf`	Improving SAT-Based Bounded Model Checking by Means of BDD-Based Approximate Traversals. DATE Gianpiero Cabodi, Sergio Nocco, Stefano Quer
2002	—	`conf`	A Symbolic Approach for the Combined Solution of Scheduling and Allocation. ISSS Luciano Lavagno, Mihai T. Lazarescu, Stefano Quer, Sergio Nocco, Claudio Passerone, Gianpiero Cabodi
2002	A*	`conf`	Can BDDs compete with SAT solvers on bounded model checking? DAC Gianpiero Cabodi, Paolo Camurati, Stefano Quer
2002	A	`conf`	Dynamic Scheduling and Clustering in Symbolic Image Computation. DATE Gianpiero Cabodi, Paolo Camurati, Stefano Quer
2002	A*	`conf`	Mixing Forward and Backward Traversals in Guided-Prioritized BDD-Based Verification. CAV Gianpiero Cabodi, Sergio Nocco, Stefano Quer
2001	A	`conf`	Biasing symbolic search by means of dynamic activity profiles. DATE Gianpiero Cabodi, Paolo Camurati, Stefano Quer
2001	A*	`conf`	Meta-BDDs: A Decomposed Representation for Layered Symbolic Manipulation of Boolean Functions. CAV Gianpiero Cabodi
2001	J	`jnl`	Reachability analysis of large circuits using disjunctive partitioning and partial iterative squaring. J. Syst. Archit. Gianpiero Cabodi, Paolo Camurati, Stefano Quer
2000	J	`jnl`	Improving symbolic reachability analysis by means of activityprofiles. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. Gianpiero Cabodi, Paolo Camurati, Stefano Quer
2000	A*	`conf`	Optimizing sequential verification by retiming transformations. DAC Gianpiero Cabodi, Stefano Quer, Fabio Somenzi
2000	J	`jnl`	Symbolic forward/backward traversals of large finite state machines. J. Syst. Archit. Gianpiero Cabodi, Paolo Camurati, Stefano Quer
2000	J	`jnl`	Verification of Similar FSMs by Mixing Incremental Re-encoding, Reachability Analysis, and Combinational Checks. Formal Methods Syst. Des. Stefano Quer, Gianpiero Cabodi, Paolo Camurati, Luciano Lavagno, Ellen Sentovich, Robert K. Brayton
1999	A	`conf`	Computing Timed Transition Relations for Sequential Cycle-Based Simulation. DATE Gianpiero Cabodi, Paolo Camurati, Claudio Passerone, Stefano Quer
1999	A*	`conf`	Improving Symbolic Traversals by Means of Activity Profiles. DAC Gianpiero Cabodi, Paolo Camurati, Stefano Quer
1999	J	`jnl`	Improving the efficiency of BDD-based operators by means of partitioning. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. Gianpiero Cabodi, Paolo Camurati, Stefano Quer
1998	J	`jnl`	Auxiliary variables for BDD-based representation and manipulation of Boolean functions. ACM Trans. Design Autom. Electr. Syst. Gianpiero Cabodi, Paolo Camurati, Stefano Quer
1998	J	`jnl`	Binary Decision Diagrams and the Multiple Variable Order Problem Universität Trier, Mathematik/Informatik, Forschungsbericht Gianpiero Cabodi, Stefano Quer, Christoph Meinel, Harald Sack, Anna Slobodová, Christian Stangier
1998	J	`jnl`	Memory Optimization in Function and Set Manipulation with BDDs. Softw. Pract. Exp. Gianpiero Cabodi, Stefano Quer, Paolo Camurati
1998	J	`jnl`	The General Product Machine: a New Model for Symbolic FSM Traversal. Formal Methods Syst. Des. Gianpiero Cabodi, Paolo Camurati, Fulvio Corno, Paolo Prinetto, Matteo Sonza Reorda
1997	—	`conf`	A parallel approach to symbolic traversal based on set partitioning. CHARME Gianpiero Cabodi, Paolo Camurati, Antonio Lioy, Massimo Poncino, Stefano Quer
1997	A*	`conf`	Disjunctive Partitioning and Partial Iterative Squaring: An Effective Approach for Symbolic Traversal of Large Circuits. DAC Gianpiero Cabodi, Paolo Camurati, Luciano Lavagno, Stefano Quer
1997	J	`jnl`	Symbolic FSM traversals based on the transition relation. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. Gianpiero Cabodi, Paolo Camurati
1997	—	`conf`	Verification and synthesis of counters based on symbolic techniques. ED&TC Gianpiero Cabodi, Paolo Camurati, Luciano Lavagno, Stefano Quer
1996	—	`conf`	Decomposed symbolic forward traversals of large finite state machines. EURO-DAC Stefano Quer, Gianpiero Cabodi, Paolo Camurati
1996	C	`conf`	Enhancing FSM Traversal by Temporary Re-Encoding. ICCD Gianpiero Cabodi, Luciano Lavagno, Enrico Macii, Massimo Poncino, Stefano Quer, Paolo Camurati, Ellen Sentovich
1996	A	`conf`	Improved reachability analysis of large finite state machines. ICCAD Gianpiero Cabodi, Paolo Camurati, Stefano Quer
1996	—	`conf`	Incremental re-encoding for symbolic traversal of product machines. EURO-DAC Gianpiero Cabodi, Paolo Camurati, Luciano Lavagno, Stefano Quer, Robert K. Brayton, Ellen Sentovich
1995	—	`conf`	Computing subsets of equivalence classes for large FSMs. EURO-DAC Gianpiero Cabodi, Stefano Quer, Paolo Camurati
1995	—	`conf`	Transforming boolean relations by symbolic encoding. CHARME Gianpiero Cabodi, Stefano Quer, Paolo Camurati
1994	C	`conf`	A BDD Package For A Massively Parallel SIMD Architecture. PDP Gianpiero Cabodi, Silvano Gai, Maurizio Rebaudengo, Matteo Sonza Reorda
1994	A*	`conf`	Auxiliary Variables for Extending Symbolic Traversal Techniques to Data Paths. DAC Gianpiero Cabodi, Paolo Camurati, Stefano Quer
1994	C	`conf`	Detecting hard faults with combined approximate forward/backward symbolic techniques. ISCAS Gianpiero Cabodi, Paolo Camurati, Stefano Quer
1994	C	`conf`	Efficient State Space Pruning in Symbolic Backward Traversal. ICCD Gianpiero Cabodi, Paolo Camurati, Stefano Quer
1994	A	`conf`	Full-Symbolic ATPG for Large Circuits. ITC Gianpiero Cabodi, Paolo Camurati, Stefano Quer
1994	—	`conf`	Symbolic exploration of large circuits with enhanced forward/backward traversals. EURO-DAC Gianpiero Cabodi, Paolo Camurati, Stefano Quer
1994	—	`conf`	Symbolic traversals of data paths with auxiliary variables. Great Lakes Symposium on VLSI Gianpiero Cabodi, Paolo Camurati, Stefano Quer
1993	J	`jnl`	A Parallel System for Test Pattern Generation. Parallel Comput. Gianpiero Balboni, Gianpiero Cabodi, Silvano Gai, Matteo Sonza Reorda
1993	—	`conf`	Advancements in Symbolic Traversal Technique. CHARME Gianpiero Cabodi, Paolo Camurati
1993	J	`jnl`	An approach to sequential circuit diagnosis based on formal verification techniques. J. Electron. Test. Gianpiero Cabodi, Paolo Camurati, Fulvio Corno, Paolo Prinetto, Matteo Sonza Reorda
1993	C	`conf`	Exploiting Cofactoring for Efficient FSM Symbolic Traversal Based on the Transition Relation. ICCD Gianpiero Cabodi, Paolo Camurati
1992	A*	`conf`	A New Model for Improving symbolic Product Machine Traversal. DAC Gianpiero Cabodi, Paolo Camurati, Fulvio Corno, Silvano Gai, Paolo Prinetto, Matteo Sonza Reorda
1992	—	`conf`	Cross-fertilizing FSM verification techniques and sequential diagnosis. EURO-DAC Gianpiero Cabodi, Paolo Camurati, Fulvio Corno, Paolo Prinetto, Matteo Sonza Reorda
1992	A	`conf`	Sequential Circuit Diagnosis Based on Formal Verification Techniques. ITC Gianpiero Cabodi, Paolo Camurati, Fulvio Corno, Paolo Prinetto, Matteo Sonza Reorda
1991	—	`conf`	A parallel system for test pattern generation. SPDP Gianpiero Balboni, Gianpiero Cabodi, Silvano Gai, D. Sismondi, Matteo Sonza Reorda
1991	C	`conf`	Fast Differential Fault Simulation by Dynamic Fault Ordering. ICCD Gianpiero Cabodi, Silvano Gai, Matteo Sonza Reorda
1991	J	`jnl`	TPDL: Extended Temporal Profile Description Language. Softw. Pract. Exp. Gianpiero Cabodi, Paolo Camurati, Paolo Prinetto, Matteo Sonza Reorda
1990	J	`jnl`	A transputer-based gate-level fault simulator. Microprocessing and Microprogramming Gianpiero Cabodi, Silvano Gai, Matteo Sonza Reorda
1989	J	`jnl`	Expressing logical and temporal conditions in simulation environments: TPDL Microprocessing and Microprogramming Gianpiero Cabodi, Paolo Camurati, Paolo Prinetto, Matteo Sonza Reorda
1988	—	`conf`	Fault simulation in a multilevel environment: the MOZART approach. FTCS Gianpiero Cabodi, Silvano Gai, Marco Mezzalama, Pier Luca Montessoro, Fabio Somenzi
1986	—	`conf`	Experiences in Prolog-Based DFT Rule Checking. FJCC Gianpiero Cabodi, Paolo Camurati, Paolo Prinetto