Melquiond, Guillaume; Rieu-Helft, Raphaël WhyMP, a formally verified arbitrary-precision integer library. (English) Zbl 07589741 J. Symb. Comput. 115, 74-95 (2023). MSC: 68Nxx 68Txx 68Qxx PDFBibTeX XMLCite \textit{G. Melquiond} and \textit{R. Rieu-Helft}, J. Symb. Comput. 115, 74--95 (2023; Zbl 07589741) Full Text: DOI
Lucanu, Dorel; Rusu, Vlad; Arusoaie, Andrei A generic framework for symbolic execution: a coinductive approach. (English) Zbl 1356.68044 J. Symb. Comput. 80, Part 1, 125-163 (2017). MSC: 68N30 68Q55 68W30 PDFBibTeX XMLCite \textit{D. Lucanu} et al., J. Symb. Comput. 80, Part 1, 125--163 (2017; Zbl 1356.68044) Full Text: DOI HAL
Moy, Yannick; Marché, Claude Modular inference of subprogram contracts for safety checking. (English) Zbl 1213.68385 J. Symb. Comput. 45, No. 11, 1184-1211 (2010). MSC: 68Q60 PDFBibTeX XMLCite \textit{Y. Moy} and \textit{C. Marché}, J. Symb. Comput. 45, No. 11, 1184--1211 (2010; Zbl 1213.68385) Full Text: DOI