Discussing "Horn Clause Solvers for Program Verification"

(Link)

Authors: Nikolaj Bjørner (Microsoft Research Redmond), Arie Gurfinkel (Software Engineering Institute), Ken McMillan (Microsoft Research Redmond) & Andrey Rybalchenko (Microsoft Research Cambridge)

Reference: Bjørner, N., Gurfinkel, A., McMillan, K., Rybalchenko, A. (2015). Horn Clause Solvers for Program Verification. In: Beklemishev, L., Blass, A., Dershowitz, N., Finkbeiner, B., Schulte, W. (eds) Fields of Logic and Computation II: Essays Dedicated to Yuri Gurevich on the Occasion of His 75th Birthday. Lecture Notes in Computer Science, vol 9300. Springer, Cham. https://doi.org/10.1007/978-3-319-23534-9_2

Why this paper? Cited by Multiple Query Satisfiability of Constrained Horn Clauses and Parameterized Recursive Refinement Types for Automated Program Verification

This paper is a small jump away from my usual research area, based as it is on automatic program verification rather than interactive theorem proving, let alone some of my more pure interests in logic and mathematics. However it does bump up against one of my interests (Craig interpolation) and fortunately is a highly readable and not too technical survey article summarising a field of work.

Horn clauses come in various forms in this paper, but in general are a sharp constraint on the way in which logic formulae can be written down: instead of the freedom to use logical connectives wherever one desires, one must write one’s formula in a precisely specified structure. For example, all universal quantifiers might be required to be on the outside level rather than nested inside the formulae, there is a limit of one implication in the whole formulae between a ‘body’ and ‘head’ which themselves have strict rules regarding their construction, and so on. Formulae of first-order logic can be tortured until they fit the pattern required by a set of Horn clauses, albeit at some cost of time and space. Furthermore, in this paper the underlying logic is extended with an additional assertion language, usually something like a limited notion of arithmetic, which may be useful for expressing properties of programs.

The point of forcing us to write our logical statements in a highly constrained fashion is to find a compromise point between expressivity – we can talk in meaningful ways about the properties of interesting programs – and efficiency for automatic verification of these properties. After introducing the basic notions, this paper is roughly split between these two concerns. One half gives examples of various notions for turning both programs and interesting properties of these programs into Horn clauses, for example an approach based on weakest preconditions applied to the verification language Boogie. The other half looks at ways that Horn clauses can be transformed to support more successful automation. It is this half where Craig interpolation, a famous property from logical theory, intersects with the practical concerns of this paper, as a certain useful Horn clause transformation called ‘unfold’ can only be guaranteed to be sound if the underlying assertion logic enjoys the property.

Discussing "Checking Interference with Fractional Permissions"

(Link)

Author: John Boyland (University of Wisconsin-Milwaukee)

Reference: Boyland, J. (2003). Checking Interference with Fractional Permissions. In: Cousot, R. (eds) Static Analysis. SAS 2003. Lecture Notes in Computer Science, vol 2694. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44898-5_4

Why this paper? Cited by Mechanised Robust Safety for Virtual Machines Communicating above FF-A, and Fractional Resources in Unbounded Separation Logic, and Verification-Preserving Inlining in Automatic Separation Logic Verifiers (extended version)

Of late the citations in my Google Scholar recommendations have been very concerned with the question of whether two different parts of a program interfere with each other, or depend on each other – see here, here, and (less directly) here. This is an important question if we want to reason about the behaviour of a program – we would like to reason about a large program piece by piece, but can only do so if we are sure the pieces do not interfere with each other (or, if they do interfere, we have a precise sense of how this interference might manifest).

Separation logic à la Reynolds tells us that we can reason about parts of a program separately if they only access disjoint parts of memory. This is correct, but needlessly blunt. Two programs that read the same piece of memory do not effect each other; it is only if one of those program write to memory the other program is interested in that we have an issue. The solution proposed in this paper is to give different (parts of) programs different levels of permission to each part of the memory. Full permission, represented by the number 1, allows one to write and read, whereas a permission represented by a fraction strictly between 0 and 1 gives only read access. Where there is parallel composition or similar in the program, permissions can be divided between threads. Conversely, a program can add its permissions back together when it completes threads and hence, if full permission is reached, regain the ability to write.

The concepts of this paper and presented in the form of a type system, but it was soon realised by others that they can also be used to generalise separation logic as well; this is the context in which fractional permissions continue to appear in papers recommended to me.

Discussing "Step-Indexed Syntactic Logical Relations for Recursive and Quantified Types"

 (Link)

Author: Amal Ahmed (Harvard University)

Reference: Ahmed, A. (2006). Step-Indexed Syntactic Logical Relations for Recursive and Quantified Types. In: Sestoft, P. (eds) Programming Languages and Systems. ESOP 2006. Lecture Notes in Computer Science, vol 3924. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11693024_6

Why this paper? Cited by Fractional Resources in Unbounded Separation Logic, and Program Equivalence in an Untyped, Call-by-value Lambda Calculus with Uncurried Recursive Functions, and Recursive Session Logical Relations

When are two programs equivalent? There are various answers one can give to this depending on whether one wishes to consider factors like time and memory usage, but one fundamental notion is contextual equivalence: two programs A and B are equivalent in this sense if any program in the language with A as a component will behave the same (with respect to termination) if that component is replaced by B. Hence, there is no context which can tell them apart. This is an intrinsically difficult fact to prove because one must consider all possible contexts, of which there are infinitely many to choose from. A general technique for demonstrating contextual equivalence in typed languages is the method of logical relations, in which a general relation between programs is built up by induction on types, and the problem of proving equivalence for particular programs is narrowed to the problem of proving that these programs are related.

The problem with defining a relation in the inductive style is that it relies on types being defined in terms of simpler subtypes. This paper looks at two important type constructors for which this fails. Inductive types like lists and trees refer to themselves – lists are defined in terms of lists – in a way that would make a naïve inductive definition on them immediately circular. Quantified types – universal types for parametric polymorphism and existential types, which resemble abstract data types – contain type variables which can be replaced by arbitrarily complicated types. This paper, picking up an idea from Appel and McAllester, shows that the unpleasant circularities can be removed if one adds a natural number ‘step-index’ to the relation to make sure that the induction remains well defined – when one is working with a type and must consider a type that is not smaller, one reduces the step-index towards zero to compensate. A lot is proved about this style of reasoning – the full version of the paper weighs in at a hefty 169 pages!

This is certainly a relevant ‘classic paper’ with respect to my own research interests; I get involved in this area via later work by Birkedal, Møgelberg, Schwinghammer and Støvring on ‘synthetic’ step-indexing, which uses a modality to hide some of the arithmetic of step-indexing. But that is, perhaps, a topic for another day.

Correspondence between Modal Hilbert Axioms and Sequent Rules with an Application to S5

(Link).

Authors: Björn Lellmann (Imperial College London) and Dirk Pattinson (Imperial College London / Australian National University).

Conference: Automated Reasoning with Analytic Tableaux and Related Methods (Tableaux 2013), Nancy, France, 16-19 September, 2013.

Journal reference: Lecture Notes in Computer Science, to appear.

Comments: This is a paper that Google Scholar Updates surely wouldn't have recommended to me a couple of weeks ago; recall that Updates uses one's papers as 'search terms' to direct its recommendations of new work to you. This paper has little in common with most of my existing papers, but it has clear (albeit somewhat shallow) similarities with my brand new paper 'Annotation-Free Sequent Calculi for Full Intuitionistic Linear Logic' (pdf), co-authored with Jeremy Dawson, Rajeev Goré, and Alwen Tiu, which I will be presenting at the conference CSL 2013 in September. I also must note that one of the authors of this paper, Dirk Pattinson, has an office in the same corridor as me at Australian National University; in this new world we apparently need big data algorithms to tell us to read the work of our colleagues next door!

A mathematical proof involves starting with agreed-upon axioms, applying agreed-upon inference rules, and reaching a conclusion; this is a rather basic definition, but leads us to the really important questions for a logician - what axioms? And what inference rules? One broad approach, called Hilbert calculi, require that only an extremely small and fixed set of inference rules be used: in the simplest systems the single rule Modus Ponens alone suffices, although with modal logic, the topic of this week's paper, a couple more are needed. All the action with Hilbert calculi is in their axioms, in the sense that many different logics developed for all sorts of different purposes may have the same inference rule(s) but very different axioms. Hilbert calculi have their charms - they can be a very concise way to present a logic, for example - but they are not much fun to construct actual proofs with, as proofs of even apparently simple tautologies can be lengthy and highly unintuitive.

To get a more structured proof system that helps both humans and machines to generate proofs, the opposite approach tends to be more helpful: more structured proof systems tend to have very few axioms - often the fact that every proposition entails itself is enough - but many inference rules. Such structured proof systems come in various styles, including natural deduction, tableau, and sequent calculus, the topic of this paper, and also of my CSL paper which has surely prompted this recommendation (broadly, these proof systems differ in the style in which the inference rules are designed and organised).

One last piece of preamble is needed before we consider this week's paper; modal logic refers to any logic involving 'modalities' that modify propositions. For example, if 'p' is a statement that might be true or false ("it is raining"), we can preface it with a range of modalities: "it is possible that", "I believe that", "I know that", "in the future it will hold that", and so on. If such modalities have any plausible logical content - e.g. you can form a deductive argument in which "it is possible that" forms an important part - then we can design a modal logic that captures this logical content, via Hilbert axioms, sequent calculus, or whatever other proof style appears most suited.

This paper concerns the translation back and forth between Hilbert calculi axioms and sequent calculi rules for modal logic. The details of this translation are far too involved to summarise adequately in this blog post, but a key wrinkle in the development is to precisely identify certain classes of axioms with certain classes of rules; these classes relate to how many modalities must be piled up on top of one proposition to describe the logic. These distinctions support the 'limitative' results of the final section of the paper, which uses the translation to show that certain modal logics (defined via Hilbert calculi) cannot be captured by certain types of sequent calculus.

Modelling Infinite Structures with Atoms

(Link).

Author: Mikołaj Bojańczyk (University of Warsaw)

Conference: Workshop on Logic, Language, Information and Computation (WoLLIC 2013), 20-23 August, 2013, Darmstadt, Germany.

Journal reference: Lecture Notes in Computer Science, to appear.

Comments: The topic of this week's paper, from an author we've met twice before (here and here) is compactness. Compactness is the property that states that an infinite set of logical sentences is satisfiable (not contradictory) if and only if all the finite subsets of that infinite set are satisfiable. Some logics have the property, but others may not. The importance of this result may not be immediately obvious; it was first discovered by Kurt Gödel for first-order logic as a mere corollary to another theorem (completeness). However compactness went on to be a cornerstone principle of the mathematical field of model theory, which in a broad sense looks at how logical claims can be 'satisfied' by mathematical constructions.

Bojańczyk is interested in shifting first-order logic from its usual set-theoretic foundations to the world of nominal sets, the mathematical model for names in syntax that I've discussed in many places on this blog, e.g. here (in fact, as discussed in that link, Bojańczyk has a somewhat more general notion in mind than is usually meant by 'nominal sets', but such subtleties are orthogonal enough to the gist of this paper that we will pass by them). Making first-order logic nominal means that predicates can involve names, and disjunctions and conjunctions can be infinite, although only 'orbit-finite'.

Compactness is fundamentally a theorem about infinite and finite collections; in nominal sets such issues become a bit subtle. First, each element of a nominal set has what is called the finite support property, which means that it 'depends' on only finitely many names. This is a very helpful assumption in practice, and is motivated by the idea that real syntax can only ever involve finitely many names (even when the syntax might get infinitely large, as I discussed here). Moving up a level, we see that no non-trivial nominal set is finite. However there is a notion something like finiteness that does make sense for nominal sets - that of orbit-finiteness, which essentially says that the nominal set is finitely 'generated', rather like an infinite number of reflections in a hall of mirrors could be generated by a finite number of people standing in its middle.

With familiar notions of finiteness and infinity upended by the nominal sets model, getting a halfway sensible notion of compactness becomes quite difficult. It clearly makes no sense to state the theorem in terms of finite sets of sentences, because there are no interesting finite nominal sets. More surprisingly, the compactness postulate got by replacing the word 'finite' with 'orbit-finite' turns out to be false. In fact to validate that version of the theorem we initially need to jump outside of the nominal sets model entirely by axing the finite support property. This is by no means an illegitimate move but it does create worries, because sets with names but no finite support property are less relevant to computer science applications. However Bojańczyk finishes the paper by putting the rabbit back into the hat by defining what are called 'stratified models', more complicated constructions which have the finite support property but also satisfy compactness by 'approximating' the non-finitely supported models.

Update: Due to workload my next post will be a fortnight after this one.

Formalizing Bounded Increase

(Link)

Author: René Thiemann (University of Innsbruck)

Conference: 4th International Conference on Interactive Theorem Proving (ITP '13), 22-26 July 2013, Rennes, France.

Journal reference: Lecture Notes in Computer Science 7998, pages 245-260, 2013.

Comments: This paper concerns the fundamental problem in computing of determining whether a given algorithm or program terminates, or instead gets stuck in an infinite loop. This is called the Halting Problem. In 1936 Alonzo Church and Alan Turing independently proved that this problem is, in general, insoluble - a program that accepts other programs as input and tells you if they terminate or not is logically impossible. This is the most spectacular result in all computer science, but the proof is really quite simple at its heart - just a little logic game involving feeding hypothetical programs to themselves until they display behaviour that it clearly paradoxical.

This is all a lot of fun, but the practical need to work out whether particular programs terminate or not remains, and so there is an obvious need for techniques that work to prove termination at least some of the time. This paper looks at bounded increase, where each iteration of the program (or some part of it) increases some index until it hits a 'ceiling' that it is provably not permitted to surpass. Because the index increases constantly but cannot do so forever, the program is guaranteed to terminate.

This technique was developed in an earlier paper by Thiemann and co-authors; this paper goes a step further by formalising it in the interactive theorem prover Isabelle/HOL. This sort of formalisation has been discussed several times on this blog - see here for example - and its usual motivation is to increase confidence in a result and detect any subtle errors. This is certainly a motivation here, and Thiemann discusses a number of issues that arise during this formalisation, particularly in the section on 'conditional constraints', but this particular formalisation is also intended to certify proofs produced by specialist termination provers such as AProVE and TTT2. Indeed, a bug in AProVE was uncovered by this research.

This is the second week in a row that Google Scholar Updates has recommended a paper that, while interesting, is not massively related to my research interests. At least this week the reason for the recommendation is a bit more clear - the author's formalisation had to grapple with some (fairly simple) issues involving variable binding, and he considers use of the specialist package Nominal Isabelle to deal with them; the outcome was that the package proved too heavy duty for his requirements and Thiemann instead defined everything needed for binding himself.

Partial Recursive Functions and Finality

(Link).

Author: Gordon Plotkin (University of Edinburgh)

Reference: Computation, Logic, Games, and Quantum Foundations: The Many Facets of Samson Abramsky, Lecture Notes in Computer Science Volume 7860, 2013, pp 311-326.

Comments: As I've mentioned before, there's a nice tradition in science of 'festschrift' volumes put out to celebrate the birthdays of prominent scientists. I myself have published a paper in a festschift for Gordon Plotkin's 60th birthday; here Plotkin himself contributes to a festschrift for the 60th birthday of Oxford computer scientist Samson Abramsky.

Despite this connection, this week's recommendation from Google Scholar Updates is unfortunately not very pertinent to my research interests. That's not to say it's not a nice paper, but Updates is supposed to be a source of personalised recommendations; I have other ways to find papers that are merely nice! The paper is about how partial recursive functions - which is to say, partially computable functions - can be 'represented' (in the technical sense used in the paper) within general category theory. Why has the algorithm recommended this to me? There is some use made of algebra and coalgebra, but that doesn't really seem sufficient grounds to send a paper my way (am I to be recommended every paper at CALCO, for example?). Perhaps publishing in a volume dedicated to Plotkin was enough?

Note: Next week I will be on leave and so my next blog will be in a fortnight.

Correctness of Functionally Specified Denotational and Operational Semantics

(Link).

Authors: Sjaak Smetsers, Ken Madlener (Radboud University Nijmegen), and Marko van Eekelen (Radboud University Nijmegen and Open University of the Netherlands)

Conference: Symposium on Trends in Functional Programming (TFP 2013), 14-16 May 2013, Provo, Utah, USA.

Journal reference: Lecture Notes in Computer Science, to appear.

Comments: Last week I looked at the ways Google Scholar Updates has been useful to my research; I recently read a blog post that saw the tool put to a rather more surprising use: Updates recommended a possibly relevant published paper that turned out to be highly related, in the sense that it was partly plagiarised from the academic's own work! Click here to read the story.

Moving on to this week's paper, we'll look at bialgebraic semantics of programming languages. The (only) good thing about technical jargon is that you can fit a lot of content into a small space, so we'll try to unpack this over the course of the post.

First, what is meant by "semantics of programming languages"? To give such is to give a precise and formal mathematical statement of how a programming language should be understood. These semantics can then be used to (a) reason about properties of the language, (b) reason about programs written in that language, and (c) guide the implementation of the language, e.g. compilation. Semantics come in a variety of different styles (see e.g. Wikipedia's overview of some options); the "bialgebraic" style of this paper is so called because it combines algebraic and coalgebraic approaches.

Algebraic semantics start with a specification of the syntax of the language, and then show how programs using that syntax can be interpreted within some mathematical setting. This mathematical translation is called the denotation of a program, and so algebraic semantics are a form of what is called denotational semantics. We discussed this approach here, but our mathematical setting in this paper is a lot simpler than that used there - the category of sets and functions rather than rich and complex "domains". The advantage of denotational semantics in general is that they are 'mathematical' in character and hence can be reasoned about with familiar mathematical tools such as induction; the disadvantage is that they are abstracted away from the original language enough that the actual behaviour of programs can be obscured.

Coalgebraic semantics are the category theoretic dual of algebraic semantics; we discussed coalgebra here. Coalgebra are a good way of talking about systems with transitions; when used in semantics they view programs as transitions between states (say, memory states of the program). This is a particular style of what is called operational semantics.

The denotational and operational semantics of a language or program should, of course, have something to do with each other; the jargon for when they conform is the adequacy property. But we'd like to say more than that: we'd like the coalgebraically specified operational behaviour of the language to very closely flow from the algebraically specified syntax. In other words we'd like the algebra to provide 'structure' for the coalgebra, in the style called structural operational semantics. It turns out this sort of structure can be imposed at the level of abstract category theory, quite independent of the attributes of any particular language, by asking that the algebra and coalgebra share certain mathematical relationships called 'distribution laws'. The seminal paper behind this idea is Turi and Plotkin's 1997 Towards a mathematical operational semantics, but I'd recommend starting with Klin's nice introduction to the area.

So what does this week's paper contribute? One problem with formal semantics - the reason most languages lack them despite their obvious advantages - is that real languages are huge and complicated and formal proofs involving them are just too big to fit in any one human being's mind. Hence there is a need for formalisation, in the sense that machines, rather than people, should at the very least record and check proofs, and preferably do some of the grunt work themselves. This is a pretty common refrain on this blog - see here for example. This paper, then, is a formalisation of bialgebraic semantics (the general theory, not any particular language) into the specification tool and theorem prover PVS. The particularities of the coding are a bit beyond me, as a non-expert in mechanised theorem proving, but the appeal of PVS seems to be that it is designed and used as a working tool for real world formal methods, and so provides a promising link between abstract category theory and application; the main impediment seems to be its weak support for certain forms of polymorphism.

An algebraic presentation of predicate logic

(Link).

Author: Sam Staton (University of Cambridge).

Conference: 16th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2013), 18-20 March 2013, Rome, Italy.

Journal reference: Lecture Notes in Computer Science (to appear).

Comments: After last week's head-scratcher, Google Scholar Updates is back on firmer ground with a paper by somebody I know, from my old university, that cites one of my own papers. In fact, this paper is due to be presented at a conference later this year that I also have a paper at (pdf), so this is a chance to read something before I see it presented.

Equational logic is the logic that allows you to reason about systems that are defined with equations; its basic rules include facts such as "everything is equal to itself", and "if x is equal to y, then y is equal to x". This may not seem particularly deep, but in fact a vast number of mathematically significant systems are amenable to equational reasoning - groups, rings, Boolean algebras, and so on. I myself have conducted a short course of lectures on equational logic at the Australian National University's Logic Summer School - my slides can be found here.

For all the power of equational logic, both the demands of applications and pure curiousity have often lead people to tweak or extend the basic logic. The bulk of my own publications have looked at a certain tweak of equational logic, and this paper introduces another (my paper Nominal Equational Logic, with Andrew Pitts, is cited as related work for this reason).

Staton's new style of equational logic is called 'parameterized algebra'. In the standard equational setting, we start with a 'signature' of operation and constant symbols that can be used to build terms. For example, if we are interested in monoids we have an identity constant and a binary multiplication; if we move to groups we add a unary inverse operation, and so forth. With parameterized algebra we have two signatures - a main one, and an ancillary one that is used to define parameters. The difference between this and ordinary equational logic with two sorts is two-fold. First, parameter-sorted variables can be bound by the main signature's operations. Second, parameter terms can be appended to the main signature's variables. For example, the term

∃ a. P[a]

where a is a parameter-sorted variable and P is a main signature variable, indicates that a is bound by the existential quantifier ∃, and that P is 'standing in' for a predicate that may make some mention of a.

Once the new logic is defined, the paper goes in two directions: first, it develops the metatheory of the logic, first via Lawvere-style classifying categories, and then via monads (in fact, relative monads; this is the second paper of the four I have had recommended to me that has made use of this fairly recently developed notion). Second, a major example is developed of 'disjunctive predicate logic', a fragment of first order logic (lacking e.g. implication) that uses parameters. This example is considered as a small programming language, and it is shown that it has a mathematically natural description in the 'classifying category' setting.