Dr. Alex Summers and colleagues make a SPLASH with their Distinguished Paper Award
Dr. Alex Summers, an associate professor at the University of British Columbia, along with his co-authors grad student Thibault Dardinier and Dr. Peter Müller of ETH Zürich, has won an ACM SIGPLAN OOPSLA Distinguished Paper Award.
The group of international researchers submitted their paper to the OOPSLA track of the SPLASH Conference (Systems, Programming, Languages, and Applications: Software for Humanity) and earned the coveted award. Out of the 294 papers submitted, only 9 papers (3 per cent) received the "distinguished" title.
Their paper, Fractional Resources in Unbounded Separation Logic, presents a new semantics for ‘Separation Logic’ that reconciles the two previously existing views on multiplication within the field. The researchers show how to define the theory differently so it matches the actual tools where theory is applied.
What is Separation Logic?
In computer science, separation logic is a way of modularly reasoning about programs that access and mutate data held in computer memory.
Thibault Dardinier, the PhD student who drove the majority of the research and developed the initial idea, worked under the supervision of Dr. Peter Müller, a professor that Dr. Summers used to work with at ETH Zürich, and with Alex himself. Dr. Summers credits much of the success of this research to Dardinier's persistence. “I must admit, we were a little skeptical at first about Thibault’s logic, because quite honestly it was a bit outlandish, but ultimately we could not find a reason why the idea wouldn't work.”
UBC Computer Science
Dr. Summers said many back-and-forth conversations ensued about the mathematical construct and the logical flow of the paper. “I was effectively playing the role of a co-supervisor for the sake of this paper. We were having regular research meetings and helping Thibault refine and revise the paper so the logic was as clear as possible. It's a very technical and complicated paper, and there are many difficult ideas to communicate.” Drs. Summers and Müller had anticipated initial skepticism from the reviewers, much like their own. “So it was our job to remove the doubt, and make it as succinct, credible and as understandable as possible,” he said.
Dr. Summers explained the motivation behind the paper, saying that there was a discrepancy between the theoretical papers being written and how programs were being implemented in tools, resulting in a distinct gap between theory and practice. This paper presents a theoretical underpinning to the tools that fully explains the gap. The logic reconciles the two existing views on the meaning of multiplication in related logics, eliminating previous shortcomings. In the paper the authors state, ‘Our assertion semantics unifies semantic and syntactic multiplication and thereby reconciles the discrepancy between separation logic theory and tools, and enjoys distributivity, factorisability, and combinability.’
The results were ultimately outstanding, with all reviewers giving the paper the rating of “strong accept,” right out of the gate, indicating unanimous agreement on the worthiness of their paper. Upon winning the Distinguished Paper Award, Dr. Summers said, “We were very happy indeed. SPLASH is one of the best conferences in this field – and these awards are quite rare.” This is his first best paper award.
Alex goes on to credit Dardinier further, saying, “I think his work is quite ground-breaking and mathematically rich. There's a lot in there. It’s also very novel, in the sense that it shakes up a standard way that people have been doing this particular kind of mathematics, and shows at least that there's an alternative that people haven't thought of before.”
It appears that the efforts of Dr. Summers and his collaborators are really adding up to a lot of progress in this evolving field of research.
Alex has recently received another accolade. He participated in a competition called VerifyThis 2023, co-located with the ETAPS 2023 conferences. This is a timed competition for program verification with tools (called program verifiers). Teams write code within the parameters of properties the code is meant to always satisfy. For example: ‘the code must always produce an answer without crashing or taking forever,’ or ‘the answer must be the right one.’ In the competition, they find ways to specify these properties in the code so that a program verifier can prove that the desired properties are guaranteed to be always true for the code. There were 16 teams competing and Alex’s team came first in the competition.
About SPLASH: SPLASH embraces all aspects of software construction and delivery, to make it the premier conference on the applications of programming languages - at the intersection of programming languages and software engineering. The Distinguished Paper Award from the OOPSLA stream is a rare and prestigious recognition for these winners.