Cormac Flanagan

University of California, Santa Cruz

Author Statistics

Papers

Citation

H-Index

i-10 index

Research Trends

Author Order

Document Type

Co-Authors

Stephen N. Freund

Williams College

Thomas H. Austin

San Jose State University

Mooly Sagiv

Tel Aviv University

Dustin Rhodes

University of California, Santa Cruz

Thomas Schmitz

University of California, Santa Cruz

Maximilian Algehed

Chalmers University of Technology

Kalev Alpernas

Tel Aviv University

Sadjad Fouladi

Microsoft Research (United Kingdom)

Barbara König

University of Duisburg-Essen

James B. Saxe

Hewlett-Packard (United States)

Cooperative Institutions

University of California, Santa Cruz

Chalmers University of Technology

Tel Aviv University

Cornell University

IBM (United States)

Google (United States)

Microsoft Research (United Kingdom)

Alcatel Lucent (Germany)

Stanford University

Institut national de recherche en informatique et en automatique

Author Statistics

Papers

Citation

H-Index

i-10 index

Research Field

Dynamic partial-order reduction for model checking software

Cormac Flanagan Patrice Godefroid

We present a new approach to partial-order reduction for model checking software. This approach is based on initially exploring an arbitrary interleaving of the various concurrent processes/threads, and dynamically tracking interactions between these to identify backtracking points where alternative paths in the state space need to be explored. We present examples of multi-threaded programs where our new dynamic partial-order reduction technique significantly reduces the search space, even though traditional partial-order algorithms are helpless.

Partial order reduction

Backtracking

Interleaving

Partial evaluation

10.1145/1040305.1040315

Cite

Citations (639)

Practices of PLDI

ACM SIGPLAN Notices (2014)

Hans J. Boehm Jack W. Davidson Kathleen Fisher Cormac Flanagan Jeremy Gibbons

column Practices of PLDI Authors: Hans Boehm View Profile , Jack Davidson View Profile , Kathleen Fisher View Profile , Cormac Flanagan View Profile , Jeremy Gibbons View Profile , Mary Hall View Profile , Graham Hutton View Profile , David Padua View Profile , Frank Tip View Profile , Jan Vitek View Profile , Philip Wadler View Profile Authors Info & Claims ACM SIGPLAN NoticesVolume 49Issue 4SApril 2014 pp 33–38https://doi.org/10.1145/2641638.2641649Published:01 July 2014Publication History 0citation30DownloadsMetricsTotal Citations0Total Downloads30Last 12 Months1Last 6 weeks1 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteGet Access

10.1145/2641638.2641649

Cite

Citations (0)

CSF 2020 TOC

David Basin Lara Schmid Véronique Cortier Vincenzo Iovino Alfredo Rial

10.1109/csf49147.2020.00004

Cite

Citations (0)

Session details: Types

Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (2005)

Cormac Flanagan

No abstract available.

10.1145/3249491

Cite

Citations (0)

Type-based race detection for Java

Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (2000)

Cormac Flanagan Stephen N. Freund

This paper presents a static race detection analysis for multithreaded Java programs. Our analysis is based on a formal type system that is capable of capturing many common synchronization patterns. These patterns include classes with internal synchronization, classes thatrequire client-side synchronization, and thread-local classes. Experience checking over 40,000 lines of Java code with the type system demonstrates that it is an effective approach for eliminating races conditions. On large examples, fewer than 20 additional type annotations per 1000 lines of code were required by the type checker, and we found a number of races in the standard Java libraries and other test programs.

Generics in Java

Java Modeling Language

10.1145/349299.349328

Cite

Citations (456)

RedCard: Redundant Check Elimination For Dynamic Race Detectors Technical Report UCSC-SOE-13-05

Cormac Flanagan Stephen N. Freund

Precise dynamic race detectors report an error if and only if an observed program trace exhibits a data race. They must typically check for races on all memory accesses to ensure that they catch all races and generate no spurious warnings. However, a race check for a particular memory access is guaranteed to be redundant if the accessing thread has already accessed that location within the same release-free span. A release-free span is any sequence of instructions containing no lock releases or other \release-like synchronization operations, such as notify or fork. We present a static analysis to identify redundant race checks by reason- ing about memory accesses within release-free spans. In contrast to prior whole program analyses for identifying accesses that are always race-free, our redundant check analysis is span-local and can also be made method- local without any major loss in eectiveness. RedCard, our prototype implementation for the Java language, enables dynamic race detectors to reduce the number of run-time checks by close to 40% with no loss in precision. We also present a complementary shadow proxy analysis for identify- ing when multiple memory locations can be treated as a single location by a dynamic race detector, again with no loss in precision. Combined, our analyses reduce the number of memory accesses requiring checks by roughly 50%.

Spurious relationship

Vector clock

Source

Cite

Citations (1)

Detecting inconsistencies via universal reachability analysis

Aaron Tomb Cormac Flanagan

Recent research has suggested that a large class of software bugs fall into the category of inconsistencies, or cases where two pieces of program code make incompatible assumptions. Existing approaches to inconsistency detection have used intentionally unsound techniques aimed at bug-finding rather than verification. We describe an inconsistency detection analysis that extends previous work and is based on the foundation of the weakest precondition calculus. On a closed program, this analysis can serve as a full verification technique, while in cases where some code is unknown, a theorem prover is incomplete, or specifications are incomplete, it can serve as bug finding technique with a low false-positive rate.

Precondition

Code (set theory)

Software bug

Predicate transformer semantics

Software verification

10.1145/2338965.2336788

Cite

Citations (23)

Proceedings of the 5th ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering

Workshop on Program Analysis For Software Tools and Engineering (2004)

Cormac Flanagan Andreas Zeller

This volume contains the papers presented at the Fifth ACM SIGPLAN/SIGSOFT Workshop on Program Analysis for Software Tools and Engineering (PASTE 2004), co-located with the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), on June 7-8, 2004 in Washington, DC.Sophisticated program analysis is more and more used in sophisticated development and maintenance tools. Coming from optimizing compilers, program analysis has found several new applications in understanding, debugging, testing, and reverse engineering programs. In addition, new program analysis techniques have been developed specifically for these tasks. PASTE 2004 provides a forum for bringing together members of the program analysis, software tools, and software engineering communities to focus on program analysis techniques in software tools.Continuing the tradition of earlier PASTE workshops, the program committee aimed at a true workshop format, with a combination of technical paper presentations, three invited talks (by Gary Leavens, Michael Ernst, and Patrice Godefroid), and ample time for lively ad hoc presentations and discussions.A record number of 37 papers were submitted, out of which the program committee selected 10 for presentation. Each paper was reviewed by at least three committee members. Special thanks go to Colin Blundell, Michael Hind, Manos Renieris, and Tao Xie for their assistance in evaluating the submissions.

Presentation (obstetrics)

Program comprehension

Reverse engineering

Source

Cite

Citations (0)

Permissive dynamic information flow analysis

Thomas H. Austin Cormac Flanagan

A key challenge in dynamic information flow analysis is handling implicit flows, where code conditional on a private variable updates a public variable x. The naive approach of upgrading x to private results in x being partially leaked, where its value contains private data but its label might remain public on an alternative execution (where the conditional update was not performed). Prior work proposed the no-sensitive-upgrade check, which handles implicit flows by prohibiting partially leaked data, but attempts to update a public variable from a private context causes execution to get stuck.

Private information retrieval

Information flow

Code (set theory)

Upgrade

Value (mathematics)

10.1145/1814217.1814220

Cite

Citations (135)

VIEWS OF 3 JUNIOR STUDENTS

Nursing Forum (1969)

James F. Meaney Cormac Flanagan Keith A. Horvath

10.1111/j.1744-6198.1969.tb00424.x

Cite

Citations (1)