I am an Assistant Professor (non-tenure) in the Department of Mathematical, Physical, and Computer Sciences at the University of Parma. Previously, from September 2019 to September 2021, I was a postdoctoral researcher at the Ca’ Foscari University of Venice. I completed my Ph.D. in Computer Science under the supervision of Isabella Mastroeni at University of Verona. I hold a Bachelor’s and a Master’s degree in Computer Science, both received from the University of Verona.
My main research interests include static program analysis, abstract interpretation, string analysis and verification, analysis of smart contracts, and, more in general, formal methods for program security.
I am always looking for strong and motivated students to work with me on static program analysis and verification. Ping me if interested!
Interests
Static program analysis
Abstract interpretation
Software verification
Blockchain
Programming languages
Education
🎓 PhD in Computer Science, 2020 University of Verona, Verona, Italy
🎓 MSc in Computer Science, 2016 University of Verona, Verona, Italy
🎓 BSc in Computer Science, 2014 University of Verona, Verona, Italy
Fundamentals of Programming within the Computer Science B.Sc. in University of Parma (15CFU, 120 hours)
Publications
2024
[j10]
P. Ferrara, V. Arceri, A. Cortesi.
Challenges of software verification: the past, the present, the future, International Journal on Software Tools for Technology Transfer, 2024. [link][pdf]
[j9]
V. Arceri, G. Dolcetti, E. Zaffanella.
Speeding up static analysis with the split operator, International Journal on Software Tools for Technology Transfer, 2024. [link][pdf]
[c17]
V. Arceri, S. M. Merenda, L. Negrini, L. Olivieri, G. Dolcetti, E. Zaffanella.
Towards a Sound Construction of EVM Bytecode Control‐ flow Graphs, In Proceedings of the 26th International Workshop on Formal Techniques for Java‐like Programs, FTfJP 2024, September 20, 2024. [link][pdf]
[c16]
L. Negrini, V. Arceri, L. Olivieri, A. Cortesi, P. Ferrara. Teaching through Practice: Advanced Static Analysis with LiSA, In Proceedings of the 6th Formal Methods Teaching Workshop, FMTea 2024, Milan, Italy, September 10, 2024. [link][pdf]
[j8]
L. Olivieri, L. Negrini V. Arceri, B. Chachar, P. Ferrara, A. Cortesi
Detection of Phantom Reads in Hyperledger Fabric, In IEEE Access. 2024. [link][pdf]
[j7]
L. Negrini V. Arceri, A. Cortesi, P. Ferrara
Tarsis: An effective automata-based abstract domain for string analysis, In Journal of Software: Evolution and Process. Wiley. 2024. [link][pdf]
[c15]
G. Boldini, A. Diana, V. Arceri, V. Bonnici, R. Bagnara
A Machine Learning Approach for Source Code Similarity via Graph-Focused Features, In Proceedings of 9th International Conference, LOD 2023, Grasmere, UK, September 22–26, 2023. [link][pdf]
[j6]
L. Olivieri, L. Negrini, V. Arceri, T. Jensen, and F. Spoto
Design and implementation of static analyses for Tezos smart contracts, In Distrib. Ledger Technol., 2024. [link][pdf]
2023
[c14]
V. Arceri, G. Dolcetti, E. Zaffanella, Unconstrained Variable Oracles for Faster Numeric Static Analyses, In Proceedings of the 30th Static Analysis Symposium, SAS 2023, Cascais, Portugal, October 22 - 24, 2023. [link][pdf]
[bc3]
L. Negrini, V. Arceri, P. Ferrara, A. Cortesi, LiSA: A Generic Framework for Multilanguage Static Analysis, In Challenges of Software Verification. Intelligent Systems Reference Library, vol. 238. Springer, Singapore, 2023. [link]
[bc2]
E. Zaffanella, V. Arceri, “Fixing” the Specification of Widenings, In Challenges of Software Verification. Intelligent Systems Reference Library, vol. 238. Springer, Singapore, 2023. [link]
[bc1]
M. Olliaro, V. Arceri, A. Cortesi, P. Ferrara, Lifting String Analysis Domains, In Challenges of Software Verification. Intelligent Systems Reference Library, vol. 238. Springer, Singapore, 2023. [link]
[j5]
L. Olivieri, L. Negrini, V. Arceri, F. Tagliaferro, P. Ferrara, A. Cortesi, F. Spoto, Information Flow Analysis for Detecting Non-Determinism in Blockchain, Dagstuhl Artifacts Series, vol. 9, n. 2, 2023 [link]
[c13]
L. Olivieri, L. Negrini, V. Arceri, F. Tagliaferro, P. Ferrara, A. Cortesi, F. Spoto, Information Flow Analysis for Detecting Non-Determinism in Blockchain, In Proceedings of the 37th European Conference on Object-Oriented Programming, ECOOP 2023, Seattle, WA, USA, July 17 - 21, 2023. [link][pdf]
[c12]
V. Arceri, G. Dolcetti, E. Zaffanella, Speeding up Static Analysis with the Split Operator, In Proceedings of the 12th ACM SIGPLAN International Workshop on the
State Of the Art in Program Analysis, SOAP 2023, Orlando, FL, USA, June 17, 2023. [link][pdf]
[c11]
V. Bonnici, V. Arceri, A. Diana, F. Bertini, E. Iotti, A. Levante, V. Bernini, E. Neviani, A. Dal Palù, BIOCHAIN: towards a platform for securely sharing microbiological data In Proceedings of 27th International Database Engineered Applications Symposium, IDEAS 2023, Heraklion, Crete, Greece, May 5-7, 2023. [link][pdf]
2022
[c10]
V. Arceri, I. Mastroeni, E. Zaffanella, Decoupling the Ascending and Descending Phases in Abstract Interpretation, In Proceedings of 20th Asian Symposium on Programming Languages and Systems, APLAS 2022, Auckland, New Zealand, December 5, 2022. [link][pdf]
[c9]
L. Olivieri, F. Tagliaferro, V. Arceri, M. Ruaro, L. Negrini, A. Cortesi, P. Ferrara, F. Spoto, E. Talin, Ensuring Determinism in Blockchain Software with GoLiSA: An Industrial Experience Report, In Proceedings of 11th ACM SIGPLAN International Workshop on the State of the Art in Program Analysis, SOAP 2022, June 17, 2022. [link][pdf]
[c8]
V. Arceri, M.Olliaro, A. Cortesi, P. Ferrara, Relational String Abstract Domains, In Proceedings of the 23th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2022, Philadelphia, January 16-19, 2022. [link][pdf]
2021
[j4]
V. Arceri, M. Olliaro, A. Cortesi, I. Mastroeni, Completeness of String Analysis for Dynamic Languages
, in Information and Computation, 104791, 2021 [link]
[c7]
P. Ferrara, L. Negrini, V. Arceri, A. Cortesi, Static Analysis for Dummies: Experiencing LiSA
, in Proceedings of 10th ACM SIGPLAN International Workshop on the State of the Art in Program Analysis, SOAP 2021, June 22th, 2021 [link][pdf]
[c6]
I. Mastroeni, V. Arceri, Improving dynamic code analysis by code abstraction
, in Proceedings of 9th International Workshop on Verification and Program Transformation, VPT 2021, March 27 and 28, 2021 [link][pdf]
[j3]
V. Arceri, I. Mastroeni, Analyzing Dynamic Code: A Sound Abstract Interpreter for evil eval, in ACM Transactions on Privacy and Security, 2021, Vol. 24, No. 2. [link]
[c5]
L.Negrini, V. Arceri, P. Ferrara, A. Cortesi, Twinning Automata and Regular Expressions for String Static Analysis, in Proceedings of the 22nd International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2021, Online, January 17-22, 2021. [link][pdf]
2020
[j2]
V. Arceri, I. Mastroeni, S. Xu, Static Analysis for ECMAScript String Manipulation Programs, in Applied Science, SI: Static Analysis Techniques: Recent Advances and New Horizons, 2020 [link]
[c4]
V. Arceri, I. Mastroeni, A Sound Abstract Interpreter for Dynamic Code, in Proceedings of the 35th ACM/SIGAPP Symposium On Applied Computing, SAC 2020, Brno, Czech Republic March 30 - April 3, 2020 [link][pdf]
2019
[c3]
V. Arceri, M. Pasqua, I. Mastroeni, An Abstract Domain for Objects in Dynamic Programming languages, in informal Proceedings of the 8th International Workshop on Numerical and Symbolic Abstract Domains, NSAD 2019, Porto, Portugal, October 8, 2019 [link][pdf]
[c2]
V. Arceri, M. Olliaro, A. Cortesi, I. Mastroeni, Completeness of Abstract Domains for String Analysis of JavaScript Programs, in Proceedings of 16th International Colloquium of Theoretical Aspects of Computing, ICTAC 2019, Hammamet, Tunisia, October 31 - November 4, 2019 [link][pdf]
[c1]
V. Arceri, I. Mastroeni, Static Program Analysis for String Manipulation Languages, in Proceedings of 7th International Workshop on Verification and Program Transformation, VPT@Programming 2019, Genova, Italy, April 2, 2019 [link][pdf]
2017
[j1]
V. Arceri, S. Maffeis, Abstract Domains for Type Juggling, in Electr. Notes Theor. Comput. Sci., 331, pp. 41-55, 2017. [link]
Ph.D. Thesis
V. Arceri, Taming Strings in Dynamic Languages – An Abstract Interpretation-based Static Analysis Approach, Ph.D. Thesis, 2020. [link]
Static Analysis for Dummies: Experiencing LiSA, SOAP@PLDI 2021 (online)
2020
May
Taming Strings in Dynamic Languages – An Abstract Interpretation-based Static Analysis Approach, PhD Thesis defence (online)
Mar
A Sound Abstract Interpreter for Dynamic Code, SAC 2020, Brno, Czech Republic (online)
2019
Nov
Completeness of Abstract Domains for String Analysis of JavaScript Programs, ICTAC 2019, Hammamet, Tunisia
Apr
Static Program Analysis for String Manipulation Languages, VPT 2019, Genova, Italy
2016
Sep
Abstract Domains for Type Juggling, NSAD 2016, Edimburgh, Scotland
Projects
EVMLiSA: an abstract interpretation‐based static analyzer for EVM bytecode
EVMLiSA is a static analyzer based on abstract interpretation for EVM bytecode of smart contracts deployed on Ethereum blockchain and built upon LiSA. Given a EVM bytecode smart contract, EVMLiSA builds a sound and precise control‐flow graph of the smart contract.
EVMLiSA is maintained by University of Parma, Italy, and it is available on Github.
LiSA: a Library for Static Analysis
LiSA (Library for Static Analysis) eases the creation and implementation of static analyzers based on the Abstract Interpretation theory. LiSA provides an analysis engine that works on a generic and extensible control flow graph representation of the program to analyze. Abstract interpreters in LiSA are built for analyzing such representation, providing a unique analysis infrastructure for all the analyzers that will rely on it.
Building an analyzer upon LiSA boils down to writing a parser for the language that one aims to analyze, translating the source code or the compiled code towards the control flow graph representation of LiSA. Then, simple checks iterating over the results provided by the semantic analyses of LiSA can be easily defined to translate semantic information into warnings that can be of value for the final user.
LiSA is maintained by the Software and System Verification group @ Ca’ Foscari University of Venice, Italy, and it is distributed under the MIT license, and it is available on GitHub.
Tarsis: an improved finite‐state automata‐based string abstract domain
Tarsis is a new abstract domain for string values based on finite state automata. Standard finite state automata abstract domain has been shown to provide precise abstractions of string values when all the components of such strings are known, but with high computational cost. Instead of considering standard finite automata built over an alphabet of single characters, Tarsis considers automata that are built over an alphabet of strings, comprising a special value to represent statically unknown strings. Tarsis is maintained by the Software and System Verification group @ Ca’ Foscari University of Venice, Italy, and it is available on Github.
