Research Areas

Design Space Exploration – Design space exploration (DSE) is the process of enumerating and ranking completions of partial system design descriptions while satisfying a (possibly huge) number of design constraints with complex interdependencies. Because of those interdependencies, system architects must consider all design constraints very early in the system design process to ensure a proposed system architecture will eventually lead to an implementation satisfying all requirements. DSE helps architects in evaluating design alternatives and choosing an appropriate architecture. Mathematically, DSE can be considered a constraint satisfaction problem. The tool FORMULA uses constraint logic programming (CLP) and satisfiability modulo theories (SMT) to solve those kinds of problems.

Software Verification – EMIC’s software verification efforts are focused on the development and application of a “Verifier for Concurrent C (VCC)”. VCC is a tool that proves correctness of annotated concurrent C programs or finds problems in them. In contrast to testing, verifying a piece of code establishes its correctness for all possible inputs and execution paths (100% coverage), which is particularly helpful for complex concurrent code where it is very hard to establish acceptable coverage with testing. VCC extends C with design by contract features, like pre- and post-conditions as well as type invariants. Today, VCC is the only verifier for C that works function- and thread-modular, which means that it scales to large code bases independently of the number of functions or threads. VCC annotations are transparent to a C compiler. They do not change the compiled code and therefore do not impact runtime behavior.

Application Domains

Embedded Systems – Modern embedded systems, such as the control system in a vehicle or the control of production processes in a factory, are distributed communicating systems whose sensors, actuators and computing nodes provide increasingly complex functionality. Moreover, these systems have to meet tight non-functional requirements in terms of their real-time behavior, memory footprint, or energy consumption. DSE helps to design those systems with better quality, fewer design iterations, and increased cost-effectiveness.

IT Management – Managing IT infrastructures requires keeping the software and configurations of hundreds or thousands of computing devices in sync – ranging from servers to PCs to smart phones or a host of embedded devices. IT administrators must match user requirements with corporate requirements and technological constraints to determine which version of what software must be installed and how it must be configured on a particular device. DSE helps administrators to makes sense of those different constraints, make smart decisions from among the myriad of different configuration options and keep their infrastructure in a healthy state.

Operating Systems and Data Base Systems – Operating systems stopped being single threaded 20 years ago. Today, they are extremely complex pieces of concurrent software that extensively use the features of the underlying hardware to execute quickly and securely. Because of this complexity, it is increasingly difficult and costly to assure the desired quality of operating system code by testing. Formal verification is an alternative that today, after more than 30 years of research, approaches practical viability. VCC has been used to verify the core of Microsoft’s hardware virtualization solution Hyper-V, which consists of 100,000 lines of concurrent C code. Similarly, data base systems face extreme performance requirements. To address those requirements, they use very aggressive optimizations, such as lock-free algorithms in transaction kernels. These algorithms are very complex and difficult to debug. Again, formal verification with VCC can establish the correctness of the implementation and prove that not only the algorithm but also its implementation is safe.