A Theory of Slicing for Imperative Probabilistic Programs |
Abstract
BibTeX
| TOPLAS in pdf (© ACM)
This is a substantially extended version of A Theory of Slicing for Probabilistic Control-Flow Graphs.
|
Correctly Slicing Extended Finite State Machines |
Abstract
BibTeX
| Hankin Festschrift in pdf (© Springer-Verlag) 2013 Tech Report in pdf
Presentation in pdf
|
A Theory of Slicing for Probabilistic Control-Flow Graphs |
Abstract
BibTeX
| FoSSaCS'16 in pdf (© Springer-Verlag) Presentation in pdf
|
A Certificate Infrastructure for Machine-Checked Proofs of Conditional Information Flow |
Abstract
BibTeX
| POST'12 in pdf (© Springer-Verlag) Presentation in pdf
|
An Alternative Characterization of Weak Order Dependence |
Abstract
BibTeX
| Short paper in pdf
|
Precise and Automated Contract-based Reasoning for Verification and Certification of Information Flow Properties of Programs with Arrays |
Abstract
BibTeX
| Preliminary full paper in pdf
ESOP'10 in pdf (© Springer-Verlag) Presentation in pdf
|
Specification and Checking of Software Contracts for Conditional Information Flow |
Abstract
BibTeX
| SAnToS report (draft) in pdf
FM'08 in pdf (© Springer-Verlag)
|
Slicing for Modern Program Structures: a Theory for Eliminating Irrelevant Loops |
Abstract
BibTeX
| KSU Report in pdf
IPL 2007 in pdf
Presentation in pdf
|
Verification Condition Generation for Conditional Information Flow |
Abstract
BibTeX
| KSU Report in pdf
FMSE'07 in pdf (
© ACM
) Presentation in pdf
|
Flow-sensitive Type Systems and the Ambient Calculus |
Abstract
BibTeX
| Full paper in pdf
Short paper in pdf
This summarizes, and puts into perspective, Causal Type System for Ambient Movements.
|
A Logic for Information Flow in Object-Oriented Programs |
Abstract
BibTeX
| Full paper in pdf
POPL 2006 in ps, pdf (
© ACM
) Presentation in pdf
|
A Logic for Information Flow Analysis with an Application to Forward Slicing of Simple Imperative Programs |
Abstract
BibTeX
| SCP 2007 in ps, pdf
This is a further development of Information Flow Analysis in Logical Form. |
A New Foundation For Control-Dependence and Slicing for Modern Program Structures |
Abstract
BibTeX
| TOPLAS (almost final) in ps, pdf
ESOP 2005 in ps, pdf (© Springer-Verlag) Presentation in pdf
|
Information Flow Analysis in Logical Form |
Abstract
BibTeX
| KSU Report in ps, pdf
SAS 2004 (extended version) in ps, pdf (© Springer-Verlag) Presentation in pdf
|
PolyA: True Type Polymorphism for Mobile Ambients |
Abstract
BibTeX
| Full paper in ps, pdf
TCS 2004 in ps, pdf
This is a further development of Mobile Processes with Dependent Communication Types and Singleton Types for Names and Capabilities.
|
Inferring Annotated Types for Inter-procedural Register Allocation with Constructor Flattening |
Abstract
BibTeX
| TLDI 2003 in ps, pdf (
© ACM
) Presentation in ppt
|
Mobile Processes with Dependent Communication Types and Singleton Types for Names and Capabilities |
Abstract
BibTeX
| Short paper in ps, pdf
Presentation in pdf
|
Causal Type System for Ambient Movements |
Abstract
BibTeX
| KSU Report in pdf
Short paper in ps, pdf
Presentation in pdf
|
Orderly Communication in the Ambient Calculus |
Abstract
BibTeX
| CLSS in pdf
This journal version of What are Polymorphically-Typed Ambients?
contains the core features only, yet complete.
|
What are Polymorphically-Typed Ambients? |
Abstract
BibTeX
| BU Report in ps, pdf
ESOP 2001 in ps, pdf (
© Springer-Verlag
) Presentation in ps, pdf, ps(4)
|
The Abstraction and Instantiation of String-Matching Programs |
Abstract
BibTeX
| Full paper in pdf
|
Faithful Translations between Polyvariant Flows and Polymorphic Types |
Abstract
BibTeX
| Draft of full paper in pdf
ESOP 2000 in ps, pdf (
© Springer-Verlag
) Presentation in ps, pdf
|
Partial Evaluation for Constraint-Based Program Analyses |
Abstract
BibTeX
| BRICS Report in ps, pdf
|
Type and Effect Systems: Behaviours for Concurrency |
Abstract
BibTeX
| Monograph
|
Behaviour Analysis for Validating Communication Patterns |
Abstract
BibTeX
| STTT 1998 in ps, pdf
Presentation in pdf
|
Behaviour Analysis and Safety Conditions: a Case Study in CML |
Abstract
BibTeX
| FASE 1998 in ps, pdf (
© Springer-Verlag
)
|
Polymorphic Subtyping for Effect Analysis: the Static Semantics |
Abstract
BibTeX
| Short paper in ps, pdf (
© Springer-Verlag
)
|
Polymorphic Subtyping for Effect Analysis: the Dynamic Semantics |
Abstract
BibTeX
| Short paper in ps, pdf (
© Springer-Verlag
)
|
Polymorphic Subtyping for Effect Analysis: the Algorithm |
Abstract
BibTeX
| Short paper in ps, pdf (
© Springer-Verlag
)
|
Type and Behaviour Reconstruction for Higher-Order Concurrent Programs |
Abstract
BibTeX
| JFP 1997 in ps, pdf
|
Local Type Reconstruction by means of Symbolic Fixed Point Iteration |
Abstract
BibTeX
| ESOP 1994 in ps, pdf (
© Springer-Verlag
)
|
Strictness Types: An Inference Algorithm and an Application |
Abstract
BibTeX
| DAIMI Report in ps, pdf
This report covers
Minimal Thunkification as well as
Local Type Reconstruction by means of Symbolic Fixed Point Iteration
|
Minimal Thunkification |
Abstract
BibTeX
| WSA 1993 in ps, pdf (
© Springer-Verlag
) Presentation in ps, pdf
|
Sharing of Computations |
Abstract
BibTeX
| PhD Thesis, 1993 in ps, pdf
|
Unfold/fold Transformations Preserving Termination Properties |
Abstract
BibTeX
| PLILP 1992 in ps, pdf (
© Springer-Verlag
)
|
Properties of Unfolding-based Meta-level Systems |
Abstract
BibTeX
| PEPM 1991 in ps, pdf
|
Partial Memoization for obtaining Linear Time Behavior of a 2DPDA |
Abstract
BibTeX
| TCS 1992
|
Experiments with Implementations of Two Theoretical Constructions |
Abstract
BibTeX
| Botik 1989 in pdf
|
Memoization and its use in Lazy and Incremental
Program Generation |
Abstract
BibTeX
| M.Sc Thesis, 1989 in pdf
|