# MONO

###### Funder (2)

###### 7 Projects, page 1 of 2

- Project . 2014 - 2016Funder: UKRI Project Code: EP/K039431/1Funder Contribution: 97,999 GBPPartners: MONO, IBM, University of London
Multiprocessor machines are now predominant, as most laptops, desktops, servers, mobile phones and aircrafts routinely have multiple to many cores. Unfortunately, concurrent programming is error-prone, which now affects everyone given this trend towards more and more concurrency. Let us mention for example a recent concurrency bug found in the PostgreSQL database (see http://archives.postgresql.org/pgsql-hackers/2011-08/msg00330.php). PostgreSQL is one of the most popular database nowadays, and many websites rely on its correct functioning. This bug was particularly difficult to observe (and indeed is not fixed yet) because it only occurred on a multicore machine, and a particular hardware platform, IBM Power. Reproducing such bugs is as hard as observing them; thus testing can hardly discover them. To prove a program free of errors, we would like to devise automated techniques that analyse the code without executing it. Thus, we can relieve programmers from the burden of writing the proofs of their programs. Yet, automatic verification of concurrent programs represents a challenge, whether it aims at proving the full correctness of a program (e.g. a program sorting a list actually sorts the list), or at checking specific properties (e.g. the program is free of data races) short of full correctness. We focus here on the latter: we would like to enhance the scalability of tools checking that a concurrent program does not violate certain safety-critical properties of interest. We would like to show that scalable automatic verification can be achieved by exploiting the rich history of partial orders for modeling concurrency.

- Project . 2013 - 2017Funder: UKRI Project Code: EP/K040049/1Funder Contribution: 550,181 GBPPartners: MICROSOFT RESEARCH LIMITED, MONO, University of London
Automatic verification tools based on separation logic have recently enabled the verification of code bases that scale into the millions of lines. Such analyses rely on the use of *inductive predicates* to describe data structures held in memory. However, such predicates are currently hard-coded into the analysis, which means that the analysis must fail when encountering an unknown data structure, not described by the hard-coded definitions. This results in reduced program coverage and increased rates of false negatives. Thus, methods for reasoning with *general* inductively defined predicates could greatly enhance the state of the art. Cyclic proof, in essence, implements reasoning by infinite descent à la Fermat for general inductive definitions. In contrast to traditional proofs by explicit induction, which force the prover to select the induction schema and hypotheses at the very beginning of a proof, cyclic proof allows these difficult decisions to be *postponed* until exploration of the proof search space makes suitable choices more evident. This makes cyclic proof an attractive method for automatic proof search. The main contention of this proposal is that cyclic proof techniques can add inductive reasoning capability, for general inductive predicates, to the many components of an interprocedural program analysis (theorem proving, abduction, frame-inference, abstraction) and thus can significantly extend the reach of current verification methods.

- Project . 2011 - 2012Funder: UKRI Project Code: EP/J002224/1Funder Contribution: 465,503 GBPPartners: MONO, University of Aberdeen, MICROSOFT RESEARCH LIMITED, QMUL, AUSTRALIAN NATIONAL UNIVERSITY
*Resource problems* are pervasive in computer science and the real world; indeed, the fundamental concept of computation is inextricably linked with the concept of resource (time, memory, etc.). Logic provides a powerful and convenient method for expressing and reasoning about properties of resource, and various resource-oriented logics have been advanced for this purpose in the past. Arguably the most successful application of logic-based resource reasoning to date is the use of *separation logic* and its relatives, based on *bunched logic*, to verify memory-manipulating and concurrent computer programs. The techniques employed are, however, highly specialised to the many domain-specific properties of the verification problem; thus they do not straightforwardly transfer to other domains. While the aforementioned advances are significant, we propose that resource-oriented logics can be used to stage a much more wide-ranging and coherent attack on resource problems in general, in line with the central role of resource in a very broad spectrum of application domains. This will be achieved by providing unifying, foundational resource concepts and using these concepts to develop novel applications. Our plan is to take resource reasoning in two main new directions. The first direction is to take a much more general view of resources themselves. For example, one can consider resources which *dualise* (e.g. assets and liabilities in a financial portfolio) or which can be assembled in several different ways (much like LEGO construction bricks). The second direction is to consider not just verification but a variety of other practical resource problems, including resource allocation, scheduling, abduction and planning. These correspond to the way that resource problems arise in a number of fields, but have until now been little addressed by resource logics. We propose that, using suitable resource logics to express resource properties, all of the resource problems above can in fact be recast essentially as *proof search* problems. Such an approach has the potential to significantly unify these diverse resource problems, and open the way for symbolic approaches to them, which could lead to more scalable solutions (as in, e.g., symbolic model checking). Solving these proof search problems will then require search algorithms of considerable sophistication, since the search space may be far too large to explore exhaustively. We plan to employ techniques from automated theorem proving, and from reinforcement learning as used in agent-oriented computing. By combining these techniques with our symbolic methods based upon resource logics, we aim to develop formal methods that are both powerful and widely transferable. If this proposal achieves its research aims then we expect a significant impact on the way that resource allocation, planning and other related resource problems are handled. These problems are fundamental not only to computer science and its various subfields (e.g. distributed systems, agent-oriented computing, and artificial intelligence) but also to other fields such as economics, engineering, environmental science and finance, and to UK industries such as software, electronics, utility provision, transportation and manufacturing.

- Project . 2012 - 2016Funder: UKRI Project Code: EP/J002224/2Funder Contribution: 423,410 GBPPartners: AUSTRALIAN NATIONAL UNIVERSITY, MICROSOFT RESEARCH LIMITED, MONO, University of Aberdeen, University of London
*Resource problems* are pervasive in computer science and the real world; indeed, the fundamental concept of computation is inextricably linked with the concept of resource (time, memory, etc.). Logic provides a powerful and convenient method for expressing and reasoning about properties of resource, and various resource-oriented logics have been advanced for this purpose in the past. Arguably the most successful application of logic-based resource reasoning to date is the use of *separation logic* and its relatives, based on *bunched logic*, to verify memory-manipulating and concurrent computer programs. The techniques employed are, however, highly specialised to the many domain-specific properties of the verification problem; thus they do not straightforwardly transfer to other domains. While the aforementioned advances are significant, we propose that resource-oriented logics can be used to stage a much more wide-ranging and coherent attack on resource problems in general, in line with the central role of resource in a very broad spectrum of application domains. This will be achieved by providing unifying, foundational resource concepts and using these concepts to develop novel applications. Our plan is to take resource reasoning in two main new directions. The first direction is to take a much more general view of resources themselves. For example, one can consider resources which *dualise* (e.g. assets and liabilities in a financial portfolio) or which can be assembled in several different ways (much like LEGO construction bricks). The second direction is to consider not just verification but a variety of other practical resource problems, including resource allocation, scheduling, abduction and planning. These correspond to the way that resource problems arise in a number of fields, but have until now been little addressed by resource logics. We propose that, using suitable resource logics to express resource properties, all of the resource problems above can in fact be recast essentially as *proof search* problems. Such an approach has the potential to significantly unify these diverse resource problems, and open the way for symbolic approaches to them, which could lead to more scalable solutions (as in, e.g., symbolic model checking). Solving these proof search problems will then require search algorithms of considerable sophistication, since the search space may be far too large to explore exhaustively. We plan to employ techniques from automated theorem proving, and from reinforcement learning as used in agent-oriented computing. By combining these techniques with our symbolic methods based upon resource logics, we aim to develop formal methods that are both powerful and widely transferable. If this proposal achieves its research aims then we expect a significant impact on the way that resource allocation, planning and other related resource problems are handled. These problems are fundamental not only to computer science and its various subfields (e.g. distributed systems, agent-oriented computing, and artificial intelligence) but also to other fields such as economics, engineering, environmental science and finance, and to UK industries such as software, electronics, utility provision, transportation and manufacturing.

- Project . 2011 - 2015Funder: EC Project Code: 287767Partners: ENS, University of Twente, REALEYES OU, RIGHTWARE, Codeplay Software, ARM, MONO, RWTH, Imperial