Questions tagged [software-verification]

Questions about methods and techniques to prove correctness of programs.

23 questions with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
3
votes
1answer
38 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 ...
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 ...
3
votes
0answers
372 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 ...
2
votes
0answers
27 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 ...
2
votes
0answers
94 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. ...
2
votes
0answers
126 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 ...
2
votes
0answers
180 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
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 ...
2
votes
0answers
50 views

Structural induction in non-local program transformation

Assume a functional language and a specialization operation (pulling out sub-expressions): let f x y = (h 23 x) + (g 42 y) becomes ...
2
votes
0answers
170 views

How to show equivalence of the Hoare assignment axiom vs Floyd assignment axiom?

I know from several sources that they are equivalent, but couldn't find a reasonable explanation. My first approach was to show their equivalence by using the logical consequence rule and both axioms, ...
2
votes
0answers
88 views

Is there any open-source tools for verifying TCTL formulae over timed automata can be imported into my project?

In my project, there is one important step to automatically verify a timed automata with TCTL formulae. I briefly surveyed the tool UPPAAL that provides a GUI to construct a timed automata and to ...
1
vote
0answers
24 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\...
1
vote
0answers
20 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 ...
1
vote
0answers
52 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
45 views

How to Construct Kripke Structure States from Nested Functions

Say I have these defined functions: ...
1
vote
0answers
67 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 ...
1
vote
0answers
79 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 ...
1
vote
0answers
455 views

How does one guarantee that the commutative, associative and distributive properties hold for a type?

While most main stream programming languages allow for user defined types that can have the following properties: associative commutative distributive the only way I know of that this can be ...
0
votes
0answers
25 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 ...
0
votes
0answers
22 views

How to solve Hoare's problem when precondition contains meta symbols?

This is the proram for which I have to prove correctness using Hoare's Axioms: {X = |x|} if(x<=0) x:=-x; else skip; {X=x} This is my solution so ...
0
votes
0answers
16 views

State-machine semantics of instruction set architectures

An instruction set architecture is an abstraction, a common interface layer between the software and the micro-architecture. The existence of this clearly delineated interface is becoming increasingly ...
0
votes
0answers
77 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 ...
0
votes
0answers
22 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, ...