Cousot, Patrick On fixpoint/iteration/variant induction principles for proving total correctness of programs with denotational semantics. (English) Zbl 1502.68078 Gabbrielli, Maurizio (ed.), Logic-based program synthesis and transformation. 29th international symposium, LOPSTR 2019, Porto, Portugal, October 8–10, 2019. Revised selected papers. Cham: Springer. Lect. Notes Comput. Sci. 12042, 3-18 (2020). MSC: 68N30 68Q55 68Q60 PDFBibTeX XMLCite \textit{P. Cousot}, Lect. Notes Comput. Sci. 12042, 3--18 (2020; Zbl 1502.68078) Full Text: DOI
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
Xu, Zhaowei; Zhang, Wenhui; Sui, Yuefei Completeness of Hoare logic relative to the standard model. (English) Zbl 1444.03122 Steffen, Bernhard (ed.) et al., SOFSEM 2017: theory and practice of computer science. 43rd international conference on current trends in theory and practice of computer science, Limerick, Ireland, January 16–20, 2017, Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10139, 119-131 (2017). MSC: 03B70 03C62 03F30 PDFBibTeX XMLCite \textit{Z. Xu} et al., Lect. Notes Comput. Sci. 10139, 119--131 (2017; Zbl 1444.03122) Full Text: DOI arXiv
Komuravelli, Anvesh; Gurfinkel, Arie; Chaki, Sagar SMT-based model checking for recursive programs. (English) Zbl 1358.68072 Form. Methods Syst. Des. 48, No. 3, 175-205 (2016). MSC: 68N30 68Q60 PDFBibTeX XMLCite \textit{A. Komuravelli} et al., Form. Methods Syst. Des. 48, No. 3, 175--205 (2016; Zbl 1358.68072) Full Text: DOI arXiv
Platzer, André Ernst-Rüdiger Olderog: a life for meaning. (English) Zbl 1360.01041 Meyer, Roland (ed.) et al., Correct system design. Symposium in honor of Ernst-Rüdiger Olderog on the occasion of his 60th birthday, Oldenburg, Germany, September 8–9, 2015. Proceedings. Cham: Springer (ISBN 978-3-319-23505-9/pbk; 978-3-319-23506-6/ebook). Lecture Notes in Computer Science 9360, 5-9 (2015). MSC: 01A70 PDFBibTeX XMLCite \textit{A. Platzer}, Lect. Notes Comput. Sci. 9360, 5--9 (2015; Zbl 1360.01041) Full Text: DOI
Bjørner, Nikolaj; Gurfinkel, Arie; McMillan, Ken; Rybalchenko, Andrey Horn clause solvers for program verification. (English) Zbl 1465.68044 Beklemishev, Lev D. (ed.) et al., Fields of logic and computation II. Essays dedicated to Yuri Gurevich on the occasion of his 75th birthday. Cham: Springer. Lect. Notes Comput. Sci. 9300, 24-51 (2015). MSC: 68N30 03B70 68Q60 PDFBibTeX XMLCite \textit{N. Bjørner} et al., Lect. Notes Comput. Sci. 9300, 24--51 (2015; Zbl 1465.68044) Full Text: DOI
Honda, Kohei; Yoshida, Nobuko; Berger, Martin An observationally complete program logic for imperative higher-order functions. (English) Zbl 1358.68071 Theor. Comput. Sci. 517, 75-101 (2014). MSC: 68N30 03B70 PDFBibTeX XMLCite \textit{K. Honda} et al., Theor. Comput. Sci. 517, 75--101 (2014; Zbl 1358.68071) Full Text: DOI
Crolard, T.; Polonowski, E. Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control. (English) Zbl 1259.03044 J. Log. Algebr. Program. 81, No. 3, 181-208 (2012). MSC: 03B70 68N18 68N30 68Q60 PDFBibTeX XMLCite \textit{T. Crolard} and \textit{E. Polonowski}, J. Log. Algebr. Program. 81, No. 3, 181--208 (2012; Zbl 1259.03044) Full Text: DOI arXiv
Leivant, Daniel On the completeness of dynamic logic. (English) Zbl 1234.03019 de Alfaro, Luca (ed.), Foundations of software science and computational structures. 12th international conference, FOSSACS 2009, held as part of the joint European conferences on theory and practice of software, ETAPS 2009, York, UK, March 22–29, 2009. Proceedings. Berlin: Springer (ISBN 978-3-642-00595-4/pbk). Lecture Notes in Computer Science 5504, 78-91 (2009). MSC: 03B70 68N30 PDFBibTeX XMLCite \textit{D. Leivant}, Lect. Notes Comput. Sci. 5504, 78--91 (2009; Zbl 1234.03019) Full Text: DOI
Clarke, Edmund M. The birth of model checking. (English) Zbl 1142.68046 Grumberg, Orna (ed.) et al., 25 years of model checking. History, achievements, perspectives. Berlin: Springer (ISBN 978-3-540-69849-4/pbk). Lecture Notes in Computer Science 5000, 1-26 (2008). Reviewer: Klaus D. Kiermeier (Berlin) MSC: 68Q60 03B44 03B70 68-03 68Q85 PDFBibTeX XMLCite \textit{E. M. Clarke}, Lect. Notes Comput. Sci. 5000, 1--26 (2008; Zbl 1142.68046) Full Text: DOI
Gravell, Andrew M. Verification conditions are code. (English) Zbl 1106.68066 Acta Inf. 43, No. 6, 431-447 (2007). MSC: 68Q60 PDFBibTeX XMLCite \textit{A. M. Gravell}, Acta Inf. 43, No. 6, 431--447 (2007; Zbl 1106.68066) Full Text: DOI Link
Compton, Kevin J. Stratified least fixpoint logic. (English) Zbl 0815.03018 Theor. Comput. Sci. 131, No. 1, 95-120 (1994). Reviewer: M.Duží (Praha) MSC: 03B70 68Q60 68N17 PDFBibTeX XMLCite \textit{K. J. Compton}, Theor. Comput. Sci. 131, No. 1, 95--120 (1994; Zbl 0815.03018) Full Text: DOI Link
German, Steven M. Semantics and reasoning with free procedures. (English) Zbl 0769.68095 Theor. Comput. Sci. 97, No. 1, 67-81 (1992). MSC: 68Q60 PDFBibTeX XMLCite \textit{S. M. German}, Theor. Comput. Sci. 97, No. 1, 67--81 (1992; Zbl 0769.68095) Full Text: DOI
Hungar, Hardi Complexity of proving program correctness. (English) Zbl 1493.68111 Ito, Takayasu (ed.) et al., Theoretical aspects of computer software. International conference TACS ’91, Sendai, Japan, September 24–27, 1991. Proceedings. Berlin etc.: Springer-Verlag. Lect. Notes Comput. Sci. 526, 459-474 (1991). MSC: 68N30 03B70 68Q15 PDFBibTeX XMLCite \textit{H. Hungar}, Lect. Notes Comput. Sci. 526, 459--474 (1991; Zbl 1493.68111) Full Text: DOI
Szczepanska, Danuta A Hoare-like verification system for a language with an exception handling mechanism. (English) Zbl 0745.68077 Theor. Comput. Sci. 80, No. 2, 319-335 (1991). MSC: 68Q60 PDFBibTeX XMLCite \textit{D. Szczepanska}, Theor. Comput. Sci. 80, No. 2, 319--335 (1991; Zbl 0745.68077) Full Text: DOI
German, Steven M.; Clarke, Edmund M.; Halpern, Joseph Y. Reasoning about procedures as parameters in the language L4. (English) Zbl 0692.68011 Inf. Comput. 83, No. 3, 265-359 (1989). MSC: 68Q60 68N01 68Q55 PDFBibTeX XMLCite \textit{S. M. German} et al., Inf. Comput. 83, No. 3, 265--359 (1989; Zbl 0692.68011) Full Text: DOI
Grabowski, Michał Arithmetical completeness versus relative completeness. (English) Zbl 0667.03018 Stud. Log. 47, No. 3, 213-220 (1989). Reviewer: H.Nishimura MSC: 03B70 68Q65 03H15 PDFBibTeX XMLCite \textit{M. Grabowski}, Stud. Log. 47, No. 3, 213--220 (1989; Zbl 0667.03018) Full Text: DOI
Sannella, Donald; Tarlecki, Andrzej Specifications in an arbitrary institution. (English) Zbl 0654.68017 Inf. Comput. 76, No. 2-3, 165-210 (1988). Reviewer: H.-D.Ehrich MSC: 68N01 68P05 68Q65 03B10 68Q60 68T15 PDFBibTeX XMLCite \textit{D. Sannella} and \textit{A. Tarlecki}, Inf. Comput. 76, No. 2--3, 165--210 (1988; Zbl 0654.68017) Full Text: DOI
Fraenkel, Aviezri S. Wythoff games, continued fractions, cedar trees and Fibonacci searches. (English) Zbl 0557.90107 Theor. Comput. Sci. 30, 49-73 (1984). Reviewer: I.Dragan MSC: 91A05 11A55 68Q25 91A20 05C05 PDFBibTeX XMLCite \textit{A. S. Fraenkel}, Theor. Comput. Sci. 30, 49--73 (1984; Zbl 0557.90107) Full Text: DOI
Nepejvoda, N. N. Semantics of algorithmic languages. (English) Zbl 0554.68006 J. Sov. Math. 25, 1558-1606 (1984). MSC: 68-02 68Q60 68Q55 PDFBibTeX XMLCite \textit{N. N. Nepejvoda}, J. Sov. Math. 25, 1558--1606 (1984; Zbl 0554.68006) Full Text: DOI
Traub, J. F.; Wasilkowski, G. W.; Woźniakowski, H. Average case optimality for linear problems. (English) Zbl 0543.68029 Theor. Comput. Sci. 30, 1-25 (1984). MSC: 68Q25 68W99 PDFBibTeX XMLCite \textit{J. F. Traub} et al., Theor. Comput. Sci. 30, 1--25 (1984; Zbl 0543.68029) Full Text: DOI
Olderog, Ernst-Rüdiger Correctness of programs with Pascal-like procedures without global variables. (English) Zbl 0534.68016 Theor. Comput. Sci. 30, 49-90 (1984). MSC: 68Q60 PDFBibTeX XMLCite \textit{E.-R. Olderog}, Theor. Comput. Sci. 30, 49--90 (1984; Zbl 0534.68016) Full Text: DOI
Bergstra, J. A.; Klop, J. W. Proving program inclusion using Hoare’s logic. (English) Zbl 0533.68011 Theor. Comput. Sci. 30, 1-48 (1984). MSC: 68Q60 68P05 PDFBibTeX XMLCite \textit{J. A. Bergstra} and \textit{J. W. Klop}, Theor. Comput. Sci. 30, 1--48 (1984; Zbl 0533.68011) Full Text: DOI Link
Olderog, Ernst-Ruediger On the notion of expressiveness and the rule of adaptation. (English) Zbl 0511.68006 Theor. Comput. Sci. 24, 337-347 (1983). MSC: 68N01 68Q60 PDFBibTeX XMLCite \textit{E.-R. Olderog}, Theor. Comput. Sci. 24, 337--347 (1983; Zbl 0511.68006) Full Text: DOI
Bergstra, J. A.; Tucker, J. V. Expressiveness and the completeness of Hoare’s logic. (English) Zbl 0549.68021 J. Comput. Syst. Sci. 25, 267-284 (1982). Reviewer: J.-J.Ch.Meyer MSC: 68Q65 68Q60 03D60 03C35 03B60 PDFBibTeX XMLCite \textit{J. A. Bergstra} and \textit{J. V. Tucker}, J. Comput. Syst. Sci. 25, 267--284 (1982; Zbl 0549.68021) Full Text: DOI Link
Kirkerud, Bjorn Completeness of Hoare-calculi revisited. (English) Zbl 0506.68030 BIT 22, 402-418 (1982). MSC: 68Q65 PDFBibTeX XMLCite \textit{B. Kirkerud}, BIT 22, 402--418 (1982; Zbl 0506.68030) Full Text: DOI
Bergstra, J. A.; Tucker, J. V. Some natural structures which fail to possess a sound and decidable Hoare-like logic for their while-programs. (English) Zbl 0483.68033 Theor. Comput. Sci. 17, 303-315 (1982). MSC: 68Q65 68Q60 03D35 03B25 PDFBibTeX XMLCite \textit{J. A. Bergstra} and \textit{J. V. Tucker}, Theor. Comput. Sci. 17, 303--315 (1982; Zbl 0483.68033) Full Text: DOI Link
Langmaack, Hans On termination problems for finitely interpreted ALGOL-like programs. (English) Zbl 0478.68013 Acta Inf. 18, 79-108 (1982). MSC: 68Q60 68Q65 PDFBibTeX XMLCite \textit{H. Langmaack}, Acta Inf. 18, 79--108 (1982; Zbl 0478.68013) Full Text: DOI
Bellia, M. Hierarchical development of programming languages. (English) Zbl 0477.68015 Calcolo 18, 219-254 (1981). MSC: 68N01 PDFBibTeX XMLCite \textit{M. Bellia}, Calcolo 18, 219--254 (1981; Zbl 0477.68015) Full Text: DOI
Trakhtenbrot, B. A. Completeness of algorithmic logic. (English. Russian original) Zbl 0459.68002 Cybernetics 15, 160-166 (1979); translation from Kibernetika 1979, No. 2, 6-11 (1979). MSC: 68W99 03B60 68N01 68Q65 PDFBibTeX XMLCite \textit{B. A. Trakhtenbrot}, Cybernetics 15, 160--166 (1979; Zbl 0459.68002); translation from Kibernetika 1979, No. 2, 6--11 (1979) Full Text: DOI
Clarke, E. M. Program invariants as fixedpoints. (English) Zbl 0399.68022 Computing 21, 273-294 (1979). MSC: 68Q60 PDFBibTeX XMLCite \textit{E. M. Clarke}, Computing 21, 273--294 (1979; Zbl 0399.68022) Full Text: DOI