You are here

Publications

  1. Armando A.; Compagna L.; Ganty P.,
    SAT-based Model-Checking of Security Protocols using Planning Graph Analysis,
    in «LECTURE NOTES IN COMPUTER SCIENCE»
    vol.2885,
    2003
    , (12th International FME Symposium (FME 2003),
    Pisa, Italy,
    8-14/09/2003)
  2. Armando A.; Compagna L.,
    Abstraction-driven SAT-based Analysis of Security Protocols,
    in «LECTURE NOTES IN COMPUTER SCIENCE»
    vol.2919,
    2003
    , pp. 257-
    271
    , (SAT 2003,
    S.Margherita Ligure, Italy,
    5-8/05/2003)
  3. Armando A.; Basin D.; Boullagui M.; Chevalier Y.; Compagna L.; Moedersheim S.; Rusinowitch M.; Turuani M.; Viganò L.; Vigneron L.,
    The AVISS Security Protocol Analysis Tool,
    in «LECTURE NOTES IN COMPUTER SCIENCE»
    vol.2404,
    2002
    , (14th Conference on Computer-Aided Verification (CAV'02),
    Copenhagen, Denmark,
    27-31/06/2002)
  4. Armando A.; Compagna L.,
    Automatic SAT-Compilation of Protocol Insecurity Problems via Reduction to Planning,
    in «LECTURE NOTES IN COMPUTER SCIENCE»
    vol.2529,
    2002
    , pp. 210-
    225
    , (Joint International Conference on Formal Techniques for Networked and Distributed Systems (FORTE 2002),
    Houston, Texas,
    11-14/11/2002)
  5. Armando A.; Campagna L.,
    Automatic SAT-compilation of Protocol Insecurity Problems via Reduction to Planning,
    2002
    , (Joint Workshops on Foundations of Computer Security (FCS02) and Verification (VERIFY02),
    Copenhagen, Denmark,
    25-26/07/2002)
  6. Armando A.; De Lucia P.,
    Symbolic Model-Checking of Linear Programs,
    Proceedings of the 2nd Workshop on Specification, Analysis and Validation for Emerging Technologies in Computational Logic (SAVE02),
    2002
    , (2nd Workshop on Specification, Analysis and Validation for Emerging Technologies in Computational Logic (SAVE02),
    Copenhagen, Denmark,
    27/07/2002)
  7. Armando A.; Bonacina M.P.; Sehgal A. K.; Ranise S.; Rusinowitch M.,
    High Performance Deduction for verification: a case study in the theory of arrays,
    Proceedings of the 2nd Verification Workshop (VERIFY02),
    2002
    , pp. 103-
    112
    , (2nd Verification Workshop (VERIFY02),
    Copenhagen, Denmark,
    25-26/07/2002)
  8. A. Armando; C. Castellini; E. Giunchiglia; Fausto Giunchiglia; A. Tacchella,
    SAT-Based Decision Procedures for Automated Reasoning: a Unifying Perspective,
    Propositional reasoning (SAT) is an essential part of many reasoning tasks. Many problems in computer science can be compiled to SAT and then effectively decided using state-of-the-art solvers. Alternatively, if reduction to SAT is not feasible, the ideas and technology of state-of-the-art SAT solvers can be useful in deciding the propositional component of the reasoning task being considered. This last approach has been used in different contexts by different authors, many times by authors of this paper. Because of the essential role played by the SAT solver, these decision procedures have been called "SAT-based". SAT-based decision procedures have been proposed for various logics, but also in other areas such as planning. In this paper we present a unifying perspective on the various SAT-based approaches to these different reasoning tasks,
    2002
  9. ARMANDO A.; COGLIO A.; GIUNCHIGLIA F.; RANISE S.,
    The Control Layer in Open Mechanized Reasoning Systems: Annotations and Tactics,
    in «JOURNAL OF SYMBOLIC COMPUTATION»,
    vol. 32,
    2001
    , pp. 305 -
    332
  10. ARMANDO A.; COGLIO A.; GIUNCHIGLIA F.; RANISE S.,
    The Control Component of Open Mechanized Reasoning Systems: Annotation and Tactics,
    in «JOURNAL OF SYMBOLIC COMPUTATION»,
    vol. 32,
    2001
    , pp. 305 -
    332

Pages