mugshot

Cormac Flanagan
Professor

Computer Science Department 
Baskin School of Engineering
University of California Santa Cruz

Email:      cormac at ucsc.edu  
Phone:     831-459-5375    (fax)  831-459-4829
Office:     Engineering 2 Building, room 367 (directions
Address:  1156 High Street MS: SOE3, Santa Cruz CA 95064
Misc:
       Vitae, Google Scholar, DBLP, ACM DL, MS academic search

---

Service Steering Committee Chair, ACM Conference on Programming Language Design and Implementation (PLDI)

Associate Editor, ACM Transactions on Programming Languages and Systems (TOPLAS)

Program Committee Chair, Programming Language Design and Implementation (PLDI)

Co-Chair,  Tools and Algorithms for Construction and Analysis of Systems (TACAS)

Steering Committee Co-Chair, ACM SIGPLAN Workshops on Programming Languages meets Program Verification

Co-Chair,  ACM SIGPLAN Workshop on Programming Languages meets Program Verification

Member of UCSC Senate Committee on Planning and Budget

Past Member of UCSC Senate Committee on Educational Policy

---

Students Dustin Rhodes

Christopher Schuster

Thomas Schmitz 

Daniel Fava

Sohum Banerjea

---

Alumni Tim Disney (now at Shape Security)

Kenn Knowles (now at Google)

Tom Austin (now a faculty member at San Jose State University)

Jaeheon Yi (now at Google)

Aaron Tomb (now at Galois Connections)

---

Awards UCSC Excellence in Teaching Award (2015)

PLDI Distinguished Artifact Award for "BigFoot: Static Check Placement for Dynamic Race Detection" (2017)

ECOOP Best Paper Award for "RedCard: Redundant Check Elimination for Dynamic Race Detectors" (2013)

Most Influential PLDI Paper Award for "Extended Static Checking for Java" (2012)

Alfred P. Sloan Foundation Fellowship

ISSTA Distinguished Paper Award



Edited
Conference Proceedings

ACM SIGPLAN Conference on Programming Language Design and Implementation 2013
Tools and Algorithms for Construction and Analysis of Systems (TACAS) 2012
ACM SIGPLAN Workshop on Programming Languages meets Program Verification 2010
ACM SIGPLAN Workshop on Program Analysis for Software Tools and Engineering 2004



Publications
(and older publications)



Multiple Facets for Dynamic Information Flow with Exceptions (TOPLAS May 2017)
BigFoot: Static Check Placement for Dynamic Race Detection (PLDI'17, Distinguished Artifact Award)
Correctness of Partial Escape Analysis for Multithreaded Optimization (FTFJP'17)
Precise, Dynamic Information Flow for Database-Backed Applications (PLDI'16)
Macrofication: Refactoring by Reverse Macro Expansion (ESOP'16)
Faceted Dynamic Information Flow via Control and Data Monads (POST'16)
Reactive Programming with Reactive Variables (CROW'16)
Array Shadow State Compression for Precise Dynamic Race Detection (ASE'15)
Live Programming for Event-Based Languages (REBLS'15)
Contracts for Async Patterns in JavaScript (STOP'15)
Game Semantics for Type Soundness (LICS'15)
A Light-Weight Effect System for JavaScript (STOP'15)
Traveling Through Time And Code: Omniscient Debugging And Beyond (UCSC Technical Report 2014)
Dynamic Detection of Object Capability Violations Through Model Checking (DLS'14)
Typed Faceted Values for Secure Information Flow in Haskell (Technical report UCSC-SOE-14-07)
Sweeten Your JavaScript: Hygienic Macros for ES5 (DLS'14)
RedCard: Redundant Check Elimination for Dynamic Race Detectors (ECOOP'13, Best Paper Award, technical report)
Faceted Execution of Policy-Agnostic Programs (PLAS'13, revision of original paper)
A Functional View of Imperative Information Flow (APLAS'12)
Cooperative Types for Controlling Thread Interference in Java (ISSTA'12)
Detecting Inconsistencies via Universal Reachability Analysis (ISSTA'12)
Multiple Facets for Dynamic Information Flow (POPL '12)
Sound Predictive Race Detection in Polynomial Time (POPL '12)
Virtual Values for Language Extension (OOPSLA'11)
Cooperative Concurrency for a Multicore World (RV'11 invited talk, slides)
Types for Precise Thread Interference (Technical report UCSC-SOE-11-22)
Temporal Higher-Order Contracts (ICFP'11)
Gradual Information Flow Typing (STOP'11)
Correct Blame for Contracts: No More Scapegoating (POPL '11)
Cooperative Reasoning for Preemptive Execution (PPOPP '11)
Adversarial Memory for Detecting Destructive Races (PLDI '10)
The RoadRunner Dynamic Analysis Framework for Concurrent Programs (PASTE '10)
Permissive Dynamic Information Flow Analysis (PLAS '10)
Effects for Cooperable and Serializable Threads (TLDI '10)
FastTrack: Efficient and Precise Dynamic Race Detection (PLDI '09)   A revised version of this paper appeared in CACM research highlights, Nov. 2010.
Hybrid Type Checking (TOPLAS'10)
SideTrack: Generalizing Dynamic Atomicity Analysis (PADTAD '09)
Efficient Purely-Dynamic Information Flow Analysis (PLAS '09)
Compositional and Decidable Checking for Dependent Contract Types (PLPV'09)
SingleTrack: A Dynamic Determinism Checker for Multithreaded Programs (ESOP '09)
Types for Atomicity: Static Checking and Inference for Java (TOPLAS '08, appendix
Velodrome: A Sound and Complete Dynamic Atomicity Checker for Multithreaded Programs (PLDI '08)
Proving correctness of a dynamic atomicity analysis in Coq (Workshop on Mechanizing Metatheory '08)
Atomizer: A Dynamic Atomicity Checker for Multithreaded Programs (Science of Computer Programming '08)

Type Inference Against Races (Science of Computer Programming '07)
Cartesian Partial-Order Reduction (SPIN '07)
Status Report: Specifying JavaScript with ML (ML’07)


Space Efficient Gradual Typing (TFP’07)

Unifying Hybrid Types and Contracts (TFP’07)

Type Reconstruction for General Refinement Types (ESOP’07, extended paper)

Sage: Unified Hybrid Checking for First-Class Types, General Refinement Types, and Dynamic (Scheme Workshop '06, extended technical report)

Types for Safe Locking: Static Race Detection for Java (TOPLAS’06)

Hybrid Type Checking (POPL’06)

Automatic Synchronization Correction (SCOOL’05)

Modular Verification of Multithreaded Programs (TCS 2005)

Extending JML for Modular Specification and Verification of Multi-Threaded Programs (ECOOP’05)

Dynamic Partial-Order Reduction for Model Checking Software (POPL’05) (addendum)

Exploiting Purity for Atomicity (ISSTA'04 Distinguished Paper)

Retrospective: The Essence of Compiling with Continuations (Best of PLDI: 1979-1999)

A Type and Effect System for Atomicity (PLDI'03)

Extended Static Checking for Java (PLDI'02, Most Influential Paper Award)



Tutorials and Talks



Cooperative Concurrency for a MultiCore World, Invited Talk at the EC2 Workshop 2015
Dynamic Analyses for Reliable Concurrency, Keynote at ISSTA 2014
UPMARC 2014 Summer School lectures on Analysis Techniques to Detect Concurrency Errors, Invited Tutorial
Cooperative Concurrency for a MultiCore World, Invited Talk at RV 2011
Virtual Values for Language Extension, Dagstuhl Workshop on Foundations of Scripting Languages 2012
Temporal Higher-Order Contracts, Dagstuhl Workshop on Foundations of Scripting Languages 2012
Static and Dynamic Analyses for Concurrency Summer School on Language-Based Techniques for Concurrent and Distributed Software 2006
Atomicity for Reliable Concurrent Software, PLDI tutorial 2005



Research Projects

Data Race Detection
RoadRunner : A Dynamic Analysis Infrastructure
Cooperable Concurrency : A Concurrent Programming Methodology
Atomicity
Hybrid Type Checking

Extended Static Checking (POPL'01, POPL'01.ppt, PLDI'02, POPL'02)

Static Race Detection (ESOP'99, CONCUR'99, PLDI'00, PASTE'01, SAS'04, SAS’04.ppt)

Constraint logic for program checkers (ESOP'03, ESOP'03.ppt, CP+CV'04, CP+CV'04.ppt, Science of Computer Programming '04)

Calvin, a checker for multithreaded Java programs (ESOP'02, CAV'02, CAV'02.ppt) based on thread-modular reasoning (SPIN'03, SPIN'03.ppt) and reduction (MC'03)

Houdini, an annotation inference system for modular static checkers (IPL'00, FME'01, FME'01.ppt)

MrSpidey, an interactive static checker for Scheme (PLDI'96, Thesis) used in DrScheme (JFP'01, PLILP'97) and based on Componential Set-Based Analysis (TOPLAS'99, PLDI'97)