Publications by
Cormac Flanagan
Refereed Publications
Atomizer: A Dynamic Atomicity Checker for Multithreaded Programs
(Science of Computer Programming '08)
Velodrome: A Sound and Complete Dynamic Analysis for Atomicity
(PLDI '08)
Static Report: Specifying JavaScript with ML
(ML '07)
Cartesian Partial-Order Reduction
(SPIN '07)
Sage: Unified Hybrid Checking for First-Class Types, General Refinement Types, and Dynamic
(extended technical report)
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
(SCP '06)
Sage: Hybrid Checking for Flexible Specifications
(Scheme '06, superceded by Sage tech report above)
Automatic Architecture Extraction
(FATES/RV '06)
Types for Safe Locking: Static Race Detection for Java
(TOPLAS '06)
Hybrid Types, Invariants, and Refinements for Imperative Objects
(FOOL '06)
Hybrid Type Checking
(POPL '06)
Automatic Synchronization Correction
(SCOOL '05)
Modular Verification of Multithreaded Programs
(TCS 2005)
Exploiting Purity for Atomicity
(TSE 2005)
Automatic Type Inference via Partial Evaluation
(PPDP '05)
Extending JML for Modular Specification and Verification of Multi-Threaded Programs
(ECOOO '05)
Type Inference for Atomicity
_ (TLDI '05)
Dynamic Partial-Order Reduction for Software Model Checking
(POPL '05)
Type Inference Against Races
(SAS'04)
Exploiting Purity for Atomicity
(ISSTA'04 Distinguished Paper)
Automatic Software Model Checking via Constraint Logic
(Science of Computer Programming '04)
Verifying Commit-Atomicity using Model-Checking
(SPIN'04)
Software Model Checking via Iterative Abstraction Refinement of Constraint Logic Queries
(CP+CV'04)
Atomizer: A Dynamic Atomicity Checker for Multithreaded Programs
(POPL'04)
Retrospective: The Essence of Compiling with Continuations
(Best of PLDI: 1979-1999)
Transactions for Software Model Checking
(Workshop on Software Model Checking'03)
Theorem Proving using Lazy Proof Explication
(CAV'03)
A Type and Effect System for Atomicity
(PLDI'03)
Thread-Modular Model Checking
(SPIN'03)
Automatic Software Model Checking via CLP
(ESOP'03)
Types for Atomicity
(TLDI'03)
A Modular Checker for Multithreaded Programs
(CAV'02)
Extended Static Checking for Java
(PLDI'02)
Thread-Modular Verification for Shared-Memory Programs
(ESOP'02)
Predicate Abstraction for Software Verification
(POPL'02)
DrScheme: A Programming Environment for Scheme
(JFP'01)
Detecting Race Conditions in Large Programs
(PASTE'01)
Houdini, an Annotation Assistant for ESC/Java
(FME'01)
Avoiding Exponential Explosion: Generating Compact Verification Conditions
(POPL'01)
Annotation Inference for Modular Checkers
(IPL'00)
Type-Based Race Detection for Java
(PLDI'00)
Type-Based Race Detection for Java (summary)
(LICS'00)
Object Types against Races
(CONCUR'99)
Types for Safe Locking
(ESOP'99)
A New Way of Debugging Lisp Programs
(Lisp in the Mainstream)
Componential Set-Based Analysis
(TOPLAS'99)
The Semantics of Future and an Application
(JFP'99)
DrScheme: A Pedagogic Programming Environment for Scheme
(PLILP'97)
Componential Set-Based Analysis
(PLDI'97)
Catching Bugs in the Web of Program Invariants
(PLDI'96)
pHluid: The Design of a Parallel Functional Language Implementation on Workstations
(ICFP'96)
The Semantics of Future and its use in Program Optimizations
(POPL'95)
The Essence of Compiling with Continuations
(PLDI'93)
Technical Reports, etc.
An Explicating Theorem Prover for Quantified Formulas
(Hewlett-Packard Labs Technical Report HPL-2004-199, Nov. 2004)
Type Inference Against Races
(extended version)
(Williams College Technical Note 04-06, Sept. 2004)
Exploiting Purity for Atomicity
(extended version)
(Williams College Technical Note 04-05, July 2004)
Partial Type And Effect Inference for Rcc/Java in NP-Complete
(
Williams
College
Technical Note 04-01, Feb. 2004)
Thread-Modular Verification for Shared-Memory Programs
(SRC Technical Note 2001-003, November 2001)
Flexible Polyvariance in Constraint-Based Analyses
(Compaq Systems Research Center Technical Note 1999-001, Jan. 1999)
PLT MrSpidey: Static Debugger Manual
(User Guide)
Modular and Polymorphic Set-Based Analysis: Theory and Practice
(Rice CS TR96-266)
Set Based Analysis for Full Scheme and Its Use in Soft-Typing
(Rice CS TR95-254)
Well-Founded Touch Optimization of Futures
(Rice CS TR94-239)
The Semantics of Future
(Rice CS TR94-238)
Ph.D. Thesis
Componential Set-Based Analysis
(Ph.D. thesis,
Rice
University
)
Some Talks
Automatic Architecture Extraction
(FATES/RVŐ06)
Type Inference Against Races
(SASŐ04)
Software Model Checking via Iterative Abstraction Refinement of Constraint Logic Queries
(CP+CV'04)
Verifying Commit-Atomicity using Model-Checking
(SPIN'04)
Types for Atomicity in Multithreaded Software
(various venues)
Thread-Modular Model Checking
(SPIN'03)
Automatic Software Model Checking via CLP
(ESOP'03)
A Modular Checker for Multithreaded Programs
(CAV'02)
Houdini, an Annotation Assistant for ESC/Java
(FME'01)
Avoiding Exponential Explosion: Generating Compact Verification Conditions
(POPL'01)