BibSLEIGH
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
EDIT!
CC-BY
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
Travelled to:
1 × Australia
1 × Canada
1 × Cyprus
1 × Estonia
1 × Finland
1 × France
1 × Hungary
1 × Latvia
1 × Poland
2 × Denmark
2 × Germany
2 × Portugal
4 × United Kingdom
6 × Italy
6 × USA
Collaborated with:
A.Cimatti A.Griggio F.Giunchiglia P.Trentin M.Vescovi S.Tonetta M.Y.Vardi M.Roveri R.Bruttomesso A.Franzén B.J.Schaafsma S.Tomasi P.F.Patel-Schneider M.Bozzano T.A.Junttila P.v.Rossum E.Giunchiglia M.Pistore A.Tacchella V.Haarslev T.T.H.Le P.Giorgini J.Mylopoulos A.Tomasi S.Schulz E.Singerman C.Stenico G.Audemard P.Bertoli A.Kornilowicz P.L.Pieraccini P.Traverso A.Villafiorita A.Irfan S.Ranise Z.Hanna A.Nadel A.Palti E.M.Clarke
Talks about:
sat (12) theori (10) modulo (10) satisfi (8) procedur (7) model (6) modal (6) logic (6) decis (6) linear (5)

Person: Roberto Sebastiani

DBLP DBLP: Sebastiani:Roberto

Facilitated 3 volumes:

SAT 2012Ed
SMT 2006Ed
IJCAR 2018Ed

Contributed to:

CAV 20152015
TACAS 20152015
SAT 20132013
TACAS 20132013
IJCAR 20122012
CADE 20112011
TACAS 20112011
TACAS 20102010
CADE 20092009
CAV 20082008
TACAS 20082008
CAV 20072007
SAT 20072007
TACAS 20072007
SAT 20062006
SFM 20062006
CADE 20052005
CAV 20052005
TACAS 20052005
CAV 20042004
CAiSE 20042004
CADE 20022002
CAV 20022002
VMCAI 20022002
IJCAR 20012001
TACAS 20012001
World Congress on Formal Methods 19991999
KR 19981998
CADE 19971997
CADE 19961996
KR 19961996
IJCAR 20162016
CADE 20172017
CADE 20192019

Wrote 36 papers:

CAV-2015-SebastianiT #modulo theories #named #optimisation
OptiMathSAT: A Tool for Optimization Modulo Theories (RS, PT), pp. 447–454.
TACAS-2015-SebastianiT #cost analysis #modulo theories #optimisation
Pushing the Envelope of Optimization Modulo Theories with Linear-Arithmetic Cost Functions (RS, PT), pp. 335–349.
SAT-2013-CimattiGSS #approach #composition #modulo theories #satisfiability
A Modular Approach to MaxSAT Modulo Theories (AC, AG, BJS, RS), pp. 150–165.
TACAS-2013-CimattiGSS #smt
The MathSAT5 SMT Solver (AC, AG, BJS, RS), pp. 93–107.
IJCAR-2012-SebastianiT #cost analysis #optimisation #smt
Optimization in SMT with ℒ𝒜(ℚ) Cost Functions (RS, ST), pp. 484–498.
CADE-2011-HaarslevSV #automation #reasoning #smt
Automated Reasoning in 𝒜ℒ𝒞𝒬 via SMT (VH, RS, MV), pp. 283–298.
TACAS-2011-GriggioLS #generative #integer #linear #performance #satisfiability
Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic (AG, TTHL, RS), pp. 143–157.
TACAS-2010-CimattiFGSS #formal method #satisfiability
Satisfiability Modulo the Theory of Costs: Foundations and Applications (AC, AF, AG, RS, CS), pp. 99–113.
CADE-2009-CimattiGS #generative
Interpolant Generation for UTVPI (AC, AG, RS), pp. 167–182.
CADE-2009-SebastianiV #analysis #axiom #encoding #lightweight #logic
Axiom Pinpointing in Lightweight Description Logics via Horn-SAT Encoding and Conflict Analysis (RS, MV), pp. 84–99.
CAV-2008-BruttomessoCFGS #smt
The MathSAT 4SMT Solver (RB, AC, AF, AG, RS), pp. 299–303.
TACAS-2008-CimattiGS #generative #modulo theories #performance #satisfiability
Efficient Interpolant Generation in Satisfiability Modulo Theories (AC, AG, RS), pp. 397–412.
CAV-2007-BruttomessoCFGHNPS #industrial #lazy evaluation #problem #smt #verification
A Lazy and Layered SMT(BV) Solver for Hard Industrial Verification Problems (RB, AC, AF, AG, ZH, AN, AP, RS), pp. 547–560.
SAT-2007-CimattiGS #flexibility #modulo theories #satisfiability
A Simple and Flexible Way of Computing Small Unsatisfiable Cores in SAT Modulo Theories (AC, AG, RS), pp. 334–339.
TACAS-2007-SebastianiTV #abstraction #clustering #refinement
Property-Driven Partitioning for Abstraction Refinement (RS, ST, MYV), pp. 389–404.
SAT-2006-SebastianiV #case study #encoding #logic #satisfiability
Encoding the Satisfiability of Modal and Description Logics into SAT: The Case Study of K(m)/ALC (RS, MV), pp. 130–135.
SFM-2006-CimattiS #performance #satisfiability
Building Efficient Decision Procedures on Top of SAT Solvers (AC, RS), pp. 144–175.
CADE-2005-BozzanoBCJRSS
The MathSAT 3 System (MB, RB, AC, TAJ, PvR, SS, RS), pp. 315–321.
CAV-2005-BozzanoBCJRRS #modulo theories #performance #satisfiability
Efficient Satisfiability Modulo Theories via Delayed Theory Combination (MB, RB, AC, TAJ, SR, PvR, RS), pp. 335–349.
CAV-2005-SebastianiTV #hybrid #ltl #model checking
Symbolic Systems, Explicit Properties: On Hybrid Approaches for LTL Symbolic Model Checking (RS, ST, MYV), pp. 350–363.
TACAS-2005-BozzanoBCJRSS #incremental #linear #logic #satisfiability
An Incremental and Layered Procedure for the Satisfiability of Linear Arithmetic Logic (MB, RB, AC, TAJ, PvR, SS, RS), pp. 317–333.
CAV-2004-SebastianiSTV #model checking
GSTE Is Partitioned Model Checking (RS, ES, ST, MYV), pp. 229–241.
CAiSE-2004-SebastianiGM #low cost #modelling #satisfiability
Simple and Minimum-Cost Satisfiability for Goal Models (RS, PG, JM), pp. 20–35.
CADE-2002-AudemardBCKS #approach #linear #satisfiability
A SAT Based Approach for Solving Formulas over Boolean and Linear Mathematical Propositions (GA, PB, AC, AK, RS), pp. 195–210.
CAV-2002-CimattiCGGPRST #model checking
NuSMV 2: An OpenSource Tool for Symbolic Model Checking (AC, EMC, EG, FG, MP, MR, RS, AT), pp. 359–364.
VMCAI-2002-CimattiPRS #encoding #ltl #model checking #satisfiability
Improving the Encoding of LTL Model Checking into SAT (AC, MP, MR, RS), pp. 196–207.
IJCAR-2001-Patel-SchneiderS #generative #random
A New System and Methodology for Generating Random Modal Formulae (PFPS, RS), pp. 464–468.
TACAS-2001-SebastianiTG #model checking #student
Model Checking Syllabi and Student Carreers (RS, AT, FG), pp. 128–142.
FM-v2-1999-CimattiPSTV #communication #protocol #specification #validation
Formal Specification and Validation of a Vital Communication Protocol (AC, PLP, RS, PT, AV), pp. 1584–1604.
KR-1998-GiunchigliaGST #evaluation #logic
More Evaluation of Decision Procedures for Modal Logics (EG, FG, RS, AT), pp. 626–635.
CADE-1997-GiunchigliaRS #logic #testing
A New Method for Testing Decision Procedures in Modal Logics (FG, MR, RS), pp. 264–267.
CADE-1996-GiunchigliaS #case study #logic
Building Decision Procedures for Modal Logics from Propositional Decision Procedure — The Case Study of Modal K (FG, RS), pp. 583–597.
KR-1996-GiunchigliaS #satisfiability
A SAT-based Decision Procedure for ALC (FG, RS), pp. 304–314.
IJCAR-2016-Sebastiani
Colors Make Theories Hard (RS), pp. 152–170.
CADE-2017-CimattiGIRS #incremental #satisfiability
Satisfiability Modulo Transcendental Functions via Incremental Linearization (AC, AG, AI, MR, RS), pp. 95–113.
CADE-2019-TrentinS #float #formal method #optimisation
Optimization Modulo the Theory of Floating-Point Numbers (PT, RS), pp. 550–567.

Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.