Alessandro Cimatti - publication list

Here you can get gzipped .ps versions of some of my publications. Inside each group, the papers are listed in reverse chronological order.
Notice that this list is very outdated. At some point I will manage to fix it, but currently CiteSeer or DBLP are definitely doing a better job. You can also find some recent papers in the sites of MathSAT and MBP.

Copyright Notice

Journals:

A. Cimatti, E. Clarke, F. Giunchiglia, M. Roveri
"NuSMV: a new Symbolic Model Checker".
"International Journal on Software Tools for Technology Transfer (STTT)." Editors-in-Chief: B. Steffen and W. R. Cleaveland. To appear.
V. Hartonas-Garmhausen, S. Campos, A. Cimatti, E. Clarke, F.Giunchiglia.
"Verification of a Safety-Critical Railway Interlocking System with Real-Time Constraints".
"Science of Computer Programming", special issue on Formal Methods for Industrial Critical Systems. To appear.
A. Cimatti, F. Giunchiglia, G. Mongardi, D. Romano, F. Torielli, P. Traverso
"Formal Verification of a Railway Interlocking System using Model Checking".
"Journal on Formal Aspects in Computing". Volume 10, pages 361-380. 1998.
A. Cimatti, F. Giunchiglia, R.W. Weyhrauch
"A many sorted natural deduction".
"Computational Intelligence". Volume 14, Issue 1, pages 135-150. 1998.
E. Giunchiglia, A. Armando, P. Traverso, A. Cimatti
"Visual Representation of Natural Language Scene Descriptions".
"IEEE Transactions on Systems, Man and Cybernetics", Volume 26, Issue 8, pages 279-293, August 1996.
A. Armando, A. Cimatti, E. Giunchiglia, P. Pecchiari, L. Spalazzi, P. Traverso
"Flexible Planning by Integrating Multilevel Reasoning".
"Journal of Engineering Application of Artificial Intelligence", Volume 4, pages 401-412, July 1995.
A. Cimatti, P. Traverso
"Computational Reflection via Mechanized Logical Deduction".
"International Journal of Intelligent Systems", Volume 11, Issue 5, pages 279-293, 1994.
P. Traverso, A. Cimatti, L. Spalazzi, E. Giunchiglia, A. Armando
"MRG: Building Planners for real world complex applications".
"Applied Artificial Intelligence", Volume 8, Issue 3, 1994.

Conferences:

A. Cimatti, M. Roveri
"Conformant Planning via Model Checking."
Proceedings of the European Conference on Planning (ECP99).
Durham, UK. September, 1999. Extended version now available.
A. Cimatti, P.L. Pieraccini, R. Sebastiani, P. Traverso, and A. Villafiorita
"Formal Specification and Validation of a Vital Communication Protocol"
Proceedings of the World Congress on Formal Methods (FM99).
LNCS 1709, pages 1584-1603. Toulouse, France, September 1999.
A. Chiappini, A. Cimatti, G. Rotondo, C. Porzia, R. Sebastiani, P. Traverso, A. Villafiorita
"Formal Specification and Development of a Safety-Critical Train Management System".
In Proceedings of the 18th International Conference on Computer Safety, Reliability and Security (SAFECOMP'99).
Toulouse, FRANCE. September 27-29, 1999. Lecture Notes in Computer Science series (LNCS), number 1698, pages 410-419. M. Felici, K. Kanoun, A. Pasquini (Eds.). Springer, 1999.
Armin Biere, Alessandro Cimatti, Edmund M. Clarke, M. Fujita, Yunshan Zhu
"Symbolic Model Checking Using SAT Procedures instead of BDDs".
In Proceedings of the 36th Conference on Design Automation, New Orleans, LA, USA, June 21-25. Pages 317-320. ACM Press, 1999.
A. Biere, A. Cimatti, E. Clarke, Y. Zhu
"Symbolic Model Checking without BDDs".
In Proceedings of the Fifth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '99), Amsterdam, the Netherlands. Lecture Notes in Computer Science, Vol. 1579, pages 193-207. Springer, 1999.
A. Cimatti, F. Giunchiglia, G. Mongardi, D. Romano, F. Torielli, P. Traverso
"Model Checking Safety Critical Software with SPIN: an Application to a Railway Interlocking System".
In Proceedings of the Seventeenth International Conference on Computer Safety, Reliability and Security (SAFECOMP'98).
Heidelberg, Germany. 1998.
Also presented at the Third SPIN Workshop, Twente University, Enschede, The Netherlands, April 1997.
P.G. Bertoli, A. Cimatti, F. Giunchiglia, P. Traverso
"A Structured Approach to the Formal Certification of Safety of Computer Aided Development Tools".
In Proceedings of the Seventeenth International Conference on Computer Safety, Reliability and Security (SAFECOMP'98).
Heidelberg, Germany. 1998.
A. Cimatti, M. Roveri, P. Traverso
"Automatic OBDD-based Generation of Universal Plans in Non-Deterministic Domains".
In proceedings of the 15th National Conference on Artificial Intelligence - AAAI98.
Madison, Wisconsin, USA, July 1998.
AAAI Press.
A. Cimatti, M. Roveri, P. Traverso
"Strong Planning in Non-Deterministic Domains via Model Checking".
In Proceeding of the Fourth International Conference on Artificial Intelligence Planning Systems (AIPS-98).
Carnegie Mellon University, Pittsburgh, USA. June 1998.
AAAI Press.
V. Hartonas-Garmhausen, S. Campos, A. Cimatti, E. Clarke, F. Giunchiglia
"Verification of a Safety-Critical Railway Interlocking System with Real-time Constraints".
In Proceedings of the 28th International Symposium on Fault-Tolerant Computing (FTCS-28).
Pages 458-463. Munich, Germany, June 1998.
IEEE Computer Society Press.
A. Cimatti, F. Giunchiglia, G. Mongardi, B. Pietra and D. Romano, F. Torielli, P. Traverso
"Formal Validation and Verification of Software for Railway Control and Protection Systems: Experimental Applications in Ansaldo".
In proceedings of the World Congress on Railway Research (WCRR'97)", Volume C, pages 467-473. Firenze, Italy. November 1997.
A. Cimatti, E. Giunchiglia, F. Giunchiglia, P. Traverso
"Planning via Model Checking: A Decision Procedure for AR".
In proceedings of the Fourth European Conference on Planning (ECP97). Lecture Notes in Artificial Intelligence 1348, pages 130-142. S. Steel and R. Alami, eds. Springer-Verlag. Toulouse, France. September 1997.
A. Cimatti, F. Giunchiglia, P. Pecchiari, B. Pietra and J. Profeta, D. Romano, P. Traverso
"A Provably Correct Embedded Verifier for the Certification of Safety Critical Software".
In proceedings of the International Conference on Computer-Aided Verification (CAV'97).
Haifa, Israel. June 1997.
A. Cimatti, L. Serafini
"A context based mechanization of multi-agent reasoning".
In proceedings of the First International and Interdisciplinary Conference on Modeling and Using Context (CONTEXT-97).
Rio De Jeneiro, Brazil. February 1997.
M. Benerecetti, A. Cimatti, E. Giunchiglia, F. Giunchiglia, L. Serafini
"Formal Specification of Multi-Agent Systems".
In Proceedings of the Third International Workshop on Agent Theories, Architectures, and Languages (ATAL-96).
In conjunction with ECAI-96, Budapest, Hungary.
Lecture Notes on Artificial Intelligence, number 1193, pages 117-130.
J.P. Mueller, M.J. Wooldridge, N. R. Jennings, eds. 1996.
A. Cimatti, L. Serafini
"Mechanizing Multi-Agent Reasoning with Belief Contexts".
In "Practical Reasoning" - proceedings of the International Conference on Formal and Applied Practical Reasoning (FAPR'96).
Lecture Notes in Artificial Intelligence, 1085, Springer. 1996.
A. Cimatti, L. Serafini
"Multi-Agent Reasoning with Belief Contexts II: Elaboration Tolerance".
In proceedings of the First International Conference on Multi-Agent Systems (ICMAS-95). 1995.
Also presented at the Third Symposium on Logical Formalizations of Commonsense Reasoning (COMMONSENSE-96). Stanford University, 1996.
A. Cimatti, L. Serafini
"Multi-Agent Reasoning with Belief Contexts: the Approach and a Case Study".
In "Intelligent Agents: Proceedings of the 1994 Workshop on Agent Theories, Architectures, and Languages". M. Wooldridge and N. R. Jennings, eds. Lecture Notes in Computer Science, 850, pages 71-85. Springer Verlag. 1995.
F. Giunchiglia, A. Cimatti
"Introspective Metatheoretic Reasoning".
In proceedings of the 1994 Workshop on Metaprogramming in Logic (META-94).
Lecture Notes in Computer Science 883, pages 425-439. Springer Verlag. Pisa, Italy. June 1994.
A. Armando, A. Cimatti, L. Viganò.
"Building and Executing Proof Strategies in a Formal Metatheory".
Proceedings of the 3rd International Conference of the Italian Association for Artificial Intelligence (AI*IA-93)". Lecture Notes on Artificial Intelligence series, number 728, pages 11-22. Springer, Berlin, 1993.
A. Cimatti, P. Traverso, L. Spalazzi.
"Programming planners with flexible architectures".
Proceedings of the 5th Irish Conference on Artificial Intelligence and Cognitive Science. Limerick, Ireland, September 1992. Springer Verlag.
P. Traverso, A. Cimatti, L. Spalazzi
"Beyond the single planning paradigm: introspective planning".
Proceedings of the European Conference on Artificial Intelligence (ECAI-92). J. Wiley and sons. Vienna, Austria. August 1992.
L. Spalazzi, A. Cimatti, P. Traverso
"Implementing Planning as Tactical Reasoning".
Proceedings of the AI Simulation and Planning in High Autonomy Systems Conference (AIS'92). IEEE Computer Society Press. Perth, Australia. 1992.

National Journals:

F. Giunchiglia, P. Traverso, A. Cimatti, L. Spalazzi, S. Dalbosco, L. Serafini, E. Giunchiglia, A. Armando, P. Pecchiari
"MRG: un nucleo di ragionamento per un sistema integrato multi-funzionale".
In "Sistemi Intelligenti", 3:435-460, 1993. In italian.

Collections:

G. Antoniol, B. Caprile, A. Cimatti, R. Fiutem.
"The Mobile Robot of MAIA: Actions and Interactions in a Real-Life Scenario".
"The Biology and Technology of Intelligent Autonomous Agents" NATO-ASI Series, Computer and Systems Sciences, vol. 144. 1994.

Workshops and Minor Conferences:

A. Cimatti, E. Clarke, F. Giunchiglia, M. Roveri
"NuSMV: a reimplementation of SMV".
In proceedings of the International Workshop on Software Tools for Technology Transfer (STTT-98).
B. Steffen and T. Margaria, eds. BRICS Notes Series, NS-98-4, pages 25-31. Aalborg, Denmark. June 1998.
A. Cimatti, F. Giunchiglia, M. Roveri
"Abstraction in Planning via Model Checking".
In proceedings of the Symposium on Abstraction, Reformulation, and Approximation" (SARA-98). May 1998, Pacific Grove, California USA.
A. Cimatti, L. Serafini
"Multi-Agent Reasoning with Belief Contexts III: Towards the Mechanization".
In proceedings of the IJCAI-95 Workshop on "Modelling Context in Knowledge Representation and Reasoning".
P. Brezillon and S. Abu-Hakima, eds.
P. Bouquet, A. Cimatti
"Mechanizing Local Reasoning with Contexts".
In proceedings of the IJCAI-95 Workshop on "Modelling Context in Knowledge Representation and Reasoning".
P. Brezillon and S. Abu-Hakima, eds.
F. Giunchiglia, A. Armando, A. Cimatti, P. Traverso
First Steps Towards Correct System Synthesis of System Code.
In the proceedings of the CADE-12 workshop on Correctness and Metatheoretic Extensibility of Automated Reasoning Systems.
Nancy, France. June 1994.
P. Traverso, L. Spalazzi, A. Cimatti
A planning language and a semantics for real world autonomous agents.
Proceedings of Workshop Italiano sulla Pianificazione Automatica. Roma, Italy. September 1993.
F. Giunchiglia, A. Cimatti, S. Dalbosco, P. Traverso, L. Spalazzi
MRG: un sistema di ragionamento distribuito per applicazioni complesse
Notes of the AI*IA working group on Distribuited Artificial Intelligence. Roma, Italy. Maggio 1992. In italian.
F. Giunchiglia, P. Traverso, A. Cimatti, P. Pecchiari
A System for Multi-Level Reasoning.
In proceedings of the IMSA'92 International Workshop on Reflection and Meta-level Architectures. A. Yonezawa and B.C. Smith, eds. Tokyo, Japan. 1992.
P. Traverso and A. Cimatti and L. Spalazzi and E. Giunchiglia
Building planners with explicit control mechanisms.
In proceedings of the Fifth International Symposium on Artificial Intelligence. AAAI Press. Cancun, Mexico. 1992.
A. Cimatti, P. Traverso, S. Dalbosco, A. Armando
Navigation by Combining Reactivity and Planning.
In proceedings of Intelligent Vehicles '92. Detroit, USA. 1992.
F. Giunchiglia, P. Traverso, A. Cimatti, L. Spalazzi
Tactics: extending the notion of plan
In proceedings of the ECAI-92 workshop "Beyond Sequential Planning". Vienna, August 1992. Only in hardcopy.
A. Armando, A. Caiti, G. Cannata, A. Cimatti, G. Casalino, G. Bartolini
"Modelling and Simulation of Complex Mechanical Systems".
"Proceedings of the IFAC symposium on Low Cost Automation". Milano, Italy. November 1989. Only in hardcopy.

Technical Reports:

A. Cimatti, F. Giunchiglia, P. Traverso, A. Villafiorita
"Run-Time Result Formal Verification of Safety Critical Software: an Industrial Case Study".
ITC-IRST technical report 9808-01.