KindSoftware: Project Proposals

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