Publications

• A. Armando, S. Ranise, T. Turkmen, and B. Crispo. Efficient Run-time Solving of RBAC User Authorization Queries: Pushing the Envelope. In the Proceedings of the 2nd ACM Conference on Data and Application Security and Privacy (CODASPY'12), San Antonio, TX (USA), February 7-9, 2012.
• A. Armando, R. Carbone, and S. Ranise. Automated Analysis of Semantic-Aware Access Control Policies: a Logic-Based Approach. In the Proceedings of the IEEE Workshop on Semantic Computing for Security and Privacy, San Francisco (USA), September 21, 2011.
• A. Armando and S. Ranise. Automated Analysis of Infinite State Workflows with Access Control Policies. In the Proceedings of the 7th International Workshop on Security and Trust Management, Copenhagen (Denmark), July 27-28, 2011.
• F. Alberti, A. Armando, and S. Ranise. ASASP: Automated Symbolic Analysis of Administrative Policies. In Proceedings of the 23rd International Conference on Automated Deduction (CADE-23), Wroclaw (Poland), July 31-August 5, 2011.
• A. Armando, R. Carbone, L. Compagna, J. Cuellar, G. Pellegrino, A. Sorniotti. From Multiple Credentials to Browser-based Single Sign-On: Are We More Secure? In the Proceedings of the 26th IFIP TC-11 International Information Security Conference (SEC 2011), Luzern (Switzerland), June 7-9, 2011.
• A. Armando, R. Carbone, L. Compagna, G. Pellegrino. Automatic Security Analysis of SAML-based Single Sign-On Protocols. In ``Digital Identity and Access Management: Technologies and Frameworks'', IGI Global. R. Sharman, S. Das Smith and M. Gupta, editors. To appear.
• A. Armando, E. Giunchiglia, M. Maratea and S. E. Ponta. An Action-based Approach to the Formal Specification and Automatic Analysis of Business Processes under Authorization Constraints. In the Journal of Computer and System Sciences vol. 1, pages 119-141, 2012.
• F. Alberti, A. Armando and S. Ranise. Efficient Symbolic Automated Analysis of Administrative Attribute-based RBAC-Policies. In Proceedings of the 6th ACM Symposium on Information, Computer and Communications Security (ASIACCS'11), Hong Kong, March 22-24, 2011.
• A. Armando and S. Ranise. Automated Symbolic Analysis of ARBAC Policies. In Proceedings of 6th International Workshop on Security and Trust Management (STM'10), Athens, September 23-24, 2010.
• A. Merlo and A. Armando. Cooperative Access Control for the Grid. Proceedings of the 6th International Conference on Information Assurance and Security (IAS 2010), Atlanta, GA, USA, August 23-24, 2010.
• A. Armando and S. E. Ponta. Model Checking of Security-sensitive Business Processes. Proceedings of the 6th International Workshop on Formal Aspects in Security and Trust (FAST2009), Eindhoven, the Netherlands, November 5-6, 2009.
• A. Armando. Building SMT-based Software Model Checkers: an Experience Report. (Invited Paper) In the proceeding of the 7th International Symposium on Frontiers of Combining Systems (FroCoS'09), Trento, Italy, September 16-18, 2009.
• A. Armando, R. Carbone and L. Compagna. LTL Model Checking for Security Protocols. Journal of Applied Non-Classical Logics, special issue on Logic and Information Security, vol. 19/4, pp. 403-429, 2009.
• A. Armando, E. Giunchiglia and S. E. Ponta. Formal Specification and Automatic Analysis of Business Processes under Authorization Constraints: an Action-based Approach. Proceedings of the 6th International Conference on Trust, Privacy & Security in Digital Business (TrustBus'09), August 31 - September 4, 2009, Linz, Austria.
• A. Armando, R. Carbone, L. Compagna, J. Cuellar and L. Tobarra. Formal Analysis of SAML 2.0 Web Browser Single Sign-On: Breaking the SAML-based Single Sign-On for Google Apps. In the proceeding of the 6th ACM Workshop on Formal Methods in Security Engineering (FMSE 2008), October 27th, 2008, Hilton Alexandria Mark Center, Virginia, USA.
  • See the following page for more information.
• A. Armando, J. Mantovani and L. Platania. Bounded Model Checking of Software using SMT Solvers instead of SAT Solvers. International Journal on Software Tools for Technology Transfer (STTT), volume 11, issue 1, pp. 69-83, 2009.
• A. Armando, M. Benerecetti, D. Carotenuto, J. Mantovani and P. Spica. The Eureka Tool for Software Model Checking. In the proceedings of the 22nd IEEE/ACM ASE Conference, November 5-9, 2007, Atlanta, Georgia, USA.
• A. Armando and L. Compagna. SAT-based Model Checking for Security Protocols Analysis. International Journal of Information Security, vol. 7, no. 1. January 2008.
• A. Armando, M. P. Bonacina, S. Ranise, and S. Schulz. New results on rewrite-based satisfiability procedures. ACM Transactions on Computational Logic (TOCL), vol. 10, no. 1, 2009.
• A. Armando, R. Carbone and L. Compagna. LTL Model Checking for Security Protocols. In the proceedings of the 20th IEEE Computer Security Foundations Symposium (CSF20), July 6-8, 2007, Venice, Italy.
• A. Armando, M. Benerecetti and J. Mantovani. Abstraction Refinement of Linear Programs with Arrays. In the Proceedings of the 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'07), March 24-April 1, 2007, Braga, Portugal, LNCS 4424, pp. 373-388.
• A. Armando, J. Mantovani and L. Platania. Bounded Model Checking of Software using SMT Solvers instead of SAT Solvers. In the Proceedings of the 13th International SPIN Workshop on Model Checking of Software (SPIN'06), March 30-April 1, 2006, Vienna, Austria. LNCS 3925, Pp. 146-162.
• A. Armando, D. Basin, J. Cuellar, M. Rusinowitch L. Viganò. AVISPA: Automated Validation of Internet Security Protocols and Applications, ERCIM News, no. 64, page 66-67, January 2006.
• A. Armando, M. P. Bonacina, S. Ranise, and S. Schulz. On a rewriting approach to satisfiability procedures: extension, combination of theories and an experimental appraisal. In the Proceedings of 5th International Workshop on Frontiers of Combining Systems (FroCoS 2005), Vienna Austria, September 19-21, 2005. Pp. 65-80, Springer Verlag.
• A. Armando, M. Benerecetti, J. Mantovani. Model Checking Linear Programs with Arrays. In the Proceedings of the 3rd Workshop on Software Model Checking (SoftMC'05), July 11, 2005 Edinburgh, Scotland. Electronic Notes in Theoretical Computer Science vol. 952, pp. 79-94, 2005.
• A. Armando, D. Basin, Y. Boichut, Y. Chevalier, L. Compagna, J. Cuellar, P. Hankes Drielsma, P.C. Heám, O. Kouchnarenko, J. Mantovani, S. Mödersheim, D. von Oheimb, M. Rusinowitch, J. Santiago, M. Turuani, L. Viganò, L. Vigneron. The AVISPA Tool for the Automated Validation of Internet Security Protocols and Applications. In the Proceedings of the 17th International Conference on Computer-Aided Verification (CAV'05), Edinburgh, Scotland, July 6-10, 2005.
• A. Armando, C. Castellini, E. Giunchiglia, M. Maratea. The SAT-based Approach to Separation Logic. Journal of Automated Reasoning. Vol. 35. Nos. 1-3, pp. 237-263, 2005.
• A. Armando, L. Compagna, S. Ranise. Rewrite and Decision Procedure Laboratory: Combining Rewriting, Satisfiability Checking, and Lemma Speculation. In Mechanizing Mathematical Reasoning, Essays in Honor of Jörg H. Siekmann on the Occasion of his 60th Birthday. D. Hutter and W. Stephan (Eds.). Lecture Notes in Computer Science, Volume 2605, Jan 2005, Pp. 30-45, Springer Verlag.
• A. Armando, C. Castellini, E. Giunchiglia, F. Giunchiglia, A. Tacchella. SAT-Based Decision Procedures for Automated Reasoning: a Unifying Perspective. In Mechanizing Mathematical Reasoning, Essays in Honor of Jörg H. Siekmann on the Occasion of his 60th Birthday. D. Hutter and W. Stephan (Eds.). Lecture Notes in Computer Science, Volume 2605, Jan 2005, Pp. 46-58, Springer Verlag.
• A. Armando, C. Ballarin. A Reconstruction and Extension of Maple's Assume Facility via Constraint Contextual Rewriting. Journal of Symbolic Computation, vol. 39/5, pp. 503-521, 2005. ISSN: 0747-7171.
• A. Armando, C. Castellini, and J. Mantovani. Software Model Checking using Linear Constraints. In the Proceedings of the 6th International Conference on Formal Engineering Methods (ICFEM'04), Nov 8-12, 2004, Seattle, USA.
• A. Armando and L. Compagna. SATMC: a SAT-based Model Checker for Security Protocols. In proceedings of the 9th European Conference on Logics in Artificial Intelligence (JELIA'04), September 27-30, 2004, Lisbon, Portugal.
• A. Armando, L. Compagna, and Y. Lierler. Automatic Compilation of Protocol Insecurity Problems into Logic Programming. In proceedings of the 9th European Conference on Logics in Artificial Intelligence (JELIA'04), September 27-30, 2004, Lisbon, Portugal.
• A. Armando, C. Castellini, E. Giunchiglia, M. Idini, and M. Maratea. TSAT++: an Open Platform for Satisfiability Modulo Theories. In the Proceedings of the 2nd Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR'04), July 05, 2004, Cork, Ireland. In Electronic Notes in Theoretical Computer Science vol. 125 pp. 25-36.
• A. Armando and L. Compagna. An Optimized Intruder Model for SAT-based Model-Checking of Security Protocols. In proceedings of the Workshop on Automated Reasoning for Security Protocol Analysis (ARSPA), July 4, 2004. Cork, Ireland.
• A. Armando, C. Castellini, E. Giunchiglia, and M. Maratea. A SAT-based Decision Procedure for the Boolean Combination of Difference Constraints. In the Proceedings of the 7th International Conference on Theory and Applications of Satisfiability Testing (SAT'04). May 10-13 2004, Vancouver, BC, Canada.
• A. Armando, L. Compagna and P. Ganty. SAT-based Model-Checking of Security Protocols using Planning Graph Analysis. In the proceedings of the 12th International FME Symposium (FME 2003), September 8-14 2003, Pisa, Italy. LNCS 2885. Copyright © Springer-Verlag.
• A. Armando and L. Compagna. Abstraction-driven SAT-based Analysis of Security Protocols. In the proceedings of the Sixth International Conference on Theory and Applications of Satisfiability Testing (SAT 2003), May 5-8, 2003, S.Margherita Ligure, Italy. LNCS 2919. Copyright © Springer-Verlag.
• A. Armando and S. Ranise. Constraint Contextual Rewriting. Journal of Symbolic Computation, Volume 36, Issues 1-2, pp. 193-216, 2003. Special Issue on FTP 2000, International Workshop on First-Order Theorem Proving. Peter Baumgartner and Hantao Zhang, Editors.
• A. Armando, S. Ranise, M. Rusinowitch. The Rewriting Approach to Satisfiability Procedures. Information and Computation 183 (2003) pp. 140-164.
• A. Armando and L. Compagna. Automatic SAT-compilation of Protocol Insecurity Problems via Reduction to Planning. In the Proceedings of the Joint International Conference on Formal Techniques for Networked and Distributed Systems (FORTE 2002), November 11-14, 2002, Houston, Texas, pp. 210-225. This paper has also been presented at the Joint Workshops on Foundations of Computer Security (FCS02) and Verification (VERIFY02), Copenhagen, Denmark, July 25-26, 2002.
• A. Armando, D. Basin, M. Bouallagui, Y. Chevalier, L. Compagna, S. Moedersheim, M. Rusinowitch, M. Turuani, L. Viganò, and L. Vigneron. The AVISS Security Protocol Analysis Tool. In the Proceedings of the 14th Conference on Computer-Aided Verification (CAV'02), pp. 249-353, Copenhagen, Denmark, July 27-31, 2002.
• A. Armando and P. De Lucia. Symbolic Model-Checking of Linear Programs. In the Proceedings of the 2nd Workshop on Specification, Analysis and Validation for Emerging Technologies in Computational Logic (SAVE02), Copenhagen, Denmark, July 27, 2002.
• A. Armando, M. P. Bonacina, A. K. Sehgal, S. Ranise, and M. Rusinowitch. High-performance deduction for verification: a case study in the theory of arrays. In the Proceedings of the 2nd Verification Workshop (VERIFY02), pp. 103-112, Copenhagen, Denmark, July 25-26, 2002.
• A. Armando, M. Rusinowitch, S. Stratulat. Incorporating Decision Procedures in Implicit Induction In the Journal of Symbolic Computation (Special Issue on the Integration of Automated Reasoning and Computer Algebra Systems) Vol. 34, No. 4, pp. 241-258, October, 2002.
• A. Armando, F. Peccia, S. Ranise. The Phase Transition of the Linear Inequalities Problem. In the Proceedings on the 7th International Conference on Principles and Practice of Constraint Programming (CP2001), Paphos, Cyprus, Nov 26 - Dec 1, 2001, pp. 422-432.
• A. Armando, S. Ranise, M. Rusinowitch. Uniform Derivation of Decision Procedures by Superposition. In the Proceedings on the Annual Conference on Computer Science Logic (CSL01), Paris, France, 10-13 September 2001, pp. 513-527.
• A. Armando, S. Ranise, M. Rusinowitch. A Superposition Based Methodology to Design Satisfiability Decision Procedures. In the Proceedings on the 5th International Workshop on Unification (UNIF'2001), Siena, Italy, 18-19 June 2001, pp. 8-12.
• A. Armando, C. Ballarin. Maple's Evaluation Process as Constraint Contextual Rewriting. In the Proceedings of the International Symposium on Symbolic and Algebraic Computation (ISSAC'2001), pp. 32-37, July 22-25, 2001, ORCCA and University of Western Ontario.
• A. Armando, M. Rusinowitch, S. Stratulat. Incorporating Decision Procedures in Implicit Induction. In the Proceedings of the 9th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning (CALCULEMUS-2001). Siena, June 21-22 2001, pp. 155-167.
• A. Armando, L. Compagna, S. Ranise. RDL---Rewrite and Decision procedure Laboratory. In the Proceedings of the International Joint Conference on Automated Reasoning (IJCAR 2001), June 18-23, Siena, Italy. Lecture Notes in Artificial Intelligence, n. 2083, pp. 663-669.
• A. Armando, S. Ranise. A Practical Extension Mechanism for Decision Procedures: the Case Study of Universal Presburger Arithmetic. In the Journal of Universal Computer Science vol. 7:2, pp. 124-140, 2001. A short version of the paper has been presented at the 4th Workshop on Tools for System Design and Verification (FM-TOOLS 2000), p. 53-57. Reisenburg Castle near Ulm, Germany. Monday 10 July - Thursday 13 July 2000.
• A. Armando, A. Coglio, F. Giunchiglia, S. Ranise. The Control Layer in Open Mechanized Reasoning Systems: Annotations and Tactics . In the Journal of Symbolic Computation (Special Issue on Calculemus-99: Integrating Computation and Deduction) Vol. 32, No. 4, October 1, 2001, pp. 305-332.
• J. Zimmer, A. Armando, C. Giromini. Towards Mathematical Agents -- Combining MathWeb-SB and LBA. In the Proceedings of the 9th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning (CALCULEMUS-2001). Siena, June 21-22 2001, pp. 64-77.
• A. Armando, S. Ranise. Termination of Constraint Contextual Rewriting. In the Proceedings of the 3rd International Workshop on Frontiers of Combining Systems (FroCoS'2000). Nancy (France), March 22-24, 2000. Lecture Notes in Computer Science, Volume 1794, pp. 47--61.
• A. Armando, M. Kohlhase, S. Ranise. Communication Protocols for Mathematical Services based on KQML and OMRS. In Symbolic Computation and Automated Reasoning. Proceedings of the Eight Symposium on the Integration of Symbolic Computation and Mechanized Reasoning (CALCULEMUS-2000), St. Andrew (Scotland), 6-7 August 2000. M. Kerber and M. Kohlhase, editors, pag. 33-48. A K Peters Publisher, Natick, Massachussetts, 2001.
• A. Armando, D. Zini. Interfacing Computer Algebra and Deduction Systems via the Logic Broker Architecture. In Symbolic Computation and Automated Reasoning, proceedings of the Eight Symposium on the Integration of Symbolic Computation and Mechanized Reasoning (CALCULEMUS-2000), St. Andrew (Scotland), 6-7 August 2000. M. Kerber and M. Kohlhase, editors, pag. 49-64. A K Peters Publisher, Natick, Massachussetts, 2001.
• A. Armando, C. Castellini, E. Giunchiglia. SAT-based procedures for temporal reasoning. In the Proceeding of the 5th European Conference on Planning (ECP-99). Durham (UK), September 8-10, 1999.
• A. Armando, A. Smaill, I. Green. Automatic Synthesis of Recursive Programs: the Proof-Planning Paradigm. In Automated Software Engineering, 6(4): 329-356, October 1999. Short version in the Proceedings of the 12th IEEE Conference on Automated Software Engineering - ASE'97, November 3 - 5, 1997. Lake Tahoe, Nevada; USA. Nominee for the best paper award.
• A. Armando, A. Coglio, F. Giunchiglia. The Control Component of Open Mechanized Reasoning Systems. In Electronic Notes in Theoretical Computer Science Volume 23, Issue 3, pp. 1--18, 1999.
• A. Armando, S. Ranise. Constraint Contextual Rewriting. In Proceedings of the International Workshop on First order Theorem Proving (FTP'98) pp. 65-75. Schloss Wilhelminenberg, Vienna, Austria November 23 - 25, 1998.
• A. Armando, J. Gallagher, A. Smaill, A. Bundy. Automating the Synthesis of Decision Procedures in a Constructive Metatheory. In the Annals of Mathematics and Artificial Intelligence vol. 22, n.3,4, pp. 259-279, 1998. Short version in the Proceedings of the Fourth International Symposium on Artificial Intelligence and Mathematics, pp. 5--8, Florida, January 3-5, 1996.
• A. Armando, P. Bertoli, A. Coglio, F. Giunchiglia, J. Meseguer, S. Ranise, C. Talcott. Open Mechanized Reasoning Systems: a Preliminary Report. In the Proceedings of the CADE Workshop on Integration of Deduction Systems. July 5-6, 1998, Lindau, Germany.
• A. Armando, S. Ranise. From Integrated Reasoning Specialists to ``Plug-and-Play'' Reasoning Components. In Proceedings of the Fourth International Conference Artificial Intelligence and Symbolic Computation (AISC98) LNCS vol. 1476, p. 42-54. Plattsburgh, NY, USA. September 16-18, 1998.
• F. Giunchiglia, P. Pecchiari, A. Armando. Towards provably correct system synthesis and extension. In the Journal of Future Generation Computer Systems vol. 12, no. 2/3, p. 1-15, 1996.
• E. Giunchiglia, A. Armando, P. Pecchiari. Structured Proof Procedures. In the Annals of Artificial Intelligence and Mathematics, vol. 15, n. 1, 1995.
• A. Armando, E. Giunchiglia. Embedding complex decision procedures inside an interactive theorem prover. In the Annals of Artificial Intelligence and Mathematics, vol. 8, n. 3-4, 1993.
• A. Armando, A. Cimatti, and L. Viganò. Building and Executing Proof Strategies in a Formal Metatheory. In Advances in Artificial Intelligence. Proc. AI*IA'93, number LNAI 728 in Lecture Notes in Artificial Intelligence, pp. 1--10, Torino, Italia, 26-28 Ottobre 1993. Springer Verlag.