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 (directions)
       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)

CMPS203 Programming Languages F04  F05  F07  W09  W11  W12  W13

Research and Teaching in Computer Science and Engineering
F09  F10

CMPS280G Software Engineering Seminar W04   F04   S06   S08    F09   F10

Topics in Software Engineering
W04  S05

Software Engineering Methodology
S04  W05  W06

Comparative Programming Languages
W07  W13  W14  W15

Advanced Programming Languages
S07  S09  S12  S15

CMPS12A/L Introduction to Programming S06  S08   F12  F13

Research Projects

RoadRunner : A Dynamic Analysis Infrastructure
Cooperable Concurrency : A Concurrent Programming Methodology 
Concurrency Types for X10: Race-Freedom, Atomicity, and Determinism
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)

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)
Status Report: Specifying JavaScript with ML (ML’07)
Cartesian Partial-Order Reduction (SPIN '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

Dynamic Analyses for Reliable Concurrency, Keynote at ISSTA 2014
UPMARC 2014 Summer School lectures on Analysis Techniques to Detect Concurrency Errors
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