Research lab · University of Udine
We design, verify, test and secure the autonomous systems the world is starting to rely on.
What we do
Modern systems are increasingly decentralised and autonomous, and more and more often rely on AI-based agents, such as those built on large language models. They must guarantee continuous service, tolerate faults, adapt to change and resist attacks. MADS develops methods and tools to build such systems correctly, test them thoroughly and keep them secure.
Finding failures before users do: automated test generation and quality assurance for complex software, AI-based and autonomous systems.
Breaking and fixing real systems: security of protocols, networks and industrial devices, from formal verification to hands-on vulnerability research.
Correct by construction: choreographic languages, types and formal models for coordinating fleets of autonomous, distributed agents.
News & events
The paper Reliable Decision Loops in Socio-Technical Collective Adaptive Systems, by Marino Miculan, has been published in the proceedings of ISoLA 2026: a formal framework for systems where...
Read moreThe paper KLAIM, Certified: Mechanising Flow Logic for Tuple-Space Coordination, by Marino Miculan, has been published (open access) in the Journal of Logical and Algebraic Methods in Programming...
Read moreFrom September 7th to 9th Udine hosted ICTCS 2026, the Italian Conference on Theoretical Computer Science, where we presented our paper Policy Automata for Stateful Authorization, by Massimiliano...
Read moreRecent publications
Our work appears in top venues in software engineering, security and theoretical computer science.
Browse all 109 publicationsLeveraging Applications of Formal Methods, Verification and Validation. Rigorous Engineering of Collective Adaptive Systems (ISoLA 2026), Lecture Notes in Computer Science 17141, pp. 71–88 · Springer · 2026
@InProceedings{m:isola26,
month = {October},
groups = {choreographies},
author = {Miculan, Marino},
editor = {Margaria, Tiziana and Steffen, Bernhard},
title = {Reliable Decision Loops in Socio-Technical Collective Adaptive Systems},
booktitle = {Leveraging Applications of Formal Methods, Verification and Validation. Rigorous Engineering of Collective Adaptive Systems (ISoLA 2026)},
series = {Lecture Notes in Computer Science},
volume = {17141},
publisher = {Springer},
year = {2026},
pages = {71--88},
doi = {10.1007/978-3-032-40108-3_5}
}Journal of Logical and Algebraic Methods in Programming, pp. 101179 · 2026
@Article{m:jlamp26,
month = {September},
groups = {choreographies},
author = {Miculan, Marino},
title = {{KLAIM}, Certified: Mechanising Flow Logic for Tuple-Space Coordination},
journal = {Journal of Logical and Algebraic Methods in Programming},
year = {2026},
pages = {101179},
doi = {10.1016/j.jlamp.2026.101179},
html = {https://doi.org/10.1016/j.jlamp.2026.101179},
code = {https://zenodo.org/records/22171485},
issn = {2352-2208},
selected = true,
}Proceedings of the 27th Italian Conference on Theoretical Computer Science (ICTCS 2026), CEUR Workshop Proceedings 4269 · CEUR-WS.org · 2026
@inproceedings{bpm:ictcs26,
month = {September},
groups = {cybersecurity},
author = {Baldo, Massimiliano and Paier, Matteo and Miculan, Marino},
title = {Policy Automata for Stateful Authorization},
booktitle = {Proceedings of the 27th Italian Conference on Theoretical Computer Science (ICTCS 2026)},
location = {Udine, Italy, September 07-09, 2026},
series = {{CEUR} Workshop Proceedings},
volume = 4269,
publisher = {CEUR-WS.org},
year = 2026,
pdf = {https://ceur-ws.org/Vol-4269/paper45.pdf},
html = {https://ceur-ws.org/Vol-4269}
}Science of Computer Programming 253, pp. 103502 · 2026
@article{vr:maryam2026giftbenc,
groups = {testing},
title = {GIFTbench: Generative Image Fuzz Testing Benchmark},
volume = {253},
doi = {10.1016/j.scico.2026.103502},
journal = {Science of Computer Programming},
publisher = {Elsevier BV},
author = {Maryam, Maryam and Biagiola, Matteo and Stocco, Andrea and Riccio, Vincenzo},
year = {2026},
month = {August},
pages = {103502},
pdf = {https://p1ndsvin.github.io/assets/pdf/scp_giftbench.pdf}
}Empirical Software Engineering 32(1) · 2026
@article{vr:klikovits2026does,
groups = {testing},
title = {Does Road Diversity Really Matter in Testing Automated Driving Systems?},
volume = {32},
doi = {10.1007/s10664-026-10920-5},
number = {1},
journal = {Empirical Software Engineering},
publisher = {Springer Science and Business Media LLC},
author = {Klikovits, Stefan and Riccio, Vincenzo and Castellano, Ezequiel and Cetinkaya, Ahmet and Gambi, Alessio and Arcaini, Paolo},
year = {2026},
month = {July},
pdf = {https://p1ndsvin.github.io/assets/pdf/EMSE2026.pdf}
}Our research is funded by and carried out with