Verification

Computing certicates in compact quadratic modules in $\mathbb{R}[x]$
Thesis Proposal Defense
Jose Abel Castellanos Joo
Sep 13, 2023
Slides
AXDInterpolator A Tool for Computing Interpolants for Arrays with MaxDiff
19th International Workshop on Satisfiability Modulo Theories
Jose Abel Castellanos Joo, Silvio Ghilardi, Alessandro Gianola and Deepak Kapur
Jul 18, 2021
Slides Video
AXDInterpolator
This project implements an interpolation algorithm proposed in FoSSaCS 2021 using the Z3 API. The project allows the user to choose Z3, Mathsat, or SMTInterpol as interpolation engines. The tool returns a formula in SMTLIB2 format, which allows compatibility with model checkers and invariant generators using such a format.
Apr 27, 2021
Code
AXDInterpolator
Implementation of Uniform Interpolation Algorithms
Master Thesis Defense, University of New Mexico
Jose Abel Castellanos Joo
Oct 20, 2020
Slides
EUFInterpolator
Master thesis work implementing new interpolation algorithms for the theory of equality and uninterpreted functions (EUF), octagonal formulas, and its combination.
Oct 1, 2020
Code
EUFInterpolator
A new interpolation algorithm for the theory of Equality with Uninterpreted Functions
Computer Science Colloquium Series, University of New Mexico
Jose Abel Castellanos Joo
Sep 9, 2020
Slides
Bosque Transpiler to $F^{*}$
Prototypical implementation of a transpiler embedding a subset of the Bosque semantics into the Proof-oriented programming language $F^{*}$.
Aug 1, 2019
Code