The Effects of Adding Reachability Predicates in Quantifier-Free Separation Logic

The list segment predicate ls used in separation logic for verifying programs with pointers is well suited to express properties on singly-linked lists. We study the effects of adding ls to the full quantifier-free separation logic with the separating conjunction and implication, which is motivated by the recent design of new fragments in which all these ingredients are used indifferently and verification tools start to handle the magic wand connective. This is a very natural extension that has not been studied so far. We show that the restriction without the separating implication can be solved in polynomial space by using an appropriate abstraction for memory states, whereas the full extension is shown undecidable by reduction from first-order separation logic. Many variants of the logic and fragments are also investigated from the computational point of view when ls is added, providing numerous results about adding reachability predicates to quantifier-free separation logic.

Eliminating above-surface diffractions from ground-penetrating radar data using iterative Stolt migration

Above-surface diffractions (ASDs) received by unshielded ground-penetrating radar (GPR) antennas are known to contaminate subsurface reflections and diffractions. Existing ASD-removal methods either leave relatively strong residual ASDs within subsurface reflections or attenuate them excessively. We have developed an iterative migration-based ASD-removal method to address this issue that separates ASDs from subsurface reflections via surgical mute. First, we isolate ASDs within the GPR profile using an optimal window function, generated using the focal center of ASDs within the migrated domain. The remainder signifies the zeroth-order separation of subsurface reflections. Second, we perform Stolt migration on the isolated ASDs using the speed of light in air. Then, we mute out the regions dominated by ASDs from the migration results, characterized by highly focused ASDs that are well separated from the majority of subsurface reflections. Following that, we demigrate the separated ASDs and subsurface reflections back to the unmigrated domain using the speed of light in air. Next, we combine the demigrated subsurface reflections with the zeroth-order subsurface reflections, thereby completing the first iteration of the separation process. The entire aforementioned process is then repeated twice on the residual data to obtain further residual subsurface reflections from ASDs, using a lower velocity and a higher velocity in sequence. Our method is verified to suppress ASDs more effectively than existing approaches by retaining a greater proportion of subsurface reflections, and its residual error is negligible. It is robust with respect to energy levels, window widths of ASDs, and clustered ASDs.

Connecting Higher-Order Separation Logic to a First-Order Outside World

Separation logic is a useful tool for proving the correctness of programs that manipulate memory, especially when the model of memory includes higher-order state: Step-indexing, predicates in the heap, and higher-order ghost state have been used to reason about function pointers, data structure invariants, and complex concurrency patterns. On the other hand, the behavior of system features (e.g., operating systems) and the external world (e.g., communication between components) is usually specified using first-order formalisms. In principle, the soundness theorem of a separation logic is its interface with first-order theorems, but the soundness theorem may implicitly make assumptions about how other components are specified, limiting its use. In this paper, we show how to extend the higher-order separation logic of the Verified Software Toolchain to interface with a first-order verified operating system, in this case CertiKOS, that mediates its interaction with the outside world. The resulting system allows us to prove the correctness of C programs in separation logic based on the semantics of system calls implemented in CertiKOS. It also demonstrates that the combination of interaction trees + CompCert memories serves well as a lingua franca to interface and compose two quite different styles of program verification.

Dynamic Separation of Powers

This book argues that constitutional review is an aspect of the separation of powers. In determining its scope, though, we do not only look to history. We look ahead as well, to the challenges our political order faces now and in the future. These challenges sometimes expose the deficiencies in the extant separation of powers and the need to update it so that it can sustain its legitimacy. Updating the constitution is a matter of a higher-order separation of powers and thus also governed by political morality. Political morality assigns constitutional authorship more liberally than we tend to think. Sometimes, it assigns constitutional authorship to actors and procedures beyond those specified in the amendment provisions of the original constitution, including courts themselves.