2009 |
82 | EE | Dirk Beyer,
Alessandro Cimatti,
Alberto Griggio,
M. Erkan Keremoglu,
Roberto Sebastiani:
Software Model Checking via Large-Block Encoding
CoRR abs/0904.4709: (2009) |
2008 |
81 | EE | Roberto Bruttomesso,
Alessandro Cimatti,
Anders Franzén,
Alberto Griggio,
Roberto Sebastiani:
The MathSAT 4SMT Solver.
CAV 2008: 299-303 |
80 | EE | Alessandro Cimatti,
Marco Roveri,
Angelo Susi,
Stefano Tonetta:
Object Models with Temporal Constraints.
SEFM 2008: 249-258 |
79 | EE | Alessandro Cimatti,
Alberto Griggio,
Roberto Sebastiani:
Efficient Interpolant Generation in Satisfiability Modulo Theories.
TACAS 2008: 397-412 |
78 | EE | Alessandro Cimatti,
Marco Roveri,
Viktor Schuppan,
Andrei Tchaltsev:
Diagnostic Information for Realizability.
VMCAI 2008: 52-67 |
77 | EE | 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 | EE | Marco Bozzano,
Alessandro Cimatti,
Francesco Tapparo:
Symbolic Fault Tree Analysis for Reactive Systems.
ATVA 2007: 162-176 |
75 | EE | Zvonimir Rakamaric,
Roberto Bruttomesso,
Alan J. Hu,
Alessandro Cimatti:
Verifying Heap-Manipulating Programs in an SMT Framework.
ATVA 2007: 237-252 |
74 | EE | Alessandro Cimatti,
Marco Roveri,
Viktor Schuppan,
Stefano Tonetta:
Boolean Abstraction for Temporal Logic Satisfiability.
CAV 2007: 532-546 |
73 | EE | 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 | EE | 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 | EE | 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 | EE | Alessandro Cimatti,
Marco Roveri,
Stefano Tonetta:
Syntactic Optimizations for PSL Verification.
TACAS 2007: 505-518 |
69 | EE | 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 | EE | Roderick Bloem,
Alessandro Cimatti,
Ingo Pill,
Marco Roveri,
Simone Semprini:
Symbolic Implementation of Alternating Automata.
CIAA 2006: 208-218 |
66 | EE | 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 | EE | 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 | EE | 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 | EE | 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 | EE | Piergiorgio Bertoli,
Marco Bozzano,
Alessandro Cimatti:
A Symbolic Model Checking Framework for Safety Analysis, Diagnosis, and Synthesis.
MoChArt 2006: 1-18 |
59 | EE | Alessandro Cimatti,
Roberto Sebastiani:
Building Efficient Decision Procedures on Top of SAT Solvers.
SFM 2006: 144-175 |
58 | EE | Piergiorgio Bertoli,
Alessandro Cimatti,
Marco Roveri,
Paolo Traverso:
Strong planning under partial observability.
Artif. Intell. 170(4-5): 337-384 (2006) |
57 | EE | Alessandro Armando,
Alessandro Cimatti:
Preface.
Electr. Notes Theor. Comput. Sci. 144(2): 1-2 (2006) |
56 | EE | 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 | EE | 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 | EE | 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 | EE | 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 | EE | 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 | EE | 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 | EE | 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 | EE | Alessandro Cimatti,
Marco Roveri,
Daniel Sheridan:
Bounded Verification of Past LTL.
FMCAD 2004: 245-259 |
46 | EE | 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 | EE | 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 | EE | 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 | EE | 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 | EE | Massimo Benerecetti,
Alessandro Cimatti:
Validation of Multiagent Systems by Symbolic Model Checking.
AOSE 2002: 32-46 |
37 | EE | 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 | EE | 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 | EE | Gilles Audemard,
Alessandro Cimatti,
Artur Kornilowicz,
Roberto Sebastiani:
Bounded Model Checking for Timed Systems.
FORTE 2002: 243-259 |
33 | EE | 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 | EE | 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 | EE | Alessandro Cimatti,
Marco Roveri,
Piergiorgio Bertoli:
Searching Powerset Automata by Combining Explicit-State and Symbolic Model Checking.
TACAS 2001: 313-327 |
2000 |
28 | EE | Alessandro Cimatti:
Industrial Applications of Model Checking.
MOVEP 2000: 153-168 |
27 | EE | Alessandro Cimatti,
Marco Roveri:
Conformant Planning via Symbolic Model Checking.
J. Artif. Intell. Res. (JAIR) 13: 305-338 (2000) |
26 | EE | 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 | EE | Alessandro Cimatti,
Edmund M. Clarke,
Fausto Giunchiglia,
Marco Roveri:
NUSMV: A New Symbolic Model Verifier.
CAV 1999: 495-499 |
23 | EE | 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 | EE | 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 | EE | Armin Biere,
Alessandro Cimatti,
Edmund M. Clarke,
Yunshan Zhu:
Symbolic Model Checking without BDDs.
TACAS 1999: 193-207 |
19 | EE | 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 | EE | 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 | EE | 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 | EE | 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 | EE | 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 |