| Nusmv 2: An opensource tool for symbolic model checking A Cimatti, E Clarke, E Giunchiglia, F Giunchiglia, M Pistore, M Roveri, ... Computer Aided Verification: 14th International Conference, CAV 2002 …, 2002 | 2533 | 2002 |
| Satisfiability Modulo Theories C Barrett, R Sebastiani, S Seshia, C Tinelli The Handbook of Satisfiability, 2009 | 2034* | 2009 |
| The mathsat5 smt solver A Cimatti, A Griggio, BJ Schaafsma, R Sebastiani International Conference on Tools and Algorithms for the Construction and …, 2013 | 738 | 2013 |
| Reasoning with goal models P Giorgini, J Mylopoulos, E Nicchiarelli, R Sebastiani Conceptual Modeling—ER 2002: 21st International Conference on Conceptual …, 2003 | 409 | 2003 |
| Lazy satisfiability modulo theories R Sebastiani Journal on Satisfiability, Boolean Modeling and Computation 3 (3-4), 141-224, 2007 | 367 | 2007 |
| Goal-oriented requirements analysis and reasoning in the tropos methodology P Giorgini, J Mylopoulos, R Sebastiani Engineering Applications of Artificial Intelligence 18 (2), 159-171, 2005 | 304 | 2005 |
| The MathSAT 4 SMT Solver: Tool Paper R Bruttomesso, A Cimatti, A Franzén, A Griggio, R Sebastiani Computer Aided Verification: 20th International Conference, CAV 2008 …, 2008 | 296 | 2008 |
| Formal reasoning techniques for goal models P Giorgini, J Mylopoulos, E Nicchiarelli, R Sebastiani Journal on data semantics I, 1-20, 2003 | 246 | 2003 |
| A SAT based approach for solving formulas over boolean and linear mathematical propositions G Audemard, P Bertoli, A Cimatti, A Korniłowicz, R Sebastiani International Conference on Automated Deduction, 195-210, 2002 | 230 | 2002 |
| Simple and minimum-cost satisfiability for goal models R Sebastiani, P Giorgini, J Mylopoulos Advanced Information Systems Engineering: 16th International Conference …, 2004 | 225 | 2004 |
| Software model checking via large-block encoding D Beyer, A Cimatti, A Griggio, ME Keremoglu, R Sebastiani 2009 Formal Methods in Computer-Aided Design, 25-32, 2009 | 198 | 2009 |
| Building decision procedures for modal logics from propositional decision procedures—the case study of modal K F Giunchiglia, R Sebastiani International Conference on Automated Deduction, 583-597, 1996 | 177 | 1996 |
| Bounded model checking for timed systems G Audemard, A Cimatti, A Kornilowicz, R Sebastiani International Conference on Formal Techniques for Networked and Distributed …, 2002 | 170 | 2002 |
| Verifying industrial hybrid systems with MathSAT G Audemard, M Bozzano, A Cimatti, R Sebastiani Electronic Notes in Theoretical Computer Science 119 (2), 17-32, 2005 | 144 | 2005 |
| OptiMathSAT: A tool for optimization modulo theories R Sebastiani, P Trentin International conference on computer aided verification, 447-454, 2015 | 124 | 2015 |
| Efficient interpolant generation in satisfiability modulo theories A Cimatti, A Griggio, R Sebastiani Tools and Algorithms for the Construction and Analysis of Systems: 14th …, 2008 | 115 | 2008 |
| A SAT-based decision procedure for ACC F Giunchiglia, R Sebastiani Proc. KR'96, 304-314, 1996 | 114 | 1996 |
| Efficient satisfiability modulo theories via delayed theory combination M Bozzano, R Bruttomesso, A Cimatti, T Junttila, S Ranise, P Van Rossum, ... Computer Aided Verification: 17th International Conference, CAV 2005 …, 2005 | 112 | 2005 |
| A lazy and layered SMT () solver for hard industrial verification problems R Bruttomesso, A Cimatti, A Franzén, A Griggio, Z Hanna, A Nadel, A Palti, ... International Conference on Computer Aided Verification, 547-560, 2007 | 105 | 2007 |
| Satisfiability modulo the theory of costs: Foundations and applications A Cimatti, A Franzén, A Griggio, R Sebastiani, C Stenico International Conference on Tools and Algorithms for the Construction and …, 2010 | 104 | 2010 |
| MathSAT: Tight Integration of SAT and Mathematical Decision Procedures M Bozzano, R Bruttomesso, A Cimatti, T Junttila, P Van Rossum, S Schulz, ... Journal of Automated Reasoning 35 (1), 265-293, 2005 | 103 | 2005 |
| “more deterministic” vs.“smaller” Büchi automata for efficient LTL model checking R Sebastiani, S Tonetta Correct Hardware Design and Verification Methods: 12th IFIP WG 10.5 Advanced …, 2003 | 97 | 2003 |
| Optimization in SMT with (ℚ) Cost Functions R Sebastiani, S Tomasi International Joint Conference on Automated Reasoning, 484-498, 2012 | 96 | 2012 |
| An incremental and layered procedure for the satisfiability of linear arithmetic logic M Bozzano, R Bruttomesso, A Cimatti, T Junttila, P Van Rossum, S Schulz, ... Tools and Algorithms for the Construction and Analysis of Systems: 11th …, 2005 | 95 | 2005 |
| Efficient theory combination via boolean search M Bozzano, R Bruttomesso, A Cimatti, T Junttila, S Ranise, P van Rossum, ... Information and Computation 204 (10), 1493-1525, 2006 | 93 | 2006 |
| Act, and the rest will follow: Exploiting determinism in planning as satisfiability E Giunchiglia, A Massarotto, R Sebastiani AAAI/IAAI, 948-953, 1998 | 90 | 1998 |
| Optimization modulo theories with linear rational costs R Sebastiani, S Tomasi ACM Transactions on Computational Logic (TOCL) 16 (2), 1-43, 2015 | 82 | 2015 |
| Efficient generation of Craig interpolants in satisfiability modulo theories A Cimatti, A Griggio, R Sebastiani ACM Transactions on Computational Logic (TOCL) 12 (1), 1-54, 2010 | 81 | 2010 |
| The mathsat 3 system M Bozzano, R Bruttomesso, A Cimatti, T Junttila, P Van Rossum, S Schulz, ... Automated Deduction–CADE-20: 20th International Conference on Automated …, 2005 | 77 | 2005 |
| Computing small unsatisfiable cores in satisfiability modulo theories A Cimatti, A Griggio, R Sebastiani Journal of Artificial Intelligence Research 40, 701-728, 2011 | 72 | 2011 |
| A simple and flexible way of computing small unsatisfiable cores in SAT modulo theories A Cimatti, A Griggio, R Sebastiani Theory and Applications of Satisfiability Testing–SAT 2007: 10th …, 2007 | 72 | 2007 |
| Improving the encoding of LTL model checking into SAT A Cimatti, M Pistore, M Roveri, R Sebastiani International Workshop on Verification, Model Checking, and Abstract …, 2002 | 71 | 2002 |
| A new general method to generate random modal formulae for testing decision procedures PF Patel-Schneider, R Sebastiani Journal of Artificial Intelligence Research 18, 351-389, 2003 | 70 | 2003 |
| Multi-objective reasoning with constrained goal models CM Nguyen, R Sebastiani, P Giorgini, J Mylopoulos Requirements Engineering 23, 189-225, 2018 | 69 | 2018 |
| Satisfiability modulo theories C Barrett, R Sebastiani, SA Seshia, C Tinelli | 67 | 2021 |
| Building decision procedures for modal logics from propositional decision procedures: The case study of modal K (m) F Giunchiglia, R Sebastiani Information and Computation 162 (1-2), 158-178, 2000 | 67 | 2000 |
| Integrating BDD-based and SAT-based symbolic model checking A Cimatti, E Giunchiglia, M Pistore, M Roveri, R Sebastiani, A Tacchella International Workshop on Frontiers of Combining Systems, 49-56, 2002 | 64 | 2002 |
| More evaluation of decision procedures for modal logics E Giunchiglia, F Giunchiglia, R Sebastiani, A Tacchella KR 98, 626-635, 1998 | 61 | 1998 |
| An analysis of empirical testing for modal decision procedures I Horrocks, PF Patel-Schneider, R Sebastiani Logic Journal of IGPL 8 (3), 293-323, 2000 | 60 | 2000 |
| Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis R Bruttomesso, A Cimatti, A Franzen, A Griggio, R Sebastiani Annals of Mathematics and Artificial Intelligence 55 (1), 63-99, 2009 | 59 | 2009 |
| Symbolic systems, explicit properties: on hybrid approaches for LTL symbolic model checking R Sebastiani, S Tonetta, MY Vardi Computer Aided Verification: 17th International Conference, CAV 2005 …, 2005 | 59 | 2005 |
| Applying GSATto Non-Clausal Formulas R Sebastiani Journal of Artificial Intelligence Research 1, 309-314, 1993 | 59 | 1993 |
| Axiom pinpointing in lightweight description logics via Horn-SAT encoding and conflict analysis R Sebastiani, M Vescovi International Conference on Automated Deduction, 84-99, 2009 | 57 | 2009 |
| Automated reasoning in modal and description logics via SAT encoding: the case study of K (m)/ALC-satisfiability R Sebastiani, M Vescovi Journal of Artificial Intelligence Research 35, 343-389, 2009 | 56 | 2009 |
| Applying the Davis-Putnam procedure to non-clausal formulas E Giunchiglia, R Sebastiani AI* IA 99: Advances in Artificial Intelligence: 6th Congress of Italian …, 2000 | 56 | 2000 |
| Incremental linearization for satisfiability and verification modulo nonlinear arithmetic and transcendental functions A Cimatti, A Griggio, A Irfan, M Roveri, R Sebastiani ACM Transactions on Computational Logic (TOCL) 19 (3), 1-52, 2018 | 54 | 2018 |
| Encoding RTL constructs for MathSAT: a preliminary report M Bozzano, R Bruttomesso, A Cimatti, A Franzén, Z Hanna, ... Electronic Notes in Theoretical Computer Science 144 (2), 3-14, 2006 | 50 | 2006 |
| OptiMathSAT: A tool for optimization modulo theories R Sebastiani, P Trentin Journal of Automated Reasoning 64 (3), 423-460, 2020 | 49 | 2020 |
| Structured learning modulo theories S Teso, R Sebastiani, A Passerini Artificial Intelligence 244, 166-187, 2017 | 49 | 2017 |
| SAT vs. Translation based decision procedures for modal logics: a comparative evaluation E Giunchiglia, R Sebastiani, F Giunchiglia, A Tacchella Journal of Applied Non-Classical Logics 10 (2), 145-172, 2000 | 47 | 2000 |
| Verilog2SMV: A tool for word-level verification A Irfan, A Cimatti, A Griggio, M Roveri, R Sebastiani 2016 Design, Automation & Test in Europe Conference & Exhibition (DATE …, 2016 | 45 | 2016 |
| Solving SAT (and MaxSAT) with a quantum annealer: Foundations, encodings, and preliminary results Z Bian, F Chudak, W Macready, A Roy, R Sebastiani, S Varotti Information and computation 275, 104609, 2020 | 44 | 2020 |
| Invariant checking of NRA transition systems via incremental reduction to LRA with EUF A Cimatti, A Griggio, A Irfan, M Roveri, R Sebastiani Tools and Algorithms for the Construction and Analysis of Systems: 23rd …, 2017 | 39 | 2017 |
| A modular approach to MaxSAT modulo theories A Cimatti, A Griggio, BJ Schaafsma, R Sebastiani International conference on theory and applications of satisfiability …, 2013 | 37 | 2013 |
| Applying SMT in symbolic execution of microcode A Franzén, A Cimatti, A Nadel, R Sebastiani, J Shalev Formal Methods in Computer Aided Design, 121-128, 2010 | 37 | 2010 |
| Pushing the envelope of optimization modulo theories with linear-arithmetic cost functions R Sebastiani, P Trentin International Conference on Tools and Algorithms for the Construction and …, 2015 | 36 | 2015 |
| Advanced SMT techniques for weighted model integration P Morettin, A Passerini, R Sebastiani Artificial Intelligence 275, 1-27, 2019 | 35 | 2019 |
| Efficient weighted model integration via SMT-based predicate abstraction P Morettin, A Passerini, R Sebastiani Proceedings of the 26th International Joint Conference on Artificial …, 2017 | 33 | 2017 |
| Efficient interpolant generation in satisfiability modulo linear integer arithmetic A Griggio, TTH Le, R Sebastiani Logical Methods in Computer Science 8, 2012 | 32 | 2012 |
| Interpolant generation for UTVPI A Cimatti, A Griggio, R Sebastiani International Conference on Automated Deduction, 167-182, 2009 | 32 | 2009 |
| Solving sat and maxsat with a quantum annealer: Foundations and a preliminary report Z Bian, F Chudak, W Macready, A Roy, R Sebastiani, S Varotti Frontiers of Combining Systems: 11th International Symposium, FroCoS 2017 …, 2017 | 29 | 2017 |
| GSTE is partitioned model checking R Sebastiani, E Singerman, S Tonetta, MY Vardi Computer Aided Verification: 16th International Conference, CAV 2004, Boston …, 2004 | 28 | 2004 |
| Satisfiability modulo transcendental functions via incremental linearization A Cimatti, A Griggio, A Irfan, M Roveri, R Sebastiani Automated Deduction–CADE 26: 26th International Conference on Automated …, 2017 | 27 | 2017 |
| Formal specification and development of a safety-critical train management system A Pasquini, A Chiappini, A Cimatti, C Porzia, G Rotondo, R Sebastiani, ... Computer Safety, Reliability and Security: 18th International Conference …, 1999 | 26 | 1999 |
| To Ackermann-ize or not to Ackermann-ize? On efficiently handling uninterpreted function symbols in R Bruttomesso, A Cimatti, A Franzén, A Griggio, A Santuari, R Sebastiani International Conference on Logic for Programming Artificial Intelligence …, 2006 | 25 | 2006 |
| Experimenting on solving nonlinear integer arithmetic with incremental linearization A Cimatti, A Griggio, A Irfan, M Roveri, R Sebastiani International Conference on Theory and Applications of Satisfiability …, 2018 | 24 | 2018 |
| Calculating criticalities A Bundy, F Giunchiglia, R Sebastiani, T Walsh Artificial Intelligence 88 (1-2), 39-67, 1996 | 24 | 1996 |
| Integrating boolean and mathematical solving: Foundations, basic algorithms, and requirements G Audemard, P Bertoli, A Cimatti, A Korniłowicz, R Sebastiani International Conference on Artificial Intelligence and Symbolic Computation …, 2002 | 23 | 2002 |
| Automated reasoning in via SMT V Haarslev, R Sebastiani, M Vescovi International Conference on Automated Deduction, 283-298, 2011 | 21 | 2011 |
| SAT techniques for modal and description logics R Sebastiani, A Tacchella The Handbook of Satisfiability, 2009 | 21 | 2009 |
| Integrating SAT solvers with math reasoners: Foundations and basic algorithms R Sebastiani ITC-IRST Technical report, 2001 | 21 | 2001 |
| On optimization modulo theories, MaxSMT and sorting networks R Sebastiani, P Trentin International Conference on Tools and Algorithms for the Construction and …, 2017 | 20 | 2017 |
| Axiom pinpointing in large EL+ ontologies via SAT and SMT techniques R Sebastiani, M Vescovi University of Trento, Italy, Tech. Rep. DISI-15-010, 2015 | 18 | 2015 |
| Stochastic local search for SMT: combining theory solvers with walksat A Griggio, QS Phan, R Sebastiani, S Tomasi International Symposium on Frontiers of Combining Systems, 163-178, 2011 | 18 | 2011 |
| The pywmi framework and toolbox for probabilistic inference using weighted model integration S Kolb, P Morettin, P Zuidberg Dos Martires, F Sommavilla, A Passerini, ... Proceedings of the Twenty-Eighth International Joint Conference on …, 2019 | 15 | 2019 |
| Requirements evolution and evolution requirements with constrained goal models CM Nguyen, R Sebastiani, P Giorgini, J Mylopoulos Conceptual Modeling: 35th International Conference, ER 2016, Gifu, Japan …, 2016 | 15 | 2016 |
| Encoding the Satisfiability of Modal and Description Logics into SAT: The Case Study of K (m) R Sebastiani, M Vescovi International Conference on Theory and Applications of Satisfiability …, 2006 | 15 | 2006 |
| Formal specification and validation of a vital communication protocol A Cimatti, PL Pieraccini, R Sebastiani, P Traverso, A Villafiorita FM’99—Formal Methods: World Congress on Formal Methods in the Development …, 1999 | 15 | 1999 |
| SAT-based decision procedures for normal modal logics: a theoretical framework R Sebastiani, A Villafiorita International Conference on Artificial Intelligence: Methodology, Systems …, 1998 | 15 | 1998 |
| A new method for testing decision procedures in modal logics F Giunchiglia, M Roveri, R Sebastiani Automated Deduction—CADE-14: 14th International Conference on Automated …, 1997 | 15 | 1997 |
| A new system and methodology for generating random modal formulae PF Patel-Schneider, R Sebastiani Automated Reasoning: First International Joint Conference, IJCAR 2001 Siena …, 2001 | 11 | 2001 |
| Computing abstraction hierarchies by numerical simulation A Bundy, F Giunchiglia, R Sebastiani, T Walsh University of Edinburgh, Department of Artificial Intelligence, 1996 | 11 | 1996 |
| Four flavors of entailment S Möhle, R Sebastiani, A Biere International Conference on Theory and Applications of Satisfiability …, 2020 | 10 | 2020 |
| SMT-based weighted model integration with structure awareness G Spallitta, G Masina, P Morettin, A Passerini, R Sebastiani Uncertainty in Artificial Intelligence, 1876-1885, 2022 | 9 | 2022 |
| A general purpose reasoner for abstraction F Giunchiglia, R Sebastiani, A Villafiorita, T Walsh Advances in Artifical Intelligence: 11th Biennial Conference of the Canadian …, 1996 | 9 | 1996 |
| Are You Satisfied by This Partial Assignment? R Sebastiani arXiv preprint arXiv:2003.04225, 2020 | 8 | 2020 |
| From KSAT to delayed theory combination: exploiting DPLL outside the SAT domain R Sebastiani International Symposium on Frontiers of Combining Systems, 28-46, 2007 | 8 | 2007 |
| On CNF conversion for disjoint SAT enumeration G Masina, G Spallitta, R Sebastiani 26th International Conference on Theory and Applications of Satisfiability …, 2023 | 7 | 2023 |
| Theory and Applications of Satisfiability Testing--SAT 2012: 15th International Conference, Trento, Italy, June 17-20, 2012, Proceedings A Cimatti, R Sebastiani Springer, 2012 | 7* | 2012 |
| Building efficient decision procedures on top of SAT solvers A Cimatti, R Sebastiani International School on Formal Methods for the Design of Computer …, 2006 | 7 | 2006 |
| On enumerating short projected models S Möhle, R Sebastiani, A Biere arXiv preprint arXiv:2110.12924, 2021 | 6 | 2021 |
| Modeling and reasoning on requirements evolution with constrained goal models CM Nguyen, R Sebastiani, P Giorgini, J Mylopoulos Software Engineering and Formal Methods: 15th International Conference, SEFM …, 2017 | 6 | 2017 |
| NuSMV Version 2: BDD-based+ SAT-based symbolic model checking A Cimatti, E Giunchiglia, M Pistore, M Roveri, R Sebastiani, A Tacchella Unpublished. Available at www. mrg. dist. unige. it/enrico, 2001 | 6 | 2001 |
| New upper bounds for satisfiability in modal logics-the case-study of modal K R Sebastiani, D McAllester Technical Report 9710-15, 1997 | 6 | 1997 |
| From MiniZinc to Optimization Modulo Theories, and Back F Contaldo, P Trentin, R Sebastiani Integration of Constraint Programming, Artificial Intelligence, and …, 2020 | 5 | 2020 |
| Optimization modulo the theory of floating-point numbers P Trentin, R Sebastiani International Conference on Automated Deduction, 550-567, 2019 | 5 | 2019 |
| Symbolic systems, explicit properties: on hybrid approaches for LTL symbolic model checking R Sebastiani, S Tonetta, MY Vardi International journal on software tools for technology transfer 13, 319-335, 2011 | 5 | 2011 |
| Property-driven partitioning for abstraction refinement R Sebastiani, S Tonetta, MY Vardi Tools and Algorithms for the Construction and Analysis of Systems: 13th …, 2007 | 5 | 2007 |
| The MathSat solver–a progress report M Bozzano, A Cimatti, G Colombini, V Kirov, R Sebastiani Proc. Workhop on Pragmatics of Decision Procedures in Automated Reasoning …, 2004 | 5 | 2004 |
| A SAT-based decision procedure for Ф F Giunchiglia, R Sebastiani Principles of Knowledge Representation and Reasoning: Proceedings of the …, 0 | 5 | |
Alessandro CimattiFondazione Bruno KesslerVerified email at fbk.eu
