Questions tagged [formal-methods]
a particular kind of mathematically-based technique for the specification, development and verification of software and hardware systems.
148
questions
0
votes
0
answers
27
views
Abstract Interpretation: prove that the sign subtraction is increasing in each of its parameters
I need to prove that the binary operator $-_\pm: \mathbb{P}^\pm\times\mathbb{P}^\pm\rightarrow\mathbb{P}^\pm$ is increasing in each of its arguments, where
$$
\mathbb{P}^\pm = \{\top_\pm, \leq0,\...
- 101
1
vote
0
answers
16
views
Rationale behind prefix-closure in CSP trace semantics
I'm currently studying Hoare's "Communicating Sequential Processes" (1) and I've come across a concept that I find a bit puzzling. In CSP trace semantics, a process's semantics are described ...
- 111
0
votes
1
answer
75
views
How to start with verifying a formal proof programmatically?
I heard the terms "theorem provers" and "proof assistants" tossed around before (which I assumed to be the same up until a couple seconds ago), and also of Coq, Idris, Agda, TLA+ (...
- 105
3
votes
0
answers
179
views
Does this paper by Patrick Cousot describe an undecidable method for model checking?
All of the discussion is in the context of this paper.
I think that the whole procedure that the paper describes is not decidable, because if we can have an algorithm for it, then we can solve halting ...
- 31
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) \...
- 33
0
votes
1
answer
1k
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 <...
- 108
0
votes
0
answers
37
views
Minimum DNF length of a conjuction of equivalences
Show that the formula $\bigcap_{i=1}^n (X_i \leftrightarrow Y_i)$ cannot have an equivalent disjunctive normal form with less than $2^n$ clauses.
I am puzzled on what approach to take -- whether to ...
- 109
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 $...
- 33
1
vote
2
answers
58
views
"Largest set" in coinductive definitions
In several explanations of coinductive definitions (for example, in the answers to What is coinduction?), we're told that while an inductive definition gives us the smallest set with a specified set ...
- 946
0
votes
2
answers
92
views
What is the difference between type inhabitant and subtyping?
I am confused with the terms inhabitant vs. subtyping.
For example,
We usually think that "john is an inhabitant of Human". This sentence is correct, because john is an individual, and an ...
- 265
1
vote
1
answer
58
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 ...
- 393
1
vote
1
answer
121
views
Proving a predicate assignment is correct
I am currently reading Formal Methods - An Appetizer and am stuck in chapter 3 (Program Verification).
I am unfamiliar with logic and I do not think I understand the $\vDash$ notation correctly.
I ...
user148883
1
vote
0
answers
40
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 ...
- 13
3
votes
1
answer
71
views
Abstract Interpretation: Connection between soundness relation and a Galois connection
I am currently studying the paper "Abstract Interpretation Frameworks" by Cousot and Cousot from 1992 (https://doi.org/10.1093/logcom/2.4.511) to gain an understanding of the theory behind ...
- 161
1
vote
1
answer
73
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
0
answers
88
views
SMT validity solvers/ quantifier elimination in Ocaml
I am working on my own expression package in Ocaml and have to perform both validity queries and quantifier elimination. I have already implemented Cooper's procedure (for Presburger and Linear ...
- 113
1
vote
1
answer
54
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:
...
- 113
3
votes
0
answers
25
views
Formal instruments to check properties of SQL queries
I have some operations defined as SQL queries which takes data from various tables combines it with the data from a base table and generates new rows, which are written back to the base table. In the ...
- 131
1
vote
0
answers
45
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 ...
user127009
0
votes
0
answers
42
views
Hoare Triple Logic
I'm having trouble understanding the logic behind Hoare Triples. The question asks for the missing value of the precondition {X}
...
2
votes
1
answer
140
views
Why sequential consistency model is widely used if it is unsound
From this talk and these lecture notes here and here I learned that sequential consistency does not actually model what really happens in practice. However, it is also pointed out that most of the ...
- 483
2
votes
1
answer
80
views
Is a system of equations derived from mutually recursive ADTs always uniquely solvable?
After looking at Can a computer determine whether a mathematical statement is true or not? for a while, I worry we may be into incompleteness/halting problem territory with this question, so an answer ...
- 645
1
vote
2
answers
134
views
Z Notation: sequence of sequences - find sum
Let me just say that this is for a university project. I do not expect an answer but more of a "hint".
I have a schema of a Supermarket that holds a sequence of queues:
...
- 111
1
vote
1
answer
49
views
Where should "imply" be placed in this formalisation?
I have to formalize the following sentence:
If any house is green then there exists a horse that is white.
I have formalized it the following way:
$$\forall(x)(\mathit{house}(x)\rightarrow \mathit{...
- 125
2
votes
0
answers
53
views
Does Rice's theorem apply to sequential logic circuits?
I am wondering if Rice's theorem (or something similar to that) applies also to sequential circuits. I.e. given any finite sequential circuit, can there be an algorithm that can formally verify any ...
- 121
1
vote
2
answers
121
views
Interpreting a proof of $2^\mathbb{N}$ being uncountable
Suppose I have the following proof:
...
- 175
3
votes
2
answers
812
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 ...
3
votes
1
answer
80
views
How to prove that replacing a character in a string in both C and JavaScript is equivalent?
I would like to try some different proofs, specifically in proving equivalence of the implementation of some feature in two different programming languages (C and JS in this question).
This is about ...
- 2,163
1
vote
3
answers
120
views
is (infinitely often p) ∨ (infinitely often ¬p) valid?
i'm trying to prove every trace over PROP = {p} is a model of the formula.
I am very stuck in figuring out a model pi that satisfies this formula, can anyone point me in the right direction?
- 39
0
votes
2
answers
85
views
Z-Specification = Routes
Im trying to make an invariant for this Z schema about routes.
1) The invariant should express that each route should contain at least 20 different places. First of all i thought of doing a universal ...
- 39
1
vote
1
answer
173
views
LTL Model of (infinitely often p) ∧ ( infinitely often q) ∧ (¬ Eventually (p ∧ q))?
Can anyone give a model of the following LTL formula?
$$
\Box\Diamond p \land \Box\Diamond q \land \lnot \Diamond (p \land q).
$$
That is, we want each of $p$ and $q$ to hold infinitely often, but $p \...
- 39
5
votes
2
answers
183
views
proving program equivalence
I understand that the general problem of program equivalence is undecidable, but I'm wondering what approaches exist to tackle the problem? I am familiar with Hoare-style verification, but are there ...
- 51
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 ...
- 503
2
votes
2
answers
65
views
Modeling a set of probabilistic concurrent processes
I'm looking into discrete-time Markov chains (DTMCs) for use in analyzing a probabilistic consensus protocol. One basic thing I haven't been able to figure out is how to model a set of independent ...
- 209
0
votes
1
answer
25
views
What's the meaning of this service specification
What's the meaning of the example statement here?
"A service specification S describes an interface: it specifies the behavior of certain program elements (functions or subprograms) through ...
- 103
5
votes
1
answer
164
views
Proving with co-induction principles
I'm going through Adam Chlipala's "Certified Programming with Dependent Types" (available here for convenience), and I'm a bit stuck at internalizing the introduction of co-induction principle for the ...
- 175
3
votes
1
answer
56
views
Having a formal ISA specification - What does correctness mean?
Does this always mean that a program can be correct in regard to that spec or is there any correctness of the spec itself ?
- 31
1
vote
1
answer
67
views
Are the two LTL properties $GF(\psi_1 \land F\psi_2 )$ and $GF(\psi_2 \land F\psi_1 )$ equivalent?
Is $GF(\psi_1 \land F\psi_2 )$ equivalent to the property $GF(\psi_2 \land F\psi_1 )$?
Attempt:
In the first property each state must eventually see $\psi_1$ and $\psi_2$, in the second property as ...
- 509
3
votes
1
answer
488
views
Hoare logic, proving conjunction rule from basic rules, possible or not?
(This is HW.) Suppose I have these following proof rules given.
I am currently considering if I can prove the conjunction rule (given below) from the above given Hoare logic rules.
My answer would ...
- 189
2
votes
2
answers
63
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,163
1
vote
0
answers
54
views
Prove that set of operations form a commutative Monoid
this is my first post on this exchange.
I am looking for some help with defining a proof that a set of operations I have designed forms a commutative monoid.
(Disclaimer: I am not sure that I have ...
- 111
0
votes
0
answers
40
views
Formal language representation of program
I have numerous records, composed of words. Each word gets translated into vectors, with a variable number of channels, provided that that word exists in a specific lookup dictionary.
For n number of ...
- 101
0
votes
1
answer
56
views
Effective Procedures and P vs NP Problem
If, suppose, P doesn't equal NP. Implication of this statement is that there is no effective procedure to solve a hard problem; however there exists an acceptable solution S. I have following two ...
- 135
1
vote
2
answers
295
views
Buchi automata in formal software verification
As I am studying the application of Buchi automata in formal software verification, I am interested in the computational complexity (or links to papers) for the algorithms used to solve the problem in ...
- 237
5
votes
1
answer
335
views
The definition of weakest precondition for a non-deterministic language
In the classical IMP language, the definition of weakest precondition is:
definition "wp c Q s ≡ ∃t. (c,s) ⇒ t ∧ Q t"
This is stating that from state s, after ...
- 2,240
3
votes
1
answer
473
views
The Law of Excluded Miracle in the language of guarded commands
The definition of weakest precondition is familiar (let me use Isabelle's syntax here):
definition "wp c Q s ≡ ∃t. (c,s) ⇒ t ∧ Q t"
the weakest precondition ...
- 2,240
2
votes
1
answer
198
views
How to prove a LTL formula correct in a specific model?
I have been learning Verification by model checking recently and I get the following question:
$Whether\ the\ LTL\ formula\ M, q_3\ \models (X\ \lnot a) \rightarrow (F\ G\ \lnot a)\ is\ established\ ...
- 135
10
votes
0
answers
115
views
Can we say McCarthy and Hoare had the same objective in the 60s regarding a mathematical theory of computation?
I don't think there's any way to ask a very precise question here, so this might be considered opinion based. Nevertheless, it seems the question is clear enough because I'm asking whether these two ...
- 237
7
votes
1
answer
359
views
Roadmap to formal verification
I would like to learn about different approaches to formal verification of software programs that goes beyond what Wikipedia has to offer. Ideally one would not only get an overview but also ...
- 171
3
votes
0
answers
185
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,622