Synthesizing APIs from Relational Specifications [Active Area]

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

Analyzing Access-Control Policies [Active Area]

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

Timing Diagrams (Diagrammatic Reasoning and Formal Methods) [Active Area]

• 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

• Teaching Reasoning Using Heterogeneous Logic. With Jon Barwise and Ruth Eberle. Presented at DIMACS workshop on Teaching Logic in an Illogical World, July 1996.