15

You might want to check out Liquid Haskell, which allow working with type refinements rather than dependent types. Type refinements can be seen as a restricted logical language that allow you to express Hoare-style properties of the inhabitants of various datatypes. Another possible candidate is the $F^*$ language, which offers similar constructs. There ...


13

Honda and Yoshida's A Compositional Program Logic for Polymorphic Higher-Order Functions (probably) pioneered Hoare logics for purely functional languages. This work is based on Hennessy-Milner logic and Milner's encoding of functions into processes, as described here: From Process Logic to Program Logic The work by Régis-Gianas et al mentioned in ...


11

See also Yann Régis-Gianas PhD thesis work with François Pottier: A Hoare Logic for Call-by-Value Functional Programs (MPC'08). This work was extended to cover the usual ML side-effects by Johannes Kanig and Jean-Cristophe Filliatre in 2009: Who: A Verifier for Effectful Higher-order Programs.


9

Amal Ahmed's very readable thesis dissertation could be a nice start.


8

There is a paper in this year's ICFP, refinement types for Haskell. The paper deals with termination checking rather than full Hoare logic, but hopefully that's a start in this direction. The related work section in that paper contains some pointers, such as Xu, Peyton-Jones, and Claessen's static contract checking for Haskell, and Sonnex, Drossopoulou, and ...


7

There has been various brand of work for formalizing such tricky code. The one I know about are (but I'm no expert on the topic): using "temporal logic" to study distributed systems; one important tool beeing the TLA+ tool is a program that verifies properties of specifications expressed in temporal logic; googling for "TLA+ dining philosopher" links to ...


7

There is a general theory here, which was introduced into CS by Robin Milner, which Lamport did not go into. A state machine is generally given as a triple $(Q \in \mathrm{Set}, q \in Q, f \in I \times Q \to \mathcal{P}(O \times Q))$, consisting of a state set $Q$, an initial state $q$, and a transition relation $f$. Now, suppose we have two automata $(Q,...


6

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 as a semantics of proofs, and SMT arises from the model-theoretic view of logic, which is a semantics of provability. A formula in SMT is a boolean ...


6

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 Abstraction for Size-Change Termination, by Codish, Fuhs, Giesl & Schneider-Kamp, basing their implementation on the papers you refer to. Performance is good ...


5

Don't worry too much about understanding everything in one source. Try reading several different articles and from their summaries and technical details, you may build up your own understanding. Symbolic Execution for Software Testing: Three Decades Later, Cristian Cadar and Koushik Sen, 2013. All You Ever Wanted to Know about Dynamic Taint Analysis and ...


5

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 Notherian finiteness by Thierry Coquand and Arnaud Spiwack. The idea is to define a set or a type $A$ to be finite if the following holds: every sequence $a : \mathbb{N}...


4

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 other well-founded orders on tuples, e.g. lexicographical order for some order of the fields (though you might need a heuristic to find the order), and various ...


3

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 approach to scaling such analyses is modularity which allows decomposing the problem into sub-problems. Indeed this usually consists in identifying cycle-like ...


3

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. Thus, what you are checking is whether a probabilistic system satisfies some property. For example "is it true that with probability at least 0.5, the system ...


3

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 | anywhere. System A incorrectly rejects a filename if it contains a prime number of b characters. Errors of the second type are much, much rarer, but this is not ...


3

This is a strange comparison. Your question is comparable to asking "how expressive is the ANSI C language specification compared to stdlib and compilation". The comparisons don't make sense. The Java Modelling Language can be used as a specification language to specify properties of code. The language alone does not solve the problem of verifying whether ...


3

Two or three years ago I started taking a look to formal methods applied to software. This was a quest driven by curiosity, and by the feeling that I had to learn programming tools and methods with longer time-spans. Although I dreamed wishfully about a Silver Bullet, I really thought that there was not an answer to the question: "How can I write a correct ...


2

there is a classic reference/framework increasingly standardized: C.A.R Hoare, Communicating Sequential Processes a 1985 book of same title is now available as ebook with open copyright. wikipedia also has a decent overview note it has some similarity/resemblance to unix pipes/filters there is an implementation in Java, JCSP by Welch/Brown & other ...


2

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 strings accepted by a Java method, using various techniques in static analysis. While the paper deals directly with the set of strings generated by a piece of Java ...


2

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 if whenever $u\notin P$, then $u$ has a finite prefix $u'\in\Sigma^*$ such that for any word $v$, $u'v\notin P$. A language $P\subseteq \Sigma^*\cup\Sigma^\...


2

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 order to be a superset of session order: $$\text{PRAM} \triangleq so \subseteq vis.$$ Thus, the offending arrow in your diagram, from $w(x)0$ to $r(x)0$, is ...


2

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 possible to build an interpreter that incurs at most a $O(1)$-factor slowdown, but I haven't checked the details (the instruction set is so primitive that the ...


1

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 available free of charge and links to them are available on the Z notation Wikipedia page. However, for this particular question, TC1 is not relevant. Section 15 ...


1

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.


1

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, but also between rep operations implementing abstract operations. The abstraction function maps each rep value to a nonempty set of abstract values: $$ \...


1

Some of the performance-related things you can objectively compare between different databases: IO complexity and computational complexity of different queries. E.g. there are different ways to do joins, sorting, different kinds of indices (including "no indices"), with objectively different asymptotic complexity. There are also column-oriented and row-...


1

Our work on soft verification of contracts is related, at OOPSLA 2012 and ICFP 2014, allows you to write contracts, which are a lot like ACSL specs, and then either statically verify them or use them a dynamic checks at runtime.


1

Being a beginner to Symbolic Execution (SE) myself, I would suggest: Symbolic execution and program testing: this is the paper to cite when you mention SE. It is easy to read, and provides the key idea without much logical formulation. All you ever wanted to know...: this paper surveys SE and its applications to Security. The third step may be to ...


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