A5004060820- Formal Methods in Verification
- Software Testing and Debugging Techniques
- Software Reliability and Analysis Research
- VLSI and Analog Circuit Testing
- Radiation Effects in Electronics
- Embedded Systems Design Techniques
- Explainable Artificial Intelligence (XAI)
- Mass Spectrometry Techniques and Applications
- IoT and Edge/Fog Computing
- Natural Language Processing Techniques
- Neural Networks and Reservoir Computing
- Logic, Reasoning, and Knowledge
- Machine Learning and Algorithms
- Model-Driven Software Engineering Techniques
- Logic, programming, and type systems
- Adversarial Robustness in Machine Learning
- Advanced Semiconductor Detectors and Materials
- Bayesian Modeling and Causal Inference
- Machine Learning in Materials Science
- Semantic Web and Ontologies
- Algorithms and Data Compression
- Interconnection Networks and Systems
- Neural Networks and Applications
- Advanced Database Systems and Queries
- Advanced Memory and Neural Computing
Consorzio Nazionale Interuniversitario per le Telecomunicazioni
2024-2025
Polytechnic University of Turin
2013-2024
Johannes Kepler University of Linz
2016
Aalto University
2016
Model checkers and sequential equivalence have become essential tools for the semiconductor industry in recent years. The Hardware Checking Competition (HWMCC) was founded 2006 with purpose of intensifying research interest t
Machine learning (ML) is ever more frequently used as a tool to aid decision-making. The need understand the decisions made by ML algorithms has sparked renewed interest in explainable models. A number of known models are often regarded interpretable human decision-makers with varying degrees difficulty. size such plays crucial role determining how easily they can be understood human. In this paper1 we propose use Binary Decision Diagrams (BDDs) an model. BDDs deemed decision trees (DTs)...
Digital systems are nowadays ubiquitous and often comprise an extremely high level of complexity. Guaranteeing the correct behavior such has become ever more pressing need for manufacturers. The correctness digital can be addressed resorting to formal verification techniques, as model checking. Currently, it is usually impossible determine a priori best algorithm use given task and, thus, portfolio approaches have de facto standard in checking suites. This paper describes most relevant...
Modern devices often include several embedded instruments, such as BIST interfaces, sensors, calibration facilities. New standards, IEEE Std 1687, provide vehicles to access these instruments. In approaches based on reconfigurable scan networks (RSNs), instruments are coupled with registers, connected into chains and interleaved modules. Such modules embed multiplexers that permit a selective different parts of the chain. A similar scenario is also supported by 1149.1-2013. The test...
Modern devices often include several embedded instruments, such as BISTs, sensors, and other analog components. New standards, IEEE Std. 1687, provide vehicles to access these instruments. In approaches based on reconfigurable scan networks, instruments are coupled with registers, connected into chains interleaved multiplexers, permitting a selective different parts of the chain. A similar scenario is also supported by 1149.1-2013, where test data register can be constructed chain multiple...
This paper introduces a new technique for fast computation of the Cone-Of-Influence (COI) multiple properties. It specifically addresses frameworks where properties belongs to same model, and they partially or fully share their COI. In order avoid repeated visits circuit sub-graph representation, it proposes algorithm, which performs single topological visit variable dependency graph. also studies mutual relationships among different properties, based on overlapping COIs. finally considers...
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, we achieve two main results: (1) a novel algorithm; (2) new flexible way to handle an incremental representation (over-approximated) forward reachable states. The algorithm (IGR: Interpolation with Guided Refinement), partially takes inspiration from IC3 interpolation sequences. It bases its robustness refinement state sets,...
Motivated by the need to understand behaviour of complex machine learning (ML) models, there has been recent interest in optimal (or sub-optimal) decision trees (DTs). This is explained fact that DTs are widely regarded as interpretable human makers. An alternative Binary Decision Diagrams (BDDs), which can be deemed interpretable. Compared DTs, and despite a fixed variable order, BDDs offer advantage more compact representations practice, due node sharing. Moreover, also extensive...
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, we achieve two main results: (1) a novel algorithm; (2) new flexible way to handle an incremental representation (over-approximated) forward reachable states. The algorithm (IGR: Interpolation with Guided Refinement), partially takes inspiration from IC3 interpolation sequences. It bases its robustness refinement state sets,...
This paper introduces a new technique for fast computation of the Cone-Of-Influence (COI) multiple properties. It specifically addresses frameworks where properties belongs to same model, and they partially or fully share their COI. In order avoid repeated visits circuit sub-graph representation, it proposes algorithm, which performs single topological visit variable dependency graph. also studies mutual relationships among different properties, based on overlapping COIs. finally considers...
This paper presents a simple 7/2-approximation algorithm for the Maximum Duo-Preservation String Mapping (MPSM) problem. problem is complementary to classical and well studied min common string partition (MCSP), that computes minimal edit distance between two strings when only operation allowed shift blocks of characters. The improves on previously best-known 4-approximation by computing local optimum.
We address the problem of reducing size Craig interpolants used in SAT-based Model Checking. are AND-OR circuits, generated by post-processing refutation proofs SAT solvers. Whereas it is well known that highly redundant, their compaction typically tackled proof graph and/or 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 techniques: (1) A set ad-hoc functions...
Motivated by the proliferation of Internet-of-Thing (IoT) devices and rapid advances in field deep learning, there is a growing interest pushing learning computations, conventionally handled cloud, to edge network deliver faster responses end users, reduce bandwidth consumption address privacy concerns. However, fully realize at edge, two main challenges still need be addressed: (i) how meet high resource requirements on resource-constrained devices, (ii) leverage availability multiple...
We address the problem of reducing size Craig's interpolants used in SAT-based model checking. are AND-OR circuits, generated by post-processing refutation proofs SAT solvers. Being highly redundant, their compaction is typically tackled proof graph and/or exploiting standard logic synthesis techniques. In this paper, we propose a set ad-hoc functions that, revisiting known approaches, specifically speed and scalability. Though general not restricted to interpolants, these techniques target...
We address the problem of reducing size Craig's interpolants (ITPs) used in SAT-based model checking. Whereas it is well known that ITPs are highly redundant, their compaction typically tackled by proof graph and/or 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 weakening/strengthening technique, for compaction, where UNSAT core extracted from additional SAT query...
We address the problem of reducing size Craig interpolants used in SAT-based Model Checking. are AND-OR circuits, generated by post-processing refutation proofs SAT solvers. Whereas it is well known that highly redundant, their compaction typically tackled proof graph and/or 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 techniques: (1) A set ad-hoc functions...