Search the dblp DataBase
Alessandro Cimatti :
[Publications ]
[Author Rank by year ]
[Co-authors ]
[Prefers ]
[Cites ]
[Cited by ]
Publications of Author
Alessandro Cimatti , Marco Roveri , Paolo Traverso Automatic OBDD-Based Generation of Universal Plans in Non-Deterministic Domains. [Citation Graph (0, 0)][DBLP ] AAAI/IAAI, 1998, pp:875-881 [Conf ] Alessandro Armando , Alessandro Cimatti , Luca Viganò Building and Executing Proof Strategies in a Formal Metatheory. [Citation Graph (0, 0)][DBLP ] AI*IA, 1993, pp:11-22 [Conf ] Alessandro Cimatti , Marco Roveri , Paolo Traverso Strong Planning in Non-Deterministic Domains Via Model Checking. [Citation Graph (0, 0)][DBLP ] AIPS, 1998, pp:36-43 [Conf ] Piergiorgio Bertoli , Alessandro Cimatti Improving Heuristics for Planning as Search in Belief Space. [Citation Graph (0, 0)][DBLP ] AIPS, 2002, pp:143-152 [Conf ] Piergiorgio Bertoli , Alessandro Cimatti , Marco Pistore , Paolo Traverso A Framework for Planning with Extended Goals under Partial Observability. [Citation Graph (0, 0)][DBLP ] ICAPS, 2003, pp:215-225 [Conf ] Gilles Audemard , Piergiorgio Bertoli , Alessandro Cimatti , Artur Kornilowicz , Roberto Sebastiani Integrating Boolean and Mathematical Solving: Foundations, Basic Algorithms, and Requirements. [Citation Graph (0, 0)][DBLP ] AISC, 2002, pp:231-245 [Conf ] Massimo Benerecetti , Alessandro Cimatti Validation of Multiagent Systems by Symbolic Model Checking. [Citation Graph (0, 0)][DBLP ] AOSE, 2002, pp:32-46 [Conf ] Massimo Benerecetti , Alessandro Cimatti , Enrico Giunchiglia , Fausto Giunchiglia , Luciano Serafini Formal Specification of Beliefs in Multi-Agent Systems. [Citation Graph (0, 0)][DBLP ] ATAL, 1996, pp:117-130 [Conf ] Gilles Audemard , Piergiorgio Bertoli , Alessandro Cimatti , Artur Kornilowicz , Roberto Sebastiani A SAT Based Approach for Solving Formulas over Boolean and Linear Mathematical Propositions. [Citation Graph (0, 0)][DBLP ] CADE, 2002, pp:195-210 [Conf ] Marco Bozzano , Roberto Bruttomesso , Alessandro Cimatti , Tommi A. Junttila , Peter van Rossum , Stephan Schulz , Roberto Sebastiani The MathSAT 3 System. [Citation Graph (0, 0)][DBLP ] CADE, 2005, pp:315-321 [Conf ] Marco Bozzano , Roberto Bruttomesso , Alessandro Cimatti , Tommi A. Junttila , Silvio Ranise , Peter van Rossum , Roberto Sebastiani Efficient Satisfiability Modulo Theories via Delayed Theory Combination. [Citation Graph (0, 0)][DBLP ] CAV, 2005, pp:335-349 [Conf ] 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. [Citation Graph (0, 0)][DBLP ] CAV, 2002, pp:359-364 [Conf ] Alessandro Cimatti , Edmund M. Clarke , Fausto Giunchiglia , Marco Roveri NUSMV: A New Symbolic Model Verifier. [Citation Graph (0, 0)][DBLP ] CAV, 1999, pp:495-499 [Conf ] 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. [Citation Graph (0, 0)][DBLP ] CAV, 1997, pp:202-213 [Conf ] Armin Biere , Alessandro Cimatti , Edmund M. Clarke , Masahiro Fujita , Yunshan Zhu Symbolic Model Checking Using SAT Procedures instead of BDDs. [Citation Graph (0, 0)][DBLP ] DAC, 1999, pp:317-320 [Conf ] Ingo Pill , Simone Semprini , Roberto Cavada , Marco Roveri , Roderick Bloem , Alessandro Cimatti Formal analysis of hardware requirements. [Citation Graph (0, 0)][DBLP ] DAC, 2006, pp:821-826 [Conf ] Piergiorgio Bertoli , Alessandro Cimatti , Marco Pistore Stong Cyclic Planning Under Partial Observability. [Citation Graph (0, 0)][DBLP ] ECAI, 2006, pp:580-584 [Conf ] Piergiorgio Bertoli , Alessandro Cimatti , John K. Slaney , Sylvie Thiébaux Solving Power Supply Restoration Problems with Planning via Symbolic Model Checking. [Citation Graph (0, 0)][DBLP ] ECAI, 2002, pp:576-580 [Conf ] Piergiorgio Bertoli , Alessandro Cimatti , Paolo Traverso Interleaving Execution and Planning for Nondeterministic, Partially Observable Domains. [Citation Graph (0, 0)][DBLP ] ECAI, 2004, pp:657-661 [Conf ] Floris Roelofsen , Luciano Serafini , Alessandro Cimatti Many Hands Make Light Work: Localized Satisfiability for Multi-Context Systems. [Citation Graph (0, 0)][DBLP ] ECAI, 2004, pp:58-62 [Conf ] Paolo Traverso , Alessandro Cimatti , Luca Spalazzi Beyond the Single Planning Paradigm: Introspective Planning. [Citation Graph (0, 0)][DBLP ] ECAI, 1992, pp:643-647 [Conf ] Alessandro Cimatti , Luciano Serafini Multi-Agent Reasoning with Belief Contexts: The Approach and a Case Study. [Citation Graph (0, 0)][DBLP ] ECAI Workshop on Agent Theories, Architectures, and Languages, 1994, pp:71-85 [Conf ] Alessandro Cimatti , Fausto Giunchiglia , Enrico Giunchiglia , Paolo Traverso Planning via Model Checking: A Decision Procedure for AR . [Citation Graph (0, 0)][DBLP ] ECP, 1997, pp:130-142 [Conf ] Alessandro Cimatti , Marco Roveri Conformant Planning via Model Checking. [Citation Graph (0, 0)][DBLP ] ECP, 1999, pp:21-34 [Conf ] Alessandro Cimatti , Luciano Serafini Mechanizing Multi-Agent Reasoning with Belief Contexts. [Citation Graph (0, 0)][DBLP ] FAPR, 1996, pp:694-696 [Conf ] Alessandro Cimatti , P. L. Pieraccini , Roberto Sebastiani , Paolo Traverso , Adolfo Villafiorita Formal Specification and Validation of a Vital Communication Protocol. [Citation Graph (0, 0)][DBLP ] World Congress on Formal Methods, 1999, pp:1584-1604 [Conf ] Alessandro Cimatti , Marco Roveri , Daniel Sheridan Bounded Verification of Past LTL. [Citation Graph (0, 0)][DBLP ] FMCAD, 2004, pp:245-259 [Conf ] Alessandro Cimatti , Marco Roveri , Simone Semprini , Stefano Tonetta From PSL to NBA: a Modular Symbolic Encoding. [Citation Graph (0, 0)][DBLP ] FMCAD, 2006, pp:125-133 [Conf ] Gilles Audemard , Alessandro Cimatti , Artur Kornilowicz , Roberto Sebastiani Bounded Model Checking for Timed Systems. [Citation Graph (0, 0)][DBLP ] FORTE, 2002, pp:243-259 [Conf ] Alessandro Cimatti , Enrico Giunchiglia , Marco Pistore , Marco Roveri , Roberto Sebastiani , Armando Tacchella Integrating BDD-Based and SAT-Based Symbolic Model Checking. [Citation Graph (0, 0)][DBLP ] FroCos, 2002, pp:49-56 [Conf ] 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. [Citation Graph (0, 0)][DBLP ] FTCS, 1998, pp:458-463 [Conf ] Alessandro Cimatti , Luciano Serafini Multiagent Reasoning with Belief Contexts II: Elaboration Tolerance. [Citation Graph (0, 0)][DBLP ] ICMAS, 1995, pp:57-64 [Conf ] Piergiorgio Bertoli , Alessandro Cimatti , Marco Roveri Heuristic Search + Symbolic Model Checking = Efficient Conformant Planning. [Citation Graph (0, 0)][DBLP ] IJCAI, 2001, pp:467-472 [Conf ] Piergiorgio Bertoli , Alessandro Cimatti , Marco Roveri , Paolo Traverso Planning in Nondeterministic Domains under Partial Observability via Symbolic Model Checking. [Citation Graph (0, 0)][DBLP ] IJCAI, 2001, pp:473-478 [Conf ] Alessandro Cimatti , Charles Pecheur , Roberto Cavada Formal Verification of Diagnosability via Symbolic Model Checking. [Citation Graph (0, 0)][DBLP ] IJCAI, 2003, pp:363-369 [Conf ] Fausto Giunchiglia , Alessandro Cimatti Introspective Metatheoretic Reasoning. [Citation Graph (0, 0)][DBLP ] META, 1994, pp:425-439 [Conf ] Roberto Bruttomesso , Alessandro Cimatti , Anders Franzén , Alberto Griggio , Roberto Sebastiani Delayed Theory Combination vs. Nelson-Oppen for Satisfiability Modulo Theories: A Comparative Analysis. [Citation Graph (0, 0)][DBLP ] LPAR, 2006, pp:527-541 [Conf ] 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 ). [Citation Graph (0, 0)][DBLP ] LPAR, 2006, pp:557-571 [Conf ] Alessandro Cimatti Industrial Applications of Model Checking. [Citation Graph (0, 0)][DBLP ] MOVEP, 2000, pp:153-168 [Conf ] Piergiorgio Bertoli , Alessandro Cimatti , Fausto Giunchiglia , Paolo Traverso A Structured Approach to the Formal Certification of Safety of Computer Aided Development Tools. [Citation Graph (0, 0)][DBLP ] SAFECOMP, 1998, pp:221-230 [Conf ] 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. [Citation Graph (0, 0)][DBLP ] SAFECOMP, 1998, pp:284-295 [Conf ] 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. [Citation Graph (0, 0)][DBLP ] SAFECOMP, 1999, pp:410-419 [Conf ] Alessandro Cimatti , Marco Roveri , Piergiorgio Bertoli Searching Powerset Automata by Combining Explicit-State and Symbolic Model Checking. [Citation Graph (0, 0)][DBLP ] TACAS, 2001, pp:313-327 [Conf ] Armin Biere , Alessandro Cimatti , Edmund M. Clarke , Yunshan Zhu Symbolic Model Checking without BDDs. [Citation Graph (0, 0)][DBLP ] TACAS, 1999, pp:193-207 [Conf ] 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. [Citation Graph (0, 0)][DBLP ] TACAS, 2005, pp:317-333 [Conf ] Marco Benedetti , Alessandro Cimatti Bounded Model Checking for Past LTL. [Citation Graph (0, 0)][DBLP ] TACAS, 2003, pp:18-33 [Conf ] Alessandro Cimatti , Marco Pistore , Marco Roveri , Roberto Sebastiani Improving the Encoding of LTL Model Checking into SAT. [Citation Graph (0, 0)][DBLP ] VMCAI, 2002, pp:196-207 [Conf ] Roderick Bloem , Alessandro Cimatti , Ingo Pill , Marco Roveri , Simone Semprini Symbolic Implementation of Alternating Automata. [Citation Graph (0, 0)][DBLP ] CIAA, 2006, pp:208-218 [Conf ] Paolo Traverso , Alessandro Cimatti , Luca Spalazzi , Alessandro Armando , Enrico Giunchiglia MRG: Building planers for real-world complex applications. [Citation Graph (0, 0)][DBLP ] Applied Artificial Intelligence, 1994, v:8, n:3, pp:333-357 [Journal ] Armin Biere , Alessandro Cimatti , Edmund M. Clarke , Ofer Strichman , Yunshan Zhu Bounded model checking. [Citation Graph (0, 0)][DBLP ] Advances in Computers, 2003, v:58, n:, pp:118-149 [Journal ] Piergiorgio Bertoli , Alessandro Cimatti , Marco Roveri , Paolo Traverso Strong planning under partial observability. [Citation Graph (0, 0)][DBLP ] Artif. Intell., 2006, v:170, n:4-5, pp:337-384 [Journal ] Alessandro Cimatti , Marco Pistore , Marco Roveri , Paolo Traverso Weak, strong, and strong cyclic planning via symbolic model checking. [Citation Graph (0, 0)][DBLP ] Artif. Intell., 2003, v:147, n:1-2, pp:35-84 [Journal ] Alessandro Cimatti , Marco Roveri , Piergiorgio Bertoli Conformant planning via symbolic model checking and heuristic search. [Citation Graph (0, 0)][DBLP ] Artif. Intell., 2004, v:159, n:1-2, pp:127-206 [Journal ] Alessandro Cimatti , Fausto Giunchiglia , Richard W. Weyhrauch A Many-Sorted Natural Deduction. [Citation Graph (0, 0)][DBLP ] Computational Intelligence, 1998, v:14, n:, pp:134-149 [Journal ] Alessandro Armando , Alessandro Cimatti Preface. [Citation Graph (0, 0)][DBLP ] Electr. Notes Theor. Comput. Sci., 2006, v:144, n:2, pp:1-2 [Journal ] Gilles Audemard , Marco Bozzano , Alessandro Cimatti , Roberto Sebastiani Verifying Industrial Hybrid Systems with MathSAT. [Citation Graph (0, 0)][DBLP ] Electr. Notes Theor. Comput. Sci., 2005, v:119, n:2, pp:17-32 [Journal ] 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. [Citation Graph (0, 0)][DBLP ] Electr. Notes Theor. Comput. Sci., 2006, v:144, n:2, pp:3-14 [Journal ] Alessandro Cimatti , Orna Grumberg Preface. [Citation Graph (0, 0)][DBLP ] Electr. Notes Theor. Comput. Sci., 1999, v:23, n:2, pp:- [Journal ] Alessandro Cimatti , Fausto Giunchiglia , Giorgio Mongardi , Dario Romano , Fernando Torielli , Paolo Traverso Formal Verification of a Railway Interlocking System using Model Checking. [Citation Graph (0, 0)][DBLP ] Formal Asp. Comput., 1998, v:10, n:4, pp:361-380 [Journal ] Marco Bozzano , Roberto Bruttomesso , Alessandro Cimatti , Tommi A. Junttila , Silvio Ranise , Peter van Rossum , Roberto Sebastiani Efficient theory combination via boolean search. [Citation Graph (0, 0)][DBLP ] Inf. Comput., 2006, v:204, n:10, pp:1493-1525 [Journal ] Alessandro Cimatti , Marco Roveri Conformant Planning via Symbolic Model Checking. [Citation Graph (0, 0)][DBLP ] J. Artif. Intell. Res. (JAIR), 2000, v:13, n:, pp:305-338 [Journal ] 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. [Citation Graph (0, 0)][DBLP ] J. Autom. Reasoning, 2005, v:35, n:1-3, pp:265-293 [Journal ] 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. [Citation Graph (0, 0)][DBLP ] Sci. Comput. Program., 2000, v:36, n:1, pp:53-64 [Journal ] Alessandro Cimatti , Edmund M. Clarke , Fausto Giunchiglia , Marco Roveri NUSMV: A New Symbolic Model Checker. [Citation Graph (0, 0)][DBLP ] STTT, 2000, v:2, n:4, pp:410-425 [Journal ] Piergiorgio Bertoli , Alessandro Cimatti , Marco Pistore Towards Strong Cyclic Planning under Partial Observability. [Citation Graph (0, 0)][DBLP ] ICAPS, 2006, pp:354-357 [Conf ] Marco Bozzano , Alessandro Cimatti , Francesco Tapparo Symbolic Fault Tree Analysis for Reactive Systems. [Citation Graph (0, 0)][DBLP ] ATVA, 2007, pp:162-176 [Conf ] Zvonimir Rakamaric , Roberto Bruttomesso , Alan J. Hu , Alessandro Cimatti Verifying Heap-Manipulating Programs in an SMT Framework. [Citation Graph (0, 0)][DBLP ] ATVA, 2007, pp:237-252 [Conf ] 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. [Citation Graph (0, 0)][DBLP ] CAV, 2007, pp:547-560 [Conf ] Alessandro Cimatti , Marco Roveri , Viktor Schuppan , Stefano Tonetta Boolean Abstraction for Temporal Logic Satisfiability. [Citation Graph (0, 0)][DBLP ] CAV, 2007, pp:532-546 [Conf ] Alessandro Cimatti , Alberto Griggio , Roberto Sebastiani A Simple and Flexible Way of Computing Small Unsatisfiable Cores in SAT Modulo Theories. [Citation Graph (0, 0)][DBLP ] SAT, 2007, pp:334-339 [Conf ] Alessandro Cimatti , Roberto Sebastiani Building Efficient Decision Procedures on Top of SAT Solvers. [Citation Graph (0, 0)][DBLP ] SFM, 2006, pp:144-175 [Conf ] Alessandro Cimatti , Marco Roveri , Stefano Tonetta Syntactic Optimizations for PSL Verification. [Citation Graph (0, 0)][DBLP ] TACAS, 2007, pp:505-518 [Conf ] Piergiorgio Bertoli , Marco Bozzano , Alessandro Cimatti A Symbolic Model Checking Framework for Safety Analysis, Diagnosis, and Synthesis. [Citation Graph (0, 0)][DBLP ] MoChArt, 2006, pp:1-18 [Conf ] Interpolant Generation for UTVPI. [Citation Graph (, )][DBLP ] Requirements Validation for Hybrid Systems. [Citation Graph (, )][DBLP ] The MathSAT 4SMT Solver. [Citation Graph (, )][DBLP ] RATSY - A New Requirements Analysis Tool with Synthesis. [Citation Graph (, )][DBLP ] A Model Checker for AADL. [Citation Graph (, )][DBLP ] Tighter integration of BDDs and SMT for Predicate Abstraction. [Citation Graph (, )][DBLP ] Structure-aware computation of predicate abstraction. [Citation Graph (, )][DBLP ] Computing Predicate Abstractions by Integrating BDDs and SMT Solvers. [Citation Graph (, )][DBLP ] Software model checking via large-block encoding. [Citation Graph (, )][DBLP ] Model Checking of Hybrid Systems Using Shallow Synchronization. [Citation Graph (, )][DBLP ] Formalization and validation of a subset of the European Train Control System. [Citation Graph (, )][DBLP ] Supporting Requirements Validation: The EuRailCheck Tool. [Citation Graph (, )][DBLP ] Symbolic Computation of Schedulability Regions Using Parametric Timed Automata. [Citation Graph (, )][DBLP ] The COMPASS Approach: Correctness, Modelling and Performability of Aerospace Systems. [Citation Graph (, )][DBLP ] Object Models with Temporal Constraints. [Citation Graph (, )][DBLP ] Verification and performance evaluation of aadl models. [Citation Graph (, )][DBLP ] Efficient Interpolant Generation in Satisfiability Modulo Theories. [Citation Graph (, )][DBLP ] Satisfiability Modulo the Theory of Costs: Foundations and Applications. [Citation Graph (, )][DBLP ] Diagnostic Information for Realizability. [Citation Graph (, )][DBLP ] From Informal Requirements to Property-Driven Formal Validation. [Citation Graph (, )][DBLP ] Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis. [Citation Graph (, )][DBLP ] Software Model Checking via Large-Block Encoding [Citation Graph (, )][DBLP ] Efficient Generation of Craig Interpolants in Satisfiability Modulo Theories [Citation Graph (, )][DBLP ] Formalization and Validation of Safety-Critical Requirements [Citation Graph (, )][DBLP ] Search in 0.088secs, Finished in 0.096secs