Google Summer of Code 2009

For the last few years, Google has offered a fantastic opportunity for students to help out Open Source software projects in the summer while getting paid for it. It's called Google Summer of Code™, and it provides free software projects a great way of attracting development effort while providing software developers who are still in university with some interesting and useful experiences. Find out more about the Summer of Code (SoC) from their site.

Event-B is a formal method for system-level modelling and analysis. Key features of Event-B are the use of set theory as a modelling notation, the use of refinement to represent systems at different abstraction levels and the use of mathematical proof to verify consistency between refinement levels. You can know more of Event-B by reading materials available on http://www.event-b.org/

The Rodin Platform is an Eclipse-based IDE for Event-B that provides effective support for refinement and mathematical proof. The platform is open source, contributes to the Eclipse framework and is further extendable with plugins.

We would like to participate in 2009's Summer of Code.

See also GSoC 2009 FAQ.

Notes on applying

Here are some tips on what you might want to include in your application.

• First of all: get feedback on your proposal from the community. The devel mailing list is a good channel for that. Ask around and get to know some people, see if they think your project is feasible or how you should change the scope to better fit the timeline and the project. (If you are new to Open Source development, reading this part of "Producing OSS" may help you find the right tone.) Talking to people before applying dramatically increases your chances of approval: it shows us that you are genuinely able to communicate your ideas, allows us to gauge your expertise level and see who might be the right mentor for you.

• Tell us about yourself. We don't know you, so it helps if you give an outline of your background and what your prior experiences are (e.g. Open Source development, using Eclipse, general software engineering experience or education). If it turns out you wouldn't be a good fit for the Rodin platform or your project idea, it's helpful for everyone involved if that can be determined before you get started. However, don't hesitate to apply just because this would be your first time working in Open Source or with Eclipse; at some point this was new for each of us.

• Make it clear that you've thought through your application. Don't use a project idea from this page verbatim. Instead, come up with your own proposal, or expand on a proposal from this page. Explore the code a little bit. Make a clear schedule to show the intermediate milestones you'll reach while progressing towards your final goal.

• Let us know why you care, what you like about formal methods in general and Event-B and the Rodin platform specifically, what things you think could be improved and how they could be improved. We like working on this project because this project makes our work more effective, and we hope you'll like it, too. Showing your motivation helps.

Getting things done

Some tips on how you can get to project completion within the scheduled timeline.

• Working on the Rodin platform in the summer should be your main activity. Having a vacation for one or two weeks is fine, of course, but we want you to take the project and the time mentors put into it seriously. If you are working two other jobs this summer, that probably won't work. Realize that collaborating on software development takes time, and not just the time used to reason about and write the code. This also means that we want you to set some intermediate milestones to be able to keep track of your progress.

• Communicate. In some ways, open source software development is more about communicating than about writing code. Some part of your time will be spent writing code, but a large part of the time spent will go towards explaining the code on mailing lists, asking and answering questions on IRC and in general reasoning about proposed software changes. If you can't do this, you take the risk of not understanding the goals of our project or not being able to explain why your patch is necessary.

• We want you to work in the open, with our community. Get on the mailing lists, both to ask for help and to provide it to other users, spend time on IRC (#rodin on irc.freenode.net) discussing your work with other developers.

• We're not going to just compare what you did at the end to what you stated you'd be doing in the beginning. We want you to put effort into the project, to think about the feature you're doing, to communicate with the community and integrate your code with the project. If you end up implementing some other cool feature or fixing some annoyance, that is great as well.

Project Ideas

Here are a bunch of project ideas you might like to apply for. Of course, if you have a different idea of something in the Rodin platform that badly needs fixing or some feature you think would make a difference, go ahead and apply with it!

Tool Support for Design Patterns

Objective

Reusing formal models in order to reduce the effort of modelling and proving is an important aspect of the Event-B method. The background theoretical work for design patterns in Event-B has been done as part of a master thesis. The objective of this project is to have a tool support for this work as a Rodin plug-in. There are strong interests from some industrialists with this pattern work.

Expectations

• Study the concept of Event-B patterns.

• Study the architecture of the Rodin platform.

• Implement the tool as a Rodin platform plug-in (Eclipse plug-in) .

• Evaluate the tool on a set of example.

• Prepare basic documentation for users.

Requirements

• Good communication skill.

• Good command of Java programming.

• Interested in formal methods.

Mentor

• Thai Son Hoang <htson at inf dot ethz dot ch>.

Optional

• Basic step-by-step tutorial for using the plug-in.

Connection to External Provers

Objective Currently the Rodin platform uses self-made automatic theorem provers to support the user in proving. There is a number of powerful first order theorem provers available. The purpose of this project is to connect one of them to the Rodin platform.

Expectations

• Study the architecture of the Rodin platform.

• Study the interface of the external prover.

• Implement the connection as a Rodin plug-in.

• Document the source code properly.

• Evaluate and test the tool.

Requirements

As an applicant,

• you have some background in logics,
• you are an experienced Java programmer,
• you have already successfully written a more-than-500-lines piece of software, preferably in teamwork,
• you are willing to learn how to code an Eclipse plug-in.

Mentor

• Matthias Schmalz <Matthias.Schmalz at inf.ethz.ch>

Optional Evaluate and optimize the connection to the external prover.

Evaluating the Rodin Provers

Objective

In order to optimize the Rodin provers, we need to compare several (prover-) configurations on a large number of proof obligations. The objective of this project is to write a plug-in supporting a systematic evaluation of prover configurations. Important features are:

• The user exports certain proof obligations together with their proofs. (He later sends them to the developers.)

• The developer imports proof obligations from the users.

• Generate statistics about how effective different prover configurations are.

The following information should be easily accessible:

• How many proof obligations does a given configuration discharge?

• Which configurations discharge a given proof obligation?

• Given a manual proof and an external prover: how many manual steps (within the manual proof) are necessary before the external prover can be successfully applied?

Expectations

• Study the architecture of the Rodin platform.

• Think about the requirements of the plug-in.

• Implement the tool as a Rodin platform plug-in (Eclipse plug-in).

• Document the source code properly.

• Evaluate and test the tool.

Requirements

As an applicant,

• you are familiar with the Rodin platform,
• you are an experienced Java programmer,
• you have already successfully written a more-than-500-lines piece of software, preferably in teamwork,
• you are willing to learn how to code an Eclipse plug-in.

Mentor

• Matthias Schmalz <Matthias.Schmalz at inf.ethz.ch>

Optional Write some user documentation.

Students Considering Application

Andreas Fuerst

• Project: Tool Support for Design Pattern in Event-B

• Motivation:

• Background:

• Milestone: