Skip to content

Projekte

Jump to bottom
schillic edited this page Feb 5, 2016 · 9 revisions

Liste möglicher zukünftiger (teilweise noch nicht ausgereifter) Projekte.

Softwareverifikation mit Nutzerinteraktion (Matthias)

Scheitert die Verifikation soll der Benutzer Rückmeldung bekommen was für das Tool schwierig war sodass der Benutzer mit Annotationen (z.B. Schleifeninvarianten) nachhelfen kann. Das Projekt wurde in Ultimate Besprechung am 2.5.2014 lange und emotional disskutiert. Ich glaube wir gehen es vorerst lieber nicht an.

Vergleich mit anderen Automatenbibliotheken (Matthias)

Mache, dass wir ein Format, dass auch das Tool Goal kann ein/und auslesen können.

Ramsey based Büchi complementation for Nested Word Automata (Matthias)

Implementiere das Master Projekt von Fabian Reiter

Implementiere support für Bitvektoren (Matthias)

Code Block soll mehrere TransFormulas bekommen, die on-demand erzeugt werden. Eine auch mit Bitvektoren. Verwende entweder SMT Bitvektoren oder explizites Bit Blasting (Informiere dich vorher über Frankenbit)

Large Block Encoding für LTL und Concurrency (Matthias)

Erweitere das LBE so, dass es mit LTL und Nebenläufigen Programmen noch Sound ist.

Integral Hull (Matthias)

Berechne Integral Hull für Polyeder welche Transitionsrelationen beschreiben. Bringt und Vollständigkeit bei Synthese von Rankingfunktionen für Integer [http://openaccess.city.ac.uk/1702/ Integer polyhedra for program analysis]

Schleifenkomplexität von Automaten (Matthias)

Erweitere das auf Nested Word Automaten. Verwende es als Hilfsmittel um den Fortschritt der Trace Abstraction zu messen. (Könnte ein schlectes Maß sein).

Alias Analyse für unsere Heap Repräsentation (Matthias)

Nimm einfache Analyse um herauszufinden welche Speicherbereiche garantiert separiert sind. Jeder diese Speicherbereiche bekommt sein eigenes Heap Array. Angeblich beschreibt folgendes Papier solch eine Idee. ''Ernie Cohen, Michal Moskal, Stephan Tobies, Wolfram Schulte: A Precise Yet Efficient Memory Model For C''

Abstract Interpretation Domains (Daniel, Marius)

Mittlerweile gibt es das Abstract Interpretation Framework, aber es könnte spannend sein, mehr Domains zu implementieren (z.B. Polytop, Points-To, Equality, ...)

Heuristics (Daniel, Martin W., et. al)

Die verschiedenen Modelchecker bei uns könnten unter Umständen an verschiedenen Stellen von Heuristiken profitieren.

  • Fehlerpfade: Im Moment verwenden sowohl CodeCheck als auch Automizer einfach den kürzesten Fehlerpfad. Andere Pfade (z.B. max. Coverage, mit AI "vorgefilterte" Pfade, Dynamic Slice, Random) könnten bessere Ergebnisse erzielen.
  • Unsat Cores: Verschiedene Unsat Cores ergeben verschiedene Interpolanten. Vielleicht kann man geeignete Heuristiken finden, um den "besten" Unsat Core auszuwählen.

k-korrektness und IRS (Daniel)

LTL Modelchecking von Programmen kann mit dem IRS-Ansatz zur Verifikation von Systemanforderungen verwendet werden. Dazu muss aber die Systemrepräsentation zum Programcode passen (Zustände im System sollten Programmzuständen entsprechen). Typischerweise entspricht ein Systemzustand aber vielen Programzuständen. Ein genaues Mapping kann automatisch gefunden werden, wenn es existiert. Wenn es nicht existiert, kann man ein ungenaues Mapping finden, und die Ungenauigkeit quantifizieren. Beide Ansätze (genaues Mapping finden, wenn es nicht existiert genauestes ungenaues finden) sollen implementiert werden.

Anbindung an Rise4Fun (Daniel)

Wir haben eine neue Website, aber immer noch keine Anbindung an Rise4Fun

Andere Toolchains+Memory Modelle für x to Boogie einbinden (Daniel, Alex)

Slicing für Boogie oder RCFGs (Daniel, Alex)

  • Slicing könnte unsere Performance erhöhen. Es wäre nett, das mal auszuprobieren. Backward Slicing sollte relativ einfach zu implementieren sein.
  • Man könnte auch ein Input-Preprocessing mit Slicing Support ausprobieren; es ist aber unklar, was es da gibt (CIL, ..? )

Interrupts unterstützen (Daniel, Sergio)

  • Ein komplizierteres Projekt. Man muss für eine gegebene Microarchitektur (z.B. MSPxxxx) ein Environment-Format definieren, mit dem man Interrupts modellieren kann.

Spaß mit AFAs (Alex)

  • Paralleles Program in einen AFA-Programautomaten übersetzen

Frontends verbessern (Alex, Daniel)

  • CLI Interface sollte Java Options benutzen und nicht so schwierig zu erweitern sein (z.B. Witness Checking) -- nett wäre auch, wenn man Optionen auf der Commandline setzten könnte.
  • CDT Interface ist seit der Rückübersetzungsveränderung nicht mehr so richtig angepasst worden. Da wäre (a) Eclipse Update nett, (b), Maintainence notwendig (erstmal so, das alles wieder läuft)

C to Boogie Übersetzung (Alex)

  • includes richtig machen
  • Checken, wie CDT das genau handhabt
  • für Standardheader eigene Dateien mit ACSL-Spezifikation erstellen?
  • pthread Unterstützung
  • C to Boogie Übersetzung: ACSL Unterstützung verbessern
  • Möglichst systematisch den ACSL-Standard durcharbeiten und in unserer Übersetzung umsetzen. Was machen wir mit Pointer dereferences?
Clone this wiki locally