COMP6210 Automated Software Verification 2022/2023 Coursework 2

Hello, dear friend, you can consult us at any time if you have any questions, add WeChat: daixieit

COMP6210 Automated Software Verification 2022/2023

Coursework 2

Due at 11:59 pm on 13 January 2023

Problem 1 of this assignment requires you to do (by hand) one step of verification of Hoare triples using Hoare logic. In Problem 2 of the assignment, you will anno- tate the given C code and verify it using Frama-C. The first part of this assignment is individual. You must work on it independently. For the second part, you should work in groups of 2 students.  Please, email me ([email protected]) if you cannot find a second person to work with.  Both students are expected to con- tribute equally. Exceptions to this should be reported. The names of all students in the group must be listed on the submission.  It is recommended that at least one student in the group has a Mac or a Linux PC.

Problem 1

In each of the following two questions, you need to show how a single Hoare Logic rule can be used to reduce the given Hoare triple to the next one towards the complete proof of the triple.

Question 1 [15 marks].

?

{y = 27} 北 := 北 + y; y := 北 + y {y − 北 = 27}

Question 2 [15 marks].

?

{z > 北} if (z > y) 北 := y + 1 else 北 := 北 + 1 {z ≥ 北}

Question 3 [15 marks]. What invariant can be used to prove the following Hoare triple:

{n = 1 ∧ 北 = 1} while (n < 100) do n = n + 1; 北 = −北 od {北 = −1}, where od denotes the end of the body of while loop.

Problem 2

In this problem, you will need to annotate the given code and verify the assert statement using Frama-C. The assert statement is already given in the code. This part of the coursework is a group assignment.

Question 1 [20 marks].

int main(){

int a = 0;

int s = 0;

while(a != 10){

a++;

int b = 0;

while(b != 10){

b++;

s++;

}

}

//@assert s == 100;

}

Question 2 [20 marks].

int f(int x){

return x+1;

}

void test(){

int s = 20;

int i = 0;

while (i<10){

s=f(s);

i++;

}

//@assert s==30;

}

Question 3 [15 marks].  Write a report (up to one page long total) to briefly describe the reasoning process you have gone through in order to arrive at the solutions to Question 1 and Question 2. Your report must include screenshots of the execution (with green marks).

Submission Instruction

For Problem 1, your submission should consist of typed Hoare triples in PDF. For Problem 2, you must include an annotated version of the files with C code and the report in PDF format. Late submissions will be penalised at 10% per working day.  Work submitted more than 5 days late will receive a mark of zero.  Your attention is drawn to the University regulations concerning Academic Integrity.


2023-01-10