Search Results
| Search type | Search syntax |
|---|---|
| Tags | [tag] |
| Exact | "words here" |
| Author |
user:1234 user:me (yours) |
| Score |
score:3 (3+) score:0 (none) |
| Answers |
answers:3 (3+) answers:0 (none) isaccepted:yes hasaccepted:no inquestion:1234 |
| Views | views:250 |
| Code | code:"if (foo != bar)" |
| Sections |
title:apples body:"apples oranges" |
| URL | url:"*.example.com" |
| Saves | in:saves |
| Status |
closed:yes duplicate:no migrated:no wiki:no |
| Types |
is:question is:answer |
| Exclude |
-[tag] -apples |
| For more details on advanced search visit our help page | |
Results tagged with software-verification
Search options answers only
not deleted
user 39
Questions about methods and techniques to prove correctness of programs.
5
votes
Accepted
Finding a good loop invariant
You have an intended postcondition for a loop, and you're looking for an interesting invariant. In this scenario, try taking the intended postcondition, and replacing the total number of iterations (h …
10
votes
Accepted
Data Flow Analysis with exceptions
Ignoring exceptions is unsound. Example:
let g = {
raise E;
}
let f = {
x := interesting_stuff();
g();
x := 0;
}
When analyzing f, you need to take into account the fact that g …
4
votes
Accepted
Proving program termination in the $\lambda$-calculus
This may take the form of a quantity which is asserted to decrease continually and vanish when the machine stops.
Lambda calculus evaluation is a sequence of beta reduction steps. So for the lambda …
20
votes
Program Correctness, The specification
D.W.'s answer is great, but I'd like to expand on one point. A specification is not just a reference against which the code is verified. One of the reasons to have a formal specification is to validat …
7
votes
Accepted
A general picture of formal verification in software
A formally proven program is a formally proven program regardless of which language it's in. Just because a program is written in Coq and perhaps extracted to OCaml or Haskell, rather than written in …
2
votes
What is a local inference system?
$\mathsf{Steps}(\Pi)$ is defined just above, in the paragraph below Definition 4.1. It's the set of node labels in the proof, i.e. the set of propositions that are proved as lemmas in that proof.
Thu …
9
votes
Accepted
How to deal with arrays during Hoare-style correctness proofs
Your axiom is not really an axiom, it's missing hypotheses. Simple presentations of Hoare logic manipulate formulas of the form $\{P\} C \{P'\}$ where $P$ and $P'$ are logical formulas and $C$ is a co …