He has published many papers on AR topics in AI or AI-related journals (e.g., Artificial Intelligence, JAIR, Information and Computation) and conferences (e.g., AAAI, CADE, KR) and also in formal methods conferences (e.g., CAV, TACAS, FORTE). He has been part of the PC of AI-related conferences and workshops like AIMSA98, KR2000, Calculemus 2001 and 2002, FroCoS 2002. He is a Trustee of the Calculemus! Interest Group. He has been co-chair of Calculemus 2001. He is guest editor of Journal of Symbolic Computation, Special Issue on the Integration of Automated Reasoning and Computer Algebra Systems (to appear).
His research focuses on Automated Reasoning, Planning and Model Checking. His research interests are Formal Verification, SAT, non-CNF SAT, SAT-based Planning and Model Checking, Decision procedures for modal logics, Integration of Automated Reasoning and Computer Algebra. He has a deep expertise in SAT algorithms and their applications [12,8,9,5]. In particular, he is an expert in techniques for integrating SAT solvers with domain-specific solvers in various fields [10,13,6,11,7,2,1,3]. He is one of the main developers of the KSAT [10,13,6,11,7] and MathSAT tools [2,1,3]. He is in the team developing the SAT+BDD based Model Checker NuSMV2 .
He has given the two specific courses on the topic of the tutorial described in Section 2. He is a staff member and part of the scientific committee of the International Graduate School in Information and Communication Technologies of University of Trento.
For details, see Roberto
Sebastiani's Home Page and
Dr. Roberto Sebastiani,
Dept. of Information and Communication Technology,
University of Trento,
via Sommarive 14, I-38050 Trento, Italy.
fax: ++39 0461 882093,