You are here

Publications

  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
  8. Alessandro Cimatti; Paolo Traverso,
    Computational Reflection via Mechanized Logical Deduction,
    in «INTERNATIONAL JOURNAL OF INTELLIGENT SYSTEMS»,
    vol. 11,
    n. 5,
    1996
    , pp. 279 -
    293
  9. 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
  10. 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)

Pages