My team works on programming tools that supply developers with actionable feedback during development. Feedback is actionable if it is relevant to the programmer's task, if the programmer can rely on its correctness, and if it arrives in a timely manner. The feedback we derive protects developers against introducing unsafe code, security vulnerabilities, and specification violations, yet it also informs development tools such as compiler optimizations and refactorings. To address this vision, we conduct basic research in programming languages, algorithms, and software verification that enables actionable feedback in a form that is useful in practice.


Incremental computing

We develop building blocks for incremental algorithms that achieve very high performance when reacting to a change in their input. Rather than repeating the entire computation over the changed input, an incremental algorithm only updates those parts of the previous result that are affected by the input change. This way, incremental algorithms provide asymptotical speedups in theory and we have observed multiple orders of magnitude speedups in practice.

Incremental algorithms are crucial for providing actionable feedback because the feedback needs to be updated after every code change the developer makes. Yet, existing algorithms, such as the Java type checker in Eclipse JDT, are one-off solutions that required years of engineering that cannot be reproduced. We develop building blocks for incremental computing and collect them in frameworks that execute regular algorithms incrementally.

Projects:

  • IncA: Incremental program analysis based on Datalog
  • PIE: Incremental software builds, supersedes pluto
  • CoCo: Co-contextual type checking and its application to incrementalization

Practical correctness proofs

Incorrect feedback gives developers a false sense of security that is not actually warranted by their code. We develop theory and tools that significantly simplifies correctness proofs. To this end, we decompose complex proof obligations into simpler ones and apply automated theorem provers. Our long-term goal is to enable analysis developers without specific training to prove correctness in little time. This will boost the confidence programmers place in analysis results.

Projects:

  • Sturdy: Compositional soundness for abstract interpreters
  • Veritas: Automated soundness verification for type checkers
  • SoundX: Type safe code generators

Domain-specific languages

Domain-specific languages abstract from technical details by providing tailored language features. Software developers who use domain-specific languages are more effective, because they reason about the code at the domain level and are freed from accidental complexity. For the same reason, domain-specific languages also make it easier for tools to derive actionable feedback. However, the effective development, application, and usage of domain-specific languages requires a large upfront investment into compilers, editors, and developer training. We develop techniques and toolboxes for significantly reducing the upfront costs of domain-specific languages.

Projects:

  • Spoofax: Language workbench for the creation of textual DSLs with IDE support
  • Evolute: Modernizing legacy code by semi-automatic introduction of DSLs
  • Monto editor: Decentralized architecture for reusable IDE language services

Former research projects: