Остановите войну!
for scientists:
default search action
Roberto Sebastiani
- > Home > Persons > Roberto Sebastiani
Publications
- 2022
- [c76]Alessandro Cimatti, Alberto Griggio, Enrico Lipparini, Roberto Sebastiani:
Handling Polynomial and Transcendental Functions in SMT via Unconstrained Optimisation and Topological Degree Test. ATVA 2022: 137-153 - 2021
- [c74]Filippo Bigarella, Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Martin Jonás, Marco Roveri, Roberto Sebastiani, Patrick Trentin:
Optimization Modulo Non-linear Arithmetic via Incremental Linearization. FroCoS 2021: 213-231 - 2019
- [c69]Ahmed Irfan, Alessandro Cimatti, Alberto Griggio, Marco Roveri, Roberto Sebastiani:
Lemmas for Satisfiability Modulo Transcendental Functions via Incremental Linearization. SC-square@SIAM AG 2019 - 2018
- [j23]Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, Roberto Sebastiani:
Incremental Linearization for Satisfiability and Verification Modulo Nonlinear Arithmetic and Transcendental Functions. ACM Trans. Comput. Log. 19(3): 19:1-19:52 (2018) - [c67]Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, Roberto Sebastiani:
Experimenting on Solving Nonlinear Integer Arithmetic with Incremental Linearization. SAT 2018: 383-398 - [c66]Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, Roberto Sebastiani:
Incremental linearization: A practical approach to satisfiability modulo nonlinear arithmetic and transcendental functions. SYNASC 2018: 19-26 - [i18]Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, Roberto Sebastiani:
Invariant Checking of NRA Transition Systems via Incremental Reduction to LRA with EUF. CoRR abs/1801.08718 (2018) - [i17]Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, Roberto Sebastiani:
Satisfiability Modulo Transcendental Functions via Incremental Linearization. CoRR abs/1801.08723 (2018) - 2017
- [c65]Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, Roberto Sebastiani:
Satisfiability Modulo Transcendental Functions via Incremental Linearization. CADE 2017: 95-113 - [c61]Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, Roberto Sebastiani:
Invariant Checking of NRA Transition Systems via Incremental Reduction to LRA with EUF. TACAS (1) 2017: 58-75 - 2016
- [c57]Ahmed Irfan, Alessandro Cimatti, Alberto Griggio, Marco Roveri, Roberto Sebastiani:
Verilog2SMV: A tool for word-level verification. DATE 2016: 1156-1159 - 2014
- [i10]Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani:
Computing Small Unsatisfiable Cores in Satisfiability Modulo Theories. CoRR abs/1401.3878 (2014) - 2013
- [c53]Alessandro Cimatti, Alberto Griggio, Bastiaan Joost Schaafsma, Roberto Sebastiani:
A Modular Approach to MaxSAT Modulo Theories. SAT 2013: 150-165 - [c52]Alessandro Cimatti, Alberto Griggio, Bastiaan Joost Schaafsma, Roberto Sebastiani:
The MathSAT5 SMT Solver. TACAS 2013: 93-107 - 2012
- [e2]Alessandro Cimatti, Roberto Sebastiani:
Theory and Applications of Satisfiability Testing - SAT 2012 - 15th International Conference, Trento, Italy, June 17-20, 2012. Proceedings. Lecture Notes in Computer Science 7317, Springer 2012, ISBN 978-3-642-31611-1 [contents] - 2011
- [j20]Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani:
Computing Small Unsatisfiable Cores in Satisfiability Modulo Theories. J. Artif. Intell. Res. 40: 701-728 (2011) - 2010
- [j17]Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani:
Efficient generation of craig interpolants in satisfiability modulo theories. ACM Trans. Comput. Log. 12(1): 7:1-7:54 (2010) - [c47]Anders Franzén, Alessandro Cimatti, Alexander Nadel, Roberto Sebastiani, Jonathan Shalev:
Applying SMT in symbolic execution of microcode. FMCAD 2010: 121-128 - [c46]Alessandro Cimatti, Anders Franzén, Alberto Griggio, Roberto Sebastiani, Cristian Stenico:
Satisfiability Modulo the Theory of Costs: Foundations and Applications. TACAS 2010: 99-113 - 2009
- [j16]Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, Roberto Sebastiani:
Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis. Ann. Math. Artif. Intell. 55(1-2): 63-99 (2009) - [c44]Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani:
Interpolant Generation for UTVPI. CADE 2009: 167-182 - [c43]Dirk Beyer, Alessandro Cimatti, Alberto Griggio, M. Erkan Keremoglu, Roberto Sebastiani:
Software model checking via large-block encoding. FMCAD 2009: 25-32 - [i3]Dirk Beyer, Alessandro Cimatti, Alberto Griggio, M. Erkan Keremoglu, Roberto Sebastiani:
Software Model Checking via Large-Block Encoding. CoRR abs/0904.4709 (2009) - [i2]Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani:
Efficient Generation of Craig Interpolants in Satisfiability Modulo Theories. CoRR abs/0906.4492 (2009) - 2008
- [c42]Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, Roberto Sebastiani:
The MathSAT 4SMT Solver. CAV 2008: 299-303 - [c41]Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani:
Efficient Interpolant Generation in Satisfiability Modulo Theories. TACAS 2008: 397-412 - 2007
- [c40]Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, Ziyad Hanna, Alexander Nadel, Amit Palti, Roberto Sebastiani:
A Lazy and Layered SMT($\mathcal{BV}$) Solver for Hard Industrial Verification Problems. CAV 2007: 547-560 - [c38]Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani:
A Simple and Flexible Way of Computing Small Unsatisfiable Cores in SAT Modulo Theories. SAT 2007: 334-339 - 2006
- [j11]Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Silvio Ranise, Peter van Rossum, Roberto Sebastiani:
Efficient theory combination via boolean search. Inf. Comput. 204(10): 1493-1525 (2006) - [c36]Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, Roberto Sebastiani:
Delayed Theory Combination vs. Nelson-Oppen for Satisfiability Modulo Theories: A Comparative Analysis. LPAR 2006: 527-541 - [c35]Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, Alessandro Santuari, Roberto Sebastiani:
To Ackermann-ize or Not to Ackermann-ize? On Efficiently Handling Uninterpreted Function Symbols in SMT(EUF ÈT). LPAR 2006: 557-571 - [c33]Alessandro Cimatti, Roberto Sebastiani:
Building Efficient Decision Procedures on Top of SAT Solvers. SFM 2006: 144-175 - 2005
- [j9]Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Peter van Rossum, Stephan Schulz, Roberto Sebastiani:
MathSAT: Tight Integration of SAT and Mathematical Decision Procedures. J. Autom. Reason. 35(1-3): 265-293 (2005) - [c31]Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Peter van Rossum, Stephan Schulz, Roberto Sebastiani:
The MathSAT 3 System. CADE 2005: 315-321 - [c30]Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Silvio Ranise, Peter van Rossum, Roberto Sebastiani:
Efficient Satisfiability Modulo Theories via Delayed Theory Combination. CAV 2005: 335-349 - [c28]Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Peter van Rossum, Stephan Schulz, Roberto Sebastiani:
An Incremental and Layered Procedure for the Satisfiability of Linear Arithmetic Logic. TACAS 2005: 317-333 - [c27]Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Ziyad Hanna, Zurab Khasidashvili, Amit Palti, Roberto Sebastiani:
Encoding RTL Constructs for MathSAT: a Preliminary Report. PDPAR@CAV 2005: 3-14 - 2004
- [c24]Gilles Audemard, Marco Bozzano, Alessandro Cimatti, Roberto Sebastiani:
Verifying Industrial Hybrid Systems with MathSAT. BMC@CAV 2004: 17-32 - 2002
- [c22]Gilles Audemard, Piergiorgio Bertoli, Alessandro Cimatti, Artur Kornilowicz, Roberto Sebastiani:
Integrating Boolean and Mathematical Solving: Foundations, Basic Algorithms, and Requirements. AISC 2002: 231-245 - [c21]Gilles Audemard, Piergiorgio Bertoli, Alessandro Cimatti, Artur Kornilowicz, Roberto Sebastiani:
A SAT Based Approach for Solving Formulas over Boolean and Linear Mathematical Propositions. CADE 2002: 195-210 - [c20]Alessandro Cimatti, Edmund M. Clarke, Enrico Giunchiglia, Fausto Giunchiglia, Marco Pistore, Marco Roveri, Roberto Sebastiani, Armando Tacchella:
NuSMV 2: An OpenSource Tool for Symbolic Model Checking. CAV 2002: 359-364 - [c18]Gilles Audemard, Alessandro Cimatti, Artur Kornilowicz, Roberto Sebastiani:
Bounded Model Checking for Timed Systems. FORTE 2002: 243-259 - [c17]Alessandro Cimatti, Enrico Giunchiglia, Marco Pistore, Marco Roveri, Roberto Sebastiani, Armando Tacchella:
Integrating BDD-Based and SAT-Based Symbolic Model Checking. FroCoS 2002: 49-56 - [c16]Alessandro Cimatti, Marco Pistore, Marco Roveri, Roberto Sebastiani:
Improving the Encoding of LTL Model Checking into SAT. VMCAI 2002: 196-207 - 1999
- [c12]Alessandro Cimatti, P. L. Pieraccini, Roberto Sebastiani, Paolo Traverso, Adolfo Villafiorita:
Formal Specification and Validation of a Vital Communication Protocol. World Congress on Formal Methods 1999: 1584-1604 - [c11]Angelo Chiappini, Alessandro Cimatti, Carmen Porzia, G. Rotondo, Roberto Sebastiani, Paolo Traverso, Adolfo Villafiorita:
Formal Specification and Development of a Safety-Critical Train Management System. SAFECOMP 1999: 410-419
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from , , and to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-03-27 23:03 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint