Questions tagged [software-verification]
Questions about methods and techniques to prove correctness of programs.
120
questions
0
votes
3
answers
76
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
77
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 ...
- 161
0
votes
0
answers
18
views
What would be the logical requirements on a language, in order to do direct meta-programming in it?
I am motivated by the idea of generating “words” or “pairs” in a programming language or set of commands.
For example, consider any arbitrary REST API.
Beyond requesting the original URL endpoint, ...
- 23
1
vote
1
answer
60
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
1k
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
1
vote
0
answers
82
views
confusion with regard to constructive axiom
we say that a constructive axiom is an equality axiom $u = s$ :
whose left member $u$ is a pattern,
whose right member $s$ is any term whose variables are all appearing in $u$.
and yet we say of $...
- 33
0
votes
1
answer
54
views
Hoare Triple Derivation Example (Precondition False)
How can i derive this Hoare Tripel?
{false} x := x + 1; {x = 0}
I do not know which rule should i use on this.
I am confused on this wrong precondition.
- 3
1
vote
1
answer
58
views
Are there invariants in text processing problems?
I have read that when programming it is good to identify relations -- invariants -- that should hold true throughout the program, and it is good to insert assertions throughout the code to check that ...
- 393
0
votes
0
answers
40
views
Dependency analysis in a neural network
I was reading [1] about verifying neural networks. $n_{i,r}$ refers to the rth neuron in layer i and all neurons have the ReLU activation function. A neuron $n_{i,r}$ is said to be strictly active if ...
- 13
1
vote
1
answer
36
views
Linear encoding of a feed forward neural network
I was reading [1] about reachability analysis of a feed forward neural network (FFNN). The paper encodes a FFNN as a linear programming problem. Suppose $x^{(i)}$ is the vector output of the ith layer,...
- 13
1
vote
0
answers
40
views
What is known about the possibility of making a program to validate another program for correctness?
I'm having a question inspired by exercise 14 from section 1.2.1 of Donald Knuth's The Art of Computer Programming. It's phrased in the following way:
(R. W. Floyd) Prepare a computer program that ...
- 13
1
vote
1
answer
72
views
Logic foundation for formal verification
What types of logic should one study as foundation before diving into the area of software verification? What I can think of are:
Hoare Logic (for proving correctness of imperative programs)
Linear ...
- 111
1
vote
1
answer
54
views
How are pointers interpreted differently to variables in a control flow graph (CFG)?
I have been working with control flow graphs and believe I understand how they function when describing dependencies between variables. For example, given the operations:
...
- 113
0
votes
1
answer
81
views
What's so difficult about computer verifiable proofs?
What's so hard about creating a piece of software with as minimal as possible mathematical axioms, defining a formal language in which one can create new constructs based on the existing ones, and ...
- 119
1
vote
0
answers
41
views
Is assignment atomic in Promela?
Is assignment atomic is Promela? That is, can concurrent
x = value1;
and
x = value2;
produce anything different from value1 ...
user127009
3
votes
0
answers
55
views
Are automata useful in software verification?
I contrast the paradigm of SMT-based verification of software, such as in LiquidHaskell with the approach based on automata. To me it appears that automata are only used in the paradigm of model ...
- 2,240
4
votes
1
answer
115
views
Proving program termination in the $\lambda$-calculus
Turing's Checking a large routine:
Finally the checker has to verify that the process comes to an end.
Here again he should be assisted by the programmer giving a further
definite assertion to be ...
- 2,240
1
vote
0
answers
214
views
How to efficiently flatten a hierarchical state machine?
David Harel's StateCharts introduces hierarchical states and history mechanism, which are really powerful when modeling complex system behaviour. But when doing model based testing we need a "...
- 111
1
vote
0
answers
70
views
Why is most research in logic and verification conducted in Europe rather than the US?
This is the CSRankings output for logic and formal verification for the last 10 years, worldwide:
http://csrankings.org/#/index?log&world
For the International Conference on Computer Aided ...
- 21
3
votes
2
answers
800
views
A general picture of formal verification in software
I'm trying to piece together a general picture of the state of formal software verification, and I'm having a good bit of trouble. For context, I come from mostly a math background. I'm quite familiar ...
1
vote
0
answers
45
views
Can you verify a word's position in an enumeration faster than performing the enumeration?
Pt 1. Given as input the tuple: (word (from an r.e. language we fix), natural number)--does there exist a verifier, that runs faster than simply enumerating that language, that can accept if the word ...
user121977
2
votes
0
answers
33
views
Is Event Calculus applied for program verification?
Recently I've read wiki page about Robert Kowalski (Prolog author) and stumbled upon interesting concept of Event Calculus. The wiki article mentions only few applications of this logical language. I ...
- 131
39
votes
5
answers
6k
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 ...
- 503
1
vote
0
answers
29
views
Review of Formal Verification and How to Apply it to Greenfield Project [duplicate]
Last year I looked heavily into Formal Verification, such as automated theorem proving, model checking, type systems, symbolic evaluation, and many others. I probably spent a few weeks or maybe months ...
- 2,153
4
votes
2
answers
594
views
Why is the assignment rule the way it is in Hoare Logic?
Why is the assignment rule the way it is in Hoare Logic/Axiomatic Semantics?
I can't wrap my head around why the assignment rule is backwards from what I expected.
I understand Hoare logic is use to ...
- 2,960
3
votes
2
answers
1k
views
Imperfection in randomness in VLC shuffle playlist - why?
Whenever I play a playlist of music using VLC (possibly other software too), I notice that some songs never get played while others get played repeatedly (even for a playlist of just 8 songs).
I know ...
- 173
1
vote
1
answer
52
views
Alternatives to Unit Testing?
During a technical interview I was asked about ways to make sure code/software design is functional before deploying to any servers and the only thing I could think of was unit testing. My interviewer ...
- 35
4
votes
1
answer
65
views
Algorithm for computing $Pr[s \vDash C \bigcup^{\geq n} B]$ for probabilistic verification
I'm having some difficulty trying to come up with an algorithm for computing $Pr[s \vDash C ~\bigcup^{\geq n} B]$ given a finite Markov chain where $S$ is the set of states, $s \in S$, $B,C \subseteq ...
- 41
0
votes
1
answer
317
views
Safety property vs Liveness property
If i take a safety property $SP$ and a liveness property $LP$, is it true that the result of their intersection is a safety property (and not a liveness property) ? Why ?
Thanks
- 21
2
votes
1
answer
316
views
Definition of liveness property in model checking
A property $P$ is simply a set of sequences of states and a certain program is characterized by its set of sequences of states, let's call it $T$. A program is compliant to a specific property P if $T\...
- 21
2
votes
2
answers
2k
views
How to check if DFA is actually a correct model of the intended system?
Suppose I have modeled a deterministic finite automaton of my system. How can I check if the traces generated by this system, actually represent the model I had in mind?
For example, say I have DFA ...
- 121
2
votes
2
answers
63
views
(Generally) How to specify asynchronous action with side effects using logic equations
Say you have this function call sequence:
function all() {
fn1()
fn2()
fn3()
}
And say that fn2 was asynchronous and ...
- 2,153
0
votes
0
answers
119
views
Why is Combinatorial Sketching for Finite programs possible?
I was reading Combinatorial Sketching for Finite Programs and wanted to understand why synthesis of the sketching language was possible/feasible.
As far as I understand a partial program is ...
- 2,960
3
votes
0
answers
185
views
Relation between “formal verification”, “formal proof”, and “type systems” for software verification?
I have a vague understanding what formal verification is about, a vague understanding of what the cutting edge is of type theory for programming languages, and a better understanding of formal proofs.
...
- 3,622
5
votes
2
answers
648
views
Is there a way to convert a program into a Boolean formula?
Let's say I have a program P, in form of a binary code for x86 architecture.
I want to find a Boolean formula F (in form of CNF, or something like that), such ...
- 153
2
votes
2
answers
391
views
how to find the depth of a concurrency bug
How to find the depth of a concurrency bug
The below program runs on two separate threads and shares the variable x. Variables t1 and t2 are local to their threads. The program has a concurrency bug ...
- 121
1
vote
1
answer
62
views
Stablishing termination of the construction of infinite stream with ranking functions
I'm working with Turing's paradigm to prove termination of programs by annotating functions with ranking functions and I encounter the following example:
...
- 2,240
5
votes
1
answer
234
views
Best way to translate while loops to functions for software verification
I have a verification engine where while loops are translated into functional code, like this:
...
- 2,240
3
votes
1
answer
54
views
How a Symbolic Evaluator Generates Test Input for this Example
Say we have some complicated function that determines if a string matches an XSS attack string, and throws an error or does something else in that case.
...
- 2,153
1
vote
0
answers
21
views
Strategy / Technique for Proving Equivalence between Multiple Program Forms
Wondering how to prove different compiled forms of a program to be "effectively the same" or "equivalent".
For example, you can have a program represented as your normal nested function calls, or ...
- 2,153
0
votes
1
answer
194
views
How CompCert "proves" different things in its codebase
In order to understand examples of formal proofs, I am interested in how CompCert applies "proof" techniques. Specifically, I am wondering what a particular example is of something CompCert "proves" ...
- 2,153
10
votes
2
answers
3k
views
An example of something you can formally verify with proofs in Software Development
I have been working on understanding formal verification of software. Formal methods include things like modeling your software with Petri Nets, Automata, or State-Transition Graphs. Other techniques ...
- 2,153
2
votes
1
answer
417
views
How to define the Atomic Propositions in Model Checking
The atomic propositions in Symbolic Model Checking form the state in the state-transition graph (the model $\mathcal{M}$ in Model Checking). The other part of Model Checking is the specification, ...
- 2,153
1
vote
1
answer
85
views
How to Specify the Behavior of Automata for Verification
I am wondering what it takes to "verify" or "prove" that an automaton is correct. What the components are that are required. It seems that an automaton would be an easier thing to formally verify as ...
- 2,153
2
votes
0
answers
247
views
What you want to "prove" in algorithms
So it seems that you can get pretty far with just type definitions as a formal model of a system. The typed properties verify that the properties will have that type, typed function arguments verify ...
- 2,153
1
vote
0
answers
98
views
CTL satisfied by Kripke Structure
given a Kripke Structure I want to check if a CTL formula is satisfied or not.
the CTL is: $$ AG(c \vee AX\neg E((a\vee b)Uc)) $$
I have read that it is better to write to CTL in terms of $\wedge $ ...
- 268
1
vote
0
answers
57
views
How to Construct Kripke Structure States from Nested Functions
Say I have these defined functions:
...
- 2,153
1
vote
0
answers
74
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 ...
- 2,153
0
votes
1
answer
128
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 (...
- 2,153
3
votes
1
answer
140
views
High-level requirements for a Proof of "Saving to the Database"
This question is about a few sentence description of what a proof would look like (and technologies / logics involved) for a complex api call through many layers. Trying to get a sense of the ...
- 2,153