I am an Assistant Professor within the SysMA research unit, as well as a member of the European Project QUANTICOL. Before that, I was a Senior Research Assistant at the School of Electronics and Computer Science of Southampton University, United Kingdom, and a Teaching Assistant at Leicester University, United Kingdom.
I received my PhD in Computer Science and Engineering, as well as the "Doctoral Europeaus" certification from IMT School for Advanced Studies Lucca, Italy, in 2013. I graduated in Computer Science at the University of Pisa, Italy.
I am interested in the development of scalable techniques for the formal qualitative and quantitative system analysis, including state space reduction and approximation. Currently, I am investigating analysis techniques for languages provided with formal semantics based on ordinary differential equations (ODEs) or continuous time Markov chains (CTMC). These include chemical reaction networks, stochastic process algebras, and Petri nets.
I am interested in applying my research in practice, and hence I provided tool support for most of my contributions. An example is ERODE
, a fully-featured tool for the Evaluation and Reduction of ODEs, which obtained the POPL'16 Artifact Evaluation Certificate
, and will be presented at TACAS'17
Furthermore, I am also investigating statistical analysis techniques, and I developed the Statistical Model Checker MultiVeStA
, which allows to easily enrich existing discrete-event simulators with distributed statistical analysis capabilities.
Syntactic Markovian Bisimulation for Chemical Reaction Networks, Luca Cardelli, Mirco Tribastone, Max Tschaikowski, Andrea Vandin, proceedings of Kim Larsen Festschrift (KimFest'17) Springer LNCS [draft];
Statistical Model Checking for Product Lines, Maurice ter Beek, Axel Legay, Alberto Lluch Lafuente, Andrea Vandin, proceedings of the 7th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISOLA'16) Springer LNCS [draft];
A Tool-chain for Statistical Spatio-Temporal Model Checking of Bike Sharing Systems, Vincenzo Ciancia, Diego Latella, Mieke Massink, Rytis Paskauskas, Andrea Vandin, proceedings of the 7th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISOLA'16) Springer LNCS [draft];
- Quantitative Analysis of Probabilistic Models of Software Product Lines with Statistical Model Checking, Maurice ter Beek, Axel Legay, Alberto Lluch Lafuente, Andrea Vandin, 6th Workshop on Formal Methods and Analysis in SPL Engineering (FMSPLE'15) EPTCS, 2015 [draft]
- Reasoning (on) Service Component Ensembles in Rewriting Logic, Lenz Belzner, Rocco De Nicola, Andrea Vandin, Martin Wirsing, Symposium on Specification, Algebra and Software (SAS'14), Springer LNCS Festschrift [draft]
- Adaptable Transition Systems, Roberto Bruni, Andrea Corradini, Fabio Gadducci, Alberto Lluch Lafuente, Andrea Vandin, 21st International Workshop on Algebraic Development Techniques (WADT'12), Springer LNCS [draft]
- Modeling and Analyzing Adaptive Self-assembling Strategies with Maude, Roberto Bruni, Andrea Corradini, Fabio Gadducci, Alberto Lluch Lafuente, Andrea Vandin, 9th International Workshop on Rewriting Logic and its Applications (WRLA'12), Springer LNCS, volume 7571, 2012 [draft]
- Towards a Maude Tool for Model Checking Temporal Graph Properties, Alberto Lluch Lafuente, Andrea Vandin, 10th International Workshop on Graph Transformation and Visual Modeling Techniques (GT-VMT'11), ECEAAST(41), 2011 [abstract] [pdf] [draft] [bib]