TBA

Due to its interdisciplinary nature, the development of data science code is subject to a wide range of potential mistakes that can easily compromise the final results. Several tools have been proposed that can help the data scientist in identi- fying the most common, low level programming issues. We discuss the steps needed to implement a tool that is rather meant to focus on higher level errors that are specific of the data science pipeline. To this end, we propose a static analysis assigning ad hoc abstract datatypes to the program variables, which are then checked for consistency when call- ing functions defined in data science libraries. By adopting a descriptive (rather than prescriptive) abstract type system, we obtain a linter tool reporting data science related code smells. While being still work in progress, the current proto- type is able to identify and report the code smells contained in several examples of questionable data science code.

@inproceedings{DBLP:conf/ftfjp/ArceriMDNOZ24, author = {Vincenzo Arceri and Saverio Mattia Merenda and Greta Dolcetti and Luca Negrini and Luca Olivieri and Enea Zaffanella}, editor = {Luca Di Stefano}, title = {Towards a Sound Construction of {EVM} Bytecode Control-Flow Graphs}, booktitle = {Proceedings of the 26th {ACM} International Workshop on Formal Techniques for Java-like Programs, FTfJP 2024, Vienna, Austria, 20 September 2024}, pages = {11--16}, publisher = {{ACM}}, year = {2024}, url = {https://doi.org/10.1145/3678721.3686227}, doi = {10.1145/3678721.3686227}, timestamp = {Tue, 22 Oct 2024 21:07:21 +0200}, biburl = {https://dblp.org/rec/conf/ftfjp/ArceriMDNOZ24.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }

Ethereum enables the creation and execution of decentralized applications through smart contracts, that are compiled to Ethereum Virtual Machine (EVM) bytecode. Once deployed in the blockchain, the bytecode is immutable; hence, ensuring that smart contracts are bug-free before their deployment is of utmost importance. A crucial preliminary step for any effective static analysis of EVM bytecode is the extraction of the control-flow graph (CFG): this presents significant challenges due to dynamically computed jump destinations. In this paper we present a novel approach, based on abstract intepretation, aiming at building a sound CFG from EVM bytecode smart contracts. Our analysis, which is implemented in our static analyzer EVMLiSA, is based on a parametric abstract domain that approximates concrete execution stacks at each program point as a $l$-sized set of abstract stacks of maximal height $h$; the results of the analysis are then used to resolve the jump destinations at jump nodes. On our preliminary experiments, by fine-tuning the analysis parameters, EVMLiSA achives sound CFGs for all smart contracts where permantent storage-related opcodes do not influence jump destinations.

@article{DBLP:journals/sttt/ArceriDZ24, author = {Vincenzo Arceri and Greta Dolcetti and Enea Zaffanella}, title = {Speeding up static analysis with the split operator}, journal = {Int. J. Softw. Tools Technol. Transf.}, volume = {26}, number = {5}, pages = {573--588}, year = {2024}, url = {https://doi.org/10.1007/s10009-024-00761-2}, doi = {10.1007/S10009-024-00761-2}, timestamp = {Mon, 07 Oct 2024 22:58:44 +0200}, biburl = {https://dblp.org/rec/journals/sttt/ArceriDZ24.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }

In the context of abstract interpretation-based static analysis, we propose a new abstract operator modeling the split of control flow paths: the goal of the operator is to enable a more efficient analysis when using abstract domains that are computationally expensive, having no negative effect on precision, and occasionally resulting in a more precise analysis. We focus on the case of conditional branches guarded by numeric linear constraints, including implicit numerical branches. We provide an experimental evaluation of real-world test cases, showing that by using the split operator we can achieve significant efficiency improvements with respect to the classical approach for a static analysis based on the domain of convex polyhedra. We also briefly discuss the applicability of this new operator to different, possibly non-numeric abstract domains.

@inproceedings{DBLP:conf/pldi/ArceriDZ23, author = {Vincenzo Arceri and Greta Dolcetti and Enea Zaffanella}, editor = {Pietro Ferrara and Liana Hadarean}, title = {Speeding up Static Analysis with the Split Operator}, booktitle = {Proceedings of the 12th {ACM} {SIGPLAN} International Workshop on the State Of the Art in Program Analysis, {SOAP} 2023, Orlando, FL, USA, 17 June 2023}, pages = {14--19}, publisher = {{ACM}}, year = {2023}, url = {https://doi.org/10.1145/3589250.3596141}, doi = {10.1145/3589250.3596141}, timestamp = {Sun, 12 Nov 2023 02:12:56 +0100}, biburl = {https://dblp.org/rec/conf/pldi/ArceriDZ23.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }

In the context of static analysis based on Abstract Interpretation, we propose a new abstract operator modeling the split of control flow paths: the goal of the operator is to enable a more efficient analysis when using abstract domains that are computationally expensive, having no effect on precision. Focusing on the case of conditional branches guarded by numeric linear constraints, we provide a preliminary experimental evaluation showing that, by using the split operator, we can achieve significant efficiency improvements for a static analysis based on the domain of convex polyhedra. We also briefly discuss the applicability of this new operator to different, possibly non-numeric abstract domains.

@inproceedings{DBLP:conf/sas/ArceriDZ23, author = {Vincenzo Arceri and Greta Dolcetti and Enea Zaffanella}, editor = {Manuel V. Hermenegildo and Jos{\'{e}} F. Morales}, title = {Unconstrained Variable Oracles for Faster Numeric Static Analyses}, booktitle = {Static Analysis - 30th International Symposium, {SAS} 2023, Cascais, Portugal, October 22-24, 2023, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {14284}, pages = {65--83}, publisher = {Springer}, year = {2023}, url = {https://doi.org/10.1007/978-3-031-44245-2\_5}, doi = {10.1007/978-3-031-44245-2\_5}, timestamp = {Thu, 09 Nov 2023 21:13:04 +0100}, biburl = {https://dblp.org/rec/conf/sas/ArceriDZ23.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }

In the context of static analysis based on Abstract Interpretation, we propose a lightweight pre-analysis step which is meant to suggest, at each program point, which program variables are likely to be unconstrained for a specific class of numeric abstract properties. Using the outcome of this pre-analysis as an oracle, we simplify the statements of the program being analyzed by propagating this lack of information, aiming at fine-tuning the precision/efficiency trade-off of the analysis. A preliminary experimental evaluation shows that the idea underlying the approach is promising, as it improves the efficiency of the more costly analysis while having a limited effect on its precision.

@Article{molecules28207082, AUTHOR = {Cozzini, Pietro and Agosta, Federica and Dolcetti, Greta and Dal Palù, Alessandro}, TITLE = {A Computational Workflow to Predict Biological Target Mutations: The Spike Glycoprotein Case Study}, JOURNAL = {Molecules}, VOLUME = {28}, YEAR = {2023}, NUMBER = {20}, ARTICLE-NUMBER = {7082}, URL = {https://www.mdpi.com/1420-3049/28/20/7082}, PubMedID = {37894561}, ISSN = {1420-3049}, DOI = {10.3390/molecules28207082} }

The biological target identification process, a pivotal phase in the drug discovery workflow, becomes particularly challenging when mutations affect proteins’ mechanisms of action. COVID-19 Spike glycoprotein mutations are known to modify the affinity toward the human angiotensin-converting enzyme ACE2 and several antibodies, compromising their neutralizing effect. Predicting new possible mutations would be an efficient way to develop specific and efficacious drugs, vaccines, and antibodies. In this work, we developed and applied a computational procedure, combining constrained logic programming and careful structural analysis based on the Structural Activity Relationship (SAR) approach, to predict and determine the structure and behavior of new future mutants. “Mutations rules” that would track statistical and functional types of substitutions for each residue or combination of residues were extracted from the GISAID database and used to define constraints for our software, having control of the process step by step. A careful molecular dynamics analysis of the predicted mutated structures was carried out after an energy evaluation of the intermolecular and intramolecular interactions using the HINT (Hydrophatic INTeraction) force field. Our approach successfully predicted, among others, known Spike mutants.

@article{cozzini2022blockchain, title={How a Blockchain Approach Can Improve Data Reliability in the COVID-19 Pandemic}, author={Cozzini, Pietro and Agosta, Federica and Dolcetti, Greta and Righi, Gianfranco}, journal={ACS Medicinal Chemistry Letters}, volume={13}, number={4}, pages={517--519}, year={2022}, publisher={ACS Publications} }

The rapid spread of COVID-19 made it necessary to quickly collect and share viral genomic sequences, sometimes making quantity prevail over the quality of information. Can research pay this price? Blockchain technology, based on the concept of a ledger that guarantees the authenticity and traceability of information, could be the best applicable solution.