Questions about methods and techniques to prove correctness of programs.
3
votes
2answers
38 views
Temporal logic for interface invariants
I am looking for some sort of temporal logic for expressing invariants in interfaces. Since interfaces do not specify data representation, the invariants must rely solely on the publicly available ...
3
votes
1answer
67 views
Evaluation of reverse Polish notation
We only consider the reverse Polish notation as an arithmetic expression.
Formally, RNP is a sequence consisted of numbers and arithmetic operators: $+,-,*,/$, and its syntax is:
...
5
votes
2answers
150 views
Introduction into first order logic verification
I am trying to teach myself different approaches to software verification. I have read some articles. As far as I learned, propositional logic with temporal generally uses model checking with SAT ...
9
votes
4answers
429 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 ...
9
votes
1answer
193 views
How to deal with arrays during Hoare-style correctness proofs
In the discussion around this question, Gilles mentions correctly that any correctness proof of an algorithm that uses arrays has to prove that there are no out-of-bounds array accesses; depending on ...
11
votes
6answers
400 views
Algorithm to solve Turing's “Halting problem”
"Alan Turing proved in 1936 that a general algorithm to solve the
halting problem for all possible program-input pairs cannot exist"
Can I find a general algorithm to solve the halting problem ...
