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 (ECOOPÕ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 Recent 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)