Research Projects for Summer 2014

This links to some extra-departmental opportunities...

Please apply by Feb. 16, 2014 via the link at left...

HMC Projects

Observationally Cooperative Multithreading

Programmers face a multi-core future but no one knows how to take advantage of it. Current techniques for concurrency tend to be primitive, complicated, and error-prone. This project will investigate OCM, a new approach to writing concurrent code without the hassle and bugs of locks. Programmers write code as if each thread has the machine to itself until it explicitly yields control; under the hood, the system detects noninteracting threads and runs them simultaneously.

Students are needed both to continue past work on the design and implementation of OCM, and to apply OCM to real problems (to measure efficiency and ease-of-use). Work on the system would benefit from CS 131 (Programming Languages) and/or CS 105 (Computer Systems) as background, but the application and measurement work should be accessible to students finishing their first year at HMC. Directed by Profs. O'Neill and Stone.

Proof Checking for Mathematical English

Errors in software become more expensive and dangerous each year. Testing is helpful, but proofs are the only way to truly guarantee that an algorithm is correct, or that a cryptographic protocol is secure, or that a programming language is safe.

Unfortunately, it's hard to get all the details of a big proof right; even careful reasoners make mistakes, and even careful readers miss them. Automation seems a natural solution, and there do exist "proof assistant" systems that help people construct proofs that can be automatically checked. In the end, though, we have a proof that we are sure is correct, yet which is almost unreadable if you're not a computer.

I want a system that can verify proofs that were written for humans to read and understand, the kind of proofs you see in textbooks and research papers. Essentially, I want to go beyond spell-checking and grammar-checking to logic-checking.

This is a new project, so we'll start by experimenting. The goal of the summer is an exploratory prototype that handles arbitrary English-language proofs about some very simple topic (such as theorems of propositional logic). Even this will be challenging, because no two people use exactly the same words to make the same argument. But if we are successful, we will have the kernel of a system that can be extended over time, covering more and more areas of mathematics and computer science. (Directed by Prof. Stone)

Computer Science Teaching Tips

I have a research project to help new CS teachers be more awesome. There are a lot of resources for new CS teachers online, but they're hard to find! This semester (Spring 2014) we'll develop hooks (FB posts, tweets, blog posts) to direct new CS teachers to these resources! Over the summer we'll continue this work and start interviewing expert CS teachers to provide more information to new CS teachers. You can read about the project at (Directed by Prof. Lewis.)

Equity in CS with Kids

There are three lines of work that relate to equity within CS:

Line 1: What do kids think about studying CS?

In this project we'll listen to interviews of 11 year olds when they talk about what makes CS appealing and unappealing. We'll compare this to interviews with college students from UC Berkeley and UW Seattle. We'll try to identify what pattens there are in student responses and how these patterns are different than what college students say. We'll read previous research about the topic and identify what new, interesting information we can contributed to the community's understanding of how kids think about studying CS.

Line 2: How do kids learn to abstract?

In this project we'll watch a bunch of videos of kids solving problems that involve abstraction. We'll look for patterns in how students reason about the problems and think about how this might help improve CS instruction for kids. We'll read previous research about how kids deal with abstraction in CS and math. (It is great if your reaction was "what the heck does Colleen mean by Abstraction???" - We'll be looking at how kids make the jump to use a loop to repeat something. Compare the following pseudo code: print "Z"; print "Z"; print "Z"; print "Z"; vs. Repeat 4 [print "Z"]. This jump to the second version is hard for ~11 year old kids!!!)

Line 3: Interviewing kids about CS

In this project, you'll interview kids about different CS concepts. These interviews will take place in the bay area (Point Richmond) in the month of July, so part of the summer you'll spend at HMC and part of the summer you'll spend in the bay area. While in the bay area you'll be responsible for paying for your own housing, but I'll help you find somewhere to live! (Directed by Prof. Lewis.)

Trace Repository

The SNIA Trace Repository contains several terabytes of data collected by observing the behavior of real file systems. Harvey Mudd is responsible for the management and enhancement of this repository. Students will develop tools related to traces, help write standards, locate, convert, and post new traces, and integrate tools contributed by researchers. (Directed by Prof. Kuenning.)

Big Data - Small Energy

Data centers are the cathedrals of our age, yet they consume far more energy than required under everyday conditions. This new NSF-funded project will investigate how zettabyte- (and larger-) scale systems can be designed and implemented in order to strike different balances between performance and energy consumption. (Directed by Prof. Kuenning.)

Photo Shoot

This project is looking for students who are interested in creating -- and being featured in -- material highlighting HMC CS, e.g., promotional materials and posters. (Directed by Prof. Kuenning.)

Java Modeling Language Tools and Specifications

The Java Modeling Language (JML) is a formal specification language for Java software. JML specifications can be used for static verification (checking an implementation against its specification through code transformation and automated satisfiability checking/theorem proving) and runtime checking (instrumenting implementations with additional code that monitors its behavior for correctness while it is running). There are many potential summer projects related to JML; the following are two.

Tool Research and Development. The current set of tools that support JML static checking, runtime checking, and automated testing need significant research and development work: the runtime checking support is limited, there are large portions of JML (in particular, those with quantifiers and set comprehensions and those dealing with issues like resource utilization, ownership of data, well-foundedness of recursion, and concurrency) that are not supported, the tool user interfaces are very rough around the edges (in the case of the testing tool, nonexistent), and the testing tool currently uses a fairly naive technique to generate automated tests.

Library Class Specification. We need formal specifications for the Java Standard Library in order to verify/check real Java programs that call library functions. Some of these specifications exist, but many critical areas of the library still need specifications and more classes are added to the library every Java release. Writing high-quality library specifications is hard, and requires human intervention, but it should be feasible to develop a method to automate a large portion of the process - very valuable, since there are almost 4,000 classes in the current library! - and carry it out on some critical parts of the library that have not yet been specified. (Directed by Prof. Zimmerman.)

Arcade-machine repair

This project is looking for students who are interested in helping a pair of arcade game machines to a functional state. Visit this online poker site to learn about how poker and poker cards work in order to solve puzzle. See Prof. Zimmerman, if you are interested... .

Games for Education

Students in CS 121 design and develop educational games for social studies middle school students. Given the semester time limits, these games are not always completed. Summer research students on this project will work with middle school student 'customers' to evaluate the games, propose modifications/enhancements of the games to make them classroom-ready, and implement the changes so the games are ready to be deployed. (Directed by Profs. Erlinger and Sweedyk.)

MyCS: Middle-years Computer Science

This project seeks to increase computational awareness in students at an age when they are open to new ideas -- in particular, at the middle-school and early high-school level. If you'd like to help develop a middle-school CS curriculum and present two week-long summer workshops to a small group of middle- and high-school teachers, join us! (Directed by Profs. Erlinger and Dodds.)

Summer Staff

Summer staff is a small group of students who help maintain and improve our CS department's computational infrastructure: software, hardware, and usage patterns/policies. No previous systems-administration experience is required: you will learn about the systems that It's fun, vital for the department, and an ideal chance to expand your systems knowledge -- join us! (Directed by Prof. Wiedermann.)

Intelligent Music Software

The Impro-Visor (Improvisation Advisor) project has been developing educational software tools to help students learn to improvise music, particularly jazz. Our approach is to aid the student in constructing melodies similar to ones that could be improvised, in order to get a better understanding of harmony and its relationship to melody construction. Two types of advice given are: empirical advice, based on a database of stored melodies that match certain chord changes, and grammatical advice, based on a grammar that generates melodies on the fly. This free software tool has been used in classroom settings for six years and has over 8000 registered users at present. In addition to its primary function, it provides a microcosm of examples for software development, including knowledge representation and real-time execution of music accompaniment. (Directed by Prof. Keller.)

Anticipated areas of focus for summer 2014 include:

  • Learning Melodic Components based on Harmonic Bricks: We currently use a method for extracting grammars from a corpus of jazz solos based on clustering and hidden-markov models. The proposed research will reorganize solo generation and learning based on idiomatic harmonic bricks, as outlined in our paper A Creative Improvisational Companion Based on Idiomatic Harmonic Bricks.
  • Audio Input and Enhancement Real-Time Aspects of Impro-Visor: We would like Impro-Visor to become a better companion for accompanying and trading melodies with the user. Ideally, the real-time improvisor would emulate the thought processes of a human improvisor at a macro scale. Many of the features of the tool are capable of working in real-time, but there are ergonomic interface and knowledge-representation issues to be researched. Work remaining includes improving the current audio-in interface, which is based on Supercollider, and developing one or more musical approaches for reacting to audio input.

Evolution of Verified Software

We would like to establish the application of genetic programming to the co-evolution of programs along with their proofs. A genotype in our case represents not simply a program as with previous work on genetic programming, but rather a program and the necessary assertions that can be used to complete a proof of the program. The advantage of this approach, if successful, is that the evolved programs are guaranteed to be correct, unlike former approaches that empirically base program adequacy solely on test cases. If successful in this basic proof of concept, we believe that we the power of networks of computers can be harnessed to make the process more efficient. (Directed by Prof. Keller.)

There are several challenges involved in this work:

  • Development of an appropriate genotype formalism that combines program syntax and assertions.
  • Development of a family of fitness functions for evaluation of genotypes.
  • Adaptation of a prover capable of checking a proof of a phenotype program together with the evolved assertions. We say "adaptation," rather than development, because we would prefer to exploit existing technology for the proof checker rather than try to develop it from first principles ourselves, which would be a substantial undertaking in its own right.

Human Agent Teaming

We all know students for whom what they want to do supersedes what they should do, and vice- versa. For most students, a well-balanced flow that avoids both extreme procrastination and extreme fatigue leads to a happier, more-productive, and more-satisfying existence. This project looks at designing a smart phone app that acts as friendly, motivating study buddy. This project explores how to (1) recognize and represent the competing motivations of human users, (2) generate agendas that effectively balance these competing motivations, and then (3) provide users with timely, convincing prompts that guide them towards more rewarding behavior.

This leads to many interesting research questions. How do we guide the dynamic intentions of users to progressively improve their time management without frustrating them? Can we augment current automated planning and scheduling techniques to dispatch timely and impactful advice? Or is it more effective to provide users with concise summaries of the down-steam implications of scheduling decisions? Can selectively deferring decision-making to the user help engender a sense of trust and autonomy while eliciting preferences and constraints that can improve problem solving?

The goal of this summer project is to develop a prototype smartphone application that can be used to perform a user study involving students from HMC in the Fall 2014 semester. Directed by Prof. Boerkoel.

3d Robotics

Mapping with a single camera is a compelling problem because we humans have no trouble wandering a new environment (even with one eye closed). What's more, we can subsequently use that experience to get around and perform tasks.

We certainly cannot hope to re-derive the amazing progress in this field! Thus, the 2014 project will depend heavily on the software scaffolding of ROS (the Robot Operating System), PCL (the Point Cloud Library), OpenCV (the Open Computer Vision library), and other helpful systems we encounter. Our concrete goal is to use autonomous navigation of our indoor space to build a 3d model that, in turn, supports both virtual and actual "fly-throughs" of that environment. (Directed by Prof. Dodds.)

CS 5 for All!

Liked CS 5? Interested in improving the CS experience for future students or non-Claremont students? Would you like to learn/develop Javascript, AJAX, web-framework skills, etc. by making our CS 5 submission system (even) better? If any of these apply, join us for this project to adapt and improve CS5 for many different audiences. Especially on tap this summer are building new projects and assignments that overlap with other disciplines, e.g., biological imaging, physics and chemical simulations, and audio-analysis. (Directed by Prof. Dodds)

Vice-chancellor of fun position

If you are applying to an HMC summer position and would enjoy working as the social coordinator for the program and for all of HMC CS summer research, then this vice-chancellor of fun position will be of interest. It adds a $1000 stipend to your existing summer stipend and puts you in charge of procuring summer foodstuff and organizing activities (or encouraging others to do so!) You need to have a driver's license, a willingness to drive the large HMC van, and enthusiasm for making things happen! (Directed by Prof. Dodds)