You are here

older than 2000

1999

  1. Alessandro Cimatti; E.M. Clarke; Fausto Giunchiglia; Marco Roveri,
    NuSMV: a New Symbolic Model Verifier,
    11th International Conference on Computer Aided Verification (CAV`99), Proceedings,
    Springer,
    1999
    , (11th International Conference on Computer Aided Verification (CAV`99), Proceedings,
    Trento, Italy,
    1999)
  2. Alessandro Cimatti; P.L. Pieraccini; Roberto Sebastiani; Paolo Traverso; Adolfo Villafiorita,
    Formal Specification and validation of a Vital Communication Protocol,
    FM`99-Formal Methods, World Congress on Formal methods in the Development of Computing Systems,
    1999
    , pp. 1584-
    1604
    , (FM`99-Formal Methods, World Congress on Formal methods in the Development of Computing Systems,
    1999)
  3. A. Chiappini; Alessandro Cimatti; C. Porzia; G. Rotondo; Roberto Sebastiani; Paolo Traverso; Adolfo Villafiorita,
    18th International Conference on Computer Safety, Reliability and Security (SAFECOMP 1999),
    Springer,
    vol.1698,
    1999
    , pp. 410-
    419
    , (18th International Conference on Computer Safety, Reliability and Security (SAFECOMP 1999),
    Toulouse, France,
    1999)
  4. Alessandro Cimatti; Marco Roveri,
    Conformant Planning via Model Checking,
    Fifth European Conference on Planning [ECP`99],
    Springer,
    1999
    , (Fifth European Conference on Planning [ECP`99],
    Durham, UK,
    08/09/1999 - 10/09/1999)
  5. Alessandro Cimatti; Fausto Giunchiglia; Paolo Traverso; Adolfo Villafiorita,
    FLoC`99 Workshop on Run-Time Result Verification,
    1999
    , (FLoC`99 Workshop on Run-Time Result Verification,
    Trento, Italy,
    1999)

1998

  1. Alessandro Cimatti; Fausto Giunchiglia; R.W. Weyhrauch,
    A Many Sorted Natural Deduction,
    in «COMPUTATIONAL INTELLIGENCE»,
    vol. 1,
    n. 14,
    1998
    , pp. 135 -
    150
  2. Alessandro Cimatti; Fausto Giunchiglia; G. Mongardi; D. Romano; F. Torielli; Paolo Traverso,
    in «FORMAL ASPECTS OF COMPUTING»,
    1998
    , pp. 361 -
    380
  3. Alessandro Cimatti; E.M. Clarke; Fausto Giunchiglia; Marco Roveri,
    NuSMV: A Reimplementation of SMV,
    International Workshop on Software Tools for Technology Transfer (STTT-98),
    vol.NS-98-4,
    1998
    , pp. 25-
    31
    , (International Workshop on Software Tools for Technology Transfer (STTT-98),
    1998)
  4. Alessandro Cimatti; Marco Roveri; Paolo Traverso,
    Fourth International Conference on Artificial Intelligence Planning Systems [AIPS-98],
    1998
    , (Fourth International Conference on Artificial Intelligence Planning Systems [AIPS-98],
    Pittsburgh, USA,
    1998)
  5. Alessandro Cimatti; Marco Roveri; Paolo Traverso,
    Automatic OBDD-based Generation of Universal Plans in Non-Deterministic Domains,
    Fifteenth National Conference on Artificial Intelligence [AAAI 98],
    AAAI Press,
    1998
    , pp. 875-
    881
    , (Fifteenth National Conference on Artificial Intelligence [AAAI 98],
    Madison, USA,
    1998)
  6. Piergiorgio Bertoli; Alessandro Cimatti; Fausto Giunchiglia; Paolo Traverso,
    A Structured Approach to the Formal Certification of Safety of Computer Aided Development Tools,
    17th International Conference on Computer Safety, Reliability and Security [SAFECOMP ‘98],
    Springer,
    vol.1516,
    1998
    , pp. 221-
    230
    , (17th International Conference on Computer Safety, Reliability and Security [SAFECOMP ‘98],
    Heidelberg, Germany,
    1998)
  7. Alessandro Cimatti; Fausto Giunchiglia; Marco Roveri,
    Abstraction in Planning via Model Checking,
    Symposium on Abstraction, Reformulation and Approximation (SARA 1998),
    1998
    , pp. 37-
    41
    , (Symposium on Abstraction, Reformulation and Approximation (SARA 1998),
    1998)
  8. Alessandro Cimatti; Fausto Giunchiglia; G. Mongardi; D. Romano; F. Torielli; Paolo Traverso,
    Model Checking Safety Critical Software with SPIN: An Application to a Railway Interlocking System,
    17th International Conference on Computer Safety, Reliability and Security [SAFECOMP ‘98],
    Springer,
    vol.1516,
    1998
    , pp. 284-
    295
    , (17th International Conference on Computer Safety, Reliability and Security [SAFECOMP ‘98],
    Heidelberg, Germany,
    1998)
  9. Alessandro Cimatti; Roberto Sebastiani,
    Servizi forniti dagli strati Safety Layer e Connection Manager,
    Obiettivo del presente documento è fornire una (proposta preliminare di) descrizione dei servizi forniti agli applicativi dagli strati Connection Manager (CM) e Safety Layer (SL), come perzialmente descritto nei documenti (1) e (3). Tale proposta è risultante della riunione in Ansaldo del 08-05-98 tra Ansaldo e Irst,
    1998
  10. Alessandro Cimatti; Roberto Sebastiani,
    Specifica formale dei protocolli Safety Layer e Connection Manager,
    Il presente documento descrive una specifica formale del protocollo di comunicazione tra applicativi in sicurezza basato su ridondanza. Il protocollo è stato suddiviso in due livelli separati, il Safety Layer (SL), come parzialmente descritto nei documenti (1) e (3), ed il Connection Manager (CM). Il S: e il CM sono stati specificati formalmente in SDL, e sono state applicate tecniche di validazione basate su simulazione esaustiva (model checking) attraverso il tool ObjectGEODE Nel presente documento vengono descritti i servizi forniti da tali livelli, e viene descritta la specifica formale delle macchine a stati che realizzano i livelli CM e SL. i dettagli del codice SDL sono descritti nel documento (6).,
    1998
  11. Alessandro Cimatti; Roberto Sebastiani,
    Protocolli Safety Layer e Connection Manager: Descrizione del Codice SDL,
    Nel presente documento viene descritto in dettaglio il codice SDL della specifica formale dei protocolli Safety Layer (SL) e Connection Manager (CM) descritta in (1). Il modello è realizzato attraverso i meccanismi di 'definizione di tipo' e di 'istanziazione' di SDL. Il codice è ripartito nei fine terminale_lib.pr, contenente la descrizione dei tipi (es. macchina SL, macchina CM), e Modello.pr, contentenente le istanze che realizzano la particolare configurazione analizzata Il presente documento assume che il lettore abbia una certa conoscenza di SDL, e fa esplicito riferimento al listato dei file Modello.pr e terminale_lib.pr allegato.,
    1998

1997

  1. Alessandro Cimatti; Enrico Giunchiglia; Fausto Giunchiglia; Paolo Traverso,
    4th European Conference on Planning [ECP`97],
    Springer,
    vol.1348,
    1997
    , pp. 130-
    142
    , (4th European Conference on Planning [ECP`97],
    Toulouse, France,
    1997)
  2. Alessandro Cimatti; Fausto Giunchiglia; P. Pecchiari; B. Pietra; J. Profeta; D. Romano; Paolo Traverso; B. Yu,
    A Provably Correct Embedded Verifier for the Certification of Safety Critical Software,
    Computer Aided Verification - 9th International Conference (CAV 1997),
    Springer,
    vol.1254,
    1997
    , pp. 202-
    213
    , (Computer Aided Verification - 9th International Conference (CAV 1997),
    Haifa, Israel,
    1997)
  3. Alessandro Cimatti; Fausto Giunchiglia; G. Mongardi; D. Romano; F. Torielli; Paolo Traverso,
    Third International SPIN Workshop [SPIN97],
    1997
    , (Third International SPIN Workshop [SPIN97],
    1997)
  4. Alessandro Cimatti; Fausto Giunchiglia; G. Mongardi; B. Pietra; D. Romano; F. Torielli; Paolo Traverso,
    Formal Validation & Verification of Software for Railway Control and Protection Systems: Experimental Applications in ANSALDO,
    World Congress on Railway Research [WCRR`97],
    1997
    , pp. 467-
    473
    , (World Congress on Railway Research [WCRR`97],
    Florence, Italy,
    1997)
  5. Alessandro Cimatti; Fausto Giunchiglia; G. Mongardi; B. Pietra; D. Romano; F. Torielli; Paolo Traverso,
    Formal Validation of an Interlocking System for Large Railway Stations: A Case Study,
    The goal of this document is to define a case study in formal verification, based on a complex real-world application developed by Ansaldo Trasporti. The application, called ACC, is a highly programmable and scalable interlocking system for the control of large railway stations. In the case study, several features of the ACC are omitted in order to limit the complexity. However, the case study still retains a close similarity to the architecture of the ACC, and raises a number of problems of interest for the problem of the formal validation of the real system,
    1997
  6. Alessandro Cimatti; Enrico Giunchiglia; Fausto Giunchiglia; Paolo Traverso,
    A Model Based Decision Procedure for Common Sense Temporal Reasoning,
    In this paper we propose a model based decision procedure for common sense temporal reasoning. This procedure exploits and enhances Lifschitz` work and distinction between action language and query language and Clarke`s work on symbolic model checking. In particular, it allows us to retain the full xpressibility of the temporal formalism and, at the same time, to perform efficient reasoning and to scale up to very complex problems, comparable or more complex than those dealt with by the current state-of-the-art planners,
    1997
  7. 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,
    1997

1996

  1. Alessandro Cimatti; Paolo Traverso,
    Computational Reflection via Mechanized Logical Deduction,
    in «INTERNATIONAL JOURNAL OF INTELLIGENT SYSTEMS»,
    vol. 11,
    n. 5,
    1996
    , pp. 279 -
    293
  2. Enrico Giunchiglia; Alessandro Armando; Paolo Traverso; Alessandro Cimatti,
    Visual Representation of Natural Language Scene Descriptions,
    in «IEEE TRANSACTIONS ON SYSTEMS MAN AND CYBERNETICS PART A-SYSTEMS AND HUMANS»,
    vol. 26,
    n. 8,
    1996
    , pp. 279 -
    293
  3. Fausto Giunchiglia; Marco Roveri; Roberto Sebastiani,
    A New Method for Testing Decision Procedures in Modal and Terminological Logics,
    1996 International Workshop on Description Logics - DL`96,
    AAAI,
    1996
    , (1996 International Workshop on Description Logics - DL`96,
    Cambridge, USA,
    02/11/1996 - 04/11/1996)
  4. Paolo Bouquet; Alessandro Cimatti,
    Mechanizing Local Reasoning with Contexts,
    Working notes of the IJCAI-95 Workshop on ``Modelling Context in Knowledge Representation and Reasoning``,
    1996
    , pp. 13-
    23
    , (Working notes of the IJCAI-95 Workshop on ``Modelling Context in Knowledge Representation and Reasoning``,
    Montreal, Canada,
    1995)
  5. Alessandro Cimatti; Luciano Serafini,
    Mechanizing Multi-Agent Reasoning with Belief Contexts,
    Practical Reasoning, International Conference on Formal and Applied Practical Reasoning [FAPR`96],
    Springer,
    1996
    , pp. 694-
    696
    , (Practical Reasoning, International Conference on Formal and Applied Practical Reasoning [FAPR`96],
    1996)
  6. Massimo Benerecetti; Alessandro Cimatti; Enrico Giunchiglia; Fausto Giunchiglia; Luciano Serafini,
    Context-Based Formal Specification of Multi-Agent Systems,
    Working Notes of the Third International Workshop on Agent Theories, Architectures, and Languages [ATAL-96],
    1996
    , pp. 295-
    307
    , (Working Notes of the Third International Workshop on Agent Theories, Architectures, and Languages [ATAL-96],
    Budapest, Hungary,
    1996)

1995

  1. A. Armando; Alessandro Cimatti; E. Giunchiglia; P. Pecchiari; L. Spalazzi; Paolo Traverso,
    Flexible Planning by Integrating Multilevel Reasoning,
    in «ENGINEERING APPLICATIONS OF ARTIFICIAL INTELLIGENCE»,
    vol. 4,
    1995
    , pp. 401 -
    412
  2. Giuliano Antoniol; Bruno Caprile; Alessandro Cimatti; Roberto Fiutem,
    Experiencing Real-Life Interactions with the Mobile Platform of MAIA,
    The Biology and Technology of Intelligent Autonomous Agents: Proceedings of the NATO Advanced Study on the Biology and Technology of Intelligent Autonomous Agents,
    Springer,
    1995
    , pp. 296-
    311
    , (The Biology and Technology of Intelligent Autonomous Agents: Proceedings of the NATO Advanced Study on the Biology and Technology of Intelligent Autonomous Agents,
    1993)
  3. Alessandro Cimatti; Luciano Serafini,
    Multi-Agent Reasoning with Belief Contexts III: Towards the Mechanization,
    IJCAI-95 Workshop on Modelling Context in Knowledge Representation and Reasoning,
    1995
    , pp. 35-
    45
    , (IJCAI-95 Workshop on Modelling Context in Knowledge Representation and Reasoning,
    Montreal, Canada,
    1995)
  4. Alessandro Cimatti; Luciano Serafini,
    Multi-Agent Reasoning with Belief Contexts: The Approach and a Case Study,
    Intelligent Agents, ECAI-94 Workshop on Agent Theories, Architectures, and Languages,
    Springer,
    vol.890,
    1995
    , pp. 71-
    85
    , (Intelligent Agents, ECAI-94 Workshop on Agent Theories, Architectures, and Languages,
    Amsterdam, The Netherlands,
    1994)
  5. Alessandro Cimatti; Luciano Serafini,
    Multiagent Reasoning with Belief Contexts II: Elaboration Tolerance,
    First International Conference on Multiagent Systems,
    MIT Press,
    1995
    , pp. 57-
    64
    , (First International Conference on Multiagent Systems,
    San Francisco, California,
    1995)

1994

  1. Paolo Traverso; Alessandro Cimatti; Luca Spalazzi; Enrico Giunchiglia; Alessandro Armando,
    MRG: Building planners for real world complex applications,
    in «APPLIED ARTIFICIAL INTELLIGENCE»,
    1994
    , pp. 333 -
    357
  2. Fausto Giunchiglia; Alessandro Armando; Alessandro Cimatti; Paolo Traverso,
    First steps towards provably correct system synthesis of system code,
    CADE-12 Workshop on Correctness and Metatheoretic Extensibility of Automated Reasoning Systems,
    1994
    , pp. 28-
    30
    , (CADE-12 Workshop on Correctness and Metatheoretic Extensibility of Automated Reasoning Systems,
    Nancy, France,
    1994)

1993

  1. Fausto Giunchiglia; Paolo Traverso; Alessandro Cimatti; Luca Spalazzi; Sandro Dalbosco; Luciano Serafini; Enrico Giunchiglia; Alessandro Armando; Paolo Pecchiari,
    MRG: sistema di ragionamento,
    in «AUTOMAZIONE E STRUMENTAZIONE»,
    vol. 9,
    1993
    , pp. 97 -
    103
  2. Fausto Giunchiglia; Paolo Traverso; Alessandro Cimatti; Luca Spalazzi; Sandro Dalbosco; Luciano Serafini; Enrico Giunchiglia; Alessandro Armando; Paolo Pecchiari,
    MRG: un nucleo di ragionamento per un sistema integrato multifunzionale,
    in «SISTEMI INTELLIGENTI»,
    vol. 3,
    1993
    , pp. 435 -
    460
  3. Paolo Traverso; Luca Spalazzi; Alessandro Cimatti,
    A planning language and a semantics for real world autonomous agents,
    1993 Italian Planning Workshop,
    1993
    , (1993 Italian Planning Workshop,
    Roma, Italy,
    1993)
  4. Alessandro Cimatti; Fausto Giunchiglia; G. Mongardi; D. Romano; F. Torielli; Paolo Traverso,
    Valutazione del CBR-tool orientato all`help desk `Case Advisor`,
    In questo documento ci prefiggiamo di riportare gli esiti della valutazione di CaseAdvisor, strumento sviluppato dalla ICue Technology Inc., per il supporto del problem solving interattivo basato sul Case-Based Reasoning (CBR). Il gruppo fa capo a Qiang Yang, direttore dell`Information Service Agents Lab (ISA Lab) presso la Simon Fraser University (Burnaby, BC, Canada). Il prodotto in oggetto è stato inizialmente sviluppato per l`ambiente Windows, mentre una seconda versione in Java è attualmente in fase di sviluppo. A fini di valutazione, ci sono state fornite una versione `demo` per Windows ed un prototipo dell`applicazione in Java. La suite di tool per WIndows conmprende tre moduli: uno per la memorizzazione dei case-base su database relazionali, uno per l`authoring ed il mantenimento dei casi, ed un terzo per l`impiego della conoscenza presente nel CB e mirato alle applicazioni `Help Desk`. Nel presente documento ci occuperemo in dettaglio dei tre moduli, e passeremo rapidamente in rassegna le caratteristiche del prototipo in Java,
    1993

1992

  1. Paolo Traverso; Alessandro Cimatti; Luca Spalazzi,
    Beyond the single planning paradigm: introspective planning,
    10th European Conference on Artificial Intelligence (ECAI 1992),
    Wiley,
    1992
    , pp. 643-
    647
    , (10th European Conference on Artificial Intelligence (ECAI 1992),
    Vienna, Austria,
    1992)
  2. Luca Spalazzi; Alessandro Cimatti; Paolo Traverso,
    Implementing planning as tactical reasoning,
    3rd Annual Conference on Artificial Intelligence, Simulation & Planning in High Autonomy Systems (AIS`92),
    IEEE Computer Society,
    1992
    , pp. 80-
    85
    , (3rd Annual Conference on Artificial Intelligence, Simulation & Planning in High Autonomy Systems (AIS`92),
    Perth, Western Australia,
    1992)
  3. Paolo Traverso; Alessandro Cimatti; Luca Spalazzi; Enrico Giunchiglia,
    Building planners with explicit control mechanism,
    2nd International Symposium on Artificial Intelligence and Mathematics (ISAI 1992),
    AAAI Press,
    1992
    , pp. 195-
    202
    , (2nd International Symposium on Artificial Intelligence and Mathematics (ISAI 1992),
    Cancun, Mexico,
    1992)
  4. Alessandro Cimatti; Paolo Traverso; Luca Spalazzi,
    Programming Planners with Flexible Architectures,
    AI and Cognitive Science `92,
    Springer Verlag,
    1992
    , pp. 311-
    314
    , (AI and Cognitive Science `92,
    Limerick, Ireland,
    1992)
  5. Alessandro Cimatti; Paolo Traverso; Sandro Dalbosco; Alessandro Armando,
    Navigation by Combining Reactivity and Planning,
    Intelligent Vechicles `92 Symposium,
    IEEE Industrial Electronics,
    1992
    , pp. 265-
    270
    , (Intelligent Vechicles `92 Symposium,
    Detroit, USA,
    1992)
  6. Fausto Giunchiglia; Paolo Traverso; Alessandro Cimatti; Paolo Pecchiari,
    A System for Multi-Level Reasoning,
    IMSA `92, International Workshop on New Models for Software Architecture,
    1992
    , pp. 190-
    195
    , (IMSA `92, International Workshop on New Models for Software Architecture,
    Tokyo, Japan,
    1992)
  7. Fausto Giunchiglia; Paolo Traverso; Alessandro Cimatti; Luca Spalazzi,
    Tactics: extending the notion of plan,
    ECAI-92 Workshop `Beyond Sequential Planning`,
    1992
    , (ECAI-92 Workshop `Beyond Sequential Planning`,
    Vienna, Austria,
    1992)
  8. Fausto Giunchiglia; Paolo Traverso; Alessandro Cimatti; Luca Spalazzi; Sandro Dalbosco; Luciano Serafini; Enrico Giunchiglia; Alessandro Armando; Paolo Pecchiari,
    Un nucleo di ragionamento per un sistema integrato multi-funzionale: stato di avanzamento,
    Automation 1992, 36th ANIPLA Conference,
    Pirella,
    1992
    , pp. 620-
    633
    , (Automation 1992, 36th ANIPLA Conference,
    Genova,
    1992)
  9. Fausto Giunchiglia; Alessandro Cimatti; Sandro Dalbosco; Paolo Traverso; Luca Spalazzi,
    MRG: un sistema di ragionamento distribuito per applicazioni complesse,
    Atti seconda giornata di lavoro del gruppo Intelligenza Artificiale Distribuita (DAI) dell`AI*IA,
    1992
    , (Atti seconda giornata di lavoro del gruppo Intelligenza Artificiale Distribuita (DAI) dell`AI*IA,
    Roma,
    1992)