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
Swierstra, Wouter; Alpuim, Joao From proposition to program. Embedding the refinement calculus in Coq. (English) Zbl 1475.68458 Kiselyov, Oleg (ed.) et al., Functional and logic programming. 13th international symposium, FLOPS 2016, Kochi, Japan, March 4–6, 2016. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9613, 29-44 (2016). MSC: 68V20 68N18 68Q60 PDFBibTeX XMLCite \textit{W. Swierstra} and \textit{J. Alpuim}, Lect. Notes Comput. Sci. 9613, 29--44 (2016; Zbl 1475.68458) Full Text: DOI
Zeyda, Frank; Cavalcanti, Ana Mechanical reasoning about families of UTP theories. (English) Zbl 1243.68270 Sci. Comput. Program. 77, No. 4, 444-479 (2012). MSC: 68T15 68N15 68Q60 PDFBibTeX XMLCite \textit{F. Zeyda} and \textit{A. Cavalcanti}, Sci. Comput. Program. 77, No. 4, 444--479 (2012; Zbl 1243.68270) Full Text: DOI
Hallerstede, Stefan; Leuschel, Michael Experiments in program verification using Event-B. (English) Zbl 1242.68067 Formal Asp. Comput. 24, No. 1, 97-125 (2012). MSC: 68N30 68Q60 PDFBibTeX XMLCite \textit{S. Hallerstede} and \textit{M. Leuschel}, Formal Asp. Comput. 24, No. 1, 97--125 (2012; Zbl 1242.68067) Full Text: DOI
Frade, Maria João; Pinto, Jorge Sousa Verification conditions for source-level imperative programs. (English) Zbl 1298.68171 Comput. Sci. Rev. 5, No. 3, 252-277 (2011). MSC: 68Q60 03B70 68N30 68-02 PDFBibTeX XMLCite \textit{M. J. Frade} and \textit{J. S. Pinto}, Comput. Sci. Rev. 5, No. 3, 252--277 (2011; Zbl 1298.68171) Full Text: DOI Link
Duran, Adolfo; Cavalcanti, Ana; Sampaio, Augusto An algebraic approach to the design of compilers for object-oriented languages. (English) Zbl 1214.68126 Formal Asp. Comput. 22, No. 5, 489-535 (2010). MSC: 68N20 68N15 68N19 PDFBibTeX XMLCite \textit{A. Duran} et al., Formal Asp. Comput. 22, No. 5, 489--535 (2010; Zbl 1214.68126) Full Text: DOI Link
Bertot, Yves Structural abstract interpretation: a formal study using Coq. (English) Zbl 1250.68089 Bove, Ana (ed.) et al., Language engineering and rigorous software development. International LerNet ALFA Summer School 2008, Piriapolis, Uruguay, February 24–March 1, 2008. Revised tutorial lectures. Berlin: Springer (ISBN 978-3-642-03152-6/pbk). Lecture Notes in Computer Science 5520, 153-194 (2009). MSC: 68N30 68T15 PDFBibTeX XMLCite \textit{Y. Bertot}, Lect. Notes Comput. Sci. 5520, 153--194 (2009; Zbl 1250.68089) Full Text: DOI arXiv
Buchberger, Bruno; Crǎciun, Adrian; Jebelean, Tudor; Kovács, Laura; Kutsia, Temur; Nakagawa, Koji; Piroi, Florina; Popov, Nikolaj; Robu, Judit; Rosenkranz, Markus; Windsteiger, Wolfgang Theorema: Towards computer-aided mathematical theory exploration. (English) Zbl 1107.68095 J. Appl. Log. 4, No. 4, 470-504 (2006). MSC: 68T15 13P10 PDFBibTeX XMLCite \textit{B. Buchberger} et al., J. Appl. Log. 4, No. 4, 470--504 (2006; Zbl 1107.68095) Full Text: DOI