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

learn more… | top users | synonyms

1
vote
0answers
13 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 ...
0
votes
0answers
15 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 ...
0
votes
0answers
29 views

Complexity of choosing a suitable conjunctive 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 ...
0
votes
0answers
25 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 ...
1
vote
2answers
35 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 ...
2
votes
0answers
35 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 ...
0
votes
0answers
52 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 ...
2
votes
1answer
30 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 ...
3
votes
1answer
20 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 ...
1
vote
1answer
42 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 ...
3
votes
1answer
34 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 ...
-2
votes
1answer
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) → ...
2
votes
0answers
65 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 ...
2
votes
1answer
136 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 ...
-1
votes
1answer
130 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?
1
vote
1answer
94 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 ...
0
votes
2answers
54 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.
1
vote
1answer
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 ...
1
vote
1answer
80 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 ...
3
votes
1answer
90 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. ...
3
votes
2answers
115 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 ...
2
votes
2answers
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 ...
3
votes
3answers
764 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
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 ...
0
votes
1answer
68 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
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 ...
0
votes
1answer
25 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
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 ...
7
votes
5answers
212 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
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 ...
5
votes
0answers
90 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
584 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
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 ...
3
votes
1answer
59 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
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 ...
4
votes
1answer
315 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
234 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
56 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
180 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
327 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} ...
1
vote
1answer
416 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
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. ...
7
votes
2answers
275 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
249 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
104 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
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 ...
3
votes
1answer
130 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}$ ...
12
votes
4answers
800 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 ...
9
votes
2answers
2k 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
194 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,$ $$ ...