Validation Support for Lightweight Languages
Hackers precede language theoreticians. We are seeing a flood of novel and innovative programming languages within various specific domains. Because they arise out of specific needs, however, they are often designed by people without traditional language design expertise, and implemented by people without traditional programming environment expertise. As a result, they present numerous opportunities for people with programming language analysis experience. What makes these languages exciting is that they are actually being used by developers, so results can both be deployed rapidly and will quickly garner useful feedback. Here are two examples:
I am especially fond of spreadsheets. Their constrained shape seems to be a structuring aid in many domains; in any case, it provides automatic naming, which reduces some of the (initial) burden on the spreadsheet author. The dominant spreadsheet, Excel, is rich in features but unfortunately poor in support for spreadsheet validation. We have, building on prior work, developed a novel type system whose types are the names of spreadsheet headers. Furthermore, because most spreadsheet data are numeric, we have also built a system for checking units.
I have also been working on two problems related to XACML, a standardized declarative language for access-control specifications. The first problem is the validation of policies against a set of known properties. Moreover, developers often do not have properties; all they have is a prior version of the policy that seemed to work correctly, and a new version with some changes applied. To support this important case-use, we also implement change impact analysis, which summarizes the semantic (as opposed to syntactic) changes to a policy. Happily, the outcome of this analysis can itself be treated as a source for verification, enabling a very elegant, lightweight formal methods technique.
Project status: Active
Research Areas
People
| Shriram Krishnamurthi |
Publications
Fisler, K., Krishnamurthi, S., Meyerovich, L. A., and Tschantz, M. C. Verification and Change-Impact Analysis of Access-Control Policies. In Proceedings of the International Conference on Software Engineering (May 2005), pp. 196-205. [ home ]
Antoniu, T., Steckler, P. A., Krishnamurthi, S., Neuwirth, E., and Felleisen, M. Validating the Unit Correctness of Spreadsheet Programs. In Proceedings of the International Conference on Software Engineering (May 2004), pp. 439-448. [ home ]
Ahmad, Y., Antoniu, T., Goldwater, S., and Krishnamurthi, S. A Type System for Statically Detecting Spreadsheet Errors. In Proceedings of the IEEE International Symposium on Automated Software Engineering (Oct 2003), pp. 174-183. [ home ]
| Page Owner: Webmaster | Last Modified: Mon Oct 23 14:57:09 2006 |