Project Proposals

These project proposals are written by KindSoftware researchers and may be chosen by advanced undergraduates for undergraduate theses, M.Sc. students for theses (at ITU and elsewhere), and visiting undergraduate and postgraduate Summer internship students.

Note that all of these projects actually fall under multiple categories but are only listed under their dominant category.

Projects in an emphasised font are no longer available as someone is working on the problem at this time.

Choose the links at right for more information about past and long-term projects.

(November 2011) ITU BSc and MSc students looking for an independent study or thesis project: please have a look at the below brief summary of projects that I'm current interested in supervising.

Each project has a name, a "Hollywood" pitch, a precondition that stipulates what you need to know to attempt the project, and a postcondition that summarizes what you will learn if you succeed in the goals of the project. Also included in each description is its "secret sauce," which is the primary ingredient that makes the project special. All of these projects have a proper research sub-component and all are potential fonts for a peer-reviewed published paper.

• Flatland - Abbott's Flatland using Artificial Life
  requires Visual Studio, C#, interest in AI and ALife, basic understanding of physics
  ensures core concepts, technologies, and algorithms of AI and ALife; 2D physics
  secret sauce 21st century AI and artificial life research + Farseer physics engine + Joe's past work in Distributed Artificial Life (published in USA Today and Wired around 10 years ago)
• Walking with Dinosaurs - evolve dinosaurs that can move on their own accord
  requires C or C++, interest in AI and ALife, basic understanding of physics, familiarity with 3D graphics engines use
  ensures core concepts, technologies, and algorithms of AI and ALife; 3D physics; dinosaurs
  secret sauce real dinosaur data + the Havoc physics engine + Karl Sims's Evolved Virtual Creatures
• BON for C# - connect BON to C#
  requires Visual Studio, C#, Code Contracts, BON
  ensures compilers, refinement theory, static checkers
  secret sauce Beetlz meets Code Contracts
• Google+Mozilla - Chrome+Firefox + V8/SpiderMonkey
  requires compilers, C++, JavaScript
  ensures compilers, optimization, static analysis
  secret sauce Joe knows Brian Rakowski, the project manager of Chrome, Kevin Milliken, the one of the main guys responsible for V8, and Brenden Eich, the inventor of JavaScript and CTO of the Mozilla Foundation, and they all want to figure out a way to work together with us. The three sub-projects that I am interested in are: (1) experiment with basic and advanced standard compiler optimizations in V8, particularly those that come from historic dynamic languages, (2) experiment with static analysis of gradually typed JavaScript with an aim toward performance optimization or correctness, and (3) profile V8 for a large body of example code for a particular popular tool/framework (e.g., Node) with an aim toward identifying hot-paths, possible architectural changes, and optimizations to improve performance or correctness.
• B/VDM/Z - old-school system specification and reasoning meets Open Source Software
  requires basic concepts of formal specification and reasoning, Visual Studio+C# or Eclipse/IntelliJ+Java
  ensures deep knowledge of at least one of B, VDM, or Z
  secret sauce Joe is good friends with the creators and main proponents of these three specification languages and all have new Open Source toolkits available (Rodin, Overture, and the CZT). Potential projects in this domain include: (a) integrating the lightweight ProverEditor plugin for Eclipse with VDM's HOL proof generation and Eclipse integration, (b) develop a new SMT-LIB backend for the VDM tool suite.
• AutoGrader for Visual Studio - automatic grading of analysis, design, architecture, validation and verification for C#
  requires Visual Studio (and add-ins), C#, Code Contracts
  ensures Visual Studio add-in development, MSTest, ReSharper, NUnit, StyleCop, FxCop, etc.
  secret sauce reuse architecture from our Eclipse AutoGrader and systems from the Microsoft world
• CLOPS generation of Eclipse plugins - use a Domain Specific Language for the specification and generation of advanced command-line argument processing to automatically generate an Eclipse plugin/feature that wraps the corresponding command-line tool
  requires Eclipse, parsers
  ensures Eclipse plugin/feature development, automatic software engineering via code generation
  secret sauce CLOPS is already shipped and being used in many projects
• java.util.logging and log4j facade for IDebug - help developers plugin/adopt an advanced logging infrastructure by migrating from existing popular APIs
  requires Java, Eclipse, JML, Javadoc, patterns
  ensures patterns, logging APIs
  secret sauce patterns for fun and profit
• rigorous development, validation, and verification of DiVS - complete the implementation and V&V of what might be the next system used in Denmark to determine the outcome of national elections
  requires Java, JML, BON, design by contract, software architecture
  ensures automated unit test generation, semantic static analysis, rigorous scenario-based testing
  secret sauce DiVS is the result of a top MSc thesis at ITU and is ready to move to the next level
• OpenJML - contribute to the modern JML tool suite for Java 1.7
  requires Java, Eclipse, parsers, compilers
  ensures typing and type checking, runtime assertion checking, code generation, extended static checking, automated theorem proving
  secret sauce large community of users, developers, and scientists desperate for a new major release
• an Open Source Digital Voter List system - design and develop an Open Source replacement for the proprietary, expensive Digital Voter List system developed and supported by KMD, used to generate and check voter cards in the 2011 national elections
  requires software engineering
  ensures networking, security, cryptography
  secret sauce the government would use an Open Source solution in lieu of the proprietary one if it were of high quality and supported by volunteer Danish citizen-activist-geeks
• an Open Source NemID - design and develop an Open Source replacement for the proprietary, expensive NemID system developed and supported by DanID
  requires OO software engineering, Open Source principles
  ensures rigorous software engineering, cryptography foundations and rigorous crypto protocol design
  secret sauce huge impact if executed properly, technical Danes and the press are calling out for a solution, the government is under pressure about NemID's security and transparency
• Eiffel to Java VM - extend and complete the Java back-end of the premiere Eiffel compiler
  requires OO software engineering, basic compilers
  ensures compilers, Eiffel, Java VM bytecode
  secret sauce a first version of the back-end for the EiffelStudio compiler was developed at ETHZ for an MSc thesis, a full .Net back-end already exists
• textual BON in EiffelStudio - integrate the textual BON language and the capabilities of BONc into EiffelStudio
  requires OO software engineering, BON
  ensures compilers, Eiffel, formal refinement
  secret sauce a detailed draft refinement from BON to Eiffel already exists and the BONc and Beetlz tools show how this can be done for the Java programming language in Eclipse
• visualizing program reasoning - intuitive graphical representations of core concepts of program reasoning
  requires novel GUI design and development, logic, an interest in program reasoning
  ensures axiomatic reasoning about programs, semantics, logic, novel interactive UIs
  secret sauce apply Apple's and Tufte's design principles to logical artifacts-as-data
• the self-playing pinball machine - my Mac knows how to make combos!
  dedicated to Prof. Ted Baker on the occasion of his semi-retirement
  requires webcam, basic fast image processing, basics of AI and physics, Java, comfortable with electricity and a solder gun
  ensures realtime Java, expert systems, automatic risk analysis, moderate Newtonian physics, basic electronic engineering
  secret sauce realtime systems programming, encode pin-specific rulesets in an expert system with risk analysis, expert pinball player and hacker as supervisor, one of Ted's students, Hong-Hee Ko, did a variant on this project back in 1991 (report)
• experiments in verified electronic voting systems - advanced programming languages and environments for critical systems
  requires good knowledge of OO programming and logic
  ensures Eiffel or SPARK/Ada or PerfectDeveloper or Z or VDM++ or Event-B or VeriFast
  secret sauce rare, broad experience with advanced specification and programming languages and IDEs are available to write verified critical systems