AdaCore Blog

7 entries tagged with #Workshop

by Fabien Chouteau

Getting Rid of Rust with Ada

There are a lot of DIY CNC projects out there (router, laser, 3D printer, egg drawing, etc.), but I never saw a DIY CNC sandblaster. So I decided to make my own.

#STM32    #embedded    #ARM    #Makers   

by Yannick Moy

Two Days Dedicated to Sound Static Analysis for Security

​AdaCore has been working with CEA, Inria and NIST to organize a two-days event dedicated to sound static analysis techniques and tools, and how they are used to increase the security of software-based systems. The program gathers top-notch experts in the field, from industry, government agencies and research institutes, around the three themes of analysis of legacy code, use in new developments and accountable software quality. Here is why it is worth attending.

#SPARK    #Frama-C    #Security    #Formal Methods    #Static Analysis   

by Yannick Moy

Verified, Trustworthy Code with SPARK and Frama-C

Last week, a few of us at AdaCore have attended a one-day workshop organized at Thales Research and Technologies, around the topic of "Verified, trustworthy code - formal verification of software". Attendees from many different branches of Thales (avionics, railway, security, networks) were given an overview of the state-of-practice in formal verification of software, focused on two technologies: the SPARK technology that we develop at AdaCore for programs in Ada, and the Frama-C technology developed at CEA research labs for programs in C. The most interesting part of the day was the feedback given by three operational teams who have experimented during a few months with either SPARK (two teams) or Frama-C (one team). The lessons learned by first-time adopters of such technologies are quite valuable.

#SPARK    #Formal Methods   

by AdaCore Admin

Project P Open Workshop

Project-P Open Workshop

#QGen    #ProjectP    #Workshop    #---    #Code generation   

by Yannick Moy

A Building Code for Building Code

In a recent article in Communications of the ACM, Carl Landwehr, a renowned scientific expert on security, defends the view that the software engineering community is doing overall a poor job at securing our global information system and that this is mostly avoidable by putting what we know works to work, to the point that most vulnerabilities could be completely avoided by design if we cared enough. Shocking! Or so it should appear.

#Ada    #SPARK    #Static Analysis    #Security   

by Yannick Moy

Use of SPARK in a Certification Context

Using SPARK or any other formal method in a certification requires that the applicant agrees with the certification authority on the verification objectives that this use of formal methods allows to reach, and how this is obtained and documented. In order to facilitate this process, the participants to the workshop on Theorem Proving in Certification have produced a draft set of guidelines, now publicly available.

#Formal Verification    #Certification   

by Yannick Moy

Case Study for System to Software Integrity Includes SPARK 2014

My colleague Matteo Bordin will present at the upcoming Embedded Real Time Software and Systems conference in Toulouse in February a case study showing how formal verification with SPARK can be included in a larger process to show preservation of properties from the system level down to the software level. The case study is based on the Nose Gear challenge from the Workshop on Theorem Proving in Certification.

#Formal Verification    #Certification    #SPARK