goblint-jobs.md

goblint jobs

All topics can also be done as hiwi jobs. Recommendations for theses:

• ba = bachelor's thesis
• ma = master's thesis

ba, ma specification system for library functions

See description

ba configuration constraints

Implementation of a framework that allows specifying and checking configuration constraints. Preferably fail type checking for configuration errors in the code and be able to output warnings/fail depending on runtime configuration.

Examples:

• type errors for wrongly accessing config. options in the code (Ralf)
• intervals not allowed in calling context
• ana.int.intervals $\implies$ solver that does widening (e.g. warn for default solver effectWCon)

ba sound handling of floats

• arb. prec. ints
• machine error / anaylsis error
• zonotope

ba, ma better detection of runtime errors

• array index out of bounds
• segfaults: null-pointer access, ...?
• div by zero
• memory leaks
• undefined behavior
• wrong API usage (use automatons)

ba, ma better output/integration

BA David Krebs

• HTML report in OCaml instead of Java?
• backend: opa / OCaml web-lib / plain OCaml?
• frontend: opa / meteor / Angular / D3.js etc.?
• has to be efficient (split XML-files (over 4GB...)) -> load as much as possible on demand
• new features
  • splicing
  • visualization of traces
  • search in paths leading to end
  • semantic search
  • better navigation in code & cfg (program, functions, callsites)
  • source mapping between original and CIL with support for phases/transformations
  • editor integration?
• fixes
  • if one line leads to multiple lines of CIL with different domain values, those need to be joined (seems like currently just the first node is displayed instead of all (which would also be acceptable))

ppx / removing boilerplate

Use type-driven code generation to get rid of boilerplate (see ppx_deriving):

• show, yojson for output of domains values
• eq, ord, map, fold
• create own ppx drivers for own ideas (e.g. modules)

refactor query system with GADTs?

Query system uses a variant type for the question and a polymorphic variant type for the result.

Problem Every query has only a subset of valid return variants. This information is not encoded in the type, i.e., every question might return any result.

Idea Use GADTs. Problem Subtyping (r can't be covariant): code, issue.

Idea Get rid of need for subtyping (the result type seems partially redundant anyway):

type 'd r = Result of 'd | Top | Bot
let rec query : type d. d t -> d r = ...

ma implement relational value analyses

MA Isabel Max

• apron

ma analyzing product lines

MA Armin Gensler

E.g. automotive manufacturers have several variations of one car model, with many different compiler flags for each one.

Problem Goblint is analyzing cpp-preprocessed C code. For $n$ boolean flags one would need to analyze the code $2^n$ times to cover all combinations. For analyses that run several hours, this is not feasible.

Idea Analyze all flag combinations simultaneously and use BDDs to avoid having to keep $2^n$ times the state.

documentation

Improve the documentation, wiki etc.

backup Arbeiten am Goblint Werkzeug

Im Rahmen der Weiterentwicklung dieses Werkzeugs ergeben sich mehrere Themen, die sich eignen, Masterarbeit oder ggf. als SEP- / Bachelorarbeit bearbeitet zu werden:

• Erweitern das Analyseframeworks um rückwärtsgerichtete und mehrphasige Analysen. Entwickeln von Methoden um die Reihenfolge von Analysen zu optimieren.
• Entwicklung eines Speicherformats für Analyseergebnisse sowie implementierung einer Import/Export funktionalität basierend auf diesem Format.
• Implementation alternativer Fixpunktalgorithmen bzw. Analysetechniken um Stärken und Schwächen verschiedener Ansätze zu finden und gegenüber zu stellen.
• Konkrete Analysen: Im Laufe der Forschungen am Lehrstuhl Seidl entsteht immer wieder der Bedarf nach Implementierungen von konkreten Analysekonzepten - am Besten fragen Sie für solche Themen direkt bei Kalmer Apinis, Martin Schwarz, Vesal Vojdani oder Prof. Seidl nach!