mugshot

Cormac Flanagan

Professor
Department of Computer Science and Engineering 
Baskin School of Engineering
University of California Santa Cruz
Email:      cormac at ucsc.edu  
Phone:     831-459-5375  
Office:     Engineering 2 Building, room 367 (directions)  
Address:  1156 High Street MS: SOE3, Santa Cruz CA 95064
Misc:
       Vitae, Google Scholar, DBLP, ACM DL

New:        Try out our Anchor Verifier!

---

Awards Fellow of the ACM

Alfred P. Sloan Foundation Fellow

POPL Most Influential Paper Award for "Multiple Facets for Dynamic Information Flow"

PLDI Most Influential Paper Award for "FastTrack: Efficient and Precise Dynamic Race Detection"

PLDI Most Influential Paper Award for "Extended Static Checking for Java"

CSF Distinguished Paper Award for "Transparent IFC Enforcement: Possibility and (In)Efficiency Results"

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

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

ISSTA Distinguished Paper Award for "Exploiting Purity for Atomicity"

UCSC Excellence in Teaching Award

---

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

Member of UCSC Senate Committee on Educational Policy

---

Students & Alumni Sohum Banerjea

Thomas Schmitz

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)

Christopher Schuster (now at Google)

Dustin Rhodes (now at Google)



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)



Transparent IFC Enforcement: Possibility and (In)Efficiency Results (CSF'20, Distinguished Paper Award)
The Anchor Verifier for Blocking and Non-blocking Concurrent Software (OOPSLA'20) Talk Artifact Demo Appendix
Optimizing Faceted Secure Multi-Execution (CSF'19)
IDVE: an Integrated Development and Verification Environment for JavaScript (Programming'19)
Secure Serverless Computing using Dynamic Information Flow Control (OOPSLA'18)
ESVERIFY: Verifying Dynamically-Typed Higher-Order Functional Programs by SMT Solving (IFL'18)
Faceted Secure Multi Execution (CCS'18)
A Better Facet of Dynamic Information Flow Control (WWW'18)
VerifiedFT: A Verified, High-Performance Dynamic Race Detector (PPOPP'18)
Using Precise Taint Tracking for Auto-sanitization (PLAS'17)
Multiple Facets for Dynamic Information Flow with Exceptions (TOPLAS May 2017)
BigFoot: Static Check Placement for Dynamic Race Detection (PLDI'17, Distinguished Artifact Award, extended technical report)
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, Most Influential Paper Award)
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, Most Influential Paper Award).   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)

Space Efficient Gradual Typing (TFP’07)

Status Report: Specifying JavaScript with ML (ML’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



Towards Efficient and Precise Concurrent Software Analysis, ETAPS 2019 Keynote
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

The Anchor Verifier for Concurrent Software
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)