Transcript Distances and previous arrays have to be initialized Vector 1

Jonathan Kuhn
Robin Mange
EPFL-SSC
 Acquire practical skills in software verification
 Statement checking through implementation
 Performance evaluation
 Discussion
 Computes shortest-paths in directed graphs
 No negative weight edges
 Widely used in networking
in
routing protocols (e.g. OSPF)
Class Node {}
Class Path {}
Class Vector{}
Class Integer{}
Class Dijkstra{}
Simulated classes for
Vector and Integer
Objects
Init
Set distances to -1 and 0 for the start node. Set empty arrays for previous (node)
Distances and previous arrays have to be initialized
Fill up Vector 1
Add to the vector 1 all the node except the starting one
Vector 1 needs to be initialized
Main loop of the algorithm
While vector 1 is not empty, take the node corresponding to the smallest
distance. Remove it from vector 1, and recompute all edges to update minimal
distances
Specifications of above need to be maintained.
 Unfortunately We still have a method that is not verified.
We already can say that:
 The execution time of a verification process of our entire program (~200
lines) is about 20min…
 The number of annotation lines is about 80 for 200 lines of code.
 VC generation algorithms can be exponential in code size
 Can lead to long verification times (even for small programs)
 Important to write modularized code
 ESC/Java is known to be faster… but has more drawbacks than Jahob
 E.g. no infinite loop check, arithmetic overflow, unsound, …
 Problems encountered

Jahob doesn’t support libraries: need to simulate them

Int and objects aren’t treated the same way in decision procedures

Strange behavior with invariants in rare cases
 Jahob was mostly tested on small data structures (linked lists, …)
 Can be enhanced and extended beyond current state
 Very promising!

To do:
To test several benchmarks to test the correctness of the
verification process.
 If time allows:
Use ESC/Java to compare performances with Jahob
Translating annotations would be straightforward .