XAPT Corporation was the winner of the Microsoft Dynamics ERP Global Partner of the Year 2011 Award

This is a CSMS Project Industrial Liaison Seminar. Refreshments will be served.

At a time when the cheapest AAA video game takes roughly two years, 20 million dollars, and 70 people to make, what sort of challenges face an independent development team with limited time, money, and man power, let alone in a rapidly growing market that demands increasingly higher quality products? In this presentation, the intimidating expectations, pie eyed goals, and crushing realities facing those trying to stand toe to toe with the video game industry behemoths will be highlighted while showcasing a student team's progress in their yearlong effort to develop a video game for the Xbox 360.

MicroRNAs and siRNAs ate small regulatory RNAs that play a vital role in diverse biological processes. Their ultimate function is to facilitate the reduction of the product of a target messenger RNA. Recent advances in genome synthesis technology allow for manipulation of existing genes and the creation of novel genomic sequences to specification, with a great number of applications. Incorporation of miRNA sites in mRNA sequences allows for enhanced expression control and facilitates dynamic regulatory network interactions. We explore the possibility of embedding miRNA binding sites in the coding region of a protein.

This is Department of Computer Science Seminar

Multirobot systems are an important research topic in wide area coverage applications such as hazardous waste clean-up, bomb detection, surveillance, and search and rescue missions. They can work in parallel and complete tasks faster than a single robot. Communications can support cooperation to speed up execution, reduce duplication, and prevent interference. Communication among team members is achieved explicitly or implicitly. In explicit communication, messages are intentionally transmitted and received from robot to robot. In implicit communication, robots observe the environment and other robot actions. Although many systems use explicit communications, in exploration of large, open areas (e.g. stadiums and parks), persistent intra-team digital communication is not guaranteed. Therefore, alternative approaches that do not rely upon message passing throughout exploration are needed.

Novel contributions of overcoming communication limitations in wide area coverage include: (1) insight on how information shared between robots that are close has more influence on immediate action selection than information shared between robots that are farther apart. Spatial and temporal locality can be instrumental in determining relevance in subsequent action selection; (2) an approach in which observation leverages spatial and temporal locality to infer state rather than rely on digital messaging; and (3) an approach in which robots use spatial rendezvous to exchange information instead of continuously passing messages. Robots explore an environment in sectors, or designated areas, and periodically meet to communicate map information of what they explored. Simulations and physical experiments were conducted and results suggest both approaches can serve as alternatives to cooperation based on continuous point-to-point communications.

This talk presents an overview of ontology, including how formal ontology compares to less formal approaches and how the Suggested Upper Merged Ontology (SUMO) (www.ontologyportal.org) compares to other formal ontologies. Classes of ontology-based applications are introduced. Issues of the capabilities and tradeoffs in first order logic inference are explored. The SUMO is also described in detail, along with its mappings to the WordNet lexicon.

Adam Pease is a senior researcher at Rearden Commerce in Foster City, Ca. He has led research in ontology, linguistics, and formal inference, including development of the Suggested Upper Merged Ontology (SUMO), the Controlled English to Logic Translation (CELT) system, and the Sigma knowledge engineering environment. Sharing research under open licenses, in order to achieve the widest possible dissemination and technology transfer, has been a core element of his research program and his products have been downloaded by thousands of people around the world. He is the author of the new book "Ontology: A Practical Guide".

This is another in the Departmental Pizza Seminar series.

In this talk I will present my research on real-time 3D graphics and virtual characters. In the first part, I will summarize the motivation behind my work and my contributions to skinning, deformable collision detection, and pre-computation based rendering. In the second part, I will talk in detail about animating cloth and clothing, starting with a playback-only baking technique and subsequently moving to a more general upsampling method, which adds fine-scale details to coarse mesh simulations. Interesting technical nuggets needed to make these approaches work efficiently include: an approximate version of principal component analysis, harmonic regularization (an extension of the classical Tikhonov approach) and our take on "tracking," i.e., how to constrain fine-scale physics to follow a given coarse-scale animation. In the final part, I will conclude with some ideas for future work, revolving mostly around the question of how to make digital content creation more intuitive.

All traditional approaches to adding identity and access management functionality to applications present the same issues: they require the developers to take matters into their own hands, demand specialized security knowledge or heavily rely on the features of the underlying infrastructure. This situation has led to a proliferation of APIs and techniques, forcing developers to continually re-learn how to perform the same task with different APIs or in other words constantly "reinventing the wheel". Claims-based identity is an approach that changes the way we think about authentication and authorization, adding a logical representation of identity transactions and identify the roles that every entity plays. By adding that further level of indirection, claims-based identity created the basis for decoupling the programming model and the details of the deploy-time systems. Consequently, taking the claims-based identity approach we can achieve high-level yet accurate descriptions, irrespective of their implementation details.

Note: This will be an excellent venue to learn about a local software company that hires interns and full time software engineers. Undergraduate Computer Science students are especially encouraged to attend.

This is another in the Departmental Pizza Seminar series.

The area of Artificial Intelligence is diverse and at a crossroads. Much of the past research in the area has focused either on high-level reasoning from abstract, ungrounded representations or on interpreting raw sensor data towards building grounded representations. However, neither of these foci taken alone is sufficient for deploying practical, real-world AI systems. My research focuses on knowledge representation and reasoning in two application areas: (1) Agents in Dynamic and Real-Time Environments and the (2) Semantic Web. I will address both areas:

(1): In recent years, much work has been done on creating complete autonomous agents: those that sense their environment, engage in high-level cognitive decision-making, and then execute their actions in the environment. We will explore the problem of enabling autonomous agents in finding the right position on the field or in tracking the ball within a soccer game while dealing with time constrains, adverse opponents, and dynamic environments. This research has implications for a variety of autonomous agents and robotics, such as robots that assists humans on an every day basis.

(2): The focus of my research in the Semantic Web area is the development of methods in order to solve the semantic heterogeneity problem (e.g., catalogue integration). I concentrate and evaluate on emerging ontology-based approaches in order to find and integrate information sources for the construction of ontologies. These techniques are used to solve problems that can be described with terminological logics. I will demonstrate an example from our NIH funded research project "BioAssay Ontologies" (in collaboration with the Miller School of Medicine).

Different Automated Theorem Proving (ATP) systems solve different parts of different problems in different ways. Given a set of proofs produced by ATP systems based on adequately common principles, it is possible to create new proofs by combining proof components extracted from the proofs in the set. It is not generally easy to say that one of the original or new proofs is better or worse than another, but ways to show that two proofs are different are available. This talk describes a process of proof combination to form new proofs that are different from the original set of proofs.

This is another in the Departmental Pizza Seminar series.

Modern life science and drug discovery research generates very large amounts of so called -omics data, including data about properties and functions of genes, proteins, and more complex biological entity modules. Large amounts of data are also generated of perturbations of biological model systems for example by chemicals. All with the goal to better understand the mechanisms of human disease and how dysregulated systems can be put back into normal function. However, despite the exponential increase of available data, new knowledge does not appear to be generated at the same pace, as can be seen for example at the relatively constant rate of new approved drugs over the last 50 years.

The enormous complexity of biological systems and mechanisms of disease call for novel approaches combining various experimental and computational strategies and require interdisciplinary cross training and collaboration. The University of Miami with the medical school and the College of Arts and Sciences provides an ideal environment to achieve just that.

For about 18 months, via the Center for Computational Science, the research groups of Dr Visser and Dr Schürer have been collaborating to develop novel approaches to enable researchers to better utilize existing high-throughput datasets. This collaboration has been so successful that we are now planning to expand it further while providing opportunities for students who are interested to develop the cross-disciplinary expertise required to address the most pressing issues related to human health.

In this seminar we will briefly introduce several current research projects covering different aspects of drug discovery. A unifying aspect is the goal of enabling scientists to better utilize large and complex available datasets and the development and application of semantic web technologies to achieve this goal.

We will introduce 1) the BioAssay Ontlogy (BAO) project (http://bioassayontology.org/), which is focused on categorizing and analyzing biological screening data; 2) "Phylostructeomics" - proteome-wide analysis of binding sites and ligand protein binding interactions targeted toward poly-pharmacology; and 3) the SMARTNames project focused on functional chemistry space, chemical reactivity and synthetic chemistry. More information and publications can be found at http://biomed.miami.edu/sschurer and http://www.ccs.miami.edu/chemoinformatics-team.html.

This is another in the Departmental Pizza Seminar series.

Psycholinguistic research shows wide evidence of the online, incremental nature of language understanding. Artificial systems that interpret language, however, have generally been designed based on essentially offline architectures. This talk is divided into two parts. First, we present a corpus of task-oriented interactive dialogue that is used to develop conversational agent systems. Second, we use information theory to analyze to what extend speakers follow optimal strategies in distributing information during language production.

This is another in the Departmental Pizza Seminar series.

In the field of Music Data Mining, Mood and Topic information has been considered as a high level metadata. The extraction of mood and topic information is difficult but is regarded as very valuable. The immense growth of Web 2.0 resulted in Social Tags being a direct interaction with users (humans) and their feedback through tags can help in classification and retrieval of music. One of the major shortcomings of the approaches that have been employed so far is the improper filtering of social tags. This thesis delves into the topic of information extraction from songs' tags and lyrics. The main focus is on removing all erroneous and unwanted tags with help of other features. The hierarchical clustering method is applied to create clusters of tags. The clusters are based on semantic information any given pair of tags share. The lyrics features are utilized by employing CLOPE clustering method to form lyrics clusters, and Naive Bayes method to computer probability values that aid in classification process. The outputs from classification are finally used to estimate the accuracy of a tag belonging to the song. The results obtained from the experiments all point towards the success of the method proposed and can be utilized by other research projects in the similar field.

This is a Department of Computer Science Masters Defence.

Emerging technologies facilitate an environment where web-based software or web services have well-defined, open interfaces and are discoverable across the Internet. Service-oriented computing is an emerging approach to software engineering that suggests that new specialized business processes can be created, on-demand, simply by integrating the services provided by others. However, in the real world, software developers tend to create applications that do not conform to consistent developmental practices even if they do use universal interface representations (e.g. the eXtensible Markup Language). Our research utilizes semantic approaches, enhanced syntactical methods, and contextual information to automate the integration of software services that are developed randomly from a wide array of diverse sources. This talk discusses our foundational lines of research and subsequent contributions in the areas of service discovery, composition, and evaluation. The talk will conclude with future work that leverages service-oriented paradigms in areas such as visual analytics, smart grid, and the "Internet of things".

This is a Department of Computer Science Colloquium.

Regular expressions are mostly known as pattern matching expressions in scripting languages (Perl, sed, awk, etc.). They are also theoretically studied as being part of Automata Theory. A regular expression denotes a language (set of words) and two regular expressions are equivalent when they denote the same language. The equivalence problem is decidable and furthermore, any equivalence can be proved axiomatically. Various such axiomatisations have flourished during the last fifty years, we will survey the most important ones. Every axiomatisation comes together with a proof of completeness of the following form: if two regular expressions are equivalent then there exists a proof within the axiomatic system. In principle, when this completeness proof is constructive one can extract from it an algorithm that produces a certificate of the equivalence. We have filled the gap developing a program (written in OCaml) that computes certificates. For this purpose we have designed a domain specific proof system with a language of commands for composing a certificate checkable within this system. During the talk I will make a demonstration of the program.

This is a joint work with Bodhayan Roy at TIFR.

This is another in the Departmental Pizza Seminar series.

Accurate earthquake prediction is a difficult, unsolved problem that is central to the ambitions of many geoscientists. Understanding why earthquakes occur requires a profound understanding of many interrelated processes; the Earth functions as a massive, complex system. Scientific visualization can be applied to such problems to improve understanding and reveal relationships between data. There are several challenges inherent to visualizing seismic data: working with large, high-resolution 3D and 4D data sets in a myriad of formats, integrating and rendering multiple models in the same space, and the need for real-time interactivity and intuitive interfaces. This work describes a product of the collaboration between computer science and geophysics. TerraVis is a real-time system that incorporates advanced visualization techniques for seismic data. The software can process and efficiently render digital elevation models, earthquake catalogs, fault slip distributions, moment tensor solutions, and scalar fields in the same space. In addition, the software takes advantage of stereoscopic viewing and head tracking for immersion and improved depth perception. During reconstruction efforts after the devastating 2010 earthquake in Haiti, TerraVis was demonstrated as a tool for assessing the risk of future earthquakes.

This is a Department of Computer Science Masters Defense.

James shares how he went from making pennies as a local Miami web developer to building the largest video game hosting company in the world in less than 8 years.

James is the CEO of Hypernia, and specializes in hosting the world's top media and entertainment businesses. He is responsible for connecting over 50 million people together each and every day through social networks, online games, websites and online communications. His goal is to keep technology affordable and flexible for everyone to promote social progress. In 2008, he worked with Michael Moore in distributing "Slacker Uprising" online, breaking all worldwide download records for a feature film.

This is a CSMS Project Industrial Liaison Seminar. Refreshments will be served.

The RoboCup Soccer Simulation 3D teams RoboCanes, of the University of Miami, and Bold Hearts, of the University of Hertfordshire, have joined forces under a grant of the RoboCup federation to enhance and develop the infrastructure for one of the largest robotics and AI competitions in the world. Firstly, we made the simulation system used in the simulated humanoid robotic soccer competitions ready to enable competitions on a larger scale and more dynamic than the years before. Secondly, we have designed and developed a framework to perform massive parallel learning and optimisation in the complex scenario of robotic soccer. Despite this collaboration, the teams are still competitors, currently competing for the first prize in the German Open competitions. In this seminar we will give an overview and demos of both our collaborative and competitive work.

This is a Department of Computer Science Colloquium. Refreshments will be served.

The Internet is at once an immense engineering artifact, a pervasive social force, and a fascinating object of study. Unfortunately many natural questions about the Internet resist precise answers, for a variety of reasons. In this talk I'll start by discussing why measuring the Internet's infrastructure, traffic, and applications is interesting and important, and why it is often so difficult. I'll then touch on methods that are often used to overcome the Internet's resistance to being measured -- in particular, statistical inference. As a detailed example I'll describe a current project in traffic measurement. We are asking the question: using traffic measurements taken at one location in the Internet, can we estimate how much traffic is flowing in a different part of the Internet? I'll show evidence that such estimation is indeed possible, and suggest how this technique may be used to answer both scientific and commercial questions.

Mark Crovella is Professor of Computer Science at Boston University. He received his Ph.D. in Computer Science from the University of Rochester in 1994. His research interests are in performance evaluation, focusing on parallel and networked computer systems. In the networking arena, he has worked on characterizing the Internet and the World Wide Web. He has explored the presence and implications of self-similarity and heavy-tailed distributions in network traffic and Web workloads. He has also investigated the implications of Web workloads for the design of scalable and cost-effective Web servers. In addition he has made numerous contributions to Internet measurement and modeling; and he has examined the impact of network properties on the design of protocols and the construction of statistical models. Professor Crovella is co-author of "Internet Measurement: Infrastructure, Traffic, and Applications" (Wiley Press, 2006) and is the author of over one hundred papers, with over 13,000 citations (Google Scholar, 2010). Between 2007 and 2009 he was Chair of ACM SIGCOMM. In 2010 he received the SIGMETRICS Test of Time Award for "Self-Similarity in World Wide Web Traffic: Evidence and Possible Causes". Professor Crovella is a Fellow of the ACM.

This is a Department of Computer Science Colloquium. Refreshments will be served.

Every agent needs information about the current state and the environment to act successfully. Often retrieving information from sensor measurements is considered as a passive process, that is done while the agent tries to reach a goal. However in many scenarios the actions of an agent have an influence on the perceptions. So it is possible to consider the information gain in the selection of actions, such that the error in the estimated state is decreased. Strategies for active sensing or active localization can lead to a large improvement of the overall performance.

The RoboCup is a robotics competition where autonomous robots play soccer. A soccer robot in this environment can not perform well without information about the own position and the location of the ball. Smaller errors in the state estimation lead to a more accurate behavior. A simple head movement that scans the environment in a fixed pattern already works, but it has to be tuned manually and is not flexible.

It will be shown how the estimation of a robot's world model can be improved by actively sensing the environment through considering the current world state estimate through minimizing the entropy of an underlying particle distribution. Being originally computationally expensive, this approach was optimized to become executable in real-time on a robot with limited resources. This approach was used on a humanoid robot, performing self-localization and ball tracking on a RoboCup soccer field.

Andreas Seekircher is a PhD student at the University of Miami. He holds a M.Sc. in Computer Science from the University of Bremen, Germany. The paper "Entropy-based Active Vision for a Humanoid Soccer Robot" won the best paper award on the RoboCup Symposium 2010. His research is focused on robotics and artificial intelligence, specifically controlling autonomous robots.

This is another in the Departmental Pizza Seminar series.

Acquiring and processing information is important for agents, both natural as artificial. Being able to use more information can give the agent an advantage over others. However, information can be very costly for many organisms, from blow flies to humans, it is known that information related processes can take up over 20% of the full energy consumption. So, we can assume that an agent tries to maximize its informational capability, but only up to the minimal requirements for being able to act successfully. We can study the effect of this assumption, and of informational bounds in general, on behavior, using tools from the well-established field of Information Theory. I will discuss some of the aspects and behavioral properties arising from this methodology, such as Empowerment, which measures the amount of observable control of an agent on the environment and leads to intrinsically motivated behavior, and Relevant Information, which is the minimum amount of information needed to achieve a certain level of performance on a task. Specifically, I will focus on hierarchical behavior structures, which are popular in ethology and machine learning, although deep understanding of why they are attractive, why they work, and whether they are necessary, is missing. Starting from the argument that behaviour generation is constrained by a range of limits on information acquisition and processing, I show how such limits spontaneously give rise to abstraction and structuring of tasks and behaviour generation, and thereby suggest that hierarchical structuring is a natural way of coping with informational constraints.

This is another in the Departmental Pizza Seminar series.

Monolithic programs are now being gradually replaced with software that is made up of a number of components, originating from various sources. Every software component is associated not only with functional, but also with non-functional aspects. A reflective middleware framework has been built to capture characteristics that a software component should have and how other components depend on those characteristics to keep the whole system working as required. The main idea is to monitor (introspection) the applications, in order to change or tune (intercession) the software components with the specific goal of making the whole system workable. To find new components, two stochastic search algorithms were developed and added to the middleware. Software component selection is done using both the most relevant characteristics that the component should have so they can be integrated to the other existing components and swarm intelligence techniques; specifically pheromone value.

This is another in the Departmental Pizza Seminar series.

Computer Science dominates every aspect of robotic and human exploration of the planets. Prior to launch, mission design and planning merge planetary body models with predicted launch vehicle, orbit, spacecraft and science payload instrument models to optimize the probability of success, define mission phases and science observation sequences, and minimize risks by having sufficient weight, power, data transmission, etc. resource margins to handle the "unknown" unknowns. During flight operations, these same models and algorithms are updated to reflect the knowledge learned of the planetary bodies, instrument flight performances and anomalies encountered to continually re-plan the remainder of the mission. Finally the scientific data analyses is performed to glean every tidbit of information that will help us determine the origins, evolutions and current states of the planetary bodies in our solar system and what lies ahead for humans. Examples will be given on observation planning, instrument modeling, image restoration, diverse data set registration and map projection, data visualization and flight operations. At the heart of all of these are models, data and algorithms optimized to run on computers, with parallel computers becoming more prevalent, having print, plot and interactive voice and terminal displays (i.e., computer science) to learn the secrets hidden in the planetary bodies.

This is a CSMS Project Industrial Liaison Seminar. Refreshments will be served.

Several methods in data and shape analysis can be regarded as transformations between metric spaces and in general, as maps from k-tuples of metric spaces into a metric space. Examples are hierarchical clustering methods, the higher order constructions of computational persistent topology, and several computational techniques that operate within the context of data/shape matching under invariances. Metric geometry, and in particular different variants of the Gromov-Hausdorff distance provide a point of view which is applicable in different scenarios. The underlying idea is to regard datasets as metric spaces, or metric measure spaces (a.k.a. mm-spaces, which are metric spaces enriched with probability measures), and then, crucially, at the same time regard the collection of all datasets as a metric space in itself. Variations of this point of view give rise to different taxonomies that include several methods, both preexisting and novel, for extracting information from datasets and shapes. I will show an ongoing application of one of these new methods to functional classification of chemical compounds by shape properties. Imposing metric structures on the collection of all datasets could be regarded as a "soft" construction. The classification of certain algorithms, or the axiomatic characterization of them, can be achieved by imposing more "rigid" directed-graph structures on the collection of all finite metric spaces. I will describe some results along these lines in the context of clustering schemes.

This is a Department of Computer Science Colloquium. Refreshments will be served in UB345 at 4:30pm.

Visualization tools are essential for deriving meaning from the avalanche of data we are generating today. To facilitate an understanding of the complex relationships embedded in this data, visualization research leverages the power of the human perceptual and cognitive systems, encoding meaning through images and enabling exploration through human-computer interactions. In my research I design visualization systems that support exploratory, complex data analysis tasks by biologists who are analyzing large amounts of heterogeneous data. These systems allow users to validate their computational models, to understand their underlying data in detail, and to develop new hypotheses and insights. My research process includes five distinct stages, from targeting a specific group of domain experts and their scientific goals through validating the efficacy of the visualization system. In this talk I'll describe a user-centered, methodological approach to designing and developing visualization tools and present several successful visualization projects in the areas of genomics and systems biology. I will also discuss the long term implications of this work and the field of visualization as a whole.

This is a Department of Computer Science Colloquium. Refreshments will be served in UB345 at 4:30pm.

Although there is a large amount of information available in formats suitable for machine reasoning (such as relational databases), the vast majority of human-made information is only available as natural language text. In this talk, I will present a hybrid, deep natural language processing approach to Information Extraction and discuss its application in two domains. First, I will describe a system which extracts geospatial information mentioned in text. Using a combination of the text mention as well as a geographic information system (GIS) database, the system grounds this information in geospatial entities and latitude and longitude coordinates and can track an entity's location over time, based only on the text description. I will also describe our recent preliminary work on using this same deep NLP framework for extracting medical history information from clinical texts.

Nate Blaylock received a Ph.D. in Computer Science at the University of Rochester in 2005 where his dissertation dealt with natural language understanding and plan recognition for dialog systems. Prior to joining IHMC in 2007, Nate was a Research Scientist at Cycorp, where his research focused on using predictive event models to apply plan recognition to level 2/3 fusion problems. Prior to that, Nate spent two years in a postdoctoral position at Saarland University in Saarbrucken, Germany, where he helped build the bilingual German/English SAMMIE in-car dialog system, using the theory of collaborative problem solving from his thesis to understand and reason with natural language in dialog. At IHMC, Nate continues to do research on dialog systems, plan and intent recognition, and natural language understanding, including information extraction in the medical and geospatial domains.

This is another in the Departmental Pizza Seminar series.

The Internet is at once an immense engineering artifact, a pervasive social force, and a fascinating object of study. Unfortunately many natural questions about the Internet resist precise answers, for a variety of reasons. In this talk I'll start by discussing why measuring the Internet's infrastructure, traffic, and applications is interesting and important, and why it is often so difficult. I'll then touch on methods that are often used to overcome the Internet's resistance to being measured - in particular, statistical inference. As a detailed example I'll describe a current project in traffic measurement. We are asking the question: using traffic measurements taken at one location in the Internet, can we estimate how much traffic is flowing in a different part of the Internet? I'll show evidence that such estimation is indeed possible, and suggest how this technique may be used to answer both scientific and commercial questions.

Speaker Bio: Mark Crovella is Professor of Computer Science at Boston University. He received his Ph.D. in Computer Science from the University of Rochester in 1994. His research interests are in performance evaluation, focusing on parallel and networked computer systems. In the networking arena, he has worked on characterizing the Internet and the World Wide Web. He has explored the presence and implications of self-similarity and heavy-tailed distributions in network traffic and Web workloads. He has also investigated the implications of Web workloads for the design of scalable and cost-effective Web servers. In addition he has made numerous contributions to Internet measurement and modeling; and he has examined the impact of network properties on the design of protocols and the construction of statistical models.

Professor Crovella is co-author of "Internet Measurement: Infrastructure, Traffic, and Applications" (Wiley Press, 2006) and is the author of over one hundred papers, with over 13,000 citations (Google Scholar, 2010). Between 2007 and 2009 he was Chair of ACM SIGCOMM. In 2010 he received the SIGMETRICS Test of Time Award for "Self-Similarity in World Wide Web Traffic: Evidence and Possible Causes". Professor Crovella is a Fellow of the ACM.

This is a Department of Computer Science Colloquium. Refreshments will be served.

Developing software to bring a complex mobile robot system to life and have it exhibit intelligent behavior in an autonomous, robust, and safe manner is a very, very difficult, complex, time-consuming, and error-prone endeavor. In this talk I analyze the reasons and origins of this complexity and present some ideas for handling it. One topic of particular relevance is architecture, and its manifold interpretations of it. I survey the approach we take in the project BRICS to structure architectural issues. Finally, I present a software development process model we recently developed in order to organize software development in robotics such that it meets professional standards.

Gerhard K. Kraetzschmar is a professor for autonomous systems at Bonn-Rhein-Sieg University, Germany. He obtained a M.Sc. (Diploma) and a Ph.D. (Dr.-Ing.) in Computer Science, both from University of Erlangen. His research interests include a wide range of fields in robotics, artificial intelligence, artificial life, and neuroinformatics, with special focus on software development for robotics, multirobot teams, robot learning, middleware for robotics, and educational robotics. He is a member of AAAI, ACM, IAS, IEEE, and GI, and Vice President RoboCupJunior of the RoboCup Federation.

This is a joint Department of Computer Science and Department of Electrical and Computer Engineering Colloquium. Refreshments will be served.

Pablo Bolivar Morales - Estimation of Repeats from Sparce Next Generation Sequencing

Andres Acevedo Ulloque - Android Game Development: The Runner
This project explores development for mobile platforms and the trend that follows it. We will talk about the use a game engine (AndEngine) during the development of a game for the Android platform. Additionally, we will discuss from the design concept to the implementation, the difficulties and challenges faced during the process of developing an Android game. Demo of Android game - Runner.

This is another in the Departmental Pizza Seminar series.

Gracia Bonilla - CoSeChar: Genomic Coding Sequence Characterization Tools

Cameron Carpenter - SporkleAI: Automatic Interfacing and Problem Solving on Sporkle.com

Oscar Sanchez - Upgrading and Restructuring the "Save Dade" Website and Services

This is another in the Departmental Pizza Seminar series.

The Deep Water Horizon well blowout on April 20th 2010 discharged between 40,000 - 1.2 million tons of crude oil into the Gulf of Mexico. In order to understand the fate and impact of the discharged oil, particularly on the environmentally sensitive Florida Keys region, we have implemented a multi-component application which consists of many individual tasks that utilize a distributed set of computational and data management resources. The application includes two 3D ocean circulation models of the Gulf and South Florida and a multi-phase oil spill model. Information from ocean models is integrated with a multi-phase oil model that tracks the fate of approximately 10 million oil particles. These individual components execute as large parallel applications on a 640 core IBM Power 5 cluster and a 5040 core Linux cluster, both operated by the Center for Computational Science, University of Miami. The work flow between the models is handled by a custom distributed software framework built using the Open Project for Networked Data Access Protocol (OPeNDAP). In this talk, we present sample results and discuss computational challenges in deploying such many task distributed work flows on large clusters and heterogeneous architectures.

This is a CSMS Project Industrial Liaison Seminar. Refreshments will be served.

GPU computing is the use of a GPU (graphics processing unit) to perform general purpose scientific and engineering computations. The GPU has evolved over the years to have teraflops of floating point performance. New massively parallel architectures enable the use of hundreds of processor cores for general computations, while their modest price and accessible programming interfaces allow the general users to take advantage of these developments. In this seminar we will examine the modern GPU architecture and design philosophy, exposing some of the benefits and limitations of the platform. We will introduce algorithmic techniques for this specialized architecture and demonstrate how to create programs using the CUDA programming model.

This is another in the Departmental Pizza Seminar series.

Modular audio programming environments such as SuperCollider or Max/MSP are used for a wide variety of tasks, such as algorithmic music composition, live sound and art installations, and acoustics research. They allow users to quickly develop specialized tools in an environment tailored for working with audio. While they are enormously powerful, using them for sound design is sometimes difficult because of the lack an intuitive interface for exploring the parameters of the synthesis graphs built in them. Synthetic is a program that wraps around SuperCollider and provides this interface. It aims to be a new breed of software that is a cross between a wave editor and a modular audio environment.

This is another in the Departmental Pizza Seminar series.

While both volunteer computing and social networks have proved successful, the merging of these two models is a new field: Social Volunteer Computing. A Social Volunteer Computing system utilizes the relationships within a social network to determine how computational resources flow towards tasks that need to be completed, and the results of these computations are added back into the social network as content. Such a system will provide scientists and artists a new facility to obtain computational resources and disseminate their work. RenderWeb, a prototype Social Volunteer Computing system, is introduced that allows animations created in Blender to be distributed and rendered within Facebook.

This is a Department of Computer Science PhD Proposal Defense

The traditional rendering technique of real-time computer graphics involves the use of geometric primitives, such as triangles, to construct surface representations of objects. This technique works well in many situations, especially when drawing objects that are solid and have easily recognizable surfaces. However, there are many visual phenomena that are nebulous, contain partial transparency, or are too complex to effectively visualize with polygonal meshes. Examples found in nature include smoke, fire, cloudes, and crepuscular rays ("god rays"). Scientists and engineers also require methods for interpreting volumetric data: pressure measurements in an area surrounding a fault, air turbulence, the behavior of fluids, or medical data with several layers and materials. With the recent evolution of programmable graphics hardware, volumetric data and related phenomena can be rendered with interactive framerates. This presentation will provide a high-level overview of the programmable graphics pipeline and how it enables powerful new approaches to visualizing volume data. The seminar will focus on 3D texture-based GPU volume rendering and demonstrate a few applications within scientific visualization.

This is another in the Departmental Pizza Seminar series.

Michael Schick - The Language of the Future. Have you ever wanted to ask Google a math problem, or the name of the Nobel Peace Prize winner from 1919, and get back the answer not just a link to a "relevant" website? Automated Theorem Proving provides us this possibility! In my talk I will be discussing the advantages of Automated Theorem Proving, specifically the advantages of certain languages, and how my research is helping to improve the field.

Matthew Ferens - Working in the Unreal Engine. The concept of video games has become an integral part in any Computer Science discussion as it incorporates many aspects of the field into a multi-billion dollar industry. Video game engines, powerful platforms on which games are built, were once extremely restricted and proprietary, but many have recently been released for public consumption. The Unreal Development Kit is perhaps the best known and most powerful as it allows for creation of everything from simple levels to complete games by anyone with the will to learn. The purpose of this project was to work with the engine and gain experience that can apply to both scholarly and real-world work. The project focused on simple level design, scripting, and connecting it all together into a final product.

Benjamin Drolet - Reducing Spam on Online Forms. Have you ever managed a web page with form validation? Have you received annoying SPAM from people blasting your forms? Have you ever had to fill out an annoying form online? My talk will discuss a new way that I developed to reduce SPAM through forms. I will talk about the advantages and disadvantages of form validation and how my program is helping improve the process.

This is another in the Departmental Pizza Seminar series.

Do you often misplace your keys? Forget someone's name a second after you've heard it? Wish you could memorize facts for a test quicker? If the answer to any of those is yes, then you are probably in the same boat as everyone else! But it doesn't have to be that way. I will be giving a seminar on how to improve your memory drastically. Remembering names, numbers, words, can be easy and fun. I have been able to train my brain to memorize a 200 digit number in less than 5 minutes, the order of a shuffled deck of cards in just under a minute, and the names of everyone I meet. In this talk I will be discussing the techniques I have trained my memory to use in order to accomplish these amazing feats. The best part: anyone can learn them!

See Nelson on TV.

This is another in the Departmental Pizza Seminar series.

Geospatial data integration with semantic web technology is one of the hot topics in the knowledge and data engineering field. What makes the integration of geospatial data task more complicated than others is the variety of the geospatial data models, formats, semantics and relations. Moreover, in order to employ the web as a medium for data and information integration, comprehensive datasets and vocabularies are required as they enable the disambiguation and alignment of other data and information. All these factors are considered challenges in the design and implementation of a semantic web based GIS system. TerraFly, a public service of Florida International University sponsored by NSF (MII, MRI et al.) and by NASA, USGS, and IBM is our candidate on which we apply the semantic web techniques for the purpose of integrating data from various knowledge bases, and enriching its search service with more accurate and meaningful query results.

This is another in the Departmental Pizza Seminar series.

In response to Hurricane Andrew, South Florida Building Code was revised to include debris impact protection of products covering exterior openings of the building. The new standards also implemented ASCE-7-88 which increased the wind pressure on building envelopes. The new testing standards with enhanced pressures, required development of advanced testing and analysis facilities. The task required the merger of several engineering and scientific disciplines. We will examine how an interdisciplinary approach to problem solving was used to address these challenges.

This is a CSMS Project Industrial Liaison Seminar. Refreshments will be served.

The recent earthquake in Haiti has motivated scientists and engineers to assess the risk of future earthquakes that could affect the rebuilding of Port-au-Prince. As part of a collaborative effort with geophysicists in the Rosentiel School of Marine and Atmospheric Science, we have developed prototype software for visualizing seismic data. Our software takes advantage of stereoscopic 3D rendering for immersion and improved perception of depth. This talk will describe the relevance of the data being visualized as well as the details of the software's implementation. The fundamentals of stereo vision and differences between the various stereo technologies will also be covered. This seminar will involve an interactive demonstration of the stereoscopic 3D vision.

This is another in the Departmental Pizza Seminar series.

Images contain large amount of data and are used in many applications. Not only compressed image data save space, but also in certain applications such as the World-Wide-Web (WWW), they save time since the amount of data to be transmitted is smaller than the original image. Codebook approaches have been used in lossy image compression. For example, vector quantization employs codebook. For lossless compression of images, more than a decade ago, a codebook approach based on spanning trees was proposed. In this talk we address suitability of permutation codes for still images.

This is another in the Departmental Pizza Seminar series.

Search Engines are our number one source for finding answers to questions in the 21st century, but unfortunately they do not provide us with immediate answers. The answers still need to be extracted by the user from the results returned by the search engine. This talk addresses this problem and discusses how we are getting closer to being able to reason about world knowledge by using theorem provers and how they provide us with the exact answers we are looking for. Currently, the theorem provers used to provide this service lack a user-friendly means of submitting a query. This talk will also discuss how, by using controlled natural language, one can submit queries with ease and in a natural way rather than a complex and esoteric way.

This is another in the Departmental Pizza Seminar series.

While both volunteer computing and social networks have already proved to be successful, the merging of these two models is a new field. We call this new field Social Volunteer Computing. A Social Volunteer Computing system utilizes the relationships within a social network to determine how computational resources flow towards tasks that need to be completed. We call this Socially-Driven Computation. The result of this computation, which we call Socially-Computed Content, is added back into the social network. This presentation will also introduce RenderWeb, a prototype Social Volunteer Computing system that allows Blender animations to be quickly rendered by friends within Facebook.

This is another in the Departmental Pizza Seminar series.

Over 40 years ago, Michael Goldberg started a Miami software company called FDP, employing many UM mathematics and computer science students over the years and eventually becoming the leading provider of software for the insurance and pension industries. After selling FDP, Michael started another company 5 years ago called Flamingo Software, specializing in web-based systems for insurance and financial services companies. Find out what a career in software development can be like and what it takes to run a successful software company.

This is a CSMS Project Industrial Liaison Seminar. Refreshments will be served.

The FIU School of Computing and Information Sciences, with partners FAU and UNCC, is leading an exciting international research and career development opportunity for students from FIU, FAU, UNCC, UM, and UPRM. This Partnership for International Research and Education (PIRE) is a 5-year long project funded for $2.3 million through a highly competitive program by the National Science Foundation. PIRE aims to provide international research and training experiences to its participants by leveraging the established programs, resources, and community of the Latin American Grid. After the successful execution of this program in the first two years, we decided to open this program to all disciplines of Science and Engineering. Students selected by the PIRE program will become part of a prestigious international research network focusing on using cyberinfrastructure to solve challenging societal problems while training a generation of globally-oriented IT professionals who will become leaders in industry and academia. We are looking for highly qualified undergraduate, graduate, and post-doctoral students in Science and Engineering disciplines who are interested in working on critical real-world applications that use or extend cyberinfrastructure as part of an international R&D team. The PIRE program includes collaboration-driven trips (6 weeks to full semesters in length) to top research sites in Argentina, Brazil, China, France, India, Italy, Mexico, Spain, and more countries. PIRE will also sponsor fellowships of up to $10,000 per semester and monetary awards for winners of PIRE annual poster sessions.

This is a joint presentation by the Department of Electrical and Computer Engineering and the Department of Computer Science.

Over the last forty years, remarkable progress has been made in the area of speech separation and enhancement, however accurate estimation of clean speech in real-world environments is still a challenge. We address the problem of speech estimation as statistical estimation with "missing" data in the independent component analysis (ICA) domain. Missing components are substituted by values drawn from "similar" data in a multi-faceted ICA representation of the complete data. I will present the algorithm for the inference of missing data in the case of a fixed pattern of missing data, and then I will present an application of our approach to the problem of bandwidth extension, where speech is degraded by a fixed filtering process. I will show the capability of the algorithm to reconstruct fine missing details of the original data with little artifacts: information of the source signal can indeed be modeled and used in order to recreate a natural sounding source in adverse conditions. The extension of the method to statistical spectral inference according to random patterns of missingness promises progress in the long open problem of performing speech enhancement while enhancing the intelligibility of speech.

This work has been done in collaboration with Doru-Cristian Balcan (Carnegie Mellon University) and Timo Gerkmann (Bochum University).

Biography: Justinian Rosca is Program Manager in Audio, Signal Processing and Wireless Communications at Siemens Corporate Research in Princeton, USA. He is also Affiliate Professor, Department of Electrical Engineering of University of Washington, Seattle, USA. He received the Dipl. Eng. degree in Computers and Control Engineering from Bucharest Polytechnic University in 1984, the M.S. and Ph.D. degrees in Computer Science from University of Rochester in 1992 and 1997 respectively. Dr. Rosca is conducting research in statistical signal processing and radio management, with an emphasis on topics involving acquisition, management and processing of data with uncertainties, such as audio processing, blind signal separation, wireless management, adaptive principles in stochastic search and optimization, and probabilistic inference in artificial intelligence.

For new terminals such as Network PC and thin-client, broadband network access is becoming significant. For mobile users, wireless communication technology such as Cognitive Radio (CR) is expected to realize seamless communications. However, QoS consideration in CR has not been well investigated. This talk intorduces a QoS control framework which consists of such as optimization of resource allocation, and shows a result of "Geographical Optimal Route Selection with Cost-Constraint".

This is another in the Departmental Pizza Seminar series.

Jose Hernandez - Axiom Selection for Automated Theorem Proving. Is Abraham Lincoln a mammal? Does there exist a capital which has the same latitude as Moscow that can get flooded? This talk will be on my work on a axiom selector mechanism (SInE) for Automated Theorem Provers. The axiom selector picks out the correct facts needed to solve a specific set of question. I will go over how I managed to get the Automated Theorem Provers integrated into the axiom selector; also problems that arose when I did and how I plan to solve them.

Alexandra Teyssandier - ATP with External Sources of Axioms for Dummies. The internet is a constantly expanding source of knowledge. External specifications allow ATPs to access information from web sources and databases to prove large theorems. The goal is to allow an end user to take a general knowledge, English conjecture and develop a conjecture in first order logic to answer questions such as "where is it sunny in the northern hemisphere today?" The first step is a simple scroll-list interface with searchable options that allows a user to find predicates relevant to their query. It links to external specifications from SUMO and XDB. Future plans include developing a more user-friendly, English language input.

Michael Schick - Changing the World of Theorem Proving: From Untyped to Typed. This talk will discuss logic languages, including First Order Form (FOF) and Typed First order Form (TFF). It will examine the TPTP and its uses, specifically related to Automated Theorem Proving. Additionally, it will show how to convert FOF axioms to TFF. Results generated from using TFF as compared to FOF, and the other potential advantages of TFF will be described.

Pascual Oliu - Fast Edit Distance and LCS Calculation Using Dominance Relationships. Calculating edit distances between two sequences is a fundamental problem in bioinformatics. A new algorithm computes edit distances efficiently by identifying dominance relationships in a dynamic programming matrix. This talk will discuss coding an efficient implementation of the algorithm in C and using it to solve the related LCS problem.

This is another in the Departmental Pizza Seminar series.

An ontology is a formal, explicit specification of a conceptualization. The process of engineering an ontology for a domain using the top-down approach is a complex task that consumes a lot of time and effort (it's the knowledge acquisition bottleneck). When the domain is a substantially large amount of texts (corpus), one way to expedite this prior process is to reverse engineer the ontology from the corpus. In this talk I am presenting my master's research proposal on an efficient and effective method to solve the reverse engineering problem using lexico-semantic analysis and probabilistic reasoning.

This is another in the Departmental Pizza Seminar series.

Almost everyone has to give a public presentation at some time. Graduate students have to defend their theses, research students have to present their results, and many jobs require presentations. It is common to have little or no experience when you give your first presentation, and you may even be a little nervous! This talk is aimed at (graduate, research, and other) students. It describes how to present a successful talk, in a simple standard format. This talk does not try to teach general speaking skills, nor impose any personally preferred techniques. It covers the structure of a talk, the use of visual aids, speaking technique, and how to cope with questions.

This is another in the Departmental Pizza Seminar series.

In the first part of this talk we defined the problem we want to solve, i.e. the need of a systematic and flexible approach to perform pattern classification of biological data coming from many sources. Since the nature of the problem dictates the nature of the solution, in this talk we will talk about the scope of the BCD, the limitations found during its implementation, and how they were resolved. The present state of the BCD and its future direction will be discussed. The bottom question is: how general can an information system be? As we will see, not much, i.e. 'very general' with a twist.

This is another in the Departmental Pizza Seminar series.

Subduction zones, where oceanic plates are pushed under the leading edge of continental plates along ocean trenches, produce Earth's largest earthquakes and most tsunamis. The pattern of strain release during earthquakes, where the leading edge of the continental plate jumps towards the ocean by several meters or more, is related to the slow build-up of strain accumulation during the interseismic period, which may last for hundreds of years. New GPS technology permits this slow pattern of strain accumulation to be measured. Studies of strain accumulation may give clues to the nature of future earthquakes, leading to improved understanding of the seismic process and improved forecast of seismic hazard. However, GPS data at a number of subuction zones indicates that not all accumulated strain is released during earthquakes; slow, aseismic slip events with durations of days - months are increasingly recognized as a major component in the strain release budget. In this talk I will describe a new GPS and seismic network that is being installed in northern Costa Rica by the University of Miami to monitor such events, and describe preliminary results from the first three years of operation. We have already observed one slow slip event, in May 2007. Maximum surface offsets were approximately 2 cm, occurring over a duration of several weeks, corresponding to an ~ M 6.5 earthquake if all of this strain had been released rapidly. Maximum slip was centered near the down-dip edge of the conventionally defined seismogenic zone. How these data are collected, analyzed and interpreted will be discussed, as well as implications for future earthquakes and improved understanding of the earthquake process.

This is a CSMS Project Industrial Liaison Seminar. Refreshments will be served.

Biodatabases are becoming increasingly accessible, increasingly big, and increasingly heterogeneous. The BCD is an (ongoing) open web information system that provides a systematic and flexible approach to perform pattern classification of biological data coming from many sources. In this talk I will describe the practical problems encountered during the design and development of the BCD and the solutions implemented related to high performance, high availability, high maintainability, high extensibility, cloud computing, database federation, web services, configuration management, and integration of third-party calculated feature vectors into the BCD data mining framework. The present state of the BCD and its future direction will be discussed. The bottom question is: how general can an information system be? As we will see, not much, i.e. "very general" with a twist.

This is another in the Departmental Pizza Seminar series.

In this talk, I will discuss the role of mathematics and computer science at NSA and discuss hiring opportunities, including REUs (Research Experiences for Undergraduates) and programs for graduate students.

This is a CSMS Project Industrial Liaison Seminar. Refreshments will be served.

Autonomous agents in real-time and dynamic adversarial environments offer numerous research challenges. Perception, localization, decision- making, communication, and locomotion are good examples. The novel modern sports simulator we will discuss integrates results from ten years of research in the area of autonomous soccer playing robots (both softbots and physical robots) with RoboCup as a testbed. We will explore the problem of enabling autonomous agents in finding the right passing point or in making a complex decision within a soccer game while dealing with time constrains, hostile opponents, and dynamic environments. We propose a framework for spatio-temporal real-time analysis of dynamic scenes. The underlying hierarchical three-tier multiagent system consists of autonomous BDI agents that allows dynamic group structures (e.g., an emergent situation for a wing attack). The online game runs seamlessly in a web browser with a new and state-of-the-art 3D visualization engine. Latest developments include research results from a motion capturing lab and face generators to enhance the believability of the players and the users' visualization experience.

This is another in the Departmental Pizza Seminar series.

Web Services is one of the most dominant tools in the world today to implement SaaS (Software As A Service) principles. It has revolutionized the way services are mashed-up to build complex services and governing bodies. QoS (Quality of Services) such as security, reliability, etc., plays an important role in creating an ultimate service with governance. This presentation will focus on harnessing the power of Web Services using Apache Axis2 to create such a service and invoking prior service using Apache Axis2 client in a matter of minutes. In logic ...

This is another in the Departmental Pizza Seminar series.

There is an enormous demand from the industry for Web Services and related technologies at present. These demands are not only from the IT field, but also from other disciplines such as finance, telecommunications, and government. Web Services is one of the most successful implementations of Service Oriented Architectures, which provides an infrastructure to build reusable software services in a heterogeneous environment. Apache Axis2 is considered to be the most successful open source Web Services middleware platform offered by the Apache Software Foundation. This presentation will focus on the basics of the Apache Axis2 architecture, concepts, and R&D opportunities available for students in the open source arena.

This is another in the Departmental Pizza Seminar series.

In recent years there has been a growing demand for Automated Theorem Proving (ATP) in large theories, which often have more axioms than can be handled effectively as normal internal axioms. This work addresses the issues of accessing external sources of axioms from a first-order logic ATP system, and presents an implemented ATP system that retrieves external axioms asynchronously, on demand. The efficacy of the system is demonstrated on test problems that make use of a range of external sources of axioms, including databases and web services. In the long term this system will be able to answer very general knowledge questions, using a natural language interface.

This is another in the Departmental Pizza Seminar series.

Developing logic and proving conjectures are some of the major goals in the world of Automated Theorem Proving. Various ATP systems have been designed for the purpose. However, for majority of ATP systems it becomes difficult to prove conjectures when the available axiom set is too large. This research introduces a concept of machine learning to deal with large axiom sets. The closest relevant axiom sets for a failed conjecture are formed by learning from existing solved conjectures in the same problem domain. Semantic axiom refining approaches are then applied on an already reduced axiom set for refining it to a much finer level. The failed conjecture is then tried proving from refined axiom set. The SWC problem domain was picked for testing purposes, and the tool proved successful by solving 24/124 failed conjectures. Performance was better when compared to SRASS.

This is a Department of Computer Science Masters Defense.

Have you ever wondered how the University of Miami is connected to the rest of the world? In the past few years the University's network has grown to include four Internet Service Providers, 46 different commercial peers, and several research and education networks, including National Lamdba Rail, Internet 2, and others. Discover what equipment is used, what it looks like, and how it is connected together. Learn about what network resources are available to the University community.

A Pizza Science Seminar. Pizza and refershments are served.

With growing trend in 'cloud computing' and increase in the data moving into the Internet, the need to store large amounts of data by service providers such as Google, Yahoo, Microsoft, etc. has increased over time. Now, more than ever, there is a need to efficiently and securely store large amounts of data. This thesis presents an implementation of a Ramp Scheme that confidentially splits a data file into a configurable number of parts or shares of equal size such that a subset of those shares can recover the data entirely. Furthermore, the implementation supports a threshold for data compromise and data checksum verification to verify that the data parts have not been tampered with. This thesis addresses two key problems faced in large-scale data storage, namely, data availability and confidentiality.

This is a Department of Computer Science Masters Defense.

Persistent and secure store for web objects is an attractive feature in today's web world and possess a good potential for exploration. Persistence of a storage mechanism refers to its ability to store an object for extremely long time periods. Resilience refers to its fault tolerance ability or its ability to retrieve the object completely even if a part of that object is lost due to any catastrophic failure like the disk failure. It is also important that this storage mechanism is able to store this object in a secure manner. In the current world usability of any storage mechanism is enhanced multiple times if it could be used from a web service. This thesis considers different techniques that provide each of these properties and proposes a storage mechanism that makes use of information dispersal techniques that is suited to store data securely with an emphasis on availability and resilience. A working prototype of this storage mechanism was developed as a part of this thesis and is made available as a library for program developers. This library provides APIs to store and retrieve data as well as a control API which can be used to query and set the configuration. The APIs to store and retrieve data also has a limited web interface which increases its usability to web developers. The performance of this prototype was measured and is presented using graphs and tables. Finally a demonstration of the applications of this prototype is also provided.

This is a Department of Computer Science Masters Defense.

Tropical cyclones continue to be a serious concern for the Nation, causing significant risk to life, property, and economic vitality. While NOAA has made steady improvements in forecasting track since 1990, intensity has lagged behind, primarily because a good track forecast is essential before addressing any intensity changes. However, over the last 5 years NOAA's track forecasts improved enough for us to now focus on intensity forecast improvements. Since the devastating 2004-2005 Hurricane Seasons NOAA developed a plan to improve forecasts of hurricane intensity, structure, and track in cooperation with other government and non-government partners. This Hurricane Forecasting Improvement Project (HFIP), is a 10-year project designed to accelerate improvements in one to five day forecasts for hurricane track, intensity, and structure and to reduce forecast uncertainty, with an emphasis on rapid intensity change because of its importance to emergency management amongst others. The HFIP Plan has been widely distributed and reviewed, with an alliance of the hurricane research and forecasting communities agreeing to move forward with its implementation. The Plan's strategy is to perform research into hurricane intensity change and rapid intensification mechanisms, exploit new observing systems, expand computing capacity, build higher resolution coupled models and ensembles, improve infrastructure for transitioning research to operations (R2O) and support operations-like systems to the research community (O2R), and broaden NOAA expertise and expand interaction with the external community.

This is a Department of Electrical and Computer Engineering presentation, and a CSMS Project Industrial Liaison Seminar. See Computer Science and Mathematics for Scientists. Refreshments will be served.

Neal Alewine and Harvey Ruback will discuss IBM's speech technology. Also present will be the IBM LA Grid program director Juan Caraballo.

Neal Alewine is an IBM Senior Technical Staff Member, Software Group Voice and DataPower Architect. Harvey Ruback is an IBM Senior Technical Staff Member, Systems and Technology Group Advanced Voice Architect. Juan F. Caraballo is the IBM Program Director for LA Grid - Corporate University and Innovation Programs. He was previously the Software Group Program Director for Enterprise Speech Solutions.

This is a CSMS Project Industrial Liaison Seminar. See Computer Science and Mathematics for Scientists. Refreshments will be served.

We will look at random number generation from the point-of-view of Monte Carlo computations. Thus, we will examine several serial methods of pseudorandom number generation and two different parallelization techniques. Among the techniques discussed with be "parameterization," which forms the basis for the Scalable Parallel Random Number Generators (SPRNG) library. SPRNG was developed several years ago by the author, and has become widely used within the international Monte Carlo community. SPRNG is briefly described, and the lecture ends with a short revue of quasirandom number generation. Quasirandom numbers offer many Monte Carlo applications the advantage of superior convergence rates.

Dr. Mascagni was born in Bologna, Italy. He has a Ph.D. in Mathematics from Courant Institute of Mathematics and has worked at the National Institute of Health and the Institute of Defense Analysis' Supercomputer Research Center. He is currently a professor in the department of Computer Science of Florida State University. Dr. Mascagni is on the editorial board of three journals in his field, and is on the Board of Directors of IMACS. He has been a visiting professor at the University of Padova in Italy, the University of Salzburg in Austria, and the Swiss Federal Technical Institute-Zurich in Switzerland, and is a consultant to industry and government

This is a joint presentation of The Center For Computational Science and the Department of Computer Science and co-sponsored by Rosenstiel School Of Marine And Atmospheric Science and the The Department Of Electrical And Computer Engineering

Joe Clarke will discuss his role in porting GNOME/GTK+ to the FreeBSD platform. As part of the discussion, the goals, structure and charter of the GNOME Project will be outlined.

Joe Clarke works at Cisco Systems, and is an expert in CiscoWorks LAN Management Solution and IOS embedded device management. His day job supports his interests in FreeBSD, including his work as Ports Manager, GNOME porter, and Tinderbox maintainer. Presented by the Department of Computer Science

Refreshments will be served.

Data cleaning is a critical component of Business Intelligence software. Specifically, the data cleaning step reconciles multiple representations of the same data and thereby ensures accurate data analysis. With the advent of the web, this problem has gained even more importance. For example, data cleaning technology is also used to capture typos and differences in representation when looking up addresses in an online address search. Traditionally, data cleaning has been driven by consultants and software that is custom made for specific vertical domains. In this talk, we take a different approach and propose a programming framework for data cleaning. We will identify some of the key aspects of such a programming framework.

Surajit Chaudhuri is a Principal Researcher and a Research Area Manager at Microsoft Research, Redmond. In 1996, Surajit started the AutoAdmin project on self-tuning database systems at Microsoft Research and along with his team developed novel automated physical design tuning technology. Their research led to the development of Index Tuning Wizard (Microsoft SQL Server 7.0, SQL Server 2000) and Database Tuning Advisor (SQL Server 2005, SQL Server 2008). More recently, along with his colleagues, Surajit has worked in the area of data cleaning. Their research on data cleaning has been incorporated in Microsoft SQL Server 2005 and SQL Server 2008. Surajit is also interested in the problem of search and querying information exploiting IR as well as DBMS techniques. Surajit did his Ph.D. from Stanford University and worked at Hewlett-Packard Laboratories, Palo Alto from 1991-1995. He is an ACM Fellow. He was awarded the ACM SIGMOD Contributions award in 2004 and a 10 year VLDB Best paper Award in 2007.

Refreshments will be served. All are invited.

Everyone is welcome. Competition, Pizza, Chun Li.
For more information contact adam _at_ mail.cs.miami.edu.

Dr. Kierchhoff presents a new generation of e-Sports-games. It is a combination of characteristics of real soccer players with modern AI technology. The user adds soccer knowledge for the next game while choosing formation, tactics, and training sessions for his team. Each game is simulated and visualized in a 3D Java applet within a web browser thereafter. This results into a unique game that has convinced the German Bundesliga (DFL GmbH) among others. Dr. Kierchhoff is one of the driving forces behind the "Official Bundesliga Manager", a game that has convinced more than 105,000 users since August 2007 and is running on www.bundesliga.de.

Users can create their own team from all 530 Bundesliga players and plays with this team to win the championship against 17 other teams in a weekly rhythm (in analogy to the real Bundesliga). The game also contains options to ascend/descend into different leagues according to the quality of the team (virtual 1./2. Bundesliga). The games have the same rhythm than the reality, however, the games will be played one day earlier.

Modern technology is the basis for the game. The players are software robots and act autonomously. They decide on their own with the help of modern AI technology which action will be executed within the next few seconds. The combination of reality with weekly (daily possible) updates of player data, the definition of the user with his formation and tactics and the autonomy of the software robots is brand-new and guarantees a unique experience for users.

The Official Bundesliga Manager is a combination of high tech artificial intelligence methods, an new 3D graphics engine, and elite sports. Artificial software robots are charged with weekly updated real data from the Bundesliga players. They then play autonomously their league games in a virtual world. (www.bundesliga.de).

The talk contains a technology demonstration and will then give insight into a vibrant industry sector by analyzing more than 120.000 customers. Dr. Kierchhoff will talk about potential markets and business opportunities in this sector. The talk underlines the importance for game programming in education.

This is another in the Department of Computer Science Pizza Seminar Series.

High quality 3D rendering requires massive computing resources. In order to render animations within a reasonable amount of time, the rendering process is often distributed among a cluster of computers, typically called a rendering farm. However, most individuals and small studios do not have the resources to purchase or lease a rendering farm. In the late 1990's, Java technology brought a hope that distributed applets could be utilized as an alternative to traditional network rendering models. Yet, this hope was never realized, nor was it fully implemented. Taking into account new developments in web application technology and the Sunflow renderer, this thesis will reexamine the possibility of distributed rendering applets. This thesis will suggest that distributed Java applets can effectively render projects across a collection of heterogeneous and geographically dispersed computers over the Internet. Moreover, this paper will present a prototype web application, called RenderWeb, that uses distributed applets to quickly render projects created in popular animation programs, such as Blender, 3D Studio MAX, and Softimage

This is a Department of Computer Science Masters Defense

Everyone is welcome. There will be games, pizza and zombies.

For more information contact adam _at_ mail.cs.miami.edu.

QoS (Quality of Service) control in WLAN (IEEE 802.11 Wireless LAN) is becoming increasingly important. Although previous research has attempted to increase total throughput, few studies have treated individual TCP/UDP flow QoS. EDCA in IEEE 802.11e might provide prioritized QoS functions that would partially address this problem. However, in uplink flow, which is defined as data moving from a terminal toward an Access Point, EDCA has limitations. These manifest themselves both across classes and in differentiated QoS control between terminals in the same class. Furthermore, 802.11e requires modification of terminals as well as other alterations proposed by other researchers. Instead of 802.11e or other modifications of 802.11, we propose an approach to controlling QoS that requires no terminal modifications or installation of additional software/hardware. The proposed idea is MAC-frame Receiving-Opportunity Control (ROC). Performance evaluation shows that the ROC causes some performance degradation in total WLAN throughput but can achieve not only QoS priority control but also arbitrary throughput performance. In particular, the ROC (in the MAC layer) can also permit different throughputs for high priority and low priority flows, conditioned on control processes in other layers. These may include rate adaptation (in the MAC layer) and TCP congestion control (in the TCP layer).

As the aging baby boomer generation approaches retirement age, health care providers are searching for ways to ease the burden of an increasingly older population. Subsequent generations are migrating away from their parents and grandparents, increasing the relevance of assisted-living facilities for elderly patients. Moreover, a rising life expectancy and dependence on a greater number of health professionals is contributing to a more expensive health care system, and depression and loneliness is now common among seniors. Researchers in the field of social robotics propose the use of robots to assist caregivers in menial tasks and to extend the independence and quality of life of aging individuals where possible.

As part of Humana's Rapid Prototyping Internship Program, we developed a system to evaluate the potential for a robotic companion's use in the home. Pleo, a robotic dinosaur manufactured by UGOBE, serves as the platform used for this prototyping. Reprogramming Pleo to perform the roles of both a health care tool and companion may provide an interface to technology that is more approachable for the elderly. We present the details and challenges in building the software used to enhance Pleo and integrate him into a system of devices that work together. The processes involved in creating new media for the robot will also be covered. In addition, we will discuss the structure and modifiability of the Pleo robot, including its limitations and advantages.

This is another in the Departmental Pizza Seminar series.

We present robust explicit construction of 3D configuration spaces using controlled linear perturbation. The input is two planar parts: a fixed set and a moving set, where each set is bounded by circle segments. The configuration space is the three-dimensional space of Euclidean transformation (translations plus rotations) of the moving set relative to the fixed set. The goal of constructing the 3D configuration space is to determine the boundary representation of the free space where the intersection of the moving set and fixed set is empty. To construct the configuration space, we use the controlled linear perturbation algorithm. The controlled linear perturbation algorithm assigns predicate polynomial signs that are correct for a nearly minimal input perturbation. The output of the algorithm is a consistent set of polynomial signs. This approach is algorithm-independent and overhead over traditional floating point methods is reasonable.

If the fixed and moving sets are computer representations of physical objects, then computing the configuration space greatly aids in many computational geometry problems. Our main focus of computing the configuration space is for the path planning problem. We must find if a path exists from the start to the goal, where the fixed set is the obstacle, and the moving set is the object trying to reach the goal.

This is a Department of Computer Science Ph.D. Defense

One aspect of Automated Reasoning deals with writing computer programs that can answer questions using logical reasoning. An Automated Theorem Proving (ATP) system translates a question to be answered to a first-order logic conjecture, and attempts to prove the conjecture from the set of axioms provided. If a proof is found an answer extraction method can be applied to answer the original question. If more than one proof is possible, more than one answer may need to be extracted. Most ATP systems can find only a single answer for a question. To extract multiple answers, users may have to re-invoke the ATP system with a modified question. This work describes some ways to achieve multiple-answer extraction. An answer extraction program, called the multi-answer system, has been developed to automate the process of answer extraction. It enables users to conveniently extract different answers in a variety of ways. Extracting more than one answer is useful but it is also helpful if the extracted answers can be compared to a list of user's answers. The multi-answer system uses set operations like union, intersection, subset, superset, element, and difference to perform answer comparison.

This is a Department of Computer Science Masters Defense

With the number of economic, environmental and foreign policy crises at the moment, have you thought about how you as an individual can directly contribute? As a technologist, have you ever thought about how you could save a life, or even better, many? If you have, think about how to promote wellness in your community (health, environment, security and happiness). With all of the crises happening around us at the moment, this is one problem on which we as individuals can have a dramatic effect, for ourselves and those around us.

Within Humana, the Innovation Center is a group of business and technology leaders who are looking at how to engage people to improve their wellness. Within the Emerging Technology Applications group we use digital media and emerging technologies such as computer games, social media, virtual worlds, social robots and the like. We run a paid Rapid Prototyping Internship Program (RPIP) that is designed to provide students with the chance to temper their skills on problems that have important and real world applications.

In 2008, three University of Miami computer science students, Justin Stoecker (BSc 2009), Richard Roesler (BSc 2009) and Adam McMahon (MSc 2009) undertook internships. Adam used Sims2 to design a game to show the health and economic benefit of using technology to assist the elderly to stay in their homes when threatened with an assisted living facility. Justin and Richard developed a prototype system for using the Pleo social robot as an alternative interface for the elderly to use technology in the home such as medication reminders, wireless scales and blood pressure cuffs. Justin also developed a memory game for the Pleo.

In the seminar, Adam, Justin and Richard will present the results of their work. The details of the upcoming RPIP'09 will also be discussed. If you are interested in applying for a paid position, please come and see the type of projects we are interested in pursuing.

This is a CSMS Project Industrial Liaison Seminar. See Computer Science and Mathematics for Scientists. Refreshments will be served.

The presentation in this pizza seminar will be split in two consecutive parts. The first presents research in the field of knowledge representation and high-level scene interpretation for autonomous agents in dynamic physical environments. The application context will be robotic soccer. To be more precise, the RoboCup 3D soccer simulation league where the University of Bremen participated with our Virtual Werder 3D agent team from 2004-2007.

After a brief introduction to the domain, I'll argue that a quantitative world model alone is inadequate for agents interacting in a highly dynamic physical environment such as (simulated) soccer. Without further efforts targeted at a hybrid knowledge base, the agents are ill-equipped to apprehend extended motion incidences. To meet this need, I propose a knowledge processing pipeline ranging from relevance-driven compilation of a concise, basic qualitative scene description to a knowledge-based detection of complex events, actions and action sequences. The detection is thereby conceived as a spatio-temporal pattern matching problem which can be solved using logic programming. A methodology for the formalization of motion patterns and their inner composition is introduced and consequently applied in a knowledge engineering process to capture human expertise about a large set of soccer-specific motion situations. The formalization scales in a natural way from low-level events towards strategic plays. I'll also propose an efficient knowledge-based detection strategy whose bottom-up search is based on the interrelationships among modeled patterns. Seizing a full-featured prototype, a thorough statistical evaluation of analysis quality and execution performance was conducted in realistic application scenarios. Results were promising with respect to precision and recall, using - as a baseline - precise, complete sensor input at a 5Hz update frequency. Also, the analysis is robust against noisy, incomplete input as encountered in application scenarios such as the RoboCup 3D Soccer Simulation League, howing a defensible graceful quality degradation. The approach is also shown suitable for non-restricted real-time employment.

The second part of the presentation will retain the focus on autonomous agent and multi-agent systems. Yet, as it is motivated by my current occupation as a research assistant in the Collaborative Research Center entitled 'Autonomous Cooperating Logistic Processes', the application domain will change to transport logistics.

The CRC is concerned with research on new paradigms that can replace and effectively optimize traditional centralized management and control of complex supply networks in emergent, fast-moving, globalized markets. The basic idea pursued in our research group is a distribution of control and thus a transfer of autonomy from the human controller to the logistic objects themselves. These objects, which might be means of transport, freight containers or (collections of) bulk goods, are thereby modeled as intelligent software agents which pro-actively assume responsibility for transport logistic tasks such as the efficient and adaptive routing of goods from the production facilities in far east to the end user market in Germany.

I will try and sketch current tentative ideas to provide heterogeneous teams of agents which can be collectively thought of as acting as a freight forwarding company could adapt to a dynamically changing logistic environment via a collaborative multi-agent learning process. The adaption is conceived as running concurrently to the primary logistic task of the agent community. Depending on their individual circumstances/capabilities (mobile, resource-bounded agents due to live on on-board embedded systems or stationary high-performance agents, located at transshipment centers), the distinct agent types contribute to the global task of team adaption in several ways. For instance, as experience canvassers or as local learners/knowledge miners. The concept strives to bring together in a beneficial way research from multi-agent systems and multi-agent-based simulation, knowledge representation, learning and data/association rule mining.

This part of the talk is intentionally presented at an early stage of concept formation in order to draw comments and ideas from the audience.

This is another in the Department of Computer Science Pizza Seminar series

Dr. Visser presents a new generation of e-Sports-games. It is a combination of characteristics of real soccer players with modern AI technology. The user adds soccer knowledge for the next game while choosing formation, tactics, and training sessions for his team. Each game is simulated and visualized in a 3D Java applet within a web browser thereafter. This results into a unique game that has convinced the German Bundesliga (DFL GmbH) among others. Dr. Visser is one of the driving forces behind the "Official Bundesliga Manager", a game that has convinced nearly 100.000 users since August 2007 and is running on www.bundesliga.de. Users can create their own team from all 530 Bundesliga players and plays with this team to win the championship against 17 other teams in a weekly rhythm (in analogy to the real Bundesliga). The game also contains options to ascend/descend into different leagues according to the quality of the team (virtual 1./2. Bundesliga). The games have the same rhythm than the reality, however, the games will be played one day earlier.

Modern technology is the basis for the game. The players are software robots and act autonomously. They decide on their own with the help of modern AI technology which action will be executed within the next few seconds. The combination of reality with weekly (daily possible) updates of player data, the definition of the user with his formation and tactics and the autonomy of the software robots is brand-new and guarantees a unique experience for users. The Official Bundesliga Manager is a combination of high tech artificial intelligence methods, an new 3D graphics engine, and elite sports. Artificial software robots are charged with weekly updated real data from the Bundesliga players. They then play autonomously their league games in a virtual world. (www.bundesliga.de). The talk contains details about the technology, an online demonstration, and an outlook within the context of the Graphics and Games Track at UM.

Ubbo Visser is currently a Visiting Associate Professor at the Department of Computer Science since August 2008. He received his Habilitation in Computer Science (qualification for Professor) from University of Bremen in 2003, a PhD in Geoinformatics from University of Muenster in 1995, and a MSc in Geography (Landscape-ecology) from University of Muenster in 1988. His research specialization is in artificial intelligence, more specifically on knowledge representation and reasoning. He is interested in the combination of symbolic and sub-symbolic technologies in the domain areas of "Semantic Web" and "Multiagent Systems". His focus in the Semantic Web area lies in the development of methods that combine terminological logics and spatio-temporal representation and reasoning techniques. The focus in the Multiagent Systems area lies in the development of techniques for agents that act in highly dynamic and real-time environments, such as mobile robots and games.

This is another in the Department of Computer Science Pizza Seminar series

Graph based semi-supervised learning (GBSSL) has attached considerable interests in machine learning, data mining and computer vision communities in recent years. In this talk, I will introduce the basic configurations in GBSSL, and a representative algorithm -- label propagation, and a multilevel scheme to make it more efficient. The applications of GBSSL in image segmentation, text classification and information retrieval will also be introduced in this talk.

Dr. Fei Wang has got his Ph.d. degree from Tsinghua University, Beijing, China in 2008. He is now a postdoctoral researcher in School of Computing & Information Sciences, Florida International University. His main research interests include machine learning, data mining, information retrieval and pattern recognition. He has published over 40 papers in the top journal & conferences of the relevant field.

This is another in the Department of Computer Science Pizza Seminar series

A brief overview of Intellectual Property (IP) Law including patents, trademarks, and copyrights. What is Intellectual Property? What role does an IP attorney play? Why is an engineering or scientific degree needed to become a patent attorney? Specific focus aimed at the process of becoming a patent attorney or agent, as well as the benefits and obstacles of pursuing this career choice.

This is a CSMS Project Industrial Liaison Seminar. See Computer Science and Mathematics for Scientists. Refreshments will be served.

A human cognitive model that can robustly execute basic tasks would make a valuable contribution to three interrelated areas of endeavor, robust agent simulations, human-computer interfaces, models of human cognition. The centerpiece of the human execution of natural tasks is the fluid use of gaze to direct and select appropriate behaviors, but little is known about the control mechanisms responsible for the gaze sequences that do this. For example, a difficult problem for all models of gaze control, intrinsic to selective perceptual systems, is how to detect important stimuli without consuming excessive computational resources. We show in both real and virtual walking environments, that human gaze patterns are tightly controlled by task demands and remarkably sensitive to the probabilistic structure of the environment. One way to understanding this use of gaze is to create a model of a human that has a sufficient amount of complexity so as to be capable of generating such behaviors. Recent technological advances in graphics models that simulate extensive human capabilities can be used as platforms from which to develop synthetic models of visuo-motor behavior. Currently such models can capture only a small portion of a full behavioral repertoire, but for the behaviors that they do model, they can describe complete visuo-motor subsystems at a useful level of detail. The value in doing so is that the body's elaborate visuo-motor structures greatly simplify the specification of the abstract behaviors that guide them. The net result is that, essentially, one is faced with proposing an embodied "operating system" model for picking the right set of abstract behaviors at each instant. We outline one such model. A centerpiece of the model uses vision to aid the behavior that has the most to gain from taking environmental measurements. Preliminary tests of the model against human performance in realistic VR environments show that main features of the model show up in human behavior.

Colloquium sponsored by the University of Miami Departments of Computer Science and of Electrical and Computer Engineering and the Center for Computational Science

I will talk about the problem of using shared resources for private computations. This problem has been studied in two closely related models: locally random reductions (LRRs) and private information retrieval (PIR) schemes.

In both models, there are two parties that communicate with each other. The first party consists only of a single client and the other party consists of one or more resources (which could be, for instance, oracles or servers). The client wishes to solve some problem on an input that is private to the client by interacting with the information resources. The crucial privacy requirement is that at the end of all communication each resource must not learn anything about the actual input, except possibly the length of the input. It is considered infeasible for the resources to simply send all information (or computational aids) that would be required by the client to solve the problem on any possible input of a given length.

The solution to this puzzle makes use of randomness in a crucial way. Basically, for any given input the client sends different random queries to different resources and uses the answers to these queries to solve the problem. The probability distribution of the random query(ies) sent to a single resource depends only on the length of the input. If we assume that the resources do not collude to learn the input of the client and that thus each resource gets to know only its own queries, then the resources do not learn anything about the actual problem instance. The challenge in constructing good LRRs and PIR schemes is to devise mechanisms with as low as possible communication requirement.

I will explain and motivate these models, describe known results related to these models, and present my recent results on the complexity of languages that have locally random reductions (LRRs) of certain types.

About the speaker: Dr. Rahul Tripathi is an assistant professor of Computer Science and Engineering at the University of South Florida (USF), Tampa, FL. His research interests are in algorithms and computational complexity theory. Dr. Tripathi holds a B.Tech. (2000) in Computer Science and Engineering from the Indian Institute of Technology, Kanpur, India, and an M.S. (2003) and Ph.D. (2005) in Computer Science from the University of Rochester, NY.

This is another in the Department of Computer Science Pizza Seminar series

Zac Brown, an undergraduate student in the University of Miami's Department of Computer Science recounts his experience as an intern with the world's most well known search engine and internet ad provider, Google. He will discuss his time there, the project he worked on and provide some insight into what Google is doing, where Google is going and some fun facts about Google. He may even provide confirmation to any rumors people have heard, provided his NDA permits him to do so. If you've ever wondered what it's like to work at Google, how they develop software, or even just how they make money, this is your chance to talk to a past Google employee.

This is another in the Department of Computer Science Pizza Seminar series

Virtual environments have the way we understand and interact with data by transforming it into "in-our-face-and-hands" information. These environments have also revolutionized the way we communicate that information to others. We are now able to gain insight in particular problem domains like never before: we can collaborate with our colleagues, locally or remotely, and we can better explain our discoveries to others through powerful virtual reality experiences. Today, the practical implementation of these capabilities is still evolving, but a growing interest and acceptance by industry is accelerating the development efforts. The non-academic communities are demanding virtual reality and virtual environments technology that is robust and stable enough to come out of research laboratories and be put to work on industrial settings. This, combined with today's limitations of traditional sources of academic funding, presents a unique opportunity for universities open to widen their academic and research models towards applied research and entrepreneurship of their faculty and students. This talk reflects Dr. Cruz's experiences and personal assessment on the current state and trends of virtual reality technology, her challenging career as a non-traditional faculty, and the opportunities to develop strong integrated academic and research programs to capitalize in this emerging field.

Dr. Carolina Cruz-Neira is a pioneer in the field of Virtual Reality (VR). She started in the early 90's being the lead designer of the CAVE Virtual Reality Environment, and the software engineer of CAVELibs, the first software API to run such complex virtual environments. Until 2005, Dr. Cruz was the Stanley Chair in Interdisciplinary Engineering and the Associate Director and co-founder of the Virtual Reality Applications Center at Iowa State University (ISU). Currently, Dr. Cruz is the Executive Director and Chief Scientist of the Louisiana Immersive Technologies Enterprise (LITE) and the William Hansen Hall Endowed Chair in Computer Engineering at the University of Louisiana at Lafayette.

Colloquium sponsored by the University of Miami Department of Computer Science and the Center for Computational Science.

This is another in the Departmental Pizza Seminar series.

We will look at random number generation from the point-of-view of Monte Carlo computations. Thus, we will examine several serial methods of pseudorandom number generation and two different parallelization techniques. Among the techniques discussed with be 'parameterization,' which forms the basis for the Scalable Parallel Random Number Generators (SPRNG) library. SPRNG was developed several years ago by the author, and has become widely used within the international Monte Carlo community. SPRNG is briefly described, and the lecture ends with a short revue of quasirandom number generation. Quasirandom numbers offer many Monte Carlo applications the advantage of superior convergence rates.

Dr. Mascagni was born in Bologna, Italy. He has a Ph.D. in Mathematics from Courant Institute of Mathematics and has worked at the National Institute of Health and the Institute of Defense Analysis's Supercomputer Research Center. He has currently a professor in the department of Computer Science of Florida State University. Dr. Mascagni is on the editorial board of three journals in his field, is on Board of Directors of IMACS. He has been a visiting professor at the University of Padova in Italy, the University of Salzburg in Austria, and the Swiss Federal Technical Institute-Zurich in Switzerland, and is a consultant to industry and government.

This is another in the Departmental Pizza Seminar series.

We will present both an experimental framework for the study of on-line optimisation algorithms for packet routing, and theoretical results on "best paths" and on travel times in random network environments. The experimental "cognitive packet network" (CPN) test-bed at Imperial College will be described, and the CPN routing algorithm will be presented together with detailed experimental results concerning its performance. We shall also show how Brownian motion can be used to predict travel delays in uncertain wired and wireless networks, and describe an application to adaptive routing in wireless sensor networks. This work is currently funded by the US/UK International Technology Alliance funded by DoD and IBM.

Prof Erol Gelenbe FIEEE, FACM, FIEE, is the Professor in the Dennis Gabor Chair at Imperial College. A graduate of the Middle East Technical University, Ankara, Turkey, he is an elected Member of Academia Europaea and of the Turkish Academy of Sciences, and has received honoris causa doctorates from the University of Rome, the University of Liege (Belgium), and Bogazici University (Turkey). His research spans both computer networks and bio-informatics. A Member of Eta Kappa Nu, he has been decorated by the President of Italy with the honours of "Grand Officer of the Order of the Star of Italian Solidarity" and of "Commander of Merit of the Republic of Italy". In France he has received the honour of Officer of the Order of Merit, and has won the Grand Prix France Telecom of the French Academy of Sciences. Prof Gelenbe is on the editorial board of the Proceedings of the Royal Society, Acta Informatica, Telecommunication Systems and several other journals; he is Editor-in-Chief of The Computer Journal (British Computer Society).

This is another in the Departmental Pizza Seminar series.

Almost everyone has to give a public presentation at some time. Graduate students have to defend their theses, research students have to present their results, and many jobs require presentations. It is common to have little or no experience when you give your first presentation, and you may even be a little nervous! This talk is aimed at (graduate, research, and other) students. It describes how to give a successful talk, in a simple standard format. This talk does not try to teach general speaking skills, nor impose any personally preferred techniques. It covers the structure of a talk, the use of visual aids, speaking technique, and how to cope with questions.

This is another in the Departmental Pizza Seminar series.

Data clustering is an important task in many disciplines. A large number of studies have attempted to improve clustering by using the side information that is often encoded as pairwise constraints. However, these studies focus on designing special clustering algorithms that can effectively exploit the pairwise constraints. We present a boosting framework for data clustering, termed as BoostCluster, that is able to iteratively improve the accuracy of any given clustering algorithm by exploiting the pairwise constraints. The key challenge in designing a boosting framework for data clustering is how to influence an arbitrary clustering algorithm with the side information since clustering algorithms by definition are unsupervised. The proposed framework addresses this problem by dynamically generating new data representations at each iteration that are, on the one hand, adapted to the clustering results at previous iterations by the given algorithm, and on the other hand consistent with the given side information. Our empirical study shows that the proposed boosting framework is effective in improving the performance of a number of popular clustering algorithms (K-means, partitional SingleLink, spectral clustering), and its performance is comparable to the state-of-the-art algorithms for data clustering with side information.

Dr. Rong Jin is an assistant professor of Computer Science and Engineering at Michigan State University. He is conducting research in the areas of statistical machine learning and its application to information retrieval. He has published over eighty research articles. Dr. Jin holds a B.A. in Engineering from Tianjin University in China, an M.S. in Physics from Beijing University in China, and an M.S. and a Ph.D. in Computer Science from Carnegie Mellon University. He received the NSF CAREER Award in 2006.

This is another in the Departmental Pizza Seminar series.

Many transform-based compression techniques have been investigated and devised for ECG (Electrocardiogram) signal compression. However, the Burrows-Wheeler Transformation has not been completely investigated. In this talk, we show that when compressing ECG signals, utilization of linear prediction, Burrows-Wheeler Transformation, and inversion ranks yield better compression gain in terms of weighted average bit per sample than recently proposed ECG-specific coders.

Actuaries help insurance companies in many areas, such as accounting, claims, lawsuits, investments, mergers & acquisitions, and premium calculations. Join Jonathan Jannarone, UM math graduate and Vice President of Life Actuarial at Assurant, as he explains how actuaries apply math, statistics, and computer science to their daily job. Learn about how to become an actuary, consistently picked as one of the top five occupations in the country.

This is a CSMS Project colloquium

As governments and the health care industry struggle with the spiraling cost of health care, proactive approaches such as preventative care, early intervention and treatment adherence procedures are necessary if we are to reign in ballooning expenditure and protect ourselves against epidemic diseases. As we face new waves of long term debilitating diseases in the developed world such as obesity, diabetes, Alzheimer's and cardio-vascular disease, our ability to identify those at risk, to intervene, educate and change behavior, and to assist the affected to maintain their treatment regiments will become vital to keeping people and our economy healthy. In this seminar, we will discuss two programs being developed ay Humana, Inc. The Visual Analytics program seeks to give analysts the ability to analyze, correlated with external data sources, and report on the massive amounts of data collected on our member population in an interactive environment. New tools, techniques and technologies are being explored to identifying patterns, trends and at-risk groups to focus resources and intervention programs. The Games for Health program promotes understanding, fitness and cognitive maintenance through the use of computer games, exploring this technology as a new communication medium.

This is another in the Departmental Pizza Seminar series.

The Internet went well beyond a technology artifact, increasingly becoming a social interaction tool. These interactions are usually complex and hard to analyze automatically, demanding the research and development of novel data mining techniques that handle the individual characteristics of each application scenario. Notice that these data mining techniques, similarly to other machine learning techniques, are intensive in terms of both computation and I/O, motivating the development of new paradigms, programming environments, and parallel algorithms that support scalable and efficient applications. In this talk we present some results that justify not only the need for developing these new techniques, as well as their parallelization.

Wagner Meira Jr. obtained his PhD from the University of Rochester in 1997 and is currently an Associate Professor at the Computer Science Department at Universidade Federal de Minas Gerais, Brazil. His research focuses on scalability and efficiency of large scale parallel and distributed systems, from massively parallel to Internet-based platforms, and on data mining algorithms, their parallelization, and application to areas such as information retrieval, bioinformatics, and e-governance.

Many social interactions that are ephemeral in the physical world are recorded and accessible in the online world. The widespread use of online systems such as blogs, wikis and social networking sites provides a treasure trove of information about human behavior. This talk discusses some recent studies of large-scale online social systems, and speculates about what these studies suggest about human interactions more generally.

There will be a reception following the lecture. This colloquium is free and open to the public.

Starting in the 1990s, a large number of young scientists left the academic life for jobs with a score of companies that wanted to merge biology with computer science to create a new branch of science - bioinformatics. Accomplishments, such as the determination of sequences of the 3 billion chemical base pairs that make up human DNA, were realized through the combined efforts of life and computer scientists.

Flesh and bones start as protein. Inside each cell is a sort of instruction book that tells the cellular machinery what type of protein to produce and, more importantly, when. That instruction book is written with a 4-letter alphabet: A, C, G, T. Reducing life to DNA reduces life to numbers. And once a problem can be stated numerically, it can be mathematically modeled, stored in computer databases and analyzed with a variety of software tools.

Today, more than even, the field of bioinformatics offers exceptional opportunities for scientists that want to contribute in understanding the natural world. Outstanding challenges, including gene regulation and function, protein synthesis, interaction and conservation, disease-susceptibility prediction based on gene sequence variation and even evolutionary conservation, just to name a few, are all areas where major advances will happen in silico as much as in vitro. And this fact is acknowledged by both academic and industrial forces, which are currently recruiting and offering a variety of well rewarded positions to qualified researchers bridging the cultural worlds of life and mathematical sciences.

This is a CSMS Project colloquium

Modern markets require businesses to stay on the edge of technology. At the same time, C-Level executives are demanding lower IT budgets. Management is forced to downsize their in-house IT departments and outsource the day to day maintenance and configuration to Value Added Resellers (VARs) . This shift towards greater reliance on external resources has made the VAR role increasingly more demanding and complicated, as it covers virtually every aspect of a corporation's IT need. In this talk, I will describe the current landscape for IT VARs and how technology is changing the workplace. Agenda: Segmenting the market space; the IT layers of a mid-size corporation; major players in each layer, in particular Microsoft, CISCO and Citrix; VAR survival skills; Conclusion.

This is a CSMS Project colloquium

Autonomous mobile robots with the capacity to perform specific tasks such as monitoring security areas or assist in rescue scenarios have become increasingly important. Preparing one robot to have these abilities involves a variety of research questions. How does the robot know where it is? How does the robot get from A to B? What kind of action does the robot choose if an unforeseen situation arises? What is the best locomotion algorithm? Can the robot predict situations and, in general how can we measure the performance of these robots? The talk comprises a summary of a number of research projects that we have carried out at the University of Bremen. We will present problems, research approaches and solutions tackling localization, navigation, decision-making, bi-ped walking as well as situation recognition and prediction. We present how we have explored these issues on both robotic and software agents, and show examples of solutions arrived at within the context of soccer playing robots. Indeed, RoboCup has been fostering research on these problems by organizing competitions yearly, in a similar spirit that chess competitions had been used in the past decades to provide a performance measure of the Artificial Intelligence of the system. Because the soccer environment is adversarial with constant changes it demands for adequate approaches for a team of robots (rather than for one single robot). It provides a platform to evaluate how the research questions described in this talk can be explored on multi agents that communicate and cooperate. We then discuss how these results are relevant to other domains, and how they can be used and generalized in other domains such as the traffic domain or the medical domain.

Ubbo Visser is a Privat-Dozent (Assistant Professor) at the Department of Mathematics and Computer Science, University of Bremen, Germany since 1999. He received his Habilitation in Computer Science (qualification for Professor) from University of Bremen in 2003, a PhD in Geoinformatics from University of Muenster in 1995, and a MSc in Geography (Landscape-ecology) from University of Muenster in 1988. His research specialization is in artificial intelligence, more specifically on knowledge representation and reasoning. He is interested in the combination of symbolic and sub-symbolic technologies in the domain areas of "Semantic Web" and "Multiagent Systems". His focus in the Semantic Web area lies in the development of methods that combine terminological logics and spatio-temporal representation and reasoning techniques. The focus in the Multiagent Systems area lies in the development of techniques for agents that act in highly dynamic and real-time environments, such as mobile robots. Dr. Visser has published over 75 scientific articles and has received public research funding at international (Australia, European Commission), national (Germany), and regional (Bremen State) levels - including DFG (German Research Council), BMBF (Federal Ministry for Education and Research), ARC (Australian Research Council), and also from Industry. He has chaired a variety of international conferences, workshops, tutorials and symposia (e.g. RoboCup, IJCAI- and ECAI-Workshops) and he has won multiple prizes and awards for outstanding research papers and software engineering (e.g. best artificial intelligence application in Germany, awarded by the German AI society). He is the Co-Founder of three software companies that develop products based on modern AI-technologies (Conterra Ltd., ProPlant Ltd., Coach and Win Ltd.). He is a trustee of the RoboCup Federation and an Executive Member of the Media & IT Association of the state of Bremen. He is the Co- Editor of the German Journal of Artificial Intelligence and member of the editorial board of the International Journal on Semantic Web and Information Systems.

Both the increase in civilian air traffic and the desire for improved routing and scheduling of aircraft put larger and larger demands on air traffic control (ATC). Automatic Dependent Surveillance - Broadcast (ADS-B) is a technique developed to meet the resulting demand for better information about the air situation. Civilian aircraft have a strong desire to be visible to ATC, and are willing to contribute to that end. This is already used in secondary radar, where aircraft transponders actively reply to radar requests and provide air traffic control with additional information like the aircraft identity and altitude. ADS-B delegates much more responsibility to the aircraft. The aircraft periodically determines its own position using a satellite-based navigation system, and broadcasts this information. The ADS-B ground station is a passive device that receives and decodes this signal, and forwards the information to ATC. ADS-B sensors can be cheap, compact, and only have minimal requirements on location. They can provide very detailed information about the air situation even in situations where radar coverage cannot effectively be achieved. This talk presents some of technical aspects of ADS-Band discusses how to build a reliable ATC infrastructure with ADS-B.

This colloquium is presented jointly by the Department of Computer Science and the Department of Electrical and Computer Engineering.

I will describe our research in computer-aided mechanical design. Mechanical design is the task of devising an assembly of parts that performs a function reliably and economically. It is a ubiquitous activity with applications in mechanical, electrical, and biomedical engineering. Our research addresses the core design task of kinematic analysis. Kinematic analysis determines the positions and orientations at which the parts of a system touch and the ways that the touching parts interact. It is a computational bottleneck in mechanical design, especially in systems with complex part shapes, tight fits, and contact changes. We have developed a general kinematic analysis method based on configuration space computation. The method incorporates efficient algorithms for function validation, tolerancing, parameter synthesis, and redesign. I will illustrate these capabilities on industrial applications in gearshift design (with Ford Motors) and micro-mechanism design (with Sandia National Laboratory).

Joint work with Leo Joskowicz, Hebrew University.

This is a talk on a graduate thesis in computational geometry. Arrangement construction is one of the fundamental problems in computational geometry, but can be very difficult in the presence of high algebraic degree and degenerate input. Numerical precision and the challenge of designing an algorithm that works in more then two dimensions can also present a significant challenge. This talk will present an arrangement algorithm that is robust, scalable in the size of input, and is simple enough to be extended beyond two dimensions in future research. The input is a set of continuous polynomials. The output is an input perturbation direction such that perturbing the input in the derived direction for a small period of time eliminates all degeneracies and numerical ambiguities. A perturbation direction is obtained by a process of iterative perturbation of input. Each perturbation is computed by solving a set of linear equations using the CPLEX library. The algorithm is fast and can handle highly degenerate and non-robust input in a simple, uniform manner.

This is another in the Departmental Pizza Seminar series.

In my presentation I will be discussing the digital scrapbook that I created for the Filipino Student Association. I will be giving some background information about the project and why I chose this project, and I will show a brief demonstration of the product. I will then discuss how I made the book using Photo Impact Pro and Macromedia Flash and give an overview of the creation process. After that, I will discuss the additions to the project and show demonstrations of their functionality. This project will be placed on the website of the Filipino Student Association so that all members can enjoy the scrapbook and the game. It will also be accessible to non-members who can learn about the club and about Filipino culture.

My project consists on creating a system for rating TPTP problems and SPC systems. The program is provided a file, containing a huge amount of data about the systems and the problems. This data contains, for example, for each system the problems it has been tested with and if the system can solve the problem or not. With this data, my program has to rate the systems and the problems. The problems are given a rating depending on the difficulty, and the systems are given a rating depending on the number of problems they solve. Once I have calculated the ratings, I gave to print it with a specific format. The issue of this project is the efficiency. Because of the large amount of data, the system has to be very efficient in order to process all the data and give the output in a reasonable time.

MiamiVideo games have been around for decades and have become a staple of entertainment across the globe. Ever wonder how they work? It all begins with the game engine. This is a crucial component of any serious game and is responsible for everything from graphical output to level management. This talk is aimed at anyone with a desire to see beyond what the player sees and learn techniques to use when building their own game engine. Topics include game state management, data organization, sprite animation, the 3D rendering pipline, character mechanics, input and sound as well as game implementation techniques. The discussion will conclude with a demo of an action adventure RPG named "Hidden in Time" developed using Jorge Jauregui's Substance Game Engine.

This is another in the Departmental Pizza Seminar series.

The wide spread use of computers and digital technology has lead way to the binding of audio and computer programming. Computer software now runs audio recording (Pro Tools), audio storage (hard drives) and audio reproduction (Ipod). Traditional computer programming teaches the fundamentals of manipulating numbers, printing out text and maybe even reading from and writing to a file. This lays the foundation for a student to perform audio programming, but how does one go to the next step? How is it possible to read and write from audio files? How are digital audio files encoded? How is it possible to synthesize audio on computer's sound card? The answer to these questions can be found by using C libraries to manipulate audio and by preparing to program complex software by learning the benefits of C++.

This is another in the Departmental Pizza Seminar series.

Almost everyone has to give a public presentation at some time. Graduate students have to defend their theses, research students have to present their results, and many jobs require presentations. It is common to have little or no experience when you give your first presentation, and you may even be a little nervous! This talk is aimed at (graduate, research, and other) students. It describes how to give a successful talk, in a simple standard format. This talk does not try to teach general speaking skills, nor impose any personally preferred techniques. It covers the structure of a talk, the use of visual aids, speaking technique, and how to cope with questions.

This is another in the Departmental Pizza Seminar series.

This talk describes the design, implementation, and testing of a system for selecting necessary axioms from a large set also containing superfluous axioms, to obtain a proof of a conjecture. The selection is determined by semantics of the axioms and conjecture, ordered heuristically by a syntactic relevance measure. The system is able to solve many problems that cannot be solved alone by the underlying conventional automated reasoning system.

This is another in the Departmental Pizza Seminar series.

Emergence of high-throughput experiments and resulting databases capture relationships and interactions between biomolecules. These interactions enable modeling and analysis of a cell from a systems perspective - generally using network models. In this talk, we focus on development of computational tools and statistical models for comparative analysis of molecular interaction networks. These tools target understanding of functional modularity in the cell by extracting novel information from massive amounts of interaction data, through integration of cellular organization, functional hierarchy, and evolutionary conservation.

We first discuss the problem of identifying conserved sub-networks in a collection of interaction networks belonging to diverse species. The main algorithmic challenges here stem from the NP-hard subgraph isomorphism problem that underlies frequent subgraph discovery. Three decades of research into theoretical aspects of this problem has highlighted the futility of syntactic approaches, thus motivating use of semantic information. Using a biologically motivated homolog contraction technique for relating proteins across species, we render this problem tractable. We experimentally show that the proposed method can be used as a pruning heuristic that accelerates existing techniques significantly, as well as a standalone tool that conveys significant biological insights at near-interactive rates.

With a view to understanding the conservation and divergence of modular substructures, we also develop network alignment techniques, grounded in theoretical models of network evolution. Through graph-theoretic modeling of evolutionary events in terms of matches, mismatches, and duplications, we reduce the alignment problem to a graph optimization problem and develop heuristics to solve this problem efficiently. In order to assess the statistical significance of the patterns identified by our algorithms, we probabilistically analyze the distribution of highly connected and conserved subgraphs in random graphs. Our methods and algorithms are implemented on various platforms and tested extensively on a comprehensive collection of molecular interaction data, illustrating their effectiveness in terms of providing novel biological insights as well as computational efficiency.

Mehmet Koyuturk received his B.S. (1998) and M.S. (2000) degrees in Electrical and Electronics Engineering, and Computer Engineering, respectively, from Bilkent University, Turkey. During his graduate studies at the Department of Computer Science at Purdue University, he worked on a number of problems in the areas of Computational Biology and Bioinformatics, Parallel and Distributed Computing, and Scientific Computing. His thesis focused on algorithmic and analytical aspects of comparative analysis of biological networks. His collaborations with domain experts in this area resulted in several significant publications and software tools. Since receiving his Ph.D. in August 2006, he has been a post-doctoral research associate in the same department.

This is joint work with Yohan Kim, Shankar Subramaniam (University of California, San Diego), Wojciech Szpankowski, and Ananth Grama (Purdue University) and is supported by the National Institutes of Health.

Many complex systems can be represented as networks, where the nodes are the elements in a system, and the edges represent relationships between pairs of elements. Examples include social networks, protein-protein interaction networks, and the world-wide web. Much effort has been devoted to the study of topological properties that seem to be common to many networks, such as the small-world property and power-law degree distributions. Another important property that has drawn a great deal of interest recently is the so-called community structure, i.e. the existence of some natural division of a network such that nodes in each sub-network are highly associated among themselves, while having relatively fewer/weaker connections with the rest of the network. Automatically identifying such communities is fundamental for revealing the relationships between the structure and function of complex networks, with many applications in different disciplines such as sociology, biology, and computer science.

In this talk, I will discuss the conceptual and algorithmic challenges in community discovery, i.e. how to define communities, and how to identify them, and present our recent contributions in addressing these challenges. I will show several real applications of our methods in biology and other areas, and demonstrate the advantages of our methods against the existing approaches. Furthermore, I will show that the members of the same community often have very strong functional ties, which shed lights on the organizing principles of the system, and provide key insights about the functions of some previously uncharacterized members. I will conclude with an overview of my research interests and plan of future works.

Bio: Jianhua Ruan is currently a PhD candidate in the Department of Computer Science and Engineering at Washington University in St Louis. He received his B.S. degree (1998) in Biology from University of Science and Technology of China, and M.S. degree (2002) in Computer Science from California State University. His current research interests in computational biology and bioinformatics include (1) structural and functional properties of biological networks, (2) reverse-engineering of gene transcriptional regulatory networks, and (3) RNA structures and functions.

The talk consists of two main parts:

Genomic sequence classification and analysis
Microorganisms dominate the biosphere, yet most have not been identified or studied. Traditional methods for culturing and characterizing microorganisms limit analysis to those that will grow under laboratory conditions, which represent less than 1% of all microorganisms. In this presentation, I will show an oligonucleotide (k-mer) classification method based on conditional probabilities, which performs substantially better than other known methods. I will demonstrate that k-mer distributions are well-preserved among related strains/species and that it is possible to identify bacterial species, even from mixed populations, via k-mer distributions, using modest amounts of sample sequence. Population analysis is persistently challenging but important to microbiologists, leading to determination of diversity and function of members of microbial communities. With our bioinformatics methods we can achieve this analysis via a homology based method for robust phylotype determination, enhancing closely related sequence associations and a methodology for achieving more accurate richness estimation, using different clustering criteria.

Genomic sequence design and synthesis
The emerging field of synthetic biology is broadly defined as the area of intersection of biology and engineering that focuses on the modification or creation of novel biological systems that do not have a counterpart in nature. We explored the problem of designing the provably shortest genomic sequence to encode a given set of genes by exploiting alternate reading frames. Here I will present an algorithm for designing the shortest DNA sequence simultaneously encoding two given amino acid sequences. We have shown that the coding sequences of naturally occurring pairs of overlapping genes approach maximum compression, as well as investigated the impact of alternate coding matrices on overlapping sequence design. Working with the group that achieved the first genome-level synthesis of a virus, we have designed, synthesized, and evaluated two new variants of poliovirus to serve as vaccines. Specifically, we seeked weakened but viable strains that may be used for preparations of a killed poliovirus vaccine. Our designs result in a virus with roughly 100-fold lower specific infectivity than the wildtype virus. Here I will present the theory behind gene design in the context of optimizing a DNA sequence for particular desired properties while simultaneously coding for a given amino acid sequence.

This overview of current graphic algorithms in the Game Industry starts with an introduction to video card capabilities highlighting the differences between software rendering, the old Fixed Function Pipeline, and the new standard, the Programmable Pipeline. Graphical approaches to game aesthetics such as Shadow mapping, Real-time lighting, Day / Night cycles, Terrain Rendering, and Cel-Shading will be demonstrated using "shader programs" on graphics hardware, utilizing the programmable pipeline that is prevalent in today's consumer desktop and video game consoles.

This is another in the Departmental Pizza Seminar series.

Data mining is a new area of computer science that integrates ideas from other areas of computer science, such as algorithms, complexity theory, computer systems, databases, machine learning, and network systems. The goal of data mining is to discover interesting information in large databases. In this talk I will present some of my past and current research work in the area of data mining. I will first introduce association mining and sequence mining, both of which have been known to be quite useful in businesses. In the former the goal is to enumerate all frequent combinations of data attributes appearing in a database, in the latter the data is time- stamped and the goal is to find all frequent sequences of frequent combinations of data attributes. I will present how these data mining tasks can be used for slightly different purposes, for finding similarities among database and for predicting future events. I will then switch a gear and talk about some work on gene expression data analysis. Semi-supervised learning refers to machine learning techniques for building more accurate models creatively using unlabeled data. I will present how semi-supervised learning can be used to improve the accuracy of gene function classification. I will then speak about multi-class sample classification using gene expression data.

In this talk, we give an overview of Buffalo's Center for Computational Research (CCR), one of the leading academic supercomputing sites in the world. CCR supports work in the physical sciences, engineering, life sciences, and visualization. We will also present an overview of our design and implementation of the ACDC-Grid, an extensive, multi-institutional proof-of-concept grid that is being expanded to incorporate leading academic and non-profit organizations in New York State. We will discuss our efforts in grid monitoring, predictive scheduling, grid-enabling application templates, backfill detection and optimization, data repositories and operations, dynamic and automated allocation of resources, and our dynamic firewall, to name a few. We will then present an overview of our Shake-and-Bake method of molecular structure determination and discuss critical parameters that have been optimized in our SnB instantiation of this procedure. Finally, we will discuss the functionality of the ACDC-Grid that enables a cost-effective and transparent grid-based port of SnB, including grid-enabled optimization via data repositories, data mining, and intelligent generation of jobs to be run by the daemon overseeing the parameter optimization routine.

Dr. Miller is UB Distinguished Professor of Computer Science and Engineering at SUNY-Buffalo and Senior Research Scientist at the Hauptman-Woodward Medical Research Institute. Shake-and-Bake was listed on the IEEE poster "Top 10 Algorithms of the 20th Century". The work presented in this talk was supported by NSF, NIH, DOE, NYS, the Oishei Foundation, the Wendt Foundation, NIMA, Dell, IBM, and HP. This talk represents joint work with many students, staff, and colleagues, who are listed in the talk.

You'll hear a short summary of the current state of the art in formal and computer-checked mathematics, as well as the motivation and history of formalization efforts. A lightweight overview of one of the leading formalization systems and projects - Mizar - will follow. Finally I'll talk about Mizar and its large formal knowledge base as a very interesting object for various Artificial Intelligence methods, and their potential combinations.

This is another in the Departmental Pizza Seminar series.

The equivalence of different axiomatizations of modal logics is well known and documented in the literature. e.g., S5 may be equivalently axiomatized by PC + necessitation + K (distribution) + M + 5, and by S10 + M6 + S3 + M9 + B. In order to automatically prove the equivalence of two modal systems using first-order theorem provers, we provide a series of encoding rules to represent modal logic syntax in first-order syntax, and a definitional approach to encode each proof problem into a TPTP file for mechanical deduction in a first-order theorem prover.

This is another in the Departmental Pizza Seminar series.

Computer Vision is the study and application of methods that allow computers to "understand" image and video content, or content of multidimensional data. The term "understand" means that specific information is being extracted from the image or video data for a specific purpose: either for presenting it to a human operator (e. g., if cancerous cells have been detected in a microscopy image), or for controlling a process (e. g., an autonomous vehicle). Computer Vision can also be described as the complement of biological vision. In contrast to biological vision and visual perception systems though, Computer Vision enables for quantitative analysis and representation of data, and therefore it is becoming more and more essential to a wide variety of research fields.

In my talk, I will focus on different methods I have been developing in the last eight years for different applications, varying from Human-Computer and Human-Human Interaction (HCI and HHI) to 3D shape reconstruction of human organs. Specifically, the first part of my talk will be on 2D and 3D tracking of rigid, deformable and articulated objects in monocular video sequences, and how low-level features (e.g., grayscale image intensity) lead to motion and shape extraction, video segmentation, and action/event recognition. I will present the various applications of my methods, from object-based video coding to American Sign Language recognition. In the second part of my talk I will present how Computer Vision methods are applied to biomedicine. I will describe the theoretical framework of LocoWorm, a software I have developed and is currently in use for multiple tracking, locomotion features extraction and classification for aging and phenotypical analysis of C. elegans nematodes. I will also present the problem of 3D reconstruction of alveoli from lung tissue scans, and I will give the general framework of my approach. Finally, I will describe a novel method for efficient medical image segmentation, which uses local and global shape and texture information. This method can be seen as a fusion between region growing and active shape models (ASMs).

This project is about designing and implementing a complete video game. By doing this we discovered all the ins and outs of making a complete software product. The game is a 3D first person adventure in which you will have to solve several puzzles and fight versus fully armed enemies; it is developed in C++ with Open GL for the graphics.

... and ...

The main purpose of the development of the application was to create a tool that can be used in the Medical Offices as a help to billing or coding personnel. Program offers selection screens to select options needed for the transfer and possible conversion of ICD-9 codes (International Classification of Diseases, 9th Revision). Problems related to this work include: maintaining the integrity of the data structure used to manipulate code, necessity of changes required by the need for conversion. There were some programming and data management issues, that will be discussed during the presentation.

... and ...

What happens when you put three code ninjas to find a solution to world hunger? They make a game of course! HeadWARe is a 3D strategy game where squads of robots wearing nifty hats battle out for world domination. Coded from the ground up during a period of two semesters, by four able hands, HeadWARe was conceived and created to showcase the talent and work that drive the people who created it. During this presentation we will walk you through the various stages of development and discuss the logistic and design challenges encountered by the team during the execution of this project.

This is another in the Departmental Pizza Seminar series.

This aim of the project was to extend an existing software tool to visualize the results of placement, compaction, as well as configuration space algorithms that were written by Dr Victor Milenkovic. Placement and compaction algorithms are heuristics to minimize the total amount of space occupied by a set of polygons. These heuristics are run with certain restrictions placed on each polygon. For a configuration space, The configuration of an unfixed 2-D polygon relative to one or more 2-D polygons fixed on a canvas can be expressed as a triple, (x,y,θ), with (x,y) specifying the polygon's coordinates and θ specifying its rotation. The configuration space of the same polygon relative to the other polygons can be expressed as the set of all configurations, or triples, (x,y,θ), that the unfixed polygon can take. This configuration space can be decomposed into a blocked space - the set of triples (x,y,θ) in which some polygons overlap, and a free space, its complement. Professor Milenkovic implemented algorithms to calculate this decomposition, and we added an interface to an existing Java application to visualize this boundary, in 3-D (i.e., the set of (x,y,θ) ), with a 2D cross-section (i.e., only the set of (x,y) ). The interface also allows the user to control the translation and rotation of the unfixed polygon and see its current configuration as a point in the 3-D space and 2-D cross-section. Vice versa, the user can control the configuration point and immediately see the actual, updated arrangement of the polygons.

... and ...

The presentation will include the following topics:

• basic idea for the project involving web based interface.
• technology involved.
• programming technique invovled.
• limitations of the cell phone screen size.
• challenges in making decision which software product to use for the programming.

... and ...

A trading system is simply a group of specific rules, or parameters, that determine entry and exit points for a given equity. It seems that everywhere you look, you see advertisements for software promising accurate buy and sell signals and profits with every trade - all with minimal time and effort. But, what if you took the time to select some predefined financial formulas and created your very own trading system, can your trading systems offer profitable methods of trading? Well now you can check years and years of past performance of the system with my Backtesting software.

This is another in the Departmental Pizza Seminar series.

Recent advances in molecular biology have resulted in immense amounts of biological data (DNA sequences, protein sequences and structures, gene expression data, and protein interaction data). As a result of this growth, scalable techniques to mine and analyze this data have become paramount. These new techniques employ principles in many different areas of computer science, especially databases, data mining, machine learning and graph theory. They also impose new challenges. This talk focuses on applying database principles and computational techniques on biological data to infer functional properties of proteins. Functional and evolutionary relationships between proteins can be discovered via structure comparison. As the sizes of experimentally determined and theoretically estimated protein structure databases grow, there is a need for scalable search techniques. In this talk I will present a technique that extracts feature vectors on triplets of SSEs (Secondary Structure Elements) of proteins and uses an index structure to answer similarity queries. Currently, a wide range of information sources is available to provide evidence about the functional relationships among proteins. I will present an automated functional classification methodology that uses these information sources. Protein interaction networks provide a different view of protein functional relationships based on their interaction properties and can be used to infer intricate relations, such as pathway and complex membership. I will present analysis techniques for mining interaction networks to capture functional relationships among proteins.

This talk discusses the production of visually appealing computer-generated drawings, through the emulation of human drawing techniques and artificial evolution. Employing a population of line drawn objects from user-input, the Darwinian process of evolution produces original drawings with increasing levels of user satisfaction.

... and ...

In the logical theory of a set of axioms there are many boring logical consequences, and scattered among them there are a few interesting ones. The few interesting ones include those that are singled out as {\em theorems} by experts in the domain. This paper describes the techniques, implementation, and results of an automated system that generates logical consequences of a set of axioms, and uses filters and ranking to identify interesting theorems among the logical consequences.

This is another in the Departmental Pizza Seminar series.

An intrusion occurs as a sequence of operations that may individually affect various aspects of a computer system. Current host-based intrusion detection systems that monitor the operations within a single subsystem (e.g. file system or network) suffer from myopic views of system state. Such local views can then lead to incorrect inferences about system status. In this talk, I will present a holistic system-centric approach to intrusion detection, which monitors the global state of the host. I will present the challenges that face building such a system and present the salient features of our approach that allow overcoming these challenges.

Dr. Raju Rangaswami is an Assistant Professor in the School of Computing and Information Sciences at Florida International University. He received M.S. and Ph.D. degrees from the University of California at Santa Barbara and his B.S. degree from the Indian Institute of Technology, Kharagpur, India. He conducts research in operating systems, security, storage systems, and real-time systems. His research is supported by the National Science Foundation. More details can be found at http://www.cs.fiu.edu/~raju/

This is another in the Departmental Pizza Seminar series.

Gene networks are traditionally modeled as a deterministic dynamic system using ordinary differential equations. However, it was found recently that gene expression is best viewed as a stochastic process, since gene expression consists of a series of events that involve a small number of molecules such as DNA, RNA, and proteins. Therefore, any computational modeling and simulation of a gene network should take into account such stochasticity in gene expression. In this talk, I will first introduce stochastic modeling of gene networks from both biological and computational perspective, and then briefly describe characterization of the stochastic dynamics of gene networks or more general any coupled chemical reaction systems. I will also briefly review stochastic simulation algorithms (SSA) including the exact SSA, approximate but more efficient leaping methods, and multiscale SSAs. Finally, I will present an efficient SSA called K-leap SSA, that we developed recently, and compare its performance with that of other SSAs.

This is another in the Departmental Pizza Seminar series.

Over the years, the advancements in science and technology have led to the increased complexity in computing systems. The systems are thus becoming increasingly more complex with growing number of heterogeneous software and hardware components, increasingly more difficult to monitor, manage and maintain. There is thus a pressing need for automatic and efficient approaches to monitor and manage complex systems. In this talk, I will first describe our research effort on mining log data for automatic system management. In particular, I will talk about two research components of the holistic effort: (a) novel text mining approaches to transform system log data in disparate formats and contents into a canonical form; (b) new temporal data mining techniques to discover relationships among event data. I will also discuss some research directions and future work on this project. If time permits, the talk will also give an overview of some other research projects that we are currently working on such as microarray data analysis, matrix factorization for text clustering, music information retrieval, adaptive workflow management.

Dr. Tao Li is currently an assistant professor in the School of Computer Science, Florida International University. He received his Ph.D. in computer science from the Department of Computer Science, University of Rochester in July 2004. His research interests are in data mining, machine learning, information retrieval, and bioinformatics. He is a recipient of NSF Career Award, IBM Faculty Award, and IBM SUR (Shared University Research) Award. More information about him can be found at http://www.cs.fiu.edu/~taoli.

This is another in the Departmental Pizza Seminar series.

The rapidly growing body of 3D protein structures provides new opportunities to study the link between protein structure and protein function. Local structural comparison, which aims to identify arrangements of amino acids common to a family of proteins, is a way to discover structural features linking protein structures to their function. Traditional approaches to local structural comparison of proteins operate in a pair-wise fashion and have prohibitive computational cost when scaled to families of proteins. This talk describes my research on graph-based representations of protein structure and new subgraph mining algorithms to identify recurring structural patterns shared by many members of a family of proteins. A statistical measure is defined to evaluate the significance of each pattern's association with a family of proteins compared to all known protein structures.

Two collaborations with domain experts at the UNC School of Pharmacy and the UNC Medical School illustrate the use of these techniques. The first is to predict the function of several newly characterized protein structures based on the amino acid arrangements they contain. The second is to identify conserved structural features in evolutionarily related proteins. Such structures may play an important role in folding. This talk presents results from both applications and concludes with my future research plans in the areas of data mining, proteomics, and systems biology.

Mr. Huan is a Ph.D. candidate in the Department of Computer Science and a member of the Bioinformatics and Computational Biology Training Program at the University of North Carolina. He received his B.S. in Biochemistry from the Peking University, China in 1997 and an M.S. in Computer Science from the Oklahoma State University in 2000. He worked at Argonne National Laboratory and Nortel before he joined UNC and has current collaborations with GlaxoSmithKline. His research interests include data mining, proteomics, systems biology, and high performance computing. He was a recipient of the UNC Scholar of Tomorrow Fellowship in 2001 and the Alumni Fellowship in 2005.

Radio Frequency Identification (RFID) is a popular contactless identification technology which has been hyped as the "next generation barcode". These tiny remotely-powered computer chips have already been integrated into consumer goods, passports, public transportation tickets, and even people. Because most RFID tags lack privacy enhancing technologies or cryptography, malicious parties can use RFID technology for nefarious ends like theft, stalking, and behavioral profiling.

This presentation will discuss RFID technology, the security and privacy threats which it faces, and proposed countermeasures. I will highlight one particular new solution, the RFID Guardian, that is the focus of a collaboration between researchers at the Vrije Universiteit and the Technical University of Delft.

This is another in the Departmental Pizza Seminar series.

Wireless Sensor Networks (WSNs) are believed to be one of the emerging technologies that would change the world. WSNs can be used in a wide range of potential applications in both military and civil. Since sensor nodes are battery powered, energy efficiency is of primary concern in WSNs. To prolong a sensor network lifetime, energy efficiency must be considered in almost every aspect of sensor network design. In this talk, I will address the maximum lifetime coverage problem, which is to maximize network lifetime while a sensor network performs the coverage tasks. I will present a novel mathematical model and a Linear Programming based algorithm to approximate the solution of this problem. I will also acknowledge the relation between this problem and the domatic number problem.

In addition, toward the end of this talk, I will highlight some important results of my other work in both wireless networks and computational biology.

The drawing of information, often represented as a graph, onto a medium such as a computer screen is a fundamental yet challenging problem in computer science. The algorithms developed incorporate techniques from computational geometry, graph theory, optimization, and computer graphics.

In general, the underlying problem is to take a graph composed of vertices and edges between the vertices and place (embed) these vertices and edges on the screen in a visually appealing and informative manner. The precise definition of "appealing" and "informative" are of great debate in the graph drawing community, but certain standards are almost universally accepted. For example, graphs with multiple edge crossings are considered less appealing and more confusing than similar graphs without any crossings.

In this talk, we shall introduce the area of graph drawing, give a brief description of basic results and problems in the field, and discuss some of our own recent results particularly in the area of simultaneous graph embeddings.

This is another in the Departmental Pizza Seminar series.

Bioinformatics has become a buzz word to mean almost anything and everything to do with the interface of computers and biology. From the perspective of the discipline of Medical Genetics, there are two clear applications for this interface. One is in the database arena, linking a patient's genetic and family history information with data on the disease or syndrome that this patient presents with. The second is in understanding how a genetic problem actually translates to a disease. In other words, analysis of the gene sequence, of the protein that this gene makes, and of how this gene is switched on and off. These methods fall mostly under the title of "genomics", and have had a meteoric rise since the completion of the human genome sequence. This talk will summarize the advances made in bioinformatics for Medical Genetics, and highlight the areas where there is room for improvement.

This is another in the Departmental Pizza Seminar series.

Background: Ever since patient medical information has been put into computerized databases, there has been a plethora of security issues related to information privacy. Now, with the HIPAA act, medical facilities are being held responsible for the security of protected information. While many of the cryptographic security issues have been solved, there is still vulnerability from unauthorized users who have obtained access to an online medical record database using legitimate login information.

Abstract of Solution: To solve this problem I have designed a modification specification to database source code which requires certain "tags" to be added to queries. An unauthorized user who has gained access to the database remotely through someone else's authorized login information would receive fictitious query results when he/she sends "untagged" queries to the database. Furthermore, the sensitive information within the patient medical record would be stored in a separate table from the patient demographic information such that an unauthorized user would have to perform a table join within the query.

This is another in the Departmental Pizza Seminar series.

We will explain the process of analyzing, planning, implementing and testing an Electronic Medical Record (EMR) system from a software engineering perspective. An EMR system is responsible for maintaining patient medical records as well as facilitating other office procedures (e.g. scheduling, billing). Part of the systems engineering process requires communication between team members to revise code and documentation. To streamline this process we developed a project management website that allows team members to upload their code and documentation remotely for review by the other team members.

This is another in the Departmental Pizza Seminar series.

Oceanic simulations have traditionally relied on structured-grid, finite difference methods to discretize the hydrostatic primitive equations governing large scale ocean flows. The complex coastlines of ocean basins, and the geometrically flexibility inherent in unstructured grids has spurred ocean modelers to pursue the development of finite element based models. Here we sketch the outlines of one such code: the spectral element ocean model (SEOM). The spectral element methods combine the geometrical flexibility of low-order finite element methods and spectral methods. Its advantages include high accuracy, very-low numerical dissipation, dense computational kernels at the element level and sparse neighbor-to-neighbor communication; the latter combination leads to extremely good scalability on parallel computers. In the talk the basis of the method will be presented, and sample two-dimensional simulations will be shown. The final part of the talk will revolve around the challenges of three-dimensional ocean modeling.

This is another in the Departmental Pizza Seminar series.

We present robust floating point algorithms for performing topologically invariant set operations on 2D semi-algebraic sets. A 2D semi-algebraic set is a set of cells from an arrangement of segments of algebraic curves. These algorithms transform and overlay multiple arrangements invariantly. Because the algorithms are implemented in floating point, certain topological changes are unavoidable. For instance, after a floating point Euclidean transformation, two very close but distinct points may transform into the same point. The topological changes that can result from floating point rounding are analyzed. The algorithms are invariant except for these types of changes. We discovered that the unavoidable topological changes in our robust topologically invariant algorithms occur rarely in testing. We ran tests on our topologically invariant algorithms against the original algorithms by Milenkovic and Sacks, comparing computing time and accuracy.

This is another in the Departmental Pizza Seminar series.

In this talk we prove new upper and lower bounds on the proper PAC learnability of decision trees, DNF formulas, and intersections of halfspaces. Several of our results were obtained by exploring a new connection between automatizability in proof complexity and learnability. After explaining this basic connection, we will prove the following new results.

1. We give new upper bounds for proper PAC learning of decision trees and DNF, based on similar known algorithms for automatizability of Resolution.
2. We show that it is not possible to PAC learn DNF by DNF in polynomial-time unless NP ⊆ BPP. We also prove the same negative result for proper PAC learning of intersections of halfspaces.
3. We show that decision trees cannot be proper PAC learned, under the assumption that SAT is not solvable by subexponential-size circuits.

This is joint work with Misha Alekhnovich, Mark Braverman, Vitaly Feldman, and Adam Klivans.

The event calculus is a powerful and highly usable formalism for reasoning about action and change. The discrete event calculus limits time to integers. This paper shows how discrete event calculus problems can be encoded in first-order logic, and solved using a first-order logic automated theorem proving system. The following techniques are discussed: reification is used to convert event and fluent atoms into first-order terms, uniqueness-of-names axioms are generated to ensure uniqueness of event and fluent terms, predicate completion is used to convert second-order circumscriptions into first-order formulae, and a limited first-order axiomatization of integer arithmetic is developed. The performance of first-order automated theorem proving is compared to that of satisfiability solving.

This is joint work with Erik Mueller of IBM Thomas J. Watson Research Center.

This is another in the Departmental Pizza Seminar series.

Using lemmas has been proved to be an effective approach for assisting ATP systems to solve hard problems. Useful lemmas can provide valuable guidance in the proof search, and help construct the proof by filling in intermediate steps. However, the formulae supplied to an ATP system as lemmas are not all necessarily useful. Unuseful lemmas act as noise, disturbing the search for the proof. It is therefore necessary to develop lemma management techniques that identify useful lemmas, and help an ATP system to use the useful lemmas to its advantage. We have designed three lemma management techniques, implemented them, and illustrated their potential with example problems. It has been shown that, with these three lemma management techniques, the problem-solving ability of an ATP system can be improved.

This is another in the Departmental Pizza Seminar series.

The Block Sorting Coder (BSC) described by Burrows and Wheeler has received considerable attention. BSC achieves a compression ratio closer to PPM, but with a faster execution speed than PPM.

An essential part of BSC schemes is the Move-to-Front (MTF) coder (recency ranking). In this talk we analyze the MTF coder and introduce a different coding (ranking) scheme, inversion coder. We prove the information theoretic relationship between interval ranks and canonical sorting permutations. Finally, we explore the relationship between inversion ranks and recency ranks and show that the inversion coding (ranking) technique introduced is superior to interval ranking and as well as recency ranking.

This is another in the Departmental Pizza Seminar series.

The standard operating system class will give you a good introduction to how operating systems work. They will likely give you overviews of some of the basic components like scheduling, IPC, memory management, etc. The knowledge that you receive will give you some direction, but little practical assistance should you choose to write your own OS. This talk is intended to provide some insight as to the specific challenges of building an OS from scratch.

This is another in the Departmental Pizza Seminar series.

The Halton sequence is one of the standard (along with (t,s)-sequences and lattice points) low-discrepancy sequences, and thus is widely used in quasi-Monte Carlo applications. One of its important advantages is that the Halton sequence is easy to implement due to its definition via the radical inverse function. However, the original Halton sequence suffers from correlations between radical inverse functions with different bases used for different dimensions. These correlations result in poorly distributed two-dimensional projections. A standard solution to this is to use a randomized (scrambled) version of the Halton sequence. Here, we analyze the correlations in the standard Halton sequence, and based on this analysis propose a new and simpler modified scrambling algorithm. We also provide a number theoretic criterion to choose the optimal scrambling from among a large family of random scramblings. Based on this criterion, we have found the optimal scrambling for up to 60 dimensions for the Halton sequence. This derandomized Halton sequence is then numerically tested and shown empirically to be far superior to the original sequence.

This work is joint with Ms. Hongmei, and is part of her Ph.D. dissertation.

The term ontological semantics refers to the apparatus of describing and manipulating meaning in natural language texts. Basic ontological-semantic analyzers take natural language texts as inputs and generate machine-tractable text meaning representations (TMRs) that form the basis of various reasoning processes. Ontological-semantic text generators take TMRs as inputs and produce natural language texts. Ontological-semantic systems centrally rely on extensive static knowledge resources:

• a language-independent ontology, the model of the world that includes models of intelligent agents;
• ontology-oriented lexicons (and onomasticons, or lexicons of proper names) for each natural language in the system; and
• a fact repository consisting of instances of ontological concepts as well as remembered text meaning representations.

Applications of ontological semantics include knowledge-based machine translation, information retrieval and extraction, text summarization, ontological support for reasoning systems, including networks of human and software agents, general knowledge management and others. In this talk I will give an overview of ontological-semantic processing and static resources and discuss its use in applications.

The development and deployment of component-based automated reasoning systems relies on an adequate infrastructure of standards and tools that allow the component systems to execute and interact in a controlled and reliable way. In the field of 1st order automated reasoning there has been limited standardization across the available component systems, resulting in adhoc combination techniques and a limited range of general purpose tools. This work presents two emerging standards in the 1st order automated reasoning community, whose adoption is leading to greater compatibility between component systems. Six general purpose tools that conform to these standards are then described. The standards and tools facilitate direct communication between components of complex systems, providing seamless integration and greater reasoning productivity.

This is another in the Departmental Pizza Seminar series.

Dimensions are numerical values assigned to certain geometric parameters. While dimensioning has been a common and basic engineering activity practiced over several centuries, a theory of dimensioning emerged only in the last decade of the 20th century. This theory is a synthesis of many ideas that range from elementary Euclidean geometry to some advanced Lie group classification of rigid motions. A prime motivator for this effort was the need to standardize the specification and exchange of product information in the computerized management of product lifecycle.

In this talk I will explain some elements of the theory of dimensioning and will point out how this also serves as a theory of parameterizing geometric models.

(This talk is based on the speaker's book "Theory of Dimensioning" published by Marcel-Dekker in October, 2003.)

About the Speaker: Vijay Srinivasan is the Program Manager for PLM Research, Standards, and Academic Programs at the IBM Corporation in New York. He is also an Adjunct Professor in the Engineering School at Columbia University, NY. He is a member of several national and international standards committees in the areas of product specification, verification, and data exchange.

Increasing competition in the development tool market has pushed vendors to combine their offerings into single products or sell them as suites. In the Web tool market, for instance, with the exception of some XML technologies, vendors are repackaging their tools into suites. eBD Software is offering alternative development methodologies to traditional Web tools such as Dreamweaver, introducing its e-Business Designer (eBD) tool in the United States.

eBD is a mix of portal and Web development environment that can generate portals, intranets and document management systems. It takes a radically different approach to Web Development. The tool follows a unique object model in which most of the features in the environment used for creating applications work like objects. Folders, pages and tables, for instance, all fall under a hierarchical structure and are treated as complete entities. Each of these structures contain a number of wizards so users can build fairly sophisticated portals with little knowledge of Web development. The wizards also come with features that enhance a site. With a few clicks, users can add calendaring, chatting and mailing links.

The talk will be a introduction to this new software solution, which will include a demo, real case studies and a discussion on this and similar technologies.

This is another in the Departmental Pizza Seminar series.

Almost everyone has to give a public presentation at some time. Graduate students have to defend their theses, research students have to present their results, and many jobs require presentations. It is common to have little or no experience when you give your first presentation, and you may even be a little nervous! This seminar is aimed at (graduate, research, and other) students. It describes how to present a successful seminar, in a simple standard format. This seminar does not try to teach general speaking skills, nor impose any personally preferred techniques. It covers the structure of a seminar, the use of visual aids, speaking technique, and how to cope with questions.

This is another in the Departmental Pizza Seminar series.

We present robust floating point algorithms for constructing arrangements of lines and semi-algebraic curves and for manipulating semi-algebraic sets. These robust algorithms construct a consistent combinatorial arrangement, and thus can handle every type of degeneracy (special cases that can give the algorithm problems). Due to floating point inaccuracies in computer arithmetic, degenerate cases arise. For example, three curves that meet at a point or two points with equal x coordinates can cause problems. An arrangement is a set of lines and curves that induces a subdivision of the plane, and it consists of vertices, edges, and cells. The construction of an arrangement is done using a plane sweep algorithm to find all the intersections. Our input is a set of continuous x-monotonic curves and lines delimited by endpoints. The sweep output is a partial vertical order on our set of segments, and these segments are obtained by splitting the input segments by their intersections. The sweep output is then converted to an arrangement (the segments are edges and their endpoints are vertices). Segments are grouped into loops by traversing through the vertices and edges, and these loops are grouped into cells using the segment order. We can now use our arrangement algorithm to rotate semi-algebraic sets and to perform set operations. The sweep runs in O((n + N + k) log n) where n is the number of curves/lines, N is the number of intersections, and k = O(n³) is the number of inconsistencies.

This is research done under the guidance of my advisor Dr. Victor Milenkovic.

This is another in the Departmental Pizza Seminar series.

A Video on Demand (VoD) system is expected to transmit many movies over a single channel as demanded by the end users. When several videos are transmitted simultaneously over a link the effective bandwidth required per video is usually much lower than that needed by a single video because of multiplexing gain. Fast and accurate estimation of multiplexing gain is necessary for developing call admission control (CAC) algorithms. Known models which estimate queue size and effective bandwidth of multiplexed video system cannot capture frame size variations in different segments of a video, and are not very useful particularly when the number of videos is not too large.

The multinomial model proposed in this paper is built on a Markov-modulated gamma (MMG)-based traffic model of a single video. It takes into consideration average frame size variations in different segments of a video and can predict multiplexing gain for any number of multiplexed videos. The model has been validated using MPEG traces of commercial movies.

This is another in the Departmental Pizza Seminar series.

A graphical game merges network models with traditional game theory to achieve a new compact representation better suited for large-population game theory. The model graph allows the explicit encoding of the detailed structure of strategic interactions yet has a natural and simple intuitive meaning: players are represented as nodes in the graph and the payoff of a player is only a function of the actions of the player's neighbors in the graph and those of the player itself.

In this talk, I will discuss computational and algorithmic aspects of graphical games. Algorithms for basic computations, including Nash and correlated equilibria, will be presented. Connections to related topics, such as graphical models for probabilistic modeling and inference, will be discussed. Throughout the talk, I will briefly sketch the state of the art in graphical games as well as recent work on extensions to related economic models. Time permitting, I will conclude with a discussion on open problems and future research directions.

This is joint work with Sham Kakade (Penn), Michael Kearns (Penn), John Langford (TTI-Chicago), Michael Littman (Rutgers), Nick Montfort (Penn), Robin Pemantle (Penn) and Siddharth Suri (Penn).

University Course Evaluations are presently done on paper. To move this to electronic format, there are several issues similar to those of electronic voting, in particular, anonymity for the author, authenticity of the review, correct collection, and accountability.

The speaker takes a stab at designing such a system, and hopes to have his students implement a model.

Come prepared to break my system!

This is another in the Departmental Pizza Seminar series.

Problems in information visualization often involve the display of a set of objects and their relationships, that can be modeled as graphs. While static graphs arise in many applications, dynamic processes give rise to graphs that evolve through time. Such dynamic processes can be found in software engineering, internet/telecommunications traffic, and social networks, among others. Typically, the underlying graph structures are large, and depending on the time-granularity, may contain from a few to a large number of timeslices. The graph representing a particular timeslice may contain fewer/more vertices/edges than the one representing the previous timeslice, or it may differ in some other graph attributes, such as node-weights, edge-weights, or labels. We describe algorithms and techniques for visualization of dynamic graph processes, using the evolution of the scientific literature as an example of such a process. In particular, we use a local copy of the ACM Digital Library of Scientific Literature dataset with over 100,000 authors and 100,000 papers.

Current techniques for rigid body simulation run slowly on scenes with many bodies in close proximity. Each time two bodies collide or make or break a static contact, the simulator must interrupt the numerical integration of velocities and accelerations. Even for simple scenes, the number of discontinuities per frame time can rise to the millions. An efficient optimization-based animation (OBA) algorithm is presented which can simulate scenes with many convex three-dimensional bodies settling into stacks and other "crowded" arrangements. This algorithm simulates Newtonian (second order) physics and Coulomb friction, and it uses quadratic programming (QP) to calculate new positions, momenta and accelerations strictly at frame times. Contact points are synchronized at the end of each frame. The extremely small integration steps inherent to traditional simulation techniques are avoided. Non-convex bodies are simulated as unions of convex bodies. Links and joints are simulated successfully with bi-directional constraints. A hybrid of OBA and retroactive detection (RD) has been implemented as well. A review of existing work finds no other packages that can simulate similarly complex scenes in a practical amount of time.

Harald Schmidl and I presented this work at SIGGRAPH 2001. He and I developed newer work as part of his Ph.D. at UM. I have continued to work on my own, and I am now working with Kanishka Bhaduri. This talk will start with an earlier 1996 SIGGRAPH paper, continue with the SIGGRAPH 2001 paper, and continue towards the present day as time allows.

This is another in the Departmental Pizza Seminar series.

Failure to understand the limitations of the human being, as a link in any computer/automated system in which the person interacts, will most certainly lead to significant problems in the operation of the system that will either: (a) result in safety problems that could harm or kill, (b) cost the organization large amounts of money to correct problems, (c) lead to unhappy employees who are forced to use a system that is awkward and cumbersome. All of these outcomes are unacceptable. There exists today, a scientific, proven technique, that enable us to analyze the needs of the user/system, to study the environment within which the system is being developed, and formulate a user interface design specification which will ensure that these problems do not occur.

Peter Mitchell is an expert in Human-computer Interaction and Usability Testing. He is President Emeritus of the New York City Chapter of the Usability Professionals' Association, and a part time lecturer in the Department of Industrial Engineering. He owns the company ergo9.

This is another in the Departmental Pizza Seminar series.

Automated Theorem Proving (ATP) systems are complex pieces of software, and thus may have bugs that make them unsound or incomplete. The derivations output by an ATP system may be semantically verified by trusted systems that check the required semantic properties of each inference step. Such verification may need to be augmented by structural verification that checks that inferences have been used correctly in the context of the overall derivation. This talk describes the design and implementation of the derivation verifier DVDV, which uses semantic verification and does structural checking for various situations.

Wed Feb 18, 5:00
In Ungar, Room 402
Free Pizza

Received: Sun Feb 1 0:17:18 2004

A Rich Theory is one whose axioms (expressed in 1st order logic) contain a large number of predicates and functors, and whose theorems are often provable from a subset of the axioms. Experimental results have shown that the removal of just a few unnecessary axioms can have a significant effect on the performance of an ATP system on a problem. This work introduces a relevance measure that estimates the potential usefulness of an axiom for proving a given theorem. The measure has been used in a control algorithm that selects combinations of axioms based on their relevance, to form {\em axiom reduced} problems that are submitted to an ATP system. Evaluation shows that this system performs better than the ATP system alone. Additionally, a scheme for using the relevance measures for selecting lemmas to augment the axioms of a problem is introduced.

Monday, November 17, 5:00 PM
Either Ungar 402 or 506, as scheduling permits.
Pizza and drinks are provided by the department.

At my last pizza talk, I described how to robustly construct an arrangement of algebraic curves. The ultimate purpose was CAD: computer aided design. However, constructing arrangements is still a far cry from designing stronger bridges, faster chips, or bigger SUVs. This talk will show how to define sets in the plane bounded by segments of algebraic curves and how to apply rigid transformations and how to perform set operations on them: union, intersection, symmetric difference, etc. Most of the work goes into dealing with degenerate cases: ``unexpected coincidences''. An important trick is a ``spin on the wheel of fortune'': apply a random rotation to the set before attempting the operation.

Again, this is joint work with Elish Sacks of Purdue University.

Monday, November 10, 2003, 5:00 PM
Either Ungar 402 or 506, as scheduling permits.
Pizza and drinks are provided by the department.

This is the third talk by Brian on this subject. Analysis of floating point error of the dot product was given in the previous talk, and error for various matrix norms.

Monday, November 3, 2003, 5:00 PM
Either Ungar 402 or 506, as scheduling permits.
Pizza and drinks are provided by the department.

Received: Fri Oct 31 10:46:59 2003

We will show how to use the floating-point arithmetic specified in IEEE754 to produce rigorous mathematical estimates of various quantities.

See seminar, 13 October for further details.

Monday, 27 October 5:00 PM
In Ungar 402 or 506
Pizza is served at 5:00 PM
All are welcome.

Received: Fri Oct 17 18:05:50 2003

A short presentation in which an ordinary deck of cards is used to compute an arbitrary boolean function by two mistrustful parties. By encoding bits and cutting the deck, neither party will learn the other party's input except for what is implied by the function output itself.

Monday, Oct 20, 5:00 PM
In Ungar, Room CC402 or 506, depending on weather.
(Weather what? whether or not it is in 402, of course).
Pizza will be served at 5:00 PM.

Received: Fri Oct 17 18:00:58 2003

Before the approval of the IEEE754 standard in 1985, many computers had idiosyncratic or problematic floating-point implementations. This led to the discovery of counterintuitive, even bizarre, programmatic situations, which in turn created a general aura of distrust for floating-point arithmetic. The standard, when implemented correctly, gives cross-platform consistency and predictability to floating-point arithmetic. While the aura of distrust lingers, the general status of floating-point arithmetic has improved. We will show how to use the floating-point arithmetic specified in IEEE754 to produce rigorous mathematical estimates of various quantities. As an example, we will show how to use floating-point arithmetic to compute a rigorous upper bound for the Euclidean norm of the inverse of a square matrix approximated by a matrix of floating-point numbers.

Monday, 13 October, 5:00 PM
In Ungar, Room CC402
This the 30th in our series of Pizza seminars.
Pizza is provided.

Received: Sun Oct 12 22:03:53 2003

I describe work with students Yi Gao, Yuan Zhang and Vera Arsova to implement the distributed cryptographic evaluation of functions.

We are concerned with the two party case. X and Y have values x and y and wish to collectively compute some function f(x,y). At the end of the computation X learns nothing of the value y except what can be inferred from x and the computed f(x,y). Likewise for Y. The protocol must also not release additional information even if Y cheats on the protocol.

Background the the problem will be followed by a discussion of the implementation and a demonstration.

Monday, 29 September, 5:00 PM
In Ungar, Room 402
This is the 28th Pizza Seminar. Pizza and drinks are served.
Received: Mon Sep 22 19:02:43 2003

BBN, Harvard, and Boston University are building the DARPA Quantum Network, the world's first network that delivers end-to-end network security via high-speed Quantum Cryptography, and testing that Network against sophisticated eavesdropping attacks. The first network link has been up and steadily operational in our laboratory since December 2002, and will soon be built out across the metro Boston area via standard telecom (dark) fiber. In this talk, we introduce quantum cryptography, discuss its relation to modern secure networks, and describe its unusual physical layer, its specialized quantum cryptographic protocol suite (quite interesting in its own right), and our extensions to IPsec to integrate it with quantum cryptography.

This is the 27rd in the Departmental Pizza Seminar series.

The drawing of a graph onto a medium such as a computer screen is a fundamental yet challenging problem in computer science. The algorithms developed incorporate techniques from computational geometry, graph theory, optimization, and computer graphics.

In general, the underlying problem is to take a graph G composed of vertices (V) and edges (E) between the vertices and place (embed) these vertices and edges on the screen in a visually appealing and informative manner. The precise definition of ``appealing'' and ``informative'' are of great debate in the graph drawing community but certain standards are almost universally accepted. For example, graphs with multiple edge crossings are considered less appealing and more confusing than similar graphs without any crossings.

In this talk, we shall introduce the area of graph drawing, give a brief description of basic results and problems in the field, and discuss some of our own recent results in the area of simultaneous graph embeddings.

This is the 25rd in the Departmental Pizza Seminar series.

We present a robust arrangement algorithm for algebraic curves based on floating point arithmetic. The algorithm performs a line sweep, tests the consistency of each sweep update, and modifies the input to prevent inconsistent updates. The output arrangement is realizable by semi-algebraic curves that are close to the input curves. We present a new performance model for robust computational geometry in which running times and error bounds are expressed in terms of the number of input inconsistencies. An inconsistency is a combinatorial property that is derivable with a given set of numerical algorithms, but that is not realizable. The running time of the arrangement algorithm is O((n+N)\log n+k(n+N)\log n) for n curves with N intersection points and with k=O(n³) inconsistencies. The distance between the realization curves and the input is O(ε+knε) where ε is the curve intersection accuracy. The output size is always the standard O(n+N). We show experimentally that k is zero for generic inputs and is tiny even for highly degenerate inputs. Hence, the algorithm running time on real-world inputs equals that of a standard sweep and the realization error equals the curve intersection error.

Joint work with Elisha Sacks of Purdue University.

This is the 24rd in the Departmental Pizza Seminar series.

Joe Clarke gives two talks on FreeBSD and workshop on firewalls. The first talk will be given as part of the Computer Science Pizza Seminar series. The next two presentations will be given on the following two days.

The FreeBSD Way.
Monday, September 8th, 2003

This talk will discuss the origins and direction of FreeBSD. We will cover the political and social layouts of the project. We will discuss the philosophy of the operating system and how it is developed, as well as the underlying BSD license. We will compare to Linux and GPL where appropriate. We will also discuss FreeBSD strengths and weaknesses, and show where FreeBSD fits into both the server and desktop niches.

Getting to know and love FreeBSD
Tuesday, September 9th, 2003

This talk will cover getting started and learning to use FreeBSD. Topics will include a basic overview of installing the operating system, and where to find help to get you to "the next step." We will discuss the layout of the file system as well as how system configuration is done in the FreeBSD world. We will go into great detail about the FreeBSD ports collection, and show how to find ported software as well as install and manage ports and packages. Finally, we will look at some advanced topics like tracking -STABLE and -CURRENT branches, and how to keep your sources up-to-date.

Working with the Cisco Pix firewall
Wednesday, September 9th, 2003

This workshop is designed to familiarize students with the workings of the Cisco PIX firewall. We discuss terminology as well as configurations. We will be configuring a sample network using a PIX 501, and then demonstrating how to troubleshoot problems in the network.

Joe Marcus Clarke, Bio.

Joe Marcus Clarke holds a Bachelor of Science in Computer Science from the University of Miami. Since graduating, he has worked for Cisco Systems, Inc. in the Technical Assistance Center (TAC) supporting Cisco's network management software and technologies. He is Cisco Certified Internetwork Expert #5384 and is also a Sun Certified Java Programmer. He is a ports committer for the FreeBSD project specializing in GNOME on FreeBSD. He also sits on the Port Managers team for FreeBSD. Other Open Source projects he works on include Netatalk and the Cisco Open Source Initiative (COSI).

This is the 23rd in the Departmental Pizza Seminar series.

A Rich Theory is one whose axioms (expressed in 1st order logic) contain a large number of predicates and functors, and whose theorems are often provable from a subset of the axioms. Examples of rich theories are set theory, geometry, and homological algebra. The complexity and scope of rich theories contribute to the difficulty of finding proofs of theorems using Automated Theorem Proving (ATP) systems. This seminar describes techniques that have been developed to improve the performance of ATP systems on theorems in rich theories.

This is the 22nd in the Departmental Pizza Seminar series.

In this talk, the presenter will discuss today's and tommorrow's emerging consumer applications/services based on video and multimedia communications. The scope of this tutorial-style presentation will include application/service classes, common technology, protocol and architectures and network planning issues for supporting video and multimedia applications over Broadband wireline communication networks. Specific discussion will be based on practical issues related to key network planning parameters such as application domains, bandwidth, quality-of-service (QoS) and multicast.

This is the 21st in the Departmental Pizza Seminar series.

This summer Agrawal, Kayal and Saxena solved the long outstanding problem of a P-time algorithm for deciding whether a given integer is prime. In this pizza seminar I will present their proof.

This is the 20th in the Departmental Pizza Seminar series.

Throughout the twentieth century, composers, performers, and technologists have yearned for robust control interfaces to mediate between musician and machine. Recent developments have enabled the creation of inexpensive gestural interfaces that facilitate straightforward, meaningful, and precise mapping of gesture into sound. I will introduce the notion and importance of the "alternate controller" and discuss several of my own instruments and interfaces. Plenty of sound will be served.

This is the 19th in the Departmental Pizza Seminar series.

In this talk, the presenter will discuss today's and tomorrow's emerging consumer applications and services which will drive widespread deployment and acceptance of the Third Generation (3G) Mobile Wireless Communication (Cellular) Systems, blurring out the long debated gray line between myth and reality of 3G. Specific discussion will be based on key parameters of popular services/application, resulting impact/challenges on 3G system implementation, technology enablers and service migration from 2G to 3G Networks.

This is the 18th in the Departmental Pizza Seminar series.

A translation lattice packing of k polygons P₁, P₂, P₃,...,P_k is a (non-overlapping) packing of the k polygons which is replicated without overlap at each point of a lattice i₀v₀+i₁v₁, where v₀ and v₁ are vectors generating the lattice and i₀ and i₁ range over all integers. A densest translational lattice packing is one which minimizes the area |v₀ x v₁| of the fundamental parallelogram. An algorithm and implementation is given for densest translation lattice packing. This algorithm has useful applications in industry, particularly clothing manufacture.

This is the 17th in the Departmental Pizza Seminar series.

A new physical model, Cleats on Ice (CoI), is described for calculating the acceleration of many rigid bodies with simultaneous contacts under the forces of gravity and contact friction. Under the CoI model, iterated quadratic programming (QP) suffices to calculate the accelerations. Like computationally more intensive complementarity-based techniques, CoI ensures complementarity: at each contact, a pair of bodies press on each other or accelerate away from each other but not both. However, CoI does so in an implicit rather than explicit manner that is both scalable and easy to implement. Furthermore, CoI can take advantage of powerful, well-maintained, and well-documented commercial optimization libraries. As part of a larger simulation package, CoI can practically generate realistic animations of scenes with over 200 bodies and over 500 simultaneous contacts.

Joint work with Harald Schmidl.

This is the 16th in the Departmental Pizza Seminar series.

The TPTP (Thousands of Problems for Theorem Provers) Problem Library is a library of test problems for Automated Theorem Proving (ATP) systems for 1st order classical logic. Since the first release of the TPTP in 1993, many researchers have used the TPTP as an appropriate and convenient basis for testing their ATP systems. The TPTP is now the de facto standard for testing and evaluating ATP systems. The TSTP Solution Library is the flip-side of the TPTP. The TSTP will maintain solutions to all the problems in the TPTP, from all currently available state-of-the-art ATP systems. The solutions output by the systems will be translated and stored in a common format, so that the TSTP can be consistently interrogated and analysed. It is expected that the TSTP will immediately contribute to the development of ATP systems, by allowing system developers to easily access and analyse other systems' solutions to TPTP problems. In a broader context the TSTP will provide a basis for understanding and comparing proof structures, will be used for certification of ATP systems, and form a framework within which users will be able to create and solve more problems using ATP tools and techniques.

This talk describes the work in progress towards the TSTP, including motivations, requirements, design decisions, and the various projects that are contributing to and using the TSTP.

This is the 15th in the Departmental Pizza Seminar series.

Computer simulation of real-world environments is one of the grand challenges of computer graphics. Applications for this technology include remote education, virtual heritage, specialist training, electronic commerce, and entertainment. Unfortunately, current computer graphics techniques fall far short of providing solutions for this challenge. In this presentation, I present a new approach to capturing and rendering large real-world environments, including several successful demonstrations and future research plans.

My ultimate goal is to allow an untrained operator to walk into a city or building (e.g., a museum) and wave around some device that captures a digital model, which later can be used to provide many people the realistic visual experience of "walking" through the environment interactively. My approach is to take advantage of recent technology trends and to obtain a dense and automatic sampling of a large viewpoint space with omnidirectional images. This strategy replaces the difficult computer vision problems of 3D reconstruction and surface reflectance modeling with the easier problems of motorized cart navigation, data compression, and working set management.

I also provide a research plan to capture and reconstruct large environments as well as a summary of previous approaches. This plan benefits from collaborative efforts in robotics (for building self-navigating high-resolution capture devices), computer vision (for developing image-reconstruction algorithms), and systems (for building and deploying large software systems over a network) and from developing applications to foment interactive tourism, to preserve historical sites, and to assist with simulation and training scenarios.

A variety of massive data sets exhibit an underlying structure that can be modeled as dynamic weighted multi-digraphs. Their sizes range from tens of gigabytes to petabytes. These include the World Wide Web, Internet Traffic and Telephone Call Detail. These data sets sheer volume brings with it a series of computational and visualization challenges due mainly to the I/O and Screen Bottlenecks.

We present external memory algorithms for connectivity and minimum spanning trees together with heuristics for quasi-clique finding. We describe how hierarchy trees help us to cope in a unified manner with both, the I/O and screen bottlenecks. This line of research has suggested the need to look for "novel" graph representations in order to provide a user or a data mining engine with informed navigation paths.

We will discuss our results with graphs having on the order of 200 million vertices and several billion edges and we will point out some mathematical problems that have surfaced along the way.

The overall goal is to extract useful information that can be brought into a user's palm top and to export these techniques to other mining domains.

Information about some of James's current visualization research projects can be obtained by accessing www.research.att.com/areas/visualization and http://www.visdays.com/.

The strength of magnetoencephalography (MEG) is that magnetic fields are not smeared by the skull, leading to greater potential spatial sensitivity. Unfortunately, this penetrative ability of magnetic fields also causes each sensor to receive signals from a large number of active sources and makes it difficult to shield out noise, both external (power grid) and internal (heartbeat, eyeblinks). We have made a systematic effort to improve MEG's performance through new signal processing for separation and dipole localization, both raising the effective performance of current MEG systems and relaxing constraints that have constrained MEG hardware design.

For separation, we applied SOBI to complex MEG data. This segregated non-neuronal sources from neuronal ones, and neuronal ones from each other. The separated neuronal sources seem focal, and have temporal responses consistent with their estimated locations. We can routinely isolate sources within modalities, across modalities, across tasks, and across subjects. The SNR is high enough to allow estimation of response onset times for single trials, which can be measured in visual, auditory, and somatosensory modalities with detection rates over 95%. Combined with an improved ability to localize the underlying neuronal sources, this makes possible the non-invasive study of a range of perceptual and memory functions that depend upon the timing of neuronal events occurring in specific brain regions.

With many recovered sources, dipole localization becomes a bottleneck. For both a 4D Neuroimaging Neuromag-122 and the experimental LANL SiS Mark I with superconducting magnetic mirrors, we addressed the single dipole localization problem at low SNR, achieving a reduction in localization time from 449ms to 0.5ms at an accuracy of 12mm, and to 35ms at an accuracy of 2.8mm. Our fast fully automatic noise-robust localizer is suitable for real-time applications, such as closed-loop experimental protocols and brain-computer interfaces.

Publications: http://www.cs.unm.edu/~bap/publications.html

In this presentation, I will cover the concepts of QoS, challenges in IP-based Multimedia networks, overall architecture, present state of design, implementation and related issues.

This is the 14th in the Departmental Pizza Seminar series.

Recent years have witnessed significant growth and interest in wireless communication. Coupled with the advances in compter hardware and architecture, progress in wireless communication has led to significant interests in the area of Mobile Computing, a paradigm of computing anytime, anywhere. In this talk we present a synthesizing overview of several issues related to architecture, mobile host detection, need for low power and large bandwidth, etc. Challenges involved in designing such systems will also be highlighted.

For detailed analyses of specific chaotic systems one must often resort to numerical simulations. Unfortunately, chaotic systems amplify small errors at an exponential rate, which makes their simulations necessarily unreliable. Indeed, many published pictures of solutions of chaotic systems are unintentional forgeries. In this talk we will present several striking simulations of chaotic systems using the soon-to-be-released Phaser (www.phaser.com). We will then reveal what these bogus pictures may really depict.

This is the 13th in the Departmental Pizza Seminar series.

The Russian Option is a two-party contract which creates a liability for the option seller to pay the option buyer an amount equal to the maximum price attained by a security over a specific time period, discounted for the option's age. For an N+1 step time period 0, 1, 2, ..., N, the option seller's liability at time step n, 0 ≤ n ≤ N, is,

L(n) = βⁿ max_{0 ≤ t ≤ n} s_t

where s_t is the security price at time t and β is the discount factor. In this work we consider the value of this option under a standard binomial model of security prices, and give efficient algorithms for value calculation.

This work gives an O(N²) dynamic programming algorithm determining the option price at all time steps as well as the optimal execution strategy.

This is the 12th in the Departmental Pizza Seminar series.

After introducing some basic molecular biology, this talk will present a sampling of problems in Bioinformatics where computer scientists have been involved and have left their mark.

This is the 11th in the Departmental Pizza Seminar series.

A computational model is black-box if it is used without a clear understanding of how it works. A model may be black-box because its computation is hidden, or it may be black-box because its computation is hard to interpret. Examples of this latter category are semi-parametric and non-parametric models such as neural networks, nearest neighbor classifiers, and ensemble classifiers like boosting. Having greater interpretability for these models is important for advancing our understanding of how they work, but also necessary for verifying their functionality for real-world applications. In this talk I will present a new approach to analyzing the generalization strategies of these kinds of models by examining their decision region structure.

In the first half we will examine the decision region properties of feed-forward neural networks. Using the Decision Intersection Boundary Algorithm, we will look at noise in networks, good and bad generalization and learning.

In the second half we will build on the intuition gained from neural networks and introduce Decision Region Connectivity Analysis, a method that allows the computationally efficient analysis of classifiers in a model and dimensionality independent manner. I will demonstrate how DRCA can be used to understand and compare completely different types of high-dimensional classifiers (a 64-input OCR example), amongst its applications, and conclude with current research directions.

Video traffic is one of the major sources of broadband network traffic. Because of large bandwidth requirement of high-quality uncompressed video most video are compressed using some variants of MPEG encoding before transmission. These compression algorithms can provide very high compression ratio while maintaining good quality of decompressed video. However, MPEG-coding provides different amount of compression for different frames and results in Variable Bit Rate (VBR) data known as VBR video. Accurate traffic models of VBR video are necessary for prediction of performance of any broadband network during its design and operation. We propose a frame size model of VBR video. It generates frame sizes for full-length VBR videos while preserving both GOP-periodicity and video-segment transitions.

A two-pass algorithm for analysis of a long-duration VBR video is presented. The algorithm identifies and partitions classes of video segments. Frames in each segment class produce three data-sets one each for I-, B-, and P-type frames. Each of these data-sets is modeled with a Gamma distribution. Markov processes model video segment transitions. We have used QQ plots to show visual similarity of model-generated VBR video data-sets with original data-set. Leaky-bucket simulation study is used to show similarity of data and frame loss rates between model-generated VBR videos and original video. Our study of frame-based VBR video also reveals even a low data loss rate could affect a large fraction of I- frames causing a significant degradation of the quality of transmitted video.

This is the 10th in the Departmental Pizza Seminar series.

It has been shown that methods such as Correlation Dimension provide inconclusive results when determining the complexity/dynamics of transient EEG signals under the presence of multiple signal components. We propose the use of Approximate Entropy since it has proven to be robust to both signal noise and statistical outliers.

This is the 9th in the Departmental Pizza Seminar series.

A new paradigm for rigid body simulation is presented and analyzed. Current techniques for rigid body simulation run slowly on scenes with many bodies in close proximity. Each time two bodies collide or make or break a static contact, the simulator must interrupt the numerical integration of velocities and accelerations. Even for simple scenes, the number of discontinuities per frame time can rise to the millions. An efficient optimization-based animation (OBA) algorithm is presented which can simulate scenes with many convex three-dimensional bodies settling into stacks and other "crowded" arrangements. This algorithm simulates Newtonian (second order) physics and Coulomb friction, and it uses quadratic programming (QP) to calculate new positions, momenta, and accelerations strictly at frame times. The extremely small integration steps inherent to traditional simulation techniques are avoided.

Contact points are synchronized at the end of each frame. Resolving contacts with friction is known to be a difficult problem. Analytic force calculation can have ambiguous or non-existing solutions. Purely impulsive techniques avoid these ambiguous cases, but still require an excessive and computationally expensive number of updates in the case of many simultaneous contacts. It is shown informally that even taking into account advances in stiff integration techniques, penalty force methods cannot overcome this issue of running time in highly crowded scenes. New algorithms are presented that calculate simultaneous impulses to resolve collisions and static contacts under the Coulomb friction model. The simultaneous impulses are the solution to a QP.

In addition, the algorithms apply "bouncing at distance" and "freezing of bodies" to further speed up the simulation. These new QP algorithms are hybridized with a traditional priority queue momentum update scheme to allow sequential impulses when they are required for realism, such as in the office toy pendulum. When added to the implementation of OBA, these new algorithms increase the speed of the simulation by a factor of up to 30.

The position update has been hybridized with retroactive detection (RD) to prevent fast and thin bodies from passing through each other. Due to the modular design of the OBA simulator, the described techniques can be used as components in any existing simulator that follows a modular design of position update, finding contacts, and resolving contacts. Non-convex bodies are simulated as unions of convex bodies. Links and joints are simulated with bi-directional constraints. Analysis of the algorithm and discussion of example simulations is provided.

We discuss the security architecture for the Computer Science department. We review the goals and challenges of the environment, look at the technology used to respond to the challenges, and get into some detail about the proposed solution.

This is the 8th in the Departmental Pizza Seminar series.

As applications manipulate an increasing amount of XML, there is growing interest in storing XML data in relational databases. Due to the mismatch between the complexity of XML's tree structure and the simplicity of flat relational tables, there are many ways to store the same XML document in an RDBMS, and a number of heuristic techniques have been proposed. These techniques typically define fixed mappings and do not take application characteristics into account. However, a fixed mapping is unlikely to work well for all possible applications.

LegoDB is a cost-based XML storage mapping engine that explores a space of possible XML-to-relational mappings and selects the best mapping for a given application. LegoDB leverages current XML and relational technologies: 1) it models the target application with an XML Schema, XML data statistics, and an XQuery workload; 2) the space of configurations is generated through XML-Schema rewritings; and 3) the best among the derived configurations is selected using cost estimates obtained through a standard relational optimizer. In this talk, I will describe the LegoDB storage engine and present experimental results that demonstrate the effectiveness of this approach.

Joint work with Philip Bohannon, Prasan Roy and Jerome Simeon.

The need to visualize unstructured volumetric data arises in a broad spectrum of applications including structural dynamics, structural mechanics, thermodynamics, fluid mechanics, and shock physics. In this talk, I will focus on direct volume rendering, a term used to define a particular set of rendering techniques which avoid generating intermediary (surface) representations of the volume data. Instead, the scalar field is generally modeled as a cloud-like material, and rendered by computing a set of lighting equations.

I will present recently developed techniques for direct volume rendering of unstructured grids. First, I will talk about "projective methods". Direct volume rendering based on projective methods works by projecting, in visibility order, the polyhedral cells of a mesh onto the image plane, and incrementally compositing the cell's color and opacity into the final image. By combining a fast visibility ordering algorithm with extensive use of graphics hardware, it is possible to achieve real-time rendering of moderate size datasets with such techniques.

Then, I will present the ZSWEEP algorithm, which can be seen as an "extended" projective technique under a generalized hardware model. I will describe several features and (parallel, distributed, and out-of-core) extensions of the ZSWEEP algorithm. Because ZSWEEP is not limited by the amount of available main memory, it is suitable for rendering large data.

This work was done in collaboration with Joao Comba (Stanford/UFRGS), R. Cook (Lawrence Livermore National Labs), R. Farias (Mississippi State), J. Klosowski (IBM Research), N. Max (LLNL), J. Mitchell (SUNY, Stony Brook), and P. Williams (LLNL).

COMPACTION takes a set of "loosely packed" geometric objects and packs them "as tightly as possible." It is akin to sitting on a suitcase to get it to close. Compaction has three inputs: 1) a set of non-overlapping geometric objects, such as polygons or polyhedra; 2) allowable transformations of those objects, such as translations or rotations; 3) an objective function to be minimized, such as gravitational energy or the z-coordinate of the "suitcase lid". Compaction plans a simultaneous non-overlapping motion of the objects that moves them to a local minimum of the objective function.

OVERLAP MINIMIZATION takes overlapping objects as inputs and minimizes a measure of their overlap.

Algorithms are presented for compaction and overlap minimization of polygons, "circular" polygons (circular arcs allowed in the boundary), and polyhedra. These algorithms are based on linear programming or quadratic programming. They also use the MINKOWSKI SUM or the MAXIMAL CONVEX SUBSET.

Some of these algorithms are widely used in the clothing industry or are the basis for new techniques for computer animation. They also are an important part of other algorithms for PACKING or other GLOBAL minimization problems.

This is the 7th in the Departmental Pizza Seminar series.

Historically, wireless networks have been designed primarily to extend the domain of circuited switched telephone service over cellular telephony. However, wireless networks that support data have now begun to appear. The third and fourth generation wireless networking technologies and wireless systems are being designed to support packet data and multimedia services in addition to voice. A typical wireless network has to support multiple classes of users with different traffic characteristics and QoS (Quality of Service) requirements. The measure of QoS is the probability of forced termination (Pft) of a call that was allowed to access the network. Guaranteeing the promised QoS for all admitted users while maximizing network efficiency is one of the major challenges. Call Admission Control plays a key role in achieving promised QoS for the mobile terminals (MTs) in a given network. Two previous CAC algorithms i) Guard Channel Scheme ii) Call Admission Control with call Pre-blocking are studied which aim to decrease Pft. In this work, we study both these schemes through extensive simulation and it is found that although they provide required QoS for constant traffic, they fail to adjust to the dynamic nature of the system and sometimes underutilize the network resources. We then propose a new Call Admission Control Algorithm that uses Fuzzy logic to adjust to the changing traffic parameters and provide any level of QoS to the users. It is also shown that computational burden on such system is very minimum.

This is the 6th in the Departmental Pizza Seminar series.

Revision programming is a knowledge representation formalism for describing constraints on databases, knowledge bases, and belief sets, and providing a computational mechanism to enforce them. Constraints are represented by sets of revision rules. Revision rules could be quite complex and are usually in a form of conditions (for instance, if these elements are present and those elements are absent, then this element must be absent). In addition to modeling logical constraints, revision rules specify a preferred way to satisfy the constraint. Justified-revision semantics assigns to any database a set (possibly empty) of its revisions. Each revision satisfies the constraints, and all deletions and additions of elements in a transition from initial database to the revision are derived from revision rules.

In this talk, we present an elegant embedding of revision programs into logic programs, which does not increase the size of a program. The embedding naturally led to extensions of the formalism of revision programming corresponding to existing extensions of logic programming. We also discuss annotated revision programs, which allow annotations like confidence factors, combined opinions of multiple experts, etc.

The modern digital world, in which computation and communication are (nearly) free and (almost) unlimited, poses critical new challenges for management of rights and information. In this talk, we will discuss some cryptographic and mathematical aspects of the concepts and mechanisms of to ensure security of and user privacy in Digital Rights Management (DRM) technology.

It is clear that cryptographic techniques can be useful in the design of a DRM system. However, they must be applied with care to the DRM setting. For example, unlike the situation in some other cryptographic scenarios, the typical end users of a DRM system may not be fully trusted by the designers of the system. Furthermore, security measures must be as unobtrusive as possible if the DRM system is going to be successfully deployed. Both perspectives lead to interesting requirements for cryptographic solutions. Besides describing the mathematical foundations for useful cryptographic techniques we will also illustrate these real-world constraints with a number of examples as they apply to the architecture of a DRM system.

Dr. Tomas Sander is a Member of the research team at the "Strategic Technologies and Architectural Research Laboratory (STAR Lab)" at InterTrust Technologies, Santa Clara, California. Prior to joining InterTrust in 1999, Tomas spent three years as a postdoctoral fellow at the International Computer Science Institute (ICSI) in Berkeley, California, for which he had received a fellowship from ICSI. Tomas received his doctoral degree in mathematics summa cum laude from the University of Dortmund, Germany in 1996. He has published and lectured scientific articles in both the practical and theoretical aspects of cryptology, computational mathematics, the theory of computing, electronic commerce and Digital Rights Management. He was the program chair of the ACM Workshop on Security and Privacy in Digital Rights Management (Nov. 2001, Philadelphia).

The propositional satisfiability problem (SAT) is one of the most prominent and conceptually simplest combinatorial problems in computing science. Over the past ten years, substantial progress has been made in the development of stochastic local search (SLS) algorithms for SAT; empirical methods played a key role in improving our ability to solve large and hard SAT instances from a broad range of domains, and increasingly help us to gain a better understanding for the behaviour of state-of-the-art algorithms. Recently, advanced empirical methods, in particular the RTD-based approach for analysing and characterising the behaviour of randomised algorithms for SAT, have been used to study some of the best-performing SAT solvers known todate.

In this talk, I will first outline the empirical approach I use for analysing and characterising the run-time behaviour of SLS algorithms for SAT and other problems. I will then present some of the most recent results I obtained using this methodology and present a surprisingly simple and general model for the behaviour of SLS algorithms for SAT that is based on these results and accounts for many observations that were previously not well understood. Based on these insights, I developed a new, self-tuning variant of Novelty+, one of the best-performing SLS algorithms for SAT. This new algorithm achieves performance levels close to the peak performance reached by Novelty+ using instance-specific, manually tuned parameter settings.

Finally, I will give a brief overview of various lines of work that demonstrate how many insights obtained for SAT can be used for improving the behaviour of SLS algorithms for other combinatorial problems, including the winner-determination problem in combinatorial auctions and a code design problem relevant to DNA computing and molecular tagging techniques.

For further information on the presenter, see http://www.cs.ubc.ca/~hoos

Future broadband wireless access systems plan to integrate various classes of mobile terminals (MTs), each class with a different type of quality of service (QoS) requirement. When the load on a wireless network is high, the guarantee of QoS for each class of MTs is a challenging task. The measure of QoS is the probability of forced termination of a call that was allowed to access the network. Two previous handoff prioritization schemes - (i) prerequest scheme and (ii) guard channel scheme - decrease handoff failure (and hence forced termination). In this work, we compare and contrast both the schemes through extensive analysis and simulation; it is found that neither method can guarantee a desired level of QoS. We then propose a novel Call­Admission Control (CAC) algorithm that can maintain any desired level of QoS, while successful call completion rate is very high. In the proposed algorithm, the new call arrival rate is estimated continuously, and when the estimated arrival rate is higher than a predetermined level, some new calls are blocked irrespective of the availability of channels. The objective of this pre­blocking of calls is to maintain the wireless network­system's observed new call arrival rate at no more than a predetermined rate. We show that the proposed method can guarantee any desired level of QoS for profiled users.

This is the 4th in the Departmental Pizza Seminar series.

Self-assembly is the ability to establish a complex, hierarchical structure from simpler, independent entities without external intervention. Amino acids, one of life's basic biological structures, can spontaneously assemble in solution and fold into a protein. The arrangement of amino acids determines a protein's folded shape which in turn dictates its specific function. The amino acids must unite in a precise sequential order to form a functioning protein, much like letters in a language must be properly sequenced to make words, sentences, and poetry. Understanding the self-assembly process of proteins would make it possible to design proteins that carry out a specific task by linking together the appropriate amino acid sequence(s).

Proteins assume a number of intermediate conformations before reaching a local or global energy minimum. In this paper, a linear programming-based algorithm is applied to previously developed energy formulations in an effort to calculate the energy diminishing path of a protein in an aqueous solution. Background on the structure of proteins, our empirical energy functions, and our linear programming, position-based algorithm is provided. We then develop the theory behind optimization of single-stranded proteins. We explain how we calculate the energy-diminishing path of a protein and compare our results with those of other software. A recommendation for future study is included.

It is an exciting time in the history of science. While the DNA contains the blueprint for the creation and evolution of life, protein's are life's machinery that perform the important tasks. Solving the protein-folding problem would open a world of new medical opportunities. This endeavor is challenging, contains a rich source of interesting problems and combines several academic fields, notably mathematics, computer science, and biochemistry.

This is the 3rd in the Departmental Pizza Seminar series.

Optical Wavelength Division Multiplexed (WDM) networks offer the potential of substantially higher bandwidths in the order of multi-gigabit to terabits per second. Wavelength routed WDM networks are an attractive candidate for the next generation Internet and beyond. In such networks, the physical topology of the network may be represented as a graph with nodes representing wavelength routers, interconnected by multi-wavelength links. Given a session request, the routing and wavelength assignment (RWA) problem is to calculate the shortest-path between two nodes, and also assign a set of wavelengths along this path. In a conventional wavelength routed network, an entire wavelength is assigned to a given session (or circuit). This can lead to lower channel utilization when the individual sessions do not need the entire channel bandwidth. This work considers a TDM-based approach to reduce this inefficiency.

In this network architecture, each individual wavelength is partitioned in the time-domain into fixed-length time-slots organized as a TDM frame. Multiple sessions are multiplexed on each wavelength by assigning a sub-set of the TDM slots to each session. Thus, given a session request with a specified bandwidth, the goal is to determine the route, wavelength and time-slot assignment (RWTA) that meets the given request. In this work, we present a family of RWTA algorithms and study the resulting blocking performance. For routing, we use shortest-path routing that uses link costs based on a least resistance weight function, which incorporates link load and number of hops to choose the path. For wavelength assignment, we employ the known least loaded wavelength selection algorithm; and for time-slot allocation, we present the least-loaded time-slot algorithm with three different variations. Simulation based analyses are used to compare the proposed RWTA algorithm to traditional wavelength-routed networks with and without wavelength conversion. The goal is to compare the benefits of TDM and wavelength conversion in improving performance. The results show that the TDM/WDM architecture provides substantial gains, especially for multi-fiber networks.

This work was supported in part by Cisco Systems, San Jose, CA.

Dr. Krishna Sivalingam is an Associate Professor in the School of Electrical Engineering and Computer Science, at Washington State University, Pullman, where he was an Assistant Professor from 1997 to 2000. From 1994 to 1997, he was an Assistant Professor at University of North Carolina Greensboro. During summer months of 1996 and 1997, he conducted research at Lucent Technologies' Bell Labs in Murray Hill, NJ, and at AT&T Labs in Whippany, NJ respectively. He also served as consultant to AT&T Labs during 1997. He received his Ph.D. and M.S. degrees in Computer Science in 1994 and 1990 respectively from State University of New York at Buffalo where he was a Presidential Fellow from 1988 to 1991. Prior, he received his B.E. degree in Computer Science and Engineering in 1988 from Anna University, Madras, India.

His research interests include wireless and mobile networks, optical WDM networks, and performance evaluation. He is co-recipient of the Best Paper Award at IEEE International Conference on Networks (ICON 2000) held at Singapore in Sep. 2000. He served as Lead Guest Editor for a special issue of the IEEE Journal on Selected Areas in Communications in optical WDM networks. Dr. Sivalingam has co-edited a book on optical WDM networks, published by Kluwer Academic Publishers in March 2000. He has served on committees of several international conferences, and is presently serving as Technical Program Co-Chair of SPIE/IEEE/ACM OptiComm conference to be held at Boston, MA in July 2002. His work has been supported by AFOSR, DoD Laboratory for Telecommunication Sciences, NSF, Cisco, Alcatel, Intel, Telcordia Technologies, and Washington Technology Center.

In this talk, we address the problem of constrained exploration of an unknown graph G=(V,E) from a given start node s with either a tethered robot or a robot with a fuel tank of limited capacity, the former being a tighter constraint. In both variations of the problem, the robot can move along only the edges of the graph, i.e, it cannot jump between non-adjacent vertices. In the tethered robot case, if the tether (rope) has length l, then the robot must remain within distance l from the start node s. In the second variation, a fuel tank of limited capacity C forces the robot to return to s after traversing C edges. The efficiency of algorithms for both variations of the problem is measured by the number of edges traversed during the exploration. We present an algorithm for a tethered robot which explores the graph in q(|E|) edge traversals. The problem of exploration using a robot with a limited fuel tank capacity can be solved with a simple reduction from the tethered robot case and also yields a q(|E|) algorithm. This improves on the previous best known bound of O(|E| + |V|log^2|V|). Since the lower bound for the graph exploration problems is |E|, our algorithm is optimal, thus answering the open problem of Awerbuch, Betke, Rivest, and Singh.

We also extend our results to a modified version of the shortest path problem called the treasure hunting problem. Here a robot wishes to quickly discover some treasure from an unknown graph. We conclude our talk with some interesting open problems.

This is the 2nd in the Departmental Pizza Seminar series.

Key concerns in the development of more powerful ATP systems are to provide breadth of coverage - an ability to solve a large range of problems, and to provide greater depth of coverage - an ability to solve more difficult problems, within the same resource limits. This work describes the design and implementation of CSSCPA, a compositional competition-cooperation parallel ATP System. CSSCPA combines existing high performance ATP systems in a framework that allows them to work independently, but also allows communication of intermediate results. The performance data shows that CSSPCA has high breadth and depth of coverage.

This is the 1st in the Departmental Pizza Seminar series.

Various computational techniques have led to discoveries in pure mathematics. These techniques include computer algebra, automated theorem provers, constraint solvers and automated theory formation programs. I will give a brief survey of some discoveries made in this way, then concentrate on our particular approach: the HR automated theory formation program. I will give some details of how HR works, and then discuss some of the mathematical results it has discovered in various domains. I will conclude with an exploration of refactorable numbers, which are such that the number of divisors is itself a divisor.

Until recently database systems were totally focused to organization and retrieval of structured data. Unstructured and semi-structured data were being managed by independent software packages built on top of file system stores or some other stores not integrated tightly with database systems. In recent times, however, with explosion of information people have started to realize importance of a tighter integration of such data with database store for the sake of inter-operability, reliability, scalability, maintainability and efficiency. Building full-text indexes as integral part of a database system is a first attempt towards that goal. Full-text indexes, inherently, come in with problems not seen usually in database applications before. Problems are mostly around the issue of scale. The talk will highlight such issues and how they impact design strategies and how some of them are addressed in present versions of Microsoft SQL Server.

Dr. Tapas K Nayak did his PhD in Computer Science from Indian Institute of Technology, Kharagpur, India, in 1992. He is presently with Microsoft at Seattle and is involved in architecting future version of full-text indexing in Microsoft SQL Server. He had earlier been a faculty at Indian Institute of Technology, Kanpur, India. His current interests lie in databases, data structures, very large system design, and computer languages.

In this talk we survey the close connection between the solution set of a finite system of linear Diophantine equations and semilinear sets. Linear sets generalize arithmetic progressions to several dimensions. The closure under union of the linear sets yields the semilinear sets, which by a kind of miracle are closed under all Boolean operations.

We give a high-level, conceptually transparent algorithm that reveals both the structure of the solution set of a system of linear Diophantine equations and its computational complexity. Along the way we also point out an important connection between the set of support of multivariate rational series and general Diophantine polynomials.

Dr. Bruce Litow is a senior lecturer in the School of Information Technology at James Cook University. His principal research interest is the computational complexity of arithmetic and algebraic problems.

Automated theorem proving (ATP) is an area of growing importance in many industrial and scientific applications. In particular, ATP systems are increasingly being used to formalize mathematical theories and results, or to verify the design of hard- and software products. Most of the current high-performance ATP systems are based on an equational paradigm.

However, while such ATP systems are extremely versatile and powerful tools, this power comes at a price. ATP systems for most interesting logics have to search for proofs in an infinite search space. This search is typically controlled by heuristic evaluation functions, which are used to select the "best" alternative at the important choice points during the search. The performance of nearly every fully automatic ATP system depends critically on the quality of these evaluation functions.

In this talk, I will present an approach to learn good evaluation heuristics from many previous proof experiences. Search decisions are represented by patterns of clauses, and evaluations for these patterns are learnt by analysis of the use of matching clauses in previous proof searches.

The approach was successfully implemented and tested in the superposition-based prover E/TSM. The talk concludes with a live demonstration of the proof system.