Cormac Flanagan
Professor
Department of Computer Science and Engineering
Baskin School of Engineering
University of California Santa Cruz
- cormac at ucsc.edu
- Office
- Engineering 2 Building, room 367 (directions)
- Address
- 1156 High Street MS: SOE3, Santa Cruz CA 95064
My research is in programming languages and software engineering, with a focus on tools and techniques for building reliable software. My current work addresses modular verification of concurrent software (Keystone, Mover Logic), dynamic information flow control to prevent leaks of confidential data (faceted execution), and reproducibility in computational notebooks (FlowBook). Earlier work includes data race detection (FastTrack, RoadRunner), atomicity, static checking (ESC/Java, Houdini), and hybrid type systems.
I am a Professor of Computer Science and Engineering at the University of California, Santa Cruz. Before joining UCSC in 2003, I was a Principal Research Scientist at Digital Equipment Corporation, Compaq, and Hewlett-Packard. I received my Ph.D. from Rice University and my B.Sc. in Computer Science and Mathematics from University College Dublin.
New FlowBook: Enforcing Reproducibility in Computational Notebooks (with Stephen Freund, Emery Berger, and Eunice Jun), arXiv 2026
Current Research Earlier projects ↓
-
FlowBook: Enforcing Reproducibility in Computational NotebooksFlowBook is a JupyterLab extension that enforces rerun consistency: re-executing any cell from the current state would produce a result consistent with a top-to-bottom execution of the notebook, regardless of which cells have been run, modified, and rerun.
(arXiv’26) -
Keystone: Modular Concurrent Software VerificationSpecifying and reasoning about thread interference with Mover Logic, a program logic for modular verification of concurrent software.
(OOPSLA’20, ECOOP’24, Melvin demo) -
Information Flow ControlDynamic mechanisms, notably faceted execution, that stop programs leaking confidential data, applied to browsers, database-backed applications, and serverless computing.
(TR’21, CSF’20, CSF’19, OOPSLA’18, CCS’18, WWW’18, TOPLAS’17, PLAS’17, PLDI’16, POST’16, TR’14, PLAS’13, APLAS’12, POPL’12, STOP’11, PLAS’10, PLAS’09)
Honors and Awards
- Fellow of the Association for Computing Machinery
- Member of the inaugural class of the ACM SIGSOFT Software Engineering Academy (2026)
- Alfred P. Sloan Foundation Fellow
- ScholarGPS highly ranked scholar in Programming Languages (lifetime)
- UCSC Excellence in Teaching Award
Most Influential Paper Awards
- POPL Most Influential Paper AwardMultiple Facets for Dynamic Information Flowwith Thomas H. AustinPOPL 2012
- PLDI Most Influential Paper AwardFastTrack: Efficient and Precise Dynamic Race Detectionwith Stephen N. FreundPLDI 2009
- PLDI Most Influential Paper AwardExtended Static Checking for Javawith K. Rustan M. Leino, Mark Lillibridge, Greg Nelson, James B. Saxe, and Raymie StataPLDI 2002
Distinguished Paper Awards
- ECOOP Distinguished Paper AwardMover Logic: A Concurrent Program Logic for Reduction and Rely-Guarantee Reasoningwith Stephen N. FreundECOOP 2024
- CSF Distinguished Paper AwardTransparent IFC Enforcement: Possibility and (In)Efficiency Resultswith Maximilian AlgehedCSF 2020
- ISSTA Distinguished Paper AwardExploiting Purity for Atomicitywith Stephen N. Freund and Shaz QadeerISSTA 2004
Other Paper Awards
- ECOOP Best Paper AwardRedCard: Redundant Check Elimination for Dynamic Race Detectorswith Stephen N. FreundECOOP 2013
- PLDI Distinguished Artifact AwardBigFoot: Static Check Placement for Dynamic Race Detectionwith Dustin Rhodes and Stephen N. FreundPLDI 2017
- TCS Top Cited Article Award 2005–2010Modular Verification of Multithreaded Programswith Stephen N. Freund, Shaz Qadeer, and Sanjit A. SeshiaTCS 2005
Service
- Steering Committee Chair, ACM Conference on Programming Language Design and Implementation (PLDI), 2016–19
- Associate Editor, ACM Transactions on Programming Languages and Systems (TOPLAS), 2013–16
- Program Committee Chair, Programming Language Design and Implementation (PLDI), 2013
- Co-Chair, Tools and Algorithms for Construction and Analysis of Systems (TACAS), 2012
- Steering Committee Co-Chair, ACM SIGPLAN Workshops on Programming Languages meets Program Verification, 2011–15
- Co-Chair, ACM SIGPLAN Workshop on Programming Languages meets Program Verification, 2010
- Member of UCSC Senate Committee on Planning and Budget, 2015–18 and 2020–21
- Member of UCSC Senate Committee on Educational Policy, 2009–11 and 2022–24
Publications
- arXiv 2026
- ECOOP 2024
- TR 2021
- OOPSLA 2020
- CSF 2020
- CSF 2019
- Programming 2019
- OOPSLA 2018
- IFL 2018
- CCS 2018
- WWW 2018
- PPoPP 2018
- PLAS 2017
- TOPLAS 2017
- PLDI 2017
- FTFJP 2017
- PLDI 2016
- ESOP 2016
- POST 2016
- CROW 2016
- SCP 2015
- ASE 2015
- REBLS 2015
- STOP 2015
- LICS 2015
- STOP 2015
-
FPW 2014
Traveling Through Time And Code: Omniscient Debugging And Beyond
- DLS 2014
- TR 2014
- DLS 2014
- ECOOP 2013
- PLAS 2013
- APLAS 2012
- ISSTA 2012
- ISSTA 2012
- POPL 2012
- POPL 2012
- OOPSLA 2011
- RV 2011
- FOOL 2011
- ICFP 2011
- STOP 2011
- POPL 2011
- PPoPP 2011
- CACM 2010
- HOSC 2010
- PLDI 2010
- PASTE 2010
- PLAS 2010
- TLDI 2010
-
PLDI 2009
FastTrack: Efficient and Precise Dynamic Race DetectionA revised version of this paper appeared in CACM research highlights, Nov. 2010.
- TOPLAS 2010
- PADTAD 2009
- PLAS 2009
- PLPV 2009
- ESOP 2009
- TOPLAS 2008
- PLDI 2008
- WMM 2008
- SCP 2008
- SCP 2007
- SPIN 2007
- TFP 2007
- ML 2007
- TFP 2007
- ESOP 2007
- Scheme 2006
-
Scheme 2006
Sage: Hybrid Checking for Flexible Specifications
- FATES/RV 2006
- TOPLAS 2006
- FOOL 2006
- POPL 2006
- SCOOL 2005
- TCS 2005
- TSE 2005
- PPDP 2005
- ECOOP 2005
- TLDI 2005
- POPL 2005
- SAS 2004
- ISSTA 2004
- SCP 2004
- SPIN 2004
- CP+CV 2004
- POPL 2004
- Best of PLDI
- SoftMC 2003
- CAV 2003
- PLDI 2003
- SPIN 2003
- ESOP 2003
- TLDI 2003
- CAV 2002
- PLDI 2002
- ESOP 2002
- POPL 2002
- JFP 2002
- PASTE 2001
- FME 2001
- POPL 2001
- IPL 2001
- PLDI 2000
- LICS 2000
- CONCUR 1999
- ESOP 1999
- Lisp 1998
- TOPLAS 1999
- JFP 1999
- PLILP 1997
- PLDI 1997
- PLDI 1996
- ICFP 1996
- POPL 1995
- PLDI 1993
Technical Reports, etc.
- 2004
- 2004
- 2004
- 2004
- 2001
- 1999
- 1997
- 1996
- 1995
- 1994
- 1994
Ph.D. Thesis
- 1997
Students & Alumni
Current Students
- Sohum Banerjea Ph.D. student (on leave)
Ph.D. Alumni
- Thomas Schmitz Ph.D. 2019Dissertation: Faceted Information Flow
- Christopher Schuster Ph.D. 2018, now at GoogleDissertation: Towards Live Programming Environments for Statically Verified JavaScript
- Dustin Rhodes Ph.D. 2018, now at GoogleDissertation: Access Classification for Race Detection Optimization
- Tim Disney Ph.D. 2015, now at Shape Security (part of F5)Dissertation: Hygienic Macros for JavaScript
- Kenn Knowles Ph.D. 2014, now at GoogleDissertation: Executable Refinement Types
- Tom Austin Ph.D. 2013, now a faculty member at San Jose State UniversityDissertation: Dynamic Information Flow Analysis for JavaScript in a Web Browser
- Jaeheon Yi Ph.D. 2011, now at GoogleDissertation: Cooperability: A New Property for Multithreading
- Aaron Tomb Ph.D. 2011, now at GaloisDissertation: Program Inconsistency Detection: Universal Reachability Analysis and Conditional Slicing
Tutorials and Talks
- Towards Efficient and Precise Concurrent Software Analysis
- Cooperative Concurrency for a MultiCore World
- Static and Dynamic Analyses for Reliable Concurrency
- UPMARC 2014 Summer School lectures on Analysis Techniques to Detect Concurrency Errors
- Cooperative Concurrency for a MultiCore World
- Virtual Values for Language Extension
- Temporal Higher-Order Contracts
- Static and Dynamic Analyses for Concurrency
- Atomicity for Reliable Concurrent Software
- Dynamic Architecture Extraction
- Type Inference Against Races
- Software Model Checking via Iterative Abstraction Refinement of Constraint Logic Queries
- Verifying Commit-Atomicity using Model-Checking
- Types for Atomicity in Multithreaded Software
- Thread-Modular Model Checking
- Automatic Software Model Checking via CLP
- A Modular Checker for Multithreaded Programs
- Houdini, an Annotation Assistant for ESC/Java
- Avoiding Exponential Explosion: Generating Compact Verification Conditions
Earlier Projects
-
RoadRunner: A Dynamic Analysis Framework for Concurrent ProgramsA framework for prototyping and composing dynamic analyses of concurrent Java programs, such as FastTrack.
(PASTE’10) -
-
-
Atomicity: Specifying and Checking Atomic Code BlocksAn atomic block behaves as if it ran without interruption, so it can be reasoned about sequentially. Type systems and dynamic checkers (Atomizer, Velodrome) verify these specifications.
(TLDI’03, PLDI’03, POPL’04, SPIN’04, ISSTA’04, TLDI’05, TSE’05, SCOOL’05, SCP’08, WMM’08, PLDI’08, TOPLAS’08, PADTAD’09) -
Hybrid Type Checking: Combining Static and Dynamic CheckingPrecise specifications such as refinement types are checked statically where possible and enforced with run-time casts otherwise, as implemented in the Sage language.
(POPL’06, TOPLAS’10, Sage technical report) -
Extended Static Checking: Finding Errors with a Theorem ProverESC/Java uses verification conditions and an automatic theorem prover to catch errors such as null dereferences and index-out-of-bounds in annotated Java programs.
(POPL’01, POPL’01.ppt, PLDI’02, POPL’02) -
-
Constraint Logic for Program Checkers: Software Model Checking via CLPSoftware model checking expressed as constraint logic queries.
(ESOP’03, ESOP’03.ppt, CP+CV’04, CP+CV’04.ppt, SCP’04) -
Calvin: A Checker for Multithreaded Java ProgramsVerifies each thread separately against a specification of how other threads may interfere (thread-modular reasoning), using reduction to treat atomic blocks as single steps.
(ESOP’02, CAV’02, CAV’02.ppt, SPIN’03, SPIN’03.ppt, MC’03) -
Houdini: Annotation Inference for Modular CheckersGuesses many candidate annotations, then uses ESC/Java to refute the invalid ones until the rest are consistent.
(IPL’01, FME’01, FME’01.ppt) -
Edited Conference Proceedings
- International Journal on Software Tools for Technology Transfer 16(2), 2014
- ACM SIGPLAN Conference on Programming Language Design and Implementation 2013
- Tools and Algorithms for Construction and Analysis of Systems (TACAS) 2012, and its special issue of selected papers in Logical Methods in Computer Science
- ACM SIGPLAN Workshop on Programming Languages meets Program Verification 2010
- Design and Validation of Concurrent Systems, Dagstuhl Seminar Proceedings 09361, 2009
- ACM SIGPLAN Workshop on Program Analysis for Software Tools and Engineering 2004