Peña, Ricardo An assertional proof of red-black trees using Dafny. (English) Zbl 1468.68082 J. Autom. Reasoning 64, No. 4, 767-791 (2020). MSC: 68P05 68V15 PDFBibTeX XMLCite \textit{R. Peña}, J. Autom. Reasoning 64, No. 4, 767--791 (2020; Zbl 1468.68082) Full Text: DOI
Montenegro, Manuel; Peña, Ricardo; Sánchez-Hernández, Jaime A generic intermediate representation for verification condition generation. (English) Zbl 1473.68051 Falaschi, Moreno (ed.), Logic-based program synthesis and transformation. 25th international symposium, LOPSTR 2015, Siena, Italy, July 13–15, 2015. Revised selected papers. Cham: Springer. Lect. Notes Comput. Sci. 9527, 227-243 (2015). MSC: 68N30 68Q60 PDFBibTeX XMLCite \textit{M. Montenegro} et al., Lect. Notes Comput. Sci. 9527, 227--243 (2015; Zbl 1473.68051) Full Text: DOI