Date: November 10, 2009
Time: 9:30AM
Place: FEC 141
Sean M. Brennan
Committee Chair:
Barney Maccabe, Director of the Computer Science and Mathematics Division at Oak Ridge National Laboratory
Committee Members:
Wenbo He, Assistant Professor of Computer Science at UNM
Sudharman Jayaweera, Assistant Professor of Electrical and Computer Engineering at UNM
Michael Cai, Los Alamos National Laboratory
Abstract:
The SENSIX software framework uniquely integrates constraint-dominated
wireless sensor networks with the flexibility of object-oriented
programming models, without violating the principles of either. Though
these two computing paradigms are opposite in many ways, SENSIX bridges
them to yield a dynamic middleware abstraction unifying low-level
resource-aware task reconfiguration and high-level object recomposition.
Through the layered approach of SENSIX, the software developer creates a
domain-specific sensing architecture by merely defining a customized
task specification and utilizing object inheritance. In addition, SENSIX
performs better at large scales (on the order of 1000 nodes or more)
than other sensor network middleware which do not include such unified
facilities for vertical integration.
Date: November 5, 2009
Time: 3:30PM
Place: ME 427
Guanyu Wang
Committee Chair:
Joe Kniss, Assistant Professor of Computer Science at UNM
Committee Members:
Pradeep Sen, Assistant Professor of Electrical and Computer Engineering at UNM
Lance Williams, Associate Professor of Computer Science at UNM
Abstract:
I will propose a simple and robust method for image and volume data segmentation based on manifold distance metrics. In this approach, pixels in an image are not considered as points with color values arranged in a grid. In this way, a new data set is built by a transform function from one traditional 2D image or 3D volume to a manifold in higher dimension feature space. Multiple possible feature spaces like position, gradient and probabilistic measures are studied and experimented. Graph algorithm and probabilistic classification are involved. Both time and space complexity of this algorithm is O(N). With appropriate choice of feature vector, this method could produce similar qualitative and quantitative results to other algorithms like Level Sets and Random Walks. Analysis of sensitivity to parameters is presented. Comparison between segmentation results and ground-truth images is also provided to validate of the robustness of this method.
Date: October 20, 2009 at 11:00am
Time: 11:00AM
Place: FEC 141
Manjunath Gorentla Venkata
Committee Chair:
Patrick Bridges, Associate Professor of Computer Science at UNM
Committee Members:
Dorian Arnold, Assistant Professor of Computer Science at UNM
Rolf Riesen, Principal Member of the Technical Staff, Scalable Systems Software, Sandia National Laboratories
Nasir Ghani, Associate Professor of Electrical and Computer Engineering at UNM
Abstract:
Modern HPC applications, for example adaptive mesh refinement and multi-physics codes, have dynamic communication characteristics which result in poor performance on current MPI implementations. The degraded application performance can be attributed to a mismatch between changing application requirements and static communication library functionality. To improve the performance of these applications, MPI libraries should change their protocol functionality in response to changing application requirements, and tailor their functionality to take advantage of hardware capabilities.
This dissertation describes PRO-MPI, a framework for constructing profile-driven reconfigurable MPI libraries; these libraries use past application characteristics (profiles) to dynamically change their functionality to match the changing application requirements. The framework addresses the challenges of designing and implementing the reconfigurable MPI libraries, which include collecting and reasoning about application characteristics to drive the protocol reconfiguration and defining abstractions required for implementing these reconfigurations. Two prototype reconfigurable MPI implementations based on the framework -- Open PRO-MPI and Cactus PRO-MPI -- are also presented to demonstrate the utility of the framework.
To demonstrate the effectiveness of reconfigurable MPI libraries, this dissertation presents experimental results to show the impact of using these libraries on the application performance. The results show that PRO-MPI improves the performance of important HPC applications and benchmarks. They also show that the application performance improves significantly when exact profiles are available, and the performance improves considerably when only approximate profiles are available.
Date: Tuesday, September 1st, 2009
Time: 10:00AM
Place: ME 400
Tamanna Arora
Committee Chair:
Melanie Moses, Assistant Professor of Computer Science at UNM
Committee Members:
George Luger, Associate Chair of Computer Science at UNM
Payman Zarkesh-Ha, Assistant Professor of Electrical and Computer Engineering at UNM
Abstract:
Convergence of computing capabilities combined with increased consumer demand has resulted in the development of devices with enhanced functionalities and capabilities. System designers face a daunting challenge of providing range of functionalities at a low cost while maintaining the reliability of existing systems. As devices become more complex, it is of prime importance to find out ways to make an optimized use of power available from batteries. This work focuses on curbing power consumption right at the design stage.
This work emphasizes minimizing active power consumption by minimizing the load capacitance of the chip. The two capacitive components are wires and vias. Wires are used for routing of components on chips. Vias provide an electrical connection between two adjacent metal layers. Multiple metal layers are very useful as they provide tiers of horizontal and vertical routing area, stacked over each other and connected by vias. Hence adding vias to the design can save wire-length whereas routing in same layer at the cost of increased wire-length can save vias. Thus there exists a trade-off between the number of wires and vias used in routing.
This work uses Ant Colony Optimization algorithm to handle the multiple constraints of minimizing wire-length and vias to achieve the goal of minimizing capacitance and hence power consumption. Ant Colony Optimization provides a multi agent framework for combinatorial optimization problems. Every agent practices an independent sequential decision process and utilizes memory, stochastic decision making and strategies of collective and distributed learning to perform optimal search. ACO can be easily adapted to follow a particular set of heuristic rules that are formulated according to the specific goals of optimization problem, in this case, finding routes that minimize the capacitance of the chip.
This work employs ACO on both manhattan and diagonal routing architectures and uses a set of heuristics to find optimal routing paths on the chip.
Date: Thursday, August 27th, 2009
Time: 8:00AM
Place: ME 427
Sushmita Roy
Committee Chair:
Terran Lane, Associate Professor of Computer Science at UNM
Committee Co-Chair:
Margaret Werner-Washburne, Professor of Biology at UNM
Committee Members:
Melanie Moses, Assistant Professor of Computer Science UNM
Susan Atlas, Research Associate Professor of Physics at UNM
Abstract:
Condition-specific cellular networks are networks of genes and proteins that describe functional interactions among genes occurring under different environmental conditions. These networks provide a systems-level view of how the parts-list (genes and proteins) interact within the cell as it functions under changing environmental conditions and can provide insight into mechanisms of stress response, cellular differentiation and disease susceptibility. The principle challenge, however, is that cellular networks remain unknown for most conditions and must be inferred from activity levels of genes (mRNA levels) under different conditions. This dissertation aims to develop computational approaches for inferring, analyzing and validating cellular networks of genes from expression data.
This dissertation first describes an unsupervised machine learning framework for inferring cellular networks using expression data from a single condition. Here cellular networks are represented as undirected probabilistic graphical models and are learned using a novel,data-driven algorithm. Then several approaches are described that can learn networks using data from multiple conditions. These approaches apply to cases where the condition may or may not be known and, therefore, must be inferred as part of the learning problem. For the latter, the condition variable is allowed to influence expression of genes at different levels of granularity: condition variable per gene to a single condition variable for all genes.
Results on simulated data suggest that the algorithm performance depends greatly on the size and number of connected components of the union network of all conditions. These algorithms are also applied to microarray data from two yeast populations, quiescent and non-quiescent,isolated from glucose starved cultures. Our results suggest that by sharing information across multiple conditions, better networks can be learned for both conditions, with many more biologically meaningful dependencies, than if networks were learned for these conditions independently. In particular, processes that were shared among both cell populations were involved in response to glucose starvation, whereas the processes specific to individual populations captured characteristics unique to each population. These algorithms were also applied for learning networks across multiple species. Preliminary analysis suggests that our approaches capture shared characteristics across different species better than approaches that learn networks for each species independently.
Finally, this dissertation focuses on validation of cellular networks. This validation framework describes scores for measuring how well network learning algorithms capture higher-order dependencies. This framework also introduces a measure for evaluating the entire inferred network structure based on the extent to which similarly functioning genes are close together on the network.
Date: Thursday, August 27th, 2009
Time: 9:00AM
Place: FEC 141
Stephan Falke
Committee Chair:
Deepak Kapur, Distinguished Professor of Computer Science at UNM
Committee Members:
Juergen Giesl, Professor of Computer Science at RWTH Aachen University,Germany
William McCune, Research Professor of Computer Science at UNM
Robert Veroff, Professor Emeritus of Computer Science at UNM
Abstract:
Term rewrite systems have been extensively used in order to model computer programs for the purpose of formal verification. This is in particular true if the termination behavior of computer programs is investigated, and automatic termination proving for term rewrite systems has received increased interest in recent years. Ordinary term rewrite systems, however, exhibit serious drawbacks. First, they do not provide a tight integration of natural numbers or integers. Since the pre-defined semantics of these primitive data types cannot be utilized, reasoning about termination of ordinary term rewrite systems operating on numbers is often cumbersome or even impossible. Second, ordinary term rewrite system cannot accurately model collection data structures such as sets or multisets, which are supported by many high-level programming languages such as Maude or OCaml.
This dissertation introduces a new class of term rewrite systems that addresses both of these drawbacks and thus makes it possible to accurately model computer programs using a high level of abstraction in a natural formalism. Then, the problem of automatically proving termination for this new class of term rewrite systems is investigated. The resulting dependency pair framework provides a flexible and modular method for proving termination. In addition to unrestricted rewriting, termination of rewriting with the innermost strategy or a context-sensitive rewriting strategy is investigated as well.
The techniques for proving termination that are developed in this dissertation have been implemented in the well-known termination prover AProVE. An empirical evaluation shows that the implementation succeeds in automatically proving termination of a large collection of computer programs that are modeled using the new class of term rewrite systems developed in this work.
Next, the use of this new class of term rewrite systems in the context of inductive theorem proving is investigated. This makes it possible to reason about the semantics of computer programs. The inductive theorem proving method developed in this dissertation provides a tight integration of inductive reasoning with a decision procedure, thus resulting in a high degree of automation.
Finally, conditions under which the inductive theorem proving method is guaranteed to succeed in proving or disproving a conjecture without any user intervention are identified. Thus, the inductive theorem proving method can be applied as a "black box" if these conditions are satisfied.
The inductive theorem proving method and checks for the conditions under which it provides a decision procedure have been implemented in the prototype prover Sail2. An empirical evaluation shows that Sail2 is very efficient, and the high degree of automation makes it possible to use Sail2 in a push-button mode for formal program verification.
Thesis & Dissertation Defenses Archive
News & Events | People | Academics | Research | Jobs | Companies | Visitors | Computer Facilities | Home
