-
Notifications
You must be signed in to change notification settings - Fork 41
Projekte
Liste möglicher zukünftiger (teilweise noch nicht ausgereifter) Projekte.
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.
Mache, dass wir ein Format, dass auch das Tool Goal kann ein/und auslesen können.
Implementiere das Master Projekt von Fabian Reiter
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]
Erweitere das auf Nested Word Automaten. Verwende es als Hilfsmittel um den Fortschritt der Trace Abstraction zu messen. (Könnte ein schlectes Maß sein).
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''
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.
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.
Wir haben eine neue Website, aber immer noch keine Anbindung an Rise4Fun
- Joogie kann Java nach Boogie übersetzen und wir würden das auch gern können (https://code.google.com/p/joogie/)
- Smack transformiert LLVM (C/C++) nach Boogie (https://github.com/smackers/smack/wiki)
- 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, ..? )
- Ein komplizierteres Projekt. Man muss für eine gegebene Microarchitektur (z.B. MSPxxxx) ein Environment-Format definieren, mit dem man Interrupts modellieren kann.
- 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?
- Home
- Ultimate Development
- Ultimate Build System
- Documentation
- Project Topics