Summary form only given. When developing products or solutions in industry and assessing their quality, formal methods provide the most rigorous tools for checking for safety and security flaws. In this talk we share our first-hand general experience in this area, and furthermore provide some details of a project specifying and modeling electronic distribution software (EDS). We comment on the motivation, practice, and impact of applying formal methods in industry, including the role of evaluation and certification according to the common criteria. Second, we give an overview of which modeling and verification techniques we have found useful so far, for which reasons. Third, we present some ongoing work on specifying and modeling EDS. The aim of EDS is to alleviate the burden of distributing initial and update versions of software in modern airplanes. By now this is done physically using disks, which is becoming unbearable with the amount of software steadily increasing. EDS is currently under standardization in the ARINC 666 committee, which includes the main players Boeing and Airbus, as well as their maintenance partners. Obviously, electronic shipment via cable-based and wireless connections faces severe security threats, such that one should better check with maximal scrutiny whether the mechanisms actually fulfill the security goals required, in particular integrity and authenticity.

Abstract This article presents a Hoare‐style calculus for a substantial subset of Java Card, which we call Java $^{\ell ight}$ . In particular, the language includes side‐effecting expressions, mutual recursion, dynamic method binding, full exception handling, and static class initialization. The Hoare logic of partial correctness is proved not only sound (w.r.t. our operational semantics of Java $^{\ell ight}$ , described in detail elsewhere) but even complete. It is the first logic for an object‐oriented language that is provably complete. The completeness proof uses a refinement of the Most General Formula approach. The proof of soundness gives new insights into the role of type safety. Further by‐products of this work are a new general methodology for handling side‐effecting expressions and their results, the discovery of the strongest possible rule of consequence, and a flexible Call rule for mutual recursion. We also give a small but non‐trivial application example. All definitions and proofs have been done formally with the interactive theorem prover Isabelle/HOL. This guarantees not only rigorous definitions, but also gives maximal confidence in the results obtained. Copyright © 2001 John Wiley & Sons, Ltd.

HOLCF is the definitional extension of Church's Higher-Order Logic with Scott's Logic for Computable Functions that has been implemented in the theorem prover Isabelle. This results in a flexible setup for reasoning about functional programs. HOLCF supports standard domain theory (in particular fixpoint reasoning and recursive domain equations), but also coinductive arguments about lazy datatypes. This paper describes in detail how domain theory is embedded in HOL, and presents applications from functional programming, concurrency and denotational semantics.

Javalight is a large sequential sublanguage of Java. We formalize its abstract syntax, type system, well-formedness conditions, and an operational evaluation semantics. Based on this formalization, we can express and prove type soundness. All definitions and proofs have been done formally in the theorem prover Isabelle/HOL. Thus this paper demonstrates that machine-checking the design of non-trivial programming languages has become a reality.