Search

Your search keyword '"O’Hearn, Peter W."' showing total 159 results
Start Over Author "O’Hearn, Peter W."
159 results on '"O’Hearn, Peter W."'

1. A True Positives Theorem for a Static Race Detector - Extended Version

Author

Gorogiannis, Nikos, O'Hearn, Peter W., and Sergey, Ilya

Subjects
Computer Science - Programming Languages
Abstract

RacerD is a static race detector that has been proven to be effective in engineering practice: it has seen thousands of data races fixed by developers before reaching production, and has supported the migration of Facebook's Android app rendering infrastructure from a single-threaded to a multi-threaded architecture. We prove a True Positives Theorem stating that, under certain assumptions, an idealized theoretical version of the analysis never reports a false positive. We also provide an empirical evaluation of an implementation of this analysis, versus the original RacerD. The theorem was motivated in the first case by the desire to understand the observation from production that RacerD was providing remarkably accurate signal to developers, and then the theorem guided further analyzer design decisions. Technically, our result can be seen as saying that the analysis computes an under-approximation of an over-approximation, which is the reverse of the more usual (over of under) situation in static analysis. Until now, static analyzers that are effective in practice but unsound have often been regarded as ad hoc; in contrast, we suggest that, in the future, theorems of this variety might be generally useful in understanding, justifying and designing effective static analyses for bug catching.

Published
2018
Full Text
View/download PDF

2. Verification Condition Generation and Variable Conditions in Smallfoot

Author

Berdine, Josh, Calcagno, Cristiano, and O'Hearn, Peter W.

Subjects
Computer Science - Logic in Computer Science, Computer Science - Programming Languages
Abstract

These notes are a companion to [1] which describe - the variable conditions that Smallfoot checks, - the analysis used to check them, - the algorithm used to compute a set of verification conditions corresponding to an annotated program, and - the treatment of concurrent resource initialization code.

Published
2012

4. The Complexity of Abduction for Separated Heap Abstractions

Author

Gorogiannis, Nikos, Kanovich, Max, O’Hearn, Peter W., 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 Yahav, Eran, editor

Published
2011
Full Text
View/download PDF

5. On Locality and the Exchange Law for Concurrent Processes

Author

Hoare, C. A. R., Hussain, Akbar, Möller, Bernhard, O’Hearn, Peter W., Petersen, Rasmus Lerchedahl, Struth, Georg, 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, Katoen, Joost-Pieter, editor, and König, Barbara, editor

Published
2011
Full Text
View/download PDF

6. Scalable Specification and Reasoning: Challenges for Program Logic

Author

O’Hearn, Peter W., 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, Meyer, Bertrand, editor, and Woodcock, Jim, editor

Published
2008
Full Text
View/download PDF

10. Introduction

Author

O’Hearn, Peter W., Tennent, Robert D., Book, Ronald V., O’Hearn, Peter W., editor, and Tennent, Robert D., editor

Published
1997
Full Text
View/download PDF

12. Footprint Analysis: A Shape Analysis That Discovers Preconditions

Author

Calcagno, Cristiano, Distefano, Dino, O’Hearn, Peter W., Yang, Hongseok, 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, Nielson, Hanne Riis, editor, and Filé, Gilberto, editor

Published
2007
Full Text
View/download PDF

13. Shape Analysis for Composite Data Structures

Author

Berdine, Josh, Calcagno, Cristiano, Cook, Byron, Distefano, Dino, O’Hearn, Peter W., Wies, Thomas, Yang, Hongseok, 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, Damm, Werner, editor, and Hermanns, Holger, editor

Published
2007
Full Text
View/download PDF

14. Beyond Reachability: Shape Abstraction in the Presence of Pointer Arithmetic

Author

Calcagno, Cristiano, Distefano, Dino, O’Hearn, Peter W., Yang, Hongseok, 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 Yi, Kwangkeun, editor

Published
2006
Full Text
View/download PDF

15. Automatic Termination Proofs for Programs with Shape-Shifting Heaps

Author

Berdine, Josh, Cook, Byron, Distefano, Dino, O’Hearn, Peter W., 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, Ball, Thomas, editor, and Jones, Robert B., editor

Published
2006
Full Text
View/download PDF

16. Smallfoot: Modular Automatic Assertion Checking with Separation Logic

Author

Berdine, Josh, Calcagno, Cristiano, O’Hearn, Peter W., 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, de Boer, Frank S., editor, Bonsangue, Marcello M., editor, Graf, Susanne, editor, and de Roever, Willem-Paul, editor

Published
2006
Full Text
View/download PDF

17. A Local Shape Analysis Based on Separation Logic

Author

Distefano, Dino, O’Hearn, Peter W., Yang, Hongseok, 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, Dough, Series editor, Vardi, Moshe Y., Series editor, Weikum, Gerhard, Series editor, Hermanns, Holger, editor, and Palsberg, Jens, editor

Published
2006
Full Text
View/download PDF

18. Symbolic Execution with Separation Logic

Author

Berdine, Josh, Calcagno, Cristiano, O’Hearn, Peter W., 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 Yi, Kwangkeun, editor

Published
2005
Full Text
View/download PDF

19. A Decidable Fragment of Separation Logic

Author

Berdine, Josh, Calcagno, Cristiano, O’Hearn, Peter W., 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, Lodaya, Kamal, editor, and Mahajan, Meena, editor

Published
2005
Full Text
View/download PDF

20. Resources, Concurrency and Local Reasoning

Author

O’Hearn, Peter W., 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, Dough, Series editor, Vardi, Moshe Y., Series editor, Weikum, Gerhard, Series editor, Gardner, Philippa, editor, and Yoshida, Nobuko, editor

Published
2004
Full Text
View/download PDF

21. On Garbage and Program Logic

Author

Calcagno, Cristiano, O’Hearn, Peter W., Goos, Gerhard, editor, Hartmanis, Juris, editor, van Leeuwen, Jan, editor, Honsell, Furio, editor, and Miculan, Marino, editor

Published
2001
Full Text
View/download PDF

29. Scaling Static Analyses at Facebook.

Author

DISTEFANO, DINO, FÄHNDRICH, MANUEL, LOGOZZO, FRANCESCO, and O'HEARN, PETER W.

Subjects
SOURCE code, COMPUTER software development, COMPUTER software quality control, DEBUGGING
Abstract

The article discusses the use of static analysis techniques by the social media firm Facebook Inc. Topics include the use of deep reasoning in relation to source code, the importance of catching software bugs in the use of static analysis, and the use of the tool Infer in relation to continuous software development practices used by Facebook.

Published
2019
Full Text
View/download PDF

30. Algebra, Logic, Locality, Concurrency

Author

O’Hearn, Peter W., 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, Jouannaud, Jean-Pierre, editor, and Shao, Zhong, editor

Published
2011
Full Text
View/download PDF

31. Abductive, Inductive and Deductive Reasoning about Resources

Author

O’Hearn, Peter W., 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, Dawar, Anuj, editor, and Veith, Helmut, editor

Published
2010
Full Text
View/download PDF

32. Separation and information hiding

Author

O'Hearn, Peter W., Yang, Hongseok, and Reynolds, John C.

Subjects
Programming language, Programming languages -- Evaluation
Abstract

We investigate proof rules for information hiding, using the formalism of separation logic. In essence, we use the separating conjunction to partition the internal resources of a module from those accessed by the module's clients. The use of a logical connective gives rise to a form of dynamic partitioning, where we track the transfer of ownership of portions of heap storage between program components. It also enables us to enforce separation in the presence of mutable data structures with embedded addresses that may be aliased. Categories and Subject Descriptors: D.2.4 [Software Engineering]: Software Program Verification--Class invariants; D.3.3 [Programming Languages]: Language Constructs and Features-Modules, packages General Terms: Languages, Theory, Verification Additional Key Words and Phrases: Separation logic, modularity, resource protection DOI = 10.1145/1498926.1498929 http://doi.acm.org/10.1145/1498926.1498929

Published
2009

40. Reasoning about Programs Using a Scientific Method

Author

O’Hearn, Peter W., 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, Qin, Shengchao, editor, and Qiu, Zongyan, editor

Published
2011
Full Text
View/download PDF

Catalog

Books, media, physical & digital resources
See catalog results