The tag has no wiki summary.

learn more… | top users | synonyms

3
votes
0answers
91 views

Taxonomy of formal methods of program verification [closed]

I'm trying to cobble together a survey of different techniques used in formal verification of software. I need a classification and brief description of various methods. It could be chronological, by ...
0
votes
1answer
58 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
500 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
241 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 ...