Imperial College London

ProfessorPhilippaGardner

Faculty of EngineeringDepartment of Computing

Professor of Theoretical Computer Science
 
 
 
//

Contact

 

+44 (0)20 7594 8292p.gardner Website

 
 
//

Location

 

453Huxley BuildingSouth Kensington Campus

//

Summary

 

Publications

Publication Type
Year
to

88 results found

Gardner P, Smith GD, Wright AD, Resource Reasoning about Mashups, Verified Software: Theories, Tools and Experiments, VSTTE’10, VS-Theory workhsop

Conference paper

Watt C, Maksimovic P, Neelakantan R K, Gardner Pet al., A program logic for first-order encapsulated WebAssembly, 33rd European Conference on Object-Oriented Programming (ECOOP 2019)., Publisher: Leibniz-Zentrum für Informatik, Dagstuhl Publishing, ISSN: 1868-8969

We introduce Wasm Logic, a sound program logic for first-order, encapsulated WebAssembly. Wedesign a novel assertion syntax, tailored to WebAssembly’s stack-based semantics and the strongguarantees given by WebAssembly’s type system, and show how to adapt the standard separationlogic triple and proof rules in a principled way to capture WebAssembly’s uncommon structuredcontrol flow. Using Wasm Logic, we specify and verify a simple WebAssembly B-tree library, givingabstract specifications independent of the underlying implementation. We mechanise Wasm Logicand its soundness proof in full in Isabelle/HOL. As part of the soundness proof, we formaliseand fully mechanise a novel, big-step semantics of WebAssembly, which we prove equivalent, upto transitive closure, to the original WebAssembly small-step semantics. Wasm Logic is the firstprogram logic for WebAssembly, and represents a first step towards the creation of static analysistools for WebAssembly.

Conference paper

Fragoso Santos J, Maksimovic P, Cunha Sampaio G, Gardner Pet al., 2019, JaVerT 2.0: Compositional Symbolic Execution for JavaScript, Proceedings of the ACM on Programming Languages, Vol: 3, ISSN: 2475-1421

We propose a novel, unified approach to the development of compositional symbolic execution tools, bridging the gap between classical symbolic execution and compositional program reasoning based on separation logic. Using this approach, we build JaVerT 2.0, a symbolic analysis tool for JavaScript that follows the language semantics without simplifications. JaVerT 2.0 supports whole-program symbolic testing, verification, and, for the first time, automatic compositional testing based on bi-abduction. The meta-theory underpinning JaVerT 2.0 is developed modularly, streamlining the proofs and informing the implementation. Our explicit treatment of symbolic execution errors allows us to give meaningful feedback to the developer during whole-program symbolic testing and guides the inference of resource of the bi-abductive execution. We evaluate the performance of JaVerT 2.0 on a number of JavaScript data-structure libraries, demonstrating: the scalability of our whole-program symbolic testing; an improvement over the state-of-the-art in JavaScript verification; and the feasibility of automatic compositional testing for JavaScript.

Journal article

Bodin M, Gardner P, Jensen T, Schmitt Aet al., 2019, Skeletal semantics and their interpretations, Proceedings of the ACM on Programming Languages, Vol: 3, ISSN: 2475-1421

The development of mechanised language specification based on structured operational semantics, with applications to verified compilers and sound program analysis, requires huge effort. General theory and frameworks have been proposed to help with this effort. However, none of this work provides a systematic way of developing concrete and abstract semantics, connected together by a general consistency result. We introduce a skeletal semantics of a language, where each skeleton describes the complete semantic behaviour of a language construct. We define a general notion of interpretation, which provides a systematic and language-independent way of deriving semantic judgements from the skeletal semantics. We explore four generic interpretations: a simple well-formedness interpretation; a concrete interpretation; an abstract interpretation; and a constraint generator for flow-sensitive analysis. We prove general consistency results between interpretations, depending only on simple language-dependent lemmas. We illustrate our ideas using a simple While language.

Journal article

Gardner P, 2018, JaVerT: JavaScript Verification and Testing Framework, 20th International Symposium on Principles and Practice of Declarative Programming (PPDP), Publisher: ASSOC COMPUTING MACHINERY

Conference paper

Faustino Fragoso Femenin Dos Santos J, Maksimovic P, Grohens T, Dolby J, Gardner PAet al., 2018, Symbolic execution for JavaScript, 20th International Symposium on Principles and Practice of Declarative Programming, PPDP 2018, Publisher: ACM

We present a framework for trustworthy symbolic execution of JavaScripts programs, whose aim is to assist developers in the testing of their code: the developer writes symbolic tests for which the framework provides concrete counter-models. We create the framework following a new, general methodology for designing compositional program analyses for dynamic languages. We prove that the underlying symbolic execution is sound and does not generate false positives. We establish additional trust by using the theory to precisely guide the implementation and by thorough testing. We apply our framework to whole-program symbolic testing of real-world JavaScript libraries and compositional debugging of separation logic specifications of JavaScript programs.

Conference paper

Ntzik G, da Rocha Pinto P, Sutherland JHJ, Gardner PAet al., A concurrent specification of POSIX file systems, 32nd European Conference on Object-Oriented Programming (ECOOP 2018)

POSIX is a standard for operating systems, with a substantial part devoted to specifying file-system operations. File-system operations exhibit complex concurrent behaviour, comprising multiple actions affecting different parts of the state: typically, multiple atomic reads followed by an atomic update. However, the standard’s description of concurrent behaviour is nsatisfactory: it is fragmented; contains ambiguities; and is generally under-specified. We provide a formal concurrent specification of POSIX file systems and demonstrate scalable reasoning for clients. Our specification is based on a concurrent specification language, which uses a modern concurrent separation logic for reasoning about abstract atomic operations, and an associated refinement calculus. Our reasoning about clients highlights an important difference between reasoning about modules built over a heap, where the interference on the shared state is restricted to the operations of the module, and modules built over a file system, where the interference cannot be restricted as the file system is a public namespace. We introduce specifications conditional on context invariants used to restrict the interference, and apply our reasoning to the example of lock files.

Conference paper

Dinsdale-Young TW, da Rocha Pinto P, Gardner PA, 2018, A perspective on specifying and verifying concurrent modules, Journal of Logical and Algebraic Methods in Programming, Vol: 98, Pages: 1-25, ISSN: 2352-2208

The specification of a concurrent program module, and the verification of implementations and clients with respect to such a specification, are difficult problems. A specification should be general enough that any reasonable implementation satisfies it, yet precise enough that it can be used by any reasonable client. We survey a range of techniques for specifying concurrent modules, using the example of a counter module to illustrate the benefits and limitations of each. In particular, we highlight four key concepts underpinning these techniques: auxiliary state, interference abstraction, resource ownership and atomicity. We demonstrate how these concepts can be combined to achieve two powerful approaches for specifying concurrent modules and verifying implementations and clients, which remove the limitations highlighted by the counter example.

Journal article

Faustino Fragoso Femenin Dos Santos J, Maksimovic P, Naudziuniene D, Wood T, Gardner PAet al., 2018, JaVerT: JavaScript verification toolchain, Proceedings of the ACM on Programming Languages, Vol: 2, ISSN: 2475-1421

The dynamic nature of JavaScript and its complex semantics make it a difficult target for logic-based verification. We introduce JaVerT, a semi-automatic JavaScript Verification Toolchain, based on separation logic and aimed at the specialist developer wanting rich, mechanically verified specifications of critical JavaScript code. To specify JavaScript programs, we design abstractions that capture its key heap structures (for example, prototype chains and function closures), allowing the developer to write clear and succinct specifications with minimal knowledge of the JavaScript internals. To verify JavaScript programs, we develop JaVerT, a verification pipeline consisting of: JS-2-JSIL, a well-tested compiler from JavaScript to JSIL, an intermediate goto language capturing the fundamental dynamic features of JavaScript; JSIL Verify, a semi-automatic verification tool based on a sound JSIL separation logic; and verified axiomatic specifications of the JavaScript internal functions. Using JaVerT, we verify functional correctness properties of: data-structure libraries (key-value map, priority queue) written in an object-oriented style; operations on data structures such as binary search trees (BSTs) and lists; examples illustrating function closures; and test cases from the official ECMAScript test suite. The verification times suggest that reasoning about larger, more complex code using JaVerT is feasible.

Journal article

Gardner P, 2017, Verified trustworthy software systems, Philosophical Transactions of the Royal Society A. Mathematical, Physical and Engineering Sciences, Vol: 375, ISSN: 1364-503X

Journal article

Faustino Fragoso Femenin Dos Santos J, Gardner P, Naudziuniene D, Maksimovic Pet al., 2017, Towards logic-based verification of javascript programs, 26th Conference on Automated Deduction (CADE 26), Publisher: Springer Verlag, Pages: 8-25, ISSN: 0302-9743

In this position paper, we argue for what we believe is a correct pathway to achieving scalable symbolic verification of JavaScript based on separation logic. We highlight the difficulties imposed by the language, the current state-of-the-art in the literature, and the sequence of steps that needs to be taken. We briefly describe JaVerT, our semiautomatic toolchain for JavaScript verification.

Conference paper

Xiong S, da Rocha Pinto P, Ntzik G, Gardner Pet al., 2017, Abstract specifications for concurrent maps, 26th European Symposium on Programming, ESOP 2017, Publisher: Springer Berlin Heidelberg, Pages: 964-990

Despite recent advances in reasoning about concurrent datastructure libraries, the largest implementations injava.util.concurrenthave yet to be verified. The key issue lies in the development of modularspecifications, which provide clear logical boundaries between clients andimplementations. A solution is to use recent advances in fine-grained con-currency reasoning, in particular the introduction ofabstract atomicityto concurrent separation logic reasoning. We present two specificationsof concurrent maps, both providing the clear boundaries we seek. Weshow that these specifications are equivalent, in that they can be builtfrom each other. We show how we can verify client programs, such as aconcurrent set and a producer-consumer client. We also give a substan-tial first proof that the main operations ofConcurrentSkipListMapinjava.util.concurrentsatisfy the map specification. This work demon-strates that we now have the technology to verify the largest implemen-tations injava.util.concurrent.

Conference paper

Dinsdale-Young T, da Rocha Pinto P, Just Andersen K, Birkedal Let al., 2017, Caper: automatic verification for fine-grained concurrency, 26th European Symposium on Programming, ESOP 2017, Publisher: Springer Berlin Heidelberg, Pages: 420-447

Recent program logics based on separation logic emphasisea modular approach to proving functional correctness for ne-grainedconcurrent programs. However, these logics have no automation support.In this paper, we presentCaper, a prototype tool for automated reason-ing in such a logic.Caperis based on symbolic execution, integratingreasoning about interference on shared data and about ghost resourcesthat are used to mediate this interference. This enablesCaperto verifythe functional correctness of ne-grained concurrent algorithms.

Conference paper

Xiong S, da Rocha Pinto P, Ntzik G, Gardner Pet al., 2017, Abstract Specifications for Concurrent Maps (Extended Version), Abstract Specifications for Concurrent Maps, Publisher: Department of Computing, Imperial College London, 2017/1

Despite recent advances in reasoning about concurrent data structure libraries, the largest implementations in java.util.concurrent have yet to be verified. The key issue lies in the development of modular specifications, which provide clear logical boundaries between clients and implementations. A solution is to use recent advances in fine-grained concurrency reasoning, in particular the introduction of abstract atomicity to concurrent separation logic reasoning. We present two specifications of concurrent maps, both providing the clear boundaries we seek. We show that these specifications are equivalent, in that they can be built from each other. We show how we can verify client programs, such as a concurrent set and a producer-consumer client. We also give a substantial first proof that the main operations of ConcurrentSkipListMap in java.util.concurrent satisfy the map specification. This work demonstrates that we now have the technology to verify the largest implementations in java.util.concurrent.

Report

Raad A, Hobor A, Villard J, Gardner Pet al., 2016, Verifying concurrent graph algorithms, Asian Symposium on Programming Languages and Systems, Publisher: Springer Verlag, Pages: 314-334, ISSN: 0302-9743

We show how to verify four challenging concurrent fine-grained graph-manipulating algorithms, including graph copy, a speculatively parallel Dijkstra, graph marking and spanning tree. We develop a reasoning method for such algorithms that dynamically tracks the contributions and responsibilities of each thread operating on a graph, even in cases of arbitrary recursive thread creation. We demonstrate how to use a logic without abstraction ( Open image in new window ) to carry out abstract reasoning in the style of iCAP, by building the abstraction into the proof structure rather than incorporating it into the semantic model of the logic.

Conference paper

Raad A, Fragoso Santos J, Gardner P, 2016, DOM: Specification and Client Reasoning, Asian Symposium on Programming Languages and Systems, Publisher: Springer Verlag, Pages: 401-422, ISSN: 0302-9743

We present an axiomatic specification of a key fragment of DOM using structural separation logic. This specification allows us to develop modular reasoning about client programs that call the DOM.

Conference paper

da Rocha Pinto P, Dinsdale-Young T, Gardner PA, Sutherland Jet al., 2016, Modular Termination Verification for Non-blocking Concurrency, 25th European Symposium on Programming, ESOP 2016, Publisher: Springer Berlin Heidelberg, Pages: 176-201, ISSN: 0302-9743

We present Total-TaDA, a program logic for verifying the total correctness of concurrent programs: that such programs both terminate and produce the correct result. With Total-TaDA, we can specify constraints on a thread’s concurrent environment that are necessary to guarantee termination. This allows us to verify total correctness for non-blocking algorithms, e.g. a counter and a stack. Our specifications can express lock- and wait-freedom. More generally, they can express that one operation cannot impede the progress of another, a new non-blocking property we call non-impedance. Moreover, our approach is modular. We can verify the operations of a module independently, and build up modules on top of each other.

Conference paper

da Rocha Pinto P, Dinsdale-Young T, Gardner P, Sutherland Jet al., 2016, Modular Termination Verification for Non-blocking Concurrency (Extended Version), Modular Termination Verification for Non-blocking Concurrency, Publisher: Department of Computing, Imperial College London, 2016/6

We present Total-TaDA, a program logic for verifying the total correctness of concurrent programs: that such programs both terminate and produce the correct result. With Total-TaDA, we can specify constraints on a thread’s concurrent environment that are necessary to guarantee termination. This allows us to verify total correctness for non-blocking algorithms, e.g. a counter and a stack. Our specifications can express lock- and wait-freedom. More generally, they can express that one operation cannot impede the progress of another, a new non-blocking property we call non-impedance. Moreover, our approach is modular. We can verify the operations of a module independently, and build up modules on top of each other.

Report

da Rocha Pinto P, Gardner PA, Dinsdale-Young T, 2015, Steps in Modular Specifications for Concurrent Modules (Invited Tutorial Paper), Mathematical Foundations of Programming Semantics XXXI (MFPS 2015), ISSN: 1571-0661

Conference paper

Ntzik G, da Rocha Pinto P, Gardner PA, 2015, Fault-tolerant resource reasoning, 13th Asian Symposium on Programming Languages and Systems, Publisher: Springer International Publishing, Pages: 169-188, ISSN: 0302-9743

Separation logic has been successful at verifying that programs do not crash due to illegal use of resources. The underlying assumption, however, is that machines do not fail. In practice, machines can fail unpredictably for various reasons, e.g. power loss, corrupting resources. Critical software, e.g. file systems, employ recovery methods to mitigate these effects. We introduce an extension of the Views framework to reason about such methods. We use concurrent separation logic as an instance of the framework to illustrate our reasoning, and explore programs using write-ahead logging, e.g. an ARIES recovery algorithm.

Conference paper

Ntzik G, Gardner P, 2015, Reasoning about the POSIX file system: Local update and global pathnames, 2015 ACM SIGPLAN International Conference on Object-Oriented Programming Systems Languages and Applications (OOPSLA 2015), Publisher: ACM, Pages: 201-220

We introduce a program logic for specifying a core sequential subset of the POSIX file system and for reasoning abstractly about client programs working with the file system. The challenge is to reason about the combination of local directory update and global pathname traversal (including '..' and symbolic links) which may overlap the directories being updated. Existing reasoning techniques are either based on first-order logic and do not scale, or on separation logic and can only handle linear pathnames (no '..' or symbolic links). We introduce fusion logic for reasoning about local update and global pathname traversal, introducing a novel effect frame rule to propagate the effect of a local update on overlapping pathnames. We apply our reasoning to the standard recursive remove utility (rm -r), discovering bugs in well-known implementations.

Conference paper

Ntzik G, da Rocha Pinto P, Gardner P, 2015, Fault-tolerant Resource Reasoning (Extended Version), London, United Kingdom, Publisher: Department of Computing, Imperial College London

Separation logic has been successful at verifying that programs do not crash due to illegal use of resources. The underlying assumption, however, is that machines do not fail. In practice, machines can fail unpredictably for various reasons, e.g. power loss, corrupting resources. Critical software, e.g. file systems, employ recovery methods to mitigate these effects. We introduce an extension of the Views framework to reason about such methods. We use concurrent separation logic as an instance of the framework to illustrate our reasoning, and explore programs using write-ahead logging, e.g. an ARIES recovery algorithm.

Report

Ntzik G, Gardner P, 2015, Reasoning about the POSIX File System: Local Update and Global Pathnames, Technical Report

We introduce a program logic for specifying a core sequential subset of the POSIX file system and for reasoning abstractly about client programs working with the file system. The challenge is to reason about the combination of local directory update and global pathname traversal (including '..' and symbolic links) which may overlap the directories being updated. Existing reasoning techniques are either based on first-order logic and do not scale, or on separation logic and can only handle linear pathnames (no '..' or symbolic links). We introduce fusion logic for reasoning about local update and global pathname traversal, introducing a novel effect frame rule to propagate the effect of a local update on overlapping pathnames. We apply our reasoning to the standard recursive remove utility (rm -r), discovering bugs in well-known implementations.

Report

Gardner P, Smith G, Watt C, Wood Tet al., 2015, A Trusted Mechanised Specification of JavaScript: One Year On, 27th International Conference on Computer Aided Verification, Publisher: Springer, Pages: 3-10, ISSN: 0302-9743

The JSCert project provides a Coq mechanised specification of the core JavaScript language. A key part of the project was to develop a methodology for establishing trust, by designing JSCert in such a way as to provide a strong connection with the JavaScript standard, and by developing JSRef, a reference interpreter which was proved correct with respect to JSCert and tested using the standard Test262 test suite. In this paper, we assess the previous state of the project at POPL’14 and the current state of the project at CAV’15. We evaluate the work of POPL’14, providing an analysis of the methodology as a whole and a more detailed analysis of the tests. We also describe recent work on extending JSRef to include Google’s V8 Array library, enabling us to cover more of the language and to pass more tests.

Conference paper

Gardner PA, Raad A, Villard J, 2015, CoLoSL: Concurrent Local Subjective Logic, 24th European Symposium on Programming, ESOP 2015, Publisher: Springer, Pages: 710-735, ISSN: 0302-9743

Conference paper

Gardner P, Raad A, Wheelhouse M, Wright Aet al., 2014, Abstract Local Reasoning for Concurrent Libraries: Mind the Gap, Mathematical Foundations of Programming Semantics Thirtieth Conference, MFPS 2014

Conference paper

Gardner P, Ntzik G, Wright A, 2014, Local Reasoning for the POSIX File System, 23rd European Symposium on Programming, ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014

Conference paper

Bodin M, Chargueraud A, Filaretti D, Gardner P, Maffeis S, Naudziuniene D, Schmitt A, Smith Get al., 2014, A Trusted Mechanised JavaScript Specification, 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), Publisher: Association for Computing Machinery (ACM), Pages: 87-100, ISSN: 1523-2867

Conference paper

da Rocha Pinto P, Dinsdale-Young T, Gardner P, 2014, TaDA: A Logic for Time and Data Abstraction (Extended Version), TaDA: A Logic for Time and Data Abstraction, London, United Kingdom, Publisher: Department of Computing, Imperial College London, DTR14-7

To avoid data races, concurrent operations should either be at distinct times or on distinct data. Atomicity is the abstraction that an operation takes effect at a single, discrete instant in time, with linearisability being a well known correctness condition which asserts that concurrent operations appear to behave atomically. Disjointness is the abstraction that operations act on distinct data resource, with concurrent separation logics enabling reasoning about threads that appear to operate independently on disjoint resources. We present TaDA, a program logic that combines the benefits of abstract atomicity and abstract disjointness. Our key contribution is the introduction of atomic triples, which offer an expressive approach to specifying program modules. By building up examples, we show that TaDA supports elegant modular reasoning in a way that was not previously possible.

Report

da Rocha Pinto P, Gardner P, Dinsdale-Young T, 2014, TaDA: A Logic for Time and Data Abstraction, European Conference on Object-Oriented Programming, ECOOP 2014, Publisher: Springer, Pages: 207-231, ISSN: 0302-9743

To avoid data races, concurrent operations should either be at distinct times or on distinct data. Atomicity is the abstraction that an operation takes effect at a single, discrete instant in time, with linearisability being a well-known correctness condition which asserts that concurrent operations appear to behave atomically. Disjointness is the abstraction that operations act on distinct data resource, with concurrent separation logics enabling reasoning about threads that appear to operate independently on disjoint resources. We present TaDA, a program logic that combines the benefits of abstract atomicity and abstract disjointness. Our key contribution is the introduction of atomic triples, which offer an expressive approach to specifying program modules. By building up examples, we show that TaDA supports elegant modular reasoning in a way that was not previously possible.

Conference paper

This data is extracted from the Web of Science and reproduced under a licence from Thomson Reuters. You may not copy or re-distribute this data in whole or in part without the written consent of the Science business of Thomson Reuters.

Request URL: http://wlsprd.imperial.ac.uk:80/respub/WEB-INF/jsp/search-html.jsp Request URI: /respub/WEB-INF/jsp/search-html.jsp Query String: respub-action=search.html&id=00306059&limit=30&person=true