Questions tagged [formal-methods]

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

Filter by
Sorted by
Tagged with
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 ...
30
votes
2answers
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 ...
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 ...
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
2k 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 ...
18
votes
5answers
918 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 ...
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 ...
17
votes
4answers
2k views

How do you check if two algorithms return the same result for any input?

How do you check if two algorithms (say, Merge sort and Naïve sort) return the same result for any input, when the set of all inputs is infinite? Update: Thank you Ben for describing how this is ...
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}} = \{\...
9
votes
3answers
898 views

Why does the state remain unchanged in the small-step operational semantics of a while loop?

Usually I see that in the structural operational semantics representation for the while loop, the program state don't change: $(while \> B \> do \>S, \sigma) \rightarrow (if \>B \> ...
9
votes
2answers
419 views

Introduction into first order logic verification

I am trying to teach myself different approaches to software verification. I have read some articles. As far as I learned, propositional logic with temporal generally uses model checking with SAT ...
9
votes
0answers
99 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 ...
8
votes
2answers
438 views

What exactly is Symbolic Model Checking?

I know that Symbolic Model Checking is state space traversal based on representations of states sets and transition relations as formulas like in CTL using models like Kripke Model. I know the theory. ...
7
votes
5answers
498 views

Can we quantify how close a partially correct programs is to being correct?

I know that there is something called partial correctness, but I was wondering if there was a way to tell how close a semi-correct program is to a fully correct program. For example, if you had a ...
6
votes
1answer
170 views

Looking for a book that derives and constructs a model checking application

I am teaching myself program verification and am currently learning proof assistants. I have the book Handbook of Practical Logic and Automated Reasoning which gives the proofs necessary for the ...
6
votes
2answers
1k views

Formal Verification of Functional Programs

So I've been interested in learning more about formal verification, and I've seen a lot of interesting things like ACSL and JML which are based on the concept of Hoare triples. My question is, that ...
6
votes
1answer
313 views

Late and Early Bisimulation

This is a follow up to my earlier questions on coinduction and bisimulation. A relation $R \subseteq S \times S$ on the states of an LTS is a bisimulation iff $\forall (p,q)\in R,$ $$ \begin{array}...
6
votes
1answer
113 views

Why are there two different `until` ($\cup$) semantics in Timed Computation Tree Logic?

Background: In the book of Principles of Model Checking (Christel Baier and Joost-Peter Katoen, MIT Press, 2007), Section 9.2, page 701, the semantics of the until modality is defined over some time-...
6
votes
0answers
119 views

Boolean formula that agrees with most truth assignments

Let $X_1,\dots,X_n$ be $n$ boolean variables. I have an unknown predicate $P(X_1,\dots,X_n)$ on these boolean variables. Of course, I can view the predicate as a function $f_P : \{0,1\}^n \to \{0,1\}...
5
votes
2answers
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 ...
5
votes
1answer
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 ...
5
votes
1answer
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 ...
5
votes
1answer
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-...
5
votes
3answers
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 ...
5
votes
0answers
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 ...
4
votes
2answers
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 ...
4
votes
1answer
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 ...
4
votes
1answer
122 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 ...
4
votes
1answer
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[2]. For my work I need to apply contracts to Java bytecode. The ...
4
votes
1answer
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 ...
4
votes
1answer
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 ...
4
votes
1answer
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 ...
4
votes
1answer
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. ...
4
votes
0answers
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 ...
3
votes
3answers
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: <...
3
votes
2answers
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]\!]\...
3
votes
1answer
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 ...
3
votes
1answer
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 ...
3
votes
1answer
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 ...
3
votes
1answer
121 views

Minimal Deterministic Buchi Automata Product

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)...
3
votes
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 ...
3
votes
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 ...
3
votes
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 ...
3
votes
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 ?
3
votes
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 ...
3
votes
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}$ ...
3
votes
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: $...
3
votes
0answers
40 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
0answers
78 views

In ontology development, where do axioms come from?

I am developing an ontology. I've got the classes, relationships and I guess I could come up with instances at this point too. But what I'm really focused on is the axioms. I've learnt that the ...