NARIZZANO , Massimo

Metodo per il supporto alla pianificazione di traiettorie stereotassiche lineari per l'impianto di dispositivi intracerebrali, quali elettrodi multicontatto, sonde bioptiche, applicatori di luce laser o simili comprendente i seguenti passi: a) realizzazione di un database all'interno del quale database sono presenti informazioni relative alle...

Background Invasive monitoring of brain activity by means of intracerebral electrodes is widely practiced to improve pre-surgical seizure onset zone localization in patients with medically refractory seizures. Stereo-Electroencephalography (SEEG) is mainly used to localize the epileptogenic zone and a precise knowledge of the location of the...

The implementation of effective reasoning tools for deciding the satisfiability of Quantified Boolean Formulas (QBFs) is an important research issue in Artificial Intelligence. Many decision proce- dures have been proposed in the last few years, most of them based on the Davis, Logemann, Love- land procedure (DLL) for propositional...

No description

Verification of embedded systems is challenging whenever control programs rely on black-box hardware components. Unless precise specifications of such components are fully available, learning their structured models is a powerful enabler for verification, but it can be inefficient when the system to be learned is data-intensive rather than...

No description

No description

The implementation of effective reasoning tools for deciding the satisfiability of Quantified Boolean Formulas (QBFs) is an important research issue in Artificial Intelligence. Many decision procedures have been proposed in the last few years, most of them based on the Davis, Logemann, Loveland procedure (DLL) for propositional satisfiability...

The best currently available solvers for quantified Boolean formulas (QBFs) process their input in prenex form, i.e., all the quan- tifiers have to appear in the prefix of the formula separated from the purely propositional part representing the matrix. However, in many QBFs derived from applications, the propositional part is intertwined with...

No description

Resolution is the rule of inference at the basis of most procedures for automated reasoning. In these procedures, the input formula is first translated into an equisatisfiable formula in conjunctive normal form (CNF) and then represented as a set of clauses. Deduction starts by inferring new clauses by resolution, and goes on until the empty...

No description

No description

Learning, i.e., the ability to record and exploit some informa- tion which is unveiled during the search, proved to be a very effective AI technique for problem solving and, in particular, for constraint satisfaction. We introduce learning as a general purpose technique to improve the performances of decision procedures for Quantified Boolean...

No description

No description

No description

No description

No description

In this paper we compare the performance of all the currently available suites to evaluate and certify QBFs. Our aim is to assess the current state of the art, and also to understand to which extent QBF en- codings can be evaluated producing certificates that can be checked in a reliable and efficient way. We con- clude that, while the...

In the context of structural testing, automatic test-pattern generation (ATPG) may fail to provide suites covering 100% of the testing requirements for grey-box programs, i.e., Applications wherein source code is available for some parts (white-box), but not for others (black-box). Furthermore, test suites based on abstract models may elicit...

No description