Skip to main content
8 votes

Ways to think formally about Satisfiability Modulo Theories

It's actually surprisingly hard to relate SMT to type-theoretic/categorical approaches to logic -- the results in this area are very recent! This is because categorical logic is primarily conceived of ...
Neel Krishnaswami's user avatar
6 votes
Accepted

Formalization of matching logic (logic behind K Framework)

There is a number of formalizations of matching logic in various proof assistants. I am a co-author of the first one in the following list; thus I have more insight into that one. I am not aware of ...
Jan Tušil's user avatar
6 votes
Accepted

Defining finite sets inductively in a proof assistant?

There are many variants of finite sets in constructive mathematics. One that can be defined using just inductive definitions, and is therefore amenable to formalization in type theory, is the ...
Andrej Bauer's user avatar
  • 29.3k
6 votes
Accepted

Lee's algorithm for synthesis of ranking functions in size-change termination proofs

The complexity is acceptable in current verifiers, and has been implemented in at least the AProVE termination analysis tool for term rewrite systems. They describe their implementation in Lazy ...
cody's user avatar
  • 14k
4 votes
Accepted

Ordering sequences containing bitvectors for size-change termination

Surely, you want $s_1 < s_2$ if there is a $t$ such that $s_1.t < s_2.t$ and $s_1.u \leq s_2.u$ for every other field $u$. That, at least, gives you a well-founded order. But there are many ...
cody's user avatar
  • 14k
3 votes
Accepted

What is region construction in timed automata?

It's not exactly about obtaining an "equivalent" DFA, but rather an NFA that has an equivalent reachability problem. The main idea is to consider what information you actually need to know ...
Shaull's user avatar
  • 5,656
3 votes
Accepted

Algebraic topology for termination proofs

As someone somewhat familiar with termination analysis, I'd say that the techniques are only as ad-hoc as the programs they aim to prove termination of, which is to say very ad-hoc indeed. The crucial ...
cody's user avatar
  • 14k
3 votes
Accepted

Difference between CTMC, DTMC, and MDP

The "probabilistic" element in probabilistic model checking is that the system being checked is probabilistic, not that we add probabilities to an existing deterministic or non-deterministic system. ...
Shaull's user avatar
  • 5,656
2 votes

How are safety/liveness languages defined on the set of finite or infinite words?

The answer is yes to all questions, so it is enough to answer 2 and 4, as the definitions work in particular for languages of finite words: A language $P\subseteq \Sigma^*\cup\Sigma^\omega$ is safety ...
Denis's user avatar
  • 8,903
2 votes

Confusion about a formal definition of PRAM consistency

When they define PRAM (page 11 of the arxiv preprint) they actually state that vis is a partial order (in particular, transitive): We define PRAM consistency by requiring the visibility partial ...
Bjørn Kjos-Hanssen's user avatar
2 votes

Running an algorithm for fixed amount of time on RAM model machine

One approach is to implement an interpreter for the RAM model, and then instrument the interpreter with a counter that keeps track of the number of instructions executed. I suspect it should be ...
D.W.'s user avatar
  • 12.3k
2 votes
Accepted

What is "structural model checking"?

I hadn't seen that term before either. In essence it seems to mean a model checking algorithm taking a program $P$ (with its syntactic structure) and a property that exploits $P$'s structure in the ...
Kai's user avatar
  • 854
2 votes

Operational semantics and denotational semantics and describing the behaviour and structure of programs

I am going to attempt an answer, or more precisely a clarification, but one should keep in mind that most ingredients of the question (semantics, operational, behavior, structure) do not have a clear ...
Beniamino Accattoli's user avatar
2 votes

State machine classes with sub-exponentially growing model spaces

I believe that there are no reasonable model where the number of machines grow subexponentially, in the sense that either such a model would be remarkably not expressive, or would require huge ...
Rémi's user avatar
  • 262
1 vote

Formalization of matching logic (logic behind K Framework)

I'm currently at the end of my PhD thesis about the interoperability of semantics. That's the reason I'm studying the translation from the semantical framework K into the logical framework Dedukti. ...
Amélie Ledein's user avatar
1 vote

Equivalence of finitary and infinitary semantics of concurrent programs

For such $P_i$ we have that $\mathcal{R}(P_i)$ is the limit-closure of $\mathcal{F}(P_i)$. That the $P_i$ in general need to be finitely-branching for this claim is due to the fact that infinite ...
Kai's user avatar
  • 854
1 vote

Proper terminology for input, parameter or variable fixing. Refinement? Projection? Fixation? Partial valuation?

"Fixing" inputs or parameters to specific values can be a valid approach, but it may not be the most appropriate term to use depending on the context. "Refining" a specification ...
Likar's user avatar
  • 11
1 vote

A possible error in the semantic chapter of the ISO standard for the Z specification notation

Firstly, in addition to the Standard from 2002, there is also Technical Corrigendum 1 (TC1) from 2007 which fixes a number of issues. I don't know of any combined document. Both documents are ...
Phil Clayton's user avatar
1 vote

Looking for an online community specializing in the Z specification language, where I can ask questions

There is the comp.specification.z newsgroup, available on Google Groups. There are some mailing lists: ZFORUM mailing list Zed Freelists mailing list Additionally, there are mailing lists for tools ...
Phil Clayton's user avatar
1 vote

SMT solving with less-than theory and monotonic functions

I can think of 2 straight forward approaches Directly add $\forall xy (x < y \Rightarrow f(x) < f(y))$. Or Akcermannize the problem and add these as axioms for all pairs of terms.
Mikolas's user avatar
  • 1,322

Only top scored, non community-wiki answers of a minimum length are eligible