General Information

Full Name Marino Miculan
Nationality Italian
Languages Italian, English, Friulian


  • Mar 1997
    PhD in Computer Science
    University of Pisa (Italy)
  • Apr 1994
    Summer School "Advanced School on Logic and Artificial Intelligence"
    CISM, Udine (Italy)
  • Jun 1993
    Summer school "Types for proofs and programs"
    TYPES, Båstad (Sweden)
  • Aug 1992
    Fourth European Summer School in Logic, Language and Information
    University of Essex (UK)
  • Jul 1992
    MSc in Computer Science (Laurea in Scienze dell'Informazione)
    University of Udine (Italy)


  • May 2022 – today
    Associate Professor in Computer Science
    Department of Environmental Sciences, Computer Science and Statistics, Ca' Foscari University of Venice
    • I have a second affiliation with Ca' Foscari University of Venice, in order to participate to the Spoke 6 Software and Platform Security of SERICS. The aim of this spoke's research is to provide an ecosystem where software developers can easily reason about software security, thanks to innovative security-aware programming abstractions and new semantic models.
  • Jan 2005 – today
    Associate Professor in Computer Science
    Department of Mathematical, Computer and Physical Sciences, University of Udine (before: Faculty of Arts and Humanities, then Faculty of Mathematical, Physical and Natural Sciences)
  • Jul 2000 - Jan 2005
    Assistant Professor in Computer Science
    Faculty of Mathematical, Physical and Natural Sciences, University of Udine
    • In this position I have taught about 4 different courses at the undergraduate level (in several Faculties), supervised about 40 undergraduate theses;
    • Written about twenty papers, participated to some research projects, chaired some conferences;
    • Served the Department in many commissions and roles; etc.
  • Jan 1999 – Jun 2000
    Technologist (Tecnologo)
    INFN (National Institute of Nuclear Physics), Trieste
    • I was involved in the creation of the Journal of High Energy Physics (JHEP), the ante litteram open access journal for theoretical physics. It was a quite applicative position focused on design and implementation of a real distribured, fault-tolerant, scalable system. During these years I hadn't carried out much research, but I learnt a lot about real distributed systems: I had to face the dire consequences of the CAP theorem, well before it was proved!
  • Mar 1997 – Dec 1998
    Research Fellow (Assegno di ricerca)
    INFN (National Institute of Nuclear Physics), Trieste
    • As above, but in a fixed-term position.


  • jun 2022
    Group "Impact Area Digital Industry", led by A. Cimatti
    Fondazione Bruno Kessler, Trento
  • sep 2019
    Group "Logic and Semantics", led by T. Uustalu
    Tallinn University of Technology
  • nov 2013
    Group "Logic and Semantics", led by L. Birkedal
    Aarhus University
  • oct 2012
    Group "Programming, Logic, and Semantics", led by T. Hildebrandt
    IT University, Copenhagen
  • oct-nov 1994
    Group "Preuves en théorie des types", led by Y. Bertot
    INRIA, Sophia-Antipolis

Current academic services at the University of Udine

Past academic services

  • Sep 2023
    President of the Selection Committee for the Scientific Class of Scuola Superiore, the excellence school of the University of Udine
  • 2019 – 2022
    Head of the Web Commission of the DMIF
  • 2009 – 2020
    Director of the Udine node of the CINI consortium
  • 2006 – 2017
    Member of the Faculty Board of the PhD Course in Computer Science
  • 2009 – 2020
    Responsible of the Erasmus Exchange with Goteborg University
  • 2013 – 2017
    Member of the Paritetic Commission of the DMIF
  • 2013 – 2016
    Deputy head of the Board of Computer Science Curricula
  • 2005 – 2008
    Deputy head of the Department of Mathematics and Computer Science
  • 2005 – 2023
    Member of many selection committees for PhD entrance, for researcher positions, etc.

Research Interests (according to the ACM CCS classification)

  • Security and privacy
    • Formal methods and theory of security: Formal security models; Logic and verification
    • Intrusion/anomaly detection and malware mitigation
    • Systems security: Distributed systems security; Virtualization and security; Information flow control
    • Network security: Security protocols
  • Software and its engineering
    • Software notations and tools: Distributed programming languages; Concurrent programming structures; Formal language definitions
    • Software architectures: Cooperating communicating processes; Peer-to-peer architectures; Publish-subscribe/event-based architectures; Space-based architectures
    • Software system structures: Distributed systems organizing principles; Abstraction, modeling and modularity
    • Software functional properties: Formal methods
    • Software verification and validation: Formal software verification
  • Theory of computation
    • Models of computation: Concurrency; Process calculi; Distributed computing models; Probabilistic computation
    • Logic: Logic and verification; Proof theory; Modal and temporal logics; Higher order logic; Type theory; Hoare Logic; Abstraction

Invited talks at international conferences and simposia

  • feb 2024
    Talk "An attribute-based events model for collective adaptive systems"
    Theory Days Conference, Randivälja, Estonia
  • jun 2023
    Talk "Modeling Collective Adaptive Systems with Attribute-based Events: Recent Trends and Open Problems"
    IFIP WG 1.8 meeting ``Open Problems in Concurrency'', Bertinoro
  • jun 2014
    Talk "The Fellowship of the Semiring: Concerning Quantitative Bisimulations"
    IFIP WG 1.8 meeting ``Open Problems in Concurrency'', Bertinoro
  • jun 2014
    Talk "Tutorial about Bigraphic Reactive Systems"
    MeMo Workshop, Berlin (associated with DisCoTec 2014)
  • oct 2013
    Talk "Weak bisimulations for LTSs weighted over semirings"
    NII Shonan Meeting on "Coinduction for computation structures and programming languages", Japan
  • feb 2010
    Talk "A bigraphical framework for protein and membrane interactions"
    Theory Days Conference, Andu, Estonia
  • may 2007
    Talk "Bigraphical models of calculi with names"
    Conference "Mathematical Theories of Abstraction, Substitution and Naming in Computer Science", ICMS, Edinburgh
  • sep 2007
    Talk "The directed bigraphical model"
    IFIP WG 2.2 Meeting, Nancy
  • feb 2006
    Talk "Behind the name: the many faces of atomic terms"
    Theory Days Conference, Koke, Estonia

Open Source Projects

PicNIC a non-interference verifier for the π-calculus
DBtk a toolkit for directed bigraphs
jLibBig a Java library for bigraphs
docker2ldb a correctness verifier for the composition of Docker containers
dbcchecker a security property verifier for containers, based on bigraphs and ProVerif
acidify an Erlang behaviour for distributed transactions over distributed storage
goabu a Go implementation of the AbU calculus
abuc a compiler for the AbU-dsl language
thud a LaTeX package for writing theses at the University of Udine

Honors and Awards

  • Jul 2021
    Best paper award for the work "Automated Symbolic Verification of Telegram’s MTProto 2.0"
    18th International Conference on Security and Cryptography (SECRYPT 2021).
  • Mar 2018
    National Scientific Qualification for the position of Full Professor in Computer Science
  • Jan 2011
    Best poster award for the work "Formal analysis of Facebook Connect Single Sign-On authentication protocol"
    37th International Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM 2011).

Other Interests

  • I play the saxophone in the Banda di Reana and in the Orchestra of the University of Udine - see our Gaudeamus, for a taste (yes, at that time I had a beard).