Alessandro Cimatti

	2009
89		Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani: Interpolant Generation for UTVPI. CADE 2009: 167-182
88		Alessandro Cimatti, Marco Roveri, Stefano Tonetta: Requirements Validation for Hybrid Systems. CAV 2009: 188-203
87		Marco Bozzano, Alessandro Cimatti, Marco Roveri, Joost-Pieter Katoen, Viet Yen Nguyen, Thomas Noll: Verification and performance evaluation of aadl models. ESEC/SIGSOFT FSE 2009: 285-286
86		Marco Bozzano, Alessandro Cimatti, Joost-Pieter Katoen, Viet Yen Nguyen, Thomas Noll, Marco Roveri: The COMPASS Approach: Correctness, Modelling and Performability of Aerospace Systems. SAFECOMP 2009: 173-186
85		Dirk Beyer, Alessandro Cimatti, Alberto Griggio, M. Erkan Keremoglu, Roberto Sebastiani: Software Model Checking via Large-Block Encoding CoRR abs/0904.4709: (2009)
84		Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani: Efficient Generation of Craig Interpolants in Satisfiability Modulo Theories CoRR abs/0906.4492: (2009)
	2008
83		Alessandro Cimatti, Robert B. Jones: Formal Methods in Computer-Aided Design, FMCAD 2008, Portland, Oregon, USA, 17-20 November 2008 IEEE 2008
82		Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, Roberto Sebastiani: The MathSAT 4SMT Solver. CAV 2008: 299-303
81		Alessandro Cimatti, Marco Roveri, Angelo Susi, Stefano Tonetta: From Informal Requirements to Property-Driven Formal Validation. FMICS 2008: 166-181
80		Alessandro Cimatti, Marco Roveri, Angelo Susi, Stefano Tonetta: Object Models with Temporal Constraints. SEFM 2008: 249-258
79		Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani: Efficient Interpolant Generation in Satisfiability Modulo Theories. TACAS 2008: 397-412
78		Alessandro Cimatti, Marco Roveri, Viktor Schuppan, Andrei Tchaltsev: Diagnostic Information for Realizability. VMCAI 2008: 52-67
77		Alessandro Cimatti, Marco Roveri, Stefano Tonetta: Symbolic Compilation of PSL. IEEE Trans. on CAD of Integrated Circuits and Systems 27(10): 1737-1750 (2008)
	2007
76		Marco Bozzano, Alessandro Cimatti, Francesco Tapparo: Symbolic Fault Tree Analysis for Reactive Systems. ATVA 2007: 162-176
75		Zvonimir Rakamaric, Roberto Bruttomesso, Alan J. Hu, Alessandro Cimatti: Verifying Heap-Manipulating Programs in an SMT Framework. ATVA 2007: 237-252
74		Alessandro Cimatti, Marco Roveri, Viktor Schuppan, Stefano Tonetta: Boolean Abstraction for Temporal Logic Satisfiability. CAV 2007: 532-546
73		Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, Ziyad Hanna, Alexander Nadel, Amit Palti, Roberto Sebastiani: A Lazy and Layered SMT($\mathcal{BV}$) Solver for Hard Industrial Verification Problems. CAV 2007: 547-560
72		Roberto Cavada, Alessandro Cimatti, Anders Franzén, Krishnamani Kalyanasundaram, Marco Roveri, R. K. Shyamasundar: Computing Predicate Abstractions by Integrating BDDs and SMT Solvers. FMCAD 2007: 69-76
71		Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani: A Simple and Flexible Way of Computing Small Unsatisfiable Cores in SAT Modulo Theories. SAT 2007: 334-339
70		Alessandro Cimatti, Marco Roveri, Stefano Tonetta: Syntactic Optimizations for PSL Verification. TACAS 2007: 505-518
69		Roderick Bloem, Alessandro Cimatti, Ingo Pill, Marco Roveri: Symbolic Implementation of Alternating Automata. Int. J. Found. Comput. Sci. 18(4): 727-743 (2007)
	2006
68		Marco Bernardo, Alessandro Cimatti: Formal Methods for Hardware Verification, 6th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM 2006, Bertinoro, Italy, May 22-27, 2006, Advanced Lectures Springer 2006
67		Roderick Bloem, Alessandro Cimatti, Ingo Pill, Marco Roveri, Simone Semprini: Symbolic Implementation of Alternating Automata. CIAA 2006: 208-218
66		Ingo Pill, Simone Semprini, Roberto Cavada, Marco Roveri, Roderick Bloem, Alessandro Cimatti: Formal analysis of hardware requirements. DAC 2006: 821-826
65		Piergiorgio Bertoli, Alessandro Cimatti, Marco Pistore: Stong Cyclic Planning Under Partial Observability. ECAI 2006: 580-584
64		Alessandro Cimatti, Marco Roveri, Simone Semprini, Stefano Tonetta: From PSL to NBA: a Modular Symbolic Encoding. FMCAD 2006: 125-133
63		Piergiorgio Bertoli, Alessandro Cimatti, Marco Pistore: Towards Strong Cyclic Planning under Partial Observability. ICAPS 2006: 354-357
62		Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, Roberto Sebastiani: Delayed Theory Combination vs. Nelson-Oppen for Satisfiability Modulo Theories: A Comparative Analysis. LPAR 2006: 527-541
61		Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, Alessandro Santuari, Roberto Sebastiani: To Ackermann-ize or Not to Ackermann-ize? On Efficiently Handling Uninterpreted Function Symbols in SMT(EUF ÈT). LPAR 2006: 557-571
60		Piergiorgio Bertoli, Marco Bozzano, Alessandro Cimatti: A Symbolic Model Checking Framework for Safety Analysis, Diagnosis, and Synthesis. MoChArt 2006: 1-18
59		Alessandro Cimatti, Roberto Sebastiani: Building Efficient Decision Procedures on Top of SAT Solvers. SFM 2006: 144-175
58		Piergiorgio Bertoli, Alessandro Cimatti, Marco Roveri, Paolo Traverso: Strong planning under partial observability. Artif. Intell. 170(4-5): 337-384 (2006)
57		Alessandro Armando, Alessandro Cimatti: Preface. Electr. Notes Theor. Comput. Sci. 144(2): 1-2 (2006)
56		Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Ziyad Hanna, Zurab Khasidashvili, Amit Palti, Roberto Sebastiani: Encoding RTL Constructs for MathSAT: a Preliminary Report. Electr. Notes Theor. Comput. Sci. 144(2): 3-14 (2006)
55		Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Silvio Ranise, Peter van Rossum, Roberto Sebastiani: Efficient theory combination via boolean search. Inf. Comput. 204(10): 1493-1525 (2006)
	2005
54		Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Peter van Rossum, Stephan Schulz, Roberto Sebastiani: The MathSAT 3 System. CADE 2005: 315-321
53		Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Silvio Ranise, Peter van Rossum, Roberto Sebastiani: Efficient Satisfiability Modulo Theories via Delayed Theory Combination. CAV 2005: 335-349
52		Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Peter van Rossum, Stephan Schulz, Roberto Sebastiani: An Incremental and Layered Procedure for the Satisfiability of Linear Arithmetic Logic. TACAS 2005: 317-333
51		Gilles Audemard, Marco Bozzano, Alessandro Cimatti, Roberto Sebastiani: Verifying Industrial Hybrid Systems with MathSAT. Electr. Notes Theor. Comput. Sci. 119(2): 17-32 (2005)
50		Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Peter van Rossum, Stephan Schulz, Roberto Sebastiani: MathSAT: Tight Integration of SAT and Mathematical Decision Procedures. J. Autom. Reasoning 35(1-3): 265-293 (2005)
	2004
49		Floris Roelofsen, Luciano Serafini, Alessandro Cimatti: Many Hands Make Light Work: Localized Satisfiability for Multi-Context Systems. ECAI 2004: 58-62
48		Piergiorgio Bertoli, Alessandro Cimatti, Paolo Traverso: Interleaving Execution and Planning for Nondeterministic, Partially Observable Domains. ECAI 2004: 657-661
47		Alessandro Cimatti, Marco Roveri, Daniel Sheridan: Bounded Verification of Past LTL. FMCAD 2004: 245-259
46		Alessandro Cimatti, Marco Roveri, Piergiorgio Bertoli: Conformant planning via symbolic model checking and heuristic search. Artif. Intell. 159(1-2): 127-206 (2004)
	2003
45		Piergiorgio Bertoli, Alessandro Cimatti, Marco Pistore, Paolo Traverso: A Framework for Planning with Extended Goals under Partial Observability. ICAPS 2003: 215-225
44		Alessandro Cimatti, Charles Pecheur, Roberto Cavada: Formal Verification of Diagnosability via Symbolic Model Checking. IJCAI 2003: 363-369
43		Marco Benedetti, Alessandro Cimatti: Bounded Model Checking for Past LTL. TACAS 2003: 18-33
42		Armin Biere, Alessandro Cimatti, Edmund M. Clarke, Ofer Strichman, Yunshan Zhu: Bounded model checking. Advances in Computers 58: 118-149 (2003)
41		Alessandro Cimatti, Marco Pistore, Marco Roveri, Paolo Traverso: Weak, strong, and strong cyclic planning via symbolic model checking. Artif. Intell. 147(1-2): 35-84 (2003)
	2002
40		Piergiorgio Bertoli, Alessandro Cimatti: Improving Heuristics for Planning as Search in Belief Space. AIPS 2002: 143-152
39		Gilles Audemard, Piergiorgio Bertoli, Alessandro Cimatti, Artur Kornilowicz, Roberto Sebastiani: Integrating Boolean and Mathematical Solving: Foundations, Basic Algorithms, and Requirements. AISC 2002: 231-245
38		Massimo Benerecetti, Alessandro Cimatti: Validation of Multiagent Systems by Symbolic Model Checking. AOSE 2002: 32-46
37		Gilles Audemard, Piergiorgio Bertoli, Alessandro Cimatti, Artur Kornilowicz, Roberto Sebastiani: A SAT Based Approach for Solving Formulas over Boolean and Linear Mathematical Propositions. CADE 2002: 195-210
36		Alessandro Cimatti, Edmund M. Clarke, Enrico Giunchiglia, Fausto Giunchiglia, Marco Pistore, Marco Roveri, Roberto Sebastiani, Armando Tacchella: NuSMV 2: An OpenSource Tool for Symbolic Model Checking. CAV 2002: 359-364
35		Piergiorgio Bertoli, Alessandro Cimatti, John K. Slaney, Sylvie Thiébaux: Solving Power Supply Restoration Problems with Planning via Symbolic Model Checking. ECAI 2002: 576-580
34		Gilles Audemard, Alessandro Cimatti, Artur Kornilowicz, Roberto Sebastiani: Bounded Model Checking for Timed Systems. FORTE 2002: 243-259
33		Alessandro Cimatti, Enrico Giunchiglia, Marco Pistore, Marco Roveri, Roberto Sebastiani, Armando Tacchella: Integrating BDD-Based and SAT-Based Symbolic Model Checking. FroCos 2002: 49-56
32		Alessandro Cimatti, Marco Pistore, Marco Roveri, Roberto Sebastiani: Improving the Encoding of LTL Model Checking into SAT. VMCAI 2002: 196-207
	2001
31		Piergiorgio Bertoli, Alessandro Cimatti, Marco Roveri: Heuristic Search + Symbolic Model Checking = Efficient Conformant Planning. IJCAI 2001: 467-472
30		Piergiorgio Bertoli, Alessandro Cimatti, Marco Roveri, Paolo Traverso: Planning in Nondeterministic Domains under Partial Observability via Symbolic Model Checking. IJCAI 2001: 473-478
29		Alessandro Cimatti, Marco Roveri, Piergiorgio Bertoli: Searching Powerset Automata by Combining Explicit-State and Symbolic Model Checking. TACAS 2001: 313-327
	2000
28		Alessandro Cimatti: Industrial Applications of Model Checking. MOVEP 2000: 153-168
27		Alessandro Cimatti, Marco Roveri: Conformant Planning via Symbolic Model Checking. J. Artif. Intell. Res. (JAIR) 13: 305-338 (2000)
26		Alessandro Cimatti, Edmund M. Clarke, Fausto Giunchiglia, Marco Roveri: NUSMV: A New Symbolic Model Checker. STTT 2(4): 410-425 (2000)
25		Vicky Hartonas-Garmhausen, Sérgio Vale Aguiar Campos, Alessandro Cimatti, Edmund M. Clarke, Fausto Giunchiglia: Verification of a safety-critical railway interlocking system with real-time constraints. Sci. Comput. Program. 36(1): 53-64 (2000)
	1999
24		Alessandro Cimatti, Edmund M. Clarke, Fausto Giunchiglia, Marco Roveri: NUSMV: A New Symbolic Model Verifier. CAV 1999: 495-499
23		Armin Biere, Alessandro Cimatti, Edmund M. Clarke, Masahiro Fujita, Yunshan Zhu: Symbolic Model Checking Using SAT Procedures instead of BDDs. DAC 1999: 317-320
22		Alessandro Cimatti, Marco Roveri: Conformant Planning via Model Checking. ECP 1999: 21-34
21		A. Chiappini, Alessandro Cimatti, Carmen Porzia, G. Rotondo, Roberto Sebastiani, Paolo Traverso, Adolfo Villafiorita: Formal Specification and Development of a Safety-Critical Train Management System. SAFECOMP 1999: 410-419
20		Armin Biere, Alessandro Cimatti, Edmund M. Clarke, Yunshan Zhu: Symbolic Model Checking without BDDs. TACAS 1999: 193-207
19		Alessandro Cimatti, P. L. Pieraccini, Roberto Sebastiani, Paolo Traverso, Adolfo Villafiorita: Formal Specification and Validation of a Vital Communication Protocol. World Congress on Formal Methods 1999: 1584-1604
18		Alessandro Cimatti, Orna Grumberg: Preface. Electr. Notes Theor. Comput. Sci. 23(2): (1999)
	1998
17		Alessandro Cimatti, Marco Roveri, Paolo Traverso: Automatic OBDD-Based Generation of Universal Plans in Non-Deterministic Domains. AAAI/IAAI 1998: 875-881
16		Alessandro Cimatti, Marco Roveri, Paolo Traverso: Strong Planning in Non-Deterministic Domains Via Model Checking. AIPS 1998: 36-43
15		Vicky Hartonas-Garmhausen, Sérgio Vale Aguiar Campos, Alessandro Cimatti, Edmund M. Clarke, Fausto Giunchiglia: Verification of a Safety-Critical Railway Interlocking System with Real-Time Constraints. FTCS 1998: 458-463
14		Piergiorgio Bertoli, Alessandro Cimatti, Fausto Giunchiglia, Paolo Traverso: A Structured Approach to the Formal Certification of Safety of Computer Aided Development Tools. SAFECOMP 1998: 221-230
13		Alessandro Cimatti, Fausto Giunchiglia, Giorgio Mongardi, Dario Romano, Fernando Torielli, Paolo Traverso: Model Checking Safety Critical Software with SPIN: An Application to a Railway Interlocking System. SAFECOMP 1998: 284-295
12		Alessandro Cimatti, Fausto Giunchiglia, Richard W. Weyhrauch: A Many-Sorted Natural Deduction. Computational Intelligence 14: 134-149 (1998)
11		Alessandro Cimatti, Fausto Giunchiglia, Giorgio Mongardi, Dario Romano, Fernando Torielli, Paolo Traverso: Formal Verification of a Railway Interlocking System using Model Checking. Formal Asp. Comput. 10(4): 361-380 (1998)
	1997
10		Alessandro Cimatti, Fausto Giunchiglia, Paolo Pecchiari, Bruno Pietra, Joe Profeta, Dario Romano, Paolo Traverso, Bing Yu: A Provably Correct Embedded Verifier for the Certification of Safety Critical Software. CAV 1997: 202-213
9		Alessandro Cimatti, Fausto Giunchiglia, Enrico Giunchiglia, Paolo Traverso: Planning via Model Checking: A Decision Procedure for AR. ECP 1997: 130-142
	1996
8		Massimo Benerecetti, Alessandro Cimatti, Enrico Giunchiglia, Fausto Giunchiglia, Luciano Serafini: Formal Specification of Beliefs in Multi-Agent Systems. ATAL 1996: 117-130
7		Alessandro Cimatti, Luciano Serafini: Mechanizing Multi-Agent Reasoning with Belief Contexts. FAPR 1996: 694-696
	1995
6		Alessandro Cimatti, Luciano Serafini: Multiagent Reasoning with Belief Contexts II: Elaboration Tolerance. ICMAS 1995: 57-64
	1994
5		Alessandro Cimatti, Luciano Serafini: Multi-Agent Reasoning with Belief Contexts: The Approach and a Case Study. ECAI Workshop on Agent Theories, Architectures, and Languages 1994: 71-85
4		Fausto Giunchiglia, Alessandro Cimatti: Introspective Metatheoretic Reasoning. META 1994: 425-439
3		Paolo Traverso, Alessandro Cimatti, Luca Spalazzi, Alessandro Armando, Enrico Giunchiglia: MRG: Building planers for real-world complex applications. Applied Artificial Intelligence 8(3): 333-357 (1994)
	1993
2		Alessandro Armando, Alessandro Cimatti, Luca Viganò: Building and Executing Proof Strategies in a Formal Metatheory. AI*IA 1993: 11-22
	1992
1		Paolo Traverso, Alessandro Cimatti, Luca Spalazzi: Beyond the Single Planning Paradigm: Introspective Planning. ECAI 1992: 643-647

Coauthor Index

1	Alessandro Armando	[2] [3] [57]
2	Gilles Audemard	[34] [37] [39] [51]
3	Marco Benedetti	[43]
4	Massimo Benerecetti	[8] [38]
5	Marco Bernardo	[68]
6	Piergiorgio Bertoli	[14] [29] [30] [31] [35] [37] [39] [40] [45] [46] [48] [58] [60] [63] [65]
7	Dirk Beyer	[85]
8	Armin Biere	[20] [23] [42]
9	Roderick Bloem	[66] [67] [69]
10	Marco Bozzano	[50] [51] [52] [53] [54] [55] [56] [60] [76] [86] [87]
11	Roberto Bruttomesso	[50] [52] [53] [54] [55] [56] [61] [62] [73] [75] [82]
12	Sérgio Vale Aguiar Campos	[15] [25]
13	Roberto Cavada	[44] [66] [72]
14	A. Chiappini	[21]
15	Edmund M. Clarke	[15] [20] [23] [24] [25] [26] [36] [42]
16	Anders Franzén	[56] [61] [62] [72] [73] [82]
17	Masahiro Fujita	[23]
18	Enrico Giunchiglia	[3] [8] [9] [33] [36]
19	Fausto Giunchiglia	[4] [8] [9] [10] [11] [12] [13] [14] [15] [24] [25] [26] [36]
20	Alberto Griggio	[61] [62] [71] [73] [79] [82] [84] [85] [89]
21	Orna Grumberg	[18]
22	Ziyad Hanna	[56] [73]
23	Vicky Hartonas-Garmhausen	[15] [25]
24	Alan J. Hu	[75]
25	Robert B. Jones	[83]
26	Tommi A. Junttila	[50] [52] [53] [54] [55]
27	Krishnamani Kalyanasundaram	[72]
28	Joost-Pieter Katoen	[86] [87]
29	M. Erkan Keremoglu	[85]
30	Zurab Khasidashvili	[56]
31	Artur Kornilowicz	[34] [37] [39]
32	Giorgio Mongardi	[11] [13]
33	Alexander Nadel	[73]
34	Viet Yen Nguyen	[86] [87]
35	Thomas Noll	[86] [87]
36	Amit Palti	[56] [73]
37	Paolo Pecchiari	[10]
38	Charles Pecheur	[44]
39	P. L. Pieraccini	[19]
40	Bruno Pietra	[10]
41	Ingo Pill	[66] [67] [69]
42	Marco Pistore	[32] [33] [36] [41] [45] [63] [65]
43	Carmen Porzia	[21]
44	Joe Profeta	[10]
45	Zvonimir Rakamaric	[75]
46	Silvio Ranise	[53] [55]
47	Floris Roelofsen	[49]
48	Dario Romano	[10] [11] [13]
49	Peter van Rossum	[50] [52] [53] [54] [55]
50	G. Rotondo	[21]
51	Marco Roveri	[16] [17] [22] [24] [26] [27] [29] [30] [31] [32] [33] [36] [41] [46] [47] [58] [64] [66] [67] [69] [70] [72] [74] [77] [78] [80] [81] [86] [87] [88]
52	Alessandro Santuari	[61]
53	Stephan Schulz	[50] [52] [54]
54	Viktor Schuppan	[74] [78]
55	Roberto Sebastiani	[19] [21] [32] [33] [34] [36] [37] [39] [50] [51] [52] [53] [54] [55] [56] [59] [61] [62] [71] [73] [79] [82] [84] [85] [89]
56	Simone Semprini	[64] [66] [67]
57	Luciano Serafini	[5] [6] [7] [8] [49]
58	Daniel Sheridan	[47]
59	R. K. Shyamasundar	[72]
60	John K. Slaney	[35]
61	Luca Spalazzi	[1] [3]
62	Ofer Strichman	[42]
63	Angelo Susi	[80] [81]
64	Armando Tacchella	[33] [36]
65	Francesco Tapparo	[76]
66	Andrei Tchaltsev	[78]
67	Sylvie Thiébaux	[35]
68	Stefano Tonetta	[64] [70] [74] [77] [80] [81] [88]
69	Fernando Torielli	[11] [13]
70	Paolo Traverso	[1] [3] [9] [10] [11] [13] [14] [16] [17] [19] [21] [30] [41] [45] [48] [58]
71	Luca Viganò	[2]
72	Adolfo Villafiorita	[19] [21]
73	Richard W. Weyhrauch	[12]
74	Bing Yu	[10]
75	Yunshan Zhu	[20] [23] [42]

Colors in the list of coauthors