We’re rewarding the question askers & reputations are being recalculated! Read more.

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
44 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 ...
1
vote
0answers
51 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 ...
0
votes
0answers
10 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 ...
4
votes
1answer
72 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 ...
3
votes
1answer
28 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 ?
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
31 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
13 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 ...
1
vote
1answer
50 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 ...
2
votes
1answer
107 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 ...
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 ...
0
votes
0answers
32 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
1answer
38 views

Effective Procedures and P vs NP Problem

If, suppose, P doesn't equal NP. Implication of this statement is that there is no effective procedure to solve a hard problem; however there exists an acceptable solution S. I have following two ...
1
vote
2answers
112 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 ...
5
votes
1answer
113 views

The definition of weakest precondition for a non-deterministic language

In the classical IMP language, the definition of weakest precondition is: definition "wp c Q s ≡ ∃t. (c,s) ⇒ t ∧ Q t" This is stating that from state s, after ...
3
votes
1answer
136 views

The Law of Excluded Miracle in the language of guarded commands

The definition of weakest precondition is familiar (let me use Isabelle's syntax here): definition "wp c Q s ≡ ∃t. (c,s) ⇒ t ∧ Q t" the weakest precondition ...
2
votes
1answer
60 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\ ...
9
votes
0answers
99 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 ...
4
votes
1answer
119 views

Roadmap to formal verification

I would like to learn about different approaches to formal verification of software programs that goes beyond what Wikipedia has to offer. Ideally one would not only get an overview but also ...
2
votes
0answers
65 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. ...
4
votes
2answers
176 views

Is there a way to convert a program into a Boolean formula?

Let's say I have a program P, in form of a binary code for x86 architecture. I want to find a Boolean formula F (in form of CNF, or something like that), such ...
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
2answers
50 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 ...
3
votes
0answers
37 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
2answers
79 views

Why does the denotational semantics for a while loop have a existence quantifier?

I was going through these notes and they have the following operator on partial functions: $$ \mathcal F^{k}(\bot)(\sigma) = \left\{ \begin{array}{ll} \alpha( [\![s]\!]\sigma ) & [\![b]\!]\...
3
votes
1answer
159 views

Relating a proof to a Haskell program

I am trying to relate the following integer square root theorem $\forall x: \mathbb{N}, \exists y : \mathbb{N}((y^2 \leq x) \land (x < (y+1)^2))$ and its proof to its role as a specification of ...
2
votes
2answers
83 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 ...
0
votes
1answer
56 views

How to collect all states of a behavior in TLA+?

Description of the problem: I am modeling checking a distributed protocol against a global property with TLA+ developed by Leslie Lamport. The global property is defined on all states of a behavior (...
0
votes
1answer
47 views

How to solve for the precondition give a postcondtion that must satisfy two conditions

I tried solving past exam question but there is this one that I haven't been able to solve. The question states that a suitable precondition should be found for the statement. $$ a= i +2; i++\{(a = ...
0
votes
1answer
99 views

Topics from theoretical computer science suitable for a bachelor (undergrate) thesis? [closed]

Is the field of theoretical computer science so complex, that it is just "too much" for a bachelor thesis? Unfortunately I haven't found any old thesises because the relevant chair of the university ...
1
vote
1answer
56 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
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
2answers
749 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 ...
2
votes
2answers
74 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 ...
4
votes
1answer
253 views

How does TLC check liveness properties?

The paper "Model Checking TLA+ Specifications" published in 1999 explained how TLC (Temporal Logic Checker) checks safety properties written in TLA+ developed by Lamport. At that time, TLC did not yet ...
1
vote
0answers
42 views

How to Construct Kripke Structure States from Nested Functions

Say I have these defined functions: ...
3
votes
1answer
75 views

High-level requirements for a Proof of “Saving to the Database”

This question is about a few sentence description of what a proof would look like (and technologies / logics involved) for a complex api call through many layers. Trying to get a sense of the ...
1
vote
1answer
154 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\\ &\}\\...
0
votes
1answer
58 views

How to apply Operational Semantics to this function

Say I have a function like this: ...
2
votes
1answer
36 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
71 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 ...
5
votes
2answers
98 views

How does automated verification of systems with infinitely many states work?

I need some help with basic definitions and intuition to understand why and how it's possible to verify systems with infinitely many states. For example, if I consider an x86 computer, and assuming ...
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
141 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
109 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
112 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
145 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 ...