Verification Techniques for New Styles of Software Composition
Software engineers often precede language theoreticians. The past decade has seen a spate of proposals for new forms of software composition, with names like "mixin layers," "hyperslices," "aspects," and so on. These proposals have emerged from a concrete need felt in the process of trying to build, deploy, maintain and re-deploy software systems. While programming language theory has fallen behind these results, the semi-formal presentations of these modularity mechanisms offer enough of a basis to enable progress on other fronts.
While each new development technology is exciting, I believe we cannot consider one mature until it provides comprehensive support for software development: programming, testing, editing, compilation, verification, etc. While we have investigated many of these issues, in this slice of work we're focused on formal verification. Of the many verification techniques, we have found model checking an especially good fit with many of the properties we have encountered in our case studies.
Project status: Active
Research Areas
People
| Shriram Krishnamurthi |
Publications
Fisler, K., and Krishnamurthi, S. Decomposing Verification by Features. In Proceedings of the International Federation for Information Processing (IFIP) Working Conference on Verified Software: Theories, Tools, Experiments. Springer-Verlag, 2006. [ home ]
Li, H. C., Krishnamurthi, S., and Fisler, K. Modular Verification of Open Features Through Three-Valued Model Checking. Automated Software Engineering Journal 12, 3 (Jul 2005), 349-382. [ home ]
Blundell, C., Fisler, K., Krishnamurthi, S., and Van Hentenryck, P. Parameterized Interfaces for Open System Verification of Product Lines. In Proceedings of the IEEE International Symposium on Automated Software Engineering (Sep 2004), pp. 258-267. [ home | pdf ]
Krishnamurthi, S., Fisler, K., and Greenberg, M. Verifying Aspect Advice Modularly. In Proceedings of the ACM Special Interest Group on Software Engineering SIGSOFT International Symposium on the Foundations of Software Engineering (Nov 2004), pp. 137-146. [ home ]
Li, H. C., Krishnamurthi, S., and Fisler, K. Interfaces for Modular Feature Verification. In Proceedings of the IEEE International Symposium on Automated Software Engineering (Sep 2002), pp. 195-204. [ home ]
Li, H. C., Fisler, K., and Krishnamurthi, S. The Influence of Software Module Systems on Modular Verification. In Proceedings of the SPIN Workshop on Software Model Checking (Apr 2002), pp. 60-78. [ home ]
Li, H. C., Krishnamurthi, S., and Fisler, K. Verifying Cross-Cutting Features as Open Systems. In Proceedings of the ACM Special Interest Group on Software Engineering (SIGSOFT) International Symposium on the Foundations of Software Engineering (Nov 2002), pp. 89-98. [ home ]
Fisler, K., Krishnamurthi, S., and Batory, D. S. Verifying Component-Based Collaboration Designs. In Proceedings of the International Conference on Software Engineering (ICSE) Workshop on Component-Based Software Engineering (May 2001). [ home ]
Fisler, K., Krishnamurthi, S., Batory, D. S., and Liu, J. A Model Checking Framework for Layered Command and Control Software. In Proceedings of the Monterey Workshop on Engineering Automation for Software Intensive System Integration (Jun 2001), pp. 63-76.
Fisler, K., and Krishnamurthi, S. Modular Verification of Collaboration-Based Software Designs. In Proceedings of the Joint European Software Engineering Conference and ACM Special Interest Group on Software Engineering (SIGSOFT) Symposium on the Foundations of Software Engineering (Sep 2001), pp. 152-163. [ home ]
Krishnamurthi, S., Fisler, K., and Batory, D. Scalable Composition, Evolution and Verification Through Feature-Oriented Programming. In Proceedings of the Workshop on New Visions for Software Design and Productivity: Research and Applications (Dec 2001).
| Page Owner: Webmaster | Last Modified: Mon Oct 23 14:57:09 2006 |