Beringer, Lennart; Appel, Andrew W. Abstraction and subsumption in modular verification of C programs. (English) Zbl 1505.68023 Form. Methods Syst. Des. 58, No. 1-2, 322-345 (2021). MSC: 68Q60 03B70 68N15 68N30 PDFBibTeX XMLCite \textit{L. Beringer} and \textit{A. W. Appel}, Form. Methods Syst. Des. 58, No. 1--2, 322--345 (2021; Zbl 1505.68023) Full Text: DOI
Garzella, Jack J.; Baranowski, Marek; He, Shaobo; Rakamarić, Zvonimir Leveraging compiler intermediate representation for multi- and cross-language verification. (English) Zbl 1451.68071 Beyer, Dirk (ed.) et al., Verification, model checking, and abstract interpretation. 21st international conference, VMCAI 2020, New Orleans, LA, USA, January 16–21, 2020. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11990, 90-111 (2020). MSC: 68N20 68N15 68Q60 PDFBibTeX XMLCite \textit{J. J. Garzella} et al., Lect. Notes Comput. Sci. 11990, 90--111 (2020; Zbl 1451.68071) Full Text: DOI
Menghi, Claudio; Spoletini, Paola; Chechik, Marsha; Ghezzi, Carlo A verification-driven framework for iterative design of controllers. (English) Zbl 1425.68262 Formal Asp. Comput. 31, No. 5, 459-502 (2019). MSC: 68Q60 03B44 68N99 68Q45 PDFBibTeX XMLCite \textit{C. Menghi} et al., Formal Asp. Comput. 31, No. 5, 459--502 (2019; Zbl 1425.68262) Full Text: DOI
Mandrykin, M. U.; Khoroshilov, A. V. Region analysis for deductive verification of C programs. (English. Russian original) Zbl 1452.68051 Program. Comput. Softw. 42, No. 5, 257-278 (2016); translation from Programmirovanie 42, No. 5, 3-29 (2016). MSC: 68N30 68N15 68Q55 68Q60 PDFBibTeX XMLCite \textit{M. U. Mandrykin} and \textit{A. V. Khoroshilov}, Program. Comput. Softw. 42, No. 5, 257--278 (2016; Zbl 1452.68051); translation from Programmirovanie 42, No. 5, 3--29 (2016) Full Text: DOI
Jacobs, Bart; Vogels, Frédéric; Piessens, Frank Featherweight VeriFast. (English) Zbl 1448.68221 Log. Methods Comput. Sci. 11, No. 3, Paper No. 19, 57 p. (2015). MSC: 68N30 03B70 68N15 68N19 68Q60 PDFBibTeX XMLCite \textit{B. Jacobs} et al., Log. Methods Comput. Sci. 11, No. 3, Paper No. 19, 57 p. (2015; Zbl 1448.68221) Full Text: DOI arXiv
Greenaway, David; Andronick, June; Klein, Gerwin Bridging the gap: automatic verified abstraction of C. (English) Zbl 1360.68751 Beringer, Lennart (ed.) et al., Interactive theorem proving. Third international conference, ITP 2012, Princeton, NJ, USA, August 13–15, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-32346-1/pbk). Lecture Notes in Computer Science 7406, 99-115 (2012). MSC: 68T15 68N15 68Q60 PDFBibTeX XMLCite \textit{D. Greenaway} et al., Lect. Notes Comput. Sci. 7406, 99--115 (2012; Zbl 1360.68751) Full Text: DOI
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
Böhme, Sascha; Moskal, Michał; Schulte, Wolfram; Wolff, Burkhart HOL-Boogie – an interactive prover-backend for the verifying C compiler. (English) Zbl 1185.68211 J. Autom. Reasoning 44, No. 1-2, 111-144 (2010). MSC: 68N20 68Q60 68T15 PDFBibTeX XMLCite \textit{S. Böhme} et al., J. Autom. Reasoning 44, No. 1--2, 111--144 (2010; Zbl 1185.68211) Full Text: DOI