Roberto Guanciale

81 papers A* 5A 7B 8C 8Misc 1Journal 26Unranked 25

Year	Rank	Type	Title / Venue / Authors
2026	B	`conf`	Forward Symbolic Execution for Trustworthy Automation of Binary Code Verification. VMCAI Andreas Lindner, Karl Palmskog, Scott Constable, Mads Dam, Roberto Guanciale, Hamed Nemati
2026	J	`jnl`	Hoare-style logic for unstructured programs. J. Log. Algebraic Methods Program. Didrik Lundberg, Roberto Guanciale, Andreas Lindner, Mads Dam
2025	J	`jnl`	Dissect-and-Restore: AI-based Code Verification with Transient Refactoring. CoRR Changjie Wang, Mariano Scazzariello, Anoud Alshnakat, Roberto Guanciale, Dejan Kostic, Marco Chiesa
2025	B	`conf`	Leveraging Petri Nets for Workflow Anomaly Detection in Microservice Architectures. Petri Nets Priyanka Kamboj, Cyrille Artho, Roberto Guanciale, Reyhaneh Jabbarvand, Brighten Godfrey
2025	—	`conf`	Mitigating Traffic Analysis Attacks While Maintaining On-Path Network Observability. NordSec János Kövér, Roberto Guanciale, György Dán
2025	A	`conf`	Partitioning Kernel With Capability Controlled Temporal and Spatial Partitioning. RTSS Henrik A. Karlsson, Roberto Guanciale
2025	C	`conf`	Pomsets for Process Management: A Healthcare Case Study. ICTAC Sourabh Pal, Roberto Guanciale, Ivan Lanese, Emilio Tuosto, Massimo Clo
2025	A	`conf`	Securing P4 Programs by Information Flow Control. CSF Anoud Alshnakat, Amir M. Ahmadian, Musard Balliu, Roberto Guanciale, Mads Dam
2025	J	`jnl`	Securing P4 Programs by Information Flow Control. CoRR Anoud Alshnakat, Amir M. Ahmadian, Musard Balliu, Roberto Guanciale, Mads Dam
2025	—	`conf`	Timing Interference in Multi-core RISC-V Systems: Security Risks and Mitigations. NordSec Andreas Wrisley, Roberto Guanciale, Simin Nadjm-Tehrani, Ingemar Söderquist
2025	J	`jnl`	Trustworthy Verification of RISC-V Binaries Using Symbolic Execution in HolBA. CoRR Karl Palmskog, Andreas Lindner, Scott Constable, Roberto Guanciale, Hamed Nemati
2024	A	`conf`	Beyond Over-Protection: A Targeted Approach to Spectre Mitigation and Performance Optimization. AsiaCCS Tiziano Marinaro, Pablo Buiras, Andreas Lindner, Roberto Guanciale, Hamed Nemati
2024	J	`jnl`	HOL4P4: Mechanized Small-Step Semantics for P4. Proc. ACM Program. Lang. Anoud Alshnakat, Didrik Lundberg, Roberto Guanciale, Mads Dam
2024	—	`conf`	Proof-Producing Symbolic Execution for P4. VSTTE Didrik Lundberg, Roberto Guanciale, Mads Dam
2024	A	`conf`	Security Properties through the Lens of Modal Logic. CSF Matvey Soloviev, Musard Balliu, Roberto Guanciale
2023	J	`jnl`	Beyond Over-Protection: A Targeted Approach to Spectre Mitigation and Performance Optimization. CoRR Tiziano Marinaro, Pablo Buiras, Andreas Lindner, Roberto Guanciale, Hamed Nemati
2023	B	`conf`	Formal Verification of Correctness and Information Flow Security for an In-Order Pipelined Processor. FMCAD Ning Dong, Roberto Guanciale, Mads Dam, Andreas Lööw
2023	J	`jnl`	P4R-Type: A Verified API for P4 Control Plane Programs. Proc. ACM Program. Lang. Jens Kanstrup Larsen, Roberto Guanciale, Philipp Haller, Alceste Scalas
2023	J	`jnl`	P4R-Type: a Verified API for P4 Control Plane Programs (Technical Report). CoRR Jens Kanstrup Larsen, Roberto Guanciale, Philipp Haller, Alceste Scalas
2023	J	`jnl`	Proof-Producing Symbolic Execution for Binary Code Verification. CoRR Andreas Lindner, Roberto Guanciale, Mads Dam
2023	J	`jnl`	Secure Partitioning of Cloud Applications, with Cost Look-Ahead. Future Internet Alessandro Bocci, Stefano Forti, Roberto Guanciale, Gian-Luigi Ferrari, Antonio Brogi
2023	J	`jnl`	Security Properties through the Lens of Modal Logic. CoRR Matvey Soloviev, Musard Balliu, Roberto Guanciale
2022	—	`conf`	A Case Study in Information Flow Refinement for Low Level Systems. The Logic of Software. A Tasting Menu of Formal Methods Roberto Guanciale, Christoph Baumann, Pablo Buiras, Mads Dam, Hamed Nemati
2022	J	`jnl`	Effective Reskilling of Foreign-Born People at Universities - The Software Development Academy. IEEE Access Mattias Wiggberg, Elina Gobena, Matti Kaulio, Richard Glassey, Olle Bälter, Dena Hussain, Roberto Guanciale, Philipp Haller
2022	B	`conf`	Formally Verified Isolation of DMA. FMCAD Jonas Haglund, Roberto Guanciale
2022	B	`conf`	Foundations and Tools in HOL4 for Analysis of Microarchitectural Out-of-Order Execution. FMCAD Karl Palmskog, Xiaomo Yao, Ning Dong, Roberto Guanciale, Mads Dam
2022	—	`conf`	HOL4P4: semantics for a verified data plane. EuroP4@CoNEXT Anoud Alshnakat, Didrik Lundberg, Roberto Guanciale, Mads Dam, Karl Palmskog
2022	—	`conf`	Secure Partitioning of Composite Cloud Applications. ESOCC Alessandro Bocci, Roberto Guanciale, Stefano Forti, Gian-Luigi Ferrari, Antonio Brogi
2022	—	`conf`	SoK: Confidential Quartet - Comparison of Platforms for Virtualization-Based Confidential Computing. SEED Roberto Guanciale, Nicolae Paladi, Arash Vahidi
2021	J	`jnl`	An abstract framework for choreographic testing. J. Log. Algebraic Methods Program. Alex Coto, Roberto Guanciale, Emilio Tuosto
2021	A	`conf`	On Compositional Information Flow Aware Refinement. CSF Christoph Baumann, Mads Dam, Roberto Guanciale, Hamed Nemati
2021	J	`jnl`	PomCho: A tool chain for choreographic design. Sci. Comput. Program. Roberto Guanciale, Emilio Tuosto
2021	B	`conf`	Refinement-Based Verification of Device-to-Device Information Flow. FMCAD Ning Dong, Roberto Guanciale, Mads Dam
2021	A*	`conf`	Validation of Side-Channel Models via Observation Refinement. MICRO Pablo Buiras, Hamed Nemati, Andreas Lindner, Roberto Guanciale
2020	—	`conf`	An Abstract Framework for Choreographic Testing. ICE Alex Coto, Roberto Guanciale, Emilio Tuosto
2020	C	`conf`	Choreographic Development of Message-Passing Applications - A Tutorial. COORDINATION Alex Coto, Roberto Guanciale, Emilio Tuosto
2020	B	`conf`	Hoare-Style Logic for Unstructured Programs. SEFM Didrik Lundberg, Roberto Guanciale, Andreas Lindner, Mads Dam
2020	A*	`conf`	InSpectre: Breaking and Fixing Microarchitectural Vulnerabilities by Formal Analysis. CCS Roberto Guanciale, Musard Balliu, Mads Dam
2020	—	`conf`	On Testing Message-Passing Components. ISoLA (1) Alex Coto, Roberto Guanciale, Emilio Tuosto
2020	J	`jnl`	Speculative Leakage in ARM Cortex-A53. CoRR Hamed Nemati, Roberto Guanciale, Pablo Buiras, Andreas Lindner
2020	J	`jnl`	Trustworthy isolation of DMA devices. J. Bank. Financial Technol. Jonas Haglund, Roberto Guanciale
2020	—	`conf`	Validation of Abstract Side-Channel Models for Computer Architectures. CAV (1) Hamed Nemati, Pablo Buiras, Andreas Lindner, Roberto Guanciale, Swen Jacobs
2020	J	`jnl`	Validation of Abstract Side-Channel Models for Computer Architectures. CoRR Hamed Nemati, Pablo Buiras, Andreas Lindner, Roberto Guanciale, Swen Jacobs
2019	C	`conf`	DiRPOMS: Automatic Checker of Distributed Realizability of POMSets. COORDINATION Roberto Guanciale
2019	J	`jnl`	InSpectre: Breaking and Fixing Microarchitectural Vulnerabilities by Formal Analysis. CoRR Musard Balliu, Mads Dam, Roberto Guanciale
2019	J	`jnl`	Realisability of pomsets. J. Log. Algebraic Methods Program. Roberto Guanciale, Emilio Tuosto
2019	J	`jnl`	TrABin: Trustworthy Analyses of Binaries. CoRR Andreas Lindner, Roberto Guanciale, Roberto Metere
2019	J	`jnl`	TrABin: Trustworthy analyses of binaries. Sci. Comput. Program. Andreas Lindner, Roberto Guanciale, Roberto Metere
2019	Misc	`conf`	Trustworthy Isolation of DMA Enabled Devices. ICISS Jonas Haglund, Roberto Guanciale
2018	—	`conf`	Formal Verification of Integrity-Preserving Countermeasures Against Cache Storage Side-Channels. POST Hamed Nemati, Christoph Baumann, Roberto Guanciale, Mads Dam
2018	—	`conf`	Protecting Instruction Set Randomization from Code Reuse Attacks. NordSec Roberto Guanciale
2018	—	`conf`	Realisability of Pomsets via Communicating Automata. ICE Roberto Guanciale, Emilio Tuosto
2018	J	`jnl`	Semantics of global view of choreographies. J. Log. Algebraic Methods Program. Emilio Tuosto, Roberto Guanciale
2018	J	`jnl`	Sound Transpilation from Binary to Machine-Independent Code. CoRR Roberto Metere, Andreas Lindner, Roberto Guanciale
2017	—	`conf`	Sound Transpilation from Binary to Machine-Independent Code. SBMF Roberto Metere, Andreas Lindner, Roberto Guanciale
2016	—	`conf`	An Abstract Semantics of the Global View of Choreographies. ICE Roberto Guanciale, Emilio Tuosto
2016	A*	`conf`	Cache Storage Channels: Alias-Driven Attacks and Verified Countermeasures. IEEE Symposium on Security and Privacy Roberto Guanciale, Hamed Nemati, Christoph Baumann, Mads Dam
2016	J	`jnl`	Provably secure memory isolation for Linux on ARM. J. Comput. Secur. Roberto Guanciale, Hamed Nemati, Mads Dam, Christoph Baumann
2015	C	`conf`	Privacy preserving business process matching. PST Dilian Gurov, Peeter Laud, Roberto Guanciale
2015	—	`conf`	Trustworthy Memory Isolation of Linux on Embedded Devices. TRUST Hamed Nemati, Mads Dam, Roberto Guanciale, Viktor Do, Arash Vahidi
2015	—	`conf`	Trustworthy Prevention of Code Injection in Linux on Embedded Devices. ESORICS (1) Hind Chfouka, Hamed Nemati, Roberto Guanciale, Mads Dam, Patrik Ekdahl
2015	B	`conf`	Trustworthy Virtualization of the ARMv7 Memory Subsystem. SOFSEM Hamed Nemati, Roberto Guanciale, Mads Dam
2014	A*	`conf`	Automating Information Flow Analysis of Low Level Code. CCS Musard Balliu, Mads Dam, Roberto Guanciale
2014	—	`conf`	Privacy Preserving Business Process Fusion. Business Process Management Workshops Roberto Guanciale, Dilian Gurov
2014	C	`conf`	Private intersection of regular languages. PST Roberto Guanciale, Dilian Gurov, Peeter Laud
2013	—	`conf`	Classification Techniques for Conformance and Performance Checking in Process Analysis. AIBP@AI*IA Hind Chfouka, Andrea Corradini, Roberto Guanciale
2013	A*	`conf`	Formal verification of information flow security for a simple arm-based separation kernel. CCS Mads Dam, Roberto Guanciale, Narges Khakpour, Hamed Nemati, Oliver Schwarz
2013	—	`conf`	Machine code verification of a tiny ARM hypervisor. TrustED@CCS Mads Dam, Roberto Guanciale, Hamed Nemati
2011	—	`conf`	Applying Process Analysis to the Italian eGovernment Enterprise Architecture. WS-FM Roberto Bruni, Andrea Corradini, Gian-Luigi Ferrari, Tito Flagella, Roberto Guanciale, Giorgio Spagnolo
2011	—	`ch.`	Model-Driven Development of Long Running Transactions. Results of the SENSORIA Project Vincenzo Ciancia, Gian-Luigi Ferrari, Roberto Guanciale, Daniele Strollo, Emilio Tuosto
2010	A	`conf`	BPMN Modelling of Services with Dynamically Reconfigurable Transactions. ICSOC Laura Bocchi, Roberto Guanciale, Daniele Strollo, Emilio Tuosto
2010	J	`jnl`	Event based choreography. Sci. Comput. Program. Vincenzo Ciancia, Gian-Luigi Ferrari, Roberto Guanciale, Daniele Strollo
2010	—	`conf`	Refactoring Long Running Transactions: A Case Study. TGC Gian-Luigi Ferrari, Roberto Guanciale, Daniele Strollo, Emilio Tuosto
2008	C	`conf`	Checking Correctness of Transactional Behaviors. FORTE Vincenzo Ciancia, Gian-Luigi Ferrari, Roberto Guanciale, Daniele Strollo
2008	J	`jnl`	Debugging Distributed Systems with Causal Nets. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. Gian-Luigi Ferrari, Roberto Guanciale, Daniele Strollo, Emilio Tuosto
2008	—	`conf`	Event-Based Service Coordination. Concurrency, Graphs and Models Gian-Luigi Ferrari, Roberto Guanciale, Daniele Strollo, Emilio Tuosto
2008	—	`conf`	Global Coordination Policies for Services. FACS Vincenzo Ciancia, Gian-Luigi Ferrari, Roberto Guanciale, Daniele Strollo
2008	—	`conf`	Refactoring Long Running Transactions. WS-FM Gian-Luigi Ferrari, Roberto Guanciale, Daniele Strollo, Emilio Tuosto
2007	C	`conf`	Coordination Via Types in an Event-Based Framework. FORTE Gianluigi Ferrari, Roberto Guanciale, Daniele Strollo, Emilio Tuosto
2006	A	`conf`	Event Based Service Coordination over Dynamic and Heterogeneous Networks. ICSOC Gian-Luigi Ferrari, Roberto Guanciale, Daniele Strollo
2006	C	`conf`	JSCL: A Middleware for Service Coordination. FORTE Gian-Luigi Ferrari, Roberto Guanciale, Daniele Strollo