Alessandro Armando's Selected Publications

[107] A. Armando, G. Costa, A. Merlo, and L. Verderame. Formal modeling and automatic enforcement of bring your own device policies. International Journal of Information Security, pages 1--18, Aug. 2014. [ DOI | .pdf ]
[106] A. Armando, G. Costa, A. Merlo, and L. Verderame. Enabling byod through secure meta-market. In Proceedings of the 2014 ACM Conference on Security and Privacy in Wireless and Mobile Networks, WiSec '14, pages 219--230, New York, NY, USA, July 2014. ACM. [ DOI | .pdf ]
[105] A. Armando, G. Costa, L. Verderame, and A. Merlo. Securing the “bring your own device” paradigm. IEEE Computer, 47(6):48--56, 2014. [ DOI | .pdf ]
[104] A. Armando, R. Carbone, and L. Compagna. Satmc: a sat-based model checker for security-critical systems. In TACAS'14: Proceedings of the 20th international Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 31--45. Springer, 2014. [ DOI | .pdf ]
[103] A. Armando and S. E. Ponta. Model checking authorization requirements in business processes. Computers & Security, 40(0):1 -- 22, 2014. [ DOI | .pdf ]
[102] A. Armando, M. Benerecetti, and J. Mantovani. Counterexample-guided abstraction refinement for linear programs with arrays. Automated Software Engineering, 21(2):225--285, 2014. [ DOI | .pdf ]
[101] S. Ranise, A. Truong, and A. Armando. Scalable and precise automated analysis of administrative temporal role-based access control. In SACMAT2014: Proceedings of the 19th ACM Symposium on Access Control Models and Technologies. ACM press, 2014. to appear. [ .pdf ]
[100] A. Armando, R. Carbone, E. G. Chekole, and S. Ranise. Attribute based access control for apis in spring security. In SACMAT2014: Proceedings of the 19th ACM Symposium on Access Control Models and Technologies. ACM press, 2014. to appear. [ .pdf ]
[99] A. Armando, R. Carbone, E. G. Chekole, C. Petrazzuolo, A. Ranalli, and S. Ranise. Selective release of smart metering data in multi-domain smart grids. In SmartGridSec14: Proceedings of the Second Open EIT ICT Labs Workshop on Smart Grid Security. Springer, 2014. to appear. [ .pdf ]
[98] A. Armando, S. Oudkerk, S. Ranise, and K. Wrona. Formal modelling of content-based protection and release for access control in nato operations. In Foundations and Practice of Security - 6th International Symposium, FPS 2013, La Rochelle, France, October 21-22, 2013, Revised Selected Papers, volume 8352 of Lecture Notes in Computer Science, pages 227--244. Springer, 2014. [ .pdf ]
[97] A. Armando, A. Merlo, and L. Verderame. Security considerations related to the use of mobile devices in the operation of critical infrastructures. International Journal of Critical Infrastructure Protection, 7(4):247 -- 256, 2014. [ DOI | http ]
[96] A. Armando, G. Costa, and A. Merlo. Formal modeling and reasoning about the android security framework. In C. Palamidessi and M. Ryan, editors, TGC'12: 7th International Symposium on Trustworthy Global Computing, volume 8191 of Lecture Notes in Computer Science, pages 64--81. Springer Berlin Heidelberg, 2013. [ DOI | .pdf ]
[95] A. Armando, R. Carbone, L. Compagna, J. Cuéllar, G. Pellegrino, and A. Sorniotti. An authentication flaw in browser-based single sign-on protocols: Impact and remediations. Computers & Security, 33(0):41 -- 58, 2013. <ce:title>Future Challenges in Security and Privacy for Academia and Industry</ce:title>. [ DOI | .pdf ]
[94] A. Armando, A. Merlo, M. Migliardi, and L. Verderame. Breaking and fixing the android launching flow. Computers & Security, 39, Part A(0):104 -- 115, 2013. [ DOI | .pdf ]
[93] A. Armando, R. Carbone, and L. Zanetti. Formal modeling and automatic security analysis of two-factor and two-channel authentication protocols. In J. Lopez, X. Huang, and R. Sandhu, editors, Network and System Security (NSS), volume 7873 of Lecture Notes in Computer Science, pages 728--734. Springer Berlin Heidelberg, 2013. [ DOI | .pdf ]
[92] A. Armando, R. Carbone, and A. Merlo. Formal analysis of a privacy-preserving billing protocol. In J. Cuéllar, editor, SmartGridSec 2012: First International Workshop on Smart Grid Security, volume 7823 of Lecture Notes in Computer Science, pages 108--119. Springer Berlin Heidelberg, 2013. [ DOI | .pdf ]
[91] A. Armando, M. Grasso, S. Oudkerk, S. Ranise, and K. Wrona. Content-based information protection and release in nato operations. In SACMAT '13: Proceedings of the 18th ACM symposium on Access control models and technologies, pages 261--264, New York, NY, USA, 2013. ACM. [ DOI | .pdf ]
[90] A. Armando, A. Castiglione, G. Costa, U. Fiore, A. Merlo, L. Verderame, and I. You. Trustworthy opportunistic access to the internet of services. In ICT-EurAsia'13: Proceedings of the 2013 international conference on Information and Communication Technology, pages 469--478, Berlin, Heidelberg, 2013. Springer-Verlag. [ DOI | .pdf ]
[89] A. Armando, G. Costa, and A. Merlo. Bring your own device, securely. In SAC '13: Proceedings of the 28th Annual ACM Symposium on Applied Computing, pages 1852--1858, New York, NY, USA, 2013. ACM. [ DOI | .pdf ]
[88] S. Ranise, A. Truong, and A. Armando. Boosting model checking to analyse large arbac policies. In A. Jøsang, P. Samarati, and M. Petrocchi, editors, Security and Trust Management, volume 7783 of Lecture Notes in Computer Science, pages 273--288. Springer Berlin Heidelberg, 2013. [ DOI | .pdf ]
[87] A. Armando, E. Giunchiglia, M. Maratea, and S. E. Ponta. Modeling and reasoning about business processes under authorization constraints: A planning-based approach. In 23rd International Conference on Automated Planning and Scheduling (ICAPS). AAAI, 2013.
[86] A. Armando, A. Merlo, and L. Verderame. An empirical evaluation of the android security framework. In L. Janczewski, H. Wolfe, and S. Shenoi, editors, Security and Privacy Protection in Information Processing Systems, Proceedings of the 28th IFIP TC 11 International Conference, SEC 2013, Auckland, New Zealand, July 8-10, 2013., volume 405 of IFIP Advances in Information and Communication Technology, pages 176--189. Springer Berlin Heidelberg, 2013. [ DOI | .pdf ]
[85] A. Armando, R. Carbone, L. Compagna, and G. Pellegrino. Automatic security analysis of saml-based single sign-on protocols. In R. Sharman, S. Das Smith, and M. Gupta, editors, Digital Identity and Access Management: Technologies and Frameworks, pages 168--187. IGI Global, Hershey, PA, USA, 2012. [ DOI | .pdf ]
[84] A. Armando and G. Lowe. Preface. Journal of Computer Security, 20(1):1, 2012. [ DOI ]
[83] A. Armando, A. Merlo, M. Migliardi, and L. Verderame. Would you mind forking this process? a denial of service attack on android (and some countermeasures). In D. Gritzalis, S. Furnell, and M. Theoharidou, editors, Information Security and Privacy Research, volume 376 of IFIP Advances in Information and Communication Technology, pages 13--24. Springer Berlin Heidelberg, 2012. [ DOI | .pdf ]
[82] A. Armando and H. Orman. Preface - wscs 2012. page xiv, 2012.
[81] A. Armando and S. Ranise. Scalable automated symbolic analysis of administrative role-based access control policies by smt solving. Journal of Computer Security, 20(4):309--352, 2012. [ DOI | .pdf ]
[80] S. Ranise and A. Armando. On the automated analysis of safety in usage control: a new decidability result. In NSS'12: Proceedings of the 6th international conference on Network and System Security, pages 15--28, Berlin, Heidelberg, 2012. Springer-Verlag. [ DOI | .pdf ]
[79] A. Armando and S. Ranise. Automated and efficient analysis of role-based access control with attributes. In DBSec'12: Proceedings of the 26th Annual IFIP WG 11.3 conference on Data and Applications Security and Privacy, pages 25--40, Berlin, Heidelberg, 2012. Springer-Verlag. [ DOI | .pdf ]
[78] A. Armando, G. Pellegrino, R. Carbone, A. Merlo, and D. Balzarotti. From model-checking to automated testing of security protocols: bridging the gap. In TAP'12: Proceedings of the 6th international conference on Tests and Proofs, pages 3--18, Berlin, Heidelberg, 2012. Springer-Verlag. [ DOI | .pdf ]
[77] A. Armando, W. Arsac, T. Avanesov, M. Barletta, A. Calvi, A. Cappai, R. Carbone, Y. Chevalier, L. Compagna, J. Cuéllar, G. Erzse, S. Frau, M. Minea, S. Mödersheim, D. von Oheimb, G. Pellegrino, S. E. Ponta, M. Rocchetto, M. Rusinowitch, M. Torabi Dashti, M. Turuani, and L. Viganò. The avantssar platform for the automated validation of trust and security of service-oriented architectures. In TACAS'12: Proceedings of the 18th international Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 267--282, Berlin, Heidelberg, 2012. Springer-Verlag. [ DOI | .pdf ]
[76] A. Armando, S. Ranise, F. Turkmen, and B. Crispo. Efficient run-time solving of rbac user authorization queries: pushing the envelope. In CODASPY '12: Proceedings of the second ACM conference on Data and Application Security and Privacy, pages 241--248, New York, NY, USA, 2012. ACM. [ DOI | .pdf ]
[75] 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. Journal of Computer and System Sciences, 78(1):119--141, 2012. [ DOI | .pdf ]
[74] A. Armando and S. Ranise. Automated analysis of infinite state workflows with access control policies. In STM'11: Proceedings of the 7th international conference on Security and Trust Management, pages 157--174, Berlin, Heidelberg, 2012. Springer-Verlag. [ DOI | .pdf ]
[73] A. Armando, G. Costa, A. Merlo, and L. Verderame. Securing the “bring your own device” policy. Journal of Internet Services and Information Security (JISIS), 2(3/4):3--17, 2012. Short version of this paper has been presented at the 4th International Workshop on Managing Insider Security Threats (MIST 2012), November 8-9, 2012 Nishijin Plaza, Kyushu University, Fukuoka, Japan. [ .pdf ]
[72] A. Armando, R. Carbone, L. Compagna, J. Cuéllar, G. Pellegrino, and A. Sorniotti. From multiple credentials to browser-based single sign-on: Are we more secure? In J. Camenisch, S. Fischer-Hübner, Y. Murayama, A. Portmann, and C. Rieder, editors, Future Challenges in Security and Privacy for Academia and Industry, volume 354 of IFIP Advances in Information and Communication Technology, pages 68--79. Springer Berlin Heidelberg, 2011. [ DOI | .pdf ]
[71] A. Armando, T. Benzel, E. Hovy, A. Hussain, H. Orman, and B. Thuraisingham. Preface. page xxiv, 2011.
[70] A. Armando, R. Carbone, and S. Ranise. Automated analysis of semantic-aware access control policies: A logic-based approach. In ICSC '11: Proceedings of the 2011 IEEE Fifth International Conference on Semantic Computing, pages 356--363, Washington, DC, USA, 2011. IEEE Computer Society. [ DOI | .pdf ]
[69] F. Alberti, A. Armando, and S. Ranise. Efficient symbolic automated analysis of administrative attribute-based rbac-policies. In ASIACCS '11: Proceedings of the 6th ACM Symposium on Information, Computer and Communications Security, pages 165--175, New York, NY, USA, 2011. ACM. [ DOI | .pdf ]
[68] A. Armando and S. Ranise. Automated symbolic analysis of arbac-policies. In STM'10: Proceedings of the 6th international conference on Security and trust management, pages 17--34, Berlin, Heidelberg, 2011. Springer-Verlag. [ DOI | .pdf ]
[67] A. Merlo and A. Armando. Cooperative access control for the grid. In Information Assurance and Security (IAS), 2010 Sixth International Conference on, pages 228--233, 2010. [ DOI | .pdf ]
[66] A. Armando and G. Lowe. Preface. In Joint Workshop on Automated Reasoning for Security Protocol Analysis and Issues in the Theory of Security, ARSPA-WITS, volume 6186 LNCS, page VI, 2010. [ DOI ]
[65] A. Armando, P. Baumgartner, and G. Dowek. Preface. Journal of Automated Reasoning, 45(2):89--89, 2010. [ DOI ]
[64] A. Armando, R. Carbone, L. Compagna, K. Li, and G. Pellegrino. Model-checking driven security testing of web-based applications. In ICSTW '10: Proceedings of the 2010 Third International Conference on Software Testing, Verification, and Validation Workshops, pages 361--370, Washington, DC, USA, 2010. IEEE Computer Society. [ DOI | .pdf ]
[63] A. Armando and S. E. Ponta. Model checking of security-sensitive business processes. In FAST'09: Proceedings of the 6th international conference on Formal Aspects in Security and Trust, pages 66--80, Berlin, Heidelberg, 2010. Springer-Verlag. [ DOI | .pdf ]
[62] A. Armando. Building smt-based software model checkers: an experience report. In FroCoS'09: Proceedings of the 7th international conference on Frontiers of combining systems, pages 1--17, Berlin, Heidelberg, 2009. Springer-Verlag. [ DOI | .pdf ]
[61] A. Armando, E. Giunchiglia, and S. E. Ponta. Formal specification and automatic analysis of business processes under authorization constraints: An action-based approach. In TrustBus '09: Proceedings of the 6th International Conference on Trust, Privacy and Security in Digital Business, pages 63--72, Berlin, Heidelberg, 2009. Springer-Verlag. [ DOI | .pdf ]
[60] A. Armando, J. Mantovani, and L. Platania. Bounded model checking of software using smt solvers instead of sat solvers. International Journal of Software Tools for Technology Transfer, 11(1):69--83, 2009. [ DOI | .pdf ]
[59] A. Armando, M. P. Bonacina, S. Ranise, and S. Schulz. New results on rewrite-based satisfiability procedures. ACM Transactions on Computational Logic, 10(1):1--51, 2009. [ DOI | .pdf ]
[58] A. Armando, R. Carbone, and L. Compagna. Ltl model checking for security protocols. Journal of Applied Non-Classical Logics, 19(4):403--429, 2009. [ DOI | arXiv | .pdf ]
[57] A. Armando, P. Baumgartner, and G. Dowek. Preface. In 4th International Joint Conference on Automated Reasoning (IJCAR), volume 5195 LNAI, 2008. [ DOI ]
[56] A. Armando, R. Carbone, L. Compagna, J. Cuéllar, 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 FMSE '08: Proceedings of the 6th ACM workshop on Formal methods in security engineering, pages 1--10, New York, NY, USA, 2008. ACM. [ DOI | .pdf ]
[55] A. Armando and L. Compagna. Sat-based model-checking for security protocols analysis. International Journal of Information Security, 7(1):3--32, 2008. [ DOI | .pdf ]
[54] A. Armando, M. Benerecetti, D. Carotenuto, J. Mantovani, and P. Spica. The eureka tool for software model checking. In ASE '07: Proceedings of the twenty-second IEEE/ACM international conference on Automated software engineering, pages 541--542, New York, NY, USA, 2007. ACM. [ DOI | .pdf ]
[53] A. Armando, R. Carbone, and L. Compagna. Ltl model checking for security protocols. In CSF '07: Proceedings of the 20th IEEE Computer Security Foundations Symposium, pages 385--396, Washington, DC, USA, 2007. IEEE Computer Society. [ DOI | .pdf ]
[52] A. Armando, M. Benerecetti, and J. Mantovani. Abstraction refinement of linear programs with arrays. In TACAS'07: Proceedings of the 13th international conference on Tools and algorithms for the construction and analysis of systems, pages 373--388, Berlin, Heidelberg, 2007. Springer-Verlag. [ DOI | .pdf ]
[51] A. Armando and C. Ringeissen. Preface: special issue: combining logical systems. Information and Computation, 204(10):1411--1412, 2006. [ DOI ]
[50] A. Armando, J. Mantovani, and L. Platania. Bounded model checking of software using smt solvers instead of sat solvers. In SPIN'06: Proceedings of the 13th international conference on Model Checking Software, pages 146--162, Berlin, Heidelberg, 2006. Springer-Verlag. [ DOI | .pdf ]
[49] A. Armando, M. Benerecetti, and J. Mantovani. Model checking linear programs with arrays. Electronic Notes in Theoretical Computer Science, 144(3):79--94, 2006. [ DOI | .pdf ]
[48] A. Armando, D. Basin, J. Cuéllar, M. Rusinowitch, and L. Viganò. Preface: Special issue on automated reasoning for security protocol analysis. Journal of Automated Reasoning, 36(1-2):1--3, 2006. [ DOI ]
[47] A. Armando and A. Cimatti. Preface. Electronic Notes in Theoretical Computer Science, 144(2):1--2, 2006. [ DOI ]
[46] A. Armando, C. Castellini, E. Giunchiglia, and M. Maratea. The sat-based approach to separation logic. Journal of Automated Reasoning, 35(1-3):237--263, 2005. [ DOI | .pdf ]
[45] 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 FroCoS'05: Proceedings of the 5th international conference on Frontiers of Combining Systems, pages 65--80, Berlin, Heidelberg, 2005. Springer-Verlag. [ DOI | .pdf ]
[44] A. Armando, D. Basin, Y. Boichut, Y. Chevalier, L. Compagna, J. Cuéllar, P. H. Drielsma, P. C. Heám, O. Kouchnarenko, J. Mantovani, S. Mödersheim, D. von Oheimb, M. Rusinowitch, J. Santiago, M. Turuani, L. Viganò, and L. Vigneron. The avispa tool for the automated validation of internet security protocols and applications. In CAV'05: Proceedings of the 17th international conference on Computer Aided Verification, pages 281--285, Berlin, Heidelberg, 2005. Springer-Verlag. [ DOI | .pdf ]
[43] A. Armando, C. Castellini, E. Giunchiglia, M. Idini, and M. Maratea. Tsat++: an open platform for satisfiability modulo theories. Electronic Notes in Theoretical Computer Science, 125(3):25--36, 2005. [ DOI | .pdf ]
[42] A. Armando and C. Ballarin. A reconstruction and extension of maple's assume facility via constraint contextual rewriting. Journal of Symbolic Computation, 39(5):503--521, 2005. [ DOI | .pdf ]
[41] A. Armando and L. Compagna. An optimized intruder model for sat-based model-checking of security protocols. Electronic Notes in Theoretical Computer Science, 125(1):91--108, 2005. [ DOI | .pdf ]
[40] A. Armando and L. Viganò. Preface. Electronic Notes in Theoretical Computer Science, 125(1):1, 2005. [ DOI ]
[39] A. Armando, C. Castellini, E. Giunchiglia, and M. Maratea. A sat-based decision procedure for the boolean combination of difference constraints. In SAT'04: Proceedings of the 7th international conference on Theory and Applications of Satisfiability Testing, pages 16--29, Berlin, Heidelberg, 2005. Springer-Verlag. [ DOI | .pdf ]
[38] A. Armando, L. Compagna, and S. Ranise. Rewrite and decision procedure laboratory: Combining rewriting, satisfiability checking, and lemma speculation. In D. Hutter and W. Stephan, editors, Mechanizing Mathematical Reasoning, volume 2605 of Lecture Notes in Computer Science, pages 30--45. Springer Berlin Heidelberg, 2005. [ DOI | .pdf ]
[37] A. Armando, C. Castellini, E. Giunchiglia, F. Giunchiglia, and A. Tacchella. Sat-based decision procedures for automated reasoning: A unifying perspective. In D. Hutter and W. Stephan, editors, Mechanizing Mathematical Reasoning, volume 2605 of Lecture Notes in Computer Science, pages 46--58. Springer Berlin Heidelberg, 2005. [ DOI | .pdf ]
[36] A. Armando, L. Compagna, and Y. Lierler. Automatic compilation of protocol insecurity problems into logic programming. In J. Alferes and J. Leite, editors, Logics in Artificial Intelligence (JELIA), volume 3229 of Lecture Notes in Computer Science, pages 617--627. Springer Berlin Heidelberg, 2004. [ DOI | .pdf ]
[35] A. Armando and L. Compagna. Abstraction-driven sat-based analysis of security protocols. In E. Giunchiglia and A. Tacchella, editors, SAT'03: Theory and Applications of Satisfiability Testing, volume 2919 of Lecture Notes in Computer Science, pages 257--271. Springer Berlin Heidelberg, 2004. [ DOI | http ]
[34] A. Armando, C. Castellini, and J. Mantovani. Software model checking using linear constraints. In J. Davies, W. Schulte, and M. Barnett, editors, Formal Methods and Software Engineering (FMSE), volume 3308 of Lecture Notes in Computer Science, pages 209--223. Springer Berlin Heidelberg, 2004. [ DOI | .pdf ]
[33] A. Armando and L. Compagna. Satmc: A sat-based model checker for security protocols. In J. Alferes and J. Leite, editors, Logics in Artificial Intelligence, volume 3229 of Lecture Notes in Computer Science, pages 730--733. Springer Berlin Heidelberg, 2004. [ DOI | .pdf ]
[32] A. Armando and S. Ranise. Constraint contextual rewriting. Journal of Symbolic Computation, 36(1-2):193--216, 2003. [ DOI | .pdf ]
[31] A. Armando, S. Ranise, and M. Rusinowitch. A rewriting approach to satisfiability procedures. Information and Computation, 183(2):140--164, 2003. [ DOI | .pdf ]
[30] A. Armando, L. Compagna, and P. Ganty. Sat-based model-checking of security protocols using planning graph analysis. In K. Araki, S. Gnesi, and D. Mandrioli, editors, FME 2003: Formal Methods Europe, volume 2805 of Lecture Notes in Computer Science, pages 875--893. Springer Berlin Heidelberg, 2003. [ DOI | http ]
[29] A. Armando, M. P. Bonacina, A. K. Sehgal, and S. Ranise. High-performance deduction for verification: A case study in the theory of arrays. In Notes of the Workshop on Verification, Third Federated Logic Conference (FLoC02, pages 103--112, 2002. [ .pdf ]
[28] A. Armando and L. Compagna. Automatic sat-compilation of protocol insecurity problems via reduction to planning. In FORTE '02: Proceedings of the 22nd IFIP WG 6.1 International Conference Houston on Formal Techniques for Networked and Distributed Systems, pages 210--225, London, UK, UK, 2002. Springer-Verlag. [ DOI | .pdf ]
[27] A. Armando, M. Rusinowitch, and S. Stratulat. Incorporating decision procedures in implicit induction. Journal of Symbolic Computation, 34(4):241--258, 2002. [ DOI | .pdf ]
[26] A. Armando, D. Basin, M. Bouallagui, Y. Chevalier, L. Compagna, S. Mödersheim, M. Rusinowitch, M. Turuani, L. Viganò, and L. Vigneron. The aviss security protocol analysis tool. In CAV '02: Proceedings of the 14th International Conference on Computer Aided Verification, pages 349--353, London, UK, UK, 2002. Springer-Verlag. [ DOI | .pdf ]
[25] A. Armando and S. Ranise. A practical extension mechanism for decision procedures: The case study of universal presburger arithmetic. Journal of Universal Computer Science, 7(2):124--140, 2001. [ DOI | http ]
[24] A. Armando, F. Peccia, and S. Ranise. The phase transition of the linear inequalities problem. In CP'01: Proceedings of the 7th International Conference on Principles and Practice of Constraint Programming, pages 422--432, London, UK, UK, 2001. Springer-Verlag. [ DOI | .pdf ]
[23] A. Armando, A. Coglio, F. Giunchiglia, and S. Ranise. The control layer in open mechanized reasoning systems: annotations and tactics. Journal of Symbolic Computation, 32(4):305--332, 2001. [ DOI ]
[22] A. Armando, S. Ranise, and M. Rusinowitch. Uniform derivation of decision procedures by superposition. In CSL '01: Proceedings of the 15th International Workshop on Computer Science Logic, pages 513--527, London, UK, UK, 2001. Springer-Verlag.
[21] A. Armando and C. Ballarin. Maple's evaluation process as constraint contextual rewriting. In ISSAC '01: Proceedings of the 2001 international symposium on Symbolic and algebraic computation, pages 32--37, New York, NY, USA, 2001. ACM. [ DOI | .pdf ]
[20] A. Armando and T. Jebelean. Foreword of the guest editors: Special issue on calculemus-99: Integrating computation and deduction. Journal of Symbolic Computation, 32(4):303--304, 2001. [ http ]
[19] A. Armando, L. Compagna, and S. Ranise. System description: Rdl : Rewrite and decision procedure laboratory. In IJCAR '01: Proceedings of the First International Joint Conference on Automated Reasoning, pages 663--669, London, UK, UK, 2001. Springer-Verlag.
[18] A. Armando, M. Kohlase, and S. Ranise. Communication protocols for mathematical services. In M. Kerber and M. Kohlhase, editors, Symbolic Computation and Automated Reasoning, pages 33--48. A. K. Peters, Ltd., Natick, MA, USA, 2001. [ .pdf ]
[17] A. Armando and D. Zini. Interfacing computer algebra and deduction systems. In M. Kerber and M. Kohlhase, editors, Symbolic Computation and Automated Reasoning, pages 49--64. A. K. Peters, Ltd., Natick, MA, USA, 2001. [ .pdf ]
[16] A. Armando, S. Ranise, and D. Zini. Integration of automated reasoners (poster session): a progress report. In M. Kerber and M. Kohlhase, editors, Symbolic Computation and Automated Reasoning, pages 237--238. A. K. Peters, Ltd., Natick, MA, USA, 2001.
[15] A. Armando and S. Ranise. Termination of constraint contextual rewriting. In FroCoS '00: Proceedings of the Third International Workshop on Frontiers of Combining Systems, pages 47--61, London, UK, 2000. Springer-Verlag. [ DOI | .pdf ]
[14] A. Armando, C. Castellini, and E. Giunchiglia. Sat-based procedures for temporal reasoning. In ECP '99: Proceedings of the 5th European Conference on Planning, pages 97--108, London, UK, UK, 2000. Springer-Verlag. [ DOI | .pdf ]
[13] A. Armando, A. Coglio, and F. Giunchiglia. The control component of open mechanized reasoning systems. Electronic Notes in Theoretical Computer Science, 23(3):322 -- 339, 1999. <ce:title>CALCULEMUS 99, Systems for Integrated Computation and Deduction (associated to FLoC'99, the 1999 Federated Logic Conference)</ce:title>. [ DOI | http ]
[12] A. Armando and T. Jebelean. Preface: Special issue on calculemus 99, systems for integrated computation and deduction. Electronic Notes in Theoretical Computer Science, 23(3):319 -- 320, 1999. <ce:title>CALCULEMUS 99, Systems for Integrated Computation and Deduction (associated to FLoC'99, the 1999 Federated Logic Conference)</ce:title>. [ DOI | http ]
[11] A. Armando, A. Smaill, and I. Green. Automatic synthesis of recursive programs: The proof-planning paradigm. Automated Software Engineering, 6(4):329--356, 1999. [ DOI | .pdf ]
[10] A. Armando and S. Ranise. Constraint contextual rewriting. In FTP'98: Proceedings of the International Workshop on First order Theorem Proving, Technical Report E1852-GS-981, pages 65--75. Technische Universität Wien, Austria, 1998. Electronically available from http://www.logic.at/ftp98. [ .pdf ]
[9] A. Armando and S. Ranise. From integrated reasoning specialists to “plug-and-play” reasoning components. In AISC '98: Proceedings of the International Conference on Artificial Intelligence and Symbolic Computation, pages 42--54, London, UK, 1998. Springer-Verlag. [ DOI | .pdf ]
[8] A. Armando, J. Gallagher, A. Smaill, and A. Bundy. Automating the synthesis of decision procedures in a constructive metatheory. Annals of Mathematics and Artificial Intelligence, 22(3-4):259--279, 1998. [ DOI | .pdf ]
[7] A. Armando, A. Smaill, and I. Green. Automatic synthesis of recursive programs: the proof-planning paradigm. In ASE '97: Proceedings of the 12th international conference on Automated software engineering (formerly: KBSE), page 2, Washington, DC, USA, 1997. IEEE Computer Society. [ DOI | .pdf ]
[6] F. Giunchiglia, P. Pecchiari, and A. Armando. Towards provably correct system synthesis and extension. Future Generation of Computer Systems, 12(2-3):123--137, 1996. [ DOI ]
[5] E. Giunchiglia, A. Armando, P. Traverso, and A. Cimatti. Visual representation of natural language scene descriptions. Transactions on Systems, Man, and Cyberetics, 26(4):575--589, 1996. [ DOI ]
[4] A. Armando, A. Cimatti, E. Giunchiglia, P. Pecchiari, L. Spalazzi, and P. Traverso. Flexible planning by integrating multilevel reasoning. Engineering Applications of Artificial Intelligence, 8(4):401 -- 412, 1995. [ DOI | http ]
[3] P. Traverso, A. Cimatti, L. Spalazzi, A. Armando, and E. Giunchiglia. Mrg: Building planners for real-world complex applications. Applied Artificial Intelligence, 8(3):333--357, 1994. [ DOI ]
[2] A. Armando, A. Cimatti, and L. Viganò. Building and executing proof strategies in a formal metatheory. In AI*IA '93: Proceedings of the Third Congress of the Italian Association for Artificial Intelligence on Advances in Artificial Intelligence, pages 11--22, London, UK, UK, 1993. Springer-Verlag.
[1] M. D. Manzo, E. Giunchiglia, A. Armando, and P. Pecchiari. Proving formulas through reduction to decidable classes. In AI*IA '93: Proceedings of the Third Congress of the Italian Association for Artificial Intelligence on Advances in Artificial Intelligence, pages 1--10, London, UK, UK, 1993. Springer-Verlag.

This file was generated by bibtex2html 1.98.