| Publication | Date of Publication | Type |
|---|
Uniswap v3: impermanent loss modeling and swap fees asymptotic analysis
SIAM Journal on Financial Mathematics | 2026-04-02 | Paper |
| Decidable entailments in separation logic with inductive definitions: beyond establishment | 2026-03-23 | Paper |
Tractable and intractable entailment problems in separation logic with inductively defined predicates
Fundamenta Informaticae | 2025-10-06 | Paper |
Statistical error bounds for weighted mean and median with application to robust aggregation of cryptocurrency data
Mathematical Finance | 2025-09-30 | Paper |
A direct procedure to test entailment in a separation logic of relations
Journal of Automated Reasoning | 2025-05-28 | Paper |
A formalization of the CHSH inequality and Tsirelson's upper-bound in Isabelle/HOL
Journal of Automated Reasoning | 2024-02-06 | Paper |
A strict constrained superposition calculus for graphs
Lecture Notes in Computer Science | 2023-11-24 | Paper |
A proof procedure for separation logic with inductive definitions and data
Journal of Automated Reasoning | 2023-10-24 | Paper |
Unbiasing and robustifying implied volatility calibration in a cryptocurrency market with large bid-ask spreads and missing quotes
Quantitative Finance | 2023-09-25 | Paper |
An undecidability result for separation logic with theory reasoning
Information Processing Letters | 2023-06-05 | Paper |
Unifying decidable entailments in separation logic with inductive definitions
(available as arXiv preprint) | 2021-12-01 | Paper |
Entailment is undecidable for symbolic heap separation logic formulæ with non-established inductive rules
Information Processing Letters | 2021-10-19 | Paper |
The Bernays-Schönfinkel-Ramsey class of separation logic with uninterpreted predicates
ACM Transactions on Computational Logic | 2020-09-11 | Paper |
| Prenex separation logic with one selector field | 2020-05-14 | Paper |
Ilinva: using abduction to generate loop invariants
(available as arXiv preprint) | 2020-05-13 | Paper |
Formalizing the Cox-Ross-Rubinstein pricing of European derivatives in Isabelle/HOL
Journal of Automated Reasoning | 2020-04-07 | Paper |
Combining induction and saturation-based theorem proving
Journal of Automated Reasoning | 2020-03-03 | Paper |
| The Bernays-Schönfinkel-Ramsey class of separation logic on arbitrary domains | 2020-01-28 | Paper |
A generic framework for implicate generation modulo theories
(available as arXiv preprint) | 2018-10-18 | Paper |
Prime implicate generation in equational logic
Journal of Artificial Intelligence Research | 2018-01-12 | Paper |
| The binomial pricing model in finance: a formalization in Isabelle | 2017-09-22 | Paper |
A superposition calculus for abductive reasoning
Journal of Automated Reasoning | 2017-08-17 | Paper |
Quantifier-free equational logic and prime implicate generation
Automated Deduction - CADE-25 | 2015-12-02 | Paper |
Instantiation schemes for nested theories
ACM Transactions on Computational Logic | 2015-09-17 | Paper |
A rewriting strategy to generate prime implicates in equational logic
Automated Reasoning | 2014-09-26 | Paper |
Rewrite-based satisfiability procedures for recursive data structures
Electronic Notes in Theoretical Computer Science | 2013-12-06 | Paper |
Rewrite-based decision procedures
Electronic Notes in Theoretical Computer Science | 2013-12-06 | Paper |
A resolution calculus for first-order schemata
Fundamenta Informaticae | 2013-08-26 | Paper |
On leaf permutative theories and occurrence permutation groups
Electronic Notes in Theoretical Computer Science | 2013-04-19 | Paper |
Modular instantiation schemes
Information Processing Letters | 2013-04-04 | Paper |
Reasoning on schemata of formulæ
Lecture Notes in Computer Science | 2012-09-07 | Paper |
A calculus for generating ground explanations
Automated Reasoning | 2012-09-05 | Paper |
An instantiation scheme for satisfiability modulo theories
Journal of Automated Reasoning | 2012-07-31 | Paper |
Instantiation of SMT problems modulo integers
Lecture Notes in Computer Science | 2010-08-24 | Paper |
| NP-completeness results for deductive problems on stratified terms | 2010-02-24 | Paper |
Theory decision by decomposition
Journal of Symbolic Computation | 2009-12-03 | Paper |
${\mathcal{T}}$ -Decision by Decomposition
Automated Deduction – CADE-21 | 2009-03-06 | Paper |
Unification and Matching Modulo Leaf-Permutative Equational Presentations
Automated Reasoning | 2008-11-27 | Paper |
On Variable-inactivity and Polynomial Formula-Satisfiability Procedures
Journal Of Logic And Computation | 2008-03-12 | Paper |
Determining Unify-Stable Presentations
Lecture Notes in Computer Science | 2008-01-02 | Paper |
Automated Reasoning
Lecture Notes in Computer Science | 2007-09-25 | Paper |
Permutative rewriting and unification
Information and Computation | 2007-04-16 | Paper |
Term Rewriting and Applications
Lecture Notes in Computer Science | 2005-11-11 | Paper |
On the complexity of deduction modulo leaf permutative equations
Journal of Automated Reasoning | 2005-06-22 | Paper |
