Relational verification encompasses information flow security, regression verification, translation validation for compilers, and more. Effective alignment of the programs and computations to be related facilitates use of simpler relational invariants and relational procedure specs, which in turn enables automation and modular reasoning. Alignment has been explored in terms of trace pairs, deductive rules of relational Hoare logics (RHL), and several forms of product automata. This article shows how a simple extension of Kleene Algebra with Tests (KAT), called BiKAT, subsumes prior formulations, including alignment witnesses for forallexists properties, which brings to light new RHLstyle rules for such properties. Alignments can be discovered algorithmically or devised manually but, in either case, their adequacy with respect to the original programs must be proved; an explicit algebra enables constructive proof by equational reasoning. Furthermore our approach inherits algorithmic benefits from existing KATbased techniques and tools, which are applicable to a range of semantic models.
more »
« less
On incorrectness logic and Kleene algebra with top and tests
Kleene algebra with tests (KAT) is a foundational equational framework for reasoning about programs, which has found applications in program transformations, networking and compiler optimizations, among many other areas. In his seminal work, Kozen proved that KAT subsumes propositional Hoare logic, showing that one can reason about the (partial) correctness of while programs by means of the equational theory of KAT. In this work, we investigate the support that KAT provides for reasoning about incorrectness, instead, as embodied by O'Hearn's recently proposed incorrectness logic. We show that KAT cannot directly express incorrectness logic. The main reason for this limitation can be traced to the fact that KAT cannot express explicitly the notion of codomain, which is essential to express incorrectness triples. To address this issue, we study Kleene Algebra with Top and Tests (TopKAT), an extension of KAT with a top element. We show that TopKAT is powerful enough to express a codomain operation, to express incorrectness triples, and to prove all the rules of incorrectness logic sound. This shows that one can reason about the incorrectness of whilelike programs by means of the equational theory of TopKAT.
more »
« less
 NSFPAR ID:
 10322534
 Date Published:
 Journal Name:
 Proceedings of the ACM on Programming Languages
 Volume:
 6
 Issue:
 POPL
 ISSN:
 24751421
 Format(s):
 Medium: X
 Sponsoring Org:
 National Science Foundation
More Like this


Reasoning about storage systems is challenging because these systems make persistence guarantees even if the system crashes at any point. To achieve these crashsafety guarantees, storage systems include recovery procedures to restore the system to a consistent state after a crash. Moreover, largescale systems are structured as multiple stacked layers and can require recovery at multiple layers of abstraction. Formal verification can ensure that crashsafety guarantees hold regardless of when the system crashes. To make verification tractable, largescale systems should be verified in a modular fashion, layerbylayer in the software stack. Layered recovery makes modularity challenging because the system can crash in the middle of a highlevel recovery procedure and must start over from the lowlevel recovery procedure. We present Argosy, a framework for machinechecked proofs of storage systems that supports layered recovery implementations with modular proofs. The framework is based on combinators for transition relations that are inspired by Kleene algebra, which provides a convenient formalism for specifying and reasoning about crashes and recovery. On top of this framework, we implement Crash Hoare Logic (CHL), the program logic used by FSCQ. Using the logic, we have verified an example of layered recovery featuring a writeahead log on top of a disk, which itself runs by replicating over two unreliable disks. The metatheory of the framework, the soundness of the program logic, and these examples are all verified in the Coq theorem prover.more » « less

Formal reasoning about hashingbased probabilistic data structures often requires reasoning about random variables where when one variable gets larger (such as the number of elements hashed into one bucket), the others tend to be smaller (like the number of elements hashed into the other buckets). This is an example of negative dependence , a generalization of probabilistic independence that has recently found interesting applications in algorithm design and machine learning. Despite the usefulness of negative dependence for the analyses of probabilistic data structures, existing verification methods cannot establish this property for randomized programs. To fill this gap, we design LINA, a probabilistic separation logic for reasoning about negative dependence. Following recent works on probabilistic separation logic using separating conjunction to reason about the probabilistic independence of random variables, we use separating conjunction to reason about negative dependence. Our assertion logic features two separating conjunctions, one for independence and one for negative dependence. We generalize the logic of bunched implications (BI) to support multiple separating conjunctions, and provide a sound and complete proof system. Notably, the semantics for separating conjunction relies on a nondeterministic , rather than partial, operation for combining resources. By drawing on closure properties for negative dependence, our program logic supports a Framelike rule for negative dependence and monotone operations. We demonstrate how LINA can verify probabilistic properties of hashbased data structures and ballsintobins processes.more » « less

Sacristán, A. I. ; CortésZavala, J. C. ; RuizArias, P. M. (Ed.)What impact, if any, do interesting lessons have on the types of questions students ask? To explore this question, we used lesson observations of six teachers from three high schools in the Northeast who were part of a larger study. Lessons come from a range of courses, spanning Algebra through Calculus. After each lesson, students reported interest via lesson experience surveys (Author, 2019). These interest measures were then used to identify each teachers’ highest and lowest interest lessons. The two lessons per teacher allows us to compare across the same set of students per teacher. We compiled 145 student questions and identified whether questions were asked within a group work setting or part of a whole class discussion. Two coders coded 10% of data to improve the rubric for type of students’ questions (what, why, how, and if) and perceived intent (factual, procedural, reasoning, and exploratory). Factual questions asked for definitions or explicit answers. Procedural questions were raised when students looked for algorithms or a solving process. Reasoning questions asked about why procedures worked, or facts were true. Exploratory questions expanded beyond the topic of focus, such as asking about changing the parameters to make sense of a problem. The remaining 90% of data were coded independently to determine interrater reliability (see Landis & Koch, 1977). A Cohen’s Kappa statistic (K=0.87, p<0.001) indicates excellent reliability. Furthermore, both coders reconciled codes before continuing with data analysis. Initial results showed differences between high and lowinterest lessons. Although students raised fewer mathematical questions in highinterest lessons (59) when compared with lowinterest lessons (86), highinterest lessons contained more “exploratory” questions (10 versus 6). A chisquare test of independence shows a significant difference, χ2 (3, N = 145) = 12.99, p = .005 for types of students’ questions asked in high and lowinterest lessons. The highinterest lessons had more student questions arise during whole class discussions, whereas lowinterest lessons had more student questions during group work. By partitioning each lesson into acts at points where the mathematical content shifted, we were able to examine through how many acts questions remained open. The average number of acts the students’ questions remained unanswered for highinterest lessons (2.66) was higher than that of lowinterest lessons (1.68). Paired samples ttests suggest that this difference is significant t(5)=2.58, p = 0.049. Therefore, student interest in the lesson did appear to impact the type of questions students ask. One possible reason for the differences in student questions is the nature of the lessons students found interesting, which may allow for student freedom to wonder and chase their mathematical ideas. There may be more overall student questions in lowinterest lessons because of confusion, but more research is needed to unpack the reasoning behind student questions.more » « less

We present Lilac, a separation logic for reasoning about probabilistic programs where separating conjunction captures probabilistic independence. Inspired by an analogy with mutable state where sampling corresponds to dynamic allocation, we show how probability spaces over a fixed, ambient sample space appear to be the natural analogue of heap fragments, and present a new combining operation on them such that probability spaces behave like heaps and measurability of random variables behaves like ownership. This combining operation forms the basis for our model of separation, and produces a logic with many pleasant properties. In particular, Lilac has a frame rule identical to the ordinary one, and naturally accommodates advanced features like continuous random variables and reasoning about quantitative properties of programs. Then we propose a new modality based on disintegration theory for reasoning about conditional probability. We show how the resulting modal logic validates examples from prior work, and give a formal verification of an intricate weighted sampling algorithm whose correctness depends crucially on conditional independence structure.more » « less