# Tag Info

Accepted

### Why is Proof Checker required in Proof Carrying Code

The purpose of the proof checker is to minimise the trusted computing base. By having a proof checker, neither the compiler nor the theorem prover need to be correct. The paper makes this point on ...
• 10.4k

### Formal semantics of OCaml in Coq

Have you seen Arthur Charguéraud's PhD thesis, Characteristic Formulae for Mechanized Program Verification? Rather than building the type system and small-step semantics as inductive relations, he ...
• 31.8k

### Why/when do we ever need transfinite loop variants?

You are correct when you observe that for any particular terminating loop $L$ we may simply define the invariant "we're getting one step closer to termination". But proving that this is indeed a valid ...
• 26.8k

### Why/when do we ever need transfinite loop variants?

I would like to add the following to Andrej's response (not enough rep for a comment). Indeed, we cannot avoid ordinals but we may hide them. One approach is to use some modal logic that takes ...

### Formal semantics of OCaml in Coq

You could be interested in Jacques Garrigue's A Certified Implementation of ML with Structural Polymorphism and Recursive Types, which establishes the soundness of static and dynamic semantics and ...
• 1,910
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 ...
• 13.3k

### Verified type checkers

Here are some results of a simple Google search: Certification of a Type Inference Tool for ML: Damas–Milner within Coq by Catherine Dubois and Valérie Ménissier-Morain Formalization of a Polymorphic ...
• 26.8k

### How to determine whether a proof requires "higher-order reasoning techniques"?

Briefly, every theorem stated in first-order logic has a first-order proof. In his book "An Introduction to Mathematical Logic and Type Theory", Peter B. Andrews develops both first-order logic and a ...
• 161
Accepted

### Complexity of a graph-rewriting problem

I don't know if it has been studied before, but after a quick look I think it should be PSPACE complete. We can build a reduction using the Nondeterministic Constraint Logic model of computation (NCL)...
• 22.3k

### 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 ...
• 13.3k
Accepted

### Proof that the theory of rationals is convex

The key idea here is that for any conjunction of equations $F\equiv u_1=v_1\wedge\ldots\wedge u_k=v_k$, the set $S_F$ is convex in the geometric sense, i.e. for any two points $p,q\in S_F$, all points ...
• 2,470
Accepted

### Is it possible to verify a typechecker for a total dependently-typed language in that language's logic?

As often in these matters, the encodings are important: you could have some silly encoding of Turing machines or Gallina terms or both where an input string $\langle n\rangle$ represents "the $n$-th ...
• 13.3k

### Type systems preventing laziness-related memory leaks?

Levy's call by push value calculus makes a distinction between values and their thunks. For a value v of type ty the ...
Accepted

### Practical example: how to formally verify "file name" implementation from a spec?

In general, the technique used is known as "fuzzing". Not all errors are equally likely. Let's consider two hypothetical errors: System A incorrectly rejects a filename if it contains an ...
• 334

### Why/when do we ever need transfinite loop variants?

If I may add something, too, I'd suggest that some of the ways ordinals are presented tend to make them sound more 'suspicious' than they actually are. At least, I think there are other ways of ...
• 670
Accepted

### State of the Art for the Monadic Class?

I found signs that such a decision procedure was implemented in the (general purpose) theorem prover SPASS. In particular see the thesis of Ann-Christin Knoll, On Resolution Decision Procedures for ...
• 13.3k

### 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 ...
• 7,757

### State of the Art for the Monadic Class?

In a 1993 LICS paper, Bachmair, Ganzinger and Waldmann showed that set constraints are equivalent to monadic FOL, in Set Constraints are the Monadic Class. If memory serves, set constraints are ...
• 31.8k

### What is the proper role of verification in quantum sampling, simulation, and extended-Church-Turing (E-C-T) testing?

The gist of the question is, given that quantum probability is a source of true randomness, how does that effect the extended (or efficient, or polynomial-time) Church-Turing thesis? The answer is ...

### Practical example: how to formally verify "file name" implementation from a spec?

For the concrete case of a specification of a regular language, there is the Java String Analyzer which roughly is able to compute a finite state automaton (i.e. regular expression) of the set of ...
• 393
Accepted

### Regular safety properties and bad prefixes of $\omega$-regular properties

Your construction for bad prefixes is not correct on NBA's. For instance take the NBA on alphabet $A=\{a,b\}$ with two initial states $q_a$ and $q_b$ where for both $x\in A$, $q_x$ goes to an ...
• 7,757
1 vote

### Confusions about the technique for verifying implementations of linearizable objects in [Herlihy and Wing, 1990]

Herlihy and Wing write on p. 477: In conclusion, the rep invariant $\mathbf{I}$ must be continually satisfied and the abstraction function continually defined, not only between abstract operations,...
• 800
1 vote

The powerful formalism you are looking for cannot exist, for otherwise we could solve the halting problem. Here is the sketch of an argument why. Consider Hoare triples $\{A\} P \{B\}$ for partial ...