Towards Certified Model Checking for PLTL Using One-Pass Tableaux. - Alex Abuin; Alexander Bolotov; Unai Díaz-de-Cerio; Montserrat Hermo; Paqui Lucio (TIME, 2019)

One-Pass Context-Based Tableaux Systems for CTL and ECTL. - Alex Abuin; Alexander Bolotov; Montserrat Hermo; Paqui Lucio (TIME, 2020)

Verified Model Checking for Conjunctive Positive Logic. - Alex Abuin; Unai Díaz-de-Cerio; Montserrat Hermo; Paqui Lucio (SN Comput. Sci., 2021)

Optimization Techniques and Formal Verification for the Software Design of Boolean Algebra Based Safety-Critical Systems. - Jon Pérez 001; Jose Luis Flores 001; Christian Blum 001; Jesús Cerquides; Alex Abuin (IEEE Trans. Ind. Informatics, 2022)

Tableaux and sequent calculi for CTL and ECTL: Satisfiability test with certifying proofs and models. - Alex Abuin; Alexander Bolotov; Montserrat Hermo; Paqui Lucio (J. Log. Algebraic Methods Program., 2023)