are also referenced under publications, because the
technical report corresponds closely to a published article.
By chronology I mean publication date; I've had my share of multi-year delays for journal publications.
A recursion theorem for predicate transformers on inductive data types, Information Processing Letters 50 (1994) 329-336. (Here is a preprint.)
Predicate transformers and higher order programs, Theoretical Computer Science 150 (1995) 111-159. (Here is a preprint).
Data refinement, call by value, and higher order programs, Formal Aspects of Computing 7 (1995) 652-662.
A categorical model of higher order imperative programming, Mathematical Structures in Computer Science 8, 4 (1998) 351-399. (Here is a preprint).
Calculating Sharp Adaptation Rules, Information Processing Letters 7 (2000) 201-208.
A Weakest Precondition Semantics for Refinement of Object-oriented Programs, IEEE Transactions on Software Engineering 26, 8 (2000) 713-728 (with Ana Cavalcanti). There is an Extended Version, SIT Report 9903.
Predicate transformer semantics of a higher order imperative language with record subtypes, Science of Computer Programming 41, 1 (2001) 1-51. (Also appeared as SIT Report 9801.)
Soundness of data refinement for a higher order imperative language, Theoretical Computer Science 278 (2002) 271-301. (Also appeared as SIT Report 99-05.)
Ownership Confinement Ensures Representation Independence for Object-oriented Programs, (with Anindya Banerjee), Journal of the ACM 52(6) (2005) 894-960. This supersedes the following POPL version (see below), improving and extending it to include a static analysis and substantial examples. Additional examples and proofs appear in SIT Report 2004-14 which is slightly revised from the Dec 2002 submission).
Stack-based Access Control for Secure Information Flow, Sept 2003 (with Anindya Banerjee). Journal of Functional Programming (2005) 15(2) 131-177, special issue on Language Based Security.
Towards imperative modules: Reasoning about invariants and sharing of mutable state. In Theoretical Computer Science 365 (2006) 143-168. This supersedes the extended abstract which appears in LICS 2004 (with Mike Barnett). Here are the slides.
Observational purity and encapsulation, Theoretical Computer Science 376 (2007) 205-224. This supersedes the conference version which appeared in Fundamental Aspects of Software Engineering (FASE) 2005 and was awarded Best Software Science Paper by the EASST at ETAPS 2005. Here are the slides.
On assertion-based encapsulation for object invariants and simulations, Formal Aspects of Computing 19(2) 2007, 205-224. Supersedes the VSTTE position paper 2005.
A common sense management model, IEEE Software, Nov. 1991 (with R.T. Yeh et al.)
Program derivation for freshmen, Proceedings of ACM Conference of the Special Interest Group in Computer Science Education 1994 (with R. Denman, W. Potter, and G. Richter).
Predicate transformer semantics of an Oberon-like language, Proceedings of IFIP TC2 Working Conference on Programming Concepts, Methods and Calculi, E.-R. Olderog, ed., Elsevier (1994) 467-487.
On the essence of Oberon, Proceedings of Conference on Programming Languages and System Architecture, J. Gutknecht, ed., Springer-Verlag (1994) 313-327.
Beyond Fun: order and membership in polytypic imperative programming, Proceedings of Mathematics of Program Construction, Johan Jeuring, ed, Springer-Verlag (1998) 286-314.
Towards squiggly refinement algebra, in Programming Concepts and Methods, David Gries and Willem-Paul de Roever, eds, Chapman and Hall (1998) 346-365.
A weakest precondition semantics for refinement in an object-oriented language, Proceedings of World Congress on Formal Methods, LNCS 1709 (1999) 1439-1459 (with Ana Cavalcanti).
Ideal models for pointwise relational and state-free imperative programming. Proceedings of ACM Principles and Practice of Declarative Programming (2001) 4-15.
Representation Independence, Confinement, and Access Control, Proceedings of ACM Principles of Programming Languages POPL 2002 (with Anindya Banerjee). (Here are slides from POPL and the paper with appendix.)
Forward simulation for data refinement of classes, Proceedings of Formal Methods Europe FME'2002, LNCS 2391, 471-490 (with Ana Cavalcanti). There is an Extended Version, SIT Report 2001-4.
On a specification-oriented model for object-orientation, Proceedings of Sixth Brazilian Symposium on Programming Languages, 114-127 (2002) (with Ana Cavalcanti).
Secure Information Flow and Pointer Confinement in a Java-like Language, Proceedings of Fifteenth IEEE Computer Security Foundations CSFW (2002) 253-270 (with Anindya Banerjee).
Using Access Control for Secure Information Flow in a Java-like Language, Proceedings of Sixteenth IEEE Computer Security Foundations CSFW (2003) 155-169 (with Anindya Banerjee).
CodeBLUE: a Bluetooth interactive dance club system, in IEEE Global Telecommunications Conference GLOBECOM (2003) 2814-2818. (with Dennis Hromin, Michael Chladil, Natalie Vanatta, Susanne Wetzel, Farooq Anjum, and Ravi Jain).
Towards imperative modules: Reasoning about invariants and sharing of mutable state (extended abstract), in IEEE Logic in Computer Science LICS 2004. Here are the slides.
Friends need a bit more: Maintaining invariants over shared state , in Mathematics of Program Construction 2004 (with Mike Barnett).
Modular and constraint-based information flow inference for an object-oriented language, in 11th International Static Analysis Symposium SAS 2004 84-99 (with Qi Sun and Anindya Banerjee).
Observational purity and encapsulation, in Fundamental Aspects of Software Engineering (FASE) 2005. Awarded Best Software Science Paper by the EASST at ETAPS 2005. Here are the slides.
State based ownership, reentrance, and encapsulation, in ECOOP 2005, 387-411 (with Anindya Banerjee).
Verifying a secure information flow analyzer, In Theorem Proving in Higher Order Logics (TPHOLS), 211-226, 2005. Here are the PVS files.
Modular reasoning in object oriented programming, position paper in Verified Softare: Theories, Tools, Technologies (VSTTE) 2005. Here are the slides.
Deriving an Information Flow Checker and certifying compiler for Java, with Gilles Barthe and Tamara Rezk, in 27th IEEE Symposium on Security and Privacy, May 2006 230-242.
Allowing State Changes in Specifications, invited paper in International Conference on Emerging Trends in Information and Communication Security, with Mike Barnett, Wolfram Schulte, and Qi Sun.
Category theoretic models of data refinement, with Michael Johnson and John Power. Proceedings of Irish Conference on Mathmatical Foundations of Computer Science and Information Technology MFCSIT (2006), invited paper, to appear.
From coupling relations to mated invariants for checking information flow (extended abstract), in ESORICS 2006 (European Symposium on Research in Computer Security), LNCS 4189, 279-296.
Closing internal timing channels by transformation, with Alejandro Russo, John Hughes, and Andrei Sabelfeld, to appear in 11th Asian Computing Science Conference, Tokyo, Dec 2006.
Beyond stack inspection: a unified access-control and information-flow security model, with Marco Pistoia and Anindya Banerjee, in 28th IEEE Symposium on Security and Privacy, May 2007, 149-163.
Modular Verification of Higher-Order Methods with Mandatory Calls Specified by Model Programs, in Object Oriented Programming, Languages, and Systems OOPSLA (2007) with Steve M. Shaner and Gary T. Leavens (Iowa State University TR-07-04). Awarded Best Student Paper.
Expressive declassification policies and modular static enforcement, with Anindya Banerjee and Stan Rosenberg, in 29th IEEE Symposium on Security and Privacy, May 2008.
Regional Logic for Local Reasoning about Global Invariants, with Anindya Banerjee and Stan Rosenberg. In European Conference on Object Oriented Programming, ECOOP 2008. Won the ECOOP 2008 Distinguished Paper Award.
Simulation and class refinement for Java (with Ana Cavalcanti). In ECOOP 2000 Workshop on Formal Techniques for Java Programs, S. Drossopoulou, S. Eisenbach, B. Jacobs, G.T. Leavens, P. Muller, and A. Poetzsch-Heffter, eds. Technical Report 269, Fernuniversitat Hagen, 2000.
Class refinement for sequential java, with Ana Cavalcanti. In ECOOP 2001 Workshop on Formal Techniques for Java Programs, S. Eisenbach, G.T. Leavens, P. Muller, A. Poetzsch-Heffter, E. Poll, eds.
High assurance for interactive applications in ad hoc networks, Proceedings of First International Workshop on Wireless Security Technologies, London, April 2003 (with Susanne Wetzel).
Ownership: transfer, sharing, and encapsulation, with Anindya Banerjee. In ECOOP 2003 Workshop on Formal Techniques for Java Programs, July 2003.
99.44% pure: Useful Abstractions in Specifications, with Mike Barnett, Wolfram Schulte, and Qi Sun. In EC0OP 2004 Workshop on Formal Techniques for Java-like Programs, June 2004.
History-based access control and secure information flow, with Anindya Banerjee, in Proceedings of the workshop on Construction and Analysis of Safe, Secure and Interoperable Smart Cards (CASSIS), May 2004.
Assertion-based encapsulation, invariants and simulations, July 2005 (invited survey paper), in proceedings of Formal Methods for Components and Objects FMCO 2004.
Towards a Logical Account of Declassification (Short Paper), with Anindya Banerjee and Stan Rosenberg, in ACM SIGPLAN workshop on Programming Languages and Analysis for Security 2007, 61-66.
Items marked with are also referenced under publications, because the
technical report corresponds closely to a published article.
* Predicate transformer semantics of a higher order imperative language with record subtypes, SIT Report 98-01 (1998).
* A Weakest Precondition Semantics for an Object-oriented Language of Refinement, extended version. SIT Report 99-03 (1999) (with Ana Cavalcanti).
* Soundness of data refinement for a higher order imperative language, SIT Report 99-05 (1999).
* Deriving sharp rules of adaptation for Hoare logics, SIT Report 99-06 (1999).
* An ideal model for pointwise relational programming, SIT Report 20-04 (Dec. 2000).
A Static Analysis for Instance-based Confinement in Java, (with Anindya Banerjee) Nov 2001.
A simple semantics and static analysis for Java security, SIT Report 2001-1 (with Anindya Banerjee). (There is also a short version: A simple static analysis for Java security, June 2001 (with Anindya Banerjee).
Patterns, heaps, and imperative lambdas, revised Jan. 2002, from following item.
Patterns and lax lambda laws for relational and imperative programming, SIT Report 2001-2.
* codeBLUE: a Bluetooth interactive dance club system, SIT Report 2002-1 (May 2002) (with Dennis Hromin, Michael Chladil, Natalie Vanatta, Farooq Anjum, and Ravi Jain).
Ownership transfer and abstraction, Kansas State University CIS Tech Report 2004-1, Oct 2003 (with Anindya Banerjee).
Constraint-based secure information flow inference for a Java-like language, Kansas State University CIS Tech Report 2004-2 (with Qi Sun and Anindya Banerjee).
Machine-checked correctness of a secure information flow analyzer (preliminary report), SIT Report CS-2004-10, March 2004. Here are the PVS files.
State based encapsulation and generics, Dec 2004 SIT Report CS-2004-11 (also appears as Kansas State University CIS-TR-2004-5) (with Anindya Banerjee)
A Logical Account of Secure Declassification, submitted Feb 2006, with Anindya Banerjee.
Behavioral Subtyping, Specification Inheritance, and Modular Reasoning, July 2006, with Gary Leavens (Iowa State University TR-06-20).
Preliminary Definition of Core JML, Sept 2006, with Gary T. Leavens and Stan Rosenberg (Stevens Institute of Technology CS Report 2006-07). See also the PVS source files.
Behavioral Subtyping is Equivalent to Modular Reasoning for Object-oriented Programs, March 2007, with Gary T. Leavens. The technical report is Iowa State University TR-06-36.
Regional Logic for Local Reasoning about Global Invariants, July 2007, with Anindya Banerjee and Stan Rosenberg. In improved treatment of the hypothetical frame rule is discussed in this note.
Expressive declassification policies and modular static enforcement, with Anindya Banerjee and Stan Rosenberg, Stevens CS TR-2007-04. A version will appear in 29th IEEE Symposium on Security and Privacy, May 2008.
An admissible second order frame rule in region logic, Mar 2008, Stevens CS TR-2008-02. There is a shorter version.
Boogie Meets Regions: a Verification Experience Report, with Anindya Banerjee and Mike Barnett. To appear in VSTTE 2008. The BoogiePL files can be found here and in the Microsoft Tech Report.
Two-categories and program structure, PhD thesis 1992.