# Tagged Questions

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

28 views

### Formal method - how to prevent deletion in an array

i have created a very basic model of an array list in the b method as shown below ...
88 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 ...
51 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

### 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 ...
29 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 ...
19 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 ...
41 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 ...
29 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 ...
36 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) → ...
126 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 ...
61 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 ...
116 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?
49 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.
51 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 ...
77 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 ...
89 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. ...
109 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 ...
63 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 ...
77 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 ...
743 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: ...
24 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 ...
24 views

### Compute Lazily - Model checking

What is meant by lazily computing online? For example, in context of synthesis, that uses model checking. ...
81 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 ...
205 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 ...
70 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

82 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 ...
312 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 ...
208 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 ...
55 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... ...
179 views

2k 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 ...
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. ...