Cormac Flanagan

Software and Languages Research Group
Computer Science DeptSchool of EngineeringUCSC

Email:      cormac at  
Phone:     831-459-5375    (fax)  831-459-4829
Address:  1156 High Street MS: SOE3, Santa Cruz CA 95064
Office:     Engineering 2 Building, room 367 (directionsOffice hours: 11-12 Thursday
       Vitae, Google Scholar, DBLP, CiteSeer, ACM DL, Libra, Arnetminer, MS academic search


Students Dustin Rhodes

Christopher Schuster

Tim Disney

Daniel Fava

Thomas Schmitz

Kenn Knowles (now at Google)

Tom Austin (now an Assistant Professor at San Jose State University)

Jaeheon Yi (now at Google)

Aaron Tomb (now at Galois Connections)


Spring 2015:  CMPS253 Advanced Programming Languages

Research Projects

Data Race Detection
RoadRunner : A Dynamic Analysis Infrastructure
Cooperable Concurrency : A Concurrent Programming Methodology
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)

Selected Recent Publications
(older publications)

Array Shadow State Compression for Precise Dynamic Race Detection (ASE'15)
Contracts for Async Patterns in JavaScript (STOP'15)
End-To-End Policy-Agnostic Security for Database-Based Applications
Game Semantics for Type Soundness (LICS'15)
A Light-Weight Effect System for JavaScript (STOP'15)
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)

Unifying Hybrid Types and Contracts (TFP’07)

Space Efficient Gradual Typing (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)

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

Conferences and Workshops

PC Chair, PLDI 2013
Co-Chair:  Tools and Algorithms for Construction and Analysis of Systems (TACAS) 2012,  Tallin, Estonia
Co-Chair:  ACM SIGPLAN Workshop on Programming Languages meets Program Verification 2010
PC Member: FOOL 2013ESSOS 2014

Conferences 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