Roberto Sebastiani

Proceedings of the Automated Reasoning - 8th International Joint Conference, 2016

2015

Optimization Modulo Theories with Linear Rational Costs.

[BibT_eX]

[DOI]

Silvia Tomasi

ACM Trans. Comput. Log., 2015

Pushing the Envelope of Optimization Modulo Theories with Linear-Arithmetic Cost Functions.

[BibT_eX]

[DOI]

Patrick Trentin

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2015

2014

Hybrid SRL with Optimization Modulo Theories.

[BibT_eX]

[DOI]

Stefano Teso

Andrea Passerini

CoRR, 2014

2013

The MathSAT5 SMT Solver.

[BibT_eX]

[DOI]

Bastiaan Joost Schaafsma

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2013

A Modular Approach to MaxSAT Modulo Theories.

[BibT_eX]

[DOI]

Bastiaan Joost Schaafsma

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2013, 2013

2012

Optimization in SMT with LA(Q) Cost Functions

[BibT_eX]

[DOI]

Silvia Tomasi

CoRR, 2012

Optimization in SMT with ${\mathcal LA}$ (ℚ) Cost Functions.

[BibT_eX]

[DOI]

Silvia Tomasi

Proceedings of the Automated Reasoning - 6th International Joint Conference, 2012

2011

Symbolic systems, explicit properties: on hybrid approaches for LTL symbolic model checking.

[BibT_eX]

[DOI]

Stefano Tonetta

Moshe Y. Vardi

Int. J. Softw. Tools Technol. Transf., 2011

Computing Small Unsatisfiable Cores in Satisfiability Modulo Theories.

[BibT_eX]

[DOI]

J. Artif. Intell. Res., 2011

Stochastic Local Search for SMT: Combining Theory Solvers with WalkSAT.

[BibT_eX]

[DOI]

Proceedings of the Frontiers of Combining Systems, 8th International Symposium, 2011

Automated Reasoning in ALCQ\mathcal{ALCQ} via SMT.

[BibT_eX]

[DOI]

Volker Haarslev

Proceedings of the Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31, 2011

Goal Modeling and Reasoning in Tropos.

[BibT_eX]

Proceedings of the Social Modeling for Requirements Engineering., 2011

2010

Efficient generation of craig interpolants in satisfiability modulo theories.

[BibT_eX]

[DOI]

ACM Trans. Comput. Log., 2010

Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic

[BibT_eX]

[DOI]

Thi Thieu Hoa Le

Log. Methods Comput. Sci., 2010

Satisfiability Modulo the Theory of Costs: Foundations and Applications.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2010

Applying SMT in symbolic execution of microcode.

[BibT_eX]

[DOI]

Proceedings of 10th International Conference on Formal Methods in Computer-Aided Design, 2010

2009

SAT Techniques for Modal and Description Logics.

[BibT_eX]

[DOI]

Armando Tacchella

Proceedings of the Handbook of Satisfiability, 2009

Satisfiability Modulo Theories.

[BibT_eX]

[DOI]

Proceedings of the Handbook of Satisfiability, 2009

Automated Reasoning in Modal and Description Logics via SAT Encoding: the Case Study of K(m)/ALC-Satisfiability.

[BibT_eX]

[DOI]

J. Artif. Intell. Res., 2009

Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis.

[BibT_eX]

[DOI]

Ann. Math. Artif. Intell., 2009

Software model checking via large-block encoding.

[BibT_eX]

[DOI]

Proceedings of 9th International Conference on Formal Methods in Computer-Aided Design, 2009

Axiom Pinpointing in Lightweight Description Logics via Horn-SAT Encoding and Conflict Analysis.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 2009

Interpolant Generation for UTVPI.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 2009

2008

Efficient Interpolant Generation in Satisfiability Modulo Theories.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2008

The MathSAT 4SMT Solver.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 20th International Conference, 2008

2007

Lazy Satisability Modulo Theories.

[BibT_eX]

[DOI]

J. Satisf. Boolean Model. Comput., 2007

Preface to Special Issue on Satisfiability Modulo Theories.

[BibT_eX]

[DOI]

Byron Cook

J. Satisf. Boolean Model. Comput., 2007

GSTE is partitioned model checking.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2007

Property-Driven Partitioning for Abstraction Refinement.

[BibT_eX]

[DOI]

Stefano Tonetta

Moshe Y. Vardi

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2007

A Simple and Flexible Way of Computing Small Unsatisfiable Cores in SAT Modulo Theories.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing, 2007

From KSAT to Delayed Theory Combination: Exploiting DPLL Outside the SAT Domain.

[BibT_eX]

[DOI]

Proceedings of the Frontiers of Combining Systems, 6th International Symposium, 2007

A Lazy and Layered SMT($\mathcal{BV}$) Solver for Hard Industrial Verification Problems.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 19th International Conference, 2007

2006

Efficient theory combination via boolean search.

[BibT_eX]

[DOI]

Inf. Comput., 2006

Preface and Foreword.

[BibT_eX]

[DOI]

Byron Cook

Proceedings of the Combined Proceedings of the Fourth Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR 2006) and the First International Workshop on Probabilistic Automata and Logics (PaUL 2006), 2006

Building Efficient Decision Procedures on Top of SAT Solvers.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods for Hardware Verification, 2006

Encoding the Satisfiability of Modal and Description Logics into SAT: The Case Study of K(m)/ALC.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing, 2006

To Ackermann-ize or Not to Ackermann-ize? On Efficiently Handling Uninterpreted Function Symbols in SMT(EUF ÈT).

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, 2006

2005

MathSAT: Tight Integration of SAT and Mathematical Decision Procedures.

[BibT_eX]

[DOI]

J. Autom. Reason., 2005

Encoding RTL Constructs for MathSAT: a Preliminary Report.

[BibT_eX]

[DOI]

Proceedings of the Third Workshop on Pragmatics of Decision Procedures in Automated Reasoning, 2005

Goal-oriented requirements analysis and reasoning in the Tropos methodology.

[BibT_eX]

[DOI]

Eng. Appl. Artif. Intell., 2005

An Incremental and Layered Procedure for the Satisfiability of Linear Arithmetic Logic.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2005

Efficient Satisfiability Modulo Theories via Delayed Theory Combination.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 17th International Conference, 2005

The MathSAT 3 System.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 2005

2004

Verifying Industrial Hybrid Systems with MathSAT.

[BibT_eX]

[DOI]

Proceedings of the 2nd International Workshop on Bounded Model Checking, 2004

Simple and Minimum-Cost Satisfiability for Goal Models.

[BibT_eX]

[DOI]

Proceedings of the Advanced Information Systems Engineering, 16th International Conference, 2004

2003

Formal Reasoning Techniques for Goal Models.

[BibT_eX]

[DOI]

Eleonora Nicchiarelli

J. Data Semant., 2003

A New General Method to Generate Random Modal Formulae for Testing Decision Procedures.

[BibT_eX]

[DOI]

Peter F. Patel-Schneider

J. Artif. Intell. Res., 2003

"More Deterministic" vs. "Smaller" Büchi Automata for Efficient LTL Model Checking.

[BibT_eX]

[DOI]

Stefano Tonetta

Proceedings of the Correct Hardware Design and Verification Methods, 2003

2002

Editorial: The Integration of Automated Reasoning and Computer Algebra Systems.

[BibT_eX]

[DOI]

Steve Linton

J. Symb. Comput., 2002

Improving the Encoding of LTL Model Checking into SAT.

[BibT_eX]

[DOI]

Proceedings of the Verification, 2002

Integrating BDD-Based and SAT-Based Symbolic Model Checking.

[BibT_eX]

[DOI]

Proceedings of the Frontiers of Combining Systems, 4th International Workshop, 2002

Bounded Model Checking for Timed Systems.

[BibT_eX]

[DOI]

Proceedings of the Formal Techniques for Networked and Distributed Systems, 2002

Reasoning with Goal Models.

[BibT_eX]

[DOI]

Eleonora Nicchiarelli

Proceedings of the Conceptual Modeling, 2002

NuSMV 2: An OpenSource Tool for Symbolic Model Checking.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 14th International Conference, 2002

A SAT Based Approach for Solving Formulas over Boolean and Linear Mathematical Propositions.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 2002

Integrating Boolean and Mathematical Solving: Foundations, Basic Algorithms, and Requirements.

[BibT_eX]

[DOI]

Proceedings of the Artificial Intelligence, 2002

2001

Model Checking Syllabi and Student Carreers.

[BibT_eX]

[DOI]

Alessandro Tomasi

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2001

A New System and Methodology for Generating Random Modal Formulae.

[BibT_eX]

[DOI]

Peter F. Patel-Schneider

Proceedings of the Automated Reasoning, First International Joint Conference, 2001

2000

SAT vs. translation based decision procedures for modal logics: a comparative evaluation.

[BibT_eX]

[DOI]

J. Appl. Non Class. Logics, 2000

An Analysis of Empirical Testing for Modal Decision Procedures.

[BibT_eX]

[DOI]

Ian Horrocks

Peter F. Patel-Schneider

Log. J. IGPL, 2000

Building Decision Procedures for Modal Logics from Propositional Decision Procedures: The Case Study of Modal K(m).

[BibT_eX]

[DOI]

Inf. Comput., 2000

1999

Formal Specification and Development of a Safety-Critical Train Management System.

[BibT_eX]

[DOI]

Proceedings of the Computer Safety, 1999

Formal Specification and Validation of a Vital Communication Protocol.

[BibT_eX]

[DOI]

Proceedings of the FM'99 - Formal Methods, 1999

Applying the Davis-Putnam Procedure to Non-clausal Formulas.

[BibT_eX]

[DOI]

Enrico Giunchiglia

Proceedings of the AI*IA 99:Advances in Artificial Intelligence, 1999

1998

More Evaluation of Decision Procedures for Modal Logics.

[BibT_eX]

Proceedings of the Sixth International Conference on Principles of Knowledge Representation and Reasoning (KR'98), 1998

SAT-Based Decision Procedures for Normal Modal Logics: A Theoretical Framework.

[BibT_eX]

[DOI]

Adolfo Villafiorita

Proceedings of the Artificial Intelligence: Methodology, 1998

Act, and the Rest Will Follow: Exploiting Determinism in Planning as Satisfiability.

[BibT_eX]

[DOI]

Enrico Giunchiglia

Alessandro Massarotto

Proceedings of the Fifteenth National Conference on Artificial Intelligence and Tenth Innovative Applications of Artificial Intelligence Conference, 1998

1997

A New Method for Testing Decision Procedures in Modal Logics.

[BibT_eX]

[DOI]

Marco Roveri

Proceedings of the Automated Deduction, 1997

1996

Calculating Criticalities.

[BibT_eX]

[DOI]

Artif. Intell., 1996

A SAT-based Decision Procedure for ALC.

[BibT_eX]

Proceedings of the Fifth International Conference on Principles of Knowledge Representation and Reasoning (KR'96), 1996

An SAT-based Decision Procedure for ALC.

[BibT_eX]

Proceedings of the 1996 International Workshop on Description Logics, 1996

A New Method for Testing Decision Procedures in Modal and Terminological Logics.

[BibT_eX]

Marco Roveri

Proceedings of the 1996 International Workshop on Description Logics, 1996

Building Decision Procedures for Modal Logics from Propositional Decision Procedure - The Case Study of Modal K.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE-13, 13th International Conference on Automated Deduction, New Brunswick, NJ, USA, July 30, 1996

A General Purpose Reasoner for Abstraction.

[BibT_eX]

[DOI]

Proceedings of the Advances in Artificial Intelligence, 1996

Computing Abstraction Hierarchies by Numerical Simulation.

[BibT_eX]

[DOI]

Proceedings of the Thirteenth National Conference on Artificial Intelligence and Eighth Innovative Applications of Artificial Intelligence Conference, 1996

1994

Applying GSAT to Non-Clausal Formulas (Research Note).

[BibT_eX]

[DOI]

J. Artif. Intell. Res., 1994

Applying GSAT to Non-Clausal Formulas.

[BibT_eX]

[DOI]