Stack Exchange Network

Stack Exchange network consists of 174 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange
Join us in building a kind, collaborative learning community via our updated Code of Conduct.

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

0
votes
1answer
21 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
18 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
41 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
39 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
27 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: ...
0
votes
2answers
88 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 ...
0
votes
0answers
14 views

How to combine Symbolic Model Checking with Symbolic Execution

I have started reading some textbooks and papers on Model Checking, and have run into the closely related but different Symbolic Execution. I have a few open questions on StackOverflow about the "...
2
votes
1answer
39 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
61 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
20 views
3
votes
1answer
56 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
16 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
49 views
2
votes
1answer
28 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 ...
1
vote
1answer
44 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
90 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
49 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: $...
1
vote
0answers
56 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 "...
3
votes
0answers
43 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
1answer
41 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
93 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 ...
3
votes
0answers
30 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 ...
0
votes
0answers
8 views

Max End Component equivalent for continuous-state MDPs

Do we have anything equivalent in continuous-state MDPs for Max End Components?
1
vote
0answers
30 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
24 views

Problem with definition of bisimularity

In my model checking class we have defined a bisimulation like this: Let $K=(S,S_0,Act,R,L)$ and $K'=(S',S'_0,Act,R',L')$ be two kripke structures. A relation $B \subseteq S \times S'$ is called ...
3
votes
1answer
35 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
77 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 ...
4
votes
0answers
71 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 ...
16
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 ...
5
votes
1answer
53 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
177 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
42 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
46 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
854 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})$?
1
vote
1answer
112 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. ...
17
votes
2answers
1k 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
44 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
37 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
94 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?
2
votes
1answer
53 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
55 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
90 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 ...
1
vote
1answer
153 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 ...
2
votes
1answer
71 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 ...
3
votes
1answer
52 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
59 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
86 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
65 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) → <>[]...