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

learn more… | top users | synonyms

2
votes
1answer
26 views

Second order function formalization

I need to work on a optimizer for a language whose operator are second order functions. They are the well known ones filter, map, reduce, fold, foreach etc. etc. I need to formalize as much as ...
-1
votes
1answer
72 views

Show that in the Myhill–Nerode equivalence relation for PAL, every string is in an equivalence class by itself [closed]

Show that in the Myhill–Nerode equivalence relation for PAL(palindrome),every string is in an equivalence class by itself
1
vote
1answer
54 views

Theory of formal languages

How do i generate grammar for Prefix of Langauge L, SupposeG=(V,􏰀,P,S)is a context-free grammar generating a CFL L then pref(L) is defined as pref(L)={x∈􏰀∗ : ∃ y such that xy∈L}. I understand for ...
3
votes
3answers
488 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: ...
1
vote
0answers
23 views

Effective method for simulating program's cycle

I'm looking for an effective method to simulate a program. Why I am needing this is because sometimes I can only have the program's description, code, and all I have left is pen and paper when I want ...
0
votes
1answer
57 views

Set containment of MinimumBadPrefix and BadPrefix of a Safety Property

This question is related to formal model checking theory, but I cannot find a tag for it. Let $P_{safe}$ be a safety property. $BadPref(P_{safe})$ is the set of bad prefixes for $P_{safe}$ A Safety ...
0
votes
1answer
39 views

Maximum value a variable can hold without documentation [closed]

Suppose we work with some particular programming language (like C++) on some particular computer. Furthermore, we want to know which values are minimum and maximum for some particular numeric data ...
0
votes
1answer
19 views

Compute Lazily - Model checking

What is meant by lazily computing online? For example, in context of synthesis, that uses model checking. ...
5
votes
0answers
41 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 ...
6
votes
5answers
137 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 ...
1
vote
1answer
63 views

Logic applications and security protocols references request

I'm a student of logic and I'm interested in looking at logic applications, of which I am told there are many, in computer science and allied areas. I've seen some applications. More specifically, I ...
5
votes
0answers
42 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 ...
3
votes
2answers
182 views

Mathematical background for programming languages, compilers and formal methods in software engineering [closed]

Can you tell me what mathematical background (concrete themes) should I have for studying and doing some investigations (in future) in programming languages, compilers and formal methods in software ...
2
votes
0answers
39 views

Is there any open-source tools for verifying TCTL formulae over timed automata can be imported into my project?

In my project, there is one important step to automatically verify a timed automata with TCTL formulae. I briefly surveyed the tool UPPAAL that provides a GUI to construct a timed automata and to ...
3
votes
1answer
50 views

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

Background: In the book of Principle of Model Checking (Section 9.2, Page 701), the semantics of the until modality is defined over some time-divergent path $\pi ...
1
vote
1answer
47 views

Questions from Dijkstra's EWD 1300: “The notational conventions I adopted, and why”

A link to the transcript of the manuscript: http://www.cs.utexas.edu/users/EWD/transcriptions/EWD13xx/EWD1300.html My questions: What does Dijkstra mean by: "Do not introduce priority ...
2
votes
1answer
271 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 ...
3
votes
1answer
141 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 ...
1
vote
1answer
49 views

Trace dependents & precedents of a program in an imperative language

We have some programs in a very basic imperative language, the programs contain some basic features: assignment, condition, loop, scalar variables, 1-dimensional arrays and 2-dimensional arrays... ...
1
vote
3answers
165 views

Binary decision diagram for a six-figure Boolean function

Let $p$ be the six-figure Boolean function with the following definition: $p(x_{0},x_{1},x_{2},x_{3},x_{4},x_{5})=\begin{cases} true & \text{if } x_{0}=x_{5} \text{ and } x_{1}=x_{4} ...
1
vote
0answers
181 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} ...
0
votes
1answer
219 views

Initial Algebra example

If the definition of Initial Algebra is: "An object is initial if there exists a unique morphism from the object to every object in the category" Why do we need such object, and could any one give ...
3
votes
1answer
72 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. ...
7
votes
2answers
228 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 ...
4
votes
1answer
151 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 ...
3
votes
1answer
85 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 ...
3
votes
1answer
110 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 ...
3
votes
1answer
84 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}$ ...
9
votes
4answers
556 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 ...
8
votes
2answers
953 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}} = ...
5
votes
1answer
135 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,$ $$ ...
12
votes
3answers
863 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 ...
29
votes
2answers
1k 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. ...
13
votes
3answers
483 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 ...
10
votes
5answers
314 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 ...
20
votes
2answers
513 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 ...
15
votes
6answers
1k 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 ...