| Publication | Date of Publication | Type |
|---|
New results on rewrite-based satisfiability procedures
ACM Transactions on Computational Logic | 2017-07-12 | Paper |
Universal guards, relativization of quantifiers, and failure models in model checking modulo theories
Journal of Satisfiability, Boolean Modeling and Computation | 2016-02-23 | Paper |
Light-weight SMT-based model checking
Electronic Notes in Theoretical Computer Science | 2015-03-18 | Paper |
An extension of lazy abstraction with interpolation for programs with arrays
Formal Methods in System Design | 2014-12-05 | Paper |
Quantifier-free interpolation in combinations of equality interpolating theories
ACM Transactions on Computational Logic | 2014-04-16 | Paper |
Symbolic backward reachability with effectively propositional logic. Application to security policy analysis
Formal Methods in System Design | 2014-03-28 | Paper |
Distributing the workload in a lazy theorem-prover
Electronic Notes in Theoretical Computer Science | 2014-01-17 | Paper |
Verification of composed array-based systems with applications to security-aware workflows
Frontiers of Combining Systems | 2013-09-20 | Paper |
Automated termination in model-checking modulo theories
International Journal of Foundations of Computer Science | 2013-07-30 | Paper |
Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs
Electronic Notes in Theoretical Computer Science | 2013-04-19 | Paper |
From strong amalgamability to modularity of quantifier-free interpolation
Automated Reasoning | 2012-09-05 | Paper |
On the verification of security-aware E-services
Journal of Symbolic Computation | 2012-06-20 | Paper |
Lazy abstraction with interpolants for arrays
Logic for Programming, Artificial Intelligence, and Reasoning | 2012-06-15 | Paper |
Quantifier-free interpolation of a theory of arrays
Logical Methods in Computer Science | 2012-05-16 | Paper |
| Rewriting-based quantifier-free interpolation for a theory of arrays | 2012-04-24 | Paper |
Rewriting-based quantifier-free interpolation for a theory of arrays
(available as arXiv preprint) | 2012-04-24 | Paper |
A combination of rewriting and constraint solving for the quantifier-free interpolation of arrays with integer difference constraints
Frontiers of Combining Systems | 2011-10-07 | Paper |
Automated Termination in Model Checking Modulo Theories
Lecture Notes in Computer Science | 2011-10-07 | Paper |
Backward reachability of array-based systems by SMT solving: termination and invariant synthesis
Logical Methods in Computer Science | 2011-03-08 | Paper |
MCMT: a model checker modulo theories
Automated Reasoning | 2010-09-14 | Paper |
Combination of convex theories: modularity, deduction completeness, and explanation
Journal of Symbolic Computation | 2009-12-03 | Paper |
Goal-directed invariant synthesis for model checking modulo theories
Lecture Notes in Computer Science | 2009-12-01 | Paper |
Decidability and Undecidability Results for Nelson-Oppen and Rewrite-Based Decision Procedures
Automated Reasoning | 2009-03-12 | Paper |
Combination Methods for Satisfiability and Model-Checking of Infinite-State Systems
Automated Deduction – CADE-21 | 2009-03-06 | Paper |
Towards SMT Model Checking of Array-Based Systems
Automated Reasoning | 2008-11-27 | Paper |
Deciding Extensions of the Theory of Arrays by Integrating Decision Procedures and Instantiation Strategies
Logics in Artificial Intelligence | 2008-10-30 | Paper |
Building Extended Canonizers by Graph-Based Deduction
Theoretical Aspects of Computing – ICTAC 2007 | 2008-09-17 | Paper |
Noetherianity and Combination Problems
Frontiers of Combining Systems | 2008-09-16 | Paper |
Combining Proof-Producing Decision Procedures
Frontiers of Combining Systems | 2008-09-16 | Paper |
Automatic Combinability of Rewriting-Based Satisfiability Procedures
Logic for Programming, Artificial Intelligence, and Reasoning | 2008-05-27 | Paper |
Decision procedures for extensions of the theory of arrays
Annals of Mathematics and Artificial Intelligence | 2007-10-23 | Paper |
Theoretical Aspects of Computing – ICTAC 2005
Lecture Notes in Computer Science | 2006-11-01 | Paper |
Efficient theory combination via Boolean search
Information and Computation | 2006-10-25 | Paper |
Frontiers of Combining Systems
Lecture Notes in Computer Science | 2006-10-10 | Paper |
Frontiers of Combining Systems
Lecture Notes in Computer Science | 2006-10-10 | Paper |
Mechanizing Mathematical Reasoning
Lecture Notes in Computer Science | 2006-01-10 | Paper |
Computer Aided Verification
Lecture Notes in Computer Science | 2006-01-10 | Paper |
Theoretical Aspects of Computing - ICTAC 2004
Lecture Notes in Computer Science | 2005-11-30 | Paper |
Logic for Programming, Artificial Intelligence, and Reasoning
Lecture Notes in Computer Science | 2005-11-10 | Paper |
Artificial Intelligence and Symbolic Computation
Lecture Notes in Computer Science | 2005-08-19 | Paper |
| scientific article; zbMATH DE number 2090056 (Why is no real title available?) | 2004-08-12 | Paper |
| scientific article; zbMATH DE number 2084721 (Why is no real title available?) | 2004-08-09 | Paper |
Constraint contextual rewriting.
Journal of Symbolic Computation | 2003-08-25 | Paper |
A rewriting approach to satisfiability procedures.
Information and Computation | 2003-08-19 | Paper |
| scientific article; zbMATH DE number 1848313 (Why is no real title available?) | 2003-01-01 | Paper |
| scientific article; zbMATH DE number 1765707 (Why is no real title available?) | 2002-07-10 | Paper |
| Communication protocols for mathematical services based on KQML and OMRS | 2002-06-13 | Paper |
The control layer in open mechanized reasoning systems: Annotations and tactics
Journal of Symbolic Computation | 2002-01-02 | Paper |
| scientific article; zbMATH DE number 1538008 (Why is no real title available?) | 2001-10-30 | Paper |
A practical extension mechanism for decision procedures: The case study of universal Presburger arithmetic
Journal of Universal Computer Science | 2001-08-13 | Paper |
