"The scientist is not the man who provides the right answers; It is the one that poses the right questions."
Claude Lévi-Strauss
Official department list of papers
Isabella's DBLP
Papers submitted for publication
➡
Papers
2019
➡ I. Mastroeni and M. Pasqua. Statically Analyzing Information Flows - An Abstract Interpretation-based Hyperanalysis for Non-Interference. In 34th Symposium on Applied Computing - Software and Verification Track (SAC - SVT). ACM (to appear).
✴ Available: PDF.
2018
➡ V. Arceri and I. Mastroeni. An Automata-based Abstract Semantics for String Manipulation Languages. CoRR abs/1808.07827 (2018).
✴ Available: PDF.
➡ I. Mastroeni and M. Pasqua. Verifying Bounded Subset-Closed Hyperproperties. In 25th Static Analysis Symposium. LNCS 11002. Springer.
✴ Available: PDF.
➡ M. Dalla Preda and I. Mastroeni . Characterizing A Property-Driven Obfuscation Strategy. In Journal of Computer Security. 26(1) pp. 31-69, 2018. IOS Press.
✴ Available: PDF.
➡ S. Buro and I. Mastroeni. Abstract Code Injection: A Semantic Approach Based on Abstract Non-Interference. In Proc. of the 9th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'18). LNCS 10747, Springer 2018. ISBN 978-3-319-73720-1
✴ Available: PDF.
➡ R. Giacobazzi, I. Mastroeni. Abstract Non-Interference: A unifying framework for weakening information flow. In ACM Transactions on Privacy and Security. Accepted for publication. ACM. December 2018.
✴ Available: PDF.
2017
➡ V. Arceri, M. Dalla Preda, R. Giacobazzi and I. Mastroeni. SEA: String Executability Analysis by Abstract Interpretation. CoRR abs/1702.02406 (2017).
✴ Available: PDF.
➡ I. Mastroeni and M. Pasqua. On topologies for (hyper)properties. In 18th Italian Conference on Theoretical Computer Science.
✴ Available: PDF.
➡ I. Mastroeni and M. Pasqua. Hyperhierarchy of Semantics - A formal framework for Hyperproperties Verification. In 24th Static Analysis Symposium. LNCS 10422. Springer.
✴ Available: PDF.
➡ R. Giacobazzi, I. Mastroeni and M. Dalla Preda. Maximal Incompleteness as Obfuscation Potency. In Formal Aspects of Computing. 29(1). pages 3-31. Springer.
✴ Available: PDF.
➡ I. Mastroeni and D. Zanardini. Abstract Program Slicing: an Abstract Interpretation-based approach to Program Slicing. In ACM Transactions on Computational Logic (TOCL). 18(1) pages 7:1-7:58. ACM.
✴ Available: PDF.
2016
➡ R. Sartea, M. Dalla Preda, A. Farinelli, R. Giacobazzi and I. Mastroeni. Active Android Malware Analysis: An approach based on stochastic Games. In Software Security, Protection and Reverse Engineering Workshop (SS-PPREW). ACM. Los Angeles, California. 2016.
✴ Available: PDF.
➡ M. Dalla Preda, R. Giacobazzi and I. Mastroeni. Completeness in approximate transduction . In 23rd Static Analysis Symposium. LNCS 9837. pp. 126-146. Springer
✴ Available: PDF.
➡ I. Mastroeni and R. Giacobazzi. Weakening residuation in adjoining closures. In Order. 33(3) pages 503-516. Springer, November 2016.
✴ Available: PDF.
➡ R. Giacobazzi, I. Mastroeni. Making abstract models complete. In Mathematical Structures in Computer Science. 26(4) pages 658 -701. Cambridge University Press. May 2016
✴ Available: PDF.
2015
➡ F. Bellini, R. Chiodi and I. Mastroeni. MIME: A Formal Approach to (Android) Emulation Malware Analysis. In 8th International Symposium on Foundation & Practice of Security (FPS’15). Springer LNCS 9482.Clermont-Ferrand, France, 26-28 October 2015.
✴ Available: PDF.
➡ F. Bellini, R. Chiodi and I. Mastroeni. MIME: A Formal Approach for Multiple Investigation in (Android) Malware Emulation Analysis. Technical Report RR 97/2015. Department of Computer science, University of Verona, August 2015.
✴ Available: PDF.
➡ I. Mastroeni and R. Giacobazzi. Weakening residuation in adjoining closures. Technical Report RR 95/2015. Department of Computer science, University of Verona, April 2015.
✴ Available: PDF.
➡ M. Dalla Preda, I. Mastroeni. Infections as Abstract Symbolic Finite Automata: Forma Model and Applications. In 1st International Workshop on Software PROtection (SPRO’15). IEEE. Firenze, Italia. May 19, 2015.
✴ Available: PDF.
➡ M. Dalla Preda, R. Giacobazzi, A. Lakhotia, I. Mastroeni. Abstract Symbolic Automata - Mixed syntactic/semantic similarity analysis of executables. In ACM SIGPLAN Notices. 50(1) pages 329 - 341. ACM press. , 2015.
✴ Available: PDF.
➡ M. Dalla Preda, R. Giacobazzi, A. Lakhotia, I. Mastroeni. Abstract Symbolic Automata - Mixed syntactic/semantic similarity analysis of executables. In 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'15), pages 329 - 341. ACM press. Mumbai, India, January 12-18, 2015.
✴ Available: PDF.
2014
➡ M. Dalla Preda, I. Mastroeni, R. Giacobazzi. Analyzing Program Dependencies for Malware Detection. In proc. of 3rd ACM SIGPLAN Program Protection and Reverse Engineering Workshop. PPREW 2014. January 25, 2014.
✴ Available: PDF.
2013
➡ I. Mastroeni. Abstract interpretation-based approaches to Security - A survey on Abstract non-Interference and its challenging application. In proc. of Semantics, Abstract Interpretation, and Reasoning about Programs. EPTCS. September 19 - 20, 2013.
✴ Available: PDF.
➡ M. Dalla Preda, I. Mastroeni and R. Giacobazzi. Formal Framework for Property-driven Obfuscations. In proc. of the 19th Intern. Symp. on Fundamentals of Computer Theory, FCT 2013, LNCS. Liverpool, UK. August 19 -21, 2013.
✴ Available: PDF.
➡ M. Dalla Preda, I. Mastroeni. Chasing infections by unveiling program dependencies. In Proc. of the 1st Workshop in Interferences and Dependencies (ID’13). Rome, Italy, 21 January 2013.
✴ Available: PDF.
➡ R. Giacobazzi, J. Berdine and I. Mastroeni (Eds). Verification, Model Checking, and Abstract Interpretation, 14th International Conference, VMCAI 2013, Rome, Italy, January 20-22, 2013. Proceedings. Lecture Notes in Computer Science 7737, Springer 2013, isbn 978-3-642-35872-2
2012
➡ R. Giacobazzi, I. Mastroeni. Making abstract interpretation incomplete - Modeling the potency of obfuscation. In Proc. of the 19th International Static Analysis Symp. (SAS ’12), LNCS 7460 pages 129 - 145. Springer. Deauville, France, 11-13 September 2012.
✴ Available: PDF.
➡ R. Giacobazzi, I. Mastroeni and D. Nikolic. Strong Preservation by Model Deformation. In Proc. of the Sixth IEEE International Symposium on Theoretical Aspects of Software Engineering Conference (TASE '12), pages 33 - 40. IEEE Computer Society Press. Beijing, China, 4-6 July 2012.
✴ Available: PDF.
➡ R. Giacobazzi, N. Jones and I. Mastroeni. Obfuscation by Partial Evaluation of Distorted Interpretation. In Proc. of the ACM SIGPLAN 2012 Symp. on Partial Evaluation and Program Manipulation (PEPM '12), pages 63 - 72. ACM press. Philadelphia, Pennsylvania, USA, January 23-24, 2012.
✴ Available: PDF.
2011
➡ I. Mastroeni and A. Banerjee. Modeling Declassification Policies using Abstract Domain Completeness. Special issue of "Mathematical Structures in Computer Science" on Programming Language Interference and Dependence, 21(6): 1253-1299, 2011.
✴ Available: PDF.
➡ I. Mastroeni. and R. Giacobazzi. An Abstract Interpretation-based Model for Safety Semantics. Journal of Computer Mathematics, 88(4): 665-694, 2011.
✴ Available: PDF.
2010
➡ M. Balliu and I. Mastroeni. A Weakest Precondition Approach to Robustness. Transactions on Computational Science 10: 261-297 (2010).
✴ Available: PDF.
➡ I. Mastroeni and D. Nikolic. Abstract Program Slicing: From theory towards an implementation. In Proc. of the 12th International Conference on Formal Engineering Methods (ICFEM'10). Volume 6447 of Lecture Notes in Computer Science, pages 452 - 467. Springer. Nov 16 - 19, 2010, Shanghai, China.
✴ Available: PDF.
➡ R. Giacobazzi and I. Mastroeni. Adjoining classified and unclassified information by Abstract Interpretation. Journal of Computer Security, 18(5): 751-797, 2010.
✴ Available: PDF.
➡ R. Giacobazzi and I. Mastroeni. A Proof System for Abstract Non-Interference. Journal of Logic and Computation, 20: 449-479. 2010.
✴ Available: PDF.
2009
➡ M. Balliu and I. Mastroeni. A weakest precondition approach to active attacks analysis. In the Proc.of ACM SIGPLAN Programming Languages and Analysis for Security (PLAS '09). pages 59-71, ACM press. Dublin,
Ireland. June 15, 2009.
✴ Available: PDF, Slides.
➡R. Giacobazzi and I. Mastroeni. An Abstract Interpretation-based Model for Safety Semantics. Technical Report RR 72/2009. Department of Computer science, University of Verona, May 2009.
✴ Available: PDF.
2008
➡ R. Giacobazzi and I. Mastroeni. Adjoining classified and unclassified information by Abstract Interpretation. Technical Report RR 63/2008. Department of Computer science, University of Verona, May 2008.
✴ Available: PDF.
➡ R. Giacobazzi and I. Mastroeni. A Proof System for Abstract Non-Interference. Technical Report RR 62/2008. Department of Computer science, University of Verona, May 2008.
✴ Available: PDF.
➡ I. Mastroeni and A. Banerjee. Modeling Declassification Policies using Abstract Domain Completeness. Technical Report RR 61/2008. Department of Computer science, University of Verona, May 2008..
✴ Available: PDF.
➡ R. Giacobazzi and I. Mastroeni. Abstract Non-Interference. Technical Report RR 60/2008. Department of Computer science, University of Verona, May 2008.
✴ Available: PDF.
➡ R. Giacobazzi and I. Mastroeni. Transforming Abstract Interpretations by Abstract Interpretation New Challenges in Language-based Security. Invited paper in the Proc.of the 15th International Static Analysis Symposium (SAS '08). Volume 5079 of Lecture Notes in Computer Science, pages 1 - 17. Springer. Valencia, Spain. July 16-18, 2008.
✴ Available: PDF, Slides.
➡ I. Mastroeni and D. Zanardini. Data dependencies and program slicing: From syntax to abstract semantics. In Proc. of the ACM SIGPLAN 2008 Symp. on Partial Evaluation and Program Manipulation (PEPM '08), pages 125 - 134. ACM press. San Francisco, CA, USA. January 7-8, 2008.
✴ Available: PDF, Slides.
➡ I. Mastroeni. Deriving Bisimulations by Simplifying Partitions. In Proc. of the Ninth International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'08). Volume 4905 of Lecture Notes in Computer Science, pages 157 - 171, Springer-Verlag. January 7-9, 2008 San Francisco, CA, USA.
✴ Available: PDF, Slides.
2007
➡ A. Banerjee, R. Giacobazzi and I. Mastroeni. What you lose is what you leak: Information Leakage in Declassification Policies . Twenty-third Conference on the Mathematical Foundations of Programming Semantics (MFPS'07).Tulane University New Orleans, LA USA April 11 - April 14, 2007
✴ Available: PDF, Slides.
2006
➡ I. Mastroeni and R. Rossato. Weakening Non-Interference on Databases (abstract). Workshop on Current and Emerging Research Issues in Computer Security (CERICS'06). July 20-21, 2006 Royal Holloway, University of London.
✴ Available: PDF, Slides.
2005
➡ I. Mastroeni. On the role of Abstract Non-Interference in language-based security. In The Third Asian Symposium on Programming Languages and Systems (APLAS'05). Volume 3780 of Lecture Notes in Computer Science, pages 418-433, Springer-Verlag. November 3-5, 2005 Tsukuba, Japan.
✴ Available: PDF, Slides.
➡ R. Giacobazzi and I. Mastroeni. Timed Abstract Non-Interference. In The International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS'05). Volume 3829 of Lecture Notes in Computer Science, pages 289-303, Springer-Verlag. September 26-28, 2005, Uppsala, Sweden.
✴ Available: PDF, Slides.
➡ R. Giacobazzi and I. Mastroeni. Generalized Abstract Non-Interference - Abstract Secure Information-flow Analysis for Automata. In The Third International Workshop "Mathematical Methods, Models and Architectures for Computer Networks Security" (MMM-ACNS'05). Volume 3685 of Lecture Notes in Computer Science, pages 221-234, Springer-Verlag. September 24-28, 2005, St. Petersburg, Russia.
✴ Available: PDF, Slides.
➡ S. Hunt and I. Mastroeni. The PER model of Abstract Non-Interference. In The 12th International Static Analysis Symposium (SAS'05). Volume 3672 of Lecture Notes in Computer Science, pages 171-185, Springer-Verlag. September 7-9, 2005. London, UK.
✴ Available: PDF, Slides.
➡ R. Giacobazzi and I. Mastroeni. Transforming Semantics by Abstract Interpretation. In Theoretical Computer Science (TCS), pages 1-50, Volume 337, Issue 1-3, June 2005.
✴ Available: PDF.
➡ R. Giacobazzi and I. Mastroeni. Adjoining Declassification and Attack Models by Abstract Interpretation. In the European Symposium on Programming (ESOP'05). Volume 3444 of Lecture Notes in Computer Science, pages 295-310, Springer-Verlag. Edinburgh, Scotland, April 2-10, 2005
✴ Available: PDF, Slides.
2004
➡ I. Mastroeni. Algebraic Power Analysis by Abstract Interpretation. In Higher-Order and Symbolic Computation (HOSC), Volume 17(4), pages 299-347. December 2004.
✴ Available: PDF.
➡ R. Giacobazzi and I. Mastroeni. Proving abstract non-interference. In the Annual Conference of the European Association for Computer Science Logic (CSL'04). Volume 3210 of Lecture Notes in Computer Science, pages 280-294, Springer-Verlag. Karpacz, September 20-24, 2004.
✴ Available: PDF, Slides.
➡ S. Genaim, R. Giacobazzi and I. Mastroeni. Modeling Information Flow Dependencies with Boolean Functions. In the 2004 IFIP WG 1.7, ACM SIGPLAN and GI FoMSESS Workshop on Issues in the Theory of Security (WITS'04). April 3 - 4, 2004, Barcelona, Spain.
✴ Available: PDF.
➡ R. Giacobazzi and I. Mastroeni. Abstract Non-Interference: Parameterizing Non-Interference by Abstract Interpretation. In 31st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'04), pages 186-197. ACM press. Venice, Italy, January 14-16, 2004.
✴ Available: PDF, Slides.
2003
➡ R. Giacobazzi and I. Mastroeni. Non-standard semantics for program slicing. In Higher-Order and Symbolic Computation (HOSC). Special issue on Partial Evaluation and Semantics-Based Program Manipulation. Volume 16(4), pages 297-339. December 2003.
✴ Available: PDF.
➡ R. Giacobazzi and I. Mastroeni. Domain Compression for Complete Abstractions. In Fourth International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'03), volume 2575 of Lecture Notes in Computer Science, pages 146-160, Springer-Verlag. New York University, New York, January 9-11, 2003.
✴ Available: PDF, Slides.
2002
➡ R. Giacobazzi and I. Mastroeni. Compositionality in the puzzle of semantics. In Proc. of the ACM SIGPLAN Symp. on Partial Evaluation and Semantics-Based Program Manipulation (PEPM'02), pages 87-97. ACM press. Portland, Oregon, USA, January 14-15, 2002.
✴ Available: PDF.
2001
➡ I. Mastroeni. Numerical Power Analysis. In Proc. of the 2nd Symposium on Programs as Data Objects (PADO'01), volume 2053 of Lecture Notes in Computer Science , pages 117-137. Springer-Verlag. Aarhus, Denmark, May 21-23, 2001.
✴ Available: PDF.
2000
➡ R. Giacobazzi and I. Mastroeni. Designing semantics by domain complementation. Joint conference on Declarative Programming (AGP'00), La Habana, Cuba, December 4-6, 2000.
✴ Available: PDF.
➡ R. Giacobazzi and I. Mastroeni. A characterization of symmetric semantics by domain complementation. In Proc. of the 2nd ACM International Conference on Principles and Practice of Declarative Programming (PPDP'00), pages 115-126. ACM Press. Montreal, Canada, September 20-22, 2000.
✴ Available: PDF.
Copyright Notice
The documents distributed have been provided by the contributing authors as a means to ensure timely dissemination of technical work on a noncommercial basis. Copyright and all rights therein are maintained by the authors or by other copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.
Book
I. Mastroeni. and C. Priami. Semantica operazionale: Strumenti e Applicazioni (Linguaggi Imperativi e Funzionali), CEDAM, ISBN 88-13-22138-X, 1999, Padova.