# Correct sorting with Frama-C

67 %
33 %
Information about Correct sorting with Frama-C
Technology

Published on July 3, 2009

Author: UlissesCosta

Source: slideshare.net

## Description

A view over bubble sort algorithm and his correctness proof in Frama-C.

Correct sorting with Frama-C Pedro Pereira Ulisses Costa Formal Methods in Software Engineering July 2, 2009 Pedro Pereira, Ulisses Costa Correct sorting with Frama-C

Algorithm implementation Implementation void bubbleSort ( int * vector , int tam ) { int j , i ; j = i = 0; for ( i =0; i < tam ; i ++) { for ( j =0; j < tam -i -1; j ++) { if ( vector [ j ] > vector [ j +1]) { swap (& vector [ j ] ,& vector [ j +1]) ; } } } } Pedro Pereira, Ulisses Costa Correct sorting with Frama-C

Contract pre-conditions tam > 0 valid range(vector , 0, tam − 1) post-conditions sorted(vector , 0, tam − 1) ∀a : 0 ≤ a < tam : (∃b : 0 ≤ b < tam : old(vector (b)) ≡ vector (a)) Pedro Pereira, Ulisses Costa Correct sorting with Frama-C

Annotations requires tam > 0; requires valid_range ( vector ,0 , tam -1) ; ensures ( forall integer a ; 0 <= a < tam == > ( exists integer b ; 0 <= b < tam == > at ( vector [ b ] , Old ) == at ( vector [ a ] , Here ) ) ) ; ensures Sorted { Here }( vector , 0 , tam -1) ; Pedro Pereira, Ulisses Costa Correct sorting with Frama-C

Inner-loop Example i = 0, [8, 5, 2, 6, 9, 3, 0, 4, 1] j = 0, [5, 8, 2, 6, 9, 3, 0, 4, 1] j = 1, [5, 2, 8, 6, 9, 3, 0, 4, 1] j = 2, [5, 2, 6, 8, 9, 3, 0, 4, 1] j = 3, [5, 2, 6, 8, 9, 3, 0, 4, 1] j = 4, [5, 2, 6, 8, 3, 9, 0, 4, 1] j = 5, [5, 2, 6, 8, 3, 0, 9, 4, 1] j = 6, [5, 2, 6, 8, 3, 0, 4, 9, 1] j = 7, [5, 2, 6, 8, 3, 0, 4, 1, 9] The j th + 1 element of sequence is greater or equal to the ﬁrst j + 1 elements of sequence. Pedro Pereira, Ulisses Costa Correct sorting with Frama-C

Inner-loop Example i = 0, [8, 5, 2, 6, 9, 3, 0, 4, 1] j = 0, [5, 8, 2, 6, 9, 3, 0, 4, 1] j = 1, [5, 2, 8, 6, 9, 3, 0, 4, 1] j = 2, [5, 2, 6, 8, 9, 3, 0, 4, 1] j = 3, [5, 2, 6, 8, 9, 3, 0, 4, 1] j = 4, [5, 2, 6, 8, 3, 9, 0, 4, 1] j = 5, [5, 2, 6, 8, 3, 0, 9, 4, 1] j = 6, [5, 2, 6, 8, 3, 0, 4, 9, 1] j = 7, [5, 2, 6, 8, 3, 0, 4, 1, 9] The j th + 1 element of sequence is greater or equal to the ﬁrst j + 1 elements of sequence. Pedro Pereira, Ulisses Costa Correct sorting with Frama-C

Inner-loop Example i = 0, [8, 5, 2, 6, 9, 3, 0, 4, 1] j = 0, [5, 8, 2, 6, 9, 3, 0, 4, 1] j = 1, [5, 2, 8, 6, 9, 3, 0, 4, 1] j = 2, [5, 2, 6, 8, 9, 3, 0, 4, 1] j = 3, [5, 2, 6, 8, 9, 3, 0, 4, 1] j = 4, [5, 2, 6, 8, 3, 9, 0, 4, 1] j = 5, [5, 2, 6, 8, 3, 0, 9, 4, 1] j = 6, [5, 2, 6, 8, 3, 0, 4, 9, 1] j = 7, [5, 2, 6, 8, 3, 0, 4, 1, 9] The j th + 1 element of sequence is greater or equal to the ﬁrst j + 1 elements of sequence. Pedro Pereira, Ulisses Costa Correct sorting with Frama-C

Inner-loop Example i = 0, [8, 5, 2, 6, 9, 3, 0, 4, 1] j = 0, [5, 8, 2, 6, 9, 3, 0, 4, 1] j = 1, [5, 2, 8, 6, 9, 3, 0, 4, 1] j = 2, [5, 2, 6, 8, 9, 3, 0, 4, 1] j = 3, [5, 2, 6, 8, 9, 3, 0, 4, 1] j = 4, [5, 2, 6, 8, 3, 9, 0, 4, 1] j = 5, [5, 2, 6, 8, 3, 0, 9, 4, 1] j = 6, [5, 2, 6, 8, 3, 0, 4, 9, 1] j = 7, [5, 2, 6, 8, 3, 0, 4, 1, 9] The j th + 1 element of sequence is greater or equal to the ﬁrst j + 1 elements of sequence. Pedro Pereira, Ulisses Costa Correct sorting with Frama-C

Inner-loop Example i = 0, [8, 5, 2, 6, 9, 3, 0, 4, 1] j = 0, [5, 8, 2, 6, 9, 3, 0, 4, 1] j = 1, [5, 2, 8, 6, 9, 3, 0, 4, 1] j = 2, [5, 2, 6, 8, 9, 3, 0, 4, 1] j = 3, [5, 2, 6, 8, 9, 3, 0, 4, 1] j = 4, [5, 2, 6, 8, 3, 9, 0, 4, 1] j = 5, [5, 2, 6, 8, 3, 0, 9, 4, 1] j = 6, [5, 2, 6, 8, 3, 0, 4, 9, 1] j = 7, [5, 2, 6, 8, 3, 0, 4, 1, 9] The j th + 1 element of sequence is greater or equal to the ﬁrst j + 1 elements of sequence. Pedro Pereira, Ulisses Costa Correct sorting with Frama-C

Inner-loop Example i = 0, [8, 5, 2, 6, 9, 3, 0, 4, 1] j = 0, [5, 8, 2, 6, 9, 3, 0, 4, 1] j = 1, [5, 2, 8, 6, 9, 3, 0, 4, 1] j = 2, [5, 2, 6, 8, 9, 3, 0, 4, 1] j = 3, [5, 2, 6, 8, 9, 3, 0, 4, 1] j = 4, [5, 2, 6, 8, 3, 9, 0, 4, 1] j = 5, [5, 2, 6, 8, 3, 0, 9, 4, 1] j = 6, [5, 2, 6, 8, 3, 0, 4, 9, 1] j = 7, [5, 2, 6, 8, 3, 0, 4, 1, 9] The j th + 1 element of sequence is greater or equal to the ﬁrst j + 1 elements of sequence. Pedro Pereira, Ulisses Costa Correct sorting with Frama-C

Inner-loop Example i = 0, [8, 5, 2, 6, 9, 3, 0, 4, 1] j = 0, [5, 8, 2, 6, 9, 3, 0, 4, 1] j = 1, [5, 2, 8, 6, 9, 3, 0, 4, 1] j = 2, [5, 2, 6, 8, 9, 3, 0, 4, 1] j = 3, [5, 2, 6, 8, 9, 3, 0, 4, 1] j = 4, [5, 2, 6, 8, 3, 9, 0, 4, 1] j = 5, [5, 2, 6, 8, 3, 0, 9, 4, 1] j = 6, [5, 2, 6, 8, 3, 0, 4, 9, 1] j = 7, [5, 2, 6, 8, 3, 0, 4, 1, 9] The j th + 1 element of sequence is greater or equal to the ﬁrst j + 1 elements of sequence. Pedro Pereira, Ulisses Costa Correct sorting with Frama-C

Inner-loop Example i = 0, [8, 5, 2, 6, 9, 3, 0, 4, 1] j = 0, [5, 8, 2, 6, 9, 3, 0, 4, 1] j = 1, [5, 2, 8, 6, 9, 3, 0, 4, 1] j = 2, [5, 2, 6, 8, 9, 3, 0, 4, 1] j = 3, [5, 2, 6, 8, 9, 3, 0, 4, 1] j = 4, [5, 2, 6, 8, 3, 9, 0, 4, 1] j = 5, [5, 2, 6, 8, 3, 0, 9, 4, 1] j = 6, [5, 2, 6, 8, 3, 0, 4, 9, 1] j = 7, [5, 2, 6, 8, 3, 0, 4, 1, 9] The j th + 1 element of sequence is greater or equal to the ﬁrst j + 1 elements of sequence. Pedro Pereira, Ulisses Costa Correct sorting with Frama-C

Inner-loop Example i = 0, [8, 5, 2, 6, 9, 3, 0, 4, 1] j = 0, [5, 8, 2, 6, 9, 3, 0, 4, 1] j = 1, [5, 2, 8, 6, 9, 3, 0, 4, 1] j = 2, [5, 2, 6, 8, 9, 3, 0, 4, 1] j = 3, [5, 2, 6, 8, 9, 3, 0, 4, 1] j = 4, [5, 2, 6, 8, 3, 9, 0, 4, 1] j = 5, [5, 2, 6, 8, 3, 0, 9, 4, 1] j = 6, [5, 2, 6, 8, 3, 0, 4, 9, 1] j = 7, [5, 2, 6, 8, 3, 0, 4, 1, 9] The j th + 1 element of sequence is greater or equal to the ﬁrst j + 1 elements of sequence. Pedro Pereira, Ulisses Costa Correct sorting with Frama-C

Inner-loop Example i = 0, [8, 5, 2, 6, 9, 3, 0, 4, 1] j = 0, [5, 8, 2, 6, 9, 3, 0, 4, 1] j = 1, [5, 2, 8, 6, 9, 3, 0, 4, 1] j = 2, [5, 2, 6, 8, 9, 3, 0, 4, 1] j = 3, [5, 2, 6, 8, 9, 3, 0, 4, 1] j = 4, [5, 2, 6, 8, 3, 9, 0, 4, 1] j = 5, [5, 2, 6, 8, 3, 0, 9, 4, 1] j = 6, [5, 2, 6, 8, 3, 0, 4, 9, 1] j = 7, [5, 2, 6, 8, 3, 0, 4, 1, 9] The j th + 1 element of sequence is greater or equal to the ﬁrst j + 1 elements of sequence. Pedro Pereira, Ulisses Costa Correct sorting with Frama-C

Inner-loop (cont.) Loop invariants 0 ≤ j < tam − i 0 < j < tam − i ⇒ (∀a : 0 ≤ a ≤ j : vector (a) ≤ vector (j + 1)) Loop variants tam − i − j − 1 Pedro Pereira, Ulisses Costa Correct sorting with Frama-C

Inner-loop invariants & variant loop invariant 0 <= j < tam - i ; loop invariant 0 < j < tam - i == > forall int a ; 0 <= a <= j == > vector [ a ] <= vector [ j +1]; loop variant tam -i -j -1; Pedro Pereira, Ulisses Costa Correct sorting with Frama-C

Outer-loop Example antes, [8, 5, 2, 6, 9, 3, 0, 4, 1] i = 0, [5, 2, 6, 8, 3, 0, 4, 1, 9] i = 1, [2, 5, 6, 3, 0, 4, 1, 8, 9] i = 2, [2, 5, 3, 0, 4, 1, 6, 8, 9] i = 3, [2, 3, 0, 4, 1, 5, 6, 8, 9] i = 4, [2, 0, 3, 1, 4, 5, 6, 8, 9] i = 5, [0, 2, 1, 3, 4, 5, 6, 8, 9] i = 6, [0, 1, 2, 3, 4, 5, 6, 8, 9] i = 7, [0, 1, 2, 3, 4, 5, 6, 8, 9] i = 8, [0, 1, 2, 3, 4, 5, 6, 8, 9] Last i + 1 elements of sequence are sorted Last i + 1 are all greater or equal to the other elements of the sequence. Pedro Pereira, Ulisses Costa Correct sorting with Frama-C

Outer-loop Example antes, [8, 5, 2, 6, 9, 3, 0, 4, 1] i = 0, [5, 2, 6, 8, 3, 0, 4, 1, 9] i = 1, [2, 5, 6, 3, 0, 4, 1, 8, 9] i = 2, [2, 5, 3, 0, 4, 1, 6, 8, 9] i = 3, [2, 3, 0, 4, 1, 5, 6, 8, 9] i = 4, [2, 0, 3, 1, 4, 5, 6, 8, 9] i = 5, [0, 2, 1, 3, 4, 5, 6, 8, 9] i = 6, [0, 1, 2, 3, 4, 5, 6, 8, 9] i = 7, [0, 1, 2, 3, 4, 5, 6, 8, 9] i = 8, [0, 1, 2, 3, 4, 5, 6, 8, 9] Last i + 1 elements of sequence are sorted Last i + 1 are all greater or equal to the other elements of the sequence. Pedro Pereira, Ulisses Costa Correct sorting with Frama-C

Outer-loop Example antes, [8, 5, 2, 6, 9, 3, 0, 4, 1] i = 0, [5, 2, 6, 8, 3, 0, 4, 1, 9] i = 1, [2, 5, 6, 3, 0, 4, 1, 8, 9] i = 2, [2, 5, 3, 0, 4, 1, 6, 8, 9] i = 3, [2, 3, 0, 4, 1, 5, 6, 8, 9] i = 4, [2, 0, 3, 1, 4, 5, 6, 8, 9] i = 5, [0, 2, 1, 3, 4, 5, 6, 8, 9] i = 6, [0, 1, 2, 3, 4, 5, 6, 8, 9] i = 7, [0, 1, 2, 3, 4, 5, 6, 8, 9] i = 8, [0, 1, 2, 3, 4, 5, 6, 8, 9] Last i + 1 elements of sequence are sorted Last i + 1 are all greater or equal to the other elements of the sequence. Pedro Pereira, Ulisses Costa Correct sorting with Frama-C

Outer-loop Example antes, [8, 5, 2, 6, 9, 3, 0, 4, 1] i = 0, [5, 2, 6, 8, 3, 0, 4, 1, 9] i = 1, [2, 5, 6, 3, 0, 4, 1, 8, 9] i = 2, [2, 5, 3, 0, 4, 1, 6, 8, 9] i = 3, [2, 3, 0, 4, 1, 5, 6, 8, 9] i = 4, [2, 0, 3, 1, 4, 5, 6, 8, 9] i = 5, [0, 2, 1, 3, 4, 5, 6, 8, 9] i = 6, [0, 1, 2, 3, 4, 5, 6, 8, 9] i = 7, [0, 1, 2, 3, 4, 5, 6, 8, 9] i = 8, [0, 1, 2, 3, 4, 5, 6, 8, 9] Last i + 1 elements of sequence are sorted Last i + 1 are all greater or equal to the other elements of the sequence. Pedro Pereira, Ulisses Costa Correct sorting with Frama-C

Outer-loop Example antes, [8, 5, 2, 6, 9, 3, 0, 4, 1] i = 0, [5, 2, 6, 8, 3, 0, 4, 1, 9] i = 1, [2, 5, 6, 3, 0, 4, 1, 8, 9] i = 2, [2, 5, 3, 0, 4, 1, 6, 8, 9] i = 3, [2, 3, 0, 4, 1, 5, 6, 8, 9] i = 4, [2, 0, 3, 1, 4, 5, 6, 8, 9] i = 5, [0, 2, 1, 3, 4, 5, 6, 8, 9] i = 6, [0, 1, 2, 3, 4, 5, 6, 8, 9] i = 7, [0, 1, 2, 3, 4, 5, 6, 8, 9] i = 8, [0, 1, 2, 3, 4, 5, 6, 8, 9] Last i + 1 elements of sequence are sorted Last i + 1 are all greater or equal to the other elements of the sequence. Pedro Pereira, Ulisses Costa Correct sorting with Frama-C

Outer-loop Example antes, [8, 5, 2, 6, 9, 3, 0, 4, 1] i = 0, [5, 2, 6, 8, 3, 0, 4, 1, 9] i = 1, [2, 5, 6, 3, 0, 4, 1, 8, 9] i = 2, [2, 5, 3, 0, 4, 1, 6, 8, 9] i = 3, [2, 3, 0, 4, 1, 5, 6, 8, 9] i = 4, [2, 0, 3, 1, 4, 5, 6, 8, 9] i = 5, [0, 2, 1, 3, 4, 5, 6, 8, 9] i = 6, [0, 1, 2, 3, 4, 5, 6, 8, 9] i = 7, [0, 1, 2, 3, 4, 5, 6, 8, 9] i = 8, [0, 1, 2, 3, 4, 5, 6, 8, 9] Last i + 1 elements of sequence are sorted Last i + 1 are all greater or equal to the other elements of the sequence. Pedro Pereira, Ulisses Costa Correct sorting with Frama-C

Outer-loop Example antes, [8, 5, 2, 6, 9, 3, 0, 4, 1] i = 0, [5, 2, 6, 8, 3, 0, 4, 1, 9] i = 1, [2, 5, 6, 3, 0, 4, 1, 8, 9] i = 2, [2, 5, 3, 0, 4, 1, 6, 8, 9] i = 3, [2, 3, 0, 4, 1, 5, 6, 8, 9] i = 4, [2, 0, 3, 1, 4, 5, 6, 8, 9] i = 5, [0, 2, 1, 3, 4, 5, 6, 8, 9] i = 6, [0, 1, 2, 3, 4, 5, 6, 8, 9] i = 7, [0, 1, 2, 3, 4, 5, 6, 8, 9] i = 8, [0, 1, 2, 3, 4, 5, 6, 8, 9] Last i + 1 elements of sequence are sorted Last i + 1 are all greater or equal to the other elements of the sequence. Pedro Pereira, Ulisses Costa Correct sorting with Frama-C

Outer-loop Example antes, [8, 5, 2, 6, 9, 3, 0, 4, 1] i = 0, [5, 2, 6, 8, 3, 0, 4, 1, 9] i = 1, [2, 5, 6, 3, 0, 4, 1, 8, 9] i = 2, [2, 5, 3, 0, 4, 1, 6, 8, 9] i = 3, [2, 3, 0, 4, 1, 5, 6, 8, 9] i = 4, [2, 0, 3, 1, 4, 5, 6, 8, 9] i = 5, [0, 2, 1, 3, 4, 5, 6, 8, 9] i = 6, [0, 1, 2, 3, 4, 5, 6, 8, 9] i = 7, [0, 1, 2, 3, 4, 5, 6, 8, 9] i = 8, [0, 1, 2, 3, 4, 5, 6, 8, 9] Last i + 1 elements of sequence are sorted Last i + 1 are all greater or equal to the other elements of the sequence. Pedro Pereira, Ulisses Costa Correct sorting with Frama-C

Outer-loop Example antes, [8, 5, 2, 6, 9, 3, 0, 4, 1] i = 0, [5, 2, 6, 8, 3, 0, 4, 1, 9] i = 1, [2, 5, 6, 3, 0, 4, 1, 8, 9] i = 2, [2, 5, 3, 0, 4, 1, 6, 8, 9] i = 3, [2, 3, 0, 4, 1, 5, 6, 8, 9] i = 4, [2, 0, 3, 1, 4, 5, 6, 8, 9] i = 5, [0, 2, 1, 3, 4, 5, 6, 8, 9] i = 6, [0, 1, 2, 3, 4, 5, 6, 8, 9] i = 7, [0, 1, 2, 3, 4, 5, 6, 8, 9] i = 8, [0, 1, 2, 3, 4, 5, 6, 8, 9] Last i + 1 elements of sequence are sorted Last i + 1 are all greater or equal to the other elements of the sequence. Pedro Pereira, Ulisses Costa Correct sorting with Frama-C

Outer-loop Example antes, [8, 5, 2, 6, 9, 3, 0, 4, 1] i = 0, [5, 2, 6, 8, 3, 0, 4, 1, 9] i = 1, [2, 5, 6, 3, 0, 4, 1, 8, 9] i = 2, [2, 5, 3, 0, 4, 1, 6, 8, 9] i = 3, [2, 3, 0, 4, 1, 5, 6, 8, 9] i = 4, [2, 0, 3, 1, 4, 5, 6, 8, 9] i = 5, [0, 2, 1, 3, 4, 5, 6, 8, 9] i = 6, [0, 1, 2, 3, 4, 5, 6, 8, 9] i = 7, [0, 1, 2, 3, 4, 5, 6, 8, 9] i = 8, [0, 1, 2, 3, 4, 5, 6, 8, 9] Last i + 1 elements of sequence are sorted Last i + 1 are all greater or equal to the other elements of the sequence. Pedro Pereira, Ulisses Costa Correct sorting with Frama-C

Outer-loop Example antes, [8, 5, 2, 6, 9, 3, 0, 4, 1] i = 0, [5, 2, 6, 8, 3, 0, 4, 1, 9] i = 1, [2, 5, 6, 3, 0, 4, 1, 8, 9] i = 2, [2, 5, 3, 0, 4, 1, 6, 8, 9] i = 3, [2, 3, 0, 4, 1, 5, 6, 8, 9] i = 4, [2, 0, 3, 1, 4, 5, 6, 8, 9] i = 5, [0, 2, 1, 3, 4, 5, 6, 8, 9] i = 6, [0, 1, 2, 3, 4, 5, 6, 8, 9] i = 7, [0, 1, 2, 3, 4, 5, 6, 8, 9] i = 8, [0, 1, 2, 3, 4, 5, 6, 8, 9] Last i + 1 elements of sequence are sorted Last i + 1 are all greater or equal to the other elements of the sequence. Pedro Pereira, Ulisses Costa Correct sorting with Frama-C

Outer-loop (cont.) Loop invariants 0 ≤ i < tam sorted(vector , tam − i − 1, tam − 1) 0 < i < tam ⇒ (∀{a,b} : 0 ≤ b ≤ tam − i − 1 ≤ a < tam : vector (a) ≥ vector (b)) Loop variants tam − i Pedro Pereira, Ulisses Costa Correct sorting with Frama-C

Outer-loop invariants & variant loop invariant 0 <= i < tam ; loop invariant Sorted { Here }( vector , tam -i -1 , tam -1) ; loop invariant 0 < i < tam == > forall int a , b ; 0 <= b <= tam -i -1 <= a < tam == > vector [ a ] >= vector [ b ]; loop variant tam - i ; Pedro Pereira, Ulisses Costa Correct sorting with Frama-C

Conclusions Fast and powerful Possible to prove bubble-sort’s correctness with just 16 annotations Constantly updated Although extensive, the documentation lacks detail x Complex programs may require advanced knowledge in Logic x Pedro Pereira, Ulisses Costa Correct sorting with Frama-C

Questions ? Pedro Pereira, Ulisses Costa Correct sorting with Frama-C

Resources - rest of the code /* @ predicate Sorted { L }( int a [] , integer l , integer h ) = @ forall integer i ; l <= i < h @ == > at ( a [ i ] , L ) <= at ( a [ i +1] , L ) ; @ */ /* @ requires valid ( i ) && valid ( j ) ; @ // BUG 0000080: Assertion failed in jc_int erp_misc . ml @ // assigns *i , * j ; @ ensures at (* i , Old ) @ == at (* j , Here ) && at (* j , Old ) @ == at (* i , Here ) ; @ */ void swap ( int *i , int * j ) { int tmp = * i ; *i = *j; * j = tmp ; } Pedro Pereira, Ulisses Costa Correct sorting with Frama-C

Resources - images Pedro Pereira, Ulisses Costa Correct sorting with Frama-C

Resources - images (cont.) Pedro Pereira, Ulisses Costa Correct sorting with Frama-C

## Add a comment

 User name: Comment:

## Related presentations

#### Neuquén y el Gobierno Abierto

October 30, 2014

Presentación que realice en el Evento Nacional de Gobierno Abierto, realizado los ...

#### Decision CAMP 2014 - Erik Marutian - Using rules-b...

October 16, 2014

In this presentation we will describe our experience developing with a highly dyna...

#### Schema.org: What It Means For You and Your Library

November 7, 2014

Presentation to the LITA Forum 7th November 2014 Albuquerque, NM

#### WearableTech: Una transformación social de los p...

November 3, 2014

Un recorrido por los cambios que nos generará el wearabletech en el futuro

#### O Impacto de Wearable Computers na vida das pessoa...

November 5, 2014

Um paralelo entre as novidades & mercado em Wearable Computing e Tecnologias Assis...

#### All you need to know about the Microsoft Band

November 6, 2014

Microsoft finally joins the smartwatch and fitness tracker game by introducing the...

## Related pages

### Correct sorting with Frama-C - PdfSR.com

Correct sorting with Frama-CPedro PereiraUlisses CostaFormal Methods in Software EngineeringJuly 2, 2009Pedro Pereira, Ulisses CostaCorrect sorting with ...
Read more

### Correct sorting with Frama-C and some thoughts on Formal ...

A couple of years ago, during my masters on Formal Methods I have been working with automatic provers and I also used Frama-C, this is a tool ...
Read more

### Sorting | LinkedIn

Food Sorting is one of the interesting field for many big Multinationals these days. ... Correct sorting with Frama-C. 8,207 Views. StewartHutchison.
Read more

### frama-c | Ulisses Costa Blog

Posts about frama-c written by Ulisses Araújo Costa. Ulisses Costa Blog. Home About; Correct sorting with Frama-C and some thoughts on Formal Methdos 12 ...
Read more

### Publications - A Source code analysis Toolbox for software ...

Frama-C is a software analysis platform that enables the design, ... Publications. An Introduction to ... An Explicit Formula for Sorting and its ...
Read more

### Frama | LinkedIn

View 1409 Frama posts, presentations, experts, and more. Get the professional knowledge you need on LinkedIn. LinkedIn Home What is LinkedIn? Join Today
Read more