Questions tagged [software-verification]

Questions about methods and techniques to prove correctness of programs.

Filter by
Sorted by
Tagged with
1 vote
1 answer
57 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 ...
user avatar
0 votes
0 answers
33 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 ...
user avatar
  • 13
1 vote
1 answer
22 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,...
user avatar
  • 13
1 vote
0 answers
23 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 ...
user avatar
0 votes
1 answer
41 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 ...
user avatar
  • 101
1 vote
1 answer
35 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: ...
user avatar
0 votes
1 answer
70 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 ...
user avatar
1 vote
0 answers
25 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 ...
user avatar
3 votes
0 answers
34 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 ...
user avatar
  • 2,196
4 votes
1 answer
93 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 ...
user avatar
  • 2,196
1 vote
0 answers
76 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 "...
user avatar
  • 111
1 vote
0 answers
57 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 ...
user avatar
2 votes
2 answers
341 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 ...
user avatar
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 ...
user avatar
2 votes
0 answers
32 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 ...
user avatar
  • 131
38 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 ...
user avatar
  • 493
1 vote
0 answers
25 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 ...
user avatar
  • 1,853
4 votes
2 answers
424 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 ...
user avatar
2 votes
2 answers
766 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 ...
user avatar
1 vote
1 answer
44 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 ...
user avatar
3 votes
1 answer
57 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 ...
user avatar
  • 31
0 votes
1 answer
203 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
user avatar
2 votes
1 answer
161 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\...
user avatar
2 votes
2 answers
1k 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 ...
user avatar
  • 121
2 votes
2 answers
62 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 ...
user avatar
  • 1,853
0 votes
0 answers
105 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 ...
user avatar
2 votes
0 answers
124 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. ...
user avatar
  • 3,464
5 votes
2 answers
536 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 ...
user avatar
  • 153
2 votes
0 answers
281 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 ...
user avatar
  • 121
1 vote
1 answer
61 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: ...
user avatar
  • 2,196
5 votes
1 answer
218 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: ...
user avatar
  • 2,196
3 votes
1 answer
52 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. ...
user avatar
  • 1,853
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 ...
user avatar
  • 1,853
0 votes
1 answer
162 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" ...
user avatar
  • 1,853
6 votes
2 answers
2k 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 ...
user avatar
  • 1,853
2 votes
1 answer
335 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, ...
user avatar
  • 1,853
1 vote
1 answer
80 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 ...
user avatar
  • 1,853
2 votes
0 answers
223 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 ...
user avatar
  • 1,853
1 vote
0 answers
62 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 $ ...
user avatar
1 vote
0 answers
51 views

How to Construct Kripke Structure States from Nested Functions

Say I have these defined functions: ...
user avatar
  • 1,853
1 vote
0 answers
72 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 ...
user avatar
  • 1,853
0 votes
1 answer
97 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 (...
user avatar
  • 1,853
3 votes
1 answer
122 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 ...
user avatar
  • 1,853
1 vote
1 answer
235 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\\ &\}\\...
user avatar
  • 1,853
1 vote
0 answers
140 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 ...
user avatar
  • 1,853
0 votes
1 answer
84 views

How to apply Operational Semantics to this function

Say I have a function like this: ...
user avatar
  • 1,853
1 vote
1 answer
122 views

If a Triple Graph Grammar rule counts as a Mathematical Proof

I am intrigued by Triple Graph Grammars (TGG) as a potential for formal mathematical proof. Triple Graph Grammars (TGGs) are a technique for defining the correspondence between two different ...
user avatar
  • 1,853
3 votes
0 answers
50 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 ...
user avatar
-2 votes
1 answer
160 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 ...
user avatar
  • 97
0 votes
1 answer
6k 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 <...
user avatar
  • 101