HOWARD-60: Editor's Preface

This book is a Festschriift volume dedicated to Howard Barringer's 60th birthday. It was created from revised papers presented at the Higher-Order Workshop on Automated Runtime verification and Debugging (HOWARD-60), held at the University of Manchester on December 20, 2011.

HOWARD-60 brought scientists from both academia and industry together to debate how to monitor, analyse and guide the execution of programs to ensure their correctness. The ultimate longer term goal is to investigate the use of lightweight formal methods applied during the execution of programs from the following two points of view. On the one hand, whether the runtime application of formal methods is a viable complement to the traditional methods of proving programs correct before their execution, such as model checking and theorem proving. On the other hand, whether formality improves traditional ad-hoc monitoring techniques used in performance monitoring, distributed debugging, etc. Dynamic program monitoring and analysis can occur during testing or during operation.

But most importantly, the workshop was mainly attended by friends and colleagues of Howard Barringer. For this reason, we saw many talks taking a lighthearted, fun, or historical perspective on research ideas related to Howard's long career. 

The workshop programme included the following talks.

• Marta Kwiatkowska. On Incremental Quantitative Verification for Probabilistic Systems
• Graham Birtwistle and Kenneth Stevens. FSM Design Spaces and Their Patterns
• Murdoch Gabbay. Stone Duality for First-Order Logic: a Nominal Approach to Logic and Topology
• Ursula Martin and Alison Pease. 1377 Questions and Counting – What Can We Learn Fom Online Math?
• Bill Roscoe, Gavin Lowe, Joel Ouaknine and Philip Armstrong. Model Checking Timed CSP
• Clare Dixon and Michael Fisher. On and On the Temporal Way
• Timothy Hinrichs, A. Prasad Sistla and Lenore D. Zuck. Model Checking Meets Run-Time Verification
• Ylies Falcone, Jean-Claude Fernandez and Laurent Mounier. On the Expressiveness of Some Runtime Validation Techniques
• David Rydeheard and Jesus Hector Dominguez Sanchez. A Note on Minimum Model Reasoning
• Howard Bowman and Li Su. Cognition, Concurrency Theory and Reverberations in the Brain: In Research of a Calculus of Communicating Neural Systems
• Eva Navarro-Lopez. DYVERSE: Putting Together the Pieces of the Hybrid Systems’ Jigsaw
• Doron Peled. Distributed Control Synthesis
• Klaus Havelund. Where Specification and Programming Meet
• Colin Stirling. Tableaux with Names for Modal and Temporal Logics with Fixpoints
• Michael Gabbay. The Proof Theoretic Foundations of Logic, Computation and Computationalism
• Ruurd Kuiper. Pandora’s Black Box
• Cliff Jones. Mechanising LPF
• Simon Thompson. Getting Engaged

HOWARD-60 was partially sponsored by the Centre for Interdisciplinary Computational and Dynamical Analysis at the University of Manchester and hosted at the University of Manchester.

This book includes research papers and an article about Howard written by Klaus Havelund with the help of Cliff Jones.