UBCCSSS has started a newsletter! It will contain information about
upcoming events, workshops, and more. If you would like to subscribe
to the newsletter, please click the button below.
Byron Cook is a researcher at Microsoft’s research lab at Cambridge University:
In this talk I will discuss Terminator, the first known automatic program termination prover to support large programs with arbitrarily nested loops or recursive functions, and imperative features such as references, functions with side-effects, and function pointers.
Terminator is based on a newly discovered method of counterexample-guided abstraction refinement for program termination proofs. Additionally, to increase the proof power, Terminator computes inductive invariants of the program when checking the lemmas that imply termination. The talk will close with results from recent experiments with Terminator on dispatch routines from Windows device drivers. This is joint work with Andreas Podelski and Andrey Rybalchenko.
Is our discipline of computer science in a time of crisis? Our field has helped unlock the human genome, has allowed a hand-held device to be a gateway to the world’s information, and has transformed communication and society. Yet students do not want to study computer science. Do enrollment trends portend serious problems requiring immediate solutions or is the crisis greatly exaggerated?
In 1988 Dijkstra excoriated the then current practice of teaching computer science by programming computers using ad hoc methods when he wrote about the “Cruelty of Really Teaching Computer Science”. When we revisit this question today we must rise above discussions about whether Scheme is better than Java, which IDE is better for novices, and what the role of the command-line is in today’s curriculum. We must discuss whether teaching computer science today should be based on understanding recursion and the Towers of Hanoi or a single nucleotide polymorphism in a DNA sequence. We need to leverage new modes of access and communication in developing and building our curriculum. Should we build our courses on concepts that will let our students design and build the next BLAST or the next Web-CT?
In this talk I will discuss possible directions we can take in teaching computer science and why if we look to ourselves for answers, rather than to other disciplines, we may lose our franchise within the university.
Many domains in the real world are richly structured, containing a diverse set of objects, related to each other in a variety of ways. For example, a living cell contains a rich network of interacting genes, that come together to perform key functions.
A robot scan of a physical environment contains diverse objects such as people, vehicles, trees, or buildings, each of which might itself be a structured object. And a website contains a set of interlinked webpages, representing diverse kinds of entities. This talk describes a rich language based on probabilistic graphical models, which allows us to model domains such as these. We show how to learn such models from data generated from the domain, and how to use the learned model both to gain a better understanding of the principles underlying these domains, and to allow us to analyze a new data set from these domains in order to recognize the entities in it and the relationships between them. In particular, I will describe applications of this framework to various tasks, including: recognizing regulatory and protein interactions in a cell from diverse types of genomic data; segmenting and recognizing objects in robot laser range scan data; and identifying the set of entities in a structured website and the relationships between them.
There are many applications where one needs to search for a “function” that has “minimal energy” while satisfying some boundary constraints. As a simple example, consider the problem of finding the minial area soap bubble surface that spans a wireframe boundary. Numerical methods are typically only good at finding local minima to such varational problems.
In this talk, we show how global optima can be found as the limit of a set of purely combinatorial problems. These combinatorial problems can be thought of higher dimensional analogues of the “shortest path in planar graph” problem. For example, when the problem dimension is 3, the combinatorial problem is to find a “discrete minimal surface” in a volumetric cellular complex. We then show how these combinatorial problems can be solved in polynomial time by reducing them to instances of MIN-CUT. If time permits, we will also explore an application of these ideas to 3-camera stereo vision. More information: [http://www.cs.ubc.ca/events/seminars/csicics.shtml](http://www.cs.ubc.ca/events/seminars/csicics.shtml)
Byron Cook is a researcher at Microsoft’s research lab at Cambridge University:
Is our discipline of computer science in a time of crisis? Our field has helped unlock the human genome, has allowed a hand-held device to be a gateway to the world’s information, and has transformed communication and society. Yet students do not want to study computer science. Do enrollment trends portend serious problems requiring immediate solutions or is the crisis greatly exaggerated?
Many domains in the real world are richly structured, containing a diverse set of objects, related to each other in a variety of ways. For example, a living cell contains a rich network of interacting genes, that come together to perform key functions.