Questions tagged [formal-methods]

The tag has no usage guidance.

11 questions with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
13
votes
0answers
267 views

Algebraic topology for termination proofs

I'm reading about various ways in which termination proofs of software verifiers are built: ad-hoc methods that detect recursions, term-rewriting, synthesis of lexicographic orderings... From the ad-...
5
votes
1answer
84 views

SMT solving with less-than theory and monotonic functions

I am attempting to solve a less-than theory within an SMT paradigm that involves variables assigned to reals and assumes that all the functions used in the theory are monotonic. The theory's signature ...
2
votes
0answers
62 views

applications of institution-independent model theory

To quote wikipedia, The notion of institution has been created by Joseph Goguen and Rod Burstall in the late 1970s in order to deal with the "population explosion among the logical systems used in ...
1
vote
0answers
43 views

How to justify this causally consistent execution in the $(vis, ar)$ framework for distributed consistency models?

In Figure 5.1 of the book "Principles of Eventual Consistency" by Sebastin Burckhardt, 2014, Causal Consistency (CC); wiki is (mainly) defined as the conjunction of $hb \subseteq vis$ and $hb \...
1
vote
0answers
60 views

Confusion about the visibility and arbitration relations in a formal framework for distributed consistency models

In the POPL'14 paper "Replicated Data Types: Specification, Verification, Optimality" and the book "Principles of Eventual Consistency", the authors propose a formal framework for specifying ...
1
vote
0answers
126 views

Have there been any practical applications of domain theory to formal methods?

By Domain Theory, I mean the use of CPOs (or related topological/order-theoretic structures) to study the denotational semantics of programming languages. Compared to the two other common approaches ...
1
vote
0answers
53 views

what is the meaning of “indicate substitution by priming metavariables”

This is a question about the usage of "indicate substitution by priming metavariables". For example, in the separation logic(it is not important whether familiar to this logic), I can understand the ...
0
votes
0answers
167 views

Theoretical background of Classes and Objects

I would like to learn about the possible ways of formalizing Classes and Objects (in programing languages like java) using formal languages. Where should I start? This might be related to my previous ...
0
votes
0answers
58 views

Specification language for specifying both Objects and Primitive data types

I am looking for an specification language, which supports both primitive data types and objects. I already know about Object-Z. But I am wondering if there is any other Specification language that I ...
0
votes
0answers
207 views

formal definition of “flowcharts”

I am looking for a formal definition of so-called "flowcharts" used as representation of programs or business processes. Is there some good one around ? Thx JCLL
-1
votes
1answer
55 views

semantics of “destroy object” in HRU model

In the access control model HRU there is the primitive request destroy object o which is only defined if o is an object in the current protection state which is not a subject. I am interested in why ...