JSCL: A Middleware for Service Coordination. - Gian-Luigi Ferrari 002; Roberto Guanciale; Daniele Strollo (FORTE, 2006)

Event Based Service Coordination over Dynamic and Heterogeneous Networks. - Gian-Luigi Ferrari 002; Roberto Guanciale; Daniele Strollo (ICSOC, 2006)

Coordination Via Types in an Event-Based Framework. - Gianluigi Ferrari 002; Roberto Guanciale; Daniele Strollo; Emilio Tuosto (FORTE, 2007)

Event-Based Service Coordination. - Gian-Luigi Ferrari 002; Roberto Guanciale; Daniele Strollo; Emilio Tuosto (Concurrency, Graphs and Models, 2008)

Checking Correctness of Transactional Behaviors. - Vincenzo Ciancia; Gian-Luigi Ferrari 002; Roberto Guanciale; Daniele Strollo (FORTE, 2008)

Refactoring Long Running Transactions. - Gian-Luigi Ferrari 002; Roberto Guanciale; Daniele Strollo; Emilio Tuosto (WS-FM, 2008)

Debugging Distributed Systems with Causal Nets. - Gian-Luigi Ferrari 002; Roberto Guanciale; Daniele Strollo; Emilio Tuosto (Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2008)

Global Coordination Policies for Services. - Vincenzo Ciancia; Gian-Luigi Ferrari 002; Roberto Guanciale; Daniele Strollo (FACS, 2008)

BPMN Modelling of Services with Dynamically Reconfigurable Transactions. - Laura Bocchi; Roberto Guanciale; Daniele Strollo; Emilio Tuosto (ICSOC, 2010)

Refactoring Long Running Transactions: A Case Study. - Gian-Luigi Ferrari 002; Roberto Guanciale; Daniele Strollo; Emilio Tuosto (TGC, 2010)

Event based choreography. - Vincenzo Ciancia; Gian-Luigi Ferrari 002; Roberto Guanciale; Daniele Strollo (Sci. Comput. Program., 2010)

Model-Driven Development of Long Running Transactions. - Vincenzo Ciancia; Gian-Luigi Ferrari 002; Roberto Guanciale; Daniele Strollo; Emilio Tuosto (Results of the SENSORIA Project, 2011)

Applying Process Analysis to the Italian eGovernment Enterprise Architecture. - Roberto Bruni 001; Andrea Corradini 001; Gian-Luigi Ferrari 002; Tito Flagella; Roberto Guanciale; Giorgio Spagnolo (WS-FM, 2011)

Classification Techniques for Conformance and Performance Checking in Process Analysis. - Hind Chfouka; Andrea Corradini 001; Roberto Guanciale (AIBP@AI*IA, 2013)

Formal verification of information flow security for a simple arm-based separation kernel. - Mads Dam; Roberto Guanciale; Narges Khakpour; Hamed Nemati; Oliver Schwarz (CCS, 2013)

Machine code verification of a tiny ARM hypervisor. - Mads Dam; Roberto Guanciale; Hamed Nemati (TrustED@CCS, 2013)

Privacy Preserving Business Process Fusion. - Roberto Guanciale; Dilian Gurov (Business Process Management Workshops, 2014)

Automating Information Flow Analysis of Low Level Code. - Musard Balliu; Mads Dam; Roberto Guanciale (CCS, 2014)

Private intersection of regular languages. - Roberto Guanciale; Dilian Gurov; Peeter Laud (PST, 2014)

Trustworthy Prevention of Code Injection in Linux on Embedded Devices. - Hind Chfouka; Hamed Nemati; Roberto Guanciale; Mads Dam; Patrik Ekdahl (ESORICS (1), 2015)

Privacy preserving business process matching. - Dilian Gurov; Peeter Laud; Roberto Guanciale (PST, 2015)

Trustworthy Virtualization of the ARMv7 Memory Subsystem. - Hamed Nemati; Roberto Guanciale; Mads Dam (SOFSEM, 2015)

Trustworthy Memory Isolation of Linux on Embedded Devices. - Hamed Nemati; Mads Dam; Roberto Guanciale; Viktor Do; Arash Vahidi (TRUST, 2015)

Cache Storage Channels: Alias-Driven Attacks and Verified Countermeasures. - Roberto Guanciale; Hamed Nemati; Christoph Baumann; Mads Dam (IEEE Symposium on Security and Privacy, 2016)

An Abstract Semantics of the Global View of Choreographies. - Roberto Guanciale; Emilio Tuosto (ICE, 2016)

Provably secure memory isolation for Linux on ARM. - Roberto Guanciale; Hamed Nemati; Mads Dam; Christoph Baumann (J. Comput. Secur., 2016)

Sound Transpilation from Binary to Machine-Independent Code. - Roberto Metere; Andreas Lindner; Roberto Guanciale (SBMF, 2017)

Protecting Instruction Set Randomization from Code Reuse Attacks. - Roberto Guanciale (NordSec, 2018)

Formal Verification of Integrity-Preserving Countermeasures Against Cache Storage Side-Channels. - Hamed Nemati; Christoph Baumann; Roberto Guanciale; Mads Dam (POST, 2018)

Realisability of Pomsets via Communicating Automata. - Roberto Guanciale; Emilio Tuosto (ICE, 2018)

Semantics of global view of choreographies. - Emilio Tuosto; Roberto Guanciale (J. Log. Algebraic Methods Program., 2018)

DiRPOMS: Automatic Checker of Distributed Realizability of POMSets. - Roberto Guanciale (COORDINATION, 2019)

Trustworthy Isolation of DMA Enabled Devices. - Jonas Haglund; Roberto Guanciale (ICISS, 2019)

Realisability of pomsets. - Roberto Guanciale; Emilio Tuosto (J. Log. Algebraic Methods Program., 2019)

TrABin: Trustworthy analyses of binaries. - Andreas Lindner; Roberto Guanciale; Roberto Metere (Sci. Comput. Program., 2019)

Validation of Abstract Side-Channel Models for Computer Architectures. - Hamed Nemati; Pablo Buiras; Andreas Lindner; Roberto Guanciale; Swen Jacobs (CAV (1), 2020)

InSpectre: Breaking and Fixing Microarchitectural Vulnerabilities by Formal Analysis. - Roberto Guanciale; Musard Balliu; Mads Dam (CCS, 2020)

Choreographic Development of Message-Passing Applications - A Tutorial. - Alex Coto; Roberto Guanciale; Emilio Tuosto (COORDINATION, 2020)

On Testing Message-Passing Components. - Alex Coto; Roberto Guanciale; Emilio Tuosto (ISoLA (1), 2020)

Hoare-Style Logic for Unstructured Programs. - Didrik Lundberg; Roberto Guanciale; Andreas Lindner; Mads Dam (SEFM, 2020)

Speculative Leakage in ARM Cortex-A53. - Hamed Nemati; Roberto Guanciale; Pablo Buiras; Andreas Lindner (CoRR, 2020)

Trustworthy isolation of DMA devices. - Jonas Haglund; Roberto Guanciale (J. Bank. Financial Technol., 2020)

On Compositional Information Flow Aware Refinement. - Christoph Baumann; Mads Dam; Roberto Guanciale; Hamed Nemati (CSF, 2021)

Refinement-Based Verification of Device-to-Device Information Flow. - Ning Dong; Roberto Guanciale; Mads Dam (FMCAD, 2021)

Validation of Side-Channel Models via Observation Refinement. - Pablo Buiras; Hamed Nemati; Andreas Lindner; Roberto Guanciale (MICRO, 2021)

An abstract framework for choreographic testing. - Alex Coto; Roberto Guanciale; Emilio Tuosto (J. Log. Algebraic Methods Program., 2021)

PomCho: A tool chain for choreographic design. - Roberto Guanciale; Emilio Tuosto (Sci. Comput. Program., 2021)

A Case Study in Information Flow Refinement for Low Level Systems. - Roberto Guanciale; Christoph Baumann; Pablo Buiras; Mads Dam; Hamed Nemati (The Logic of Software. A Tasting Menu of Formal Methods, 2022)

HOL4P4: semantics for a verified data plane. - Anoud Alshnakat; Didrik Lundberg; Roberto Guanciale; Mads Dam; Karl Palmskog (EuroP4@CoNEXT, 2022)

Secure Partitioning of Composite Cloud Applications. - Alessandro Bocci; Roberto Guanciale; Stefano Forti 002; Gian-Luigi Ferrari 002; Antonio Brogi (ESOCC, 2022)

Formally Verified Isolation of DMA. - Jonas Haglund; Roberto Guanciale (FMCAD, 2022)

Foundations and Tools in HOL4 for Analysis of Microarchitectural Out-of-Order Execution. - Karl Palmskog; Xiaomo Yao; Ning Dong; Roberto Guanciale; Mads Dam (FMCAD, 2022)

SoK: Confidential Quartet - Comparison of Platforms for Virtualization-Based Confidential Computing. - Roberto Guanciale; Nicolae Paladi; Arash Vahidi (SEED, 2022)

Effective Reskilling of Foreign-Born People at Universities - The Software Development Academy. - Mattias Wiggberg; Elina Gobena; Matti Kaulio; Richard Glassey; Olle Bälter; Dena Hussain; Roberto Guanciale; Philipp Haller (IEEE Access, 2022)

Formal Verification of Correctness and Information Flow Security for an In-Order Pipelined Processor. - Ning Dong; Roberto Guanciale; Mads Dam; Andreas Lööw (FMCAD, 2023)

Proof-Producing Symbolic Execution for Binary Code Verification. - Andreas Lindner; Roberto Guanciale; Mads Dam (CoRR, 2023)

P4R-Type: a Verified API for P4 Control Plane Programs (Technical Report). - Jens Kanstrup Larsen; Roberto Guanciale; Philipp Haller; Alceste Scalas (CoRR, 2023)

Secure Partitioning of Cloud Applications, with Cost Look-Ahead. - Alessandro Bocci; Stefano Forti 002; Roberto Guanciale; Gian-Luigi Ferrari 002; Antonio Brogi (Future Internet, 2023)

P4R-Type: A Verified API for P4 Control Plane Programs. - Jens Kanstrup Larsen; Roberto Guanciale; Philipp Haller; Alceste Scalas (Proc. ACM Program. Lang., 2023)

Beyond Over-Protection: A Targeted Approach to Spectre Mitigation and Performance Optimization. - Tiziano Marinaro; Pablo Buiras; Andreas Lindner; Roberto Guanciale; Hamed Nemati (AsiaCCS, 2024)

Security Properties through the Lens of Modal Logic. - Matvey Soloviev; Musard Balliu; Roberto Guanciale (CSF, 2024)

Proof-Producing Symbolic Execution for P4. - Didrik Lundberg; Roberto Guanciale; Mads Dam (VSTTE, 2024)

HOL4P4: Mechanized Small-Step Semantics for P4. - Anoud Alshnakat; Didrik Lundberg; Roberto Guanciale; Mads Dam (Proc. ACM Program. Lang., 2024)

Leveraging Petri Nets for Workflow Anomaly Detection in Microservice Architectures. - Priyanka Kamboj; Cyrille Artho; Roberto Guanciale; Reyhaneh Jabbarvand; Brighten Godfrey (Petri Nets, 2025)

Securing P4 Programs by Information Flow Control. - Anoud Alshnakat; Amir M. Ahmadian; Musard Balliu; Roberto Guanciale; Mads Dam (CSF, 2025)

Trustworthy Verification of RISC-V Binaries Using Symbolic Execution in HolBA. - Karl Palmskog; Andreas Lindner; Scott Constable; Roberto Guanciale; Hamed Nemati (CoRR, 2025)