Questions tagged [formal-methods]
a particular kind of mathematically-based technique for the specification, development and verification of software and hardware systems.
38
questions with no upvoted or accepted answers
10
votes
0
answers
116
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 ...
- 237
9
votes
0
answers
178
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\}...
D.W.♦
- 159k
5
votes
0
answers
189
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
0
answers
98
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 ...
- 141
4
votes
0
answers
51
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
0
answers
192
views
Does this paper by Patrick Cousot describe an undecidable method for model checking?
All of the discussion is in the context of this paper.
I think that the whole procedure that the paper describes is not decidable, because if we can have an algorithm for it, then we can solve halting ...
- 31
3
votes
0
answers
27
views
Formal instruments to check properties of SQL queries
I have some operations defined as SQL queries which takes data from various tables combines it with the data from a base table and generates new rows, which are written back to the base table. In the ...
- 131
3
votes
0
answers
225
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.
...
- 3,752
3
votes
0
answers
107
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....
- 245
3
votes
0
answers
212
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 "...
- 257
2
votes
0
answers
54
views
Does Rice's theorem apply to sequential logic circuits?
I am wondering if Rice's theorem (or something similar to that) applies also to sequential circuits. I.e. given any finite sequential circuit, can there be an algorithm that can formally verify any ...
- 121
2
votes
0
answers
186
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, ...
- 29.8k
2
votes
0
answers
176
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 ...
- 1,234
2
votes
0
answers
38
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 ...
- 29.8k
2
votes
0
answers
156
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 ...
- 121
2
votes
0
answers
101
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 ...
- 21
1
vote
0
answers
58
views
How to convert wp equations into linear algebra equations?
I am reading this paper [1], wherein the authors first formulated a safety constraint in terms of wp equations. Then, they converted the equations into linear algebra form.
As per section 4.3, their ...
- 153
1
vote
0
answers
144
views
How to deal with missing variables when utilizing weakest precondition for verification?
I am reading the example given in [1], section 4.2. It deals with applying weakest precondition (wp) rules to ensure that the velocity of a car doesn't exceed a certain limit. We have the following ...
- 153
1
vote
0
answers
29
views
How do I prove relations of two CTL formulas?
If I have two CTL equations, how do I prove they're equivalent or that one implies the other?
What's the general approach? Disproving is obvious, but I am unable to figure out how to prove the ...
- 153
1
vote
0
answers
18
views
Rationale behind prefix-closure in CSP trace semantics
I'm currently studying Hoare's "Communicating Sequential Processes" (1) and I've come across a concept that I find a bit puzzling. In CSP trace semantics, a process's semantics are described ...
- 111
1
vote
0
answers
82
views
confusion with regard to constructive axiom
we say that a constructive axiom is an equality axiom $u = s$ :
whose left member $u$ is a pattern,
whose right member $s$ is any term whose variables are all appearing in $u$.
and yet we say of $...
- 33
1
vote
0
answers
48
views
What is known about the possibility of making a program to validate another program for correctness?
I'm having a question inspired by exercise 14 from section 1.2.1 of Donald Knuth's The Art of Computer Programming. It's phrased in the following way:
(R. W. Floyd) Prepare a computer program that ...
- 23
1
vote
0
answers
96
views
SMT validity solvers/ quantifier elimination in Ocaml
I am working on my own expression package in Ocaml and have to perform both validity queries and quantifier elimination. I have already implemented Cooper's procedure (for Presburger and Linear ...
- 113
1
vote
0
answers
49
views
Is assignment atomic in Promela?
Is assignment atomic is Promela? That is, can concurrent
x = value1;
and
x = value2;
produce anything different from value1 ...
user127009
1
vote
0
answers
55
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 ...
- 111
1
vote
0
answers
40
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:
...
- 2,223
1
vote
0
answers
64
views
How to Construct Kripke Structure States from Nested Functions
Say I have these defined functions:
...
- 2,223
1
vote
0
answers
66
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,632
1
vote
0
answers
86
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 ...
- 333
1
vote
0
answers
224
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,401
1
vote
0
answers
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 ...
- 135
1
vote
0
answers
584
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} \...
- 345
0
votes
0
answers
19
views
Evaluate under Hoare logic
Evaluate
WP(a = i + 2; i=i+1, ((a=6)^(i=5))
WP(x=x+1,y=y-1. (xxy>0))
wp(if x > 2 then y = 1 else y = -1,(x > 0))
wp(while n <> 0 do n:=n-1; n = 10)
wp(while n = 0 do n:=n-1; n=-10)
wp(...
0
votes
0
answers
47
views
Minimum DNF length of a conjuction of equivalences
Show that the formula $\bigcap_{i=1}^n (X_i \leftrightarrow Y_i)$ cannot have an equivalent disjunctive normal form with less than $2^n$ clauses.
I am puzzled on what approach to take -- whether to ...
- 109
0
votes
0
answers
54
views
Hoare Triple Logic
I'm having trouble understanding the logic behind Hoare Triples. The question asks for the missing value of the precondition {X}
...
0
votes
2
answers
90
views
Z-Specification = Routes
Im trying to make an invariant for this Z schema about routes.
1) The invariant should express that each route should contain at least 20 different places. First of all i thought of doing a universal ...
- 39
0
votes
0
answers
40
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 ...
- 101
0
votes
0
answers
18
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 ...
- 101