Naumann’s research papers, talks, and software

Contents

1  Selected papers by general topic

Rather than cross-list I’ve chosen arbitrarily in cases that fit multiple topics. For superseded conference and workshop versions, see section .

1.1  Security and secure information flow

Spartan Jester: end-to-end information flow control for hybrid Android applications, with Julian Sexton and Andrey Chudnov. In Mobile Security Technologies workshop (2017) to appear.

Hypercollecting semantics and its application to static analysis of information flow, with Mounir Assaf, Julien Signoles, Éric Totel, and Frédéric Tronel). In 44th ACM Symposium on Principles of Programming Languages (2017).

Calculational design of information flow monitors, with Mounir Assaf. In IEEE Computer Security Foundations Symposium (2016) 210–224.

Inlined information flow monitoring for JavaScript, with Andrey Chudnov. In ACM Conference on Computer and Communication Security (2015) 629–643.

Information flow monitoring as abstract interpretation for relational logic, with Andrey Chudnov and George Kuan. In IEEE Computer Security Foundations Symposium 2014.

Guiding a General-Purpose C Verifier to Prove Cryptographic Protocols, with François Dupressoir, Andrew D. Gordon, and Jan Jürjens. In Journal of Computer Security 22 (2014) 823-866.

A Simple Semantics and Static Analysis for Stack Inspection, with Anindya Banerjee. In Semantics, Abstract Interpretation, and Reasoning about Programs: Essays Dedicated to David A. Schmidt on the Occasion of his Sixtieth Birthday, EPTCS 129, September 2013, 284–308. (DOI: 10.4204/EPTCS.129, ISSN: 2075-2180, link).

Analysis of authentication and key establishment in inter-generational mobile telephony (long version), with Chunyu Tang and Susanne Wetzel. In the 4th International Symposium on Trust, Security and Privacy for Emerging Applications (TSP 2013).

Symbolic Analysis for Security of Roaming Protocols in Mobile Networks [Extended Abstract], with Chunyu Tang and Susanne Wetzel. In 7th International ICST Conference on Security and Privacy in Communication Networks (SecureComm), Sept 2011, 480–490.

Guiding a General-Purpose C Verifier to Prove Cryptographic Protocols, with François Dupressoir, Andrew D. Gordon, and Jan Jürjens. In IEEE Computer Security Foundations Symposium, July 2011. Extended version as Microsoft MSR–TR–2011–50.

Information Flow Monitor Inlining, with Andrey Chudnov. In IEEE Computer Security Foundations Symposium, July 2010, 200–214. See also slightly older version with proofs.

Expressive declassification policies and modular static enforcement, with Anindya Banerjee and Stan Rosenberg. In 29th IEEE Symposium on Security and Privacy, May 2008, 339–353.

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.

Closing internal timing channels by transformation, with Alejandro Russo, John Hughes, and Andrei Sabelfeld. In 11th Asian Computing Science Conference, Tokyo, Dec 2006.

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.

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.

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.

Modular and constraint-based information flow inference for an object-oriented language, with Qi Sun and Anindya Banerjee. In 11th International Static Analysis Symposium SAS 2004 84–99

Stack-based Access Control for Secure Information Flow, with Anindya Banerjee. In Journal of Functional Programming (2005) 15(2) 131–177, special issue on Language Based Security. This supersedes our CSFW 2002 and CSFW 2003 papers.

1.2  Data refinement and representation-independence

State Based Encapsulation for Modular Reasoning about Behavior-Preserving Refactorings, with Anindya Banerjee. Invited chapter in Aliasing in Object-oriented Programming, Dave Clarke and James Noble and Tobias Wrigstad, eds., Springer State-of-the-art Surveys, 2012.

Refactoring and representation independence for class hierarchies, with Leila Silva and Augusto Sampaio. Theoretical Computer Science 433 (2012) 60–97. This supersedes our FTfJP 2010 paper.

Category theoretic models of data refinement, with Michael Johnson and John Power. In Electronic Notes in Theoretical Computer Science 225(2) 21–38. Proceedings of Irish Conference on Mathmatical Foundations of Computer Science and Information Technology MFCSIT 2006.

State based ownership, reentrance, and encapsulation, with Anindya Banerjee. In ECOOP 2005, 387–411.

Ownership Confinement Ensures Representation Independence for Object-oriented Programs, with Anindya Banerjee. In Journal of the ACM 52(6) (2005) 894–960. This supersedes our POPL 2002 paper.

Forward simulation for data refinement of classes, with Ana Cavalcanti. Proceedings of Formal Methods Europe FME’2002, LNCS 2391, 471–490. There is an Extended Version, SIT Report 2001-4.

Soundness of data refinement for a higher order imperative language, Theoretical Computer Science 278 (2002) 271–301.

Data refinement, call by value, and higher order programs, Formal Aspects of Computing 7 (1995) 652–662.

1.3  Verification, semantics and refinement calculi

Relational Logic with Framing and Hypotheses, with Anindya Banerjee and Mohammad Nikouei. In 36th Conference on Foundations of Software Technology and Theoretical Computer Science (2016) 11:1–11:16. Technical report on arXiv.

Specifying and verifying advanced control features, with Gary T. Leavens, Hridesh Rajan, Tomoyuki Aotani. In 7th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (2016) LNCS 9953, 80–96.

A Logical Analysis of Framing for Specifications with Pure Method Calls, with Anindya Banerjee and Mohammad Nikouei, submitted for publication 2015. Supersedes A Logical Analysis of Framing for Specifications with Pure Method Calls, with Anindya Banerjee, in Verified Software: Theories, Tools, Experiments (VSTTE) 2014, post-proceedings, LNCS 8471.

Behavioral Subtyping, Specification Inheritance, and Modular Reasoning, with Gary Leavens. In ACM Transactions on Programming Languages and Systems 47(4) 13:1–13:88, 2015. Supersedes Iowa State tech reports TR-06-36 and TR-06-20 and U. of Central Florida CS-TR-13-03a.

Laws of Programming for References, with Giovanny Lucero and Augusto Sampaio. In 11th Asian Symposium on Programming Languages and Systems (APLAS 2013) LNCS 8301, 124–139.

Decision Procedures for Region Logic, with Anindya Banerjee and Stan Rosenberg. In 13th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), January 2012, LNCS 7148, 379–395.

Local Reasoning for Global Invariants, Part I: Region Logic, with Anindya Banerjee and Stan Rosenberg. In Journal of the ACM 60 (2013) 18:1–18:56. . (This version has an index of definitions and differs by slight copy-edits from the published version.)

Local Reasoning for Global Invariants, Part II: Dynamic Boundaries, with Anindya Banerjee. In Journal of the ACM 60 (2013) 19:1–19:73. (This version has an index of definitions and differs by slight copy-edits from the published version.)

Dynamic Boundaries: Information Hiding by Second Order Framing with First Order Assertions, with Anindya Banerjee. In Programming Languages and Systems, 19th European Symposium on Programming (ESOP) 2010, invited paper. (The version here corrects a bug in the proceedings and includes appendix.) Superseded by Local Reasoning for Global Invariants, Part II: Dynamic Boundaries (see above).

Local Reasoning and Dynamic Framing for the Composite Pattern and its Clients, with Stan Rosenberg and Anindya Banerjee. In Verified Software: Theories, Tools, Experiments, VSTTE 2010, LNCS 6217, pages 183–198.

Theory for Software Verification —DRAFT, Jan 2009.

Boogie Meets Regions: a Verification Experience Report, with Anindya Banerjee and Mike Barnett. In Verified Software: Theories, Tools, Experiments, VSTTE 2008. The BoogiePL files can be found here and in the Microsoft Tech Report.

An admissible second order frame rule in region logic, Mar 2008, Stevens CS TR-2008-02. Superseded by Local Reasoning for Global Invariants, Part II: Dynamic Boundaries (see above)

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. Superseded by Local Reasoning for Global Invariants, Part I: Region Logic (see above).

Modular Verification of Higher-Order Methods with Mandatory Calls Specified by Model Programs, with Steve M. Shaner and Gary T. Leavens. In Object Oriented Programming, Languages, and Systems OOPSLA 2007. (Iowa State University TR-07-04). Awarded Best Student Paper.

On assertion-based encapsulation for object invariants and simulations, Formal Aspects of Computing 19(2) 2007, 205–224. Supersedes my position paper in VSTTE 2005.

Preliminary Definition of Core JML, Sept 2006, with Gary T. Leavens and Stan Rosenberg. (Stevens Institute of Technology CS Report 2006-07, revised.) See also the PVS source files.

Allowing State Changes in Specifications, with Mike Barnett, Wolfram Schulte, and Qi Sun. Invited paper in International Conference on Emerging Trends in Information and Communication Security, 2006.

Observational purity and encapsulation, Theoretical Computer Science 376 (2007) 205–224. This supersedes the version that 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.

Towards imperative modules: Reasoning about invariants and sharing of mutable state, with Mike Barnett. In Theoretical Computer Science 365 (2006) 143–168. This supersedes the version in LICS 2004.

Assertion-based encapsulation, invariants and simulations, July 2005 (survey paper, in proceedings of Formal Methods for Components and Objects FMCO 2004.

Verifying a secure information flow analyzer, In Theorem Proving in Higher Order Logics (TPHOLS), 211–226, 2005. Here are the PVS files and tech report.

Friends need a bit more: Maintaining invariants over shared state , with Mike Barnett. In Mathematics of Program Construction MPC 2004.

On a specification-oriented model for object-orientation, with Ana Cavalcanti. Proceedings of Sixth Brazilian Symposium on Programming Languages, 114–127 (2002).

Predicate transformer semantics of a higher order imperative language with record subtypes, Science of Computer Programming 41, 1 (2001) 1-51.

Calculating Sharp Adaptation Rules, Information Processing Letters 7 (2000) 201-208.

A Weakest Precondition Semantics for Refinement of Object-oriented Programs, with Ana Cavalcanti. In IEEE Transactions on Software Engineering 26, 8 (2000) 713-728. There is an Extended Version, SIT Report 99-03.

1.4  Algebra of higher order imperative programs

Towards patterns, heaps and imperative lambdas, Journal of Logical and Algebraic Methods in Programming 85 (2016) 1038–1056.

Ideal models for pointwise relational and state-free imperative programming. Proceedings of ACM Principles and Practice of Declarative Programming (2001) 4–15.

Beyond Fun: order and membership in polytypic imperative programming, Proceedings of Mathematics of Program Construction, LNCS 1442 (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 categorical model of higher order imperative programming, Mathematical Structures in Computer Science 8, 4 (1998) 351–399. (Here is a preprint).

Predicate transformers and higher order programs, Theoretical Computer Science 150 (1995) 111–159. (Here is a preprint).

A recursion theorem for predicate transformers on inductive data types, Information Processing Letters 50 (1994) 329-336 (Here is a preprint.)

Two-categories and program structure, PhD thesis 1992.

1.5  Ad hoc networking, music performance, education, software engineering, etc.

ModelWizard: Toward Interactive Model Construction, Masters Thesis by Dylan Hutchison.

CodeBLUE: a Bluetooth interactive dance club system, with Dennis Hromin, Michael Chladil, Natalie Vanatta, Susanne Wetzel, Farooq Anjum, and Ravi Jain. In IEEE Global Telecommunications Conference GLOBECOM (2003) 2814–2818.

High assurance for interactive applications in ad hoc networks, with Susanne Wetzel. Proceedings of First International Workshop on Wireless Security Technologies, London, April 2003.

codeBLUE: a Bluetooth interactive dance club system, May 2002 (with Dennis Hromin, Michael Chladil, Natalie Vanatta, Farooq Anjum, and Ravi Jain). SIT Report 2002-1.

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).

A categorical algebra of programs, course module in Proceedings of Workshop on Teaching Formal Methods to Undergraduates 1994.

A common sense management model, IEEE Software, Nov. 1991 (with R.T. Yeh et al.)

2  Papers chronologically, including superseded conference versions etc.

By chronology I mean publication date.

2.1  Journal articles

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, with Ana Cavalcanti. In IEEE Transactions on Software Engineering 26, 8 (2000) 713-728. There is an Extended Version, SIT Report 99-03.

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 our POPL 2002 paper, 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, with Anindya Banerjee. In Journal of Functional Programming (2005) 15(2) 131–177, special issue on Language Based Security. This supersedes our CSFW 2002 and CSFW 2003 papers.

Towards imperative modules: Reasoning about invariants and sharing of mutable state, with Mike Barnett. In Theoretical Computer Science 365 (2006) 143–168. This supersedes the version in LICS 2004.

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.

Refactoring and representation independence for class hierarchies, with Leila Silva and Augusto Sampaio. Theoretical Computer Science 433 (2012) 60–97. This supersedes our FTfJP 2010 paper.

Local Reasoning for Global Invariants, Part I: Region Logic, with Anindya Banerjee and Stan Rosenberg. In Journal of the ACM 60 (2013) 18:1–18:56. . (This version has an index of definitions and differs by slight copy-edits from the published version.)

Local Reasoning for Global Invariants, Part II: Dynamic Boundaries, with Anindya Banerjee. In Journal of the ACM 60 (2013) 19:1–19:73. (This version has an index of definitions and differs by slight copy-edits from the published version.)

Guiding a General-Purpose C Verifier to Prove Cryptographic Protocols, with François Dupressoir, Andrew D. Gordon, and Jan Jürjens. In Journal of Computer Security 22 (2014) 823-866.

Behavioral Subtyping, Specification Inheritance, and Modular Reasoning, with Gary Leavens. In ACM Transactions on Programming Languages and Systems 47(4) 13:1–13:88, 2015. Supersedes Iowa State tech reports TR-06-36 and TR-06-20 and U. of Central Florida CS-TR-13-03a.

Towards patterns, heaps and imperative lambdas, Journal of Logical and Algebraic Methods in Programming 85 (2016) 1038–1056.

2.2  Articles in conference proceedings

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, with Ana Cavalcanti. Proceedings of Formal Methods Europe FME’2002, LNCS 2391, 471–490. There is an Extended Version, SIT Report 2001-4.

On a specification-oriented model for object-orientation, with Ana Cavalcanti. Proceedings of Sixth Brazilian Symposium on Programming Languages, 114–127 (2002).

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, with Dennis Hromin, Michael Chladil, Natalie Vanatta, Susanne Wetzel, Farooq Anjum, and Ravi Jain. In IEEE Global Telecommunications Conference GLOBECOM (2003) 2814–2818.

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 , with Mike Barnett. In Mathematics of Program Construction MPC 2004.

Modular and constraint-based information flow inference for an object-oriented language, with Qi Sun and Anindya Banerjee. In 11th International Static Analysis Symposium SAS 2004.

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, with Anindya Banerjee. In ECOOP 2005, 387–411.

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, with Mike Barnett, Wolfram Schulte, and Qi Sun. Invited paper in International Conference on Emerging Trends in Information and Communication Security, 2006.

Category theoretic models of data refinement, with Michael Johnson and John Power. In Electronic Notes in Theoretical Computer Science 225(2) 21–38. Proceedings of Irish Conference on Mathmatical Foundations of Computer Science and Information Technology MFCSIT 2006.

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, 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, with Steve M. Shaner and Gary T. Leavens. In Object Oriented Programming, Languages, and Systems OOPSLA 2007. (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, 339–353.

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. Superseded by Local Reasoning for Global Invariants, Part I: Region Logic (see above).

Boogie Meets Regions: a Verification Experience Report, with Anindya Banerjee and Mike Barnett. In Verified Software: Theories, Tools, Experiments, VSTTE 2008. The BoogiePL files can be found here and in the Microsoft Tech Report.

Dynamic Boundaries: Information Hiding by Second Order Framing with First Order Assertions, with Anindya Banerjee. In Programming Languages and Systems, 19th European Symposium on Programming (ESOP) 2010, invited paper. (The version here corrects a bug in the proceedings and includes appendix.)

Information Flow Monitor Inlining, with Andrey Chudnov. In IEEE Computer Security Foundations Symposium, July 2010, 200–214. See also slightly older version with proofs.

Local Reasoning and Dynamic Framing for the Composite Pattern and its Clients, with Stan Rosenberg and Anindya Banerjee. In Verified Software: Theories, Tools, Experiments, VSTTE 2010, LNCS 6217, pages 183–198.

Guiding a General-Purpose C Verifier to Prove Cryptographic Protocols, with François Dupressoir, Andrew D. Gordon, and Jan Jürjens. In IEEE Computer Security Foundations Symposium, July 2011. Extended version as Microsoft MSR–TR–2011–50.

Symbolic Analysis for Security of Roaming Protocols in Mobile Networks [Extended Abstract], with Chunyu Tang and Susanne Wetzel. In 7th International ICST Conference on Security and Privacy in Communication Networks (SecureComm), Sept 2011.

Decision Procedures for Region Logic, with Anindya Banerjee and Stan Rosenberg. In 13th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), January 2012, LNCS 7148, 379–395.

Laws of Programming for References, with Giovanny Lucero and Augusto Sampaio. In 11th Asian Symposium on Programming Languages and Systems (APLAS 2013) LNCS 8301, 124–139.

Analysis of authentication and key establishment in inter-generational mobile telephony (long version), with Chunyu Tang and Susanne Wetzel. To appear in the 4th International Symposium on Trust, Security and Privacy for Emerging Applications (TSP 2013).

Information flow monitoring as abstract interpretation for relational logic, with Andrey Chudnov and George Kuan. In IEEE Computer Security Foundations Symposium 2014.

A Logical Analysis of Framing for Specifications with Pure Method Calls, with Anindya Banerjee. In Verified Software: Theories, Tools, Experiments (VSTTE) 2014, post-proceedings, LNCS 8471.

Inlined information flow monitoring for JavaScript, with Andrey Chudnov. In ACM Conference on Computer and Communication Security (2015) 629–643.

Calculational design of information flow monitors, with Mounir Assaf. In IEEE Computer Security Foundations Symposium (2016) 210–224.

Specifying and verifying advanced control features, with Gary T. Leavens, Hridesh Rajan, Tomoyuki Aotani. In 7th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (2016) LNCS 9953, 80–96.

Relational Logic with Framing and Hypotheses, with Anindya Banerjee and Mohammad Nikouei. In 36th Conference on Foundations of Software Technology and Theoretical Computer Science (2016) 11:1–11:16. Technical report on arXiv.

Hypercollecting semantics and its application to static analysis of information flow, with Mounir Assaf, Julien Signoles, Éric Totel, and Frédéric Tronel). In 44th ACM Symposium on Principles of Programming Languages (2017).

Spartan Jester: end-to-end information flow control for hybrid Android applications, with Julian Sexton and Andrey Chudnov. In Mobile Security Technologies workshop (2017) to appear.

2.3  Book chapters

State Based Encapsulation for Modular Reasoning about Behavior-Preserving Refactorings, with Anindya Banerjee. Invited chapter in Aliasing in Object-oriented Programming, Dave Clarke and James Noble and Tobias Wrigstad, eds., Springer State-of-the-art Surveys, 2012.

A Simple Semantics and Static Analysis for Stack Inspection, with Anindya Banerjee. In Semantics, Abstract Interpretation, and Reasoning about Programs: Essays Dedicated to David A. Schmidt on the Occasion of his Sixtieth Birthday, EPTCS 129, September 2013, 284–308. (DOI: 10.4204/EPTCS.129, ISSN: 2075-2180, link).

2.4  Articles in refereed workshop proceedings

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, with Susanne Wetzel. Proceedings of First International Workshop on Wireless Security Technologies, London, April 2003.

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.

Refactoring and representation independence for class hierarchies [extended abstract], with Leila Silva and Augusto Sampaio. In the 12th ECOOP Workshop on Formal Techniques for Java-like Programs, June 2010.

2.5  Unpublished and Technical Reports

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 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)

Behavioral Subtyping, Specification Inheritance, and Modular Reasoning, July 2006, with Gary Leavens (Iowa State University TR-06-20). Superseded by U. Central Florida CS-TR-13-03a.

Preliminary Definition of Core JML, Sept 2006, with Gary T. Leavens and Stan Rosenberg. (Stevens Institute of Technology CS Report 2006-07, revised.) 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. Superseded by U. Central Florida CS-TR-13-03a.

* Expressive declassification policies and modular static enforcement, with Anindya Banerjee and Stan Rosenberg, Stevens CS TR-2007-04. A version appears 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.

Theory for Software Verification —DRAFT, Jan 2009.

Behavioral Subtyping, Specification Inheritance, and Modular Reasoning, with Gary Leavens. University of Central Florida CS-TR-13-03a, July 2013. Supersedes Iowa State tech reports TR-06-36 and TR-06-20.

A Logical Analysis of Framing for Specifications with Pure Method Calls, with Anindya Banerjee and Mohammad Nikouei, submitted for publication 2015. Supersedes A Logical Analysis of Framing for Specifications with Pure Method Calls, with Anindya Banerjee, in Verified Software: Theories, Tools, Experiments (VSTTE) 2014, post-proceedings, LNCS 8471.

2.6  Dissertation

Two-categories and program structure, PhD thesis 1992.

3  Software

The SecJ Secure Information Flow Inferencer, developed by my PhD student Qi Sun.

The VERL Verifier for Region Logic developed by my PhD student Stan Rosenberg.

Modeling and Analysis of Mobile Telephony Protocols developed by my PhD student Chunyu Tang.

The JEST JavaScript Information Flow Monitor developed by my PhD student Andrey Chudnov.

4  Edited collections

Proceedings of the ACM SIGPLAN Fourth Workshop on Programming Languages and Analysis for Security, 2009, Dublin, Ireland. Co-editor with Stephen Chong. Published by ACM Press, 131 pages, ISBN 978-1-60558-645-8

VSTTE (Verified Software: Theories, Tools, Experiments) 2010 Workshop Proceedings Co-editor with Rajeev Joshi (NASA), Tiziana Margaria (Potsdam), Peter Müller (ETH Zurich), and Hongseok Yang (U. London). Technical Reports 676, ETH Zurich, Computer Science.

Formal Methods: Foundations and Applications – Proceedings of 15th Brazilian Symposium, 2012. Co-editor with Rohit Gheyi. Springer Lecture Notes in Computer Science volume 7498.

5th International Symposium on Unifying Theories of Programming (UTP 2014), Revised Selected Papers. Editor. Springer Lecture Notes in Computer Science volume 8963.

5  Miscellaneous talks not linked with papers above (incomplete list)

Naïve and flexible declassification with scalable enforcement, at The Open Group, Real-Time Embedded Systems Forum, San Diego, 2 Feb 2009.

Verification of Object-oriented Programs, seven hours of lectures for ITU Copenhagen First Fall PhD School on Logics and Types for State, 2008.

Use auxiliary state to express modular structure, at ETAPS 2005 Grand Challenge Workshop on Software Verification, Edinburgh, 3 April 2005.

Assertion based encapsulation and refinement of classes, at Formal Methods for Components and Objects, Leiden NL, 4 Nov 2004.

Towards imperative modules, at the New Jersey Programming Languages Seminar, Princeton, 1 Oct 2004.

Reasoning about modules: data refinement and simulation, at the Java Verification Workshop in conjunction with POPL 2002.

Java, Access Control, and Static Analysis, at the NJITES Symposium on Cyber Security and Trustworthy Software, March 15, 2002.

Invited talk at 2002 Brazilian Symposium on Programming Languages on talk on confinement and abstraction.

NJ Programming Languages Seminar 10/10/02 confinement and representation independence.

6  Acknowledgment of support

My recent work has been partially supported by NSF awards INT-9813854, CCR-0208984, CCF-0429894, CNS-0627338, CNS-0708330, CCF-0915611, CNS-1228930, and CCF-1649884. US Department of Homeland Security; Microsoft Research Redmond; Microsoft Research Cambridge; a visiting fellowship from the Swedish Emergency Management Agency; a grant from the New Jersey Commission on Science and Technology; a Visiting Fellowship at SRI International (NSF CCR-ITR-0326540, ONR N00014-01-1-0837); a visiting professorship at IMDEA Software, Madrid.

7  Copyright Notice

To satisfy the conditions of certain publishers regarding distribution of my papers on the web, I have been asked to include the following:

This material is presented to ensure timely disemination of scholarly and technical work. Copyright and all rights therein are maintained by the authors or by other copyright holders, notwithstanding that they have offered their works here electronically. All persons copying this information are expected to adhere to the terms and constraints invoked by each author’s copyright. In most cases, these works may not be reposted without the explicit written permission of thecopyright holder.
Naumann publications          Revision: 1.8 , Date: 2017/03/20 03:33:01
This document was translated from LATEX by HEVEA.