Alexander Grothendieck passed away in November 2014 at the age of 86. He contributed to several areas of mathematics and most prominently, laid the modern foundations of the field of algebraic geometry. As is often the case with mathematics, one can connect theoretical concepts from one area of inquiry to practically observed phenomena by using ideas from other areas to forge such a connection. This post is the first of a series that will describe an informal connection that leads from Grothendieck’s work in algebraic geometry via category theory and mathematical logic to high-performance solvers for NP-hard problems. Though these connections are not formal, it is amazing that they even exist.
1. Alexander Grothendieck (1928 – 2014)
Eep! I completely forgot the notes I typed out way back in 2012 about CAV and have neglected this blog for a while now.
The Gauge Domain: Scalable Analysis of Linear Inequality Invariants, Arnaud Venet
There is a rather curious algorithmic phenomenon that has a very direct impact on static analysis for numeric invariants. We can reason about equality and congruence relationships between variables somewhat efficiently. We can reason about inequalities concerning single variables somewhat efficiently. Efficient reasoning about inequalities over multiple variables is, however, not considered a solved problem.
There are intuitive reasons for the efficient solutions. When reasoning about equalities, the only property we have to worry about is transitivity, so a simple saturation routine comes to our aid. In the presence of uninterpreted functions, we also have to reason about congruences and the congruence closure algorithms still permits efficient reasoning. There are two generalisations of the logic of equality with uninterpreted functions that are relevant and useful in practice.
I missed the second day of pre-CAV workshops and the tutorial day on account of a deadline, but managed to make time to attend talks on the first day of CAV. This is the second time I was attending CAV, having previously attended it in Edinburgh in 2010. Surprisingly, I think I probably read more CAV papers before 2010 than after. I assume that CAV regulars can make more informed comments on trends visible in CAV proceedings, but from my limited knowledge, I would say that there are very few papers appearing on hardware verification, and the number of papers on temporal-logic related topics also seems to be declining. That said, Day 1 of CAV included a fair amount of automata and temporal logic. I will briefly summarise the talks I remember from this day.
I’ve delayed posting about the Computer Aided Verification conference (CAV) for about half a year. CAV 2012 was the second CAV I attended, with CAV 2010 having been the first. On both occasions, I did not pay much attention to the first half of the conference because of the Principles of Programming Languages (POPL) deadline and also did not immerse myself in the latter part of the conference because I was recovering from the deadline. The scheduling is not entirely symmetric. In both 2011 and 2012, the CAV submission deadline was a few days before the POPL conference started.
I imagine that these two venues historically had a very different focus. At present, program analysis papers appear in CAV and verification and logic papers appear in POPL, so there is greater overlap between material presented at the two venues. Even if deadlines are chosen not to clash, I think that authors will be facing pretty hectic schedules with submission and conference attendance dates being so close. One option, and a sensible one, would be to take it easier and consider fewer venues and make fewer submissions (since the total number of accepts I am left with does not seem to change all that much anyway). Let me see if I can work on that in the coming year.
My former colleague Philipp Rümmer co-organised a workshop on topics broadly concerned with applying logic to determine properties of various kinds of systems. I only managed to attend the morning session of the workshop, so the report below is very incomplete.
The invited talk was delivered by Radu Grosu. He covered a very broad and fascinating range of topics from philosophical ruminations about time and quantum mechanics, semantics of temporal logics to computerised analysis of music. The main point I took away was that time and frequency are well known dual concepts. This duality is the foundation of several techniques in physics and signal processing that exploit properties of the frequency domain to make conclusions about the time domain. The duality of time and frequency can also be used in the analysis of hybrid systems using temporal logic.
The idea of embedding frequency semantics into a temporal logic appealed to me a lot. I find that adding a modality or operator to a logic forces me to think about that operator very seriously and helps me truly understand and apply it. During the talk I found myself trying to think of standard hybrid systems and their properties in terms of the frequency domain and what it might mean to interpret a temporal logic over this domain. Moreover, I wonder if standard frequency domain techniques can be leveraged to obtain model checking algorithms for such a logic. I imagine that Radu and his collaborators have already answered some of these questions.
In addition to being thought provoking and having interesting mathematics, there were several applications that scored very high on my internal coolness meter. I can’t remember the details of the biological examples, except that they were there. Radu also had examples of a few bars of classical and blues music that could be succinctly described in such a logic.
Descriptions of the other talks can be found in the workshop proceedings.
Over lunch, I had the chance to meet Ashish Tiwari from SRI for the first time. He has done pioneering work in the intersection of decision procedures, program verification, abstract interpretation, hybrid systems and systems biology (to name only a few areas). I hope to cover some of his work in future posts.
William Thurston is a prominent mathematician. I know nothing about his research except that his work is held in high regard by professional mathematicians. He has received several awards for both his research and expository work. He has also written a few essays about the philosophy of mathematics, the most prominent of these I am aware of is titled On proof and progress in mathematics. Much of what he says is applicable to any form of intellectual discourse, particularly of a mathematical nature.
Mathematics in some sense has a common language: a language of symbols, technical definitions, computations, and logic. This language efficiently conveys some, but not all, modes of mathematical thinking. Mathematicians learn to translate certain things almost unconsciously from one mental mode to the other, so that some statements quickly become clear. […] Continue reading
Did we get the date wrong? Isn’t 2010 last year?
Yes. We know. But, when we landed in warm and sunny Paphos, it was this year and we thought: “This is amazing. We have to tell all those people we pretend to like back in cold and rainy England how the sun is browning our skins and how the warm waves are gently lapping at our feet and all those things we do for our true friends.”
Thus came our two correspondents to the idea of a blog. They saw that it was good and it pleased them. So much so that they promptly ordered a full mezze in the nearest restaurant causing a taste space explosion problem leading them to fall into a deep slumber for an entire week, at which point the conference was over.
A year later, with the wisdom of age and the ability to look back with fond memories, we had the startling revelation: Just because we weren’t there, doesn’t mean we don’t have to tell you about it. Without further ado, we bring you Vijay’s commentary on Philipp’s snapshots of ETAPS 2010.
We were very proud of our super-cheap hotel deal.
Until we discovered that the conference was 12km away! Despite the mendacity of Google Maps and Cyprus not being friends with The Internet, we managed to find the conference hotel.