mugshot

Cormac Flanagan
Professor and Director of Graduate Studies

Software and Languages Research Group
Computer Science Dept,  School of Engineering,  UCSC

Email:      cormac at ucsc.edu  
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)
Misc:       Vitae, publications, Google Scholar, DBLP, CiteSeer, Libra, h-index = 28


Students
 Kenneth Knowles

Caitlin Sadowski

Aaron Tomb

Jaeheon Yi

Tom Austin



Teaching
 CMPS12A/L
 Introduction to Programming S06  S08

CMPS203
 Programming Languages F04  F05  F07 W09

CMPS280G
 Software Engineering Seminar W04 F04  S06  S08  F09

CMPS290G
 Topics in Software Engineering
 W04 S05

CMPS115
 Software Engineering Methodology
 S04  W05 W06

CMPS112
 Comparative Programming Languages
 W07

CMPS253
 Advanced Programming Languages
 S07   S09

CMPS200
 Research and Teaching in Computer Science and Engineering
 F09



Research Projects

 Atomicity
Hybrid Type Checking

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

Static Race Detectors (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 (more)



 Effects for Cooperable and Serializable Threads (TLDI '10)
FastTrack: Efficient and Precise Dynamic Race Detection (PLDI '09)
Hybrid Type Checking (to appear in TOPLAS)
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)
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)
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)

Type Inference Against Races (Science of Computer Programming '07)

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)

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



 Lectures at the 2006 Summer School on Language-Based Techniques for Concurrent and Distributed Software on Static and Dynamic Analyses for Concurrency
PLDI 2005 tutorial on Atomicity for Reliable Concurrent Software



Some upcoming
Conferences and Workshops
 Co-Chair:  ACM SIGPLAN Workshop on Programming Languages meets Program Verification 2010
PC Member: POPL 2010
PC Member: ESOP 2010

PC Member: PADTAD 2010