Edit Profile (opens in new tab) Cimatti, Alessandro Compute Distance To: Compute Author ID: cimatti.alessandro Published as: Cimatti, Alessandro; Cimatti, A. Documents Indexed: 84 Publications since 1996 5 Contributions as Editor Co-Authors: 88 Co-Authors with 88 Joint Publications 1,535 Co-Co-Authors all top 5 Co-Authors 1 single-authored 31 Roveri, Marco 30 Sebastiani, Roberto 26 Griggio, Alberto 16 Tonetta, Stefano 13 Bozzano, Marco 9 Bruttomesso, Roberto 8 Mover, Sergio 6 Bertoli, Piergiorgio 6 Irfan, Ahmed 5 Franzén, Anders 5 Micheli, Andrea 4 Audemard, Gilles 4 Giunchiglia, Fausto 4 Junttila, Tommi A. 4 Magnago, Enrico 4 Pistore, Marco 4 Traverso, Paolo 4 van Rossum, Peter 3 Clarke, Edmund Melson jun. 3 Gario, Marco 3 Korniłowicz, Artur 3 Mattarei, Cristian 2 Abbott, John A. 2 Ábrahám, Erika 2 Becker, Bernd 2 Bigatti, Anna Maria 2 Bloem, Roderick 2 Brain, Martin 2 Buchberger, Bruno 2 Davenport, James Harold 2 England, Matthew 2 Fontaine, Pascal 2 Forrest, Stephen 2 Giunchiglia, Enrico 2 Kröning, Daniel 2 Narasamdya, Iman 2 Pill, Ingo 2 Ranise, Silvio 2 Schaafsma, Bastiaan Joost 2 Schulz, Stephan 2 Schuppan, Viktor 2 Seiler, Werner M. 2 Serafini, Luciano 2 Sturm, Thomas 2 Tacchella, Armando 1 Abate, Alessandro 1 Armando, Alessandro 1 Becchi, Anna 1 Benedetti, Marco H. 1 Benerecetti, Massimo 1 Bernardo, Marco 1 Bigarella, Filippo 1 Bittner, Benjamin 1 Bliudze, Simon 1 Daniel, Jakub 1 Demasi, Ramiro 1 Geatti, Luca 1 Gigante, Nicola 1 Grumberg, Orna 1 Hanna, Ziyad 1 Hu, Alan J. 1 Hunsberger, Luke 1 Jaber, Mohamad Y. 1 Jonáš, Martin 1 Khasidashvili, Zurab O. 1 Mongardi, Giovanni 1 Montanari, Angelo 1 Mufid, Muhammad Syifa’ul 1 Palti, Amit 1 Posenato, Roberto 1 Rakamarić, Zvonimir 1 Redondi, Gianluca 1 Saab, Wajeb 1 Santuari, Alessandro 1 Semprini, Simone 1 Sessa, Mirko 1 Sheridan, Daniel 1 Sirjani, Marjan 1 Smith, David E. 1 Stenico, Cristian 1 Stojic, Ivan 1 Tapparo, Francesco 1 Tchaltsev, A. 1 Torielli, F. 1 Trentin, Patrick 1 Vozarova, Viktoria 1 Wang, Qiang 1 Zaffanella, Enea all top 5 Serials 6 Artificial Intelligence 4 Information and Computation 4 Formal Methods in System Design 3 Formal Aspects of Computing 3 Lecture Notes in Computer Science 2 The Journal of Artificial Intelligence Research (JAIR) 2 ACM Transactions on Computational Logic 2 Electronic Notes in Theoretical Computer Science 2 Logical Methods in Computer Science 1 Acta Informatica 1 Information Processing Letters 1 Journal of Automated Reasoning 1 International Journal of Intelligent Systems 1 International Journal of Foundations of Computer Science 1 Annals of Mathematics and Artificial Intelligence 1 Constraints 1 1 ACM Communications in Computer Algebra all top 5 Fields 88 Computer science (68-XX) 15 Mathematical logic and foundations (03-XX) 5 General and overarching topics; collections (00-XX) 4 Systems theory; control (93-XX) 2 Dynamical systems and ergodic theory (37-XX) 2 Operations research, mathematical programming (90-XX) 1 Ordinary differential equations (34-XX) 1 Information and communication theory, circuits (94-XX) Publications by Year all cited Publications top 5 cited Publications Citations contained in zbMATH Open 65 Publications have been cited 697 times in 479 Documents Cited by ▼ Year ▼ NuSMV 2: An OpenSource tool for symbolic model checking. Zbl 1010.68766Cimatti, Alessandro; Clarke, Edmund; Giunchiglia, Enrico; Giunchiglia, Fausto; Pistore, Marco; Roveri, Marco; Sebastiani, Roberto; Tacchella, Armando 95 2002 The MathSAT5 SMT solver. Zbl 1381.68153Cimatti, Alessandro; Griggio, Alberto; Schaafsma, Bastiaan Joost; Sebastiani, Roberto 60 2013 Diagnostic information for realizability. Zbl 1138.68442Cimatti, A.; Roveri, M.; Schuppan, V.; Tchaltsev, A. 42 2008 NuSMV: A new symbolic model checker. Zbl 1059.68582Cimatti, Alessandro; Clarke, Edmund; Giunchiglia, Fausto; Roveri, Marco 37 2000 Weak, strong, and strong cyclic planning via symbolic model checking. Zbl 1082.68800Cimatti, A.; Pistore, M.; Roveri, M.; Traverso, P. 35 2003 NuSMV: A new symbolic model verifier. Zbl 1046.68587Cimatti, A.; Clarke, E.; Giunchiglia, F.; Roveri, M. 35 1999 Efficient interpolant generation in satisfiability modulo theories. Zbl 1134.68402Cimatti, Alessandro; Griggio, Alberto; Sebastiani, Roberto 19 2008 Conformant planning via symbolic model checking. Zbl 0963.68195Cimatti, A.; Roveri, M. 19 2000 Infinite-state invariant checking with IC3 and predicate abstraction. Zbl 1368.68245Cimatti, Alessandro; Griggio, Alberto; Mover, Sergio; Tonetta, Stefano 18 2016 Efficient generation of Craig interpolants in satisfiability modulo theories. Zbl 1351.68247Cimatti, Alessandro; Griggio, Alberto; Sebastiani, Roberto 18 2010 Conformant planning via symbolic model checking and heuristic search. Zbl 1086.68591Cimatti, A.; Roveri, M.; Bertoli, P. 16 2004 A SAT based approach for solving formulas over Boolean and linear mathematical propositions. Zbl 1072.68562Audemard, Gilles; Bertoli, Piergiorgio; Cimatti, Alessandro; Korniłowicz, Artur; Sebastiani, Roberto 15 2002 Verifying industrial hybrid systems with MathSAT. Zbl 1272.68220Audemard, Gilles; Bozzano, Marco; Cimatti, Alessandro; Sebastiani, Roberto 15 2005 Efficient theory combination via Boolean search. Zbl 1137.68578Bozzano, Marco; Bruttomesso, Roberto; Cimatti, Alessandro; Junttila, Tommi; Ranise, Silvio; Van Rossum, Peter; Sebastiani, Roberto 14 2006 Incremental linearization for satisfiability and verification modulo nonlinear arithmetic and transcendental functions. Zbl 1407.68285Cimatti, Alessandro; Griggio, Alberto; Irfan, Ahmed; Roveri, Marco; Sebastiani, Roberto 14 2018 Strong planning under partial observability. Zbl 1131.68095Bertoli, Piergiorgio; Cimatti, Alessandro; Roveri, Marco; Traverso, Paolo 13 2006 Computing small unsatisfiable cores in satisfiability modulo theories. Zbl 1216.68241Cimatti, A.; Griggio, A.; Sebastiani, R. 12 2011 SC\(^2\): satisfiability checking meets symbolic computation. (Project paper). Zbl 1344.68198Ábrahám, Erika; Abbott, John; Becker, Bernd; Bigatti, Anna M.; Brain, Martin; Buchberger, Bruno; Cimatti, Alessandro; Davenport, James H.; England, Matthew; Fontaine, Pascal; Forrest, Stephen; Griggio, Alberto; Kroening, Daniel; Seiler, Werner M.; Sturm, Thomas 12 2016 Bounded model checking for timed systems. Zbl 1037.68549Audemard, G.; Cimatti, A.; Kornilowicz, A.; Sebastiani, R. 12 2002 Satisfiability modulo the theory of costs: foundations and applications. Zbl 1284.68388Cimatti, Alessandro; Franzén, Anders; Griggio, Alberto; Sebastiani, Roberto; Stenico, Cristian 11 2010 SMT-based scenario verification for hybrid systems. Zbl 1284.03216Cimatti, Alessandro; Mover, Sergio; Tonetta, Stefano 10 2013 An incremental and layered procedure for the satisfiability of linear arithmetic logic. Zbl 1087.68630Bozzano, Marco; Bruttomesso, Roberto; Cimatti, Alessandro; Junttila, Tommi; van Rossum, Peter; Schulz, Stephan; Sebastiani, Roberto 10 2005 Solving strong controllability of temporal problems with uncertainty using SMT. Zbl 1314.90043Cimatti, Alessandro; Micheli, Andrea; Roveri, Marco 10 2015 A simple and flexible way of computing small unsatisfiable cores in SAT modulo theories. Zbl 1214.68348Cimatti, Alessandro; Griggio, Alberto; Sebastiani, Roberto 8 2007 Requirements validation for hybrid systems. Zbl 1242.68156Cimatti, Alessandro; Roveri, Marco; Tonetta, Stefano 8 2009 A modular approach to MaxSAT modulo theories. Zbl 1390.68572Cimatti, Alessandro; Griggio, Alberto; Schaafsma, Bastiaan Joost; Sebastiani, Roberto 8 2013 Symbolic implementation of alternating automata. Zbl 1160.68401Bloem, R.; Cimatti, A.; Pill, I.; Roveri, M.; Semprini, S. 7 2006 Boolean abstraction for temporal logic satisfiability. Zbl 1135.68469Cimatti, Alessandro; Roveri, Marco; Schuppan, Viktor; Tonetta, Stefano 7 2007 Infinite-state liveness-to-safety via implicit abstraction and well-founded relations. Zbl 1411.68062Daniel, Jakub; Cimatti, Alessandro; Griggio, Alberto; Tonetta, Stefano; Mover, Sergio 6 2016 MathSAT: Tight integration of SAT and mathematical decision procedures. Zbl 1109.68101Bozzano, Marco; Bruttomesso, Roberto; Cimatti, Alessandro; Junttila, Tommi; van Rossum, Peter; Schulz, Stephan; Sebastiani, Roberto 6 2005 Efficient satisfiability modulo theories via delayed theory combination. Zbl 1081.68610Bozzano, Marco; Bruttomesso, Roberto; Cimatti, Alessandro; Junttila, Tommi; Ranise, Silvio; van Rossum, Peter; Sebastiani, Roberto 6 2005 Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis. Zbl 1192.68627Bruttomesso, Roberto; Cimatti, Alessandro; Franzen, Anders; Griggio, Alberto; Sebastiani, Roberto 6 2009 Theory and applications of satisfiability testing – SAT 2012. 15th international conference, Trento, Italy, June 17–20, 2012. Proceedings. Zbl 1268.68009 6 2012 Dynamic controllability via timed game automata. Zbl 1350.68251Cimatti, Alessandro; Hunsberger, Luke; Micheli, Andrea; Posenato, Roberto; Roveri, Marco 6 2016 Industrial applications of model checking. Zbl 0985.68653Cimatti, Alessandro 5 2001 Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: A comparative analysis. Zbl 1165.68483Bruttomesso, Roberto; Cimatti, Alessandro; Franzén, Anders; Griggio, Alberto; Sebastiani, Roberto 5 2006 To Ackermann-ize or not to Ackermann-ize? On efficiently handling uninterpreted function symbols in SMT\((\mathcal{EUF} \cup \mathcal{T})\). Zbl 1165.68482Bruttomesso, Roberto; Cimatti, Alessandro; Franzén, Anders; Griggio, Alberto; Santuari, Alessandro; Sebastiani, Roberto 5 2006 Interpolant generation for UTVPI. Zbl 1250.68186Cimatti, Alessandro; Griggio, Alberto; Sebastiani, Roberto 5 2009 Symbolic fault tree analysis for reactive systems. Zbl 1141.68455Bozzano, Marco; Cimatti, Alessandro; Tapparo, Francesco 4 2007 Satisfiability modulo transcendental functions via incremental linearization. Zbl 1494.68281Cimatti, Alessandro; Griggio, Alberto; Irfan, Ahmed; Roveri, Marco; Sebastiani, Roberto 4 2017 Formal design of asynchronous fault detection and identification components using temporal epistemic logic. Zbl 1448.68289Bozzano, Marco; Cimatti, Alessandro; Gario, Marco; Tonetta, Stefano 4 2015 HRELTL: a temporal logic for hybrid systems. Zbl 1332.68139Cimatti, Alessandro; Roveri, Marco; Tonetta, Stefano 4 2015 Searching powerset automata by combining explicit-state and symbolic model checking. Zbl 0978.68546Cimatti, Alessandro; Roveri, Marco; Bertoli, Piergiorgio 3 2001 Bounded verification of past LTL. Zbl 1117.68424Cimatti, Alessandro; Roveri, Marco; Sheridan, Daniel 3 2004 Verifying heap-manipulating programs in an SMT framework. Zbl 1141.68484Rakamarić, Zvonimir; Bruttomesso, Roberto; Hu, Alan J.; Cimatti, Alessandro 3 2007 Integrating BDD-based and SAT-based symbolic model checking. Zbl 1057.68623Cimatti, Alessandro; Giunchiglia, Enrico; Pistore, Marco; Roveri, Marco; Sebastiani, Roberto; Tacchella, Armando 3 2002 Strong temporal planning with uncontrollable durations. Zbl 1443.68163Cimatti, Alessandro; Do, Minh; Micheli, Andrea; Roveri, Marco; Smith, David E. 3 2018 Bounded model checking for past LTL. Zbl 1031.68077Benedetti, Marco; Cimatti, Alessandro 3 2003 Encoding RTL constructs for MathSAT: a preliminary report. Zbl 1272.68230Bozzano, Marco; Bruttomesso, Roberto; Cimatti, Alessandro; Franzén, Anders; Hanna, Ziyad; Khasidashvili, Zurab; Palti, Amit; Sebastiani, Roberto 3 2006 Universal invariant checking of parametric systems with quantifier-free SMT reasoning. Zbl 07437076Cimatti, Alessandro; Griggio, Alberto; Redondi, Gianluca 3 2021 Experimenting on solving nonlinear integer arithmetic with incremental linearization. Zbl 06916318Cimatti, Alessandro; Griggio, Alberto; Irfan, Ahmed; Roveri, Marco; Sebastiani, Roberto 2 2018 Symbolic implementation of alternating automata. Zbl 1142.68418Bloem, Roderick; Cimatti, Alessandro; Pill, Ingo; Roveri, Marco 2 2007 Improving the encoding of LTL model checking into SAT. Zbl 1057.68056Cimatti, Alessandro; Pistore, Marco; Roveri, Marco; Sebastiani, Roberto 2 2002 Invariant checking of NRA transition systems via incremental reduction to LRA with EUF. Zbl 1452.68116Cimatti, Alessandro; Griggio, Alberto; Irfan, Ahmed; Roveri, Marco; Sebastiani, Roberto 2 2017 Formal specification and verification of dynamic parametrized architectures. Zbl 1460.68056Cimatti, Alessandro; Stojic, Ivan; Tonetta, Stefano 2 2018 Proving the existence of fair paths in infinite-state systems. Zbl 1472.68085Cimatti, Alessandro; Griggio, Alberto; Magnago, Enrico 2 2021 Formal reliability analysis of redundancy architectures. Zbl 1425.68039Bozzano, Marco; Cimatti, Alessandro; Mattarei, Cristian 1 2019 An SMT-based approach to weak controllability for disjunctive temporal problems with uncertainty. Zbl 1343.68237Cimatti, Alessandro; Micheli, Andrea; Roveri, Marco 1 2015 Quantifier-free encoding of invariants for hybrid systems. Zbl 1317.68111Cimatti, Alessandro; Mover, Sergio; Tonetta, Stefano 1 2014 Building efficient decision procedures on top of SAT solvers. Zbl 1182.68114Cimatti, Alessandro; Sebastiani, Roberto 1 2006 Integrating Boolean and mathematical solving: Foundations, basic algorithms, and requirements. Zbl 1072.68603Audemard, Gilles; Bertoli, Piergiorgio; Cimatti, Alessandro; Korniłowicz, Artur; Sebastiani, Roberto 1 2002 Proceedings of the 1st international workshop on Symbolic model checking (SMC ’99), as part of the 2nd federated logic conference (FLoC ’99). Trento, Italy, July 6, 1999. Zbl 0920.00044 1 1999 Formal safety assessment via contract-based design. Zbl 1448.68174Bozzano, Marco; Cimatti, Alessandro; Mattarei, Cristian; Tonetta, Stefano 1 2014 Computation of the transient in max-plus linear systems via SMT-solving. Zbl 07317096Abate, Alessandro; Cimatti, Alessandro; Micheli, Andrea; Mufid, Muhammad Syifa’ul 1 2020 Implicit semi-algebraic abstraction for polynomial dynamical systems. Zbl 1493.68217Mover, Sergio; Cimatti, Alessandro; Griggio, Alberto; Irfan, Ahmed; Tonetta, Stefano 1 2021 Universal invariant checking of parametric systems with quantifier-free SMT reasoning. Zbl 07437076Cimatti, Alessandro; Griggio, Alberto; Redondi, Gianluca 3 2021 Proving the existence of fair paths in infinite-state systems. Zbl 1472.68085Cimatti, Alessandro; Griggio, Alberto; Magnago, Enrico 2 2021 Implicit semi-algebraic abstraction for polynomial dynamical systems. Zbl 1493.68217Mover, Sergio; Cimatti, Alessandro; Griggio, Alberto; Irfan, Ahmed; Tonetta, Stefano 1 2021 Computation of the transient in max-plus linear systems via SMT-solving. Zbl 07317096Abate, Alessandro; Cimatti, Alessandro; Micheli, Andrea; Mufid, Muhammad Syifa’ul 1 2020 Formal reliability analysis of redundancy architectures. Zbl 1425.68039Bozzano, Marco; Cimatti, Alessandro; Mattarei, Cristian 1 2019 Incremental linearization for satisfiability and verification modulo nonlinear arithmetic and transcendental functions. Zbl 1407.68285Cimatti, Alessandro; Griggio, Alberto; Irfan, Ahmed; Roveri, Marco; Sebastiani, Roberto 14 2018 Strong temporal planning with uncontrollable durations. Zbl 1443.68163Cimatti, Alessandro; Do, Minh; Micheli, Andrea; Roveri, Marco; Smith, David E. 3 2018 Experimenting on solving nonlinear integer arithmetic with incremental linearization. Zbl 06916318Cimatti, Alessandro; Griggio, Alberto; Irfan, Ahmed; Roveri, Marco; Sebastiani, Roberto 2 2018 Formal specification and verification of dynamic parametrized architectures. Zbl 1460.68056Cimatti, Alessandro; Stojic, Ivan; Tonetta, Stefano 2 2018 Satisfiability modulo transcendental functions via incremental linearization. Zbl 1494.68281Cimatti, Alessandro; Griggio, Alberto; Irfan, Ahmed; Roveri, Marco; Sebastiani, Roberto 4 2017 Invariant checking of NRA transition systems via incremental reduction to LRA with EUF. Zbl 1452.68116Cimatti, Alessandro; Griggio, Alberto; Irfan, Ahmed; Roveri, Marco; Sebastiani, Roberto 2 2017 Infinite-state invariant checking with IC3 and predicate abstraction. Zbl 1368.68245Cimatti, Alessandro; Griggio, Alberto; Mover, Sergio; Tonetta, Stefano 18 2016 SC\(^2\): satisfiability checking meets symbolic computation. (Project paper). Zbl 1344.68198Ábrahám, Erika; Abbott, John; Becker, Bernd; Bigatti, Anna M.; Brain, Martin; Buchberger, Bruno; Cimatti, Alessandro; Davenport, James H.; England, Matthew; Fontaine, Pascal; Forrest, Stephen; Griggio, Alberto; Kroening, Daniel; Seiler, Werner M.; Sturm, Thomas 12 2016 Infinite-state liveness-to-safety via implicit abstraction and well-founded relations. Zbl 1411.68062Daniel, Jakub; Cimatti, Alessandro; Griggio, Alberto; Tonetta, Stefano; Mover, Sergio 6 2016 Dynamic controllability via timed game automata. Zbl 1350.68251Cimatti, Alessandro; Hunsberger, Luke; Micheli, Andrea; Posenato, Roberto; Roveri, Marco 6 2016 Solving strong controllability of temporal problems with uncertainty using SMT. Zbl 1314.90043Cimatti, Alessandro; Micheli, Andrea; Roveri, Marco 10 2015 Formal design of asynchronous fault detection and identification components using temporal epistemic logic. Zbl 1448.68289Bozzano, Marco; Cimatti, Alessandro; Gario, Marco; Tonetta, Stefano 4 2015 HRELTL: a temporal logic for hybrid systems. Zbl 1332.68139Cimatti, Alessandro; Roveri, Marco; Tonetta, Stefano 4 2015 An SMT-based approach to weak controllability for disjunctive temporal problems with uncertainty. Zbl 1343.68237Cimatti, Alessandro; Micheli, Andrea; Roveri, Marco 1 2015 Quantifier-free encoding of invariants for hybrid systems. Zbl 1317.68111Cimatti, Alessandro; Mover, Sergio; Tonetta, Stefano 1 2014 Formal safety assessment via contract-based design. Zbl 1448.68174Bozzano, Marco; Cimatti, Alessandro; Mattarei, Cristian; Tonetta, Stefano 1 2014 The MathSAT5 SMT solver. Zbl 1381.68153Cimatti, Alessandro; Griggio, Alberto; Schaafsma, Bastiaan Joost; Sebastiani, Roberto 60 2013 SMT-based scenario verification for hybrid systems. Zbl 1284.03216Cimatti, Alessandro; Mover, Sergio; Tonetta, Stefano 10 2013 A modular approach to MaxSAT modulo theories. Zbl 1390.68572Cimatti, Alessandro; Griggio, Alberto; Schaafsma, Bastiaan Joost; Sebastiani, Roberto 8 2013 Theory and applications of satisfiability testing – SAT 2012. 15th international conference, Trento, Italy, June 17–20, 2012. Proceedings. Zbl 1268.68009 6 2012 Computing small unsatisfiable cores in satisfiability modulo theories. Zbl 1216.68241Cimatti, A.; Griggio, A.; Sebastiani, R. 12 2011 Efficient generation of Craig interpolants in satisfiability modulo theories. Zbl 1351.68247Cimatti, Alessandro; Griggio, Alberto; Sebastiani, Roberto 18 2010 Satisfiability modulo the theory of costs: foundations and applications. Zbl 1284.68388Cimatti, Alessandro; Franzén, Anders; Griggio, Alberto; Sebastiani, Roberto; Stenico, Cristian 11 2010 Requirements validation for hybrid systems. Zbl 1242.68156Cimatti, Alessandro; Roveri, Marco; Tonetta, Stefano 8 2009 Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis. Zbl 1192.68627Bruttomesso, Roberto; Cimatti, Alessandro; Franzen, Anders; Griggio, Alberto; Sebastiani, Roberto 6 2009 Interpolant generation for UTVPI. Zbl 1250.68186Cimatti, Alessandro; Griggio, Alberto; Sebastiani, Roberto 5 2009 Diagnostic information for realizability. Zbl 1138.68442Cimatti, A.; Roveri, M.; Schuppan, V.; Tchaltsev, A. 42 2008 Efficient interpolant generation in satisfiability modulo theories. Zbl 1134.68402Cimatti, Alessandro; Griggio, Alberto; Sebastiani, Roberto 19 2008 A simple and flexible way of computing small unsatisfiable cores in SAT modulo theories. Zbl 1214.68348Cimatti, Alessandro; Griggio, Alberto; Sebastiani, Roberto 8 2007 Boolean abstraction for temporal logic satisfiability. Zbl 1135.68469Cimatti, Alessandro; Roveri, Marco; Schuppan, Viktor; Tonetta, Stefano 7 2007 Symbolic fault tree analysis for reactive systems. Zbl 1141.68455Bozzano, Marco; Cimatti, Alessandro; Tapparo, Francesco 4 2007 Verifying heap-manipulating programs in an SMT framework. Zbl 1141.68484Rakamarić, Zvonimir; Bruttomesso, Roberto; Hu, Alan J.; Cimatti, Alessandro 3 2007 Symbolic implementation of alternating automata. Zbl 1142.68418Bloem, Roderick; Cimatti, Alessandro; Pill, Ingo; Roveri, Marco 2 2007 Efficient theory combination via Boolean search. Zbl 1137.68578Bozzano, Marco; Bruttomesso, Roberto; Cimatti, Alessandro; Junttila, Tommi; Ranise, Silvio; Van Rossum, Peter; Sebastiani, Roberto 14 2006 Strong planning under partial observability. Zbl 1131.68095Bertoli, Piergiorgio; Cimatti, Alessandro; Roveri, Marco; Traverso, Paolo 13 2006 Symbolic implementation of alternating automata. Zbl 1160.68401Bloem, R.; Cimatti, A.; Pill, I.; Roveri, M.; Semprini, S. 7 2006 Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: A comparative analysis. Zbl 1165.68483Bruttomesso, Roberto; Cimatti, Alessandro; Franzén, Anders; Griggio, Alberto; Sebastiani, Roberto 5 2006 To Ackermann-ize or not to Ackermann-ize? On efficiently handling uninterpreted function symbols in SMT\((\mathcal{EUF} \cup \mathcal{T})\). Zbl 1165.68482Bruttomesso, Roberto; Cimatti, Alessandro; Franzén, Anders; Griggio, Alberto; Santuari, Alessandro; Sebastiani, Roberto 5 2006 Encoding RTL constructs for MathSAT: a preliminary report. Zbl 1272.68230Bozzano, Marco; Bruttomesso, Roberto; Cimatti, Alessandro; Franzén, Anders; Hanna, Ziyad; Khasidashvili, Zurab; Palti, Amit; Sebastiani, Roberto 3 2006 Building efficient decision procedures on top of SAT solvers. Zbl 1182.68114Cimatti, Alessandro; Sebastiani, Roberto 1 2006 Verifying industrial hybrid systems with MathSAT. Zbl 1272.68220Audemard, Gilles; Bozzano, Marco; Cimatti, Alessandro; Sebastiani, Roberto 15 2005 An incremental and layered procedure for the satisfiability of linear arithmetic logic. Zbl 1087.68630Bozzano, Marco; Bruttomesso, Roberto; Cimatti, Alessandro; Junttila, Tommi; van Rossum, Peter; Schulz, Stephan; Sebastiani, Roberto 10 2005 MathSAT: Tight integration of SAT and mathematical decision procedures. Zbl 1109.68101Bozzano, Marco; Bruttomesso, Roberto; Cimatti, Alessandro; Junttila, Tommi; van Rossum, Peter; Schulz, Stephan; Sebastiani, Roberto 6 2005 Efficient satisfiability modulo theories via delayed theory combination. Zbl 1081.68610Bozzano, Marco; Bruttomesso, Roberto; Cimatti, Alessandro; Junttila, Tommi; Ranise, Silvio; van Rossum, Peter; Sebastiani, Roberto 6 2005 Conformant planning via symbolic model checking and heuristic search. Zbl 1086.68591Cimatti, A.; Roveri, M.; Bertoli, P. 16 2004 Bounded verification of past LTL. Zbl 1117.68424Cimatti, Alessandro; Roveri, Marco; Sheridan, Daniel 3 2004 Weak, strong, and strong cyclic planning via symbolic model checking. Zbl 1082.68800Cimatti, A.; Pistore, M.; Roveri, M.; Traverso, P. 35 2003 Bounded model checking for past LTL. Zbl 1031.68077Benedetti, Marco; Cimatti, Alessandro 3 2003 NuSMV 2: An OpenSource tool for symbolic model checking. Zbl 1010.68766Cimatti, Alessandro; Clarke, Edmund; Giunchiglia, Enrico; Giunchiglia, Fausto; Pistore, Marco; Roveri, Marco; Sebastiani, Roberto; Tacchella, Armando 95 2002 A SAT based approach for solving formulas over Boolean and linear mathematical propositions. Zbl 1072.68562Audemard, Gilles; Bertoli, Piergiorgio; Cimatti, Alessandro; Korniłowicz, Artur; Sebastiani, Roberto 15 2002 Bounded model checking for timed systems. Zbl 1037.68549Audemard, G.; Cimatti, A.; Kornilowicz, A.; Sebastiani, R. 12 2002 Integrating BDD-based and SAT-based symbolic model checking. Zbl 1057.68623Cimatti, Alessandro; Giunchiglia, Enrico; Pistore, Marco; Roveri, Marco; Sebastiani, Roberto; Tacchella, Armando 3 2002 Improving the encoding of LTL model checking into SAT. Zbl 1057.68056Cimatti, Alessandro; Pistore, Marco; Roveri, Marco; Sebastiani, Roberto 2 2002 Integrating Boolean and mathematical solving: Foundations, basic algorithms, and requirements. Zbl 1072.68603Audemard, Gilles; Bertoli, Piergiorgio; Cimatti, Alessandro; Korniłowicz, Artur; Sebastiani, Roberto 1 2002 Industrial applications of model checking. Zbl 0985.68653Cimatti, Alessandro 5 2001 Searching powerset automata by combining explicit-state and symbolic model checking. Zbl 0978.68546Cimatti, Alessandro; Roveri, Marco; Bertoli, Piergiorgio 3 2001 NuSMV: A new symbolic model checker. Zbl 1059.68582Cimatti, Alessandro; Clarke, Edmund; Giunchiglia, Fausto; Roveri, Marco 37 2000 Conformant planning via symbolic model checking. Zbl 0963.68195Cimatti, A.; Roveri, M. 19 2000 NuSMV: A new symbolic model verifier. Zbl 1046.68587Cimatti, A.; Clarke, E.; Giunchiglia, F.; Roveri, M. 35 1999 Proceedings of the 1st international workshop on Symbolic model checking (SMC ’99), as part of the 2nd federated logic conference (FLoC ’99). Trento, Italy, July 6, 1999. Zbl 0920.00044 1 1999 all cited Publications top 5 cited Publications all top 5 Cited by 1,033 Authors 31 Cimatti, Alessandro 19 Griggio, Alberto 17 Sebastiani, Roberto 14 Roveri, Marco 12 Barrett, Clark W. 12 Tonetta, Stefano 11 Tinelli, Cesare 10 Kröning, Daniel 10 Vardi, Moshe Ya’akov 8 Ábrahám, Erika 8 Rümmer, Philipp 8 Weidenbach, Christoph 7 Bozzano, Marco 7 Davenport, James Harold 7 Kremer, Gereon 6 Abate, Alessandro 6 Bruttomesso, Roberto 6 England, Matthew 6 Irfan, Ahmed 6 Reynolds, Andrew 6 Strichman, Ofer 6 Sturm, Thomas 5 Bromberger, Martin 5 Fontaine, Pascal 5 Fränzle, Martin 5 Gheorghe, Marian 5 Giunchiglia, Enrico 5 Ipate, Florentin 5 Konur, Savas 5 Micheli, Andrea 5 Mover, Sergio 5 Ranise, Silvio 5 Sharygina, Natasha 4 Becker, Bernd 4 Bonacina, Maria Paola 4 Chatterjee, Krishnendu 4 Eggers, Andreas 4 Lefticaru, Raluca 4 Montanari, Angelo 4 Niemetz, Aina 4 Preiner, Mathias 4 Traverso, Paolo 4 Trentin, Patrick 4 Zhan, Naijun 4 Zohar, Yoni 3 Alechina, Natasha 3 Alrajeh, Dalal 3 Bersani, Marcello Maria 3 Bertoli, Piergiorgio 3 Biere, Armin 3 Bonakdarpour, Borzoo 3 Bonet, Blai 3 Brain, Martin 3 Bright, Curtis 3 Brim, Luboš 3 Cavezza, Davide Giacomo 3 Chechik, Marsha 3 Cook, Byron 3 de Moura, Leonardo 3 Déharbe, David 3 Duan, Zhenhua 3 Eiter, Thomas 3 Ganesh, Vijay 3 Geffner, Hector 3 Ghilardi, Silvio 3 Gurfinkel, Arie 3 Hyvärinen, Antti E. J. 3 Johansson, Moa 3 Jovanović, Dejan 3 Kotsireas, Ilias S. 3 Li, Jianwen 3 Liffiton, Mark H. 3 Lindauer, Marius 3 Logan, Brian 3 Lomuscio, Alessio 3 Magnago, Enrico 3 Mann, Makai 3 Maratea, Marco 3 Marques-Silva, João P. 3 Mateescu, Radu 3 Menghi, Claudio 3 Monteiro, Pedro T. 3 Nau, Dana 3 Nicolini, Enrica 3 Nieuwenhuis, Robert 3 Oliveras, Albert 3 Passerini, Andrea 3 Pu, Geguang 3 Rossi, Matteo A. C. 3 Rozier, Kristin Yvonne 3 Schuppan, Viktor 3 Teige, Tino 3 Tian, Cong 3 van de Pol, Jan Cornelis 3 Zeljić, Aleksandar 3 Zhang, Nan 2 Abbott, John A. 2 Alur, Rajeev 2 Amat, Nicolas 2 Armando, Alessandro ...and 933 more Authors all top 5 Cited in 59 Serials 44 Artificial Intelligence 43 Formal Methods in System Design 28 Journal of Automated Reasoning 25 Formal Aspects of Computing 20 Theoretical Computer Science 14 Information and Computation 12 Acta Informatica 10 Journal of Symbolic Computation 7 Constraints 6 Annals of Mathematics and Artificial Intelligence 6 Mathematics in Computer Science 5 Science of Computer Programming 5 Journal of Applied Logic 4 Journal of Computer and System Sciences 4 ACM Transactions on Computational Logic 4 Journal of Logical and Algebraic Methods in Programming 3 Discrete Event Dynamic Systems 3 The Journal of Artificial Intelligence Research (JAIR) 3 The Journal of Logic and Algebraic Programming 3 Theory and Practice of Logic Programming 3 Journal of Applied Mathematics 2 Automatica 2 Journal of Computer Science and Technology 2 International Journal of Approximate Reasoning 2 Distributed Computing 2 Cybernetics and Systems Analysis 2 Journal of Applied Non-Classical Logics 2 Fundamenta Informaticae 2 Logical Methods in Computer Science 2 Nonlinear Analysis. Hybrid Systems 2 Frontiers of Computer Science 2 Journal of Membrane Computing 1 Discrete Applied Mathematics 1 International Journal of General Systems 1 Information Processing Letters 1 Computing 1 Programming and Computer Software 1 Studia Logica 1 International Journal of Foundations of Computer Science 1 Journal of Global Optimization 1 Archives of Control Sciences 1 Journal of Heuristics 1 Theory of Computing Systems 1 Journal of Combinatorial Optimization 1 Chaos 1 Electronic Commerce Research 1 Computer Languages, Systems & Structures 1 Computational Intelligence 1 Science in China. Series F 1 Journal of Zhejiang University. Science A 1 Electronic Notes in Theoretical Computer Science 1 ACM Communications in Computer Algebra 1 Acta Universitatis Sapientiae. Informatica 1 Algorithms 1 Science China. Information Sciences 1 Symmetry 1 Computer Science Review 1 Modelirovanie i Analiz Informatsionnykh Sistem 1 Prikladnaya Diskretnaya Matematika all top 5 Cited in 25 Fields 442 Computer science (68-XX) 109 Mathematical logic and foundations (03-XX) 42 Systems theory; control (93-XX) 31 Operations research, mathematical programming (90-XX) 19 Game theory, economics, finance, and other social and behavioral sciences (91-XX) 14 Biology and other natural sciences (92-XX) 9 Information and communication theory, circuits (94-XX) 6 Combinatorics (05-XX) 6 Ordinary differential equations (34-XX) 5 Numerical analysis (65-XX) 4 Probability theory and stochastic processes (60-XX) 3 Number theory (11-XX) 3 Dynamical systems and ergodic theory (37-XX) 2 General and overarching topics; collections (00-XX) 2 Commutative algebra (13-XX) 2 Measure and integration (28-XX) 1 Field theory and polynomials (12-XX) 1 Algebraic geometry (14-XX) 1 Category theory; homological algebra (18-XX) 1 Calculus of variations and optimal control; optimization (49-XX) 1 Convex and discrete geometry (52-XX) 1 Statistics (62-XX) 1 Mechanics of particles and systems (70-XX) 1 Quantum theory (81-XX) 1 Mathematics education (97-XX) Citations by Year