Concept Inventories

For CS courses I teach

Image from 123RF, copyright Illia Uriadnikov

Definition: A test measuring students knowledge of a set of concepts and also their conceptions and misconceptions.

Concept Inventories exist for some subfields of computer science but are missing for CS2 with its four basic ADTs, Algorithm Analysis, Programming Language Concepts and Compilers.

The Hoist Project

Static Verification of Device Drivers

Image Copyright 2013 Thaddeus B. Kubis,

This project is exploring the use of type safe languages in writing or verifying device drivers. The languages use an advanced type systems to prevent data or IO misuse. Specifically, they only allow a thread to access its own memory, they provide safe concurrency support, and support for pre- and post-conditions to prove other properties about device drivers. The language checks safety at compile time (statically) whenever possible. project has focused on the needs of device drivers since studies have shown that these contain most OS bugs. Our long term goal is to automate static verification of the existing drivers in Linux to prove that they meet all the saftey criteria or pinpoint where they fail.

Formal languages developed in this project include Lambda-low which provides linear access to memory, Lambda-concurrent which adds concurrency support (locks) to Lambda-low, and Laddie (Language for Automated Device Drivers), a specification language for the IO interface used between a driver and a device. A formal language is expressed as a syntax and a type system that run on an abstract machine using a set of evaluation rules. (It has proven properties of soundness: preservation and progress). Formal languages are implemented as concrete languages in order to actually use them.

The formal languages are implemented in concrete languages and actual device driver code has been written in them and run in Linux on a network card. Lambda-low and Lambda-concurrent are implemented in Clay, a C-like imperative language with linear access to memory, arithmetic constraints on function pre- and post-conditions, and concurrency support. After typechecking, Clay compiles to C++/C (user choice). Laddie is implemented as a declarative language which compiles to Clay.

The current phase of this project is a semi-automated translator for existing C drivers to Clay.

Clay Files

Laddie Files Translator from C to Clay (Language name needed) files