# Questions tagged [formal-methods]

a particular kind of mathematically-based technique for the specification, development and verification of software and hardware systems.

130 questions
Filter by
Sorted by
Tagged with
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 ...
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 ...
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: ...
46 views

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 ...
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 ...
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 (...
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 = ...
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 ...
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 ...
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: ...
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 ...
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 ...
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 ...
47 views

### How to Construct Kripke Structure States from Nested Functions

Say I have these defined functions: ...