Days: Tuesday, December 2nd Wednesday, December 3rd Thursday, December 4th Friday, December 5th
View this program: with abstractssession overviewtalk overview
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.
View this program: with abstractssession overviewtalk overview
| 09:00 | Safe Evolution of Smart Contracts Supported by LLMs and Bounded Model Checking |
| 11:00 | State-based Security and Time-Inserting Supervisors (abstract) |
| 11:30 | A Modular Orthogonal Integration of Operational and Prescriptive Timing Requirements using TASTD (abstract) |
| 12:00 | A Proof of the De Zolt Postulate in Three-dimensional Space (abstract) |
| 16:00 | Bridging the B-Method and ACSL: Towards Verified C Code (abstract) PRESENTER: Fagner Dias |
| 16:30 | A Research Agenda for the Living SysML v2 Blueprint: Toward Executable, Verifiable, and Navigable System Models (abstract) |
| 17:00 | Formal Verification of Epistemic States with Uncertainty in Multi-Agent Systems (abstract) |
View this program: with abstractssession overviewtalk overview
| 09:00 | Exploring Modelling Language Engineering |
| 11:00 | The Turner 2-Strings Machines (abstract) |
| 11:30 | Deriving Sound Test Scripts from Requirements written in a Controlled Natural Language (abstract) |
| 12:00 | Executable Conformance Testing Theories: from Theory to Practice and Back (abstract) |
| 14:00 | Formal Development of a Safety Controller for Machine Learning Outputs in Vital Railway Systems (abstract) |
| 14:30 | Industry talk (TBA) |
| 15:00 | Industry panel |
View this program: with abstractssession overviewtalk overview
| 09:00 | Formal Reasoning for Assuring Product Lines of Complex Systems |
| 11:00 | Inference of Deterministic Finite Automata via Q-Learning (abstract) |
| 11:30 | Availability Model and Evaluation of Bus Rapid Transit Surveillance System (abstract) |
| 12:00 | Resource Contracts for Active Objects (abstract) |