Publications
(and older publications)
|
|
Mover Logic: A Concurrent
Program Logic for Reduction and Rely-Guarantee Reasoning
(ECOOP'24, Distinguished Paper Award)
|
| Transparent IFC Enforcement:
Possibility and (In)Efficiency Results (CSF'20, Distinguished
Paper Award) |
The Anchor
Verifier for Blocking and Non-blocking Concurrent Software
(OOPSLA'20) Talk
Artifact
Demo
Appendix
|
| Optimizing Faceted
Secure Multi-Execution (CSF'19) |
IDVE: an Integrated
Development and Verification Environment for JavaScript
(Programming'19)
|
| Secure
Serverless Computing using Dynamic Information Flow
Control (OOPSLA'18) |
ESVERIFY:
Verifying Dynamically-Typed Higher-Order Functional
Programs by SMT Solving (IFL'18)
|
| Faceted Secure
Multi Execution (CCS'18) |
| A Better Facet of
Dynamic Information Flow Control (WWW'18) |
VerifiedFT: A
Verified, High-Performance Dynamic Race Detector
(PPOPP'18)
|
| Using Precise
Taint Tracking for Auto-sanitization (PLAS'17) |
| Multiple Facets
for Dynamic Information Flow with Exceptions (TOPLAS
May 2017) |
BigFoot: Static
Check Placement for Dynamic Race Detection (PLDI'17, Distinguished
Artifact Award, extended
technical report)
|
Correctness of
Partial Escape Analysis for Multithreaded Optimization
(FTFJP'17)
|
| Precise, Dynamic
Information Flow for Database-Backed Applications
(PLDI'16) |
| Macrofication:
Refactoring by Reverse Macro Expansion (ESOP'16) |
| Faceted Dynamic
Information Flow via Control and Data Monads (POST'16) |
Reactive
Programming with Reactive Variables (CROW'16)
|
| Array Shadow State
Compression for Precise Dynamic Race Detection
(ASE'15) |
Live Programming
for Event-Based Languages (REBLS'15)
|
| Contracts for
Async Patterns in JavaScript (STOP'15) |
|
|
Traveling
Through Time And Code: Omniscient Debugging And Beyond
(UCSC Technical Report 2014)
|
| Dynamic Detection
of Object Capability Violations Through Model Checking
(DLS'14) |
Typed
Faceted Values for Secure Information Flow in Haskell
(Technical report UCSC-SOE-14-07)
|
Sweeten Your
JavaScript: Hygienic Macros for ES5 (DLS'14)
|
|
|
| Faceted Execution
of Policy-Agnostic Programs (PLAS'13, revision of
original paper) |
|
|
| Cooperative
Types for Controlling Thread Interference in Java
(ISSTA'12) |
Detecting
Inconsistencies via Universal Reachability Analysis
(ISSTA'12)
|
| Multiple
Facets for Dynamic Information Flow (POPL '12, Most
Influential Paper Award) |
Sound
Predictive Race Detection in Polynomial Time (POPL
'12)
|
| Virtual
Values
for
Language Extension (OOPSLA'11) |
Cooperative
Concurrency
for
a Multicore World (RV'11 invited talk, slides)
|
Types
for
Precise
Thread
Interference (Technical report UCSC-SOE-11-22)
|
| Temporal
Higher-Order Contracts (ICFP'11) |
| Gradual
Information
Flow
Typing (STOP'11) |
Correct
Blame
for
Contracts: No More Scapegoating (POPL '11)
|
|
|
| Adversarial
Memory
for
Detecting Destructive Races (PLDI '10) |
| The
RoadRunner
Dynamic Analysis Framework for Concurrent Programs
(PASTE '10) |
| Permissive
Dynamic
Information
Flow Analysis (PLAS '10) |
| Effects
for
Cooperable
and Serializable Threads (TLDI '10) |
FastTrack:
Efficient
and
Precise Dynamic Race Detection (PLDI '09, Most
Influential Paper Award). A revised version of
this paper appeared in CACM
research
highlights,
Nov. 2010.
|
| Hybrid
Type Checking (TOPLAS'10) |
| SideTrack:
Generalizing
Dynamic
Atomicity Analysis (PADTAD '09) |
| Efficient
Purely-Dynamic
Information
Flow Analysis (PLAS '09) |
|
|
| SingleTrack:
A
Dynamic
Determinism Checker for Multithreaded Programs (ESOP
'09) |
Types for Atomicity:
Static Checking and Inference for Java (TOPLAS '08, appendix)
|
| 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) |
|
|
| Cartesian
Partial-Order Reduction (SPIN '07) |
|
Space
Efficient Gradual Typing (TFP’07) |
|
Status Report: Specifying
JavaScript with ML (ML’07) |
|
Unifying
Hybrid Types and Contracts (TFP’07) |
|
Type
Reconstruction
for General Refinement Types (ESOP’07, extended paper) |
|
|
|
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) (addendum)
|
|
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, Most Influential Paper Award)
|
