Pearce, David J.; Utting, Mark; Groves, Lindsay Verifying Whiley programs with Boogie. (English) Zbl 1512.68059 J. Autom. Reasoning 66, No. 4, 747-803 (2022). MSC: 68N30 68Q60 68V15 PDFBibTeX XMLCite \textit{D. J. Pearce} et al., J. Autom. Reasoning 66, No. 4, 747--803 (2022; Zbl 1512.68059) Full Text: DOI
Runge, Tobias; Potanin, Alex; Thüm, Thomas; Schaefer, Ina Traits: correctness-by-construction for free. (English) Zbl 1499.68067 Mousavi, Mohammad Reza (ed.) et al., Formal techniques for distributed objects, components, and systems. 42nd IFIP WG 6.1 international conference, FORTE 2022, held as part of the 17th international federated conference on distributed computing techniques, DisCoTec 2022, Lucca, Italy, June 13–17, 2022. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 13273, 131-150 (2022). MSC: 68N30 PDFBibTeX XMLCite \textit{T. Runge} et al., Lect. Notes Comput. Sci. 13273, 131--150 (2022; Zbl 1499.68067) Full Text: DOI arXiv
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
Eilers, Marco; Meier, Severin; Müller, Peter Product programs in the wild: retrofitting program verifiers to check information flow security. (English) Zbl 1493.68106 Silva, Alexandra (ed.) et al., Computer aided verification. 33rd international conference, CAV 2021, virtual event, July 20–23, 2021. Proceedings. Part I. Cham: Springer. Lect. Notes Comput. Sci. 12759, 718-741 (2021). MSC: 68N30 68N19 68Q60 PDFBibTeX XMLCite \textit{M. Eilers} et al., Lect. Notes Comput. Sci. 12759, 718--741 (2021; Zbl 1493.68106) Full Text: DOI
Matsushita, Yusuke; Tsukada, Takeshi; Kobayashi, Naoki RustHorn: CHC-based verification for Rust programs. (English) Zbl 1508.68071 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, 484-514 (2020). MSC: 68N30 68Q60 PDFBibTeX XMLCite \textit{Y. Matsushita} et al., Lect. Notes Comput. Sci. 12075, 484--514 (2020; Zbl 1508.68071) Full Text: DOI arXiv
Neider, Daniel; Madhusudan, P.; Saha, Shambwaditya; Garg, Pranav; Park, Daejun A learning-based approach to synthesizing invariants for incomplete verification engines. (English) Zbl 1468.68074 J. Autom. Reasoning 64, No. 7, 1523-1552 (2020). MSC: 68N30 68P05 68Q60 68T05 PDFBibTeX XMLCite \textit{D. Neider} et al., J. Autom. Reasoning 64, No. 7, 1523--1552 (2020; Zbl 1468.68074) Full Text: DOI arXiv
Summers, Alexander J.; Müller, Peter Automating deductive verification for weak-memory programs. (English) Zbl 1423.68111 Beyer, Dirk (ed.) et al., Tools and algorithms for the construction and analysis of systems. 24th international conference, TACAS 2018, held as part of the European joint conferences on theory and practice of software, ETAPS 2018, Thessaloniki, Greece, April 14–20, 2018. Proceedings. Part I. Cham: Springer. Lect. Notes Comput. Sci. 10805, 190-209 (2018). MSC: 68N30 68Q60 68T15 PDFBibTeX XMLCite \textit{A. J. Summers} and \textit{P. Müller}, Lect. Notes Comput. Sci. 10805, 190--209 (2018; Zbl 1423.68111) Full Text: DOI arXiv
Dinsdale-Young, Thomas; da Rocha Pinto, Pedro; Gardner, Philippa A perspective on specifying and verifying concurrent modules. (English) Zbl 1395.68187 J. Log. Algebr. Methods Program. 98, 1-25 (2018). MSC: 68Q60 68N30 68Q85 PDFBibTeX XMLCite \textit{T. Dinsdale-Young} et al., J. Log. Algebr. Methods Program. 98, 1--25 (2018; Zbl 1395.68187) 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
Filliâtre, Jean-Christophe; Gondelman, Léon; Paskevich, Andrei The spirit of ghost code. (English) Zbl 1358.68070 Form. Methods Syst. Des. 48, No. 3, 152-174 (2016). MSC: 68N30 68Q60 PDFBibTeX XMLCite \textit{J.-C. Filliâtre} et al., Form. Methods Syst. Des. 48, No. 3, 152--174 (2016; Zbl 1358.68070) Full Text: DOI HAL
Leino, K. Rustan M.; Lucio, Paqui An assertional proof of the stability and correctness of Natural Mergesort. (English) Zbl 1367.68080 ACM Trans. Comput. Log. 17, No. 1, Article No. 6, 22 p. (2015). MSC: 68P10 68Q60 68T15 PDFBibTeX XMLCite \textit{K. R. M. Leino} and \textit{P. Lucio}, ACM Trans. Comput. Log. 17, No. 1, Article No. 6, 22 p. (2015; Zbl 1367.68080) 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
Roşu, Grigore From rewriting logic, to programming language semantics, to program verification. (English) Zbl 1321.68337 Martí-Oliet, Narciso (ed.) et al., Logic, rewriting, and concurrency. Essays dedicated to José Meseguer on the occasion of his 65th birthday. Cham: Springer (ISBN 978-3-319-23164-8/pbk; 978-3-319-23165-5/ebook). Lecture Notes in Computer Science 9200, 598-616 (2015). MSC: 68Q42 03B70 68N30 68Q55 68Q60 PDFBibTeX XMLCite \textit{G. Roşu}, Lect. Notes Comput. Sci. 9200, 598--616 (2015; Zbl 1321.68337) Full Text: DOI
Daum, Matthias; Billing, Nelson; Klein, Gerwin Concerned with the unprivileged: user programs in kernel refinement. (English) Zbl 1342.68079 Formal Asp. Comput. 26, No. 6, 1205-1229 (2014). MSC: 68N30 68Q60 PDFBibTeX XMLCite \textit{M. Daum} et al., Formal Asp. Comput. 26, No. 6, 1205--1229 (2014; Zbl 1342.68079) Full Text: DOI
Dodds, Josiah; Appel, Andrew W. Mostly sound type system improves a foundational program verifier. (English) Zbl 1426.68045 Gonthier, Georges (ed.) et al., Certified programs and proofs. Third international conference, CPP 2013, Melbourne, VIC, Australia, December 11–13, 2013. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 8307, 17-32 (2013). MSC: 68N30 68V15 PDFBibTeX XMLCite \textit{J. Dodds} and \textit{A. W. Appel}, Lect. Notes Comput. Sci. 8307, 17--32 (2013; Zbl 1426.68045) Full Text: DOI
Křena, Bohuslav; Vojnar, Tomáš Automated formal analysis and verification: an overview. (English) Zbl 1286.68318 Int. J. Gen. Syst. 42, No. 4, 335-365 (2013). MSC: 68Q60 68T15 68N30 PDFBibTeX XMLCite \textit{B. Křena} and \textit{T. Vojnar}, Int. J. Gen. Syst. 42, No. 4, 335--365 (2013; Zbl 1286.68318) Full Text: DOI
Anureev, I. S.; Mar’yasov, Il’ya; Nepomniashchiĭ, V. A. Two-level mixed verification method of C-light programs in terms of safety logic. (English) Zbl 1374.68269 Jt. Bull. NCC IIS, Ser. Comput. Sci. 34, 23-42 (2012). MSC: 68Q60 68N30 68Q55 PDFBibTeX XMLCite \textit{I. S. Anureev} et al., Jt. Bull. NCC IIS, Ser. Comput. Sci. 34, 23--42 (2012; Zbl 1374.68269) Full Text: Link
Hatcliff, John; Leavens, Gary T.; Leino, K. Rustan M.; Müller, Peter; Parkinson, Matthew Behavioral interface specification languages. (English) Zbl 1293.68078 ACM Comput. Surv. 44, No. 3, Paper No. 7, 58 p. (2012). MSC: 68N30 68Q60 68-02 PDFBibTeX XMLCite \textit{J. Hatcliff} et al., ACM Comput. Surv. 44, No. 3, Paper No. 7, 58 p. (2012; Zbl 1293.68078) Full Text: DOI
Leino, K. Rustan M.; Yessenov, Kuat Stepwise refinement of heap-manipulating code in Chalice. (English) Zbl 1259.68034 Formal Asp. Comput. 24, No. 4-6, 519-535 (2012). MSC: 68N30 PDFBibTeX XMLCite \textit{K. R. M. Leino} and \textit{K. Yessenov}, Formal Asp. Comput. 24, No. 4--6, 519--535 (2012; Zbl 1259.68034) Full Text: DOI Link
Giorgino, Mathieu; Strecker, Martin Correctness of pointer manipulating algorithms illustrated by a verified BDD construction. (English) Zbl 1372.68062 Giannakopoulou, Dimitra (ed.) et al., FM 2012: Formal methods. 18th international symposium, Paris, France, August 27–31, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-32758-2/pbk). Lecture Notes in Computer Science 7436, 202-216 (2012). MSC: 68N30 68Q60 68T15 PDFBibTeX XMLCite \textit{M. Giorgino} and \textit{M. Strecker}, Lect. Notes Comput. Sci. 7436, 202--216 (2012; Zbl 1372.68062) Full Text: DOI
Siegel, Stephen F.; Zirkel, Timothy K. Loop invariant symbolic execution for parallel programs. (English) Zbl 1326.68106 Kuncak, Viktor (ed.) et al., Verification, model checking, and abstract interpretation. 13th international conference, VMCAI 2012, Philadelphia, PA, USA, January 22–24, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-27939-3/pbk). Lecture Notes in Computer Science 7148, 412-427 (2012). MSC: 68N30 68Q60 PDFBibTeX XMLCite \textit{S. F. Siegel} and \textit{T. K. Zirkel}, Lect. Notes Comput. Sci. 7148, 412--427 (2012; Zbl 1326.68106) Full Text: DOI
Promsky, A. V. Error-tracing axiomatic semantics for C-kernel. (English) Zbl 1374.68115 Jt. Bull. NCC IIS, Ser. Comput. Sci. 31, 123-138 (2010). MSC: 68N30 03B70 68N19 68Q55 68Q60 PDFBibTeX XMLCite \textit{A. V. Promsky}, Jt. Bull. NCC IIS, Ser. Comput. Sci. 31, 123--138 (2010; Zbl 1374.68115) Full Text: Link
Hoenicke, Jochen; Leino, K. Rustan M.; Podelski, Andreas; Schäf, Martin; Wies, Thomas Doomed program points. (English) Zbl 1211.68090 Form. Methods Syst. Des. 37, No. 2-3, 171-199 (2010). MSC: 68N30 68Q60 PDFBibTeX XMLCite \textit{J. Hoenicke} et al., Form. Methods Syst. Des. 37, No. 2--3, 171--199 (2010; Zbl 1211.68090) Full Text: DOI
Leino, K. Rustan M. Dafny: an automatic program verifier for functional correctness. (English) Zbl 1253.68095 Clarke, Edmund M. (ed.) et al., Logic for programming, artificial intelligence, and reasoning. 16th international conference, LPAR-16, Dakar, Senegal, April 25 – May 1, 2010. Revised selected papers. Berlin: Springer (ISBN 978-3-642-17510-7/pbk). Lecture Notes in Computer Science 6355. Lecture Notes in Artificial Intelligence, 348-370 (2010). MSC: 68N30 68Q60 PDFBibTeX XMLCite \textit{K. R. M. Leino}, Lect. Notes Comput. Sci. 6355, 348--370 (2010; Zbl 1253.68095) Full Text: DOI
Naumann, David A.; Banerjee, Anindya Dynamic boundaries: information hiding by second order framing with first order assertions. (English) Zbl 1260.68112 Gordon, Andrew D. (ed.), Programming languages and systems. 19th European symposium on programming, ESOP 2010, held as part of the joint European conferences on theory and practice of software, ETAPS 2010, Paphos, Cyprus, March 20–28, 2010. Proceedings. Berlin: Springer (ISBN 978-3-642-11956-9/pbk). Lecture Notes in Computer Science 6012, 2-22 (2010). MSC: 68N30 PDFBibTeX XMLCite \textit{D. A. Naumann} and \textit{A. Banerjee}, Lect. Notes Comput. Sci. 6012, 2--22 (2010; Zbl 1260.68112) Full Text: DOI
Kreiker, Jörg; Seidl, Helmut; Vojdani, Vesal Shape analysis of low-level C with overlapping structures. (English) Zbl 1273.68086 Barthe, Gilles (ed.) et al., Verification, model checking, and abstract interpretation. 11th international conference, VMCAI 2010, Madrid, Spain, January 17–19, 2010. Proceedings. Berlin: Springer (ISBN 978-3-642-11318-5/pbk). Lecture Notes in Computer Science 5944, 214-230 (2010). MSC: 68N30 68P05 PDFBibTeX XMLCite \textit{J. Kreiker} et al., Lect. Notes Comput. Sci. 5944, 214--230 (2010; Zbl 1273.68086) Full Text: DOI