Projekte

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)

• 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 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

Spaß mit Baumautomaten (Alex)

• ???

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?

Minimierung von Büchi Nested Word Automaten (Matthias)

Erweitere ''2005SIAMCOMP - Etessami,Wilke,Schuller - Fair Simulation Relations, Parity Games, and State Space Reduction for Buchi Automata'' auf Nested Word Automaten

Error Invariants (Christian and Matthias)

Motivation/Applications:

• Analyzing an error trace helps a programmer understand the reason for an error.
• Checking overapproximation in traces is relevant for an error.
• Trace generalization (for test generation - avoids "similar" tests).

Relevant Literature: 2013 VMCAI - Christ, Ermis, Schäf, Wies - Flow-Sensitive Fault Localization

Problem: Given a consistent (feasible) error trace in a program automaton, find statements that are irrelevant for feasibility of the trace.

General approach: Analyze the "tiger" trace. Construct some trace formula for the tiger trace. Check satisfiability of this trace formula. Use interpolants or an unsatisfiable core to find the relevant conjuncts/statements.

Naive approach: Construct the flow insensitive trace formula for the tiger trace; check satisfiability.

Two shortcomings of the naive approach:

1. works only if tiger trace is infeasible (cases where error trace is feasible iff tiger trace is infeasible?)
2. naive approach is not flow-sensitive

How to address these shortcomings:

1. Do not analyze solely the tiger trace but analyze tiger trace + precondition, namely the weakest precondition wp(false, error-trace). Because not(wp(false, error-trace)) together with the tiger trace is infeasible.
2. Use the flow-sensitive trace formula.

• Obstacle: Algorithm (from the paper) is only defined for traces that contain additional control flow information (if, endif, ...).
• Task: Develop a new algorithm for traces without control flow information (e.g., traces that orginate from program with gotos).