Preface

Many groups around the world conduct research on formal methods for software development, and in most of these groups, some of the effort goes into the problem of reasoning about loops. There is of course a well-known classic way of dealing with loops, namely by having the software developer provide an invariant, which can be shown to be preserved by the loop. However, experience shows that writing these invariants can be difficult in some cases, trivial but tedious in others, unnecessary in still others. The hope of obviating the need for hand-written invariants, or at least simplifying their production, is what keeps the research on loops alive. Research results tend to be presented at general conferences on formal methods, logic, or mathematics, usually depending on their scope and the methods employed, but this means that researchers using different approaches often do not know about each others ’ work. To improve this situation, we decided to organize a workshop bringing together people interested particularly in reasoning about loops