Questions tagged [formal-methods]
a particular kind of mathematically-based technique for the specification, development and verification of software and hardware systems.
17
questions
23
votes
6answers
3k views
Algorithm to solve Turing's “Halting problem”
"Alan Turing proved in 1936 that a general algorithm to solve the
halting problem for all possible program-input pairs cannot exist"
Can I find a general algorithm to solve the halting problem for ...
70
votes
2answers
8k views
What is coinduction?
I've heard of (structural) induction. It allows you to build up finite structures from smaller ones and gives you proof principles for reasoning about such structures. The idea is clear enough.
But ...
18
votes
5answers
952 views
Is it possible to solve the halting problem if you have a constrained or a predictable input?
The halting problem cannot be solved in the general case. It is possible to come up with defined rules that restrict allowed inputs and can the halting problem be solved for that special case?
For ...
30
votes
2answers
990 views
Equivalence of Büchi automata and linear $\mu$-calculus
It's a known fact that every LTL formula can be expressed by a Büchi $\omega$-automaton. But, apparently, Büchi automata are a more powerful, expressive model. I've heard somewhere that Büchi automata ...
2
votes
2answers
904 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 ...
10
votes
2answers
4k views
A Question relating to a Turing Machine with a useless state
OK, so here is a question from a past test in my Theory of Computation class:
A useless state in a TM is one that is never entered on any input string. Let $$\mathrm{USELESS}_{\mathrm{TM}} = \{\...
3
votes
1answer
80 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 ...
20
votes
3answers
1k views
Path to formal methods
It is not uncommon to see students starting their PhDs with only a limited background in mathematics and the formal aspects of computer science. Obviously it will be very difficult for such students ...
20
votes
3answers
3k views
When are two simulations not a bisimulation?
Given a labelled transition system $(S,\Lambda,\to)$, where $S$ is a set of states, $\Lambda$ is a set of labels, and $\to\subseteq S\times\Lambda\times S$ is a ternary relation. As usual, write $p \...
18
votes
2answers
3k views
What is this fraction-like “discrete mathematics”–style notation used for formal rules?
In the paper "A Conflict-Free Replicated JSON Datatype", I encountered this notation for formally defining "rules":
What is this notation called? How do I read it?
For example:
the ...
17
votes
2answers
2k views
Program Correctness, The specification
From Wikipedia: In theoretical computer science, correctness of an algorithm is asserted when it is said that the algorithm is correct with respect to a specification.
But the problem is that to get ...
5
votes
1answer
124 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
166 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 ...
1
vote
0answers
45 views
How to Construct Kripke Structure States from Nested Functions
Say I have these defined functions:
...
1
vote
0answers
434 views
Logical conjunction of two binary decision diagrams
Compute a BDD for $B_{1} \wedge B_{2}$ by using an algorithm that applies dynamic programming. Document the execution of the algorithm by indicating pairs of BDDs $(q_{1},q_{2})$ and the BDD $q_{1} \...
1
vote
1answer
174 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\\
&\}\\...
0
votes
1answer
58 views
