Pubblications

Selected Works

DeepREST: Automated Test Case Generation for REST APIs Exploiting Deep Reinforcement Learning
Corradini D., Montolli Z., Pasqua M., and Ceccato M.

PDF file $\TeX$ ref

In: Proceedings of the 39^th IEEE/ACM International Conference on Automated Software Engineering (pp. 1383–1394), ACM, 2024, DOI: 10.1145/3691620.3695511

REST API · Deep Reinforcement Learning · Automated software testing · OpenAPI

Behavioral Equivalences for AbU: Verifying Security and Safety in Distributed IoT Systems
Pasqua M. and Miculan M.

PDF file $\TeX$ ref

In: Theoretical Computer Science (pp. 1–23), Elsevier, 2024, DOI: 10.1016/j.tcs.2024.114537

ECA rules · Distributed systems · Bisimulations · Edge computing · IoT Security

Hypertesting of Programs: Theoretical Foundation and Automated Test Generation
Pasqua M., Ceccato M. and Tonella P.

PDF file $\TeX$ ref

In: Proceedings of the 46^th IEEE/ACM International Conference on Software Engineering (pp. 1409–1420), ACM, 2024 DOI: 10.1145/3597503.3640323

Hyperproperties · Security testing · Information flows · Automated software testing

Domain Precision in Galois Connection-less Abstract Interpretation
Mastroeni I. and Pasqua M.

PDF file $\TeX$ ref

In: Proceedings of the 30^th Static Analysis International Symposium (pp. 434–459), Springer Nature Switzerland, 2023, DOI: 10.1007/978-3-031-44245-2_19

Abstract interpretation · Completeness · Static program analysis

Enhancing REST API Testing with NLP Techniques
Kim M., Corradini D., Sinha S., Orso A., Pasqua M., Tzoref-Brill R. and Ceccato M.

PDF file $\TeX$ ref

In: Proceedings of the 32^nd ACM International Symposium on Software Testing and Analysis (pp. 1232–1243), ACM, 2023, DOI: 10.1145/3597926.3598131

REST API · NLP · OpenAPI specification · Automated software testing

Automated Black-box Testing of Mass Assignment Vulnerabilities in RESTful APIs
Corradini D., Pasqua M. and Ceccato M.

PDF file $\TeX$ ref

In: Proceedings of the 45^th IEEE/ACM International Conference on Software Engineering (pp. 2553–2564), IEEE, 2023, DOI: 10.1109/ICSE48619.2023.00213

REST API · Security testing · Mass assignment · Automated software testing

AbU: A Calculus for Distributed Event-driven Programming with Attribute-based Interaction
Pasqua M. and Miculan M.

PDF file $\TeX$ ref

In: Theoretical Computer Science (pp. 1–32), Elsevier, 2023, DOI: 10.1016/j.tcs.2023.113841

ECA rules · Distributed systems · Formal methods · Edge computing · IoT programming

Enhancing Ethereum smart-contracts static analysis by computing a precise Control-Flow Graph of Ethereum bytecode
Pasqua M., Benini A., Contro F., Crosara M., Dalla Preda M. and Ceccato M.

PDF file $\TeX$ ref

In: Journal of Systems and Software (pp. 1–18), Elsevier, 2023, DOI: 10.1016/j.jss.2023.111653

Smart-contracts · Reverse engineering · Static analysis · Ethereum

Automated black‐box testing of nominal and error scenarios in RESTful APIs
Corradini, D., Zampieri A., Pasqua, M., Viglianisi E., Dallago M. and Ceccato, M.

PDF file $\TeX$ ref

In: Software Testing Verification and Reliability (pp. 1–33), John Wiley & Sons, 2022, DOI: 10.1002/stvr.1808

REST API · Black-box testing · Automated test case generation

A Calculus for Attribute-based Memory Updates
Miculan, M. and Pasqua, M.

PDF file $\TeX$ ref

In: Proceedings of the 18^th International Colloquium on Theoretical Aspects of Computing (pp. 366–385), Springer International Publishing, 2021, DOI: 10.1007/978-3-030-85315-0_21

ECA rules · Attribute-based communication · Distributed systems · Autonomic computing

Friendly Fire: Cross-App Interactions in IoT Platforms
Balliu, M., Merro, M., Pasqua, M. and Shcherbakov, M.

PDF file $\TeX$ ref

In: ACM Transactions on Privacy and Security (pp. 1–40), ACM, 2021, DOI: 10.1145/3444963

Cloud-based IoT platform · IoT application security · Cross-app interference

Statically Analyzing Information Flows
An Abstract Interpretation-based Hyperanalysis for Non-Interference
Mastroeni, I. and Pasqua, M.

PDF file $\TeX$ ref

In: Proceedings of the 34^th SIGAPP Symposium On Applied Computing (pp. 2215–2223), ACM, 2019, DOI: 10.1145/3297280.3297498

Static analysis · Abstract interpretation · Hyperproperties · Non-interference

An abstract domain for objects in dynamic programming languages
Arceri, V., Pasqua, M. and Mastroeni, I.

PDF file $\TeX$ ref

In: Proceedings of the Formal Methods 2019 International Workshops (pp. 136–151), Springer International Publishing, 2019, DOI: 10.1007/978-3-030-54997-8_9

Dynamic languages · Abstract interpretation · Objects · Automata domain

Semantics-based Software Watermarking by Abstract Interpretation
Dalla Preda, M. and Pasqua, M.

PDF file $\TeX$ ref

In: Mathematical Structures in Computer Science (pp. 339–388), Cambridge University Press, 2018, DOI: 10.1017/S0960129518000038

Software watermarking · Abstract interpretation · Completeness

Verifying Bounded Subset-Closed Hyperproperties
Mastroeni, I. and Pasqua, M.

PDF file $\TeX$ ref

In: Proceedings of the 25^th Static Analysis International Symposium (pp. 263–283), Springer International Publishing, 2018, DOI: 10.1007/978-3-319-99725-4_17

Hyperproperties · Collecting hypersemantics · Abstract interpretation · Verification

Hyperhierarchy of Semantics
A Formal Framework for Hyperproperties Verification
Mastroeni, I. and Pasqua, M.

PDF file $\TeX$ ref

In: Proceedings of the 24^th Static Analysis International Symposium (pp. 232–252), Springer International Publishing, 2017, DOI: 10.1007/978-3-319-66706-5_12

Hyperproperties · Abstract interpretation · Hypersemantics · Verification