Personal information

New Zealand

Biography

David graduated with a PhD from Imperial College London in 2005, and took up a lecturer position at Victoria University of Wellington, NZ. David’s PhD thesis was on efficient algorithms for pointer analysis of C, and his techniques have since been incorporated into GCC. His interests are in programming languages, compilers and static analysis. Since 2009, he has been developing the Whiley Programming Language which is designed specifically to simplify program verification. David has previously interned at Bell Labs, New Jersey, where he worked on compilers for FPGAs; and also at IBM Hursely, UK, where he worked with the AspectJ development team on profiling systems.

Activities

Employment (1)

Victoria University of Wellington: Wellington, NZ

2004-07-12 to present | Senior Lecturer (School of Engineering and Computer Science)
Employment
Source: Self-asserted source
David Pearce

Education and qualifications (2)

Imperial College of Science, Technology and Medicine: London, US

2000-09-01 to 2005-02-01 | PhD (Department of Computing)
Education
Source: Self-asserted source
David Pearce

Imperial College of Science, Technology and Medicine: London, GB

1996-09-01 to 2000-08-01 | MEng (Department of Computing)
Education
Source: Self-asserted source
David Pearce

Funding (1)

Attacking the grand challenge of a verifying compiler

2012 to 2015 | Contract
Marsden Fund (Wellington, NZ)
PROPOSAL_ID:

MFP-11-VUW-123

GRANT_NUMBER:

MFP-VUW1105

Source: check_circle
Royal Society Te Apārangi

Works (42)

Formal and Executable Semantics of the Ethereum Virtual Machine in Dafny

2023 | Book chapter
Contributors: Franck Cassez; Joanne Fuller; Milad K. Ghale; David J. Pearce; Horacio M. A. Quiles
Source: check_circle
Crossref

On the Termination of Borrow Checking in Featherweight Rust

2022 | Book chapter
Contributors: Étienne Payet; David J. Pearce; Fausto Spoto
Source: check_circle
Crossref

Verifying Whiley Programs with Boogie

Journal of Automated Reasoning
2022-11 | Journal article
Contributors: David J. Pearce; Mark Utting; Lindsay Groves
Source: check_circle
Crossref

A Lightweight Formalism for Reference Lifetimes and Borrowing in Rust

ACM Transactions on Programming Languages and Systems
2021-03-31 | Journal article
Contributors: David J. Pearce
Source: check_circle
Crossref

An Introduction to Software Verification with Whiley

2019 | Book chapter
Contributors: David J. Pearce; Mark Utting; Lindsay Groves
Source: check_circle
Crossref

Rewriting for Sound and Complete Union, Intersection and Negation Types

Proceedings of the Conference on `Generative Programming: Concepts & Experience (GPCE)
2017 | Conference paper
Source: Self-asserted source
David Pearce

A Mechanical Soundness Proof for Subtyping over Recursive Types

Proceedings of the Workshop on Formal Techniques for Java-like Programs (FTFJP)
2016 | Conference paper
Source: Self-asserted source
David Pearce

A space-efficient algorithm for finding strongly connected components

Information Processing Letters
2016 | Journal article
Source: Self-asserted source
David Pearce

Designing a Verifying Compiler: Lessons Learned from Developing Whiley

Science of Computer Programming
2015 | Journal article
Source: Self-asserted source
David Pearce

Integer Range Analysis for Whiley on Embedded Systems

Proceedings of the IEEE/IFIP Workshop on Software Technologies for Future Embedded and Ubiquitous Systems
2015 | Conference paper
Source: Self-asserted source
David Pearce

The Whiley Rewrite Language (WyRL)

Proceedings of the Conference on Software Language Engineering (SLE)
2015 | Conference paper
Source: Self-asserted source
David Pearce

Towards a Vertex and Edge Label Aware Force Directed Layout Algorithm

Proceedings of the Australasian conference on Computer Science (ACSC)
2014 | Conference paper
Source: Self-asserted source
David Pearce

A Calculus for Constraint-Based Flow Typing

Proceedings of the Workshop on Formal Techniques for Java-like Programs (FTFJP)
2013 | Conference paper
Source: Self-asserted source
David Pearce

Balloon Types for Safe Parallelisation over Arbitrary Object Graphs

Proceedings of the Workshop on Determinism and Correctness in Parallel Programming (WODET)
2013 | Conference paper
Source: Self-asserted source
David Pearce

OwnKit: Inferring Modularly Checkable Ownership Annotations for Java

Proceedings of the Australasian Software Engineering Conference (ASWEC)
2013 | Conference paper
Source: Self-asserted source
David Pearce

Reflections on Verifying Software with Whiley

Proceedings of the Workshop on Formal Techniques for Safety-Critical Systems (FTSCS)
2013 | Conference paper
Source: Self-asserted source
David Pearce

Sound and Complete Flow Typing with Unions, Intersections and Negations

Proceedings of the Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI)
2013 | Conference paper
Source: Self-asserted source
David Pearce

Whiley: a Platform for Research in Software Verification

Proceedings of the Conference on Software Language Engineering (SLE)
2013 | Conference paper
Source: Self-asserted source
David Pearce

Patterns as Objects in Grace

Proceedings of the Dynamic Languages Symposium (DLS)
2012 | Conference paper
Source: Self-asserted source
David Pearce

Profiling Object Initialization for Java

Proceedings of the Conference on Runtime Verification (RV)
2012 | Conference paper
Source: Self-asserted source
David Pearce

Formalisation and Implementation of an Algorithm for Bytecode Verification of @NonNull Types

Science of Computer Programming
2011 | Journal article
Source: Self-asserted source
David Pearce

Implementing a Language with Flow-Sensitive and Structural Typing on the JVM

Electronic Notes in Computer Science
2011 | Journal article
Source: Self-asserted source
David Pearce

JPure: a Modular Purity System for Java

Proceedings of the confererence on Compiler Construction (CC)
2011 | Conference paper
Source: Self-asserted source
David Pearce

Computing Tutte Polynomials

Transactions of Mathematical Software (TOMS)
2010 | Journal article
Source: Self-asserted source
David Pearce

Caching and Incrementalization for the Java Query Language.

Proceedings of the ACM conference on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA)
2008 | Conference paper
Source: Self-asserted source
David Pearce

Java Bytecode Verification for @NonNull Types

Proceedings of the confererence on Compiler Construction (CC)
2008 | Conference paper
Source: Self-asserted source
David Pearce

Efficient Field-sensitive pointer analysis for C

ACM Transactions on Programming Languages and Systems
2007 | Journal article
Source: Self-asserted source
David Pearce

Patterns of Aspect-Oriented Design

Proceedings of the European Conference on Pattern Languages of Programs (EuroPLOP)
2007 | Conference paper
Source: Self-asserted source
David Pearce

Profiling with AspectJ

Software: Pracice and Experience
2007 | Journal article
Source: Self-asserted source
David Pearce

Visualising the Tutte Polynomial Computation

Proceedings of the New Zealand Conference on Software Engineering (SIENZ)
2007 | Conference paper
Source: Self-asserted source
David Pearce

A dynamic topological sort algorithm for directed acyclic graphs

ACM Journal of Experimental Algorithms
2006 | Journal article
Source: Self-asserted source
David Pearce

Efficient Object Querying for Java

Proceedings of the European Confereince on Object-Oriented Programming (ECOOP)
2006 | Conference paper
Source: Self-asserted source
David Pearce

Relationship Aspect Patterns

Proceedings of the European Conference on Pattern Languages of Programs (EuroPLOP)
2006 | Conference paper
Source: Self-asserted source
David Pearce

Relationship Aspects

Proceedings of the Conference on Aspect Oriented Software Development (AOSD)
2006 | Conference paper
Source: Self-asserted source
David Pearce

Towards a Semiotics of Object- and Aspect-Oriented Design

Proceedings of the European Conference on Computing and Philosophy (ECAP)
2006 | Conference paper
Source: Self-asserted source
David Pearce

Some directed graph algorithms and their application to pointer analysis

2005 | Dissertation or Thesis
Source: Self-asserted source
David Pearce

A dynamic algorithm for topologically sorting directed acyclic graphs

Proceedings of the Workshop on Efficient and experimental Algorithms (WEA)
2004 | Conference paper
Source: Self-asserted source
David Pearce

Efficient Field-sensitive pointer analysis for C

Proceedings of the Workshop on Program Analysis for Software Tools and Engineering (PASTE)
2004 | Conference paper
Source: Self-asserted source
David Pearce

Online Cycle Detection and Difference Propagation: Applications to Pointer Analysis

Software Quality Journal
2004 | Journal article
Source: Self-asserted source
David Pearce

Design space exploration with A Stream Compiler

Proceedings of the IEEE Conference on Field-Programmable Technology (FPT'03)
2003 | Conference paper
Source: Self-asserted source
David Pearce

Online Cycle Detection and Difference Propagation for Pointer Analysis

Proceedings of the IEEE workshop on Source Code Analysis and Manipulation (SCAM)
2003 | Conference paper
Source: Self-asserted source
David Pearce

GILK: A Dynamic Instrumentation Tool for the Linux Kernel

Proceedings of the International TOOLS conference
2002 | Conference paper
Source: Self-asserted source
David Pearce