Questions tagged [formal-methods]
a particular kind of mathematically-based technique for the specification, development and verification of software and hardware systems.
130
questions
2
votes
1answer
71 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 ...
2
votes
1answer
57 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 ...
1
vote
1answer
36 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:
...
1
vote
1answer
46 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{...
2
votes
0answers
43 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 ...
0
votes
0answers
19 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.
1
vote
2answers
79 views
2
votes
2answers
86 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
1answer
74 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 ...
1
vote
3answers
83 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?
0
votes
1answer
46 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 ...
0
votes
1answer
69 views
LTL Model of (infinitely often p) ∧ ( infinitely often q) ∧ (¬ Eventually (p ∧ q))?
Can anyone give a model (pi) of the ltl formula above?
5
votes
1answer
104 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 ...
0
votes
0answers
30 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 ...
37
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 ...
2
votes
2answers
50 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 ...
0
votes
1answer
22 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 ...
4
votes
1answer
110 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 ...
3
votes
1answer
34 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 ?
1
vote
1answer
60 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 ...
2
votes
1answer
233 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 ...
2
votes
2answers
58 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 ...
1
vote
0answers
48 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 ...
0
votes
0answers
36 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 ...
0
votes
1answer
45 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 ...
1
vote
2answers
173 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 ...
5
votes
1answer
234 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 ...
3
votes
1answer
237 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
votes
1answer
134 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\ ...
10
votes
0answers
105 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 ...
5
votes
1answer
190 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 ...
2
votes
0answers
109 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.
...
5
votes
2answers
363 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 ...
1
vote
1answer
31 views
Define a length function over $A^{*} \leftarrow{N}$ such that $length(l)$ outputs the length of $l$
Consider the following definitions
LIST:
$\overline{nil} \ \ \ \ \ \frac{l}{a \ l}$ $a \in A$
$A^* = \mu \widehat{LIST}, \ A^{\infty} = v \widehat{LIST}$
NAT:
$\overline{0} \ \ \ \ \ \frac{x}{s(...
1
vote
2answers
62 views
How can MLTT etc encode computability?
I am recently thinking about proving the undecidability of some problem. This problem has been formalized in Coq and by staring at it, people including me think "for sure" this is undecidable. "For ...
3
votes
0answers
58 views
What is the difference between the choice operator and nondeterminism in CSP?
I'm learning CSP now for my research. First time doing formal work in CS. I'm having a hard time understanding the difference between choice $\square$ operator and the nondeterminism $\sqcap$ operator....
3
votes
2answers
153 views
Why does the denotational semantics for a while loop have a existence quantifier?
I was going through these notes and they have the following operator on partial functions:
$$
\mathcal F^{k}(\bot)(\sigma) =
\left\{
\begin{array}{ll}
\alpha( [\![s]\!]\sigma ) & [\![b]\!]\...
3
votes
1answer
206 views
Relating a proof to a Haskell program
I am trying to relate the following integer square root theorem
$\forall x: \mathbb{N}, \exists y : \mathbb{N}((y^2 \leq x) \land (x < (y+1)^2))$
and its proof to its role as a specification of ...
2
votes
2answers
95 views
How to express the existence of winning strategy of the starter of a game in temporal logic?
Consider a two-player game. A winning strategy of a player is a strategy following which the player can always beat his opponent, no matter how his opponent responds.
A game can be unfolded to a ...
0
votes
1answer
148 views
How to collect all states of a behavior in TLA+?
Description of the problem:
I am modeling checking a distributed protocol against a global property with TLA+ developed by Leslie Lamport. The global property is defined on all states of a behavior (...
0
votes
1answer
72 views
How to solve for the precondition give a postcondtion that must satisfy two conditions
I tried solving past exam question but there is this one that I haven't been able to solve.
The question states that a suitable precondition should be found for the statement.
$$
a= i +2; i++\{(a = ...
0
votes
1answer
170 views
Topics from theoretical computer science suitable for a bachelor (undergrate) thesis? [closed]
Is the field of theoretical computer science so complex, that it is just "too much" for a bachelor thesis? Unfortunately I haven't found any old thesises because the relevant chair of the university ...
1
vote
1answer
61 views
Software code generation from the (operational) semantics - reference request for automatic programming
Are there research trends that try to research code generation directly from the (operational or some other kind of) semantics? One can imagine cognitive architecture that discovers and reasons about ...
1
vote
0answers
33 views
How Model Checking works with User Interaction
In order to understand how to apply Model Checking, I am wondering how to apply it to a pseudo-realistic async program.
Say I have the following pseudocode:
...
5
votes
2answers
2k 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
2answers
101 views
What exactly state is in Model Checking
So I finally realized the difference between transition systems and automata, and now am closer to understanding Model Checking. One of the last pieces is understanding what exactly "state" is in ...
5
votes
1answer
392 views
How does TLC check liveness properties?
The paper "Model Checking TLA+ Specifications" published in 1999 explained how TLC (Temporal Logic Checker) checks safety properties written in TLA+ developed by Lamport. At that time, TLC did not yet ...
1
vote
0answers
47 views
How to Construct Kripke Structure States from Nested Functions
Say I have these defined functions:
...
3
votes
1answer
101 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
207 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\\
&\}\\...
