| Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
| 1 | Roberto Sebastiani, Silvia Tomasi |
Optimization in SMT with LA(Q) Cost Functions  |
CoRR  |
2012 |
DBLP BibTeX RDF |
|
| 1 | Peter F. Patel-Schneider, Roberto Sebastiani |
A New General Method to Generate Random Modal Formulae for Testing Decision Procedures |
CoRR |
2011 |
DBLP BibTeX RDF |
|
| 1 | Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani |
Computing Small Unsatisfiable Cores in Satisfiability Modulo Theories. |
J. Artif. Intell. Res. (JAIR) |
2011 |
DBLP BibTeX RDF |
|
| 1 | Roberto Sebastiani, Stefano Tonetta, Moshe Y. Vardi |
Symbolic systems, explicit properties: on hybrid approaches for LTL symbolic model checking. |
STTT |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Volker Haarslev, Roberto Sebastiani, Michele Vescovi |
Automated Reasoning in ALCQ\mathcal{ALCQ} via SMT. |
CADE |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Alberto Griggio, Thi Thieu Hoa Le, Roberto Sebastiani |
Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic. |
TACAS |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Alberto Griggio, Quoc-Sang Phan, Roberto Sebastiani, Silvia Tomasi |
Stochastic Local Search for SMT: Combining Theory Solvers with WalkSAT. |
FroCos |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Alberto Griggio, Thi Thieu Hoa Le, Roberto Sebastiani |
Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic |
CoRR |
2010 |
DBLP BibTeX RDF |
|
| 1 | Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani |
Efficient generation of craig interpolants in satisfiability modulo theories. |
ACM Trans. Comput. Log. |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Alessandro Cimatti, Anders Franzén, Alberto Griggio, Roberto Sebastiani, Cristian Stenico |
Satisfiability Modulo the Theory of Costs: Foundations and Applications. |
TACAS |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Anders Franzén, Alessandro Cimatti, Alexander Nadel, Roberto Sebastiani, Jonathan Shalev |
Applying SMT in symbolic execution of microcode. |
FMCAD |
2010 |
DBLP BibTeX RDF |
|
| 1 | Dirk Beyer, Alessandro Cimatti, Alberto Griggio, M. Erkan Keremoglu, Roberto Sebastiani |
Software Model Checking via Large-Block Encoding |
CoRR |
2009 |
DBLP BibTeX RDF |
|
| 1 | Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani |
Efficient Generation of Craig Interpolants in Satisfiability Modulo Theories |
CoRR |
2009 |
DBLP BibTeX RDF |
|
| 1 | Roberto Sebastiani, Michele Vescovi |
Automated Reasoning in Modal and Description Logics via SAT Encoding: the Case Study of K(m)/ALC-Satisfiability. |
J. Artif. Intell. Res. (JAIR) |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | 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. |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Clark W. Barrett, Roberto Sebastiani, Sanjit A. Seshia, Cesare Tinelli |
Satisfiability Modulo Theories. |
Handbook of Satisfiability |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Roberto Sebastiani, Armando Tacchella |
SAT Techniques for Modal and Description Logics. |
Handbook of Satisfiability |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani |
Interpolant Generation for UTVPI. |
CADE |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Roberto Sebastiani, Michele Vescovi |
Axiom Pinpointing in Lightweight Description Logics via Horn-SAT Encoding and Conflict Analysis. |
CADE |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Dirk Beyer, Alessandro Cimatti, Alberto Griggio, M. Erkan Keremoglu, Roberto Sebastiani |
Software model checking via large-block encoding. |
FMCAD |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Silvio Ghilardi, Roberto Sebastiani (eds.) |
Frontiers of Combining Systems, 7th International Symposium, FroCoS 2009, Trento, Italy, September 16-18, 2009. Proceedings |
FroCoS |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani |
Efficient Interpolant Generation in Satisfiability Modulo Theories. |
TACAS |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, Roberto Sebastiani |
The MathSAT 4SMT Solver. |
CAV |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Roberto Sebastiani |
Lazy Satisability Modulo Theories. |
JSAT |
2007 |
DBLP BibTeX RDF |
|
| 1 | Byron Cook, Roberto Sebastiani |
Preface. |
JSAT |
2007 |
DBLP BibTeX RDF |
|
| 1 | Byron Cook, Roberto Sebastiani |
Preface and Foreword. |
Electr. Notes Theor. Comput. Sci. |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Roberto Sebastiani, Eli Singerman, Stefano Tonetta, Moshe Y. Vardi |
GSTE is partitioned model checking. |
Formal Methods in System Design |
2007 |
DBLP DOI BibTeX RDF |
GSTE, Property-driven partitioning, Symbolic model checking |
| 1 | Roberto Sebastiani, Stefano Tonetta, Moshe Y. Vardi |
Property-Driven Partitioning for Abstraction Refinement. |
TACAS |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani |
A Simple and Flexible Way of Computing Small Unsatisfiable Cores in SAT Modulo Theories. |
SAT |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Roberto Sebastiani |
From KSAT to Delayed Theory Combination: Exploiting DPLL Outside the SAT Domain. |
FroCos |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | 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 |
DBLP DOI BibTeX RDF |
|
| 1 | Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Silvio Ranise, Peter van Rossum, Roberto Sebastiani |
Efficient theory combination via boolean search. |
Inf. Comput. |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | 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. |
Electr. Notes Theor. Comput. Sci. |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | 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 |
DBLP DOI BibTeX RDF |
|
| 1 | 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 |
DBLP DOI BibTeX RDF |
|
| 1 | Roberto Sebastiani, Michele Vescovi |
Encoding the Satisfiability of Modal and Description Logics into SAT: The Case Study of K(m)/ALC. |
SAT |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Alessandro Cimatti, Roberto Sebastiani |
Building Efficient Decision Procedures on Top of SAT Solvers. |
SFM |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Paolo Giorgini, John Mylopoulos, Roberto Sebastiani |
Goal-oriented requirements analysis and reasoning in the Tropos methodology. |
Eng. Appl. of AI |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Audemard, Marco Bozzano, Alessandro Cimatti, Roberto Sebastiani |
Verifying Industrial Hybrid Systems with MathSAT. |
Electr. Notes Theor. Comput. Sci. |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | 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. Reasoning |
2005 |
DBLP DOI BibTeX RDF |
Satisfiability module theory, Integrated decision procedures, Linear arithmetic logic, Propositional satisfiability |
| 1 | Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Peter van Rossum, Stephan Schulz, Roberto Sebastiani |
The MathSAT 3 System. |
CADE |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | 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 |
DBLP DOI BibTeX RDF |
|
| 1 | 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 |
DBLP DOI BibTeX RDF |
|
| 1 | Roberto Sebastiani, Stefano Tonetta, Moshe Y. Vardi |
Symbolic Systems, Explicit Properties: On Hybrid Approaches for LTL Symbolic Model Checking. |
CAV |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Roberto Sebastiani, Paolo Giorgini, John Mylopoulos |
Simple and Minimum-Cost Satisfiability for Goal Models. |
CAiSE |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Roberto Sebastiani, Eli Singerman, Stefano Tonetta, Moshe Y. Vardi |
GSTE Is Partitioned Model Checking. |
CAV |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Paolo Giorgini, John Mylopoulos, Eleonora Nicchiarelli, Roberto Sebastiani |
Formal Reasoning Techniques for Goal Models. |
J. Data Semantics |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Peter F. Patel-Schneider, Roberto Sebastiani |
A New General Method to Generate Random Modal Formulae for Testing Decision Procedures. |
J. Artif. Intell. Res. (JAIR) |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Roberto Sebastiani, Stefano Tonetta |
"More Deterministic" vs. "Smaller" Büchi Automata for Efficient LTL Model Checking. |
CHARME |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Steve Linton, Roberto Sebastiani |
Editorial: The Integration of Automated Reasoning and Computer Algebra Systems. |
J. Symb. Comput. |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Audemard, Alessandro Cimatti, Artur Kornilowicz, Roberto Sebastiani |
Bounded Model Checking for Timed Systems. |
FORTE |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | 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 |
DBLP DOI BibTeX RDF |
|
| 1 | Alessandro Cimatti, Enrico Giunchiglia, Marco Pistore, Marco Roveri, Roberto Sebastiani, Armando Tacchella |
Integrating BDD-Based and SAT-Based Symbolic Model Checking. |
FroCos |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | Paolo Giorgini, John Mylopoulos, Eleonora Nicchiarelli, Roberto Sebastiani |
Reasoning with Goal Models. |
ER |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Audemard, Piergiorgio Bertoli, Alessandro Cimatti, Artur Kornilowicz, Roberto Sebastiani |
Integrating Boolean and Mathematical Solving: Foundations, Basic Algorithms, and Requirements. |
AISC |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | 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 |
DBLP DOI BibTeX RDF |
|
| 1 | Alessandro Cimatti, Marco Pistore, Marco Roveri, Roberto Sebastiani |
Improving the Encoding of LTL Model Checking into SAT. |
VMCAI |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | Peter F. Patel-Schneider, Roberto Sebastiani |
A New System and Methodology for Generating Random Modal Formulae. |
IJCAR |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | Roberto Sebastiani, Alessandro Tomasi, Fausto Giunchiglia |
Model Checking Syllabi and Student Carreers. |
TACAS |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | Enrico Giunchiglia, Fausto Giunchiglia, Roberto Sebastiani, Armando Tacchella |
SAT vs. translation based decision procedures for modal logics: a comparative evaluation. |
Journal of Applied Non-Classical Logics |
2000 |
DBLP BibTeX RDF |
|
| 1 | Ian Horrocks, Peter F. Patel-Schneider, Roberto Sebastiani |
An Analysis of Empirical Testing for Modal Decision Procedures. |
Logic Journal of the IGPL |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | Fausto Giunchiglia, Roberto Sebastiani |
Building Decision Procedures for Modal Logics from Propositional Decision Procedures: The Case Study of Modal K(m). |
Inf. Comput. |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | 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 |
DBLP DOI BibTeX RDF |
|
| 1 | Enrico Giunchiglia, Roberto Sebastiani |
Applying the Davis-Putnam Procedure to Non-clausal Formulas. |
AI*IA |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | 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 |
DBLP DOI BibTeX RDF |
|
| 1 | Enrico Giunchiglia, Fausto Giunchiglia, Roberto Sebastiani, Armando Tacchella |
More Evaluation of Decision Procedures for Modal Logics. |
KR |
1998 |
DBLP BibTeX RDF |
|
| 1 | Enrico Giunchiglia, Alessandro Massarotto, Roberto Sebastiani |
Act, and the Rest Will Follow: Exploiting Determinism in Planning as Satisfiability. |
AAAI/IAAI |
1998 |
DBLP BibTeX RDF |
|
| 1 | Roberto Sebastiani, Adolfo Villafiorita |
SAT-Based Decision Procedures for Normal Modal Logics: A Theoretical Framework. |
AIMSA |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Fausto Giunchiglia, Marco Roveri, Roberto Sebastiani |
A New Method for Testing Decision Procedures in Modal Logics. |
CADE |
1997 |
DBLP DOI BibTeX RDF |
|
| 1 | Alan Bundy, Fausto Giunchiglia, Roberto Sebastiani, Toby Walsh |
Calculating Criticalities. |
Artif. Intell. |
1996 |
DBLP DOI BibTeX RDF |
|
| 1 | Fausto Giunchiglia, Roberto Sebastiani |
Building Decision Procedures for Modal Logics from Propositional Decision Procedure - The Case Study of Modal K. |
CADE |
1996 |
DBLP DOI BibTeX RDF |
|
| 1 | Fausto Giunchiglia, Roberto Sebastiani |
An SAT-based Decision Procedure for ALC. |
Description Logics |
1996 |
DBLP BibTeX RDF |
|
| 1 | Fausto Giunchiglia, Marco Roveri, Roberto Sebastiani |
A New Method for Testing Decision Procedures in Modal and Terminological Logics. |
Description Logics |
1996 |
DBLP BibTeX RDF |
|
| 1 | Fausto Giunchiglia, Roberto Sebastiani |
A SAT-based Decision Procedure for ALC. |
KR |
1996 |
DBLP BibTeX RDF |
|
| 1 | Fausto Giunchiglia, Roberto Sebastiani, Adolfo Villafiorita, Toby Walsh |
A General Purpose Reasoner for Abstraction. |
Canadian Conference on AI |
1996 |
DBLP DOI BibTeX RDF |
|
| 1 | Alan Bundy, Fausto Giunchiglia, Roberto Sebastiani, Toby Walsh |
Computing Abstraction Hierarchies by Numerical Simulation. |
AAAI/IAAI, Vol. 1 |
1996 |
DBLP BibTeX RDF |
|
| 1 | Roberto Sebastiani |
Applying GSAT to Non-Clausal Formulas (Research Note). |
J. Artif. Intell. Res. (JAIR) |
1994 |
DBLP DOI BibTeX RDF |
|
![[Valid RSS]](Pics/valid-rss.png "Validate my RSS feed")