Automatic program verification has made tremendous strides, but is not yet for the masses. How do we make it less painful? This article addresses one of the obstacles: the need to specify explicit "frame clauses", expressing what properties are left unchanged by an operation. It is fair enough to ask the would-be (human) prover to state what each operation changes, and how, but the (mechanical) prover also requires knowledge of what it does not change. The process of specifying and verifying these properties is tedious and error-prone, and must be repeated whenever the software evolves. it is also hard to justify, since all the information about what the code changes is in the code itself. The AutoFrame tool presented here performs this analysis entirely automatically. It applies to object-oriented programming, where the issue is compounded by aliasing: if x is aliased to y, any update to x.a also affects y.a, even though the updating instruction usually does not even mention y. This aspect turns out to be the most delicate, and is addressed in AutoFrame by taking advantage of a companion tool, AutoAlias, which performs sound and sufficiently precise alias analysis, also in an entirely automatic way. Some practical results of AutoFrame so far are: (1) the automatic reconstruction (in about 25 seconds on an ordinary laptop) of the exact frame clauses, a total of 169 clauses, for an 8,000-line data structures and algorithms library which was previously (with the manually written frame clauses) verified for functional correctness using a mechanical program prover; and (2) the automatic generation (in less than 4 minutes) of frame conditions for a 150,000-line graphical and GUI library. The source code of AutoFrame and these examples are available for download.
 The Spec# programming system is a new attempt at a more cost effective way to develop and maintain high-quality software. This paper describes the goals and architecture of the Spec# programming system, consisting of the object-oriented Spec# programming language, the Spec# compiler, and the Boogie static program verifier. The language includes constructs for writing specifications that capture programmer intentions about how methods and data are to be used, the compiler emits run-time checks to enforce these specifications, and the verifier can check the consistency between a program and its specifications. This monograph addresses the use of formal specification languages and supporting tools. Concentrating on the Larch specification work taking place at DEC and MIT, it discusses the use of formal specifications in program development and introduces the notation of mathematical logic. Many state-based specification languages, including the Java Modeling Language (JML), contain at their core specification constructs familiar to most undergraduates: e.g., assertions, pre- and postconditions, and invariants. Unfortunately, these constructs are not sufficiently expressive to permit formal modular verification of programs written in modern object-oriented languages like Java. The necessary extra constructs for specifying an object-oriented module include (perhaps the less familiar) frame properties, datagroups, and ghost and model fields. These constructs help specifiers deal with potential problems related to, for example, unexpected side effects, aliasing, class invariants, inheritance, and lack of information hiding. This tutorial paper focuses on JML's realization of these constructs, explaining their meaning while illustrating how they can be used to address the stated problems. Dafny is a programming language and program verifier. The language includes specification constructs and the verifier checks that the program lives up to its specifications. These tutorial notes give some Dafny programs used as examples in the tutorial. Auto-active verifiers provide a level of automation intermediate between fully automatic and interactive: users supply code with annotations as input while benefiting from a high level of automation in the back-end. This paper presents AutoProof, a state-of-the-art auto-active verifier for object-oriented sequential programs with complex functional specifications. AutoProof fully supports advanced object-oriented features and a powerful methodology for framing and class invariants, which make it applicable in practice to idiomatic objectoriented patterns. The paper focuses on describing AutoProof's interface, design, and implementation features, and demonstrates AutoProof's performance on a rich collection of benchmark problems. The results attest AutoProof's competitiveness among tools in its league on cutting-edge functional verification of object-oriented programs. JML is a behavioral interface specification language tailored to Java(TM). Besides pre- and postconditions, it also allows assertions to be intermixed with Java code; these aid verification and debugging. JML is designed to be used by working software engineers; to do this it follows Eiffel in using Java expressions in assertions. JML combines this idea from Eiffel with the model-based approach to specifications, typified by VDM and Larch, which results in greater expressiveness. Other expressiveness advantages over Eiffel include quantifiers, specification-only variables, and frame conditions.This paper discusses the goals of JML, the overall approach, and describes the basic features of the language through examples. It is intended for readers who have some familiarity with both Java and behavioral specification using pre- and postconditions. Abstract We describe the basic structure of an environment for proving Java programs annotated with JML specifications. Our method is generic with respect to the API, and thus well suited for JavaCard applets certification. It involves three distinct components: the Why tool, which computes proof obligations for a core imperative language annotated with pre- and post-conditions, the Coq proof assistant for modeling the program semantics and conducting the development of proofs, and finally the Krakatoa tool, a translator of our own, which reads the Java files and produces specifications for Coq and a representation of the semantics of the Java program into Why ’s input language.  