More Like this

1. Abstraction and subsumption in modular verification of C programs

   https://doi.org/10.1007/s10703-020-00353-1  

   Beringer, Lennart ; Appel, Andrew W. ( March 2021 , Formal Methods in System Design)

   null (Ed.)

   The type-theoretic notions of existential abstraction, subtyping, subsumption, and intersection have useful analogues in separation-logic proofs of imperative programs. We have implemented these as an enhancement of the verified software toolchain (VST). VST is an impredicative concurrent separation logic for the C language, implemented in the Coq proof assistant, and proved sound in Coq. For machine-checked functional-correctness verification of software at scale, VST embeds its expressive program logic in dependently typed higher-order logic (CiC). Specifications and proofs in the program logic can leverage the expressiveness of CiC—so users can overcome the abstraction gaps that stand in the way of top-to-bottom verification: gaps between source code verification, compilation, and domain-specific reasoning, and between different analysis techniques or formalisms. Until now, VST has supported the specification of a program as a flat collection of function specifications (in higher-order separation logic)—one proves that each function correctly implements its specification, assuming the specifications of the functions it calls. But what if a function has more than one specification? In this work, we exploit type-theoretic concepts to structure specification interfaces for C code. This brings modularity principles of modern software engineering to concrete program verification. Previous work used representation predicates to enable data abstraction in separation logic. We go further, introducing function-specification subsumption and intersection specifications to organize the multiple specifications that a function is typically associated with. As in type theory, if 𝜙 is a of 𝜓, that is 𝜙<:𝜓, then 𝑥:𝜙 implies 𝑥:𝜓, meaning that any function satisfying specification 𝜙 can be used wherever a function satisfying 𝜓 is demanded. Subsumption incorporates separation-logic framing and parameter adaptation, as well as step-indexing and specifications constructed via mixed-variance functors (needed for C’s function pointers). 

   more » « less
2. Verified sequential Malloc/Free

   https://doi.org/10.1145/3381898.3397211  

   Appel, Andrew W. ; Naumann, David A. ( June 2020 , International Symposium on Memory Management)

   null (Ed.)

   We verify the functional correctness of an array-of-bins (segregated free-lists) single-thread malloc/free system with respect to a correctness specification written in separation logic. The memory allocator is written in standard C code compatible with the standard API; the specification is in the Verifiable C program logic, and the proof is done in the Verified Software Toolchain within the Coq proof assistant. Our "resource-aware" specification can guarantee when malloc will successfully return a block, unlike the standard Posix specification that allows malloc to return NULL whenever it wants to. We also prove subsumption (refinement): the resource-aware specification implies a resource-oblivious spec. 

   more » « less
3. Verified Software Units

   https://doi.org/10.1007/978-3-030-72019-3_5  

   Beringer, Lennart ( March 2021 , Programming Languages and Systems. ESOP 2021.)

   Yoshida, Nobuko (Ed.)

   Modularity - the partitioning of software into units of functionality that interact with each other via interfaces - has been the mainstay of software development for half a century. In case of the C language, the main mechanism for modularity is the compilation unit / header file abstraction. This paper complements programmatic modularity for C with modularity idioms for specification and verification in the context of Verifiable C, an expressive separation logic for CompCert Clight. Technical innovations include (i) abstract predicate declarations – existential packages that combine Parkinson & Bierman’s abstract predicates with their client-visible reasoning principles; (ii) residual predicates, which help enforcing data abstraction in callback-rich code; and (iii) an application to pure (Smalltalk-style) objects that connects code verification to model-level reasoning about features such as subtyping, self, inheritance, and late binding. We introduce our techniques using concrete example modules that have all been verified using the Coq proof assistant and combine to fully linked verified programs using a novel, abstraction-respecting component composition rule for Verifiable C. 

   more » « less
4. Phase-factor spectra of turbulent phase screens

   https://doi.org/10.1364/JOSAA.429928  

   Muschinski, Andreas ( August 2021 , Journal of the Optical Society of America A)

   The optical phase$\mathrm{\varphi <\#comment/>}$is a key quantity in the physics of light propagating through a turbulent medium. In certain respects, however, the statistics of the phasefactor,$\mathrm{\psi <\#comment/>}=\exp <\#comment/>(i\mathrm{\varphi <\#comment/>})$, are more relevant than the statistics of the phase itself. Here, we present a theoretical analysis of the 2D phase-factor spectrum$F_{\mathrm{\psi <\#comment/>}}(\mathit{\kappa <\#comment/>})$of a random phase screen. We apply the theory to four types of phase screens, each characterized by a power-law phase structure function,$D_{\mathrm{\varphi <\#comment/>}}(r)=(r/r_c{)}^{\mathrm{\gamma <\#comment/>}}$(where$r_c$is the phase coherence length defined by$D_{\mathrm{\varphi <\#comment/>}}(r_c)=1{\mathrm{r}\mathrm{a}\mathrm{d}}^2$), and a probability density function$p_{\mathrm{\alpha <\#comment/>}}(\mathrm{\alpha <\#comment/>})$of the phase increments for a given spatial lag. We analyze phase screens with turbulent ($\mathrm{\gamma <\#comment/>}=5/3$) and quadratic ($\mathrm{\gamma <\#comment/>}=2$) phase structure functions and with normally distributed (i.e., Gaussian) versus Laplacian phase increments. We find that there is a pronounced bump in each of the four phase-factor spectra$F_{\mathrm{\psi <\#comment/>}}(\mathrm{\kappa <\#comment/>})$. The precise location and shape of the bump are different for the four phase-screen types, but in each case it occurs at$\mathrm{\kappa <\#comment/>}\sim <\#comment/>1/r_c$. The bump is unrelated to the well-known “Hill bump” and is not caused by diffraction effects. It is solely a characteristic of the refractive-index statistics represented by the respective phase screen. We show that the second-order$\mathrm{\psi <\#comment/>}$statistics (covariance function, structure function, and spectrum) characterize a random phase screen more completely than the second-order$\mathrm{\varphi <\#comment/>}$counterparts.

    

   more » « less
5. Eventual Discounting Temporal Logic Counterfactual Experience Replay

   Cameron Voloshin ; Abhinav Verma ; Yisong Yue ( January 2023 , arXivorg)

   Linear temporal logic (LTL) offers a simplified way of specifying tasks for policy optimization that may otherwise be difficult to describe with scalar reward functions. However, the standard RL framework can be too myopic to find maximally LTL satisfying policies. This paper makes two contributions. First, we develop a new value-function based proxy, using a technique we call eventual discounting, under which one can find policies that satisfy the LTL specification with highest achievable probability. Second, we develop a new experience replay method for generating off-policy data from on-policy rollouts via counterfactual reasoning on different ways of satisfying the LTL specification. Our experiments, conducted in both discrete and continuous state-action spaces, confirm the effectiveness of our counterfactual experience replay approach. 

   more » « less