Search

Your search keyword '"Pearce, David J."' showing total 168 results
Start Over Author "Pearce, David J."
168 results on '"Pearce, David J."'

1. Formal and Executable Semantics of the Ethereum Virtual Machine in Dafny

Author

Cassez, Franck, Fuller, Joanne, Ghale, Milad K., Pearce, David J., and Quiles, Horacio M. A.

Subjects
Computer Science - Logic in Computer Science
Abstract

The Ethereum protocol implements a replicated state machine. The network participants keep track of the system state by: 1) agreeing on the sequence of transactions to be processed and 2) computing the state transitions that correspond to the sequence of transactions. Ethereum transactions are programs, called smart contracts, and computing a state transition requires executing some code. The Ethereum Virtual Machine (EVM) provides this capability and can execute programs written in EVM bytecode. We present a formal and executable semantics of the EVM written in the verification-friendly language Dafny: it provides (i) a readable, formal and verified specification of the semantics of the EVM; (ii) a framework to formally reason about bytecode.

Published
2023

2. Putting the Semantics into Semantic Versioning

Author

Lam, Patrick, Dietrich, Jens, and Pearce, David J.

Subjects
Computer Science - Software Engineering, D.2.4, D.2.7, D.2.9, D.2.12, D.2.13
Abstract

The long-standing aspiration for software reuse has made astonishing strides in the past few years. Many modern software development ecosystems now come with rich sets of publicly-available components contributed by the community. Downstream developers can leverage these upstream components, boosting their productivity. However, components evolve at their own pace. This imposes obligations on and yields benefits for downstream developers, especially since changes can be breaking, requiring additional downstream work to adapt to. Upgrading too late leaves downstream vulnerable to security issues and missing out on useful improvements; upgrading too early results in excess work. Semantic versioning has been proposed as an elegant mechanism to communicate levels of compatibility, enabling downstream developers to automate dependency upgrades. While it is questionable whether a version number can adequately characterize version compatibility in general, we argue that developers would greatly benefit from tools such as semantic version calculators to help them upgrade safely. The time is now for the research community to develop such tools: large component ecosystems exist and are accessible, component interactions have become observable through automated builds, and recent advances in program analysis make the development of relevant tools feasible. In particular, contracts (both traditional and lightweight) are a promising input to semantic versioning calculators, which can suggest whether an upgrade is likely to be safe., Comment: to be published as Onward! Essays 2020

Published
2020
Full Text
View/download PDF

5. On the Termination of Borrow Checking in Featherweight Rust

Author

Payet, Étienne, Pearce, David J., Spoto, Fausto, Goos, Gerhard, Founding Editor, Hartmanis, Juris, Founding Editor, Bertino, Elisa, Editorial Board Member, Gao, Wen, Editorial Board Member, Steffen, Bernhard, Editorial Board Member, Yung, Moti, Editorial Board Member, Deshmukh, Jyotirmoy V., editor, Havelund, Klaus, editor, and Perez, Ivan, editor

Published
2022
Full Text
View/download PDF

6. An Introduction to Software Verification with Whiley

Author

Pearce, David J., Utting, Mark, Groves, Lindsay, Hutchison, David, Editorial Board Member, Kanade, Takeo, Editorial Board Member, Kittler, Josef, Editorial Board Member, Kleinberg, Jon M., Editorial Board Member, Mattern, Friedemann, Editorial Board Member, Mitchell, John C., Editorial Board Member, Naor, Moni, Editorial Board Member, Pandu Rangan, C., Editorial Board Member, Steffen, Bernhard, Editorial Board Member, Terzopoulos, Demetri, Editorial Board Member, Tygar, Doug, Editorial Board Member, Goos, Gerhard, Founding Editor, Hartmanis, Juris, Founding Editor, Bowen, Jonathan P., editor, Liu, Zhiming, editor, and Zhang, Zili, editor

Published
2019
Full Text
View/download PDF

8. Making Whiley Boogie!

Author

Utting, Mark, Pearce, David J., Groves, Lindsay, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Weikum, Gerhard, Series editor, Polikarpova, Nadia, editor, and Schneider, Steve, editor

Published
2017
Full Text
View/download PDF

10. On Leveraging Tests to Infer Nullable Annotations

Author

Jens Dietrich and David J. Pearce and Mahin Chandramohan, Dietrich, Jens, Pearce, David J., Chandramohan, Mahin, Jens Dietrich and David J. Pearce and Mahin Chandramohan, Dietrich, Jens, Pearce, David J., and Chandramohan, Mahin

Abstract

Issues related to the dereferencing of null pointers are a pervasive and widely studied problem, and numerous static analyses have been proposed for this purpose. These are typically based on dataflow analysis, and take advantage of annotations indicating whether a type is nullable or not. The presence of such annotations can significantly improve the accuracy of null checkers. However, most code found in the wild is not annotated, and tools must fall back on default assumptions, leading to both false positives and false negatives. Manually annotating code is a laborious task and requires deep knowledge of how a program interacts with clients and components. We propose to infer nullable annotations from an analysis of existing test cases. For this purpose, we execute instrumented tests and capture nullable API interactions. Those recorded interactions are then refined (santitised and propagated) in order to improve their precision and recall. We evaluate our approach on seven projects from the spring ecosystems and two google projects which have been extensively manually annotated with thousands of @Nullable annotations. We find that our approach has a high precision, and can find around half of the existing @Nullable annotations. This suggests that the method proposed is useful to mechanise a significant part of the very labour-intensive annotation task.

Published
2023
Full Text
View/download PDF

12. On Leveraging Tests to Infer Nullable Annotations

Author

Dietrich, Jens, Pearce, David J., and Chandramohan, Mahin

Subjects
Software and its engineering → Software reliability, program analysis, null safety, Software and its engineering → Dynamic analysis, null analysis, Software and its engineering → Software defect analysis, testing
Abstract

Issues related to the dereferencing of null pointers are a pervasive and widely studied problem, and numerous static analyses have been proposed for this purpose. These are typically based on dataflow analysis, and take advantage of annotations indicating whether a type is nullable or not. The presence of such annotations can significantly improve the accuracy of null checkers. However, most code found in the wild is not annotated, and tools must fall back on default assumptions, leading to both false positives and false negatives. Manually annotating code is a laborious task and requires deep knowledge of how a program interacts with clients and components. We propose to infer nullable annotations from an analysis of existing test cases. For this purpose, we execute instrumented tests and capture nullable API interactions. Those recorded interactions are then refined (santitised and propagated) in order to improve their precision and recall. We evaluate our approach on seven projects from the spring ecosystems and two google projects which have been extensively manually annotated with thousands of @Nullable annotations. We find that our approach has a high precision, and can find around half of the existing @Nullable annotations. This suggests that the method proposed is useful to mechanise a significant part of the very labour-intensive annotation task., LIPIcs, Vol. 263, 37th European Conference on Object-Oriented Programming (ECOOP 2023), pages 10:1-10:25

Published
2023
Full Text
View/download PDF

15. Sound and Complete Flow Typing with Unions, Intersections and Negations

Author

Pearce, David J., Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Giacobazzi, Roberto, editor, Berdine, Josh, editor, and Mastroeni, Isabella, editor

Published
2013
Full Text
View/download PDF

16. Profiling Field Initialisation in Java

Author

Nelson, Stephen, Pearce, David J., Noble, James, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Qadeer, Shaz, editor, and Tasiran, Serdar, editor

Published
2013
Full Text
View/download PDF

17. Whiley: A Platform for Research in Software Verification

Author

Pearce, David J., Groves, Lindsay, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Erwig, Martin, editor, Paige, Richard F., editor, and Van Wyk, Eric, editor

Published
2013
Full Text
View/download PDF

18. JPure: A Modular Purity System for Java

Author

Pearce, David J., Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Nierstrasz, Oscar, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Sudan, Madhu, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Vardi, Moshe Y., Series editor, Weikum, Gerhard, Series editor, and Knoop, Jens, editor

Published
2011
Full Text
View/download PDF

19. Understanding the Impact of Collection Contracts on Design

Author

Nelson, Stephen, Pearce, David J., Noble, James, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, and Vitek, Jan, editor

Published
2010
Full Text
View/download PDF

20. Java Bytecode Verification for @NonNull Types

Author

Male, Chris, Pearce, David J., Potanin, Alex, Dymnikov, Constantine, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, and Hendren, Laurie, editor

Published
2008
Full Text
View/download PDF

21. Efficient Object Querying for Java

Author

Willis, Darren, Pearce, David J., Noble, James, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Dough, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, and Thomas, Dave, editor

Published
2006
Full Text
View/download PDF

22. Automating Optimized Table-with-Polynomial Function Evaluation for FPGAs

Author

Lee, Dong-U, Mencer, Oskar, Pearce, David J., Luk, Wayne, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Dough, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Becker, Jürgen, editor, Platzner, Marco, editor, and Vernalde, Serge, editor

Published
2004
Full Text
View/download PDF

23. A Dynamic Algorithm for Topologically Sorting Directed Acyclic Graphs

Author

Pearce, David J., Kelly, Paul H. J., Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Dough, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Ribeiro, Celso C., editor, and Martins, Simone L., editor

Published
2004
Full Text
View/download PDF

30. Efficient field-sensitive pointer analysis of C

Author

Pearce, David J., Kelly, Paul H.J., and Hankin, Chris

Subjects
Algorithm, Programming language, Algorithms -- Analysis, Programming languages -- Analysis
Abstract

The subject of this article is flow- and context-insensitive pointer analysis. We present a novel approach for precisely modelling struct variables and indirect function calls. Our method emphasises efficiency and simplicity and is based on a simple language of set constraints. We obtain an O(v.sup.4) bound on the time needed to solve a set of constraints from this language, where v is the number of constraint variables. This gives, for the first time, some insight into the hardness of performing fieldsensitive pointer analysis of C. Furthermore, we experimentally evaluate the time versus precision trade-off for our method by comparing against the field-insensitive equivalent. Our benchmark suite consists of 11 common C programs ranging in size from 15,000 to 200,000 lines of code. Our results indicate the field-sensitive analysis is more expensive to compute, but yields significantly better precision. In addition, our technique has been integrated into the latest release (version 4.1) of the GNU Compiler GCC. Finally, we identify several previously unknown issues with an alternative and less precise approach to modelling struct variables, known as field-based analysis. Categories and Subject Descriptors: F.3.2 [Logics a Meanings of Programs]: Semantics of Programm in Languages--program analysis General Terms: Algorithms, Theory, Languages, Verification Additional Key Words and Phrases: Set-constraints, pointer analysis ACM Reference Format: Pearce, D. J., Kelly, P. H. J., and Hankin, C. 2007. Efficient field-sensitive pointer analysis of C. ACM Trans. Program. Lang. Syst. 30, 1, Article 4 (November 2007), 42 pages. DOI = 10.1145/1290520.1290524 http://doi.acm.org/10.1145/1290520.1290524

Published
2008

42. Contracts in the Wild: A Study of Java Programs

Author

Dietrich, Jens, Pearce, David J., Jezek, Kamil, and Brada, Premek

Subjects
000 Computer science, knowledge, general works, Computer Science, 0202 electrical engineering, electronic engineering, information engineering, 020207 software engineering, 020201 artificial intelligence & image processing, 02 engineering and technology
Published
2017
Full Text
View/download PDF

43. On declarative rewriting for sound and complete union, intersection and negation types

Author

Pearce, David J.

Abstract

•We detail an implementation using declarative rewrite rules of a subtype operator involving union, intersection and negation types.•We report experiment results over a range of range of benchmarks comparing this with an ad-hoc existing implementation.•We detail the implementation of our system in the Rascal meta-programming framework.•We discuss an approach to supporting recursive types via coinductive rewriting.

Published
2024
Full Text
View/download PDF

45. Contracts in the Wild: A Study of Java Programs (Artifact)

Author

http://dx.doi.org/10.4230/LIPIcs.ECOOP.2017.9, Dietrich, Jens, Pearce, David J., Jezek, Kamil, Brada, Premek, http://dx.doi.org/10.4230/LIPIcs.ECOOP.2017.9, Dietrich, Jens, Pearce, David J., Jezek, Kamil, and Brada, Premek

Abstract

This artefact contains a dataset of open-source programs obtained from the Maven Central Repository and scripts that first extract contracts from these programs and then perform several analyses on the contracts extracted. The extraction and analysis is fully automated and directly produces the tables presented in the accompanying paper. The results show how contracts are used in real-world program, and how their usage changes between versions and within inheritance hierarchies.

Published
2017
Full Text
View/download PDF

46. Contracts in the Wild: A Study of Java Programs

Author

Jens Dietrich and David J. Pearce and Kamil Jezek and Premek Brada, Dietrich, Jens, Pearce, David J., Jezek, Kamil, Brada, Premek, Jens Dietrich and David J. Pearce and Kamil Jezek and Premek Brada, Dietrich, Jens, Pearce, David J., Jezek, Kamil, and Brada, Premek

Abstract

The use of formal contracts has long been advocated as an approach to develop programs that are provably correct. However, the reality is that adoption of contracts has been slow in practice. Despite this, the adoption of lightweight contracts — typically utilising runtime checking — has progressed. In the case of Java, built-in features of the language (e.g. assertions and exceptions) can be used for this. Furthermore, a number of libraries which facilitate contract checking have arisen. In this paper, we catalogue 25 techniques and tools for lightweight contract checking in Java, and present the results of an empirical study looking at a dataset extracted from the 200 most popular projects found on Maven Central, constituting roughly 351,034 KLOC. We examine (1) the extent to which contracts are used and (2) what kind of contracts are used. We then investigate how contracts are used to safeguard code, and study problems in the context of two types of substitutability that can be guarded by contracts: (3) unsafe evolution of APIs that may break client programs and (4) violations of Liskovs Substitution Principle (LSP) when methods are overridden. We find that: (1) a wide range of techniques and constructs are used to represent contracts, and often the same program uses different techniques at the same time; (2) overall, contracts are used less than expected, with significant differences between programs; (3) projects that use contracts continue to do so, and expand the use of contracts as they grow and evolve; and, (4) there are cases where the use of contracts points to unsafe subtyping (violations of Liskov's Substitution Principle) and unsafe evolution.

Published
2017
Full Text
View/download PDF

47. Contracts in the Wild: A Study of Java Programs (Artifact)

Author

Jens Dietrich and David J. Pearce and Kamil Jezek and Premek Brada, Dietrich, Jens, Pearce, David J., Jezek, Kamil, Brada, Premek, Jens Dietrich and David J. Pearce and Kamil Jezek and Premek Brada, Dietrich, Jens, Pearce, David J., Jezek, Kamil, and Brada, Premek

Abstract

This artefact contains a dataset of open-source programs obtained from the Maven Central Repository and scripts that first extract contracts from these programs and then perform several analyses on the contracts extracted. The extraction and analysis is fully automated and directly produces the tables presented in the accompanying paper. The results show how contracts are used in real-world program, and how their usage changes between versions and within inheritance hierarchies.

Published
2017
Full Text
View/download PDF

48. A Review of the Tools Used for Marine Monitoring in the UK: Combining Historic and Contemporary Methods with Modeling and Socioeconomics to Fulfill Legislative Needs and Scientific Ambitions

Author

Bean, Tim P., primary, Greenwood, Naomi, additional, Beckett, Rachel, additional, Biermann, Lauren, additional, Bignell, John P., additional, Brant, Jan L., additional, Copp, Gordon H., additional, Devlin, Michelle J., additional, Dye, Stephen, additional, Feist, Stephen W., additional, Fernand, Liam, additional, Foden, Dean, additional, Hyder, Kieran, additional, Jenkins, Chris M., additional, van der Kooij, Jeroen, additional, Kröger, Silke, additional, Kupschus, Sven, additional, Leech, Clare, additional, Leonard, Kinson S., additional, Lynam, Christopher P., additional, Lyons, Brett P., additional, Maes, Thomas, additional, Nicolaus, E. E. Manuel, additional, Malcolm, Stephen J., additional, McIlwaine, Paul, additional, Merchant, Nathan D., additional, Paltriguera, Lucille, additional, Pearce, David J., additional, Pitois, Sophie G., additional, Stebbing, Paul D., additional, Townhill, Bryony, additional, Ware, Suzanne, additional, Williams, Oliver, additional, and Righton, David, additional

Published
2017
Full Text
View/download PDF

Catalog

Books, media, physical & digital resources
See catalog results