## page was renamed from Dvlab Open Wiki
## page was renamed from FrontPage
#format wiki
#language en
#pragma section-numbers off

= UCSC Design and Verification Lab =

This Wiki is the home page of the '''Design and Verification Lab''' 
at the [http://www.soe.ucsc.edu School of Engineering], [http://www.ucsc.edu/ University of California, Santa Cruz]. 
It can be reached via [wiki:DvlabHttpWiki/ HTTP] or (preferably) [wiki:DvlabWiki/ HTTPS].
The lab is located in Room 307 of the Engineering 2 Building
([http://www.soe.ucsc.edu/general/directions/school.html directions]). 

== Tools ==

 * {*} '''[:Ticc: 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: 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: 

 * [wiki:LucaHome/Publications Luca de Alfaro's publications]

== Other Software ==

 * '''[wiki:LucaHome/Robos Robos]:''' ''Our version of the BrickOS/LegOS operating system'' 
 * '''[attachment:blifmv-to-rm.tgz blifmv-to-rm.tgz]:''' ''A translator from [http://vlsi.colorado.edu/~vis/doc/blifmv/blifmv/blifmv.html BLIF-MV] to the input language of [http://embedded.eecs.berkeley.edu/research/mocha/ c-Mocha].'' 

= People =

[[Include(People)]]

= Resources =

 * ["Wikis"] - How to access all the Dvlab wikis [[BR]]
 * ["How to edit the Dvlab Wiki"]