Verification of Hardware Implementations through Correctness of their Recursive Definitions in PVS. - Ariane Alves Almeida; Carlos H. Llanos; Janier Arias-Garcia; Mauricio Ayala-Rincón (SBCCI, 2014)

The Computational Relevance of Formal Logic Through Formal Proofs. - Ariane Alves Almeida; Ana Cristina Rocha Oliveira; Thiago Mendonça Ferreira Ramos; Flávio L. C. de Moura; Mauricio Ayala-Rincón (FMTea, 2019)

Formalizing the dependency pair criterion for innermost termination. - Ariane Alves Almeida; Mauricio Ayala-Rincón (Sci. Comput. Program., 2020)

Formalization of the Computational Theory of a Turing Complete Functional Language Model. - Thiago Mendonça Ferreira Ramos; Ariane Alves Almeida; Mauricio Ayala-Rincón (J. Autom. Reason., 2022)

Formal Verification of Termination Criteria for First-Order Recursive Functions. - César A. Muñoz; Mauricio Ayala-Rincón; Mariano M. Moscato; Aaron Dutle; Anthony J. Narkawicz; Ariane Alves Almeida; Andréia B. Avelar da Silva; Thiago Mendonça Ferreira Ramos (J. Autom. Reason., 2023)