| 2025 | FC | A Formalization of Signum's Consensus. | Fausto Spoto |
| 2025 | SAC | Static Detection of Untrusted Cross-Contract Invocations in Go Smart Contracts. | Luca Olivieri, Luca Negrini, Vincenzo Arceri, Pietro Ferrara, Agostino Cortesi, Fausto Spoto |
| 2023 | ECOOP | Information Flow Analysis for Detecting Non-Determinism in Blockchain. | Luca Olivieri, Luca Negrini, Vincenzo Arceri, Fabio Tagliaferro, Pietro Ferrara, Agostino Cortesi, Fausto Spoto |
| 2023 | PERCOM | MichelsonLiSA: A Static Analyzer for Tezos. | Luca Olivieri, Thomas P. Jensen, Luca Negrini, Fausto Spoto |
| 2022 | PLDI | Ensuring determinism in blockchain software with GoLiSA: an industrial experience report. | Luca Olivieri, Fabio Tagliaferro, Vincenzo Arceri, Marco Ruaro, Luca Negrini, Agostino Cortesi, Pietro Ferrara, Fausto Spoto, Enrico Talin |
| 2021 | FC | On-Chain Smart Contract Verification over Tendermint. | Luca Olivieri, Fausto Spoto, Fabio Tagliaferro |
| 2020 | FC | Enforcing Determinism of Java Smart Contracts. | Fausto Spoto |
| 2020 | SAC | Cross-program taint analysis for IoT systems. | Amit Kr Mandal, Pietro Ferrara, Yuliy Khlyebnikov, Agostino Cortesi, Fausto Spoto |
| 2020 | VMCAI | BackFlow: Backward Context-Sensitive Flow Reconstruction of Taint Analysis Results. | Pietro Ferrara, Luca Olivieri, Fausto Spoto |
| 2019 | FC | A Java Framework for Smart Contracts. | Fausto Spoto |
| 2018 | CADE | Checking Array Bounds by Abstract Interpretation and Symbolic Expressions. | tienne Payet, Fausto Spoto |
| 2018 | ICSE | CIL to Java-bytecode translation for static analysis leveraging. | Pietro Ferrara, Agostino Cortesi, Fausto Spoto |
| 2018 | TrustCom | SDLI: Static Detection of Leaks Across Intents. | Rocco Salvia, Pietro Ferrara, Fausto Spoto, Agostino Cortesi |
| 2016 | ICSE | Locking discipline inference and checking. | Michael D. Ernst, Alberto Lovato, Damiano Macedonio, Fausto Spoto, Javier Thaine |
| 2016 | SAS | The Julia Static Analyzer for Java. | Fausto Spoto |
| 2015 | LPAR | Boolean Formulas for the Static Identification of Injection Attacks in Java. | Michael D. Ernst, Alberto Lovato, Damiano Macedonio, Ciprian Spiridon, Fausto Spoto |
| 2014 | PEPM | An operational semantics for android activities. | tienne Payet, Fausto Spoto |
| 2014 | SEFM | A Thread-Safe Library for Binary Decision Diagrams. | Alberto Lovato, Damiano Macedonio, Fausto Spoto |
| 2012 | CADE | Reachability Analysis of Program Variables. | Durica Nikolic, Fausto Spoto |
| 2012 | ICTAC | Definite Expression Aliasing Analysis for Java Bytecode. | Durica Nikolic, Fausto Spoto |
| 2012 | LATA | Automaton-Based Array Initialization Analysis. | Durica Nikolic, Fausto Spoto |
| 2011 | CADE | Static Analysis of Android Programs. | tienne Payet, Fausto Spoto |
| 2011 | ICSE | Inference of field initialization. | Fausto Spoto, Michael D. Ernst |
| 2010 | LPAR | The Nullness Analyser of julia. | Fausto Spoto |
| 2008 | SAC | Special track on Software Verification: editorial message. | Fausto Spoto |
| 2008 | SEFM | Nullness Analysis in Boolean Form. | Fausto Spoto |
| 2007 | SAS | Magic-Sets Transformation for the Analysis of Java Bytecode. | tienne Payet, Fausto Spoto |
| 2006 | VMCAI | Detecting Non-cyclicity by Abstract Compilation into Boolean Functions. | Stefano Rossignoli, Fausto Spoto |
| 2005 | ICTAC | Information Flow Is Linear Refinement of Constancy. | Fausto Spoto |
| 2005 | SAS | Pair-Sharing Analysis of Object-Oriented Programs. | Stefano Secci, Fausto Spoto |
| 2005 | VMCAI | Information Flow Analysis for Java Bytecode. | Samir Genaim, Fausto Spoto |
| 2003 | PADL | Logic Programs as Compact Denotations. | Patricia M. Hill, Fausto Spoto |
| 2002 | VMCAI | A Refinement of the Escape Property. | Patricia M. Hill, Fausto Spoto |
| 2001 | FLOPS | Abstract Compilation for Sharing Analysis. | Gianluca Amato, Fausto Spoto |
| 2001 | FOSSACS | Class Analysis of Object-Oriented Programs through Abstract Interpretation. | Thomas P. Jensen, Fausto Spoto |
| 2001 | SAS | Watchpoint Semantics: A Tool for Compositional and Focussed Static Analyses. | Fausto Spoto |
| 2000 | PEPM | Non Pair-Sharing and Freeness Analysis Through Linear Refinement. | Giorgio Levi, Fausto Spoto |
| 1999 | SAS | Freeness Analysis Through Linear Refinement. | Patricia M. Hill, Fausto Spoto |