Sabina Rossi   Assistant Professor   Dipartimento di Informatica   Università Ca' Foscari di Venezia

Contents   (last update: November 2009)

• Address
• Research Interests
• Projects
• Recent Events
• Software
• Papers available on line
• Teaching
• Personal

Address

Dipartimento di Informatica Università Ca' Foscari di Venezia Via Torino 155, 30172 Mestre-Venezia, Italy    Phone: +39-041-23.48.422 Fax: +39-041-23.48.419    Email: srossi@dsi.unive.it

Research Interests

• Semantics of programming languages: static analysis, abstract interpretation, verification, specialisation, transformation
• Logic programming, Prolog
• Formal methods for security
• Process algebra and cryptographic protocols
• Algorithms and verification tools

Projects

• PRIN (2006-2007): Fondamenti Logici dei Sistemi Distribuiti e Codice Mobile
• FIRB (2003-2007): Abstract interpretation and model checking for the verification of embedded systems
• FET-Global Computing (2002-2004): MyThS Models and Types for Security in Mobile Distributed Systems

Recent Events

• TCS 2010 (PC member) 6th IFIP International Conference on Theoretical Computer Science (TCS 2010), September 20-23, 2010, Brisbane (Australia).
• CILC 2010 (PC member) 25-esimo Convegno Italiano di Logica Computazionale, July 7-9, 2010, Rende, Università della Calabria (Italy).
• UMSA 2009 (PC member) International Workshop on Ubiquitous Multimedia Systems and Applications, October 12-14, 2009, St. Petersburg (Russia).
• LOPSTR 2009 (PC member) International Symposium on Logic-based Program Synthesis and Transformation, September 7-11, 2009, Coimbra (Portugal).
• CILC 2009 (PC member) 24-esimo Convegno Italiano di Logica Computazionale, June 25-26, 2009, Ferrara (Italy).
• WLPE 2008 (PC member) 18th Workshop on Logic-based methods in Programming Environments, December 9-13, 2008, Udine (Italy).
• LOPSTR 2008 (PC member) International Symposium on Logic-based Program Synthesis and Transformation, July 17-18, 2008, Valencia (Spain).
• INFORMATICS 2008 (PC member) IADIS International Conference Informatics 2008, July 25-27, 2008, Amsterdam (Netherlands).
• CILC 2008 (PC member) 23-esimo Convegno Italiano di Logica Computazionale, July 10-12, 2008, Perugia (Italy).
• LOPSTR 2006 (PC member and Local Arrangments Chair) International Symposium on Logic-based Program Synthesis and Transformation, July 12-14, 2006, San Servolo, Venice (Italy).
• VERIFY 2006 (PC member) 3rd International Verification Workshop, August 15-16, 2006, Seattle, Washington (USA).
• ICALP 2006 (Workshop co-chair) 33rd International Colloquium on Automata Languages and Programming, July 9-16, 2006, San Servolo, Venice (Italy).

Software

• CoPS - Checker of Persistent Security: a tool for verifying persistent non-interference properties of CCS processes.
• PicNIc- Pi-calculus Non-Interference checker:a tool for verifying non-interference properties of processes in the Pi-calculs.

Papers available on line

Top

Please read the Copyright notice below.

Journals

• S. Crafa and S. Rossi.
  Controlling Information Release in the pi-calculus.
  Information and Computation, volume 285, n. 8, pag. 1235-1273, 2007. Elsevier Science.
  [bibTeX]
• A. Bossi, C. Piazza and S. Rossi.
  Compositional Information Flow Security for Concurrent Programs.
  Journal of Computer Security, volume 15, n. 3, pag. 373-416, 2007. IOS Press.
  [bibTeX]
• R. Focardi and S. Rossi.
  Information Flow Security in Dynamic Contexts.
  Journal of Computer Security, volume 14, n. 1, pag. 65-110, 2006. IOS Press.
  [bibTeX]
• A. Bossi, D. Macedonio, C. Piazza and S. Rossi.
  Information Flow in Secure Contexts.
  Journal of Computer Security, volume 13, n. 3, pag. 391-422, 2005. IOS Press.
  [bibTeX]
• M. Bugliesi, S. Rossi.
  Non-Interference Proof Techniques for the Analysis of Cryptographic Protocols.
  Journal of Computer Security, volume 13, n. 1, pag. 87-113, 2005. IOS Press.
  [bibTeX]
• A. Bossi, R. Focardi, C. Piazza, and S. Rossi.
  Verifying Persistent Security Properties.
  Computer Languages, Systems and Structures, volume 30, n. 3-4, pag. 231-258, 2004. Elsevier Science.
  [bibTeX]
• A. Bossi, S. Etalle, S. Rossi and J.-G. Smaus.
  Termination of Simply Moded Logic Programs with Dynamic Scheduling.
  ACM Transactions on Computational Logic (TOCL), volume 5, n. 3, pag. 470-507, 2004. ACM Press.
  [bibTeX]
• A. Bossi, N. Cocco, S. Etalle, and S. Rossi.
  On Modular Termination Proofs of General Logic Programs.
  Theory and Practice of Logic Programming (TPLP), volume 2, n. 3, pag. 263-291, 2002. Cambridge University Press.
  [bibTeX]
• A. Bossi, S. Etalle, and S. Rossi.
  Properties of Input-Consuming Derivations.
  Theory and Practice of Logic Programming (TPLP), volume 2, n. 2, pag. 125-154, 2002. Cambridge University Press.
  [bibTeX]
• B. Le Charlier, S. Rossi, and P. Van Hentenryck.
  Sequence-based Abstract Interpretation of Prolog.
  Theory and Practice of Logic Programming (TPLP), volume 2, n. 1, pag. 25-84, 2002. Cambridge University Press.
  [bibTeX]
• A. Bossi, S. Etalle, and S. Rossi.
  Semantics of Well-Moded Input-Consuming Logic Programs.
  Computer Languages, volume 26, n.1, pag. 1-25, 2000. Elsevier Science.
  [bibTeX]
• B. Le Charlier, C. Leclere, S. Rossi, and A. Cortesi.
  Automated Verification of Prolog Programs.
  Journal of Logic Programming, volume 39, n.1-3, pag. 3-42, 1999. Elsevier Science.
  [bibTeX]

International Conferences

• M. Bugliesi, D. Macedonio, L. Pino, and S. Rossi.
  Compliance Preorders for Web Services
  Proc. of the 6th International Workshop on Web Services and Formal Methods (WS-FM'09), LNCS ???, pag. ???, Springer-Verlag, 2009.
  [bibTeX]
• S. Rossi, and D. Macedonio.
  Information Flow Security for Service Compositions
  Proc. of the IEEE International Workshop on Ubiquitous Multimedia Systems and Applications (UMSA'09) - International Conference on Ultramodern Telecommunications (ICUMT'09), IEEE Press, 2009.
  [bibTeX]
• G. Bernardi, M. Bugliesi, D. Macedonio, and S. Rossi.
  A Theory of Adaptable Contract-based Service Composition
  Proc. of the 10th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'08), pag. 327-334, IEEE Press, 2008.
  [bibTeX]
• S. Crafa, M. Mio, M. Miculan, C. Piazza, and S. Rossi.
  PicNic - Pi-calculus Non-Interference checker. (Tool paper)
  Proc. of the 8th International Conference on Application of Concurrency to System Design (ACSD'08), pag. 33-38,IEEE Press, 2008.
  [bibTeX]
• M. Bugliesi, D. Macedonio, and S. Rossi.
  Static vs Dynamic Typing for Access Control in Pi-Calculus.
  Proc. of the 12th Annual Asian Computing Science Conference Focusing on Computer and Network Security (ASIAN'07), LNCS 4846, pag. 282-296, Springer-Verlag, 2007.
  [bibTeX]
• A. Bossi, C. Piazza and S. Rossi.
  Action Refinement in Process Algebra and Security Issues.
  Proc. of the 17th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR'07) LNCS 4915, pag. 201-217, Springer-Verlag, 2008.
  [bibTeX]
• S. Crafa and S. Rossi.
  P-Congruences as Non-Interference for the pi-calculus.
  Proc. of the 4th ACM Workshop on Formal Methods in Security Engineering: From Specifications to Code (FMSE'06), pag. 13-22, ACM Press 2006.
  [bibTeX]
• A. Bossi, C. Piazza, and S. Rossi.
  Unwinding Conditions for Security in Imperative Languages.
  Proc. of the International Workshop on Logic Based Program Synthesis and Transformation (LOPSTR '04), LNCS 3573, pag. 85-100, Springer-Verlag, 2005.
  [bibTeX]
• S. Crafa and S. Rossi.
  A Theory of Noninterference for the Pi-calculus.
  Proc. of the Symposium on Trustworthy Global Computing (TGC'05), LNCS 3705, pag. 2-18, Springer-Verlag, 2005.
  [bibTeX]
• R. Focardi, S. Rossi, and A. Sabelfeld.
  Bridging Language-Based and Process Calculi Security.
  Proc. of the International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'05), LNCS 3441, pag. 299-315, Springer-Verlag, 2005.
  [bibTeX]
• A. Bossi, C. Piazza, and S. Rossi.
  Modelling Downgrading in Information Flow Security.
  Proc. of the 17th IEEE Computer Security Foundations Workshop (CSFW'04), pag. 187-201, IEEE Computer Society Press, 2004.
  [bibTeX]
• C. Piazza, E. Pivato and S. Rossi.
  CoPS - Checker of Persistent Security.
  Proc. of the Tenth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'04), LNCS 2988, pag. 144-152, Springer-Verlag, 2004.
  [bibTeX]
• A. Bossi, R. Focardi, C. Piazza, and S. Rossi.
  Refinement Operators and Information Flow Security.
  Proc. of the International Conference on Software Engineering and Formal Methods (SEFM'03), pag. 44-53, IEEE Computer Society Press, 2003.
  [bibTeX]
• A. Bossi, D. Macedonio, C. Piazza, and S. Rossi.
  Information Flow Security and Recursive Systems.
  Proc. of the Italian Conference on Theoretical Computer Science (ICTCS'03), LNCS 2841, pag. 369-382, Springer-Verlag, 2003.
  [bibTeX]
• M. Bugliesi, A. Ceccato, and S. Rossi.
  Context-Sensitive Equivalences for Non-Interference based Protocol Analysis.
  Proc. of the 14th International Symposium on Fundamentals of Computation Theory (FCT'03), LNCS 2751, pag. 364-375, Springer-Verlag, 2003.
  [bibTeX]
• A. Bossi, D. Macedonio, C. Piazza, and S. Rossi.
  Secure Contexts for Confidential Data.
  Proc. of the 16th IEEE Computer Security Foundations Workshop (CSFW'03), pag. 14-28, IEEE Computer Society Press, 2003.
  [bibTeX]
• A. Bossi, R. Focardi, C. Piazza, and S. Rossi.
  Bisimulation and Unwinding for Verifying Possibilistic Security Properties.
  Proc. of the Fourth International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'03), LNCS 2575, pag. 223-237, Springer-Verlag, 2003.
  [bibTeX]
• R. Focardi and S. Rossi.
  Information Flow Security in Dynamic Contexts.
  Proc. of the 15th IEEE Computer Security Foundations Workshop (CSFW'02), pag. 307-319, IEEE Computer Society Press, 2002.
  [bibTeX]
• R. Focardi, C. Piazza, and S. Rossi.
  Proofs Methods for Bisimulation based Information Flow Security.
  Proc. of the Third International Workshop on Verification, Model Checking and Abstract Interpretation (VMCAI'02), LNCS 2294, pag. 16-31, Springer-Verlag, 2002.
  [bibTeX]
• A. Bossi, R. Focardi, C. Piazza, and S. Rossi.
  A Proof System for Information Flow Security.
  Proc. of the International Workshop on Logic Based Program Development and Transformation (LOPSTR'02), LNCS 2664, pag. 199-218, Springer-Verlag, 2002.
  [bibTeX]
• A. Bossi, R. Focardi, C. Piazza, and S. Rossi.
  Transforming Processes to Check and Ensure Information Flow Security.
  Proc. of the 9th International Conference on Algebraic Methodology And Software Technology (AMAST'02), LNCS 2422 , pag. 271-286, Springer-Verlag, 2002.
  [bibTeX]
• A. Cortesi, B. Le Charlier, and S. Rossi.
  Reexecution-based Analysis of Logic Programs with Delay Declarations.
  Proc. of the Andrei Ershov Fourth International Conference on Perspectives of System Informatics(PSI'01), LNCS 2244, pag. 395-405, Springer-Verlag, 2001.
  [bibTeX]
• A. Bossi, N. Cocco, and S. Rossi.
  Termination of Well-Typed Logic Programs.
  Proc. of the Third International Conference on Principles and Practice of Declarative Programming (PPDP'01), pag. 73-81, ACM Press, 2001.
  [bibTeX]
• A. Bossi, S. Etalle, S. Rossi, and J.-G. Smaus.
  Semantics and Termination of Simply-moded Logic Programs with Dynamic Scheduling.
  Proc. of the European Symposium on Programming (ESOP'01), LNCS 2028, pag. 402-416, Springer-Verlag, 2001.
  [bibTeX]
• A. Bossi, S. Etalle, and S. Rossi.
  Semantics of Input-Consuming Programs.
  Proc. of Theory and Extensions of Logic Programming, Stream of CL 2000 First International Conference on Computational Logic, LNCS 1861, pag. 194-208, Springer-Verlag, 2000.
  [bibTeX]
• A. Bossi, S. Rossi.
  Call-Correct Specialisation of Logic Programs.
  Proc. of the Sixth Italian Conference on Theoretical Computer Science (ICTCS'98), pag. 335-346, World Scientific, 1998.
  [bibTeX]
• A. Bossi, S. Rossi.
  Specialising Logic Programs with respect to Call/Post Specifications.
  Proc. of the 8th International Workshop on Logic-based Program Synthesis and Transformation (LOPSTR'98), LNCS 1559, pag. 143-158, Springer-Verlag, 1998.
  [bibTeX]
• B. Le Charlier, C. Leclere, S. Rossi, and A. Cortesi.
  Automated Verification of Behavioural Properties of Prolog Programs.
  Proc. of the Asian Computing Science Conference (ASIAN'97), LNCS 1345, pag. 225-238, Springer-Verlag, 1997.
  [bibTeX]
• B. Le Charlier, S. Rossi, and A. Cortesi.
  Specification-based Automatic Verification of Prolog Programs.
  Proc. of the Sixth International Workshop on Logic Program Synthesis and Transformation (LOPSTR'96), LNCS 1207, pag. 38-57, Springer-Verlag, 1996.
  [bibTeX]
• B. Le Charlier, S. Rossi.
  Extending the FOLON Environment for Automatically Deriving Totally Correct Prolog Procedures from Logic Descriptions.
  Proc. of the Seventh International Workshop on Logic Programming Environments (WLPE'95), 1995.
  
• B. Le Charlier, S. Rossi, and P. Van Hentenryck.
  An Abstract Interpretation Framework which Accurately Handles Prolog Search-Rule and the Cut.
  Proc. of the International Logic Programming Symposium (ILPS'94), pag. 157-171, The MIT Press, 1994.
  [bibTeX]
• G. File', S. Rossi.
  Static Analysis of Prolog with Cut.
  Proc. of the Fourth International Conference on Logic Programming and Automated Reasoning (LPAR'93), LNCS 698, pag. 134-145, Springer-Verlag, 1993.
  [bibTeX]
• A. Cortesi, G. File', and S. Rossi.
  Abstract Interpretation of Prolog Programs with Cut and Built-ins.
  Proc. WSA92, Workshop on Static Analysis, 1992.
  

Electronic Journals

• A. Bossi, R. Focardi, C. Piazza, and S. Rossi.
  Unwinding in Information Flow Security.
  Electronic Notes of Theoretical Computer Science, volume 99, pag. 127-154, 2004.
  [bibTeX]
• A. Cortesi, S. Rossi, and B. Le Charlier.
  Operational Semantics for Reexecution-based Analysis of Logic Programs with Delay Declarations.
  Electronic Notes of Theoretical Computer Science, volume 48, 2001.
  [bibTeX]
• A. Bossi, S. Etalle, and S. Rossi.
  Properties of Input-Consuming Derivations.
  Electronic Notes of Theoretical Computer Science, volume 99, n. 1, 1999.
  [bibTeX]

Papers in Collections

• A. Bossi, N. Cocco, S. Etalle, and S. Rossi.
  Declarative Semantics of Input Consuming Logic Programs.
  Program Development in Computational Logic, LNCS 3049, pag. 90-114, Springer-Verlag, 2004.
  

Copyright notice

The versions given here are not necessarily identical to any of the previously published ones. I believe that the technical contents are the same. The documents distributed by this server have been provided as a means to ensure timely dissemination of scholarly and technical work on a noncommercial basis. Copyright and all rights therein are maintained by the authors or by other copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.

Teaching

A.A. 2009/2010

• Programmazione: Parte 1. Laurea Triennale in Informatica, Facoltà di Scienze MM.FF.NN., Università Ca' Foscari di Venezia. [course site]
• Fondamenti dei Linguaggi di Programmazione. Laurea Magistrale in Informatica, Facoltà di Scienze MM.FF.NN., Università Ca' Foscari di Venezia. [course site]

A.A. 2008/2009

• Programmazione: Parte 1. Laurea Triennale in Informatica, Facoltà di Scienze MM.FF.NN., Università Ca' Foscari di Venezia. [course site]
• Sistemi di Elaborazione delle Informazioni 1. Lauree Triennali in discipline economiche, Facoltà di Economia, Università Ca' Foscari di Venezia. [course site]
• Metodi, linguaggi e strumenti informatici. Master in Informatica per la comunicazione, Università Ca' Foscari di Venezia. [course site]

A.A. 2007/2008 (INSEGNAMENTI DISATTIVATI)

• Esercitazioni di Programmazione. Laurea Triennale in Informatica, Facoltà di Scienze MM.FF.NN., Università Ca' Foscari di Venezia. [course site]
• Informatica 1. Lauree Specialistiche in discipline economiche, Facoltà di Economia, Università Ca' Foscari di Venezia. [course site]

Personal

Some pictures...

• My family
• My daughters, Daria and Caterina

srossi@dsi.unive.it