Publications

On the Reactive Nature of Financial Networks
S. Crafa and D. Varacca.
Proc. of ICTCS 2018, September 2018, and subject to patent application.

Proof search in a contextsensitive logic for molecular biology
F. Sestini and S. Crafa.
Journal of Logic and Computation, 28(7):15651600. Oxford University Press, 2018.

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: typestateoriented actor programming in ScalaAkka
Silvia Crafa, Slides, Paris May 2017.

The Chemical Approach to TypestateOriented 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 typestateoriented 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 typestateoriented programming
 S. Crafa and L. Padovani.

In OOPSLA 2015  ACM SIGPLAN International Conference on ObjectOriented Programming, Systems, Languages, and Applications: pag 917934. 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:732741 (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

Finegrained 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 510534. 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:124:36, July
2014. doi: 10.1145/2629638
 Hereditary historypreserving 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:469488.Springer
 Semantics of (Resilient) X10.
 S. Crafa, D. Cunningham, V.Saraswat, A. Shinnar, O. Tardieu.
 ECOOP'2014  European Conference on ObjectOriented
Programming, Uppsala, Sweden, July 2014. LNCS n.8586,
pages 670696. 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):356376 (2012)

Event Structure Semantics of Parallel Extrusion in the Picalculus.
 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 225239, 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 124139, 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 295306, Springer, 2011.
 Saving space in a time efficient simulation algorithm.
 S. Crafa, F. Ranzato and F.Tapparo.
 Fundamenta Informaticae, 108(12):2342,2011.
 A logic for true concurrency
 P. Baldan, S. Crafa.
 CONCUR'10  Concurrency Theory. LNCS 6269, pag 147161, 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): 839875 (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 6069. IEEE Press. Augsburg, Germany, 2009.

 PicNic  Picalculus NonInterference 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. 3338,
IEEE Press, 2008.

 Controlling Information Release in the picalculus.
 S. Crafa and S. Rossi.
 Information and Computation 205 (2007):12351273.
 Compositional Event Structure Semantics for the Internal picalculus
 S. Crafa, D. Varacca, N. Yoshida.
 CONCUR'07  Concurrency Theory. LNCS 4703, pag 317332,
Sept 2007.
 PCongruences as Noninterference for the
picalculus.
 S. Crafa and S. Rossi.
 Proc. of the 4th ACM Workshop on
Formal Methods in Security Engineering, FMSE 2006. ACM Press pag 1322. [Slides]
 A Theory
of Noninterference for the
picalculus.
 S. Crafa and S. Rossi.
 Proc. of the Symposium on Trustworthy Global
Computing, TGC 2005, LNCS 3705, pag. 218, 2005.
 Communication and
Mobility Control in Boxed Ambients.
 M. Bugliesi, S. Crafa, M. Merro and V. Sassone.
 Information and Computation 202 (2005):3986.
 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):57124, Jan. 2004.
 Type
Based Discretionary Access Control
 M. Bugliesi, D. Colazzo, S. Crafa.
 CONCUR'04  Concurrency Theory. LNCS n.3170, pages 225239,
Sept 2004.[Slides]
 Secrecy in
Untrusted Networks
 M. Bugliesi, S. Crafa, A. Prelic and V. Sassone.
 ICALP'03. LNCS n.2719, pages 969983, July 2003.

Communication Interference
in Mobile Boxed Ambients
 M.Bugliesi, S. Crafa, M. Merro and V. Sassone.
 In FSTTCS 2002. LNCS n.2556, pages 7184, 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) 562603, August
2002.
 Boxed
Ambients.
 M.Bugliesi, G. Castagna and S. Crafa.
 In TACS 2001, LNCS n. 2215, pages 3863, Springer 2001.
 Reasoning
about security in
Mobile Ambients.
 M.Bugliesi, G. Castagna and S. Crafa.
 In CONCUR 2001, LNCS n. 2154, pages 102120, Springer 2001.
 Matching
and Subtyping for Mobile
Objects.
 M.Bugliesi, G. Castagna and S. Crafa.
 In ICTCS '01, LNCS n. 2202, pages 235255
 Typed Mobile Objects.
 Michele Bugliesi, Giuseppe Castagna and Silvia Crafa.
 In C.Palamidessi ed. Proc. CONCUR2000, volume 1877 of LNCS,
pages 504520 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.