Questions tagged [software-verification]

Questions about methods and techniques to prove correctness of programs.

Filter by
Sorted by
Tagged with
1
vote
0answers
48 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 ...
0
votes
0answers
10 views

Transform pLTLf to LTLf and vice versa

I want to verify some properties on finite traces. These properties can be in pLTLf (past LTLf) or LTLf. I want to be able to always traverse the trace forwards, which, depending on the algorithm, is ...
0
votes
0answers
18 views

Textbooks about the verification of computer programs that use Z as the specification language

I'm looking for textbooks/lecture notes about the verification of computer programs, i.e. proving their correctness, that use Z as the specification language against which the correctness is verified.
0
votes
0answers
14 views

Informal definition of a safety property

Could someone kindly explain why safety properties are commonly informally described as "something bad never happens"? This doesn't seem accurate at all. Rather, it seems that one should say ...
2
votes
1answer
47 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
0answers
44 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 ...
0
votes
0answers
26 views

Understanding Subset construction in following example

In going through the paper, Synthesizing Runtime Enforcer of Safety Properties Under Burst Error, https://link.springer.com/chapter/10.1007/978-3-319-40648-0_6, where the example automata considered ...
2
votes
0answers
28 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 ...
36
votes
5answers
5k 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 ...
1
vote
0answers
21 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 ...
4
votes
2answers
286 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
votes
1answer
104 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
1answer
39 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 ...
3
votes
1answer
42 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 ...
0
votes
1answer
148 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
2
votes
1answer
55 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\...
2
votes
2answers
511 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 ...
2
votes
2answers
57 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 ...
0
votes
0answers
85 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
votes
0answers
102 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. ...
4
votes
2answers
288 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 ...
2
votes
0answers
167 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 ...
1
vote
1answer
59 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: ...
5
votes
1answer
172 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: ...
3
votes
1answer
44 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. ...
1
vote
0answers
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 ...
0
votes
1answer
125 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" ...
4
votes
2answers
1k 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
votes
1answer
212 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, ...
1
vote
1answer
56 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
votes
0answers
192 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 ...
1
vote
0answers
53 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 $ ...
1
vote
0answers
46 views

How to Construct Kripke Structure States from Nested Functions

Say I have these defined functions: ...
1
vote
0answers
68 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 ...
0
votes
1answer
61 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 (...
3
votes
1answer
93 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 ...
1
vote
1answer
203 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\\ &\}\\...
1
vote
0answers
90 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 ...
0
votes
1answer
68 views

How to apply Operational Semantics to this function

Say I have a function like this: ...
1
vote
1answer
102 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 ...
3
votes
0answers
48 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 ...
-2
votes
1answer
91 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 ...
0
votes
1answer
4k 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 <...
0
votes
0answers
23 views

Does there exist a conservative algorithm to determine if a certain property is satisfied at a certain part of a program?

... x = a / b; For the above code, for example, is there a way to determine whether b could be zero at the time of division, ...
4
votes
1answer
147 views

Continuation-passing style: what is meant by “CPS'ing”?

I'm reading Dijkstra Monads for Free for a presentation I'll be doing and it's pretty meaty. One of the things that I keep running into is the term "CPS'ing". I've read a little bit on ...
3
votes
0answers
416 views

Expression of the weakest precondition of a while loop

I am interested in computing weakest preconditions (WP) of loops. If I refer to Wikipedia "Predicate Transformer semantics", the WP for e.g. total correction of a loop annotated with an invariant I ...
1
vote
1answer
150 views

How to prove the equivalence between Hoare and Floyd assignment axioms?

How to show that these two axioms are equivalent: 1: $\{G[v/e]\} v:=e \{G\}$ 2: $\{F\} v:=e \{\exists v' (F[v/v'] \land v=e[v/v'])\}$ I've tried with $G = \exists v' (F[v/v'] \land v=e[v/v']) $and ...
2
votes
0answers
32 views

State-of-the-art for Set Constraints?

I've recently stumbled across the field of Set constraints for program analysis, that is, solving equations of the form $exp_1 \subseteq exp_2$, where (depending on the particular variant of the ...
0
votes
1answer
127 views

LTL to GBA versus LTL to BA

Let's assume that I have an LTL formula and I want to convert it to a Buchi automaton. For which fragment of LTL, GBA is more succinct and for which fragment BA has the same size as GBA.
2
votes
3answers
75 views

What are some comparative studies on program termination verification tools? [closed]

Comparative studies of tools like AProver, 2LS