Verification of embedded software relying on black-box hardware is challenging whenever precise specifications of the underlying systems are incomplete or not available. Learning structured hardware models is a powerful enabler of verification in these cases, but it can be inefficient when the system to be learned is data-intensive rather than control-intensive. We contribute a methodology to attack this problem based on a specific class of automata which are well suited to model systems wherein data paths are known to be decoupled from control paths. We show the effectiveness of our approach by combining learning and verification to assess the correctness of embedded programs relying on FIFO register circuitry to control an elevator system.

In the context of Requirements Engineering, checking the consistency of functional requirements is an important and still mostly open problem. In case of requirements written in natural language, the corresponding manual review is time consuming and error prone. On the other hand, automated consistency checking most often requires overburdening formalizations. In this paper we introduce ReqV, a tool for formal consistency checking of requirements. The main goal of the tool is to provide an easy-to-use environment for the verification of requirements in Cyber-Physical Systems (CPS). ReqV takes as input a set of requirements expressed in a structured natural language, translates them in a formal language and it checks their inner consistency. In case of failure, ReqV can also extracts a minimal set of conflicting requirements to help designers in correcting the specification.

BACKGROUND: In the evaluation of Stereo-Electroencephalography (SEEG) signals, the physicist's workflow involves several operations, including determining the position of individual electrode contacts in terms of both relationship to grey or white matter and location in specific brain regions. These operations are (i) generally carried out manually by experts with limited computer support, (ii) hugely time consuming, and (iii) often inaccurate, incomplete, and prone to errors. RESULTS: In this paper we present SEEG Assistant, a set of tools integrated in a single 3DSlicer extension, which aims to assist neurosurgeons in the analysis of post-implant structural data and hence aid the neurophysiologist in the interpretation of SEEG data. SEEG Assistant consists of (i) a module to localize the electrode contact positions using imaging data from a thresholded post-implant CT, (ii) a module to determine the most probable cerebral location of the recorded activity, and (iii) a module to compute the Grey Matter Proximity Index, i.e. the distance of each contact from the cerebral cortex, in order to discriminate between white and grey matter location of contacts. Finally, exploiting 3DSlicer capabilities, SEEG Assistant offers a Graphical User Interface that simplifies the interaction between the user and the tools. SEEG Assistant has been tested on 40 patients segmenting 555 electrodes, and it has been used to identify the neuroanatomical loci and to compute the distance to the nearest cerebral cortex for 9626 contacts. We also performed manual segmentation and compared the results between the proposed tool and gold-standard clinical practice. As a result, the use of SEEG Assistant decreases the post implant processing time by more than 2 orders of magnitude, improves the quality of results and decreases, if not eliminates, errors in post implant processing. CONCLUSIONS: The SEEG Assistant Framework for the first time supports physicists by providing a set of open-source tools for post-implant processing of SEEG data. Furthermore, SEEG Assistant has been integrated into 3D Slicer, a software platform for the analysis and visualization of medical images, overcoming limitations of command-line tools.

Twelve years have elapsed since the first Quantified Boolean Formulas (QBFs) evaluation was held as an event linked to SAT conferences. During this period, researchers have striven to propose new algorithms and tools to solve challenging formulas, with evaluations periodically trying to assess the current state of the art. In this paper, we present an experimental account of solvers and formulas with the aim to understand the progress in the QBF arena across these years. Unlike typical evaluations, the analysis is not confined to the snapshot of submitted solvers and formulas, but rather we consider several tools that were proposed over the last decade, and we run them on different formulas from previous QBF evaluations. The main contributions of our analysis, which are also the messages we would like to pass along to the research community, are: (i) many formulas that turned out to be difficult to solve in past evaluations, remain still challenging after twelve years, (ii) there is no single solver which can significantly outperform all the others, unless specific categories of formulas are considered, and (iii) effectiveness of preprocessing depends both on the coupled solver and the structure of the formula.

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 electrodes is expected to facilitate the recordings interpretation and the planning of resective surgery. However, the localization of intracerebral electrodes on post-implant acquisitions is usually time-consuming (i.e., manual segmentation), it requires advanced 3D visualization tools, and it needs the supervision of trained medical doctors in order to minimize the errors. In this paper we propose an automated segmentation algorithm specifically designed to segment SEEG contacts from a thresholded post-implant Cone-Beam CT volume (0.4 mm, 0.4 mm, 0.8 mm). The algorithm relies on the planned position of target and entry points for each electrode as a first estimation of electrode axis. We implemented the proposed algorithm into DEETO, an open source C++ prototype based on ITK library. RESULTS: We tested our implementation on a cohort of 28 subjects in total. The experimental analysis, carried out over a subset of 12 subjects (35 multilead electrodes; 200 contacts) manually segmented by experts, show that the algorithm: (i) is faster than manual segmentation (i.e., less than 1s/subject versus a few hours) (ii) is reliable, with an error of 0.5 mm ± 0.06 mm, and (iii) it accurately maps SEEG implants to their anatomical regions improving the interpretability of electrophysiological traces for both clinical and research studies. Moreover, using the 28-subject cohort we show here that the algorithm is also robust (error < 0.005 mm) against deep-brain displacements (< 12 mm) of the implanted electrode shaft from those planned before surgery. CONCLUSIONS: Our method represents, to the best of our knowledge, the first automatic algorithm for the segmentation of SEEG electrodes. The method can be used to accurately identify the neuroanatomical loci of SEEG electrode contacts by a non-expert in a fast and reliable manner.

In this paper we present the parallel QBF Solver PaQuBE. This new solver leverages the additional computational power that can be exploited from modern computer architectures, from pervasive multi-core boxes to clusters and grids, to solve more relev

ERTMS is the European Railway Traffic Management System. The CENELEC EN50128 guidelines for software development of safety critical system require that the software produced is verified by providing a set of tests covering the 100% of the code. This requirement, however, substantially increases the costs associated to the testing phase, since it may involve the manual generation of tests. In this paper we present a methodology to automatic generate test achieving the desired code coverage. The automatization of the test generation phase, applied to some modules of the ERTMS developed by Ansaldo STS (an Italian leading company in the field), led to a dramatic increase in the productivity and to a reduction of the costs of the entire software development process.

The best currently available solvers for quantified Boolean formulas (QBFs) process their input in prenex form, i.e., all the quantifiers 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 the quantifier structure. To tackle this problem, the standard approach is to convert such QBFs in prenex form, thereby losing structural information about the prefix. In the case of search-based solvers, the prenex-form conversion introduces additional constraints on the branching heuristic and reduces the benefits of the learning mechanisms. In this paper, we show that conversion to prenex form is not necessary: current search-based solvers can be naturally extended in order to handle nonprenex QBFs and to exploit the original quantifier structure. We highlight the two mentioned drawbacks of the conversion in prenex form with a simple example, and we show that our ideas can also be useful for solving QBFs in prenex form. To validate our claims, we implemented our ideas in the state-of-the-art search-based solver QuBE and conducted an extensive experimental analysis. The results show that very substantial speedups can be obtained

The best currently available solvers for quantified Boolean formulas (QBFs) process their input in prenex form, i.e., all the quantifiers have to appear in the prefix of the formula separated from the purely proppositional part representing the matrix. However, in many QBFs deriving from applications, the propositional part is intertwined with the quantifier structure. To tackle this problem, the standard approach is to first convert them in prenex form, thereby loosing structural information about the prefix. In this paper we show that conversion to prenex form is not necessary, i.e., that it is relatively easy to extend current search based solvers in order to exploit the original quantifier structure, i.e., to handle non prenex QBFs. Further, we show that the conversion can lead to the exploration of search spaces bigger than the space explored by solvers handling non prenex QBFs. To validate our claims, we implemented our ideas in the state-of-the-art search based solver QuBE, and conducted an extensive experimental analysis. The results show that very substantial speedups can be obtained

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 clause is generated or satisfiability of the set of clauses is proven, e.g., because no new clauses can be generated. In this paper, we restrict our attention to the problem of evaluating Quantified Boolean Formulas (QBFs). In this setting, the above outlined deduction process is known to be sound and complete if given a formula in CNF and if a form of resolution, called ``Q-resolution'', is used. We introduce Q-resolution on terms, to be used for formulas in disjunctive normal form. We show that the computation performed by most of the available procedures for QBFs --based on the Davis-Logemann-Loveland procedure (DLL) for propositional satisfiability-- corresponds to a tree in which Q-resolution on terms and clauses alternate. This poses the theoretical bases for the introduction of learning, corresponding to recording Q-resolution formulas associated with the nodes of the tree. We discuss the problems related to the introduction of learning in DLL based procedures, and present solutions extending state-of-the-art proposals coming from the literature on propositional satisfiability. Finally, we show that our DLL based solver extended with learning, performs significantly better on benchmarks used in the 2003 QBF solvers comparative evaluation.