Skip to main content

Questions tagged [software-verification]

Questions about methods and techniques to prove correctness of programs.

Filter by
Sorted by
Tagged with
0 votes
1 answer
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 ...
revision's user avatar
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 ...
math boy's user avatar
  • 359
0 votes
0 answers
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$ ...
BlockchainThomas's user avatar
0 votes
0 answers
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 ...
James Bowery's user avatar
5 votes
1 answer
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 ...
mell_o_tron's user avatar
0 votes
4 answers
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 ...
Mason Rashford's user avatar
0 votes
1 answer
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, ...
ZENG's user avatar
  • 113
0 votes
3 answers
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?
Hovercraft2's user avatar
0 votes
0 answers
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 ...
programonkey's user avatar
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) \...
V_head's user avatar
  • 33
0 votes
1 answer
3k 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 <...
mateleco's user avatar
  • 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 $...
V_head's user avatar
  • 33
0 votes
1 answer
116 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.
40er's user avatar
  • 3
1 vote
1 answer
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 ...
Roger Costello's user avatar
0 votes
0 answers
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 ...
Vanessa's user avatar
  • 13
1 vote
1 answer
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,...
Vanessa's user avatar
  • 13
1 vote
0 answers
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 ...
Rusurano's user avatar
1 vote
1 answer
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 ...
a_fan's user avatar
  • 111
1 vote
1 answer
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: ...
John Harrington's user avatar
0 votes
1 answer
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 ...
user14789259's user avatar
1 vote
0 answers
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 ...
user avatar
4 votes
1 answer
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 ...
user1868607's user avatar
  • 2,194
2 votes
0 answers
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 "...
kexanie's user avatar
  • 121
1 vote
0 answers
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 ...
burnedWood's user avatar
6 votes
2 answers
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 ...
Physical Mathematics's user avatar
1 vote
0 answers
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 ...
user avatar
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 ...
M. Twarog's user avatar
  • 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 ...
J. Auon's user avatar
  • 503
1 vote
0 answers
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 ...
Lance's user avatar
  • 2,243
5 votes
2 answers
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 ...
Charlie Parker's user avatar
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 ...
Sridhar Sarnobat's user avatar
1 vote
1 answer
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 ...
adamcasey's user avatar
4 votes
1 answer
66 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 ...
enigma's user avatar
  • 41
0 votes
1 answer
384 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
AleWereWolf's user avatar
2 votes
1 answer
489 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\...
AleWereWolf's user avatar
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 ...
Melanie A's user avatar
  • 121
2 votes
2 answers
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 ...
Lance's user avatar
  • 2,243
0 votes
0 answers
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 ...
Charlie Parker's user avatar
3 votes
0 answers
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. ...
user56834's user avatar
  • 3,952
5 votes
2 answers
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 ...
Arqwer's user avatar
  • 153
2 votes
2 answers
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 ...
Tim's user avatar
  • 121
1 vote
1 answer
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: ...
user1868607's user avatar
  • 2,194
5 votes
1 answer
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: ...
user1868607's user avatar
  • 2,194
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. ...
Lance's user avatar
  • 2,243
1 vote
0 answers
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 ...
Lance's user avatar
  • 2,243
0 votes
1 answer
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" ...
Lance's user avatar
  • 2,243
11 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 ...
Lance's user avatar
  • 2,243
2 votes
1 answer
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, ...
Lance's user avatar
  • 2,243
1 vote
1 answer
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 ...
Lance's user avatar
  • 2,243
2 votes
0 answers
257 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 ...
Lance's user avatar
  • 2,243