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

Contents   (last update: October 2010)

• 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
• Formal methods for web services and service compositions
• Formal methods for wireless systems such as ad-hoc, mesh, vehicular, and sensor networks

Projects

• PRIN (2008-2010): Interacting Processes in Open-ended Distributed Systems (IPODS)
• PRIN (2005-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

• IFIP Wireless Days 2011 (PC member), October 10-12, 2011, Niagara Falls, Ontario (Canada).
• ICUMT 2011 (PC member), 3rd IEEE International Congress on Ultra Modern Telecommunications and Control Systems (ICUMT 2011), October 5-7, 2011, Budapest (Hungary).
• CILC 2011 (PC member) 26-esimo Convegno Italiano di Logica Computazionale, 31 Agosto - 2 Settembre 2011, Pescara (Italy).
• ICUMT 2010 (PC member), 2nd IEEE International Congress on Ultra Modern Telecommunications and Control Systems (ICUMT 2010), October 18-20, 2010, Moscow (Russia).
• IFIP Wireless Days 2010 (PC member and Local Arrangement Chair), October 20-22, 2010, Venice (Italy).
• 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

• L. Gallina, S. Hamadou, A. Marin and S. Rossi.
  A Framework for Throughput and Energy Efficiency in Mobile ad Hoc Networks (Best Paper Award)
  Proc. of IFIP Wireless Days 2011, IEEE Press, 2011.
  [bibTeX]
• L. Gallina, S. Hamadou, A. Marin and S. Rossi.
  A Probabilistic Energy-Aware Model for Mobile Ad-Hoc Networks
  Proc. of the 18th International Conference on Analytical and Stochastic Modelling Techniques and Applications (ASMTA'11), LNCS 6751, pag. 316-330, Springer-Verlag, 2011.
  [bibTeX]
• L. Gallina and S. Rossi.
  A Calculus for Power-aware Multicast Communications in Ad Hoc Networks (Invited Paper)
  Proc. of the 6th IFIP International Conference on Theoretical Computer Science (TCS'10), pag. 20-31, Springer, 2010.
  [bibTeX]
• L. Gallina and S. Rossi.
  Sender- and Receiver-centered Interference in Wireless Ad Hoc Networks
  Proc. of IFIP Wireless Days 2010, IEEE Press, 2010.
  [bibTeX]
• S. Rossi.
  Model Checking Adaptive Multilevel Service Compositions
  Proc. of the 7th International Workshop on Formal Aspects of Component Software, LNCS 6921, pag. ???, Springer-Verlag, 2010.
  [bibTeX]
• L. Gallina and S. Rossi.
  A Model for Broadcast, Unicast and Multicast Communications of Mobile Ad Hoc Networks
  Proc. of the 2010 International Conference on Modeling, Simulation and Control (ICMSC'10), IEEE Press, 2010.
  [bibTeX]
• 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 6194, pag. 76-91, Springer-Verlag, 2010.
  [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. 2011/2012

• Programmazione: Mod. 1. Laurea Triennale in Informatica, Università Ca' Foscari di Venezia. [course site]
• Foundations of Programming Languages: Mod. 2. Laurea Magistrale in Informatica - Computer Science, Università Ca' Foscari di Venezia. [course site]
• Sistemi di Elaborazione delle Informazioni. Laurea Magistrale in Amministrazione, Finanza e Controllo, Università Ca' Foscari di Venezia. [course site]
• Informatica per la Traduzione Assistita Italiano-Inglese: Mod 1. Laurea Magistrale in Interpretariato e Traduzione Editoriale, Settoriale, Università Ca' Foscari di Venezia.

A.A. 2010/2011

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

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.
• 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]

Personal

Some pictures...

• My family
• My daughters, Daria and Caterina 2007 Daria and Caterina 2010

srossi@dsi.unive.it