About me

My name is Andrea Micheli, I am a post-doc researcher in Artificial Intelligence Planning and Temporal Reasoning at the Embedded Systems unit in Fondazione Bruno Kessler.

In the past, I worked in the field of Formal Verification, first as a developer of the NuSMV and nuXmv model checkers and later in the development of the KRATOS software model checker.

I currently work on temporal planning in presence of temporal uncertainty and continuous resources, and I am one of the leaders of the open-source PySMT project.

  Research interests

My primary interests include Artificial Intelligence Planning in Continuous Domains and Temporal Reasoning Under Uncertainty. I focused my research on the study of temporal uncontrollability in planning and I'm currently developing planning systems that take into account these aspects while reasoning.

I am also interested in Satisfiablility Modulo Theory especially in Linear and Non-linear Real Arithmetic and Quantified Theories as an enabling technology for my planning research.

I am still involved in the development of NuSMV, hence I am interested in Formal Verification in general and Model Checking in particular.

  PhD Thesis

My PhD thesis titled "Planning and Scheduling in Temporally Uncertain Domains" has been successfully defended at the University of Trento, Italy on January, 19th 2016.

The thesis won the following awards and recognitions:

The thesis and the relative additional materials are available from the buttons below.

Download Thesis

  Publications

J4
Minh Do, Alessandro Cimatti, Andrea Micheli, Marco Roveri and David E. Smith
Strong Temporal Planning with Uncontrollable Durations
in Artificial Intelligence 2017
Paper
C15
Alessandro Cimatti, Andrea Micheli and Marco Roveri
Validating Domains and Plans for Temporal Planning via Encoding into Infinite-State Linear Temporal Logic
in AAAI 2017
Paper
J3
Alessandro Cimatti, Luke Hunsberger, Andrea Micheli, Roberto Posenato and Marco Roveri
Dynamic Controllability via Timed Game Automata
in Acta Informatica 2016
Paper
C14
Alessandro Cimatti, Andrea Micheli and Marco Roveri
Dynamic Controllability of Disjunctive Temporal Networks: Validation and Synthesis of Executable Strategies
in AAAI 2016
Paper
C13
Marco Gario and Andrea Micheli
pySMT: a Solver-Agnostic Library for Fast Prototyping of SMT-Based Algorithms
in SMT Workshop 2015
Paper
C12
Andrea Micheli, Minh Do and David E. Smith
Compiling Away Uncertainty in Strong Temporal Planning with Uncontrollable Durations
in IJCAI 2015
Paper
I1
Benjamin Bittner, Marco Bozzano, Roberto Cavada, Alessandro Cimatti, Marco Gario, Alberto Griggio, Cristian Mattarei, Andrea Micheli and Gianni Zampedri
The xSAP Safety Analysis Platform
in CoRR 2015
Paper
W2
Andrea Micheli, Minh Do and David E. Smith
Compiling Away Uncertainty in Strong Temporal Planning with Uncontrollable Durations
in SPARK 2015
Paper
J2
Alessandro Cimatti, Andrea Micheli and Marco Roveri
An SMT-based approach to Weak Controllability for Disjunctive Temporal Problems with Uncertainty
in Artificial Intelligence 2015
Paper
C11
Marco Bozzano, Alessandro Cimatti, Marco Gario and Andrea Micheli
SMT-based Validation of Timed Failure Propagation Graphs
in AAAI 2015
Paper
C10
Alessandro Cimatti, Andrea Micheli and Marco Roveri
Strong Temporal Planning with Uncontrollable Durations: a State-Space Approach
in AAAI 2015
Paper
J1
Alessandro Cimatti, Andrea Micheli and Marco Roveri
Solving strong controllability of temporal problems with uncertainty using SMT
in Constraints 2015
Paper
C9
Roberto Cavada, Alessandro Cimatti, Michele Dorigatti, Alberto Griggio, Alessandro Mariotti, Andrea Micheli, Sergio Mover, Marco Roveri and Stefano Tonetta
The nuXmv Symbolic Model Checker
in CAV 2014, pages 334-342
Paper
C8
Alessandro Cimatti, Luke Hunsberger, Andrea Micheli, Roberto Posenato and Marco Roveri
Sound and Complete Algorithms for Checking the Dynamic Controllability of Temporal Networks with Uncertainty, Disjunction and Observation
in TIME 2014
Paper
C7
Alessandro Cimatti, Luke Hunsberger, Andrea Micheli and Marco Roveri
Using Timed Game Automata to Synthesize Execution Strategies for Simple Temporal Networks with Uncertainty
in AAAI 2014
Paper
C6
Alessandro Cimatti, Andrea Micheli and Marco Roveri
Timelines with Temporal Uncertainty
in AAAI 2013
Paper Slides
C5
Alessandro Cimatti, Andrea Micheli and Marco Roveri
Solving Temporal Problems Using SMT: Strong Controllability
in CP 2012, pages 248-264
Paper Slides
C4
Alessandro Cimatti, Andrea Micheli and Marco Roveri
Solving Temporal Problems Using SMT: Weak Controllability
in AAAI 2012, pages 448-454
Paper Slides
C3
Alessandro Cimatti, ALberto Griggio, Andrea Micheli, Iman Narasamdya and Marco Roveri
Kratos - A Software Model Checker for SystemC
in CAV 2011, pages 310-316
Paper
W1
Roberto Cavada, Alessandro Cimatti, Andrea Micheli, Marco Roveri, Angelo Susi and Stefano Tonetta
OthelloPlay: a plug-in based tool for requirement formalization and validation
in TOPI 2010, pages 59-59
Paper
C2
Alessandro Cimatti, Andrea Micheli, Iman Narasamdya and Marco Roveri
Verifying SystemC: A software model checking approach
in FMCAD 2010, pages 51-59
Paper
C1
Roberto Cavada, Alessandro Cimatti, Alessandro Mariotti, Cristian Mattarei, Andrea Micheli, Sergio Mover, Marco Pensallorto, Marco Roveri, Angelo Susi and Stefano Tonetta
Supporting Requirements Validation: The EuRailCheck Tool
in ASE 2009, pages 665-667
Paper

  Teaching

I served as teaching assistant for the Functional and Logic Programming Languages course at the Free University of Bolzano during the academic year 2010/2011.

  Contacts

Andrea Micheli
Embedded Systems Unit, FBK-ICT
Via Sommarive 18, 38123, Trento, Italy
 
  (+39) 0461 314 138