| CARVIEW |
Select Language
HTTP/1.1 302 Found
Date: Thu, 15 Jan 2026 22:57:54 GMT
Server: Apache/2.4.6 (CentOS)
Strict-Transport-Security: max-age=63072000; includeSubDomains
X-Frame-Options: SAMEORIGIN
X-Content-Type-Options: nosniff
Location: https://users.soe.ucsc.edu/~cormac/
Content-Length: 303
Connection: close
Content-Type: text/html; charset=iso-8859-1
HTTP/1.1 200 OK
Date: Thu, 15 Jan 2026 22:57:55 GMT
Server: Apache/2.4.6 (CentOS)
Strict-Transport-Security: max-age=63072000; includeSubDomains
X-Frame-Options: SAMEORIGIN
X-Content-Type-Options: nosniff
Accept-Ranges: bytes
Connection: close
Transfer-Encoding: chunked
Content-Type: text/html
Cormac Flanagan Homepage
 |
Cormac Flanagan
Professor |
| Awards | Fellow of the Association for Computing
Machinery |
| 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" |
|
| ECOOP 2024 Distinguished Paper Award for "Mover Logic: A Concurrent Program Logic for Reduction and Rely-Guarantee Reasoning" | |
| 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 | |
| ScholarGPS
highly ranked scholar |
| Service | Steering Committee Chair, ACM
Conference on Programming Language Design and
Implementation (PLDI) |
|
| Associate Editor, ACM Transactions on
Programming Languages and Systems (TOPLAS) |
||
|
||
| 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) |
| 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 |
|
|
|
| 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) |