The Coq mailing list

[Ashish Darbari <ashish.darbari AT gmail.com>]

Axiomise has launched a new on-demand course on applied formal methods. The course provides an in-depth introduction to formal verification covering theorem proving, model checking and equivalence checking using HOL 4, and model checking tools from Cadence, Synopsys and Siemens EDA (formerly Mentor Graphics).

The course can be taken by a graduate student in CS/EE/ECE/Maths/Physics. We only assume familiarity with basic digital design using Verilog/VHDL. If you're already familiar with theorem provers and would like to know how to drive model checkers to find corner-case bugs in designs with 100 million flip-flops and more, this would be a great introduction. If you are a model checking person and would like to see how easy it is to get started proving theorems with HOL like provers, then there are plenty of demos teaching just that. Currently, we use HOL 4, but in the future, we will be putting more material in HOL Light and Coq.

The course consists of 55 modules, including videos, reference material, downloadable source code to play and interactive quizzes. If you like to take a final exam and pass with a 70% grade, you can get a certificate. The course is totally focussed on problem-solving, and how to apply formal on projects?

The course is priced at £500, but with an introductory discount of 40%, you can have it at even a greater value. For students, there is an additional discount of 20%.

More information is available from https://elearn.axiomise.com

Ashish

-- 

Dr Ashish Darbari, FBCS, FIETE, DPhil (Oxon)
Founder & CEO
ashish.darbari AT axiomise.com
Axiomise Ltd. Company No: 11016128
71-75 Shelton Street
WC2H 9JQ

London, UK