UCSC Design and Verification Lab

This Wiki is the home page of the Design and Verification Lab at the School of Engineering, University of California, Santa Cruz. It can be reached via HTTP or (preferably) HTTPS. The lab is located in Room 307 of the Engineering 2 Building (directions).

Tools

• Ticc: Tool for Interface Compatibility and Composition. Ticc is a tool that allows to model design components, verify their behavior, and verify their compatibility in a design.

• Direct: Directed Testing of Embedded Software. Direct is an infrastructure that can be used to do testing and explore coverage of multi-threaded embedded software.

Research

Our main research directions are the following:

• Game theory. In the past, we have worked at the theory of zero-sum repeated games, with applications to system design, verification, and control. More recently, our interests in game theory are growing broader.

• Games as component models. We argue that games provide the natural model for open systems, or systems that interact with their environment. We are developing a theory in which the component of a design are modeled as games. The theory enables the verification of the functionality and compatibility of the components, as well as the synthesis of controllers and schedulers. Our tool Ticc implements some of these ideas.

• Embedded software synthesis. Embedded software is difficult to design: software components compete for resources, time, device access, and memory, making their composition into a design difficult. We are developing an approach that facilitates the composition of embedded software components. The approach relies on the use of game theory to model component interaction.

• Quantitative systems theory. The traditional setting for system verification is boolean: both verification questions (is a system correct?) and refinement questions (can this component be substited by another?) are answered in yes/no fashion. We are developing a quantitative theory of system properties and relations, where we can quantify how well a system meets a specification, and how similar the behavior of two systems is.

• Techniques for system design and verification. We are interested in techniques for the design and verification of digital and embedded systems.

Of course, these are only the established research directions. There is work also on new topics, but... we can't tell you just yet!

Publications

There is no single repository of the publications of the Design and Verification Lab. Rather, the publications are available from the home pages of the authors. Some of these pages are linked below:

• Luca de Alfaro's publications

Other Software

• Robos: Our version of the BrickOS/LegOS operating system

• blifmv-to-rm.tgz: A translator from BLIF-MV to the input language of c-Mocha.

People

Resources

• Wikis - How to access all the Dvlab wikis
  

• How to edit the Dvlab Wiki