Roberto Guanciale

Orcid: 0000-0002-8069-6495

According to our database1, Roberto Guanciale authored at least 61 papers between 2006 and 2023.

Collaborative distances:

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2023
P4R-Type: A Verified API for P4 Control Plane Programs.
Proc. ACM Program. Lang., October, 2023

Secure Partitioning of Cloud Applications, with Cost Look-Ahead.
Future Internet, July, 2023

Beyond Over-Protection: A Targeted Approach to Spectre Mitigation and Performance Optimization.
CoRR, 2023

Security Properties through the Lens of Modal Logic.
CoRR, 2023

P4R-Type: a Verified API for P4 Control Plane Programs (Technical Report).
CoRR, 2023

Proof-Producing Symbolic Execution for Binary Code Verification.
CoRR, 2023

Formal Verification of Correctness and Information Flow Security for an In-Order Pipelined Processor.
Proceedings of the Formal Methods in Computer-Aided Design, 2023

2022
Effective Reskilling of Foreign-Born People at Universities - The Software Development Academy.
IEEE Access, 2022

SoK: Confidential Quartet - Comparison of Platforms for Virtualization-Based Confidential Computing.
Proceedings of the 2022 IEEE International Symposium on Secure and Private Execution Environment Design (SEED), 2022

Foundations and Tools in HOL4 for Analysis of Microarchitectural Out-of-Order Execution.
Proceedings of the 22nd Formal Methods in Computer-Aided Design, 2022

Formally Verified Isolation of DMA.
Proceedings of the 22nd Formal Methods in Computer-Aided Design, 2022

Secure Partitioning of Composite Cloud Applications.
Proceedings of the Service-Oriented and Cloud Computing, 2022

HOL4P4: semantics for a verified data plane.
Proceedings of the 5th International Workshop on P4 in Europe, 2022

A Case Study in Information Flow Refinement for Low Level Systems.
Proceedings of the Logic of Software. A Tasting Menu of Formal Methods, 2022

2021
PomCho: A tool chain for choreographic design.
Sci. Comput. Program., 2021

Validation of Side-Channel Models via Observation Refinement.
Proceedings of the MICRO '21: 54th Annual IEEE/ACM International Symposium on Microarchitecture, 2021

Refinement-Based Verification of Device-to-Device Information Flow.
Proceedings of the Formal Methods in Computer Aided Design, 2021

On Compositional Information Flow Aware Refinement.
Proceedings of the 34th IEEE Computer Security Foundations Symposium, 2021

2020
Trustworthy isolation of DMA devices.
J. Bank. Financial Technol., 2020

An Abstract Framework for Choreographic Testing.
Proceedings of the Proceedings 13th Interaction and Concurrency Experience, 2020

Speculative Leakage in ARM Cortex-A53.
CoRR, 2020

Hoare-Style Logic for Unstructured Programs.
Proceedings of the Software Engineering and Formal Methods - 18th International Conference, 2020

On Testing Message-Passing Components.
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles, 2020

Choreographic Development of Message-Passing Applications - A Tutorial.
Proceedings of the Coordination Models and Languages, 2020

InSpectre: Breaking and Fixing Microarchitectural Vulnerabilities by Formal Analysis.
Proceedings of the CCS '20: 2020 ACM SIGSAC Conference on Computer and Communications Security, 2020

Validation of Abstract Side-Channel Models for Computer Architectures.
Proceedings of the Computer Aided Verification - 32nd International Conference, 2020

2019
TrABin: Trustworthy analyses of binaries.
Sci. Comput. Program., 2019

Realisability of pomsets.
J. Log. Algebraic Methods Program., 2019

Trustworthy Isolation of DMA Enabled Devices.
Proceedings of the Information Systems Security - 15th International Conference, 2019

DiRPOMS: Automatic Checker of Distributed Realizability of POMSets.
Proceedings of the Coordination Models and Languages, 2019

2018
Semantics of global view of choreographies.
J. Log. Algebraic Methods Program., 2018

Realisability of Pomsets via Communicating Automata.
Proceedings of the Proceedings 11th Interaction and Concurrency Experience, 2018

Formal Verification of Integrity-Preserving Countermeasures Against Cache Storage Side-Channels.
Proceedings of the Principles of Security and Trust - 7th International Conference, 2018

Protecting Instruction Set Randomization from Code Reuse Attacks.
Proceedings of the Secure IT Systems - 23rd Nordic Conference, NordSec 2018, Oslo, Norway, 2018

2017
Sound Transpilation from Binary to Machine-Independent Code.
Proceedings of the Formal Methods: Foundations and Applications - 20th Brazilian Symposium, 2017

2016
Provably secure memory isolation for Linux on ARM.
J. Comput. Secur., 2016

An Abstract Semantics of the Global View of Choreographies.
Proceedings of the Proceedings 9th Interaction and Concurrency Experience, 2016

Cache Storage Channels: Alias-Driven Attacks and Verified Countermeasures.
Proceedings of the IEEE Symposium on Security and Privacy, 2016

2015
Trustworthy Memory Isolation of Linux on Embedded Devices.
Proceedings of the Trust and Trustworthy Computing - 8th International Conference, 2015

Trustworthy Virtualization of the ARMv7 Memory Subsystem.
Proceedings of the SOFSEM 2015: Theory and Practice of Computer Science, 2015

Privacy preserving business process matching.
Proceedings of the 13th Annual Conference on Privacy, Security and Trust, 2015

Trustworthy Prevention of Code Injection in Linux on Embedded Devices.
Proceedings of the Computer Security - ESORICS 2015, 2015

2014
Private intersection of regular languages.
Proceedings of the 2014 Twelfth Annual International Conference on Privacy, 2014

Automating Information Flow Analysis of Low Level Code.
Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security, 2014

Privacy Preserving Business Process Fusion.
Proceedings of the Business Process Management Workshops, 2014

2013
Machine code verification of a tiny ARM hypervisor.
Proceedings of the TrustED'13, 2013

Formal verification of information flow security for a simple arm-based separation kernel.
Proceedings of the 2013 ACM SIGSAC Conference on Computer and Communications Security, 2013

Classification Techniques for Conformance and Performance Checking in Process Analysis.
Proceedings of the Workshop AI Meets Business Processes 2013 co-located with the 13th Conference of the Italian Association for Artificial Intelligence (AI*IA 2013), 2013

2011
Applying Process Analysis to the Italian eGovernment Enterprise Architecture.
Proceedings of the Web Services and Formal Methods - 8th International Workshop, 2011

Model-Driven Development of Long Running Transactions.
Proceedings of the Rigorous Software Engineering for Service-Oriented Systems, 2011

2010
Event based choreography.
Sci. Comput. Program., 2010

Refactoring Long Running Transactions: A Case Study.
Proceedings of the Trustworthly Global Computing - 5th International Symposium, 2010

BPMN Modelling of Services with Dynamically Reconfigurable Transactions.
Proceedings of the Service-Oriented Computing - 8th International Conference, 2010

2008
Global Coordination Policies for Services.
Proceedings of the 5th International Workshop on Formal Aspects of Component Software, 2008

Debugging Distributed Systems with Causal Nets.
Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2008

Refactoring Long Running Transactions.
Proceedings of the Web Services and Formal Methods, 5th International Workshop, 2008

Checking Correctness of Transactional Behaviors.
Proceedings of the Formal Techniques for Networked and Distributed Systems, 2008

Event-Based Service Coordination.
Proceedings of the Concurrency, 2008

2007
Coordination Via Types in an Event-Based Framework.
Proceedings of the Formal Techniques for Networked and Distributed Systems, 2007

2006
Event Based Service Coordination over Dynamic and Heterogeneous Networks.
Proceedings of the Service-Oriented Computing, 2006

JSCL: A Middleware for Service Coordination.
Proceedings of the Formal Techniques for Networked and Distributed Systems, 2006


  Loading...