Formal Systems Laboratory at UIUC

Web Page: http://k-framework.org/index.php/ProjectIdeas

Mailing List: http://lists.cs.uiuc.edu/mailman/listinfo/fsl-gsoc

[IMAGE http://mzero.org/images/fsl.png]

The Formal Systems Laboratory (FSL) at the University of Illinois at Urbana-Champaign (UIUC) is a group of researchers and developers aiming to increase the quality of computing systems. We achieve this goal by developing tools and ideas that allow us to precisely determine how software behaves and to verify that software behaves correctly. One such tool is the K framework, a system for easily creating new programming languages and formally defining existing ones. Programs written in a language created or defined in the K framework can be reasoned about rigorously and can be used more confidently in safety-critical systems.

Projects

• Automated test case generation for the K Framework I propose to develop automated test case generation capabilities for the K Framework, allowing test cases to be generated from the specification of languages implemented in K.
• Haskell compiler for K The goal of this project is to provide robust and fast Haskell backend for K framework, which will make it possible to build efficient interpreters from formal definitions of different programming languages.
• HTML/CSS Backend for K The goal of this project is to provide a HTML/CSS-visualizer for the K framework. This would allow to quickly view an elegant summary of any programming language described using K. In the current version of K, this is achieved by compiling the definition using Latex. Creating a webpage rather than using Latex should greatly speed up the creation of the visual representation. The HTML would be generated in Java from the XML-like structures produced by the K tools. Using Javascipt and/or PHP, it would be possible to make the visual representation interactive by offering editing features. Ultimately, this project could be used as debugger. The fast generation of the webpage would allow a developer to directly examine and fix the result of his work in a browser.
• Klint - a lint-like tool for K-framework This project aims to create a stand-alone lint-like tool for K-framework that might be integrated on K compiler frontend.