# Questions tagged [software-verification]

Questions about methods and techniques to prove correctness of programs.

103 questions
Filter by
Sorted by
Tagged with
25 views

### From verification to program code

Suppose we have modeled the operational behavior as FSM, and properties as LTL or CTL, and we have used a model checking tool to confirm the fsm satisfies the LTL/CTl properties. What is the next ...
5k views

### Do theorem provers demonstrate their own correctness?

I am not very well-versed in the world of theorem proving, much less automated theorem proving, so please correct me if anything I say or assume in my question is wrong. Basically my question is: are ...
35 views

55 views

45 views

### How to Construct Kripke Structure States from Nested Functions

Say I have these defined functions: ...
65 views

### Understanding a Single Step in the Model Checking Algorithm

This answer explains roughly how to convert a nested boolean function into a Binary Decision Diagram (BDD). This question is about how to structure the states for the BDD. Now in this question I am ...
53 views

### What the State is, and Where it comes from, when Generating Reachability Graphs

For Timed Automata, I found Figure 1 below. For Coloured Petri Nets I found Figure 2. Both are for "Reachability Graph Construction". However, they don't describe where they got the states from (...
177 views

### How to use Hoare Logic to Prove this Assertion

Given this assertion in Hoare Logic: \begin{align} &\mathbf{\{p >= 0\}}\\ &s = 0 ; n = 1 ;\\ &\mathtt{while}\ (n <= p)\ \{\\ &\quad s = s + n ;\\ &\quad n = n + 1\\ &\}\\...
77 views

### How to apply Hoare Logic to this function

I would like to apply Hoare Logic to realistic, complex imperative programs that use while loops, if statements, functions, modules, etc. and have side effects (e.g. access the network). In order to ...
59 views

### How to apply Operational Semantics to this function

Say I have a function like this: ...
48 views

### Formal basis for “peephole reasoning” about code

The approaches I've seen to abstractly talking about the semantics of a programming language like Turing machines, various lambda calculi, and Hoare logic seem to be talking about the behavior of ...
3k views

### Finding weakest precondition

I have the following program x := y + 1; if (y > 0) then x := x + y else x := y + 100; x := x + y; I want to compute the weakest precondition for getting <...
67 views

### Learning to prove correctness of simple linked-list algorithms

I understand how to use linked lists, and build algorithm using them. But I don't understand how can we prove their correctness, even of simplest algorithm. I haven't even found a good tutorial ...
22 views

### Does there exist a conservative algorithm to determine if a certain property is satisfied at a certain part of a program?

... x = a / b; For the above code, for example, is there a way to determine whether b could be zero at the time of division, ...
275 views

### Proof Carrying LLVM?

I am intrigued by and understand the very basics of Proof Carrying Code (PCC) and I recognize that LLVM is a machine-independent intermediate language. LLVM is the intermediate form of many languages,...
325 views

### Expression of the weakest precondition of a while loop

I am interested in computing weakest preconditions (WP) of loops. If I refer to Wikipedia "Predicate Transformer semantics", the WP for e.g. total correction of a loop annotated with an invariant I ...