Deciding KAT and Hoare Logic with Derivatives - Ricardo Almeida 003; Sabine Broda; Nelma Moreira (GandALF, 2012)

Reduction of Nondeterministic Tree Automata. - Ricardo Almeida 003; Lukás Holík; Richard Mayr (TACAS, 2016)

Reducing Nondeterministic Tree Automata by Adding Transitions. - Ricardo Manuel de Oliveira Almeida (MEMICS, 2016)

Efficient algorithms for hard problems in nondeterministic tree automata - Ricardo Manuel de Oliveira Almeida (2017)

A Report on Achieving Complete Regular-Expression Matching using Mealy Machines. - Ricardo Almeida 003 (CoRR, 2022)

Formal Mechanised Semantics of CHERI C: Capabilities, Undefined Behaviour, and Provenance. - Vadim Zaliva; Kayvan Memarian; Ricardo Almeida 003; Jessica Clarke 001; Brooks Davis; Alexander Richardson 001; David Chisnall; Brian Campbell 001; Ian Stark; Robert N. M. Watson; Peter Sewell (ASPLOS (1), 2024)

A CHERI C Memory Model for Verified Temporal Safety. - Vadim Zaliva; Kayvan Memarian; Brian Campbell 001; Ricardo Almeida 003; Nathaniel Wesley Filardo; Ian Stark; Peter Sewell (CPP, 2025)

Morello-Cerise: A Proof of Strong Encapsulation for the Arm Morello Capability Hardware Architecture. - Angus Hammond; Ricardo Almeida 003; Thomas Bauereiss; Brian Campbell 001; Ian Stark; Peter Sewell (Proc. ACM Program. Lang., 2025)