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
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 ...
3
votes
1answer
57 views

Weak bisimulation up-to $\approx$

Given this definition of weak bisimilarity: A configuration relation $\mathcal{R}$ is a weak bisimulation provided that whenever $P\ \mathcal{R}\ Q$ and $\alpha$ is $\mu$ or $\tau$ action then: $...
2
votes
0answers
159 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
122 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, ...
3
votes
1answer
130 views

Minimal Deterministic Buchi Automata Product

Problem: Let $\varphi = \varphi_1 \land \varphi_2$ be Deterministic Buchi Automata (DBA) expressible LTL formulas. Let $A$, $A_1$ and $A_2$ be translated DBAs such that ${\cal{L}}(A) = {\cal{L}}(A_1)...
0
votes
0answers
17 views

What is the name for the theory that guarantees proof for negative and not for all possible positives

I have heard of some people mentioning the general rule that says that you can only ever guarantee that a program will not capture the negative cases but you can never guarantee that it captures all ...
2
votes
0answers
150 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 ...
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 ...
5
votes
3answers
215 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 ...
2
votes
1answer
39 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, ...
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 ...
3
votes
0answers
78 views

In ontology development, where do axioms come from?

I am developing an ontology. I've got the classes, relationships and I guess I could come up with instances at this point too. But what I'm really focused on is the axioms. I've learnt that the ...
17
votes
2answers
2k views

Program Correctness, The specification

From Wikipedia: In theoretical computer science, correctness of an algorithm is asserted when it is said that the algorithm is correct with respect to a specification. But the problem is that to get ...
9
votes
2answers
423 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 ...
5
votes
1answer
70 views

Efficient Algorithm Linear Temporal Logic to Deterministic Rabin Automata

I am trying to construct an equivalent Deterministic Rabin Automata (DRA) given a Linear Temporal Logic (LTL) Formula. One (expensive) way to do this would be to construct an equivalent Non-...
3
votes
1answer
355 views

What does “AF AX p” mean in CTL?

Both Logic in Computer Science (Huth and Ryan, 2004) and Branching vs. Linear Time: Final Showdown (Vardi, 2002), state something to this effect (paraphrased): In LTL, X F p and F X p are ...
4
votes
0answers
46 views

How the $EX(f)$ is evaluated in symbolic model checking?

I was reading the symbolic model checking, So there it has mentioned that we can represent the set of states and transition relations of any transition system with the help of ROBDDs. I was trying to ...
1
vote
0answers
60 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 ...
9
votes
3answers
904 views

Why does the state remain unchanged in the small-step operational semantics of a while loop?

Usually I see that in the structural operational semantics representation for the while loop, the program state don't change: $(while \> B \> do \>S, \sigma) \rightarrow (if \>B \> ...
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})$?
6
votes
1answer
322 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,$ $$ \begin{array}...
70
votes
2answers
8k 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. But ...
1
vote
1answer
187 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
1answer
179 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. ...
6
votes
1answer
113 views

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

Background: In the book of Principles of Model Checking (Christel Baier and Joost-Peter Katoen, MIT Press, 2007), Section 9.2, page 701, the semantics of the until modality is defined over some time-...
18
votes
2answers
3k views

What is this fraction-like “discrete mathematics”–style notation used for formal rules?

In the paper "A Conflict-Free Replicated JSON Datatype", I encountered this notation for formally defining "rules": What is this notation called? How do I read it? For example: the ...
2
votes
1answer
50 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 ...
1
vote
0answers
52 views

How to prevent the change of other objects in Z specification?

I have Z specification of Banking system, whose fragments are: and I think that the specification is OK, but my professor says that this specifiction is completely wrong, because AddAccount ...
1
vote
2answers
141 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?
3
votes
1answer
385 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
82 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. ...
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 ...
2
votes
0answers
147 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
1answer
111 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
60 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
62 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
136 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
98 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
1answer
367 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
vote
1answer
3k 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?
0
votes
2answers
933 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
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
1answer
628 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 ...
6
votes
2answers
1k 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
0answers
88 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 ...
2
votes
2answers
299 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
2k 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
27 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
85 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 ...