×

Cimatti, Alessandro

Author ID: cimatti.alessandro Recent zbMATH articles by "Cimatti, Alessandro"
Published as: Cimatti, Alessandro; Cimatti, A.
all top 5

Co-Authors

1 single-authored
32 Roveri, Marco
31 Griggio, Alberto
31 Sebastiani, Roberto
22 Tonetta, Stefano
14 Bozzano, Marco
9 Bruttomesso, Roberto
9 Mover, Sergio
7 Micheli, Andrea
6 Bertoli, Piergiorgio
6 Irfan, Ahmed
5 Franzén, Anders
5 Geatti, Luca
4 Audemard, Gilles
4 Gigante, Nicola
4 Giunchiglia, Fausto
4 Junttila, Tommi A.
4 Magnago, Enrico
4 Montanari, Angelo
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 Abate, Alessandro
2 Abbott, John A.
2 Ábrahám, Erika
2 Becchi, Anna
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 Jonáš, Martin
2 Kimberly, Greg
2 Kröning, Daniel
2 Mufid, Muhammad Syifa’ul
2 Narasamdya, Iman
2 Pill, Ingo
2 Ranise, Silvio
2 Redondi, Gianluca
2 Schaafsma, Bastiaan Joost
2 Schulz, Stephan
2 Schuppan, Viktor
2 Seiler, Werner M.
2 Serafini, Luciano
2 Sturm, Thomas
2 Tacchella, Armando
1 Armando, Alessandro
1 Benedetti, Marco H.
1 Benerecetti, Massimo
1 Bernardo, Marco
1 Bigarella, Filippo
1 Bittner, Benjamin
1 Bliudze, Simon
1 Cashmore, Michael
1 Daniel, Jakub
1 Demasi, Ramiro
1 Grumberg, Orna
1 Hanna, Ziyad
1 Hu, Alan J.
1 Hunsberger, Luke
1 Jaber, Mohamad Y.
1 Khasidashvili, Zurab O.
1 Lipparini, Enrico
1 Magazzeni, Daniele
1 Mongardi, Giovanni
1 Palti, Amit
1 Posenato, Roberto
1 Rakamarić, Zvonimir
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 Tian, Chun
1 Torielli, F.
1 Trentin, Patrick
1 Vozarova, Viktoria
1 Wang, Qiang
1 Zaffanella, Enea
1 Zehtabi, Parisa

Publications by Year

Citations contained in zbMATH Open

74 Publications have been cited 833 times in 569 Documents Cited by Year
NuSMV 2: An OpenSource tool for symbolic model checking. Zbl 1010.68766
Cimatti, Alessandro; Clarke, Edmund; Giunchiglia, Enrico; Giunchiglia, Fausto; Pistore, Marco; Roveri, Marco; Sebastiani, Roberto; Tacchella, Armando
114
2002
The MathSAT5 SMT solver. Zbl 1381.68153
Cimatti, Alessandro; Griggio, Alberto; Schaafsma, Bastiaan Joost; Sebastiani, Roberto
76
2013
NuSMV: A new symbolic model checker. Zbl 1059.68582
Cimatti, Alessandro; Clarke, Edmund; Giunchiglia, Fausto; Roveri, Marco
47
2000
Diagnostic information for realizability. Zbl 1138.68442
Cimatti, A.; Roveri, M.; Schuppan, V.; Tchaltsev, A.
43
2008
Weak, strong, and strong cyclic planning via symbolic model checking. Zbl 1082.68800
Cimatti, A.; Pistore, M.; Roveri, M.; Traverso, P.
42
2003
NuSMV: A new symbolic model verifier. Zbl 1046.68587
Cimatti, A.; Clarke, E.; Giunchiglia, F.; Roveri, M.
37
1999
Infinite-state invariant checking with IC3 and predicate abstraction. Zbl 1368.68245
Cimatti, Alessandro; Griggio, Alberto; Mover, Sergio; Tonetta, Stefano
27
2016
Efficient interpolant generation in satisfiability modulo theories. Zbl 1134.68402
Cimatti, Alessandro; Griggio, Alberto; Sebastiani, Roberto
21
2008
Conformant planning via symbolic model checking. Zbl 0963.68195
Cimatti, A.; Roveri, M.
20
2000
Verifying industrial hybrid systems with MathSAT. Zbl 1272.68220
Audemard, Gilles; Bozzano, Marco; Cimatti, Alessandro; Sebastiani, Roberto
20
2005
Efficient generation of Craig interpolants in satisfiability modulo theories. Zbl 1351.68247
Cimatti, Alessandro; Griggio, Alberto; Sebastiani, Roberto
19
2010
Incremental linearization for satisfiability and verification modulo nonlinear arithmetic and transcendental functions. Zbl 1407.68285
Cimatti, Alessandro; Griggio, Alberto; Irfan, Ahmed; Roveri, Marco; Sebastiani, Roberto
19
2018
Efficient theory combination via Boolean search. Zbl 1137.68578
Bozzano, Marco; Bruttomesso, Roberto; Cimatti, Alessandro; Junttila, Tommi; Ranise, Silvio; Van Rossum, Peter; Sebastiani, Roberto
17
2006
Conformant planning via symbolic model checking and heuristic search. Zbl 1086.68591
Cimatti, A.; Roveri, M.; Bertoli, P.
16
2004
A SAT based approach for solving formulas over Boolean and linear mathematical propositions. Zbl 1072.68562
Audemard, Gilles; Bertoli, Piergiorgio; Cimatti, Alessandro; Korniłowicz, Artur; Sebastiani, Roberto
16
2002
Strong planning under partial observability. Zbl 1131.68095
Bertoli, Piergiorgio; Cimatti, Alessandro; Roveri, Marco; Traverso, Paolo
15
2006
Bounded model checking for timed systems. Zbl 1037.68549
Audemard, G.; Cimatti, A.; Kornilowicz, A.; Sebastiani, R.
14
2002
Solving strong controllability of temporal problems with uncertainty using SMT. Zbl 1314.90043
Cimatti, Alessandro; Micheli, Andrea; Roveri, Marco
13
2015
Computing small unsatisfiable cores in satisfiability modulo theories. Zbl 1216.68241
Cimatti, A.; Griggio, A.; Sebastiani, R.
13
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
13
2016
SMT-based scenario verification for hybrid systems. Zbl 1284.03216
Cimatti, Alessandro; Mover, Sergio; Tonetta, Stefano
11
2013
Satisfiability modulo the theory of costs: foundations and applications. Zbl 1284.68388
Cimatti, Alessandro; Franzén, Anders; Griggio, Alberto; Sebastiani, Roberto; Stenico, Cristian
11
2010
An incremental and layered procedure for the satisfiability of linear arithmetic logic. Zbl 1087.68630
Bozzano, Marco; Bruttomesso, Roberto; Cimatti, Alessandro; Junttila, Tommi; van Rossum, Peter; Schulz, Stephan; Sebastiani, Roberto
10
2005
Infinite-state liveness-to-safety via implicit abstraction and well-founded relations. Zbl 1411.68062
Daniel, Jakub; Cimatti, Alessandro; Griggio, Alberto; Tonetta, Stefano; Mover, Sergio
9
2016
A simple and flexible way of computing small unsatisfiable cores in SAT modulo theories. Zbl 1214.68348
Cimatti, Alessandro; Griggio, Alberto; Sebastiani, Roberto
8
2007
MathSAT: Tight integration of SAT and mathematical decision procedures. Zbl 1109.68101
Bozzano, Marco; Bruttomesso, Roberto; Cimatti, Alessandro; Junttila, Tommi; van Rossum, Peter; Schulz, Stephan; Sebastiani, Roberto
8
2005
Efficient satisfiability modulo theories via delayed theory combination. Zbl 1081.68610
Bozzano, Marco; Bruttomesso, Roberto; Cimatti, Alessandro; Junttila, Tommi; Ranise, Silvio; van Rossum, Peter; Sebastiani, Roberto
8
2005
Symbolic implementation of alternating automata. Zbl 1160.68401
Bloem, R.; Cimatti, A.; Pill, I.; Roveri, M.; Semprini, S.
8
2006
Boolean abstraction for temporal logic satisfiability. Zbl 1135.68469
Cimatti, Alessandro; Roveri, Marco; Schuppan, Viktor; Tonetta, Stefano
8
2007
Requirements validation for hybrid systems. Zbl 1242.68156
Cimatti, Alessandro; Roveri, Marco; Tonetta, Stefano
8
2009
A modular approach to MaxSAT modulo theories. Zbl 1390.68572
Cimatti, Alessandro; Griggio, Alberto; Schaafsma, Bastiaan Joost; Sebastiani, Roberto
8
2013
Dynamic controllability via timed game automata. Zbl 1350.68251
Cimatti, Alessandro; Hunsberger, Luke; Micheli, Andrea; Posenato, Roberto; Roveri, Marco
8
2016
Interpolant generation for UTVPI. Zbl 1250.68186
Cimatti, Alessandro; Griggio, Alberto; Sebastiani, Roberto
7
2009
Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: A comparative analysis. Zbl 1165.68483
Bruttomesso, Roberto; Cimatti, Alessandro; Franzén, Anders; Griggio, Alberto; Sebastiani, Roberto
7
2006
To Ackermann-ize or not to Ackermann-ize? On efficiently handling uninterpreted function symbols in SMT\((\mathcal{EUF} \cup \mathcal{T})\). Zbl 1165.68482
Bruttomesso, Roberto; Cimatti, Alessandro; Franzén, Anders; Griggio, Alberto; Santuari, Alessandro; Sebastiani, Roberto
7
2006
Industrial applications of model checking. Zbl 0985.68653
Cimatti, Alessandro
6
2001
Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis. Zbl 1192.68627
Bruttomesso, 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
Bounded model checking for past LTL. Zbl 1031.68077
Benedetti, Marco; Cimatti, Alessandro
5
2003
Symbolic fault tree analysis for reactive systems. Zbl 1141.68455
Bozzano, Marco; Cimatti, Alessandro; Tapparo, Francesco
5
2007
Universal invariant checking of parametric systems with quantifier-free SMT reasoning. Zbl 07437076
Cimatti, Alessandro; Griggio, Alberto; Redondi, Gianluca
5
2021
Formal design of asynchronous fault detection and identification components using temporal epistemic logic. Zbl 1448.68289
Bozzano, Marco; Cimatti, Alessandro; Gario, Marco; Tonetta, Stefano
4
2015
HRELTL: a temporal logic for hybrid systems. Zbl 1332.68139
Cimatti, Alessandro; Roveri, Marco; Tonetta, Stefano
4
2015
Satisfiability modulo transcendental functions via incremental linearization. Zbl 1494.68281
Cimatti, Alessandro; Griggio, Alberto; Irfan, Ahmed; Roveri, Marco; Sebastiani, Roberto
4
2017
Bounded verification of past LTL. Zbl 1117.68424
Cimatti, Alessandro; Roveri, Marco; Sheridan, Daniel
4
2004
Formal specification and verification of dynamic parametrized architectures. Zbl 1460.68056
Cimatti, Alessandro; Stojic, Ivan; Tonetta, Stefano
4
2018
Proving the existence of fair paths in infinite-state systems. Zbl 1472.68085
Cimatti, Alessandro; Griggio, Alberto; Magnago, Enrico
4
2021
Invariant checking of NRA transition systems via incremental reduction to LRA with EUF. Zbl 1452.68116
Cimatti, Alessandro; Griggio, Alberto; Irfan, Ahmed; Roveri, Marco; Sebastiani, Roberto
4
2017
Searching powerset automata by combining explicit-state and symbolic model checking. Zbl 0978.68546
Cimatti, Alessandro; Roveri, Marco; Bertoli, Piergiorgio
3
2001
Verifying heap-manipulating programs in an SMT framework. Zbl 1141.68484
Rakamarić, Zvonimir; Bruttomesso, Roberto; Hu, Alan J.; Cimatti, Alessandro
3
2007
Improving the encoding of LTL model checking into SAT. Zbl 1057.68056
Cimatti, Alessandro; Pistore, Marco; Roveri, Marco; Sebastiani, Roberto
3
2002
Integrating BDD-based and SAT-based symbolic model checking. Zbl 1057.68623
Cimatti, Alessandro; Giunchiglia, Enrico; Pistore, Marco; Roveri, Marco; Sebastiani, Roberto; Tacchella, Armando
3
2002
Encoding RTL constructs for MathSAT: a preliminary report. Zbl 1272.68230
Bozzano, Marco; Bruttomesso, Roberto; Cimatti, Alessandro; Franzén, Anders; Hanna, Ziyad; Khasidashvili, Zurab; Palti, Amit; Sebastiani, Roberto
3
2006
Strong temporal planning with uncontrollable durations. Zbl 1443.68163
Cimatti, Alessandro; Do, Minh; Micheli, Andrea; Roveri, Marco; Smith, David E.
3
2018
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
2
1999
Symbolic implementation of alternating automata. Zbl 1142.68418
Bloem, Roderick; Cimatti, Alessandro; Pill, Ingo; Roveri, Marco
2
2007
Quantifier-free encoding of invariants for hybrid systems. Zbl 1317.68111
Cimatti, Alessandro; Mover, Sergio; Tonetta, Stefano
2
2014
Automatic discovery of fair paths in infinite-state transition systems. Zbl 1497.68290
Cimatti, Alessandro; Griggio, Alberto; Magnago, Enrico
2
2021
SMT-based satisfiability of first-order LTL with event freezing functions and metric operators. Zbl 1443.68104
Cimatti, Alessandro; Griggio, Alberto; Magnago, Enrico; Roveri, Marco; Tonetta, Stefano
2
2020
Experimenting on solving nonlinear integer arithmetic with incremental linearization. Zbl 1511.68244
Cimatti, Alessandro; Griggio, Alberto; Irfan, Ahmed; Roveri, Marco; Sebastiani, Roberto
2
2018
An SMT-based approach to weak controllability for disjunctive temporal problems with uncertainty. Zbl 1343.68237
Cimatti, Alessandro; Micheli, Andrea; Roveri, Marco
1
2015
Formal safety assessment via contract-based design. Zbl 1448.68174
Bozzano, Marco; Cimatti, Alessandro; Mattarei, Cristian; Tonetta, Stefano
1
2014
Software engineering and formal methods. 15th international conference, SEFM 2017, Trento, Italy, September 4–8, 2017. Proceedings. Zbl 1369.68017
1
2017
Building efficient decision procedures on top of SAT solvers. Zbl 1182.68114
Cimatti, Alessandro; Sebastiani, Roberto
1
2006
Integrating Boolean and mathematical solving: Foundations, basic algorithms, and requirements. Zbl 1072.68603
Audemard, Gilles; Bertoli, Piergiorgio; Cimatti, Alessandro; Korniłowicz, Artur; Sebastiani, Roberto
1
2002
Model-based safety assessment of a triple modular generator with xSAP. Zbl 1511.68149
Bozzano, Marco; Cimatti, Alessandro; Gario, Marco; Jones, David; Mattarei, Cristian
1
2021
A first-order logic characterization of safety and co-safety languages. Zbl 07731941
Cimatti, Alessandro; Geatti, Luca; Gigante, Nicola; Montanari, Angelo; Tonetta, Stefano
1
2023
Optimization modulo non-linear arithmetic via incremental linearization. Zbl 07497924
Bigarella, Filippo; Cimatti, Alessandro; Griggio, Alberto; Irfan, Ahmed; Jonáš, Martin; Roveri, Marco; Sebastiani, Roberto; Trentin, Patrick
1
2021
Implicit semi-algebraic abstraction for polynomial dynamical systems. Zbl 1493.68217
Mover, Sergio; Cimatti, Alessandro; Griggio, Alberto; Irfan, Ahmed; Tonetta, Stefano
1
2021
LTL falsification in infinite-state systems. Zbl 07629158
Cimatti, Alessandro; Griggio, Alberto; Magnago, Enrico
1
2022
Computation of the transient in max-plus linear systems via SMT-solving. Zbl 07317096
Abate, Alessandro; Cimatti, Alessandro; Micheli, Andrea; Mufid, Muhammad Syifa’ul
1
2020
From electrical switched networks to hybrid automata. Zbl 1427.94116
Cimatti, Alessandro; Mover, Sergio; Sessa, Mirko
1
2016
Synthesis of P-stable abstractions. Zbl 1476.68059
Becchi, Anna; Cimatti, Alessandro; Zaffanella, Enea
1
2020
Formal reliability analysis of redundancy architectures. Zbl 1425.68039
Bozzano, Marco; Cimatti, Alessandro; Mattarei, Cristian
1
2019
A first-order logic characterization of safety and co-safety languages. Zbl 07731941
Cimatti, Alessandro; Geatti, Luca; Gigante, Nicola; Montanari, Angelo; Tonetta, Stefano
1
2023
LTL falsification in infinite-state systems. Zbl 07629158
Cimatti, Alessandro; Griggio, Alberto; Magnago, Enrico
1
2022
Universal invariant checking of parametric systems with quantifier-free SMT reasoning. Zbl 07437076
Cimatti, Alessandro; Griggio, Alberto; Redondi, Gianluca
5
2021
Proving the existence of fair paths in infinite-state systems. Zbl 1472.68085
Cimatti, Alessandro; Griggio, Alberto; Magnago, Enrico
4
2021
Automatic discovery of fair paths in infinite-state transition systems. Zbl 1497.68290
Cimatti, Alessandro; Griggio, Alberto; Magnago, Enrico
2
2021
Model-based safety assessment of a triple modular generator with xSAP. Zbl 1511.68149
Bozzano, Marco; Cimatti, Alessandro; Gario, Marco; Jones, David; Mattarei, Cristian
1
2021
Optimization modulo non-linear arithmetic via incremental linearization. Zbl 07497924
Bigarella, Filippo; Cimatti, Alessandro; Griggio, Alberto; Irfan, Ahmed; Jonáš, Martin; Roveri, Marco; Sebastiani, Roberto; Trentin, Patrick
1
2021
Implicit semi-algebraic abstraction for polynomial dynamical systems. Zbl 1493.68217
Mover, Sergio; Cimatti, Alessandro; Griggio, Alberto; Irfan, Ahmed; Tonetta, Stefano
1
2021
SMT-based satisfiability of first-order LTL with event freezing functions and metric operators. Zbl 1443.68104
Cimatti, Alessandro; Griggio, Alberto; Magnago, Enrico; Roveri, Marco; Tonetta, Stefano
2
2020
Computation of the transient in max-plus linear systems via SMT-solving. Zbl 07317096
Abate, Alessandro; Cimatti, Alessandro; Micheli, Andrea; Mufid, Muhammad Syifa’ul
1
2020
Synthesis of P-stable abstractions. Zbl 1476.68059
Becchi, Anna; Cimatti, Alessandro; Zaffanella, Enea
1
2020
Formal reliability analysis of redundancy architectures. Zbl 1425.68039
Bozzano, Marco; Cimatti, Alessandro; Mattarei, Cristian
1
2019
Incremental linearization for satisfiability and verification modulo nonlinear arithmetic and transcendental functions. Zbl 1407.68285
Cimatti, Alessandro; Griggio, Alberto; Irfan, Ahmed; Roveri, Marco; Sebastiani, Roberto
19
2018
Formal specification and verification of dynamic parametrized architectures. Zbl 1460.68056
Cimatti, Alessandro; Stojic, Ivan; Tonetta, Stefano
4
2018
Strong temporal planning with uncontrollable durations. Zbl 1443.68163
Cimatti, Alessandro; Do, Minh; Micheli, Andrea; Roveri, Marco; Smith, David E.
3
2018
Experimenting on solving nonlinear integer arithmetic with incremental linearization. Zbl 1511.68244
Cimatti, Alessandro; Griggio, Alberto; Irfan, Ahmed; Roveri, Marco; Sebastiani, Roberto
2
2018
Satisfiability modulo transcendental functions via incremental linearization. Zbl 1494.68281
Cimatti, 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.68116
Cimatti, Alessandro; Griggio, Alberto; Irfan, Ahmed; Roveri, Marco; Sebastiani, Roberto
4
2017
Software engineering and formal methods. 15th international conference, SEFM 2017, Trento, Italy, September 4–8, 2017. Proceedings. Zbl 1369.68017
1
2017
Infinite-state invariant checking with IC3 and predicate abstraction. Zbl 1368.68245
Cimatti, Alessandro; Griggio, Alberto; Mover, Sergio; Tonetta, Stefano
27
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
13
2016
Infinite-state liveness-to-safety via implicit abstraction and well-founded relations. Zbl 1411.68062
Daniel, Jakub; Cimatti, Alessandro; Griggio, Alberto; Tonetta, Stefano; Mover, Sergio
9
2016
Dynamic controllability via timed game automata. Zbl 1350.68251
Cimatti, Alessandro; Hunsberger, Luke; Micheli, Andrea; Posenato, Roberto; Roveri, Marco
8
2016
From electrical switched networks to hybrid automata. Zbl 1427.94116
Cimatti, Alessandro; Mover, Sergio; Sessa, Mirko
1
2016
Solving strong controllability of temporal problems with uncertainty using SMT. Zbl 1314.90043
Cimatti, Alessandro; Micheli, Andrea; Roveri, Marco
13
2015
Formal design of asynchronous fault detection and identification components using temporal epistemic logic. Zbl 1448.68289
Bozzano, Marco; Cimatti, Alessandro; Gario, Marco; Tonetta, Stefano
4
2015
HRELTL: a temporal logic for hybrid systems. Zbl 1332.68139
Cimatti, Alessandro; Roveri, Marco; Tonetta, Stefano
4
2015
An SMT-based approach to weak controllability for disjunctive temporal problems with uncertainty. Zbl 1343.68237
Cimatti, Alessandro; Micheli, Andrea; Roveri, Marco
1
2015
Quantifier-free encoding of invariants for hybrid systems. Zbl 1317.68111
Cimatti, Alessandro; Mover, Sergio; Tonetta, Stefano
2
2014
Formal safety assessment via contract-based design. Zbl 1448.68174
Bozzano, Marco; Cimatti, Alessandro; Mattarei, Cristian; Tonetta, Stefano
1
2014
The MathSAT5 SMT solver. Zbl 1381.68153
Cimatti, Alessandro; Griggio, Alberto; Schaafsma, Bastiaan Joost; Sebastiani, Roberto
76
2013
SMT-based scenario verification for hybrid systems. Zbl 1284.03216
Cimatti, Alessandro; Mover, Sergio; Tonetta, Stefano
11
2013
A modular approach to MaxSAT modulo theories. Zbl 1390.68572
Cimatti, 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.68241
Cimatti, A.; Griggio, A.; Sebastiani, R.
13
2011
Efficient generation of Craig interpolants in satisfiability modulo theories. Zbl 1351.68247
Cimatti, Alessandro; Griggio, Alberto; Sebastiani, Roberto
19
2010
Satisfiability modulo the theory of costs: foundations and applications. Zbl 1284.68388
Cimatti, Alessandro; Franzén, Anders; Griggio, Alberto; Sebastiani, Roberto; Stenico, Cristian
11
2010
Requirements validation for hybrid systems. Zbl 1242.68156
Cimatti, Alessandro; Roveri, Marco; Tonetta, Stefano
8
2009
Interpolant generation for UTVPI. Zbl 1250.68186
Cimatti, Alessandro; Griggio, Alberto; Sebastiani, Roberto
7
2009
Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis. Zbl 1192.68627
Bruttomesso, Roberto; Cimatti, Alessandro; Franzen, Anders; Griggio, Alberto; Sebastiani, Roberto
6
2009
Diagnostic information for realizability. Zbl 1138.68442
Cimatti, A.; Roveri, M.; Schuppan, V.; Tchaltsev, A.
43
2008
Efficient interpolant generation in satisfiability modulo theories. Zbl 1134.68402
Cimatti, Alessandro; Griggio, Alberto; Sebastiani, Roberto
21
2008
A simple and flexible way of computing small unsatisfiable cores in SAT modulo theories. Zbl 1214.68348
Cimatti, Alessandro; Griggio, Alberto; Sebastiani, Roberto
8
2007
Boolean abstraction for temporal logic satisfiability. Zbl 1135.68469
Cimatti, Alessandro; Roveri, Marco; Schuppan, Viktor; Tonetta, Stefano
8
2007
Symbolic fault tree analysis for reactive systems. Zbl 1141.68455
Bozzano, Marco; Cimatti, Alessandro; Tapparo, Francesco
5
2007
Verifying heap-manipulating programs in an SMT framework. Zbl 1141.68484
Rakamarić, Zvonimir; Bruttomesso, Roberto; Hu, Alan J.; Cimatti, Alessandro
3
2007
Symbolic implementation of alternating automata. Zbl 1142.68418
Bloem, Roderick; Cimatti, Alessandro; Pill, Ingo; Roveri, Marco
2
2007
Efficient theory combination via Boolean search. Zbl 1137.68578
Bozzano, Marco; Bruttomesso, Roberto; Cimatti, Alessandro; Junttila, Tommi; Ranise, Silvio; Van Rossum, Peter; Sebastiani, Roberto
17
2006
Strong planning under partial observability. Zbl 1131.68095
Bertoli, Piergiorgio; Cimatti, Alessandro; Roveri, Marco; Traverso, Paolo
15
2006
Symbolic implementation of alternating automata. Zbl 1160.68401
Bloem, R.; Cimatti, A.; Pill, I.; Roveri, M.; Semprini, S.
8
2006
Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: A comparative analysis. Zbl 1165.68483
Bruttomesso, Roberto; Cimatti, Alessandro; Franzén, Anders; Griggio, Alberto; Sebastiani, Roberto
7
2006
To Ackermann-ize or not to Ackermann-ize? On efficiently handling uninterpreted function symbols in SMT\((\mathcal{EUF} \cup \mathcal{T})\). Zbl 1165.68482
Bruttomesso, Roberto; Cimatti, Alessandro; Franzén, Anders; Griggio, Alberto; Santuari, Alessandro; Sebastiani, Roberto
7
2006
Encoding RTL constructs for MathSAT: a preliminary report. Zbl 1272.68230
Bozzano, 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.68114
Cimatti, Alessandro; Sebastiani, Roberto
1
2006
Verifying industrial hybrid systems with MathSAT. Zbl 1272.68220
Audemard, Gilles; Bozzano, Marco; Cimatti, Alessandro; Sebastiani, Roberto
20
2005
An incremental and layered procedure for the satisfiability of linear arithmetic logic. Zbl 1087.68630
Bozzano, 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.68101
Bozzano, Marco; Bruttomesso, Roberto; Cimatti, Alessandro; Junttila, Tommi; van Rossum, Peter; Schulz, Stephan; Sebastiani, Roberto
8
2005
Efficient satisfiability modulo theories via delayed theory combination. Zbl 1081.68610
Bozzano, Marco; Bruttomesso, Roberto; Cimatti, Alessandro; Junttila, Tommi; Ranise, Silvio; van Rossum, Peter; Sebastiani, Roberto
8
2005
Conformant planning via symbolic model checking and heuristic search. Zbl 1086.68591
Cimatti, A.; Roveri, M.; Bertoli, P.
16
2004
Bounded verification of past LTL. Zbl 1117.68424
Cimatti, Alessandro; Roveri, Marco; Sheridan, Daniel
4
2004
Weak, strong, and strong cyclic planning via symbolic model checking. Zbl 1082.68800
Cimatti, A.; Pistore, M.; Roveri, M.; Traverso, P.
42
2003
Bounded model checking for past LTL. Zbl 1031.68077
Benedetti, Marco; Cimatti, Alessandro
5
2003
NuSMV 2: An OpenSource tool for symbolic model checking. Zbl 1010.68766
Cimatti, Alessandro; Clarke, Edmund; Giunchiglia, Enrico; Giunchiglia, Fausto; Pistore, Marco; Roveri, Marco; Sebastiani, Roberto; Tacchella, Armando
114
2002
A SAT based approach for solving formulas over Boolean and linear mathematical propositions. Zbl 1072.68562
Audemard, Gilles; Bertoli, Piergiorgio; Cimatti, Alessandro; Korniłowicz, Artur; Sebastiani, Roberto
16
2002
Bounded model checking for timed systems. Zbl 1037.68549
Audemard, G.; Cimatti, A.; Kornilowicz, A.; Sebastiani, R.
14
2002
Improving the encoding of LTL model checking into SAT. Zbl 1057.68056
Cimatti, Alessandro; Pistore, Marco; Roveri, Marco; Sebastiani, Roberto
3
2002
Integrating BDD-based and SAT-based symbolic model checking. Zbl 1057.68623
Cimatti, Alessandro; Giunchiglia, Enrico; Pistore, Marco; Roveri, Marco; Sebastiani, Roberto; Tacchella, Armando
3
2002
Integrating Boolean and mathematical solving: Foundations, basic algorithms, and requirements. Zbl 1072.68603
Audemard, Gilles; Bertoli, Piergiorgio; Cimatti, Alessandro; Korniłowicz, Artur; Sebastiani, Roberto
1
2002
Industrial applications of model checking. Zbl 0985.68653
Cimatti, Alessandro
6
2001
Searching powerset automata by combining explicit-state and symbolic model checking. Zbl 0978.68546
Cimatti, Alessandro; Roveri, Marco; Bertoli, Piergiorgio
3
2001
NuSMV: A new symbolic model checker. Zbl 1059.68582
Cimatti, Alessandro; Clarke, Edmund; Giunchiglia, Fausto; Roveri, Marco
47
2000
Conformant planning via symbolic model checking. Zbl 0963.68195
Cimatti, A.; Roveri, M.
20
2000
NuSMV: A new symbolic model verifier. Zbl 1046.68587
Cimatti, A.; Clarke, E.; Giunchiglia, F.; Roveri, M.
37
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
2
1999
all top 5

Cited by 1,182 Authors

42 Cimatti, Alessandro
25 Griggio, Alberto
19 Sebastiani, Roberto
16 Roveri, Marco
15 Tonetta, Stefano
14 Vardi, Moshe Ya’akov
12 Barrett, Clark W.
11 Kröning, Daniel
11 Tinelli, Cesare
9 Ábrahám, Erika
9 Bozzano, Marco
8 Abate, Alessandro
8 Bruttomesso, Roberto
8 Davenport, James Harold
8 Rümmer, Philipp
8 Weidenbach, Christoph
7 England, Matthew
7 Fränzle, Martin
7 Ghilardi, Silvio
7 Kremer, Gereon
7 Ranise, Silvio
6 Gheorghe, Marian
6 Ipate, Florentin
6 Irfan, Ahmed
6 Konur, Savas
6 Micheli, Andrea
6 Montanari, Angelo
6 Mover, Sergio
6 Reynolds, Andrew
6 Sharygina, Natasha
6 Strichman, Ofer
6 Sturm, Thomas
5 Bonacina, Maria Paola
5 Bromberger, Martin
5 Chatterjee, Krishnendu
5 Fontaine, Pascal
5 Giunchiglia, Enrico
5 Lefticaru, Raluca
5 Zavatteri, Matteo
4 Becker, Bernd
4 De Angelis, Emanuele
4 Eggers, Andreas
4 Fioravanti, Fabio
4 Gigante, Nicola
4 Menghi, Claudio
4 Nicolini, Enrica
4 Niemetz, Aina
4 Pettorossi, Alberto
4 Preiner, Mathias
4 Proietti, Maurizio
4 Schuppan, Viktor
4 Teige, Tino
4 Traverso, Paolo
4 Trentin, Patrick
4 Zhan, Naijun
4 Zohar, Yoni
3 Alechina, Natasha
3 Alrajeh, Dalal
3 Belle, Vaishak
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 Brown, Christopher W.
3 Cavezza, Davide Giacomo
3 Chechik, Marsha
3 Ciardo, Gianfranco
3 Clarke, Edmund Melson jun.
3 Comet, Jean-Paul
3 Cook, Byron
3 de Moura, Leonardo
3 Déharbe, David
3 Duan, Zhenhua
3 Eiter, Thomas
3 Ganesh, Vijay
3 Geffner, Hector
3 Gurfinkel, Arie
3 Hoffmann, Jörg
3 Hyvärinen, Antti E. J.
3 Johansson, Moa
3 Jovanović, Dejan
3 Kapur, Deepak
3 Katoen, Joost-Pieter
3 Konnov, Igor V.
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 Monteiro, Pedro T.
...and 1,082 more Authors
all top 5

Cited in 65 Serials

48 Artificial Intelligence
45 Formal Methods in System Design
28 Journal of Automated Reasoning
24 Formal Aspects of Computing
23 Theoretical Computer Science
16 Information and Computation
12 Acta Informatica
12 Journal of Symbolic Computation
9 Constraints
7 ACM Transactions on Computational Logic
6 Annals of Mathematics and Artificial Intelligence
6 Mathematics in Computer Science
5 Science of Computer Programming
5 Discrete Event Dynamic Systems
5 Journal of Applied Logic
4 Journal of Computer and System Sciences
4 The Journal of Artificial Intelligence Research (JAIR)
4 Theory and Practice of Logic Programming
4 Journal of Applied Mathematics
4 Journal of Logical and Algebraic Methods in Programming
3 Cybernetics and Systems Analysis
3 The Journal of Logic and Algebraic Programming
3 Logical Methods in Computer Science
2 Automatica
2 Journal of Computer Science and Technology
2 International Journal of Approximate Reasoning
2 Distributed Computing
2 Journal of Applied Non-Classical Logics
2 Fundamenta Informaticae
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 Physics Letters. B
1 Computing
1 Information Sciences
1 Programming and Computer Software
1 Studia Logica
1 MSCS. Mathematical Structures in Computer Science
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 Mathematical and Computer Modelling of Dynamical Systems
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 Journal of Satisfiability, Boolean Modeling and Computation
1 Foundations and Trends 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

Citations by Year