V&D on Monday, August 21st

Session 1: Practice (08:30‑10:30)
Chair: Roderick Bloem

08:30‑09:15	John Moondanos (Future Formal Technologies Group, Logic Design Group, Intel) From Error to Error: Debugging in the Era of Multi-core Designs
09:15‑10:00	Alper Sen (Freescale Semiconductor Inc) Error Diagnosis in Equivalence Checking of High Performance Microprocessors
10:00‑10:30	Lionel van den Berg (University of Queensland) Paul Strooper (University of Queensland) Wendy Johnston (University of Queensland) An Automated Approach for the Interpretation of Counter-Examples Model checking is an automatic technique used for the verification of finite systems. A model checker explores the full state space of a given model and checks it against a set of requirements. If a state exists in which a requirement is not satisfied most tools will generate a counter-example. Counter-examples are useful for debugging a model and determining if an error exists in the modelled system. However, they can be difficult for end users to understand and this may limit the take-up of model checking in industry. This paper describes a domain-specific approach to automatically interpreting counter-examples and presenting the results in an intuitive form to the end user. Our research extends previous work on model checking railway signalling control tables with signalling engineers from Queensland Rail.

Break (10:30‑11:00)

Session 2: Debugging (11:00‑12:30)
Chair: Fabio Somenzi

11:00‑11:30

Jooyong Lee (BRICS, Department of Computer Science, University of Aarhus) Dynamic Reverse Code Generation for Backward Execution Need for backward execution in debuggers has been raised a number of times. Backward execution helps a user naturally think backwards and, in turn, easily locate the cause of a bug. Backward execution has been implemented mostly by state-saving or checkpointing, which are inherently not scalable. In this paper, we present a method to generate reverse code, so that backtracking can be performed by executing reverse code. The novelty of our work is that we generate reverse code on-the-fly, while running a debugger, which makes it possible to apply the method even to debugging multi-threaded programs.

11:30‑12:30

Andreas Zeller (University of Saarbruecken) Where Do Bugs Come From? [pdf]

Lunch break (12:30‑14:00)

Session 3: Fault Localization (14:00‑15:30)
Chair: Marco Roveri

14:00‑15:00

Wolfgang Mayer (UniSA) Markus Stumptner (UniSA) Model-Based Debugging -- State of the Art And Future Challenges A considerable body of work on model-based software debugging (MBSD) has been published in the past decade. We summarise the underlying ideas and present the different approaches as abstractions of the concrete semantics of the programming language. Subsequently, we map and compare the model-based framework to other well-known Automated Debugging approaches according to multiple criteria and present open issues, challenges and potential future directions of MBSD.

15:00‑15:30

Irith Pomeranz (Purdue University) Sudhakar Reddy (University of Iowa) On the Use of Functional Test Generation in Diagnostic Test Generation for Synchronous Sequential Circuits We study the relationship between diagnostic test generation for a gate-level fault model, which is used for generating diagnostic test sets for manufacturing defects, and functional test generation for a high-level fault model. In general, a functional fault may partially represent some of the effects of one gate-level fault but not another. Generating a test sequence for the functional fault is then likely to detect one gate-level fault but not the other, thus distinguishing the two faults. This relationship points to the ability to use a functional test generation procedure (that targets functional fault detection) as a way to generate diagnostic test sequences for gate-level faults. We use this observation in two ways. The more direct way is to define functional faults that correspond to the differences between pairs of gate-level faults. The second way is to use functional test sequences as diagnostic test sequences without explicitly considering gate-level faults. We support the use of the resulting procedures with experimental results.

Break (15:30‑16:00)

Session 4: From Localization to Correction (16:00‑18:00)
Chair: Alex Groce

16:00‑16:30	Andreas Griesmayer, Stefan Staber and Roderick Bloem Automated Fault Localization for C Programs If software does not fulfill a given specification, a model checker can be used to search for a counterexample, a run which demonstrates the wrong behavior. Even with a counterexample, locating the actual fault in the source code is often a difficult task to be performed manually by the verification engineer. We present an automatic approach for fault localization in C programs. The method is based on model checking and reports only components that can be changed such that the difference between actual and intended behavior of the example is removed. To identify these components, we use the bounded model checker CBMC on an instrumented version of the checked software. We present experimental data that supports the applicability of our approach.
16:30‑17:30	Martin Rinard (MIT) Automated Techniques for Surviving Software Errors [ppt] Many deployed software systems must often operate completely on their own, with little or no prospect of timely human intervention if things go wrong, either because human operators are not available or because human reaction times are too long to be of practical use. This talk presents a set of techniques that can enable such programs to continue to execute through otherwise fatal errors. Because these techniques forcibly coerce the program into potentially unanticipated states that provide continued execution, our evaluation of the viability of these techniques is necessarily empirical. Our initial results indicate that these techniques usually provide a viable and, in the right context, much more useful alternative to standard fail-stop approaches.
17:30‑18:00	Juan Carlos López Pimentel (Tecnológico de Monterrey, Campus Estado de México) Raúl Monroy (Tecnológico de Monterrey-Campus Estado de México) Dieter Hutter (DFKI) A method for patching interleaving-replay attacks in faulty security protocols The verification of security protocols has attracted a lot of interest in the formal methods community, yielding two main verification approaches: i) state exploration, e.g.~FDR~\cite{Lowe96} and OFMC [Basin03]; and ii) theorem proving, e.g.~the Isabelle inductive method [Paulson98] and Coral [CORAL03]. Complementing formal methods, Abadi and Needham's principles aim to guide the design of security protocols in order to make them simple and, hopefully, correct [AN96]. We are interested in a problem related to verification but far less explored: the correction of faulty security protocols. Experience has shown that the analysis of counterexamples or failed proof attempts often holds the key to the completion of proofs and for the correction of a faulty model. In this paper, we introduce a method for patching faulty security protocols that are susceptible to a replay attack. Our method makes use of Abadi and Needham's principles to the prudent engineering practice for cryptographic protocols in order to guide the location of the fault in a protocol as well as the proposition of candidate patches. We have run a test on our method with encouraging results. The test set includes 21 faulty security protocols borrowed from the Clark-Jacob library [Clark-Jacob].