Search

This paper presents Holbert: a work-in-progress pedagogical proof assistant and online textbook platform, aimed at the educational use-case, specifically for the teaching of programming language theory. Holbert allows proof exercises and rule definitions to be embedded directly in an online textbook, where proofs and rules can be manipulated using a graphical interface. We give an overview of the logical foundations of Holbert, examples of its use, and give an update as to its current implementation status., Short paper for Human Aspects of Types and Reasoning Assistants (HATRA), 2022. 8 pages, plus 2 pages references

We present Quickstrom, a property-based testing system for acceptance testing of interactive applications. Using Quickstrom, programmers can specify the behaviour of web applications as properties in our testing-oriented dialect of Linear Temporal Logic (LTL) called QuickLTL, and then automatically test their application against the given specification with hundreds of automatically generated interactions. QuickLTL extends existing finite variants of LTL for the testing use-case, determining likely outcomes from partial traces whose minimum length is itself determined by the LTL formula. This temporal logic is embedded in our specification language, Specstrom, which is designed to be approachable to web programmers, expressive for writing specifications, and easy to analyse. Because Quickstrom tests only user-facing behaviour, it is agnostic to the implementation language of the system under test. We therefore formally specify and test many implementations of the popular TodoMVC benchmark, used for evaluation and comparison across various web frontend frameworks and languages. Our tests uncovered bugs in almost half of the available implementations.

Property-based testing (PBT) is a powerful tool that is widely available in modern programming languages. It has been used to reduce formal software verification effort. We demonstrate how PBT can be used in conjunction with formal verification to incrementally gain greater assurance in code correctness by integrating PBT into the verification framework of Cogent---a programming language equipped with a certifying compiler for developing high-assurance systems components. Specifically, for PBT and formal verification to work in tandem, we structure the tests to mirror the refinement proof that we used in Cogent's verification framework: The expected behaviour of the system under test is captured by a functional correctness specification, which mimics the formal specification of the system, and we test the refinement relation between the implementation and the specification. We exhibit the additional benefits that this mutualism brings to developers and demonstrate the techniques we used in this style of PBT, by studying two concrete examples.

Natural convection is ubiquitous throughout the physical sciences and engineering, yet many of its important properties remain elusive. To study convection in a novel context, we derive and solve a quasilinear form of the Rayleigh-B\'enard problem by representing the perturbations in terms of marginally-stable eigenmodes. The amplitude of each eigenmode is determined by requiring that the background state maintains marginal stability. The background temperature profile evolves due to the advective flux of every marginally-stable eigenmode, as well as diffusion. To ensure marginal stability and to obtain the eigenfunctions at every timestep, we perform a one-dimensional eigenvalue solve on each of the allowable wavenumbers. The background temperature field evolves to an equilibrium state, where the advective flux from the marginally-stable eigenmodes and the diffusive flux sum to a constant. These marginally-stable thermal equilibria (MSTE) are exact solutions of the quasilinear equations. The mean temperature profile has thinner boundary layers and larger Nusselt numbers than thermally-equilibrated 2D and 3D simulations of the full nonlinear equations. We find the Nusselt number scales like $\rm{Nu} \sim\rm{Ra}^{1/3}$. When an MSTE is used as initial conditions for a 2D simulation, we find that Nu quickly equilibrates without the burst of turbulence often induced by purely conductive initial conditions, but we also find that the kinetic energy is too large and viscously attenuates on a long viscous time scale. This is due to the thin temperature boundary layers which diffuse heat very effectively, thereby requiring high-velocity advective flows to reach an equilibrium.

This paper presents a framework aimed at significantly reducing the cost of proving functional correctness for low-level operating systems components. The framework is designed around a new functional programming language, Cogent. A central aspect of the language is its uniqueness type system, which eliminates the need for a trusted runtime or garbage collector while still guaranteeing memory safety, a crucial property for safety and security. Moreover, it allows us to assign two semantics to the language: The first semantics is imperative, suitable for efficient C code generation, and the second is purely functional, providing a user-friendly interface for equational reasoning and verification of higher-level correctness properties. The refinement theorem connecting the two semantics allows the compiler to produce a proof via translation validation certifying the correctness of the generated C code with respect to the semantics of the Cogent source program. We have demonstrated the effectiveness of our framework for implementation and for verification through two file system implementations.

We present a self-certifying compiler for the COGENT systems language. COGENT is a restricted, polymorphic, higher-order, and purely functional language with linear types and without the need for a trusted runtime or garbage collector. It compiles to efficient C code that is designed to interoperate with existing C functions. The language is suited for layered systems code with minimal sharing such as file systems or network protocol control code. For a well-typed COGENT program, the compiler produces C code, a high-level shallow embedding of its semantics in Isabelle/HOL, and a proof that the C code correctly implements this embedding. The aim is for proof engineers to reason about the full semantics of real-world systems code productively and equationally, while retaining the interoperability and leanness of C. We describe the formal verification stages of the compiler, which include automated formal refinement calculi, a switch from imperative update semantics to functional value semantics formally justified by the linear type system, and a number of standard compiler phases such as type checking and monomorphisation. The compiler certificate is a series of language-level meta proofs and per-program translation validation phases, combined into one coherent top-level theorem in Isabelle/HOL.

Graffiti is art, graffiti is crime, graffiti is beautiful, graffiti is ugly, graffiti is political, graffiti is style, graffiti is an ASBO, graffiti is Banksy. Regardless of where you sit in any debate on the value of graffiti, there is always one indelible truth: it exists. And to exist it must exist somewhere. It is in the study of this ‘where’ that we hope to learn something about the essence of these scribbles on walls. We ask: why is graffiti in this place and not in that place? We do this by taking a GIS approach to the question, in which we collect graffiti, digitise graffiti, analyse graffiti and visualise graffiti. We find that the physical factors which define the location of graffiti in the city centre are, for the most part, limited to perfunctory city constructs such as crossing guards, phone boxes and electricity boxes but that every now and again, city features come together in such a way as to create the opportunity for clusters of graffiti to exist. However, it is necessary that we not only locate graffiti in space, we also need to locate it within the motivations of the subculture to which it belongs. In the end we find graffiti to be a duel construct, made up of the desires of a global subculture and how the city allows these desires to be made manifest.