Speaker: Rick Hehner
Title: Practical Predicative Programming Primer
Link to webcast of lecture
http://mediacast.ic.utoronto.ca/20120608-CompSci/index.htm
Abstract:
This talk introduces a method of programming from specifications so that each programming step can be checked by a verifier. Logic errors can be reported the way syntax errors are reported now. Program verification is easier than you think. Invariants and variants are not explicitly needed. The kinds of comments that programmers write, when formalized, are sufficient. And the proofs are well within the abilities of existing provers. This talk (or a close relative) was given at a summer school in Turku, at Verified Software: Theories, Tools, and Experiments Toronto, 2008 October 6-9, and an updated version will be given at Integrated Formal Methods iFM 2012 in Pisa. "Out with a Howl" Series Background, as described by Rick Hehner:
I am retiring, but not quietly. I have given about 160 invited talks, sometimes in a Distinguished Lecturer Series, at many places around the world. But I rarely speak here at my own university (just the occasional practice talk to my own group). So I have decided to give four talks here on my way out. They take place Thursday to Tuesday, June 7 to 12, at 2pm, in BA1240. Everyone is welcome, and no-one is obliged to come. I love to give talks; all I need is one interested listener. All the talks are of general computer science interest, not specialized to my research area (only one is about formal methods, and it's a tutorial introduction). The talks are all reasonably current, and they are arranged in chronological order (oldest to newest). If you can come to only one, make it be the last one.
Biography:
Rick Hehner received his first degree in Mathematics and Physics from Carleton University in 1969, and his PhD in Computer Science from the University of Toronto in 1974. He then joined the faculty, becoming a full professor in 1983, and Bell University Chair in Software Engineering in 2001.
His research has been mainly on the subject of formal programming methods, and the mathematics of program construction in the areas of programming methodology and software engineering. He is the first winner of the annual Computer Science undergraduate teaching award, and he has been a Visiting Scientist at Xerox Research Center, Palo Alto, a Visiting Fellow at Oxford University, a Visiting Researcher at the University of Texas, Austin, Professeur Invité at the Université de Grenoble, a Visiting Professor at UBC, Vancouver, and at the University of Southampton.
Rick has written two books (the Logic of Programming, Prentice-Hall, 1984, and a Practical Theory of Programming, first edition Springer-Verlag 1993, current edition online) and many journal and conference papers. He has given approximately 160 invited lectures at institutions around the world, and he has taught short courses in Marktoberdorf Germany, Macau China, Turku Finland, and Tandil Argentina.
This June, Rick is retiring from the Department of Computer Science after 43 years at the University of Toronto, as both a PhD student and a faculty member.
|