Questions tagged [software-verification]
Questions about methods and techniques to prove correctness of programs.
129 questions
0
votes
0
answers
26
views
IC3/PDR: Why is $\neg s$ included in the relative induction query?
I am currently trying to understand the IC3/PDR algorithm. My intuitive understanding is that in each iteration, IC3 tries to find a counterexample $c$ (which is a single, concrete state) such that
$c ...
2
votes
2
answers
103
views
Equivalence checking: product program vs bisimulation
Consider the problem of equivalence checking two terminating sequential programs $P$ and $P'$ with the same input signatures and return statements. Two programs are equivalent if for all inputs ($args$...
- 23
1
vote
1
answer
87
views
Software that finds/proves runtime complexity of given code?
Is there software that can prove the runtime complexity of given code?
- 224
0
votes
0
answers
54
views
SLAM (model checking) at microsoft: successors?
The SLAM project at Microsoft (as detailed in this slide) was highly regarded for detecting bugs in Windows device drivers. Some of its key strengths include discovering real bugs, scalability (...
0
votes
0
answers
57
views
Proving properties of algorithims in computer science vs mathematics
In a course on logic and model theory I took, there were many methods of proving properties of loops discussed. In particular, we did this thing where we considered a simple language called "...
1
vote
0
answers
73
views
Version of SSSP
Let $G=(V,E)$ a directed graph s.t $|V|=n$. Let $w:E \to \mathbb{R}$ a weight function.
Describe an algorithm which finds the minimal-weighted walk of length $\leq n$ from $s \in V$ to all other nodes....
- 189
0
votes
1
answer
65
views
Linear Time properties classification
I know LT Properties can be classified with classes Invariants, Safety Properties, Liveness Properties as in https://en.wikipedia.org/wiki/Linear_time_property. My question is, does this cover all ...
- 92
5
votes
4
answers
2k
views
What's role of software verification in modern software engineering
There are standard courses in computer science faculties that teach software verification, yet modern software products (Operating Systems especially) require periodic updates and bugs are constantly ...
- 394
5
votes
1
answer
187
views
Closures break induction in correctness proof of interpreter
I'm trying to prove the correctness of an interpreter for a simple extension of untyped lambda-calculus with De Bruijn indices. The interpreter is bounded, i.e. in order to ensure its finiteness it ...
- 297
0
votes
4
answers
520
views
Find median in a sorted matrix
Suppose we are given a $n\times n$ matrix that is sorted row-wise and column-wise. We want to find the median in $\mathcal{O}(n\log{n})$.
This is my approach:
We know median is such element that is ...
- 187
0
votes
1
answer
150
views
Formally Verify if a Sequence of Regex-Based Modifications is Idempotent
I'm performing a sequence of text formatting using regex in Python.
I'm curious to know if it's possible to formally verify whether a single (or a sequence of) regex modification(s) is idempotent, ...
- 113
0
votes
3
answers
199
views
Is there a 2SAT encoding for a NAND gate
I am trying to encode some circuit checking algorithms, but encountered difficulty creating a 2SAT representation for a NAND circuit. Is there a proof that this is not possible?
0
votes
0
answers
513
views
Real-life applications of pure Mealy machines
I'm currently studying formal methods in software engineering related to state machines, specifically Mealy machines. This made me wonder how relevant Mealy machines really are for practical ...
- 181
1
vote
1
answer
75
views
0<i => 0 < i + j proof?
If we have the natural numbers defined as:
Plus the following:
$pred \space \_\_<\_\_ \space: Nat \times Nat$
$\forall i,j:Nat$
$0<suc(j)$
$\neg(i<0)$
$suc(i) < suc(j) \...
- 33
0
votes
1
answer
5k
views
MergeSort's merge function loop invariant
I am reading a proof of correctness for the MergeSort Algorithm. This is the code for the MergeSort and the Merge function:
The correctness of the MergeSort function is easy to prove since the two <...
- 108