User Tools

Site Tools


plt17:assignment_4

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
plt17:assignment_4 [2017/11/02 12:04]
hossein [Task 3]
plt17:assignment_4 [2017/11/21 19:32] (current)
hossein [Task 3]
Line 58: Line 58:
 ===== Task 3 ===== ===== Task 3 =====
  
-Verify ​the input program by checking the satisfiability of the generated Horn solvers by consulting ​an off-the-shelf Horn solver (e.g. [[https://​github.com/​Z3Prover/​z3|Z3]],​ [[https://​github.com/​uuverifiers/​eldarica|Eldarica]] ​ or [[https://​bitbucket.org/​spacer/​|Spacer]]). ​+When the user calls your program ​with the -v argument, it will verify the input file by checking the satisfiability of the generated Horn clauses. For satisfiability you can consult ​an off-the-shelf Horn solver (e.g. [[https://​github.com/​Z3Prover/​z3|Z3]],​ [[https://​github.com/​uuverifiers/​eldarica|Eldarica]] ​ or [[https://​bitbucket.org/​spacer/​|Spacer]]). ​
 Your program will either print ''​correct''​ for a program with no bug.  Your program will either print ''​correct''​ for a program with no bug. 
 Or, it will write ''​incorrect''​ for a program that has bug. Or, it will write ''​incorrect''​ for a program that has bug.
plt17/assignment_4.txt ยท Last modified: 2017/11/21 19:32 by hossein