AdaCore Blog

Building High-Assurance Software without Breaking the Bank

by AdaCore Admin

AdaCore will be hosting a joint webcast next Monday 12th December 2pm ET/11am PT with SPARK experts Yannick Moy and Rod Chapman. Together, they will present the current status of the SPARK solution and explain how it can be successfully adopted in your current software development processes.

Attendees will learn:

  • How to benefit from formal program verification
  • Lessons learned from SPARK projects
  • How to integrate SPARK into existing projects
  • Where to learn about SPARK
  • Why "too hard, too costly, too risky" is a myth

The late computer scientist Edsger Dijkstra once famously said "Program testing can be used to show the presence of bugs, but never to show their absence." This intrinsic drawback has become more acute in recent years, with the need to make software "bullet proof" against increasingly complex requirements and pervasive security attacks. Testing can only go so far. Fortunately, formal program verification offers a practical complement to testing, as it addresses security concerns while keeping the cost of testing at an acceptable level.

Formal verification has a proven track record in industries where reliability is paramount, and among the available technologies, the SPARK toolset features prominently. It has been used successfully for developing high confidence software in industries including Aerospace, Defense, and Air Traffic Management. SPARK tools can address specific requirements for robustness (absence of run-time errors) and functional correctness (contract-based verification) that are relevant in critical systems, including those that are subject to certification requirements.

You can join us for this webinar by registering here.

Posted in #Formal Methods    #SPARK