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
2
votes
2answers
75 views

What exactly state is in Model Checking

So I finally realized the difference between transition systems and automata, and now am closer to understanding Model Checking. One of the last pieces is understanding what exactly "state" is in ...
2
votes
1answer
921 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 ...
2
votes
2answers
86 views

How to express the existence of winning strategy of the starter of a game in temporal logic?

Consider a two-player game. A winning strategy of a player is a strategy following which the player can always beat his opponent, no matter how his opponent responds. A game can be unfolded to a ...
2
votes
1answer
49 views

Where in the toolchain does formal specification come in?

Where is the formal spec located? Like this? Are tests made from formal or informal spec? I saw a project where they where generated from a the formal spec and that never made sense to me. Is the ...
2
votes
1answer
75 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. ...
2
votes
2answers
296 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 ...
2
votes
1answer
114 views

Hoare logic, proving conjunction rule from basic rules, possible or not?

(This is HW.) Suppose I have these following proof rules given. I am currently considering if I can prove the conjunction rule (given below) from the above given Hoare logic rules. My answer would ...
2
votes
2answers
52 views

(Generally) How to specify asynchronous action with side effects using logic equations

Say you have this function call sequence: function all() { fn1() fn2() fn3() } And say that fn2 was asynchronous and ...
2
votes
1answer
38 views

Cut costly functions in inter-procedural abstract interpretation

I am performing some inter-procedural abstract interpretation to capture certain program properties. Following the standard way, what I am doing is to maintain a work list of to-be-analyzed functions, ...
2
votes
1answer
59 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 ...
2
votes
2answers
45 views

Modeling a set of probabilistic concurrent processes

I'm looking into discrete-time Markov chains (DTMCs) for use in analyzing a probabilistic consensus protocol. One basic thing I haven't been able to figure out is how to model a set of independent ...
2
votes
1answer
37 views

Any mathematical tools for analyzing mutable memory

Wondering if there are any documents, theories, or methodologies for dealing with mutable memory mathematically. Basically a formal algebraic model of how computers manipulate memory. Along the lines ...
2
votes
1answer
108 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 ...
2
votes
1answer
365 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 ...
2
votes
1answer
61 views

How to prove a LTL formula correct in a specific model?

I have been learning Verification by model checking recently and I get the following question: $Whether\ the\ LTL\ formula\ M, q_3\ \models (X\ \lnot a) \rightarrow (F\ G\ \lnot a)\ is\ established\ ...
2
votes
1answer
74 views

Single Input Single Output Sequential Circuit Explanation Required

I'm a student of Formal Methods in Software Engineering, I'm trying to study this question for two days but still haven't figured it out, I couldn't even find a similar solution or explanation, so ...
2
votes
0answers
68 views

Relation between “formal verification”, “formal proof”, and “type systems” for software verification?

I have a vague understanding what formal verification is about, a vague understanding of what the cutting edge is of type theory for programming languages, and a better understanding of formal proofs. ...
2
votes
0answers
146 views

Most efficient unification algorithm?

I've been trying to find the most efficient unification algorithm by following reference chains on the Wikipedia article on unification. As far as I can tell, the fastest one is the one presented in "...
2
votes
0answers
112 views

Passing arrays vs functions as arguments in SMT?

In SAT Modulo Theories (SMT), with the theory of uninterpreted functions, all functions are first order, that is, they don't take functions as arguments or return functions. In the theory of arrays, ...
2
votes
0answers
146 views

Novel escape analysis algorithm for Java

Today I read a very interesting article about escape analysis in Java called Escape Analysis for Object Oriented Languages: Application to Java I think I have some grasp on how escape analysis works ...
2
votes
0answers
32 views

State-of-the-art for Set Constraints?

I've recently stumbled across the field of Set constraints for program analysis, that is, solving equations of the form $exp_1 \subseteq exp_2$, where (depending on the particular variant of the ...
2
votes
0answers
135 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 ...
2
votes
0answers
87 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 ...
1
vote
2answers
820 views

An example of something you can formally verify with proofs in Software Development

I have been working on understanding formal verification of software. Formal methods include things like modeling your software with Petri Nets, Automata, or State-Transition Graphs. Other techniques ...
1
vote
1answer
2k 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
2answers
52 views

How can MLTT etc encode computability?

I am recently thinking about proving the undecidability of some problem. This problem has been formalized in Coq and by staring at it, people including me think "for sure" this is undecidable. "For ...
1
vote
1answer
186 views

Using B-method, and formal methods in general, to model and verify a reverse linked list

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 ...
1
vote
3answers
211 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
1answer
52 views

Are the two LTL properties $GF(\psi_1 \land F\psi_2 )$ and $GF(\psi_2 \land F\psi_1 )$ equivalent?

Is $GF(\psi_1 \land F\psi_2 )$ equivalent to the property $GF(\psi_2 \land F\psi_1 )$? Attempt: In the first property each state must eventually see $\psi_1$ and $\psi_2$, in the second property as ...
1
vote
2answers
113 views

Buchi automata in formal software verification

As I am studying the application of Buchi automata in formal software verification, I am interested in the computational complexity (or links to papers) for the algorithms used to solve the problem in ...
1
vote
1answer
30 views

Define a length function over $A^{*} \leftarrow{N}$ such that $length(l)$ outputs the length of $l$

Consider the following definitions LIST: $\overline{nil} \ \ \ \ \ \frac{l}{a \ l}$ $a \in A$ $A^* = \mu \widehat{LIST}, \ A^{\infty} = v \widehat{LIST}$ NAT: $\overline{0} \ \ \ \ \ \frac{x}{s(...
1
vote
1answer
57 views

Software code generation from the (operational) semantics - reference request for automatic programming

Are there research trends that try to research code generation directly from the (operational or some other kind of) semantics? One can imagine cognitive architecture that discovers and reasons about ...
1
vote
1answer
176 views

How to verify a property about a certain order of events in TCTL / UPPAAL?

I'd like to check if a certain order of events happens if another property holds true using UPPAAL and TCTL. ...
1
vote
2answers
132 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?
1
vote
1answer
586 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 ...
1
vote
1answer
81 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 ...
1
vote
1answer
115 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 [...
1
vote
1answer
173 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
1answer
168 views

How to use Hoare Logic to Prove this Assertion

Given this assertion in Hoare Logic: \begin{align} &\mathbf{\{p >= 0\}}\\ &s = 0 ; n = 1 ;\\ &\mathtt{while}\ (n <= p)\ \{\\ &\quad s = s + n ;\\ &\quad n = n + 1\\ &\}\\...
1
vote
2answers
60 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 ...
1
vote
1answer
60 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 "...
1
vote
1answer
72 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
0answers
52 views

How are safety/liveness languages defined on the set of finite or infinite words? [closed]

Let $Σ$ be an alphabet (e.g., the powerset of atomic propositions coming from some Kripke structure, though such details are irrelevant here). For infinite words, a language $P\subseteq Σ^ω$ is ...
1
vote
0answers
45 views

Prove that set of operations form a commutative Monoid

this is my first post on this exchange. I am looking for some help with defining a proof that a set of operations I have designed forms a commutative monoid. (Disclaimer: I am not sure that I have ...
1
vote
0answers
32 views

How Model Checking works with User Interaction

In order to understand how to apply Model Checking, I am wondering how to apply it to a pseudo-realistic async program. Say I have the following pseudocode: ...
1
vote
0answers
44 views

How to Construct Kripke Structure States from Nested Functions

Say I have these defined functions: ...
1
vote
0answers
58 views

Determining when equal 2CNF has pure literal

Let us assume that we have a 2CNF $\varphi(X,y)$. Then we want to see if there is equal formula where $y$ (or $\overline y$) is pure literal. Can this be done in polynomial time? Are there some ...
1
vote
1answer
90 views

Formal specification; Logical formula

* Initial Question * I'm trying to write a logical formula consists of three Boolean variable C1, C2, C3. My program takes graph as input and checks properties about them. C1 represents presence of ...
1
vote
0answers
59 views

Operational Semantics - Include SKIP, SEQUENCE and IF?

I'm writing a paper for a programming languages workshop in which I have to describe the semantics of a new optimization for Java using Operational Semantics, small step style. I have never used ...
1
vote
0answers
32 views

How to prove that $\lfloor{\sqrt{n}\rfloor} = \Theta(\sqrt{n})$? [duplicate]

It is quite direct to prove that $\lfloor{\sqrt{n}\rfloor} = O(\sqrt{n})$. But how can I prove that $\lfloor{\sqrt{n}\rfloor} = \Omega(\sqrt{n})$?