×

Cimatti, Alessandro

Compute Distance To:
Author ID: cimatti.alessandro Recent zbMATH articles by "Cimatti, Alessandro"
Published as: Cimatti, Alessandro; Cimatti, A.
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

Publications by Year

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.68766
Cimatti, Alessandro; Clarke, Edmund; Giunchiglia, Enrico; Giunchiglia, Fausto; Pistore, Marco; Roveri, Marco; Sebastiani, Roberto; Tacchella, Armando
95
2002
The MathSAT5 SMT solver. Zbl 1381.68153
Cimatti, Alessandro; Griggio, Alberto; Schaafsma, Bastiaan Joost; Sebastiani, Roberto
60
2013
Diagnostic information for realizability. Zbl 1138.68442
Cimatti, A.; Roveri, M.; Schuppan, V.; Tchaltsev, A.
42
2008
NuSMV: A new symbolic model checker. Zbl 1059.68582
Cimatti, Alessandro; Clarke, Edmund; Giunchiglia, Fausto; Roveri, Marco
37
2000
Weak, strong, and strong cyclic planning via symbolic model checking. Zbl 1082.68800
Cimatti, A.; Pistore, M.; Roveri, M.; Traverso, P.
35
2003
NuSMV: A new symbolic model verifier. Zbl 1046.68587
Cimatti, A.; Clarke, E.; Giunchiglia, F.; Roveri, M.
35
1999
Efficient interpolant generation in satisfiability modulo theories. Zbl 1134.68402
Cimatti, Alessandro; Griggio, Alberto; Sebastiani, Roberto
19
2008
Conformant planning via symbolic model checking. Zbl 0963.68195
Cimatti, A.; Roveri, M.
19
2000
Infinite-state invariant checking with IC3 and predicate abstraction. Zbl 1368.68245
Cimatti, Alessandro; Griggio, Alberto; Mover, Sergio; Tonetta, Stefano
18
2016
Efficient generation of Craig interpolants in satisfiability modulo theories. Zbl 1351.68247
Cimatti, Alessandro; Griggio, Alberto; Sebastiani, Roberto
18
2010
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
15
2002
Verifying industrial hybrid systems with MathSAT. Zbl 1272.68220
Audemard, Gilles; Bozzano, Marco; Cimatti, Alessandro; Sebastiani, Roberto
15
2005
Efficient theory combination via Boolean search. Zbl 1137.68578
Bozzano, 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.68285
Cimatti, Alessandro; Griggio, Alberto; Irfan, Ahmed; Roveri, Marco; Sebastiani, Roberto
14
2018
Strong planning under partial observability. Zbl 1131.68095
Bertoli, Piergiorgio; Cimatti, Alessandro; Roveri, Marco; Traverso, Paolo
13
2006
Computing small unsatisfiable cores in satisfiability modulo theories. Zbl 1216.68241
Cimatti, 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.68549
Audemard, G.; Cimatti, A.; Kornilowicz, A.; Sebastiani, R.
12
2002
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
SMT-based scenario verification for hybrid systems. Zbl 1284.03216
Cimatti, Alessandro; Mover, Sergio; Tonetta, Stefano
10
2013
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
Solving strong controllability of temporal problems with uncertainty using SMT. Zbl 1314.90043
Cimatti, Alessandro; Micheli, Andrea; Roveri, Marco
10
2015
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
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
Symbolic implementation of alternating automata. Zbl 1160.68401
Bloem, R.; Cimatti, A.; Pill, I.; Roveri, M.; Semprini, S.
7
2006
Boolean abstraction for temporal logic satisfiability. Zbl 1135.68469
Cimatti, Alessandro; Roveri, Marco; Schuppan, Viktor; Tonetta, Stefano
7
2007
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
6
2016
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
6
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
6
2005
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
Dynamic controllability via timed game automata. Zbl 1350.68251
Cimatti, Alessandro; Hunsberger, Luke; Micheli, Andrea; Posenato, Roberto; Roveri, Marco
6
2016
Industrial applications of model checking. Zbl 0985.68653
Cimatti, Alessandro
5
2001
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
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.68482
Bruttomesso, Roberto; Cimatti, Alessandro; Franzén, Anders; Griggio, Alberto; Santuari, Alessandro; Sebastiani, Roberto
5
2006
Interpolant generation for UTVPI. Zbl 1250.68186
Cimatti, Alessandro; Griggio, Alberto; Sebastiani, Roberto
5
2009
Symbolic fault tree analysis for reactive systems. Zbl 1141.68455
Bozzano, Marco; Cimatti, Alessandro; Tapparo, Francesco
4
2007
Satisfiability modulo transcendental functions via incremental linearization. Zbl 1494.68281
Cimatti, 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.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
Searching powerset automata by combining explicit-state and symbolic model checking. Zbl 0978.68546
Cimatti, Alessandro; Roveri, Marco; Bertoli, Piergiorgio
3
2001
Bounded verification of past LTL. Zbl 1117.68424
Cimatti, Alessandro; Roveri, Marco; Sheridan, Daniel
3
2004
Verifying heap-manipulating programs in an SMT framework. Zbl 1141.68484
Rakamarić, Zvonimir; Bruttomesso, Roberto; Hu, Alan J.; Cimatti, Alessandro
3
2007
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
Strong temporal planning with uncontrollable durations. Zbl 1443.68163
Cimatti, Alessandro; Do, Minh; Micheli, Andrea; Roveri, Marco; Smith, David E.
3
2018
Bounded model checking for past LTL. Zbl 1031.68077
Benedetti, Marco; Cimatti, Alessandro
3
2003
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
Universal invariant checking of parametric systems with quantifier-free SMT reasoning. Zbl 07437076
Cimatti, Alessandro; Griggio, Alberto; Redondi, Gianluca
3
2021
Experimenting on solving nonlinear integer arithmetic with incremental linearization. Zbl 06916318
Cimatti, Alessandro; Griggio, Alberto; Irfan, Ahmed; Roveri, Marco; Sebastiani, Roberto
2
2018
Symbolic implementation of alternating automata. Zbl 1142.68418
Bloem, Roderick; Cimatti, Alessandro; Pill, Ingo; Roveri, Marco
2
2007
Improving the encoding of LTL model checking into SAT. Zbl 1057.68056
Cimatti, Alessandro; Pistore, Marco; Roveri, Marco; Sebastiani, Roberto
2
2002
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
2
2017
Formal specification and verification of dynamic parametrized architectures. Zbl 1460.68056
Cimatti, Alessandro; Stojic, Ivan; Tonetta, Stefano
2
2018
Proving the existence of fair paths in infinite-state systems. Zbl 1472.68085
Cimatti, Alessandro; Griggio, Alberto; Magnago, Enrico
2
2021
Formal reliability analysis of redundancy architectures. Zbl 1425.68039
Bozzano, Marco; Cimatti, Alessandro; Mattarei, Cristian
1
2019
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
1
2014
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
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.68174
Bozzano, Marco; Cimatti, Alessandro; Mattarei, Cristian; Tonetta, Stefano
1
2014
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
Implicit semi-algebraic abstraction for polynomial dynamical systems. Zbl 1493.68217
Mover, Sergio; Cimatti, Alessandro; Griggio, Alberto; Irfan, Ahmed; Tonetta, Stefano
1
2021
Universal invariant checking of parametric systems with quantifier-free SMT reasoning. Zbl 07437076
Cimatti, Alessandro; Griggio, Alberto; Redondi, Gianluca
3
2021
Proving the existence of fair paths in infinite-state systems. Zbl 1472.68085
Cimatti, Alessandro; Griggio, Alberto; Magnago, Enrico
2
2021
Implicit semi-algebraic abstraction for polynomial dynamical systems. Zbl 1493.68217
Mover, Sergio; Cimatti, Alessandro; Griggio, Alberto; Irfan, Ahmed; Tonetta, Stefano
1
2021
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
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
14
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 06916318
Cimatti, Alessandro; Griggio, Alberto; Irfan, Ahmed; Roveri, Marco; Sebastiani, Roberto
2
2018
Formal specification and verification of dynamic parametrized architectures. Zbl 1460.68056
Cimatti, Alessandro; Stojic, Ivan; Tonetta, Stefano
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
2
2017
Infinite-state invariant checking with IC3 and predicate abstraction. Zbl 1368.68245
Cimatti, 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.68062
Daniel, Jakub; Cimatti, Alessandro; Griggio, Alberto; Tonetta, Stefano; Mover, Sergio
6
2016
Dynamic controllability via timed game automata. Zbl 1350.68251
Cimatti, Alessandro; Hunsberger, Luke; Micheli, Andrea; Posenato, Roberto; Roveri, Marco
6
2016
Solving strong controllability of temporal problems with uncertainty using SMT. Zbl 1314.90043
Cimatti, Alessandro; Micheli, Andrea; Roveri, Marco
10
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
1
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
60
2013
SMT-based scenario verification for hybrid systems. Zbl 1284.03216
Cimatti, Alessandro; Mover, Sergio; Tonetta, Stefano
10
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.
12
2011
Efficient generation of Craig interpolants in satisfiability modulo theories. Zbl 1351.68247
Cimatti, Alessandro; Griggio, Alberto; Sebastiani, Roberto
18
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
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
Interpolant generation for UTVPI. Zbl 1250.68186
Cimatti, Alessandro; Griggio, Alberto; Sebastiani, Roberto
5
2009
Diagnostic information for realizability. Zbl 1138.68442
Cimatti, A.; Roveri, M.; Schuppan, V.; Tchaltsev, A.
42
2008
Efficient interpolant generation in satisfiability modulo theories. Zbl 1134.68402
Cimatti, Alessandro; Griggio, Alberto; Sebastiani, Roberto
19
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
7
2007
Symbolic fault tree analysis for reactive systems. Zbl 1141.68455
Bozzano, Marco; Cimatti, Alessandro; Tapparo, Francesco
4
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
14
2006
Strong planning under partial observability. Zbl 1131.68095
Bertoli, Piergiorgio; Cimatti, Alessandro; Roveri, Marco; Traverso, Paolo
13
2006
Symbolic implementation of alternating automata. Zbl 1160.68401
Bloem, 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.68483
Bruttomesso, 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.68482
Bruttomesso, Roberto; Cimatti, Alessandro; Franzén, Anders; Griggio, Alberto; Santuari, Alessandro; Sebastiani, Roberto
5
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
15
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
6
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
6
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
3
2004
Weak, strong, and strong cyclic planning via symbolic model checking. Zbl 1082.68800
Cimatti, A.; Pistore, M.; Roveri, M.; Traverso, P.
35
2003
Bounded model checking for past LTL. Zbl 1031.68077
Benedetti, Marco; Cimatti, Alessandro
3
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
95
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
15
2002
Bounded model checking for timed systems. Zbl 1037.68549
Audemard, G.; Cimatti, A.; Kornilowicz, A.; Sebastiani, R.
12
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
Improving the encoding of LTL model checking into SAT. Zbl 1057.68056
Cimatti, Alessandro; Pistore, Marco; Roveri, Marco; Sebastiani, Roberto
2
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
5
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
37
2000
Conformant planning via symbolic model checking. Zbl 0963.68195
Cimatti, A.; Roveri, M.
19
2000
NuSMV: A new symbolic model verifier. Zbl 1046.68587
Cimatti, 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 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

Citations by Year