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 DTU, 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.

(June 2012) I am no longer available to directly supervise ITU BSc and MSc students. If you have an interest in a security-related thesis topic, please contact me anyway as we might be able to work out some kind of co-supervision arrangement.

(November 2012) I am now at DTU, so am considering thesis students there.

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.

  • DSL to 3D - compiling a voting domain specific language to mechanical hardware using 3D printing
    requires: programming languages (PL) and domain specific languages (DSL) basics, interest in 3D printing
    ensures: PL, DSL, and 3D printing expertise
    secret sauce: mechanical printing devices were all-the-rage for over a hundred years and all of the patents are now public
  • OpenConfigurator - software product lines meets Web 2.0
    requires: software engineering, Web 2.0 programming in .Net
    ensures: software product lines, advanced Web 2.0 programming in .Net, distributed REST-based architectures
    secret sauce: OpenConfigurator is a running, successful Open Source project started by another member of our team
  • Practical SPL4S - Software Project Lines (SPL) for software
    requires: software engineering (SE) and programming languages (PL)
    ensures: advanced SE and PL
    secret sauce: nearly all of the research in SPL focuses on models with no concrete relationship to code = opportunity!
  • The Frankenstein of Hip Gaming - Minecraft meets Dwarf Fortress
    requires: interest in text-based and 3D gaming, game engines, strange composition techniques
    ensures: expert in these two games and Frankenstein techniques for composition
    secret sauce: Sense-Compute-Control becomes Screenscraping-Compute-Render
  • SketchCode: The Next Generation - intentional programming meets JavaScript
    requires: JavaScript, Web 2.0 programming
    ensures: expertise in the history and technical foundations of object-based languages and novel IDEs
    secret sauce: a SketchCode prototype was developed by a member of our group
  • ESC/Objective-C - verification of Objective-C programs
    requires: Objective-C and theoretical understanding of logic and program reasoning
    ensures: object-based programming language semantics and reasoning, theorem proving
    secret sauce: object calculi meet verification condition generation
  • iRewrite - automated advice for writing and rewriting scientific and technical documents
    requires: an interest in writing, grammar, and linguistics
    ensures: in-depth knowledge writing analysis, grammar, and computational linguistics
    secret sauce: Strunk & White meets iSpell/aSpell
  • ESC/Go - Extended Static Checking for Google's Go Programming Language
    requires: firm foundation in logic and programming languages
    ensures: knowledge of the Go programming language, semantic static checking, programming language semantics, the SMT-LIB language and SMT solvers (consider the list of participants in the last SMT-LIB competition)
    secret sauce: the power of modern solvers attacking the complexities of modern languages
  • EMFText/DSL Experiments - experiment with Domain Specific Language (DSL) tools like EMFText or Visual Studio's DSL technologies to support modern specification languages like JML and BON
    requires: basic, firm knowledge of model-driven developments ideas and technologies
    ensures: core concepts, technologies, and algorithms of DSL design and development and the use, design, and meaning of modern specification languages
    secret sauce: push DSL language development tools to their limit
  • 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)
    A first version of this project was completed in Fall of 2012 by Anders Høst Kjærgaard. His project report is available on the reports page. That project would be extended by any new student that wishes to pursue this project.
  • 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
    A first version of this project was completed in Fall of 2012 by Benjamin Ma and Peter Ølsted. Their project report is available on the reports page. That project would be extended by any new student that wishes to pursue this project.
  • 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/RAISE - 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, Z, or RAISE
    secret sauce: Joe is good friends with the creators and main proponents of these four specification languages and all have new Open Source toolkits available (Rodin, Overture, CZT, and the RSLTC tool). 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, (c) extending the RAISE tools with new capabilities, or (d) improving integration of tools in Eclipse.
  • 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
    A first version of this project was completed in Fall of 2012 by Nikolaj Aaes and Nicolai Skovvart. Their project report is available on the reports page. That project would be extended by any new student that wishes to pursue this project.
  • 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
    A first version of this project was completed in Fall of 2012 by Søren Engel. His project report is available on the reports page. That project would be extended by any new student that wishes to pursue this project.
  • 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