Wolf, Felix A.; Schwerhoff, Malte; Müller, Peter Concise outlines for a complex logic: a proof outline checker for TaDA. (English) Zbl 07785153 Form. Methods Syst. Des. 61, No. 1, 110-136 (2022). MSC: 68Q60 68N30 PDFBibTeX XMLCite \textit{F. A. Wolf} et al., Form. Methods Syst. Des. 61, No. 1, 110--136 (2022; Zbl 07785153) Full Text: DOI arXiv OA License
Wolter, U. E.; Martini, A. R.; Häusler, E. H. Indexed and fibered structures for partial and total correctness assertions. (English) Zbl 1512.68060 Math. Struct. Comput. Sci. 32, No. 9, 1145-1175 (2022). MSC: 68N30 03B70 03G30 18D30 PDFBibTeX XMLCite \textit{U. E. Wolter} et al., Math. Struct. Comput. Sci. 32, No. 9, 1145--1175 (2022; Zbl 1512.68060) Full Text: DOI
Schmid, Georg Stefan; Kunčak, Viktor Generalized arrays for Stainless frames. (English) Zbl 1498.68172 Finkbeiner, Bernd (ed.) et al., Verification, model checking, and abstract interpretation. 23rd international conference, VMCAI 2022, Philadelphia, PA, USA, January 16–18, 2022. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 13182, 332-354 (2022). MSC: 68Q60 03B70 68N30 68V15 PDFBibTeX XMLCite \textit{G. S. Schmid} and \textit{V. Kunčak}, Lect. Notes Comput. Sci. 13182, 332--354 (2022; Zbl 1498.68172) Full Text: DOI
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
Murali, Adithya; Peña, Lucas; Löding, Christof; Madhusudan, P. A first-order logic with frames. (English) Zbl 1508.68072 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, 515-543 (2020). MSC: 68N30 03B70 68Q60 PDFBibTeX XMLCite \textit{A. Murali} et al., Lect. Notes Comput. Sci. 12075, 515--543 (2020; Zbl 1508.68072) Full Text: DOI arXiv
Krishna, Siddharth; Summers, Alexander J.; Wies, Thomas Local reasoning for global graph properties. (English) Zbl 1508.68065 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, 308-335 (2020). MSC: 68N30 03B70 68P05 68Q60 68R10 PDFBibTeX XMLCite \textit{S. Krishna} et al., Lect. Notes Comput. Sci. 12075, 308--335 (2020; Zbl 1508.68065) Full Text: DOI arXiv
Apt, Krzysztof R.; Olderog, Ernst-Rüdiger Fifty years of Hoare’s logic. (English) Zbl 1427.68008 Formal Asp. Comput. 31, No. 6, 751-807 (2019). MSC: 68-03 03B70 68N30 68Q55 PDFBibTeX XMLCite \textit{K. R. Apt} and \textit{E.-R. Olderog}, Formal Asp. Comput. 31, No. 6, 751--807 (2019; Zbl 1427.68008) Full Text: DOI arXiv Link
Bao, Yuyan; Leavens, Gary T.; Ernst, Gidon Unifying separation logic and region logic to allow interoperability. (English) Zbl 1398.68091 Formal Asp. Comput. 30, No. 3-4, 381-441 (2018). MSC: 68N30 03B70 68P05 PDFBibTeX XMLCite \textit{Y. Bao} et al., Formal Asp. Comput. 30, No. 3--4, 381--441 (2018; Zbl 1398.68091) Full Text: DOI
Bannister, Callum; Höfner, Peter; Klein, Gerwin Backwards and forwards with separation logic. (English) Zbl 1511.68067 Avigad, Jeremy (ed.) et al., Interactive theorem proving. 9th international conference, ITP 2018, held as part of the federated logic conference, FloC 2018, Oxford, UK, July 9–12, 2018. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10895, 68-87 (2018). MSC: 68N30 03B70 68V15 PDFBibTeX XMLCite \textit{C. Bannister} et al., Lect. Notes Comput. Sci. 10895, 68--87 (2018; Zbl 1511.68067) Full Text: DOI
Feldman, Yotam M. Y.; Padon, Oded; Immerman, Neil; Sagiv, Mooly; Shoham, Sharon Bounded quantifier instantiation for checking inductive invariants. (English) Zbl 1452.68119 Legay, Axel (ed.) et al., Tools and algorithms for the construction and analysis of systems. 23rd international conference, TACAS 2017, held as part of the European joint conferences on theory and practice of software, ETAPS 2017, Uppsala, Sweden, April 22–29, 2017. Proceedings. Part I. Berlin: Springer. Lect. Notes Comput. Sci. 10205, 76-95 (2017). MSC: 68Q60 03B70 68N30 PDFBibTeX XMLCite \textit{Y. M. Y. Feldman} et al., Lect. Notes Comput. Sci. 10205, 76--95 (2017; Zbl 1452.68119) Full Text: DOI arXiv
Brenas, Jon Haël; Echahed, Rachid; Strecker, Martin Ensuring correctness of model transformations while remaining decidable. (English) Zbl 1482.68085 Sampaio, Augusto (ed.) et al., Theoretical aspects of computing – ICTAC 2016. 13th international colloquium, Taipei, Taiwan, ROC, October 24–31, 2016. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9965, 315-332 (2016). MSC: 68N30 03B70 68Q42 68Q60 68T30 PDFBibTeX XMLCite \textit{J. H. Brenas} et al., Lect. Notes Comput. Sci. 9965, 315--332 (2016; Zbl 1482.68085) Full Text: DOI HAL
Qin, Shengchao; He, Guanhua; Luo, Chenguang; Chin, Wei-Ngan; Chen, Xin Loop invariant synthesis in a combined abstract domain. (English) Zbl 1256.68044 J. Symb. Comput. 50, 386-408 (2013). MSC: 68N30 68N19 68P05 68Q60 PDFBibTeX XMLCite \textit{S. Qin} et al., J. Symb. Comput. 50, 386--408 (2013; Zbl 1256.68044) Full Text: DOI
Parkinson, Matthew J.; Summers, Alexander J. The relationship between separation logic and implicit dynamic frames. (English) Zbl 1326.68104 Barthe, Gilles (ed.), Programming languages and systems. 20th European symposium on programming, ESOP 2011, held as part of the joint European conferences on theory and practice of software, ETAPS 2011, Saarbrücken, Germany, March 26 – April 3, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-19717-8/pbk). Lecture Notes in Computer Science 6602, 439-458 (2011). MSC: 68N30 03B70 68Q60 PDFBibTeX XMLCite \textit{M. J. Parkinson} and \textit{A. J. Summers}, Lect. Notes Comput. Sci. 6602, 439--458 (2011; Zbl 1326.68104) Full Text: DOI arXiv
Clarke, Edmund M. (ed.); Voronkov, Andrei (ed.) Logic for programming, artificial intelligence, and reasoning. 16th international conference, LPAR-16, Dakar, Senegal, April 25 – May 1, 2010. Revised selected papers. (English) Zbl 1203.68004 Lecture Notes in Computer Science 6355. Lecture Notes in Artificial Intelligence. Berlin: Springer (ISBN 978-3-642-17510-7/pbk). x, 517 p. (2010). MSC: 68-06 03-06 03B70 68T27 00B25 PDFBibTeX XMLCite \textit{E. M. Clarke} (ed.) and \textit{A. Voronkov} (ed.), Logic for programming, artificial intelligence, and reasoning. 16th international conference, LPAR-16, Dakar, Senegal, April 25 -- May 1, 2010. Revised selected papers. Berlin: Springer (2010; Zbl 1203.68004) Full Text: DOI