Kathi Fisler's Publications

Kathi Fisler

Publications

Policy Analysis and Authoring [Active Area]

Embracing Policy Engineering. Kathi Fisler, Shriram Krishnamurthi, and Daniel J. Dougherty. NSF/FSE Workshop on the Future of Software Engineering, Nov 2010.
The Margrave Tool for Firewall Analysis. Timothy Nelson, Christopher Barratt, Daniel J. Dougherty, Kathi Fisler, Shriram Krishnamurthi. Usenix Large System Administration Conference (LISA) 2010.
A Model of Triangulating Environments for Policy Authoring. Kathi Fisler, Shriram Krishnamurthi. ACM Symposium on Access Control Models and Technologies, July 2010.
Escape From the Matrix: Lessons From a Case Study in Access-Control Requirements. Kathi Fisler and Shriram Krishnamurthi. Symposium on Usable Security and Privacy (SOUPS) Poster Session. July 2009. (full technical report version)
Obligations and their Interaction with Programs. Daniel J. Dougherty, Kathi Fisler, and Shriram Krishnamurthi. European Symposium on Research in Computer Security (ESORICS), September 2007.
Specifying and Reasoning about Dynamic Access Control Policies. Daniel J. Dougherty, Kathi Fisler, and Shriram Krishnamurthi. International Joint Conference on Automated Reasoning (IJCAR), August 2006.
Verification and Change Impact Analysis of Access-Control Policies. Kathi Fisler, Shriram Krishnamurthi, Leo Meyerovich, and Michael Tschantz. International Conference on Software Engineering (ICSE), May 2005.

User-studies and Development of Programming Environments for Novices [Active Area]

Mind Your Language: On Novices' Interactions with Error Messages. Guillaume Marceau, Kathi Fisler, and Shriram Krishnamurthi. OOPSLA Onward 2011.
Do Values Grow on Trees?: Expression Integrity in Functional Programing. Guillaume Marceau, Kathi Fisler, and Shriram Krishnamurthi. ICER 2011 Discussion Paper.
WeScheme: The Browser is Your Programming Environment. Danny Yoo, Emmanuel Schanzer, Shriram Krishnamurthi, and Kathi Fisler. ITiCSE 2011.
Measuring the Effectiveness of Error Messages Designed for Novice Programmers. Guillaume Marceau, Kathi Fisler, Shriram Krishnamurthi. (Follow link for comparison to Scheme Workshop '10 paper) ACM SIGCSE 2011. Best Paper Award
Measuring the Effectiveness of Error Messages Designed for Novice Programmers. Guillaume Marceau, Kathi Fisler, Shriram Krishnamurthi. Scheme Workshop 2010.

Synthesizing APIs from Relational Specifications [Active Area]

Towards An Operational Semantics for Alloy. Daniel J. Dougherty, Shriram Krishnamurthi, Kathi Fisler, and Theophilos Giannakopoulos. International Conference on Formal Methods (FM). November 2009.
Alchemy: Transmuting Base Alloy Specifications into Implementations. Shriram Krishnamurthi, Daniel J. Dougherty, Kathi Fisler, and Daniel Yoo. International Conference on Foundations of Software Engineering (FSE). November 2008.

Timing Diagrams (Diagrammatic Reasoning and Formal Methods)

Two-Dimensional Regular Expressions for Compositional Bus Protocols (short paper). Kathi Fisler. International Conference on Formal Methods in Computer-Aided Design (FMCAD). November 2007.
Temporal Modalities for Concisely Capturing Timing Diagrams. With Hana Chockler. CHARME 2005.
Towards Diagrammability and Efficiency in Event Sequence Languages. CHARME 2003. Journal version accepted to Software Tools for Technology Transfer, 2005.
Diagrams and Computational Efficacy. In Words, Proofs, and Diagrams, Dave Barker-Plummer, David I. Beaver, Johan van Benthem, and Patrick Scotto di Luzio, editors. CSLI Publications, 2002.
On Tableau Constructions for Timing Diagrams. NASA Langley Workshop on Formal Methods, June 2000.
Timing Diagrams: Formalization and Algorithmic Verification. Journal of Logic, Language, and Information; volume 8, number 3, July 1999.
Containment of Regular Languages in Non-Regular Timing Diagram Languages is Decidable. Proceedings of CAV '97, LNCS, June 1997.
A Unified Approach to Hardware Verification Through a Heterogeneous Logic of Design Diagrams. PhD Dissertation. Indiana University Department of Computer Science, August 1996 (abstract, full dissertation postscript)
Visualizing System Language Relationships with Logic. CADE '96 workshop on Visual Reasoning, July 1996.
Exploiting the Potential of Diagrams in Guiding Hardware Reasoning. In Logical Reasoning with Diagrams, edited by Gerard Allwein and Jon Barwise, Oxford University Press, 1996.
Integrating Design and Verification Environments Through a Logic Supporting Hardware Diagrams. With Steven D. Johnson. CHDL '95, June 1995.
A Canonical Form for Circuit Diagrams. Indiana University Technical Report 432, May 1995.
A Logical Formalization of Hardware Design Diagrams. Indiana University Technical Report 416. September 1994.
Extending Formal Reasoning with Support for Hardware Diagrams. TPCD '94, September 1994.

Aspect-Oriented Verification

Foundations of Incremental Aspect Model-Checking. Shriram Krishnamurthi and Kathi Fisler. Accepted for publication in TOSEM. June 2006.
Verifying Aspect Advice Modularly. Shriram Krishnamurthi, Kathi Fisler, and Michael Greenberg. International Conference on Foundations of Software Engineering (FSE). November 2004.

Feature-Oriented Verification

Decomposing Verification Around End-Users Features. Kathi Fisler and Shriram Krishnamurthi. IFIP Working Conference on Verified Software: Theories, Tools, Experiments, 2005.
A Case Study in Using ACL2 for Feature-Oriented Verification. Kathi Fisler and Brian Roberts. Proceedings of the ACL2 Workshop. November 2004.
Parameterized Interfaces for Open System Verification of Product Lines. Colin Blundell, Kathi Fisler, Shriram Krishnamurthi, and Pascal Van Hentenryck. International Conference on Automated Software Engineering (ASE). September 2004.
Modular Verification of Open Features Through Three-Valued Model Checking. Harry Li, Shriram Krishnamurthi and Kathi Fisler. Accepted to the Journal of Automated Software Engineering, July 2003.
Verifying Cross-Cutting Features as Open Systems. Harry Li, Shriram Krishnamurthi and Kathi Fisler. International Conference on Foundations of Software Engineering. November 2002.
Interfaces for Modular Feature Verification. Harry Li, Shriram Krishnamurthi and Kathi Fisler. International Conference on Automated Software Engineering. September 2002.
The Influence of Software Module Systems on Modular Verification. Harry Li, Kathi Fisler, and Shriram Krishnamurthi. 9th International SPIN Workshop on Model Checking of Software. April 2002.
Modular Verification of Collaboration-Based Soft/ware Designs. With Shriram Krishnamurthi. International Conference on Foundations of Software Engineering. September 2001. (full technical report version)
A Model Checking Framework for Layered Command and Control Software. With Shriram Krishnamurthi, Don Batory, and Jia Liu. Monterey Workshop on Software Engineering, June 2001.
Verifying Component-Based Collaboration Designs. With Shriram Krishnamurthi and Don Batory. 4th ICSE Workshop on Component-Based Software Engineering: Component Certification and System Prediction, May 2001.

General Computer-Aided Verification

Bisimulation and Model Checking. With Moshe Y. Vardi. Formal Methods in System Design, 2002. Short version presented at Conference on Correct Hardware Reasoning Methods (CHARME) 1999. (full technical report version).
Is There a Best Symbolic Cycle-Detection Algorithm? With Ranan Fraer, Gila Kamhi, Moshe Y. Vardi and Zijiang Yang. Proceedings of TACAS 2001, April 2001.
Bisimulation Minimization in an Automata-Theoretic Verification Framework. With Moshe Y. Vardi. Proceedings of the Conference on Formal Methods in Computer-Aided Design (FMCAD), 1998. (full technical report version)
Testing the FormalCheck Query Library. S. Dershowitz, K. Fisler, S. K. Shukla, G.J. Holzmann, R.P. Kurshan, and D. Peled. Proceedings of LCET 96, Vol. 14, pp. 173-176, Lucent Technologies, 1997.

Software Engineering Issues

Implementing Extensible Theorem Provers. With Shriram Krishnamurthi and Kathryn E. Gray. Theorem Proving in Higher-Order Logics: Emerging Trends. INRIA Research Report, September 1999.

Verification in Practice

Modelling and Model Checking a Shared Memory Consistency Protocol. With Claude Girault. International Conference on Applications and Theory of Petri Nets, 1998.
Verifying VHDL Designs with COSPAN. With R.P. Kurshan. In Formal Hardware Verification: Methods and Systems in Comparison, Thomas Kropf, ed, Springer Verlag Lecture Notes in Computer Science 1287, 1997.
Verification Using Abstractions, Reductions, and Decompositions: A Case Study in COSPAN. Unpublished report, 1996.
Using COSPAN to Partially Verify and Debug a Barcode Reader. AT&T Bell Laboratories Technical Memorandum, December 1995.

Teaching Issues

CounterMeasures: A Game for Teaching Computer Security. Craig Jordan, Matt Knapp, Dan Mitchell, Mark Claypool, and Kathi Fisler. NetGames 2011 [WPI MQP project]
"Little Language" Project Modules. With John Clements. Journal of Functional Programming Educational Pearl. January 2010.
Teaching Reasoning Using Heterogeneous Logic. With Jon Barwise and Ruth Eberle. Presented at DIMACS workshop on Teaching Logic in an Illogical World, July 1996.