We present λλ1, a programming language for silicon photonics. λλ uses a linear type system to encode the physical constraints of optics, rejecting unrealizable programs at compile time. The compiler lowers well-typed programs to a graph-based intermediate representation, then solves a constrained embedding problem to map these graphs onto arbitrary silicon photonic switch targets while minimizing signal loss. We validate λλ on a commercial photonic switch, demonstrating correct operation for circuit switching, time-varying rotor switching and analog in-network computation. Across various hardware targets and programs, the λλ compiler scales to silicon photonic switches with over 100,000 programmable elements and handles switch programs with 128 input-output pairs. Finally, we develop a synthesizer to automatically generate λλ programs from high-level specifications, allowing users to program photonic hardware without reasoning about optical primitives.

Many natural program correctness properties can be stated in terms of symmetries, but existing formal methods have little support for reasoning about such properties. We consider how to formally verify a broad class of symmetry properties expressed in terms of group actions. To specify these properties, we design a syntax for group actions, supporting standard constructions and a natural notion of entailment. Then, we develop a Hoare-style logic for verifying symmetry properties of imperative programs, where group actions take the place of the typical pre- and post-condition assertions. Finally, we develop a prototype tool SymVerif, and use it to verify symmetry properties on a series of handcrafted benchmarks. Our tool uncovered an error in a model of a dynamical system described by McLachlan and Quispel [Acta Numerica 2002].

Security protocols are essential building blocks of modern IT systems. Subtle flaws in their design or implementation may compromise the security of entire systems. It is, thus, important to prove the absence of such flaws through formal verification. Much existing work focuses on the verification of protocol models, which is not sufficient to show that their implementations are actually secure. Verification techniques for protocol implementations (e.g., via code generation or model extraction) typically impose severe restrictions on the used programming language and code design, which may lead to sub-optimal implementations. In this paper, we present a methodology for the modular verification of strong security properties directly on the level of the protocol implementations. Our methodology leverages state-of-the-art verification logics and tools to support a wide range of implementations and programming languages. We demonstrate its effectiveness by verifying memory safety and security of Go implementations of the Needham-Schroeder-Lowe, Diffie-Hellman key exchange, and WireGuard protocols, including forward secrecy and injective agreement for WireGuard. We also show that our methodology is agnostic to a particular language or program verifier with a prototype implementation for C.