# Questions tagged [formal-methods]

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

121 questions
Filter by
Sorted by
Tagged with
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 ...
979 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 ...
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 ...
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 ...
3k views

98 views

### How does automated verification of systems with infinitely many states work?

I need some help with basic definitions and intuition to understand why and how it's possible to verify systems with infinitely many states. For example, if I consider an x86 computer, and assuming ...
62 views

### Problem with definition of bisimilarity

In my model checking class we have defined a bisimulation like this: Let $K=(S,S_0,Act,R,L)$ and $K'=(S',S'_0,Act,R',L')$ be two kripke structures. A relation $B \subseteq S \times S'$ is called ...
120 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 ...
66 views

### Efficient Algorithm Linear Temporal Logic to Deterministic Rabin Automata

I am trying to construct an equivalent Deterministic Rabin Automata (DRA) given a Linear Temporal Logic (LTL) Formula. One (expensive) way to do this would be to construct an equivalent Non-...
215 views

### Formalizing self-propagating behaviour

Since reading Ken Thompson's Reflections on Trusting Trust I am trying to formalize the idea of a program which mutates its own behaviour; specifically, a program that would be self-reproducing except ...
143 views

### Introduction to bounded model checking that describes model generation

Most of the tutorials I have found on model checking and bounded model checking start with, the model is given as a Kripke Structure M = (S,I,T,L) where S is a set of states, I is a set of initial ...
182 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 ...
262 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 ...
122 views

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 ...
360 views

### Contracts for Java Bytecode

Introduction For a paper I need contracts, which are also referred to as Design by Contract (DbC)1, and conceptually go back to Hoare. For my work I need to apply contracts to Java bytecode. The ...
360 views

### How to implement simulation on two LTSs?

Does any one know how to implement the simulation relation on two labelled transition systems (LTS)? I know how to do it for branching bi-simulation. The signature refinement theorem is used for ...
139 views

### Witness for the $EU(\phi_1,\phi_2)$ using BDDs

I wanted ask if you know an algorithm to find the witness for $EU(\phi_1,\phi_2)$ (CTL formula "Exist Until") using BDDs (Binary Decision Diagram). In pratice you should use the fixed point for ...
74 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 ...
90 views

### Reference Request for Synthesis

New to the world of software verification and synthesis. It was suggested to me that the book "Principles of Model Checking" is a good reference for verification, but I am clueless about synthesis. ...
46 views

### How the $EX(f)$ is evaluated in symbolic model checking?

I was reading the symbolic model checking, So there it has mentioned that we can represent the set of states and transition relations of any transition system with the help of ROBDDs. I was trying to ...
2k views

### Rigorous Proof of Insertion Sort

Currently I self study CLRS book (Outside of any course, so I got no access to an instructor) And I am stuck proving Insertion Sort, The proof in CLRS book is not so formal. Here's the algorithm: <...
80 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]\!]\...
164 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 ...
78 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 ...
558 views

### Language independent software libraries

When trying to decide on the choice of a programming language for a specific task, people will often tell me: "use this language because it has the best library for the type of problems you are ...
121 views

Problem: Let $\varphi = \varphi_1 \land \varphi_2$ be Deterministic Buchi Automata (DBA) expressible LTL formulas. Let $A$, $A_1$ and $A_2$ be translated DBAs such that ${\cal{L}}(A) = {\cal{L}}(A_1)... 1answer 329 views ### What does “AF AX p” mean in CTL? Both Logic in Computer Science (Huth and Ryan, 2004) and Branching vs. Linear Time: Final Showdown (Vardi, 2002), state something to this effect (paraphrased): In LTL, X F p and F X p are ... 1answer 126 views ### Anotation rules for while rule in deductive verification I have been studying deductive verification of software lately, with weakest precondition, strongest postcondition, annotation calculus, and etc. I came across the following rules for the while ... 1answer 377 views ### How to Generate Control flow graph from a Petri net model? My research is mainly focused on generating test sequences automatically using Colored Petri net.CFG provides techniques for generating test sequences. But some papers says that, test sequence ... 1answer 28 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 ? 1answer 143 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 ... 1answer 256 views ### Time to construct a GNBA for LTL formula I have a problem with the proof for constructing a GNBA (generalized nondeterministic Büchi automaton) for a LTL formula: Theorem: For any LTL formula$\varphi$there exists a GNBA$G_{\varphi}$... 1answer 57 views ### Weak bisimulation up-to$\approx$Given this definition of weak bisimilarity: A configuration relation$\mathcal{R}$is a weak bisimulation provided that whenever$P\ \mathcal{R}\ Q$and$\alpha$is$\mu$or$\tau$action then:$...
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....