The program-verification tag has no wiki summary.
0
votes
1answer
22 views
applying CTL/LTL model-checking on some system
I apologies if my title is vague, I'm trying to apply CTL/LTL model-checking on some system written in java, however, I still don't understand how to reach a result using either of the approaches ...
9
votes
4answers
430 views
How do you check if two algorithms return the same result for any input?
How do you check if two algorithms (say, Merge sort and Naïve sort) return the same result for any input, when the set of all inputs is infinite?
Update: Thank you Ben for describing how this is ...
4
votes
3answers
144 views
Hoare triple for assignment P{x/E} x:=E {P}
I am trying to understand Hoare logic presented at Wikipedia,
Hoare logic at Wikipedia
Apparently, if I understand correctly, a Hoare triple $$\{P\}~ C ~\{Q\}$$ means
if P just before C, then Q ...
