A large fraction of the costs of developing and maintaining software is associated with detecting and fixing software errors. As a result, the last decade has seen a sustained research effort directed toward designing and developing techniques for automatically detecting software errors, with some of these techniques making their way into commercial and open-source tools. However, detecting an error is only the first step toward fixing it. In fact, many known errors remain unpatched due to the high cost required to diagnose and repair them, combined with the fear that patches are more likely to introduce failures compared to other types of code changes. The goal of this research project is to address both of these problems, by devising novel techniques based on dynamic symbolic execution for: (1) automatically testing and verifying the correctness of software patches, and (2) (semi-)automatically generating candidate patches for software bugs. The strength of dynamic symbolic execution lies in its ability to precisely model the behaviour of program paths using mathematical constraints. However, the cost associated with this level of precision is poor scalability. The number of paths in a program is usually exponential in the number of branches, which makes it difficult to scale the analysis to very large programs. However, by focusing the analysis on the incremental changes introduced by program patches, we hope to significantly reduce the cost of symbolic execution and significantly increase its applicability in practice. Furthermore, the ability to check software patches opens up the possibility of performing patch generation in an automatic or semi-automatic fashion. In particular, starting from the mathematical constraints gathered from a buggy execution path -- and with the potential addition of a manually-written patch template -- we plan to design techniques for generating a set of candidate patches resembling the ones that would be generated manually by developers.

We propose to establish a design and development working group (DDWG) to cover exascale science topics in experimental high energy physics (HEP). The HEP computing usage is currently at the preExascale stage and the participation to ExCALIBUR will enable exchange of ideas and good practice with other Sciences at a similar scale to ours. This proposal is put forward by the UK HEP community and aims to foster collaboration with colleagues from other communities. During the first phase of ExCALIBUR the HEP DDWG will provide demonstrators of exascale algorithms and data management infrastructure for the benefit of HEP and beyond. These activities follow the ExCALIBUR four pillars approach and are chosen to provide high research impact in areas of UK leadership evolving towards exascale science in the 2020s. Attachments with full details: - Case for Support - Justification of Resources - Track Record - Workplan - Pathways to Impact Project partners: - StackHPC (letter attached) - Maxeller (letter attached) Support letters: - Joint letter from Worldwide LHC Computing Grid, Hep Software Foundation, IRIS-HEP (international support) - Letter from the Alan Turing Institute