Research Buffet
Friday, September 9, 2011
3147 MEB
Refreshments 3:40 p.m.
Lecture 4:00 p.m.
Jur van den Berg
Assistant Professor
Title: Recent advances in collision avoidance and motion planning for autonomous robots
Friday, September 9, 2011
3147 MEB
Refreshments 3:40 p.m.
Lecture 4:00 p.m.
Jur van den Berg
Assistant Professor
Title: Recent advances in collision avoidance and motion planning for autonomous robots
Abstract
One of the main challenges in robotics is to create truly autonomous robots for home, hospital, and public environments. This talk will focus on the challenges of autonomous motion for mobile agents and presents an overview of my work on reciprocal collision avoidance, with applications in mobile robotics, crowd simulation, and animation of virtual characters for computer games. I will also discuss my recent work on planning and control under motion and sensing uncertainty with applications in medical robotics, such as automated robotic surgery and robotic control of steerable needles. Finally, the long-term prospects for the future development of robot autonomy as it relates to these application domains will be discussed.
Ganesh Gopalakrishnan
Professor
Title: Taking Formal into areas unaccustomed to it
One of the main challenges in robotics is to create truly autonomous robots for home, hospital, and public environments. This talk will focus on the challenges of autonomous motion for mobile agents and presents an overview of my work on reciprocal collision avoidance, with applications in mobile robotics, crowd simulation, and animation of virtual characters for computer games. I will also discuss my recent work on planning and control under motion and sensing uncertainty with applications in medical robotics, such as automated robotic surgery and robotic control of steerable needles. Finally, the long-term prospects for the future development of robot autonomy as it relates to these application domains will be discussed.
Ganesh Gopalakrishnan
Professor
Title: Taking Formal into areas unaccustomed to it
Abstract
Every area of concurrent programming requires formal correctness frameworks within which its designers can safely conduct performance optimizations. Our interest is in contributing formal methods for high performance computing. The main set of challenges that HPC faces in this regard is the use of multiple concurrency models and APIs to support a mixture of legacy and new software, millions of threads running on heterogeneous cores, and an impoverished base of formal methods to start from. We show that by attempting to formalize even age-old APIs such as MPI, one learns about the formal model underlying message passing concurrency, and this can not only help build correctness tools for MPI programs, but understand similar issues sure to arise in future HPC programming proposals. We show that understanding MPI's `matches-before' order is crucial to building formal dynamic verification tools, and resource-dependent correctness outcomes. We show how unmodified MPI applications can be dynamically analyzed on 1000-CPU platforms. We also briefly cover another line of work that involves modeling and analyzing SIMD concurrency in GPU-based programs through SMT-based methods.
Every area of concurrent programming requires formal correctness frameworks within which its designers can safely conduct performance optimizations. Our interest is in contributing formal methods for high performance computing. The main set of challenges that HPC faces in this regard is the use of multiple concurrency models and APIs to support a mixture of legacy and new software, millions of threads running on heterogeneous cores, and an impoverished base of formal methods to start from. We show that by attempting to formalize even age-old APIs such as MPI, one learns about the formal model underlying message passing concurrency, and this can not only help build correctness tools for MPI programs, but understand similar issues sure to arise in future HPC programming proposals. We show that understanding MPI's `matches-before' order is crucial to building formal dynamic verification tools, and resource-dependent correctness outcomes. We show how unmodified MPI applications can be dynamically analyzed on 1000-CPU platforms. We also briefly cover another line of work that involves modeling and analyzing SIMD concurrency in GPU-based programs through SMT-based methods.