Research Papers Service Awards Teaching		Researcher Phone: +39.0461.314.192 Fax: +39.0461.302.040 E-mail: ranise@fbk.eu
News Consider to submit your papers to one of the following events: WooPS'12, SecureComm'12, STM'12, AREIS'12, SoICT'12, SBP'12 Tutorial on Model Checking Modulo Theories [Updated with material used during presentation] Tool: ASASP (Automated Symbolic Analysis of Security Policies)

Research

• Automated analysis of security properties (ASASP, Avantssar, SIAM)
• Model checking infinite state systems (MCMT)
• SMT-based verification
• SMT solvers and decision procedures (SMT-Lib, haRVey)
• Automated theorem proving

[Top page]

Papers

(DBLP, outdated list)

Some recent papers

• A. Armando and S. Ranise. Automated and Efficient Analysis of Role-Based Access Control with Attributes (extended version), Proc. of DBSEC'12. LNCS vol. 7371, Springer, 2012. [The program to generate and solve the synthetic benchmarks in the paper can be found here.]
  
• R. Bruttomesso, S. Ghilardi, S. Ranise. Quantifier-free Interpolation of a Theory of Arrays. In Logical Methods in Computer Science (LMCS), Vol. 8, 2012.
• R. Bruttomesso, S. Ghilardi, S. Ranise. From Strong Amalgamation to Modularity of Quantifier-Free Interpolation (extended version), Proc. of IJCAR 2012, To appear in LNAI, Springer.
• F. Alberti, R. Bruttomesso, S, Ghilardi, S. Ranise, N. Sharygina. SAFARI: SMT-based Abstraction For Arrays
  with Interpolants, Proceedings of CAV 2012. To appear in LNCS, Springer, 2012.
  
• R. Bruttomesso, A. Carioni, S. Ghilardi, S. Ranise. Automated Analysis of Parametric Timing Based Mutual Exclusion Protocols, Proceedings of the Fourth NASA Formal Methods Symposium, LNCS vol. 7226, Springer, 2012.
• F. Alberti, S. Ghilardi, E. Pagani, S. Ranise, and G. P. Rossi. Universal Guards, Relativization of Quantifiers, and Failure Models in Model Checking Modulo Theories. In Journal of Satisfiability, Boolean Modeling, and Computation. Vol 8 (2012), pages 29-61.
  
• F. Alberti, R. Bruttomesso, S. Ghilardi, S. Ranise, and N. Sharyagina. Lazy Abstraction with Interpolants for Arrays (extended version with proofs). In Int. Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR18), March 10-15, Venzuela.  Also in LNCS vol. 7180, Springer, 2012.
• A. Armando, S. Ranise, F. Turkmen, and B. Crispo. Efficient run-time solving of RBAC user authorization queries: pushing the envelope. Second ACM Conf. on Data And Application Security, CODASPY'12, San Antonio, TX, USA.. ACM Press.
• S. Ranise. On the Verification of Security-Aware E-services.  In Press, Journal of Symbolic Computation, Special Issue dedicated to the FTP'09 workshop, 2011.
  
• A. Armando, R. Carbone, and S. Ranise. Automated Analysis of Semantic-Aware Access Control Policies: a Logic-based Approach.  Proc. of IEEE Int. Workshop on Semantics, Security, and Privacy (TCSEM + TCSP) affiliated with 5th IEEE Int. Conference on Semantic Computing, Sept. 18-21, 2011 (Stanford Univ., Palo Alto, CA, USA).
• R. Bruttomesso, S. Ghilardi, and S. Ranise. A Combination of Rewriting and Constraint Solving for the Quantifier-free Interpolation of Arrays with Integer Difference Constraints.  Proc. of the 8th Int. Symp. on Frontiers of Combining Systems (FroCoS'11).  Also to appear in Springer LNAI, 2011. (Extended version)
• A. Carioni, S. Ghilardi, and S. Ranise. Automated Termination in Model Checking Modulo Theories. Proc. of the 5th Int. Workshop on Reachability Problems (RP 11).  Also to appear in Springer LNCS, 2011. (Extended version)
  
• A. Armando and S. Ranise. Automated Analysis of Infinite State Workflows with Access Control Policies.  Proc. of the 7th Int. Workshop on Security and Trust Management (co-located with 5th IFIP WG 11.11 Int. Conference on Trust Management), June 27-28, Copnhagen, Denmark, 2011.  To be presented also at the 9th International Workshop on Security Issues in Concurrency (SecCo), 2011. Also to appear in Springer LNCS, 2011. (Extended version)
  
• M. Barletta, A. Calvi, S. Ranise, L. Vigano, and L. Zanetti. Workflow and Access Control Reloaded: a Declarative Specification Framework for the Automated Analysis of Web Services. In Scalable Computing: Practice and Experience, vol. 12, no. 1. Special issue with selected papers from 1st workshop on Software services.
• F. Alberti, A. Armando, and S. Ranise. ASASP: Automated Symbolic Analysis of Security Policies. Proc. of the 23rd Conference on Automated Deduction (CADE), 2011.  In LNCS vol 6803, pages 26-34, Springer, 2011.
  
• C. Lynch, S. Ranise, C. Ringeissen, and D.-K. Tran. Automatic Decidability and Combinability. Information and Computation 209:7 (July, 2011) 1026-1047
  
• R. Bruttomesso, S. Ghilardi, S. Ranise. Rewriting-based Quantifier-free Interpolation for a Theory of Arrays, Proc. of the 22nd Int. Conf. on Rewriting Techniques and Applications (RTA '11), Leibniz Int. Proc. in Informatics, Dagstuhl Publishing, 2011 (Extended version with proofs and technical details).
  
• M. Barletta, S. Ranise, and L. Vigano. A Declarative Two-level Framework to Specify and Verify Workflow and Authorization Policies in Service Oriented Architetures. In Journal of Service Oriented Computing and Applications, vol. 5, nr. 1, 2011.
  
• F. Alberti, A. Armando, and S. Ranise. Efficient Symbolic Automated Analysis of Administrative Role Based Access Control Policies. In Proc. of the 6th ACM Symposium on Information, Computer, and Communications Security (ASIACCS), Hong Kong, March 22-24, 2011. To appear in ACM SIG, 2011 [Tool and benchmarks used in the paper].
• S. Ghilardi and S. Ranise. Backward Reachability of Array-based Systems by SMT solving: Termination and Invariant Synthesis. In Logical Methods in Computer Science (LMCS), Vol. 6, Issue 4, 2010.
• A. Armando and S. Ranise. Automated Symbolic Analysis of ARBAC Policies. In Proc. of 6th Int. Workshop on Security and Trust Management (co-located with EUROPKI'10, CRITIS'10, and ESORICS'10), Athens, Sept. 23-24 (2010). In LNCS volume 6710, pages 17-33, Springer, 2011. (Extended version).
  
• M. Barletta, A. Calvi, S. Ranise, L. Vigano, and L. Zanetti. WSSMT: Towards the Automated Analysis of Security-Sensitive Services and Applications. In Proc. of 1st Workshop on Software Service (satellite of SYNASC symposium), Timisoara, Sept. 23-25 (2010). In IEEE Comp. Society, 2010.
  
• A. Calvi, S. Ranise, L. Vigano. Automated Validation of Security-sensitive Web Services specified in BPEL and RBAC. In Proc. of 1st Workshop on Software Service (satellite of SYNASC symposium), Timisoara, Sept. 23-25 (2010). In IEEE Comp. Society, 2010.
  
• A. Carioni, S. Ghilardi, S. Ranise. MCMT in the Land of Parameterized Timed Automata, In Proc. of VERIFY Workshop, co-located with IJCAR, Edinburgh (2010)
  
• S. Ghilardi and S. Ranise. MCMT: a Model Checker Modulo Theories (system description), Proc. of the 5th International Joint Conference on Automated Reasoning (IJCAR 2010), Springer LNAI, vol. 6173, pp. 22-29.
• M. Barletta, S. Ranise, and L. Vigano. Verifying the Interplay of Authorization Policies and Workflow in Service-Oriented Architectures. In Proc. IEEE CSE'09, 12th IEEE Intern. Conf. on Computational Science and Engineering, Aug. 29-31, 2009, Vancouver, BC, Canada. IEEE Comp. Society, 2009.

[Top page]

Service

• SoICT'11
• FroCoS 2011
• Wf SAC
• FTP'11
• CICM 2011 (Calculemus Track)
• AVoCS 2010

[Top page]

Awards

• HVC'10 award

[Top page]

Teaching

Fundamentals of Software Engineering [Master in Game Programming] 2011/2012

• Lecture 11.11.11: Introduction and Overview
• Lecture 18.11.11: Software Development Processes and Analysis of Requirements
• Lecture 02.12.11: Requirements Engineering and System Models I
• Lecture 09.12.11: System Models II and System Models III (Pointer to paper describing the RBAC model)
• Lecture 15.12.11: Access Control

[Top page]