Animated Logic: Correct Functional Conversion to Conjunctive Normal Form. - Pedro Barroso; Mário Pereira; António Ravara (PAAR+SC²@IJCAR, 2020)

Leroy and Blazy Were Right: Their Memory Model Soundness Proof is Automatable. - Pedro Barroso; Mário Pereira; António Ravara (VSTTE, 2022)

Leroy and Blazy were right: their memory model soundness proof is automatable (Extended Version). - Pedro Barroso; Mário Pereira; António Ravara (CoRR, 2022)

Hedging with an Edge: Parametric Currency Overlay. - Pedro Barroso; Jurij-Andrei Reichenecker; Marco J. Menichetti (Manag. Sci., 2022)