Program correctness and incorrectness are two sides of the same coin. As a programmer, even if you would like to have correctness, you might find yourself spending most of your time reasoning about incorrectness. This includes informal reasoning that people do while looking at or thinking about their code, as well as that supported by automated testing and static analysis tools. This paper describes a logic for program incorrectness which is, in a sense, the the other side of the coin to Hoare’s logic of correctness.
Thu 23 JanDisplayed time zone: Saskatchewan, Central America change
Thu 23 Jan
Displayed time zone: Saskatchewan, Central America change
15:35 - 16:40 | Program LogicsResearch Papers at Ile de France II (IDF II) Chair(s): Chung-Kil Hur Seoul National University | ||
15:35 21mTalk | Deductive Verification with Ghost Monitors Research Papers Martin Clochard ETH Zürich, Claude Marché Inria Saclay & Université Paris-Saclay, Andrei Paskevich LRI, Université Paris-Sud & CNRS Link to publication DOI Media Attached | ||
15:56 21mTalk | The Next 700 Relational Program Logics Research Papers Kenji Maillard Inria Nantes & University of Chile, Cătălin Hriţcu Inria Paris, Exequiel Rivas Inria Paris, Antoine Van Muylder Inria Paris and Paris 7 Link to publication DOI Media Attached File Attached | ||
16:18 21mTalk | Incorrectness Logic Research Papers Peter O'Hearn Facebook Link to publication DOI Media Attached |