Person: Roberto Sebastiani

DBLP: Sebastiani:Roberto

Facilitated 3 volumes:

Ed

Ed

Ed

Contributed to:

2015

2015

2013

2013

2012

2011

2011

2010

2009

2008

2008

2007

2007

2007

2006

2006

2005

2005

2005

2004

2004

2002

2002

2002

2001

2001

1999

1998

1997

1996

1996

2016

2017

2019

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.