Skip to main content

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
0 votes
1 answer
20 views

Z vs B-method vs VDM?

What are the differences between these formal methods? Is one objectively better than the others or do they all have pros and cons?
UNRESTR1CTED's user avatar
0 votes
1 answer
78 views

NFA for a regular expression without $\epsilon$-transitions

I think I know how to convert a regular expression to NFA without requiring epsilon transitions, but I'm not sure if I'm right (I'm just using common sense to be honest, no particular algorithm in my ...
Acad's user avatar
  • 101
1 vote
0 answers
60 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 ...
desert_ranger's user avatar
3 votes
1 answer
407 views

What is special about a canonical representation of Boolean functions?

My textbook (Saurabh's Introduction to VLSI Design Flow) mentions while discussing formal verification that a representation of a Boolean function is said to be canonical if the following holds: If a ...
EE18's user avatar
  • 133
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 ...
desert_ranger's user avatar
3 votes
1 answer
177 views

How did this work apply weakest precondition rule on their example car problem?

While reading the example given in [1]., I couldn't understand how the authors set up the logic to compute the weakest preconditions (wp) in their car example in section 4.2. The dynamics of the ...
desert_ranger's user avatar
1 vote
0 answers
38 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 ...
JobHunter69's user avatar
0 votes
0 answers
20 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(...
Salma muhammad's user avatar
1 vote
1 answer
118 views

Abstract Interpretation: prove that the sign subtraction is increasing in each of its parameters

I need to prove that the binary operator $-_\pm: \mathbb{P}^\pm\times\mathbb{P}^\pm\rightarrow\mathbb{P}^\pm$ is increasing in each of its arguments, where $$ \mathbb{P}^\pm = \{\top_\pm, \leq0,\...
Kiuhnm's user avatar
  • 141
1 vote
0 answers
24 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 ...
nasosev's user avatar
  • 111
0 votes
1 answer
118 views

How to start with verifying a formal proof programmatically?

I heard the terms "theorem provers" and "proof assistants" tossed around before (which I assumed to be the same up until a couple seconds ago), and also of Coq, Idris, Agda, TLA+ (...
toraritte's user avatar
  • 105
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 ...
Senmorta's user avatar
1 vote
1 answer
60 views

0<i => 0 < i + j proof?

If we have the natural numbers defined as: Plus the following: $pred \space \_\_<\_\_ \space: Nat \times Nat$ $\forall i,j:Nat$ $0<suc(j)$ $\neg(i<0)$ $suc(i) < suc(j) \...
V_head's user avatar
  • 33
0 votes
1 answer
4k views

MergeSort's merge function loop invariant

I am reading a proof of correctness for the MergeSort Algorithm. This is the code for the MergeSort and the Merge function: The correctness of the MergeSort function is easy to prove since the two <...
mateleco's user avatar
  • 108
0 votes
0 answers
53 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 ...
DesmondMiles's user avatar
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 $...
V_head's user avatar
  • 33
1 vote
2 answers
72 views

"Largest set" in coinductive definitions

In several explanations of coinductive definitions (for example, in the answers to What is coinduction?), we're told that while an inductive definition gives us the smallest set with a specified set ...
N. Virgo's user avatar
  • 976
0 votes
2 answers
100 views

What is the difference between type inhabitant and subtyping?

I am confused with the terms inhabitant vs. subtyping. For example, We usually think that "john is an inhabitant of Human". This sentence is correct, because john is an individual, and an ...
chansey's user avatar
  • 295
1 vote
1 answer
61 views

Are there invariants in text processing problems?

I have read that when programming it is good to identify relations -- invariants -- that should hold true throughout the program, and it is good to insert assertions throughout the code to check that ...
Roger Costello's user avatar
1 vote
1 answer
124 views

Proving a predicate assignment is correct

I am currently reading Formal Methods - An Appetizer and am stuck in chapter 3 (Program Verification). I am unfamiliar with logic and I do not think I understand the $\vDash$ notation correctly. I ...
user avatar
1 vote
0 answers
55 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 ...
Rusurano's user avatar
3 votes
1 answer
96 views

Abstract Interpretation: Connection between soundness relation and a Galois connection

I am currently studying the paper "Abstract Interpretation Frameworks" by Cousot and Cousot from 1992 (https://doi.org/10.1093/logcom/2.4.511) to gain an understanding of the theory behind ...
cherrywoods's user avatar
1 vote
1 answer
100 views

Logic foundation for formal verification

What types of logic should one study as foundation before diving into the area of software verification? What I can think of are: Hoare Logic (for proving correctness of imperative programs) Linear ...
a_fan's user avatar
  • 111
1 vote
0 answers
100 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 ...
Theo Deep's user avatar
  • 113
1 vote
1 answer
60 views

How are pointers interpreted differently to variables in a control flow graph (CFG)?

I have been working with control flow graphs and believe I understand how they function when describing dependencies between variables. For example, given the operations: ...
John Harrington's user avatar
3 votes
0 answers
28 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 ...
Radu Dumbrăveanu's user avatar
1 vote
0 answers
55 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 ...
user avatar
0 votes
0 answers
60 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} ...
Redone123's user avatar
2 votes
1 answer
171 views

Why sequential consistency model is widely used if it is unsound

From this talk and these lecture notes here and here I learned that sequential consistency does not actually model what really happens in practice. However, it is also pointed out that most of the ...
Barte's user avatar
  • 503
2 votes
1 answer
85 views

Is a system of equations derived from mutually recursive ADTs always uniquely solvable?

After looking at Can a computer determine whether a mathematical statement is true or not? for a while, I worry we may be into incompleteness/halting problem territory with this question, so an answer ...
D. Ben Knoble's user avatar
1 vote
2 answers
180 views

Z Notation: sequence of sequences - find sum

Let me just say that this is for a university project. I do not expect an answer but more of a "hint". I have a schema of a Supermarket that holds a sequence of queues: ...
tdranv's user avatar
  • 111
1 vote
1 answer
52 views

Where should "imply" be placed in this formalisation?

I have to formalize the following sentence: If any house is green then there exists a horse that is white. I have formalized it the following way: $$\forall(x)(\mathit{house}(x)\rightarrow \mathit{...
Wolfuryo's user avatar
  • 125
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 ...
Grisu47's user avatar
  • 121
1 vote
2 answers
132 views

Interpreting a proof of $2^\mathbb{N}$ being uncountable

Suppose I have the following proof: ...
0xd34df00d's user avatar
6 votes
2 answers
1k views

A general picture of formal verification in software

I'm trying to piece together a general picture of the state of formal software verification, and I'm having a good bit of trouble. For context, I come from mostly a math background. I'm quite familiar ...
Physical Mathematics's user avatar
3 votes
1 answer
82 views

How to prove that replacing a character in a string in both C and JavaScript is equivalent?

I would like to try some different proofs, specifically in proving equivalence of the implementation of some feature in two different programming languages (C and JS in this question). This is about ...
Lance's user avatar
  • 2,265
1 vote
3 answers
135 views

is (infinitely often p) ∨ (infinitely often ¬p) valid?

i'm trying to prove every trace over PROP = {p} is a model of the formula. I am very stuck in figuring out a model pi that satisfies this formula, can anyone point me in the right direction?
Jim's user avatar
  • 39
0 votes
2 answers
96 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 ...
Jim's user avatar
  • 39
1 vote
1 answer
202 views

LTL Model of (infinitely often p) ∧ ( infinitely often q) ∧ (¬ Eventually (p ∧ q))?

Can anyone give a model of the following LTL formula? $$ \Box\Diamond p \land \Box\Diamond q \land \lnot \Diamond (p \land q). $$ That is, we want each of $p$ and $q$ to hold infinitely often, but $p \...
Jim's user avatar
  • 39
5 votes
2 answers
227 views

proving program equivalence

I understand that the general problem of program equivalence is undecidable, but I'm wondering what approaches exist to tackle the problem? I am familiar with Hoare-style verification, but are there ...
user120913's user avatar
39 votes
5 answers
6k views

Do theorem provers demonstrate their own correctness?

I am not very well-versed in the world of theorem proving, much less automated theorem proving, so please correct me if anything I say or assume in my question is wrong. Basically, my question is: are ...
J. Auon's user avatar
  • 503
2 votes
2 answers
69 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 ...
ahelwer's user avatar
  • 209
0 votes
1 answer
28 views

What's the meaning of this service specification

What's the meaning of the example statement here? "A service specification S describes an interface: it specifies the behavior of certain program elements (functions or subprograms) through ...
Hemaolle's user avatar
  • 103
5 votes
1 answer
196 views

Proving with co-induction principles

I'm going through Adam Chlipala's "Certified Programming with Dependent Types" (available here for convenience), and I'm a bit stuck at internalizing the introduction of co-induction principle for the ...
0xd34df00d's user avatar
3 votes
1 answer
63 views

Having a formal ISA specification - What does correctness mean?

Does this always mean that a program can be correct in regard to that spec or is there any correctness of the spec itself ?
Malte's user avatar
  • 31
1 vote
1 answer
70 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 ...
kauray's user avatar
  • 519
3 votes
1 answer
613 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 ...
runeblaze's user avatar
  • 189
2 votes
2 answers
66 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 ...
Lance's user avatar
  • 2,265
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 ...
goral's user avatar
  • 111
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 ...
Stumbler's user avatar
  • 101