ABSTRACT. With the progress in deductive program verification research, new tools and techniques have become available to reason about non-trivial programs written in widely-used programming languages. However, deductive program verification remains an activity for experts, with ample experience in programming, specification and verification. We would like to change this situation, by developing program verification techniques that are available to a larger audience. Therefore, in this presentation, we show how we developed program verification support for Snap!. Snap! is a visual programming language, aiming in particular at high school students. We support both static and dynamic verification of Snap! programs. Moreover, we also outline how program verification in Snap! could be introduced to high school students in a classroom situation.

ABSTRACT. Dedicated many-core processors such as GPGPUs, enable programmers to design and implement parallel algorithms to optimize performance. The stream compaction and summed-area table algorithms are two examples where parallel versions have been proposed in the literature with substantial speed ups compared to sequential counterparts. Since these two algorithms are widely used, their correctness is of the utmost importance, i.e., the algorithms must be functionally correct and their implementations must be memory safe. These algorithms use the parallel prefix sum algorithm internally. In our previous work, we verified two parallel prefix sum algorithms. In this paper, we show how we can reuse a verified sub-function (i.e., prefix sum) to prove more complicated algorithms (i.e., stream compaction and summed area table) in a modular way with less effort. Moreover, we demonstrate that it is feasible in practice to verify larger case studies by building the verification of the complicated algorithm on top of the basic one. To show the correctness of the algorithms, we use deductive program verification based on permission-based separation logic, which is supported by the program verifier VerCors. To the best of our knowledge, we are the first to verify functional correctness of the parallel stream compaction and summed-area table algorithms for an arbitrary array size, using tool support.

ABSTRACT. CafeOBJ is a language for writing formal specifications of software and hardware systems. It implements equational logic by rewriting and has been used to verify properties of systems using both proof scores and theorem proving. In this paper, we present CiMPG+F, an extension of the CafeInMaude interpreter that, for a large class of CafeOBJ specifications, (i) generates complete proofs from scratch and (ii) fixes incomplete proof scores. CiMPG+F allowed us to prove from scratch the correctness of different protocols, giving us confidence in the %applicability of the approach.

ABSTRACT. Logical frameworks are often equipped with an extensional mechanism to define new symbols. The definitional mechanism is expected to be conservative, i.e. it shall not introduce new theorems of the original language. The theorem proving framework Isabelle implements a variant of higher-order logic where constants may be ad-hoc overloaded, allowing a constant to have different definitions for non-overlapping types. In this paper we prove soundness and completeness for the logic of Isabelle/HOL with general (Henkin-style) semantics, and we prove model-theoretic and proof-theoretic conservativity for theories of definitions.

ABSTRACT. Replicated Data Types (RDTs) have been introduced as an abstraction for dealing with weakly consistent data stores, which may (temporarily) expose multiple, inconsistent views of their state. In the literature, RDTs are usually presented in set-theoretical terms: Only recently different specification flavours have been proposed, among them a denotational formalism that inter alia captures specification refinement. So far, however, no abstract model has been proposed for the implementations and their correctness with respect to specifications. This paper fills the gap: We give categorical constructions for distilling an operational model from a specification, as well as its implementations. Then we define a notion of implementation correctness via simulation. This improves and simplifies the current set-theoretical approaches.

ABSTRACT. Hybrid programs combine digital control with differential equations, and naturally appear in a wide range of application domains, from biology and control theory to real-time software engineering. The entanglement of discrete and continuous behaviour inherent to such programs goes beyond the established computer science foundations, producing challenges related to e.g. infinite iteration and combination of hybrid behaviour with other effects. A systematic treatment of hybridness as a dedicated computational effect has emerged recently; in particular, a generic idealized functional language HybCore with a sound and adequate operational semantics has been proposed. The latter semantics however did not provide hints to implementing HybCore as a runnable language, suitable for hybrid system simulation (e.g. the semantics features rules with uncountably many premises). We introduce an imperative counterpart of HybCore, whose semantics is simpler and runnable, and yet intimately related with the semantics of HybCore at the level of hybrid monads. We then establish a corresponding soundness and adequacy theorem. To attest that the resulting semantics can serve as a firm basis for the implementation of typical tools of programming oriented to the hybrid domain, we present a web-based prototype implementation to evaluate and inspect hybrid programs, in the spirit of GHCi for Haskell and UTop for OCaml. The major asset of our implementation is that it formally follows the operational semantic rules.

ABSTRACT. We extend the λ-calculus with constructs suitable for relational and functional-logic programming: non-deterministic alternative, fresh variable introduction, and unification of expressions. In order to be able to unify lambda-expressions and still obtain a confluent theory, we depart from related approaches, such as λProlog, in that we do not attempt to solve higher-order unification. Instead, abstractions are decorated with a location, which intuitively may be understood as its memory address, and we impose a simple invariant: abstractions in the same location must be equal. This allows us to formulate a confluent small-step operational semantics which only performs first-order unification and does not require strong evaluation (below lambdas). We propose a simply typed version of the system. Moreover, a denotational semantics for the calculus is proposed the reduction is shown to be sound with respect to the denotational semantics.

ABSTRACT. As part of the design of a space mission, an important part is the design of so-called flight rules. Flight rules express constraints on various parts and processes of the mission, that if followed, will reduce the risk of failure. One such set of flight rules constrain the format of command sequences regularly (e.g. daily) sent to the spacecraft to con- trol its next near term behavior. We present a high-level view of the automated flight rule checker Frc for checking command sequences sent to NASA’s LADEE Lunar mission spacecraft, used throughout its entire mission. A command sequence is in this case essentially a program (a sequence of commands) with no loops or conditionals, and it can there- fore be verified with a trace analysis tool. Frc is implemented using the TraceContract runtime verification tool, an internal Scala DSL for checking event sequences against “formal specifications”. The paper illustrates this untraditional use of runtime verification in a real con- text, with strong demands on the expressiveness and flexibility of the specification language, illustrating the advantages of an internal DSL.