 Award ID(s):
 1811894
 NSFPAR ID:
 10167667
 Date Published:
 Journal Name:
 23rd Symposium on Formal Methods, FM 2019, in the form of the 3rd World Congress on Formal Methods,
 Volume:
 11800
 Page Range / eLocation ID:
 573590
 Format(s):
 Medium: X
 Sponsoring Org:
 National Science Foundation
More Like this

null (Ed.)The typetheoretic notions of existential abstraction, subtyping, subsumption, and intersection have useful analogues in separationlogic 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 machinechecked functionalcorrectness verification of software at scale, VST embeds its expressive program logic in dependently typed higherorder 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 toptobottom verification: gaps between source code verification, compilation, and domainspecific 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 higherorder 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 typetheoretic 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 functionspecification 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 separationlogic framing and parameter adaptation, as well as stepindexing and specifications constructed via mixedvariance functors (needed for C’s function pointers).more » « less

null (Ed.)We verify the functional correctness of an arrayofbins (segregated freelists) singlethread 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 "resourceaware" 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 resourceaware specification implies a resourceoblivious spec.more » « less

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 clientvisible reasoning principles; (ii) residual predicates, which help enforcing data abstraction in callbackrich code; and (iii) an application to pure (Smalltalkstyle) objects that connects code verification to modellevel 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, abstractionrespecting component composition rule for Verifiable C.more » « less

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/>}=\mathrm{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 phasefactor 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 powerlaw 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\phantom{\rule{thickmathspace}{0ex}}{\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 phasefactor spectra${F}_{\mathrm{\psi <\#comment/>}}(\mathrm{\kappa <\#comment/>})$ . The precise location and shape of the bump are different for the four phasescreen types, but in each case it occurs at$\mathrm{\kappa <\#comment/>}\sim <\#comment/>1/{r}_{c}$ . The bump is unrelated to the wellknown “Hill bump” and is not caused by diffraction effects. It is solely a characteristic of the refractiveindex statistics represented by the respective phase screen. We show that the secondorder$\mathrm{\psi <\#comment/>}$ statistics (covariance function, structure function, and spectrum) characterize a random phase screen more completely than the secondorder$\mathrm{\varphi <\#comment/>}$ counterparts. 
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 valuefunction 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 offpolicy data from onpolicy rollouts via counterfactual reasoning on different ways of satisfying the LTL specification. Our experiments, conducted in both discrete and continuous stateaction spaces, confirm the effectiveness of our counterfactual experience replay approach.more » « less