# Questions tagged [software-verification]

Questions about methods and techniques to prove correctness of programs.

125 questions
Filter by
Sorted by
Tagged with
22 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 ...
• 80
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 ...
• 359
16 views

### How do static analysis tools automate separation logic?

I understand separation logic as a form of verification method, similar to Hoare logic. That is, they allow to reason about statements of the form $\{P\} C \{Q\}$, where $C$ is an instruction, and $P$ ...
27 views

### Algorithmic Information Approximation As Software Surface Minimization

Can putting information systems through a "functional bottleneck" to approximate their Algorithmic Information reduce their attack and argument surfaces substantially? Software surface may ...
• 404
141 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 ...
• 287
400 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 ...
82 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
86 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?
326 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
1 vote
60 views

• 33
115 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
61 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 ...
49 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
40 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
53 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 ...
• 23
1 vote
95 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
60 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: ...
87 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
55 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 ...
137 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,194
272 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 "...
• 121
1 vote
75 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 ...
1k 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
46 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 ...
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
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
31 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,243
781 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 ...
• 3,050
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 ...
1 vote
56 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 ...
66 views

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
66 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,243
125 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 ...
• 3,050
227 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,932
776 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
430 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
63 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,194
254 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,194
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,243
1 vote
24 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,243
212 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,243
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,243
491 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,243
1 vote
91 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,243