You are here

Publications

Primary tabs

  1. Marco Aste; Roldano Cattoni; Bruno Caprile,
    VGS - Visual Gate Simulator Simulatore degli eventi di occlusione di fotocellule in varchi controllati Manuale d'uso Versione: 1.0,
  2. Paolo Tonella; R. Fiutem; G. Antoniol; F. Calzolari,
    Modular Reaching Definitions Analysis,
    Reaching definitions are used in debugging, testing, program understanding and impact analysis. Interprocedural reaching definitions computation is difficult because the different invocation contexts of each procedure have not to be mixed, in order to produce accurate results. We propose a modular reaching definitions algorithm which exploits the structure of the call graph to determine an effective computation order. This algorithm avoids repeating fixpoint computation inside each procedure for every different calling context, but still remains context sensitive. It also enjoys some interesting properties related to modularity, incrementality and subsystem analysis. Experimental results provide evidence of good execution time performance and scalability,
  3. Paolo Tonella; G. Antoniol; R. Fiutem; F. Calzolari,
    Studio di fattibilità relativo alla analisi del software di proprietà ITALTEL,
  4. Mauro Cettolo; D. Falavigna,
    Automatic Speech Recognition of Spontaneous Dialogues,
    Some solutions for coping with the problem of recognition of spontaneous speech dialogues are presented. Starting from a baseline system, developed for dictation tasks, some modifications are introduced at the acoustic level and in the language model. Acoustic model parameters are modified for addressing speaking rate variations, and specific models of extra-linguistic phenomena are defined and included into the language model. Different acoustic model sets are arranged in a single recognizer though their integration into a multi-model search space. Experiments and evaluations were carried out on a corpus of spontaneous dialogues collected in our laboratory,
  5. Francesco Ricci; D.W. Aha,
    Bias, Variance, and Error Correcting Output Codes for Local Learners,
    This paper focuses on a bias variance decomposition analysis of a local learning algorithm, the nearest neighbor classifier, that has been extended with 'error correcting output codes'. This extended algorithm often considerably reduces the 0-1 (i.e., classification) error in comparison with nearest neigbor (Ricci & Aha, 1997). The analysis presented here reveals that this performance improvement is obtained by drastically reducing bias at the cost of increasing variance. We also show that, even in classification problems with few classes (m<_5), extending the codeword length beyond the limit that assures column separation yields an error reduction. This error reduction is not only in the variance, which is due to the voting mechanism used for error-correcting output codes, but also in the bias,
  6. Roberto Sebastiani; Fausto Giunchiglia,
    From Tableau-based to SAT-based procedures - preliminary report,
    Tableau systems are very popular in AI for their simplicity and versatility. In recent papers we showed that tableau-based procedures are intrinsically inefficient, and proposed an alternative approach of building decision procedures on top of SAT decision procedure. We called this approach ‘SAT based’. In extensive empirical tests on the case study of modal K, a SAT-based procedure drastically outperformed a state-of-the-art tableau-based system. In this paper we provide the theoretical foundations for developing SAT-based decision procedures for many different modal logics,
  7. F. Ciravegna; Alberto Lavelli; D. Petrelli; Fabio Pianesi,
    The GEPPETTO Development Environment. Version 2.1. User Manual,
  8. Piergiorgio Bertoli; Alessandro Cimatti; Fausto Giunchiglia; Paolo Traverso,
    Certification of Translators via Off-line and On-line Proof Logging and Checking,
    Using non failure-safe components in the implementation of safety-critical systems is desirable because of the extremely high cost of certified components. In order to enhance the safety of such systems, we adopt a solution based on the idea of verifying each single execution of the software running upon them. In particular, we consider the class of translation-based tools used in the development of safety-critical systems. In order to perform the verification in an automatic and efficient way, we follow an innovative approach, by distinguishing an off-line and an on-line verification phases. Each proof in the two phases is guaranteed correct thanks to the use of a logging-and-checking architecture for the tools used to generate them. We describe in detail the off-line and on-line logging-and-checking methodology, its application in the frame of an industrial project, and the ongoing logging-and-checking redesign of a state-of-the-art prover which we intend to use in future applications,
  9. Roberto Sebastiani; D. McAllester,
    New Upper Bounds for Satisfiability in Modal Logics: The Case-Study of Modal K,
  10. Paolo Tonella; G. Antoniol; R. Fiutem; F. Calzolari,
    Studio di fattibilità relativo alla analisi del software per l'archiviazione di immagini di proprietà SGS,