Contact info
| Address | e-Services for Life and Health San Raffaele Scientific Institute DIBIT 2, San Gabriele building 2, 5th Floor Via Olgettina 60, 20132 - Milano, IT |
|---|---|
| Phone | +39 02 2643 3137 |
| surname.name@hsr.it | |
| GPG Key | 0x5BC15558 (fingerprint: 1B56 65F2 F1FE 132B 4F5A 26B9 6E09 D0F8 5BC1 5558) |
About myself
Since February, 2015, I am a researcher of the eServices for Life and Health unit of the Fondazione Centro San Raffaele.
On the 17th of February, 2015, I defended my PhD thesis titled "An SMT-based verification framework for software systems handling arrays" (available here).
From September, 2010 since January, 2015 I have been working as a Research Assistant in the Formal verification group of the Università della Svizzera Italiana led by Prof. Natasha Sharygina.
In 2014 I have been awarded a research fellowship from the SNSF (Doc.Mobility program) giving me the great opportunity of joining Prof. David Monniaux's group at Verimag for six months (from January to June, 2014).
In 2010 I have been working for three months (Jun - Aug) as a research intern at FBK in the "Security & Trust" unit led by Prof. Alessandro Armando.
I got my M.Sc. degree in Computer Science on April 26, 2010 from the Università degli Studi di Milano (University of Milan, Italy) with a thesis (available here in Italian language only) on the formal parameterized verification of fault-tolerant protocols.
I got my B.Sc. degree in Computer Science on October 25, 2007 from the Università degli Studi di Milano (University of Milan, Italy) with a thesis on the analysis of stop condition approaches for epidemic algorithms used in opportunistic networks.
On the 17th of February, 2015, I defended my PhD thesis titled "An SMT-based verification framework for software systems handling arrays" (available here).
From September, 2010 since January, 2015 I have been working as a Research Assistant in the Formal verification group of the Università della Svizzera Italiana led by Prof. Natasha Sharygina.
In 2014 I have been awarded a research fellowship from the SNSF (Doc.Mobility program) giving me the great opportunity of joining Prof. David Monniaux's group at Verimag for six months (from January to June, 2014).
In 2010 I have been working for three months (Jun - Aug) as a research intern at FBK in the "Security & Trust" unit led by Prof. Alessandro Armando.
I got my M.Sc. degree in Computer Science on April 26, 2010 from the Università degli Studi di Milano (University of Milan, Italy) with a thesis (available here in Italian language only) on the formal parameterized verification of fault-tolerant protocols.
I got my B.Sc. degree in Computer Science on October 25, 2007 from the Università degli Studi di Milano (University of Milan, Italy) with a thesis on the analysis of stop condition approaches for epidemic algorithms used in opportunistic networks.
Projects
-
WITDOM
empoWering prIvacy and securiTy in clouD envirOnMents. -
Booster
An abstraction and acceleration-based software model-checker for programs handling arrays. -
Automated Support for the Design and Validation of Parameterized Systems
Towards the application of infinite-state model checkers in the design and verification of fault-tolerant parameterized protocols. -
MCMT
A model checker for infinite-state systems based on the integration of Satisfiability Modulo Theories (SMT) solving and backward reachability.
Publications
| 20. |
"Decision Procedures for Flat Array Properties"
Francesco Alberti, Silvio Ghilardi, Natasha Sharygina
Journal of Automated Reasoning (JAR), vol. 54, p. 327-352, 2015
[Link]
|
|---|---|
| 19. |
"Polyhedra to the rescue of array interpolants"
Francesco Alberti, David Monniaux
30th ACM/SIGAPP Symposium On Applied Computing (SAC), Salamanca, Spain, April 13-17, 2015
|
| 18. |
"Monotonic Abstraction Techniques: from Parametric to Software Model Checking"
Francesco Alberti, Silvio Ghilardi, Natasha Sharygina
1st Workshop on Logics and Model-checking for Self-* Systems (MOD*), UITP 2014, Bertinoro, Italy, September 12, 2014
[Link]
|
| 17. |
"Booster: an acceleration-based verification framework for array programs"
Francesco Alberti, Silvio Ghilardi, Natasha Sharygina
12th International Symposium on Automated Technology for Verification and Analysis (ATVA), Sydney, Australia, November 3-7, 2014
[Link]
|
| 16. |
"VERIGE: VERification with Invariant Generation Engine"
Nicolas Latorre, Francesco Alberti, Natasha Sharygina
21st International Symposium on Model Checking of Software (SPIN), San Josè, California, USA, July 21-23, 2014
[Link]
|
| 15. |
"A framework for the verification of parameterized infinite-state systems"
Francesco Alberti, Silvio Ghilardi, Natasha Sharygina
29th Italian Conference on Computational Logic (CILC), Turin, Italy, June 16-18, 2014
[Link]
|
| 14. |
"An extension of Lazy Abstraction with Interpolation for programs with arrays"
Francesco Alberti, Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise, Natasha Sharygina
Formal Methods in System Design (FMSD), vol. 45, p. 63-109, 2014
[Link]
|
| 13. |
"A SMT-based verification framework for software systems handling unbounded arrays"
Francesco Alberti
Doctoral Symposium (co-located with FM), Singapore, May 13, 2014
|
| 12. |
"Decision Procedures for Flat Array Properties"
Francesco Alberti, Silvio Ghilardi, Natasha Sharygina
20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Grenoble, France, April 5-13, 2014
[Link]
[Slides]
|
| 11. |
"Acceleration-based Safety Decision Procedure for Programs with Arrays"
Francesco Alberti, Silvio Ghilardi, Natasha Sharygina
Short paper at the 19th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), Stellenbosh, South Africa, December 15-19, 2013.
[Link]
[Slides]
|
| 10. |
"Definability of Accelerated Relations in a Theory of Arrays and its Applications"
Francesco Alberti, Silvio Ghilardi, Natasha Sharygina
9th International Symposium on Frontiers of Combining Systems (FroCoS), Nancy, France, September 18-20, 2013.
[Link]
[Slides]
|
| 9. |
"SAFARI: SMT-based Abstraction For Arrays with Interpolants"
Francesco Alberti, Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise, Natasha Sharygina
24th International Conference on Computer Aided Verification (CAV), Berkeley, California, USA, July 7-13, 2012.
[Link]
|
| 8. |
"Invariant Generation by Infinite-State Model Checking"
Francesco Alberti, Natasha Sharygina
2nd International Workshop on Intermediate Verification Languages (BOOGIE), Berkeley, California, USA, July 8, 2012.
|
| 7. |
"Reachability Modulo Theory Library"
Francesco Alberti, Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise, Natasha Sharygina
10th International Workshop on Satisfiability Modulo Theories (SMT), Manchester, UK, June 30 - July 1, 2012.
[Link]
|
| 6. |
"Lazy Abstraction with Interpolants for Arrays"
Francesco Alberti, Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise, Natasha Sharygina
18th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), Mérida, Venezuela, March 10-15, 2012.
[Link]
[Slides]
|
| 5. |
"Universal guards, relativization of quantifiers, and failure models in model checking modulo theories"
Francesco Alberti, Silvio Ghilardi, Elena Pagani, Silvio Ranise, Gianpaolo Rossi
Journal on Satisfiability, Boolean Modeling and Computation (JSAT), vol. 8, p. 29-61, 2012
[Link]
|
| 4. |
"ASASP: Automated Symbolic Analysis of Security Policies"
Francesco Alberti, Alessandro Armando, Silvio Ranise
23rd International Conference on Automated Deduction (CADE), Wrocław, Poland, July 31 - August 5, 2011.
[Link]
|
| 3. |
"Efficient Symbolic Automated Analysis of Administrative Attribute-based RBAC-policies"
Francesco Alberti, Alessandro Armando, Silvio Ranise
6th ACM Symposium on Information, Computer and Communications Security (ASIACCS), Hong Kong, March 22-24, 2011.
[Link]
|
| 2. |
"Automated Support for the Design and Validation of Parameterized Systems: a case study"
Francesco Alberti, Silvio Ghilardi, Elena Pagani, Silvio Ranise, Gianpaolo Rossi
10th International Workshop on Automated Verification of Critical Systems (AVoCS), Dusseldorf, Germany, September 21-23, 2010.
Electronic Communications of the EASST (ECEASST), vol 35, 2010.
[Link]
[Slides]
|
| 1. |
"Brief Announcement: Automated Support for the Design and Validation of Parameterized Systems: a case study"
Francesco Alberti, Silvio Ghilardi, Elena Pagani, Silvio Ranise, Gianpaolo Rossi
XXIV DIStributed Computing Conference (DISC), Boston, Massachusetts, USA, September 13-15, 2010.
[Link]
|
Teaching
-
Teaching assistant for the course "Discrete Mathematics", academic year 2014/15 - Fall semester.
-
Teaching assistant for the course "Automata and Formal Languages", academic year 2012/13 - Spring semester.
-
Teaching assistant for the course "Software Atelier V: Languages and Compilers", academic year 2012/13 - Fall semester.
-
Teaching assistant for the course "Automata and Formal Languages", academic year 2011/12 - Spring semester.
-
Teaching assistant for the course "Theory of Computation", academic year 2011/12 - Fall semester.
-
Teaching assistant for the course "Software Atelier I: Software Tools", academic year 2010/11 - Fall semester.