Jose Abel Castellanos Joo

Ph.D. candidate

University of New Mexico

Biography

I’m a Ph.D. candidate at the University of New Mexico in the Computer Science Department advised by Prof. Deepak Kapur working on formal methods and computer algebra. I’m interested in software verification, programming languages, commutative algebra, and non-classical logics.

I obtained my bacherlor’s degree in electronics engineering from Universidad de las Americas Puebla advised by Prof. Mauricio Osorio Galindo, working on the paraconsistent logic $C_{1}$ .

Here is my resumé .

Interests

Formal Verification
Archimedean Quadratic Modules
Groebner Basis Algorithms
Quantifier-free Interpolation Algorithms for Decidable Logics
Non-classical Logics

Education

MS in Computer Science, 2020

University of New Mexico
BSc in Electrical Engineering, 2015

Universidad de las Americas Puebla

Posts

A not not Brief Introduction to Kripke Semantics for Propositional Intuitionistic Logic

Abstract In this paper we motivate the study of Kripke semantics for propositional intuitionistic logic by showing fundamental properties at the proof theory level using

n + 1

-valued logics. Some non-theorems of propositional intuitionistic logic (like the excludded middle principle) are discussed using this approach.

Aug 16, 2022

My first post: how to make posts and academic websites using Hugo with the academic theme

While building this website, I thought it would be convenient to take some notes of the process so I can recall the necessary steps if I have to start from scratch again.

Aug 13, 2022

Projects

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.

EUFInterpolator

Master thesis work implementing new interpolation algorithms for the theory of equality and uninterpreted functions (EUF), octagonal formulas, and its combination.

Bosque Transpiler to

F^{*}

Prototypical implementation of a transpiler embedding a subset of the Bosque semantics into the Proof-oriented programming language

F^{*}

.

Publications

Jose Abel Castellanos Joo, Silvio Ghilardi, Alessandro Gianola, Deepak Kapur (2021). AXDInterpolator: A Tool for Computing Interpolants for Arrays with MaxDiff. 19th International Workshop on Satisfiability Modulo Theories co-located with 33rd International Conference on Computer Aided Verification (CAV 2021).

Cite

Mauricio Osorio, Jose Abel Castellanos Joo (2017). Equivalence among