Publications




  • A theorem prover for a logical calculus of molecolar biology
    F. Sestini and S. Crafa.
    In TLLA2017 - International workshop on Trends in Linear Logic and Applications, September 2017, Oxford UK.
  • Formal methods in action: typestate-oriented actor programming in Scala-Akka
    Silvia Crafa, Slides, Paris May 2017.
  • The Chemical Approach to Typestate-Oriented Programming
    S.Crafa and L. Padovani
    ACM Transactions on Programming Languages and Systems (TOPLAS): 39(3), May 2017.
  • CobaltBlue: a tool for (TypeState-)checking whether concurrent objects are used according to their protocol.
  • On the chemistry of typestate-oriented actors.
    S.Crafa and Luca Padovani
    Technical Report. arXiv:1607.02927. July 2016.[Slides presented at CurryOn 2016]
  • Comprendere lo sviluppo dei moderni linguaggi di programmazione in chiave evolutiva.
    S.Crafa.
    Mondo Digitale. AICA. 2016 (1).
  • The chemical approach to typestate-oriented programming
  • S. Crafa and L. Padovani.
    In OOPSLA 2015 - ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications: pag 917-934. ACM. 2015

  • Modelling the Evolution of Programming Languages.
    S.Crafa.
    Technical Report. arXiv:1510.04440. 2015. [Abstract]
    Note: This is an interdisciplinary work that studies the application of the Darwinian explanation to the programming languages evolution.
  • The role of concurrency in an evolutionary view of programming abstractions.
  • S. Crafa
    Journal of Logical and Algebraic Methods in Programming 84:732-741 (2015).

  • Actors vs Shared Memory: two models at work on Big Data application frameworks.
  • S. Crafa and L. Tronchin
    Technical Report. arXiv:1505.03060 May 2015

  • Fine-grained detection of privilege escalation attacks on browser extensions.
  • S. Calzavara, M. Bugliesi, S. Crafa, E. Steffinlongo.
    In ESOP'15 -- European Symposium on Programming. April 2015. LNCS n.9032, pages 510--534. Springer.

  • Logical characterizations of behavioral relations on transition systems of probability distributions.
  • S. Crafa and F. Ranzato.
    ACM Transactions on Computational Logic 16(1):2, doi:10.1145/2641566, ACM Press, 2014.

  • Computing from LaTeX: automated numerical computing from LaTeX expressions.
  • S. Crafa, F. Marcuzzi and M. Virgulin.
    Technical Report. Padua@research [ID:6930] June 2014

  • A Logic for True Concurrency.
  • P. Baldan and S. Crafa.
    Journal of the ACM (JACM), 61(4):24:1--24:36, July 2014. doi: 10.1145/2629638

  • Hereditary history-preserving bisimilarity: logics and automata.
  • P. Baldan and S. Crafa.
    APLAS'2014 - Programming Languages and Systems - 12th Asian Symposium, Singapore, November 2014, LNCS n.8858, pages:469-488.Springer

  • Semantics of (Resilient) X10.
  • S. Crafa, D. Cunningham, V.Saraswat, A. Shinnar, O. Tardieu.
    ECOOP'2014 - European Conference on Object-Oriented Programming, Uppsala, Sweden, July 2014. LNCS n.8586, pages 670-696. Springer

  • Causality in concurrent systems
  • S. Crafa and F. Russo.
    Technical Report arXiv:1303.1384 [cs.DC] March 2013
    HaPoC: International Conference on the History and Philosophy of Computing. Paris, France, 2013. [Slides .pdf]
    Note: This is an interdisciplinary paper. It addresses a class of causal models developed in computer science from an epistemic perspective, namely in terms of philosophy of causality

  • Behavioural Types for Actor Systems.
  • S. Crafa.
    Technical Report arXiv:1206.1687v1 May 2012

  • Bisimulation and Simulation Algorithms on Probabilistic Transition Systems by Abstract Interpretation.
  • S. Crafa and F. Ranzato.
    Formal Methods in System Design. Volume 40(3):356-376 (2012)

  • Event Structure Semantics of Parallel Extrusion in the Pi-calculus.
  • S. Crafa, D. Varacca and N. Yoshida.
    FoSSaCS'12 - 15th International Conference on Foundations of Software Science and Computation Structures Tallin, Estonia. LNCS n.7213, pag 225-239, Springer, 2012

  • A spectrum of behavioral relations over LTSs on probability distributions.
  • S. Crafa, F. Ranzato.
    CONCUR'11 - 22nd International Conference on Concurrency Theory Aachen, Germany. LNCS vol. 6901, pages 124-139, Springer, 2011

  • Probabilistic Bisimulation and Simulation Algorithms by Abstract Interpretation
  • S. Crafa, F. Ranzato.
    ICALP'11 - 38th International Colloquium on Automata, Languages, and Programming Zurich, Switzerland. LNCS n.6756, pag 295-306, Springer, 2011.

  • Saving space in a time efficient simulation algorithm.
  • S. Crafa, F. Ranzato and F.Tapparo.
    Fundamenta Informaticae, 108(1-2):23-42,2011.

  • A logic for true concurrency
  • P. Baldan, S. Crafa.
    CONCUR'10 - Concurrency Theory. LNCS 6269, pag 147-161, Sept. 2010.[Slides.pptx] [Slides.pdf]

  • A Type System for Discretionary Access Control.
  • M.Bugliesi, D. Colazzo, S. Crafa, and D. Macedonio.
    Mathematical Structures in Computer Science, 19(4): 839-875 (2009)

  • Saving space in a time efficient simulation algorithm
  • S. Crafa, F. Ranzato, and F. Tapparo.
    In Proc. of the 9th Int. Conf. on Application of Concurrency to System Design (ACSD'09), pag 60-69. IEEE Press. Augsburg, Germany, 2009.

  • PicNic - Pi-calculus Non-Interference checker. (Tool paper)
  • S. Crafa, M. Mio, M. Miculan, C. Piazza, and S. Rossi.
    Proc. of the 8th International Conference on Application of Concurrency to System Design (ACSD'08), pag. 33-38, IEEE Press, 2008.

  • Controlling Information Release in the pi-calculus.
  • S. Crafa and S. Rossi.
    Information and Computation 205 (2007):1235-1273.

  • Compositional Event Structure Semantics for the Internal pi-calculus
  • S. Crafa, D. Varacca, N. Yoshida.
    CONCUR'07 - Concurrency Theory. LNCS 4703, pag 317-332, Sept 2007.

  • P-Congruences as Noninterference for the pi-calculus.
  • S. Crafa and S. Rossi.
    Proc. of the 4th ACM Workshop on Formal Methods in Security Engineering, FMSE 2006. ACM Press pag 13-22. [Slides]

  • A Theory of Noninterference for the pi-calculus.
  • S. Crafa and S. Rossi.
    Proc. of the Symposium on Trustworthy Global Computing, TGC 2005, LNCS 3705, pag. 2-18, 2005.

  • Communication and Mobility Control in Boxed Ambients.
  • M. Bugliesi, S. Crafa, M. Merro and V. Sassone.
    Information and Computation 202 (2005):39-86.

  • Access Control for Mobile Agents: the Calculus of Boxed Ambients.
  • M. Bugliesi, G. Castagna, S. Crafa.
    ACM Transactions on Programming Languages and Systems 26(1):57-124, Jan. 2004.

  • Type Based Discretionary Access Control
  • M. Bugliesi, D. Colazzo, S. Crafa.
    CONCUR'04 - Concurrency Theory. LNCS n.3170, pages 225-239, Sept 2004.[Slides]

  • Secrecy in Untrusted Networks
  • M. Bugliesi, S. Crafa, A. Prelic and V. Sassone.
    ICALP'03. LNCS n.2719, pages 969-983, July 2003.

  • Communication Interference in Mobile Boxed Ambients
  • M.Bugliesi, S. Crafa, M. Merro and V. Sassone.
    In FSTTCS 2002. LNCS n.2556, pages 71-84, Dec. 2002

  • Information Flow Security in Boxed Ambients.
  • S. Crafa, M.Bugliesi and G. Castagna.
    In FWAN: Int. Workshop on Found. of WAN Computing, ENTCS, 66 (3). Elsevier, 2002.

  • Typed Interpretations of Extensible Objects.
  • V. Bono, M. Bugliesi and S. Crafa.
    ACM Transactions on Computational Logic 3(4) 562-603, August 2002.

  • Boxed Ambients.
  • M.Bugliesi, G. Castagna and S. Crafa.
    In TACS 2001, LNCS n. 2215, pages 38-63, Springer 2001.

  • Reasoning about security in Mobile Ambients.
  • M.Bugliesi, G. Castagna and S. Crafa.
    In CONCUR 2001, LNCS n. 2154, pages 102-120, Springer 2001.

  • Matching and Subtyping for Mobile Objects.
  • M.Bugliesi, G. Castagna and S. Crafa.
    In ICTCS '01, LNCS n. 2202, pages 235--255

  • Typed Mobile Objects.
  • Michele Bugliesi, Giuseppe Castagna and  Silvia Crafa.
    In C.Palamidessi ed. Proc. CONCUR2000, volume 1877 of LNCS, pages 504-520 Springer,2000.

  • Object Calculi with Dynamic Messages.
  • M. Bugliesi and Silvia Crafa.
    FOOL'6 Proc. of the 6th Int. Workshop on Foundations of OO Languages. Electronic Proceedings.



    Ph D Thesis

    Models and Types for Wide Area Computing: The calculus of Boxed Ambients
    Dottorato di Ricerca in Informatica del consorzio delle Universita' di Bologna, Padova, Venezia.
    Winner of the award for the two best italian PhD theses in theoretical computer science in the year 2003,
    assigned by the Italian Chapter of the European Association for Theoretical Computer Science.