Design by Contract in Practice: A Guided Tour of Verified Java Programs with OpenJML

Correctness is not a luxury—it is a necessity for dependable software systems. Yet, testing alone can never prove that a program always behaves as intended. The Design by Contract principle offers a pragmatic way to bridge programming and formal reasoning, by making software specifications explicit and checkable.

This mini-course introduces the Java Modeling Language (JML) and the OpenJML verification tool through a hands-on, example-driven journey. Participants will learn how to specify contracts, invariants, and loop properties, and how to use OpenJML to automatically verify that Java implementations respect these specifications.

Beyond the technical aspects, the course aims to inspire a mindset shift: that formal verification is not an abstract academic exercise, but a practical and empowering technique for programmers who want to make their code provably trustworthy. By the end, participants will be able to write Java programs with precise contracts and use OpenJML to verify that these contracts are correctly implemented.

Introduction to formal verification for hardware design

This course introduces participants to essential formal verification techniques for hardware projects using Cadence Jasper, the industry-leading platform for formal verification. Participants will learn fundamental concepts of hardware functional verification and basic principles of formal verification methodologies using the market's most advanced solutions. The curriculum covers key topics including SystemVerilog Assertions (SVA) language for property specification, Sequential Equivalence Checking (SEC) for design comparison, and an introduction to formal verification methodologies. Students will have direct contact with the tool's main functionalities through guided practical exercises. Participants will also be introduced to the tool's C/C++ capabilities and learn basic concepts for verification between C/C++ models and RTL implementations. By the end of this course, participants will have the initial knowledge needed to begin exploring formal verification in the hardware development world.