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

81 results found

Dinsdale-Young T, Pinto PDR, Gardner P, 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

JOURNAL ARTICLE

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, Pinto PDR, Sutherland J, Gardner Pet al., 2018, A concurrent specification of POSIX file systems, ISSN: 1868-8969

© Gian Ntzik, Pedro da Rocha Pinto, Julian Sutherland, and Philippa Gardner. POSIX is a standard for operating systems, with a substantial part devoted to specifying filesystem 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 unsatisfactory: 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 T, da Rocha Pinto P, Andersen KJ, Birkedal Let al., 2017, CAPER: Automatic verification for fine-grained concurrency, Pages: 420-447, ISSN: 0302-9743

© Springer-Verlag GmbH Germany 2017. Recent program logics based on separation logic emphasise a modular approach to proving functional correctness for fine-grained concurrent programs. However, these logics have no automation support. In this paper, we present Caper, a prototype tool for automated reasoning in such a logic. Caper is based on symbolic execution, integrating reasoning about interference on shared data and about ghost resources that are used to mediate this interference. This enables Caper to verify the functional correctness of fine-grained concurrent algorithms.

CONFERENCE PAPER

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

Fragoso Santos J, Maksimović P, Naudžiūnienė D, Wood T, Gardner Pet al., 2017, JaVerT: JavaScript verification toolchain, Proceedings of the ACM on Programming Languages, Vol: 2, Pages: 1-33

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

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

Xiong S, da Rocha Pinto P, Ntzik G, Gardner Pet al., 2017, Abstract specifications for concurrent maps, Pages: 964-990, ISSN: 0302-9743

© Springer-Verlag GmbH Germany 2017. 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.

CONFERENCE PAPER

Pinto PDR, Dinsdale-Young T, Gardner P, Sutherland Jet al., 2016, Modular Termination Verification for Non-blocking Concurrency, 25th European Symposium on Programming (ESOP) Held as Part of the European Joint Conferences on Theory and Practice of Software (ETAPS), Publisher: SPRINGER-VERLAG BERLIN, Pages: 176-201, ISSN: 0302-9743

CONFERENCE PAPER

Raad A, Hobor A, Villard J, Gardner Pet al., 2016, Verifying concurrent graph algorithms, Pages: 314-334, ISSN: 0302-9743

© Springer International Publishing AG 2016. We show how to verify four challenging concurrent finegrained 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 (CoLoSL) 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, Santos JF, Gardner P, 2016, DOM: Specification and client reasoning, Pages: 401-422, ISSN: 0302-9743

© Springer International Publishing AG 2016. 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 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

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 (CAV), Publisher: SPRINGER-VERLAG BERLIN, Pages: 3-10, ISSN: 0302-9743

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

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

Ntzik G, Gardner P, 2015, Reasoning about the POSIX File System Local Update and Global Pathnames, ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), Publisher: ASSOC COMPUTING MACHINERY, Pages: 201-220, ISSN: 0362-1340

CONFERENCE PAPER

Ntzik G, Pinto PDR, Gardner P, 2015, Fault-Tolerant Resource Reasoning, 13th Asian Symposium on Programming Languages and Systems (APLAS), Publisher: SPRINGER INT PUBLISHING AG, Pages: 169-188, ISSN: 0302-9743

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

Pinto PDR, Dinsdale-Young T, Gardner P, 2015, Steps in Modular Specifications for Concurrent Modules, Publisher: ELSEVIER SCIENCE BV, Pages: 3-18, ISSN: 1571-0661

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

Gardner P, Ntzik G, Wright A, 2014, Local Reasoning for the POSIX File System, 23rd European Symposium on Programming (ESOP), Publisher: SPRINGER-VERLAG BERLIN, Pages: 169-188, ISSN: 0302-9743

CONFERENCE PAPER

Gardner P, Raad A, Wheelhouse M, Wright Aet al., 2014, Abstract local reasoning for concurrent libraries: Mind the gap, Pages: 147-166, ISSN: 1571-0661

© 2014 The Authors. We study abstract local reasoning for concurrent libraries. There are two main approaches: provide a specification of a library by abstracting from concrete reasoning about an implementation; or provide a direct abstract library specification, justified by refining to an implementation. Both approaches have a significant gap in their reasoning, due to a mismatch between the abstract connectivity of the abstract data structures and the concrete connectivity of the concrete heap representations. We demonstrate this gap using structural separation logic (SSL) for specifying a concurrent tree library and concurrent abstract predicates (CAP) for reasoning about a concrete tree implementation. The gap between the abstract and concrete connectivity emerges as a mismatch between the SSL tree predicates and CAP heap predicates. This gap is closed by an interface function I which links the abstract and concrete connectivity. In the accompanying technical report, we generalise our SSL reasoning and results to arbitrary concurrent data libraries.

CONFERENCE PAPER

Pinto PDR, Dinsdale-Young T, Gardner P, 2014, TaDA: A Logic for Time and Data Abstraction, 28th European Conference on Object-Oriented Programming (ECOOP), Publisher: SPRINGER-VERLAG BERLIN, Pages: 207-231, ISSN: 0302-9743

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

Dinsdale-Young T, Birkedal L, Gardner P, Parkinson M, Yang Het al., 2013, Views: Compositional Reasoning for Concurrent Programs, Publisher: ASSOC COMPUTING MACHINERY, Pages: 287-299, ISSN: 0362-1340

CONFERENCE PAPER

Felleisen M, Gardner P, 2013, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics): Preface, ISBN: 9783642370359

BOOK

Wickerson J, Dodds M, Parkinson MJ, 2013, Ribbon Proofs for Separation Logic., Publisher: Springer, Pages: 189-208

CONFERENCE PAPER

Wood T, 2013, A Program Logic for Verification of Security Properties of Secure ECMAScript Programs

We present an Operational Semantics of the Secure ECMAScript (SES) language. We extend Separation Logic with a backpointer operator to permit reasoning about reachability in the object graph whilst maintaining local reasoning. We define inference rules in the extended logic for SES. Finally, we prove the correctness of the Membrane design pattern.

THESIS DISSERTATION

Cardelli L, Gardner P, 2012, Processes in space, THEORETICAL COMPUTER SCIENCE, Vol: 431, Pages: 40-55, ISSN: 0304-3975

JOURNAL ARTICLE

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