Questions tagged [formal-methods]

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

30 questions with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
10
votes
0answers
102 views

Can we say McCarthy and Hoare had the same objective in the 60s regarding a mathematical theory of computation?

I don't think there's any way to ask a very precise question here, so this might be considered opinion based. Nevertheless, it seems the question is clear enough because I'm asking whether these two ...
7
votes
0answers
122 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 \{0,1\}...
5
votes
0answers
147 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 ...
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 ...
3
votes
0answers
44 views

What is the difference between the choice operator and nondeterminism in CSP?

I'm learning CSP now for my research. First time doing formal work in CS. I'm having a hard time understanding the difference between choice $\square$ operator and the nondeterminism $\sqcap$ operator....
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 ...
2
votes
0answers
81 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
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, ...
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 ...
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
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 ...
1
vote
0answers
46 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
33 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
45 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
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 ...
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
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 ...
1
vote
0answers
439 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} \...
0
votes
0answers
20 views

Textbook for Hoare logic

I am looking to understand what Hoare logic is, and how it is used to prove program-correctness. I am interested in an applied text, which shows how to actually state formal specifications of programs,...
0
votes
0answers
23 views

How to generate tests using Model-Based Testing paradigm (for a newcomer)

So I just learned of Model-Based Testing. It sounds like this is a practical approach to some level of formal verification of production software applications. As I understand it, you have a ...
0
votes
0answers
17 views

Does formal specification of UX needs special language apart from the general specification languages?

I am fan of Alloy and CASL specification languages and my question is - what is the common practice regarding the formal methods in UX? Does UX require distinct specification languages? Generally one ...
0
votes
0answers
20 views

How to solve Hoare's problem when precondition contains meta symbols?

This is the proram for which I have to prove correctness using Hoare's Axioms: {X = |x|} if(x<=0) x:=-x; else skip; {X=x} This is my solution so ...
0
votes
0answers
35 views

Confusion regarding algebraic specification of the queue

I was given the following question in the test where I had to write the algebraic specification and its axioms based on below-defined operations: ...
0
votes
0answers
15 views

State-machine semantics of instruction set architectures

An instruction set architecture is an abstraction, a common interface layer between the software and the micro-architecture. The existence of this clearly delineated interface is becoming increasingly ...
0
votes
0answers
33 views

Formal language representation of program

I have numerous records, composed of words. Each word gets translated into vectors, with a variable number of channels, provided that that word exists in a specific lookup dictionary. For n number of ...
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 ...
-1
votes
0answers
25 views

From verification to program code

Suppose we have modeled the operational behavior as FSM, and properties as LTL or CTL, and we have used a model checking tool to confirm the fsm satisfies the LTL/CTl properties. What is the next ...