| 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 |
