Seminars

Developing correct parallel and distributed software is a daunting task. The parallelism causes the state-spaced explosion problem: the number of states in the system grows exponentially with the number of parallel components. One of the ways to verify that such a system satisfies its requirements is model checking.

In this talk, I will describe the application of model checking to two real-world systems, and describe the errors that were uncovered using this approach.

The first system is the session setup protocol that is part of the IEEE 11073-20601:2008 standard for…

For economic reasons, the design and fabrication of semiconductor ICs is increasingly outsourced. This comes at the expense of trust. An untrusted entity, for instance a malicious designer or semiconductor foundry could pirate the design, or worse, maliciously modify it to leak secret information from the chip or sabotage its functionality. In addition, several companies now provide IC reverse engineering services that can reconstruct a manufactured chip's internal design details, thus compromising the designer's IP. Reverse engineering attack's on embedded devices and smart-cards have…

Energy-efficiency is a critical concern in continuously-running mobile applications, such as those for health and context monitoring. An attractive approach to saving energy in such applications is to defer the execution of delay-tolerant op- erations until a time when they would consume less energy. However, introducing delays to save power may have a detri- mental impact on the user experience. To address this prob- lem, we present Tempus, a new approach to managing the trade-off between energy savings and delay. Tempus saves power by enabling programmers to annotate power-hungry…

The realization of complex cyber-physical systems is creating design and verification challenges that will soon become insurmountable with today’s engineering practices. While model-based design tools are already facilitating several design tasks, harnessing the complexity of the Internet-of-Things scenario is only deemed possible within a unifying methodology. This methodology should help interconnect different tools, possibly operating on different system representations, to enable scalable design space exploration and early detection of requirement inconsistencies.

In this talk…

A central goal of artificial intelligence (AI) is to develop algorithms and software that can solve complex problems as a human would. AI is poised to have a significant impact on making discoveries in biomedical big data given the availability of powerful algorithms, visualization methods, and high-performance computing. We introduce here the Exploratory Modeling for Extracting Relationships using Genetic and Evolutionary Navigation Techniques (EMERGENT) algorithm as an AI approach for the large-scale genetic analysis of common human diseases. EMERGENT builds models of genetic variation…