Griffin, Matt; Dongol, Brijesh Verifying secure speculation in Isabelle/HOL. (English) Zbl 1521.68077 Huisman, Marieke (ed.) et al., Formal methods. 24th international symposium, FM 2021, virtual event, November 20–26, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 13047, 43-60 (2021). MSC: 68Q60 68N30 68Q55 68V15 PDFBibTeX XMLCite \textit{M. Griffin} and \textit{B. Dongol}, Lect. Notes Comput. Sci. 13047, 43--60 (2021; Zbl 1521.68077) Full Text: DOI
Mansky, William; Honoré, Wolf; Appel, Andrew W. Connecting higher-order separation logic to a first-order outside world. (English) Zbl 1508.68070 Müller, Peter (ed.), Programming languages and systems. 29th European symposium on programming, ESOP 2020, held as part of the European joint conferences on theory and practice of software, ETAPS 2020, Dublin, Ireland, April 25–30, 2020. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12075, 428-455 (2020). MSC: 68N30 03B70 68Q60 PDFBibTeX XMLCite \textit{W. Mansky} et al., Lect. Notes Comput. Sci. 12075, 428--455 (2020; Zbl 1508.68070) Full Text: DOI
Lundberg, Didrik; Guanciale, Roberto; Lindner, Andreas; Dam, Mads Hoare-style logic for unstructured programs. (English) Zbl 1476.68064 de Boer, Frank (ed.) et al., Software engineering and formal methods. 18th international conference, SEFM 2020, Amsterdam, The Netherlands, September 14–18, 2020. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12310, 193-213 (2020). MSC: 68N30 03B70 68V15 PDFBibTeX XMLCite \textit{D. Lundberg} et al., Lect. Notes Comput. Sci. 12310, 193--213 (2020; Zbl 1476.68064) Full Text: DOI Link
Syeda, Hira Taqdees; Klein, Gerwin Formal reasoning under cached address translation. (English) Zbl 1468.68070 J. Autom. Reasoning 64, No. 5, 911-945 (2020). MSC: 68N25 03B70 68N30 68V15 PDFBibTeX XMLCite \textit{H. T. Syeda} and \textit{G. Klein}, J. Autom. Reasoning 64, No. 5, 911--945 (2020; Zbl 1468.68070) Full Text: DOI
Paulson, Lawrence C. Computational logic: its origins and applications. (English) Zbl 1402.68160 Proc. R. Soc. Lond., A, Math. Phys. Eng. Sci. 474, No. 2210, Article ID 20170872, 14 p. (2018). MSC: 68T15 68-03 01A60 01A61 03B35 03B70 68Q60 PDFBibTeX XMLCite \textit{L. C. Paulson}, Proc. R. Soc. Lond., A, Math. Phys. Eng. Sci. 474, No. 2210, Article ID 20170872, 14 p. (2018; Zbl 1402.68160) Full Text: DOI arXiv
Bauereiß, Thomas; Pesenti Gritti, Armando; Popescu, Andrei; Raimondi, Franco CoSMed: a confidentiality-verified social media platform. (English) Zbl 1451.68168 J. Autom. Reasoning 61, No. 1-4, 113-139 (2018). MSC: 68Q60 68V15 PDFBibTeX XMLCite \textit{T. Bauereiß} et al., J. Autom. Reasoning 61, No. 1--4, 113--139 (2018; Zbl 1451.68168) Full Text: DOI Link
Vu, Dieu-Huong; Chiba, Yuki; Yatake, Kenro; Aoki, Toshiaki Checking the conformance of a Promela design to its formal specification in Event-B. (English) Zbl 1328.68131 Artho, Cyrille (ed.) et al., Formal techniques for safety-critical systems. Third international workshop, FTSCS 2014, Luxembourg, November 6–7, 2014. Revised selected papers. Cham: Springer (ISBN 978-3-319-17580-5/pbk; 978-3-319-17581-2/ebook). Communications in Computer and Information Science 476, 110-126 (2015). MSC: 68Q60 68N30 PDFBibTeX XMLCite \textit{D.-H. Vu} et al., Commun. Comput. Inf. Sci. 476, 110--126 (2015; Zbl 1328.68131) Full Text: DOI
Cheng, Shu; Woodcock, Jim; D’Souza, Deepak Using formal reasoning on a model of tasks for FreeRTOS. (English) Zbl 1328.68044 Formal Asp. Comput. 27, No. 1, 167-192 (2015). MSC: 68N25 68Q60 PDFBibTeX XMLCite \textit{S. Cheng} et al., Formal Asp. Comput. 27, No. 1, 167--192 (2015; Zbl 1328.68044) Full Text: DOI
Boldo, Sylvie; Clément, François; Filliâtre, Jean-Christophe; Mayero, Micaela; Melquiond, Guillaume; Weis, Pierre Trusting computations: a mechanized proof from partial differential equations to actual program. (English) Zbl 1369.35051 Comput. Math. Appl. 68, No. 3, 325-352 (2014). MSC: 35Q35 65M06 68Q60 65G20 68T15 65M12 PDFBibTeX XMLCite \textit{S. Boldo} et al., Comput. Math. Appl. 68, No. 3, 325--352 (2014; Zbl 1369.35051) Full Text: DOI arXiv
Alkassar, Eyad; Böhme, Sascha; Mehlhorn, Kurt; Rizkallah, Christine A framework for the verification of certifying computations. (English) Zbl 1314.68180 J. Autom. Reasoning 52, No. 3, 241-273 (2014). MSC: 68Q60 68T15 PDFBibTeX XMLCite \textit{E. Alkassar} et al., J. Autom. Reasoning 52, No. 3, 241--273 (2014; Zbl 1314.68180) Full Text: DOI arXiv
Marić, Filip; Janičić, Predrag Formalization of abstract state transition systems for SAT. (English) Zbl 1237.68179 Log. Methods Comput. Sci. 7, No. 3, Paper No. 19, 37 p. (2011). MSC: 68T15 68Q60 PDFBibTeX XMLCite \textit{F. Marić} and \textit{P. Janičić}, Log. Methods Comput. Sci. 7, No. 3, Paper No. 19, 37 p. (2011; Zbl 1237.68179) Full Text: DOI arXiv