# Tagged Questions

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

50 views

### Efficient algorithms for checking non-emptiness of the language of a Turing machine

I know that language non-emptiness is TM recognizable, and one can perform a BFS to find an input string that TM accepts, if there is any. But, what is the most efficient algorithm for that?
43 views

### What are these questions in the PoplMark challenge asking?

I was reading the paper Mechanized Metatheory for the Masses: the PoplMark Challenge by Aydemir et al (PDF) and I found the following three questions on page 13 of the PDF a bit confusing. ...
11 views

### how to understand these in PoPLMARK challenge? [duplicate]

I was reading the PoPLMARK challenge and in the paper proposed that challenge, I find some parts confusing me, here original paper. In challenge 3:Testing and Animating with respect to semantics, I ...
22 views

### Complexity of choosing a suitable Boolean algebra domain for program analysis

Do you know the complexity class of the following problem? Input: A sequential non-deterministic program over integer variables, equipped with initial values of these variables. The exact ...
21 views

### Complexity of choosing a suitable positive domain for program analysis

Do you know the complexity class of the following problem? Input: A sequential nondeterministic program over integer variables, equipped with initial values of these variables. The exact ...
36 views

### Complexity of choosing a suitable disjunctive domain for program analysis

Do you know the complexity class of the following problem? Input: A sequential nondeterministic program over integer variables, equipped with initial values of these variables. The exact ...
39 views

### How to prevent deletion in an array in the B method

I have created a very basic model of an array list in the B method as shown below ...
39 views

### Proving weak simulation

I want to prove something but I am not sure if it is the right way to do it. I have two LTS that define different semantics. A=($Q_a,Λ,\to)$, and B=$(Q_b,Λ\cup\{\beta\},\leadsto)$, where $\beta$ is ...
55 views

### Reverse linked listed — formal method?

I am trying to do some formal modeling of a linked list, however instead of referencing the next block, each block needs to reference the previous block instead. Is there already any formal methods ...
32 views

### What is a local inference system?

A inference system is a set of rules that can be used to prove something in some formal model. I understand that. But what does it mean to a inference system to be local? For instance, in the page ...
22 views

### What does “post-image analysis” mean in the context of formal program analysis?

I am reviewing an anonymous paper about a sort of static analysis of programs that uses the phrase "post-image analysis", or "post-image operation" without defining what that is. I am guessing it is a ...
45 views

### How might I express a sequence of operations in formal terms?

I want to be able to represent a set of operations in sequential order such that they will represent what is traditionally called a "function" (which is not always the mathematical definition of a "...
38 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 ...
38 views

### Help understaning LTL formulae [closed]

I am studying Software Engineering and I have different LTL formulas for which I have to determine if they are valid, unsatisfiable or neither. Here are the formulas : (<>[]p ∧ <>[]q) → <>[...
86 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 ...
159 views

### LTL properties in bounded model checking via assertions

Is there a way to check LTL properties in a bounded model checker? As an example, consider a liveness property ($G F p$ - always eventually $p$)? Suppose we have the following trivial program ...
151 views

### What are GEN and KILL statements in dataflow analysis?

In data flow analysis, is GEN statement where a variable is used and KILL statement is where variable is redefined?
104 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 ...
55 views

### What does least fix point and greatest fix point mean in Safety games

In safety games there are these mathematical notation about greatest fix points and least fix points but I don't get it. How would we describe them plain English without mathematical symbols.
59 views

### Double ended queue data abstraction and axioms

I am trying to show the data abstraction for a double ended queue along with the axioms. A double ended queue is a queue where items can be added to and remove from either end of the queue. I have ...
81 views

### Regular Expressions with at least 2 0's and at most 1

I think the answer should be: $(1+ \epsilon)000^* + 0^*0(1+\epsilon)00^* + 000^*(1+\epsilon)$ But I am not sure if this is the right answer. Can someone explain the correct answer? And if it is ...
93 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. ...
140 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 ...
80 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 ...
783 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: <...
25 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 ...
68 views

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 ...
49 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 ...
25 views

### Compute Lazily - Model checking

What is meant by lazily computing online? For example, in context of synthesis, that uses model checking. http://www.cs.colostate.edu/~france/CS614/Readings/Readings2011/Model-checking-Survey-a21-...
84 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 ...
222 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 ...
71 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 ...
90 views

85 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 [...
316 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 ...
249 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 ...
57 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... ...
180 views

440 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 ...
75 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. ...
279 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 ...
250 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 ...
105 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 ...
128 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 ...
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}$ ...