The Curious Engineer

All blogs / Other languages

AdaCore Blog

adacore.com/blog

AdaCore is the leading provider of commercial software solutions for Ada, C and C++ — helping developers build safe and secure software that matters.

Other languagesSecurityEmbedded / microcontrollersRust

’10’15’20’25
Posts
647 from 14 May 2007 to 30 Oct 2026
Posting
weekly (64 in the last year)
Kind
company blog
Feed
https://www.adacore.com/feed.rss

2026 57

  1. Rotate, Sort, Last Column: The Burrows Wheeler Transform in SPARK
  2. Foundational Cryptography in SPARK
  3. Try Taint Analysis in CodeSonar for Ada
  4. Proving Kruskal’s Algorithm in SPARK: When Generative AI Meets Formal Verification
  5. Security Is a Team Sport. Give Your Engineers the Tools to Win.
  6. AdaCore Partners with Prologin to Support the Girls Can Code! Initiative
  7. RustConf 2026 - Montreal
  8. Experiencing the Journey Towards Memory Safety
  9. Catching Defects Before They Fly
  10. Rust for DO-178C and ISO 26262
  11. From Raw Arrays to Typed Ownership: A Layered Allocator in SPARK
  12. Ada-FPGA-Programmer: Configuring a Tang Nano 9K from Bare-Metal Ada, Built by Students
  13. Breaking the Triage Bottleneck: When GNAT SAS meets GNAT DAS
  14. GNAT Foundry Intersection: Demonstrating Trustworthy AI Development
  15. Wishbone-NPU: A Neural Processing Unit for RISC-V Soft-Cores, Built by Students
  16. Ada SPARK Office Hours
  17. Specifications Matter: The Case for SPARK in the Undergraduate Curriculum
  18. Multiple Levels of Models and Refinement
  19. AI Will Multiply Your Code Output. It Will Also Multiply Your Liability
  20. Jun 18, 2026Mark HermelingAbstract Interpretation vs Agentic AIThis blog explores how static analysis compares to using an LLM to find defects in source code, and when would you use one over the other.
  21. memcp: token-efficient, multi-project, multi-surface external memory for AI agents written in SPARK Silver
  22. Jun 23, 2026Dana Binkley, Monika KurovszkyInternational Women in Engineering Day: My Path to SuccessHear about what it’s like to work in technical roles at AdaCore from our Director of Field Engineering and a Senior Software Engineer.
  23. SPARK Doesn't Comply With MISRA C. It Makes Most of It Moot
  24. Jun 25, 2026Fabien ChouteauAnnouncing the 2026 Ada/SPARK Crate of the Year AwardWe're happy to announce the sixth edition of our programming awards, The Ada/SPARK Crate of the Year Award!
  25. Prototyping memory safety in your automotive stack — in weeks, not years
  26. Jun 30, 2026Mark HermelingHow Language Design Impacts SecurityIn this blog we have created a table listing each CWE and/or CWE class, along with how each programming language addresses that category.
  27. Building and evolving multi-language systems with confidence using GNATpolyglot
  28. Jul 01, 2026M. Anthony AielloMARS Rover GNCSee how SPARK both helps with autonomy- and control-relevant problems on the Mars Rover and integrates productively into agentic AI.
  29. Your Compiler Is Part Of Your Software Supply Chain
  30. Three Ways SPARK Catches Bugs Before Your Hardware Does
  31. Apr 14, 2026M. Anthony AielloChallenging Agentic AI with SPARK using OpenUxAS“How well does generative AI do with writing Ada?” The simple answer is: “quite well!” But the details are also interesting, so I encourage you to…
  32. Apr 16, 2026Claire DrossFormally Verified Hashed Sets in Ada SPARKThis blog explores the formal verification of an implementation of bounded hashed sets in Ada SPARK.
  33. Apr 23, 2026Mark HermelingGetting Started in Functional Safety with RustExpert-Led Rust Training for Safety-Critical Teams
  34. Apr 28, 2026Mark HermelingThe Compliance Trap: Why More Code, More Connectivity, and More Regulation Are Colliding (and What to Do About It)Software development teams in embedded systems must navigate between stricter regulations, rising customer demands, and unfulfilled AI promises to…
  35. Apr 30, 2026Claire DrossReasoning about Linked Structures in an ArrayReasoning about linked data structures within an array is complicated, requiring high-level concepts such as reachability and inductive reasoning.…
  36. May 05, 2026Mark HermelingAda on Zephyr: How the Alire Skill Wires It TogetherIntegrating Ada code into Zephyr can be simple as a single LLM prompt and a single make command. This post is about what happens between make and a…
  37. May 12, 2026Mark Hermeling, Sean EvoyFrom CodeSecure to AdaCore: Our Journeys in Product and Technical MarketingHear from Mark Hermeling and Sean Evoy about how they’ve found their transition from CodeSecure to joining AdaCore as part of last year’s merger.
  38. May 13, 2026Matthieu EyraudUnit Testing with Google Test and GNATcoverageThis blog explores the use of Google Test to drive our unit test cases, combined with GNATcoverage to measure our code coverage.
  39. May 28, 2026Claire DrossInformation Hiding and Context Management in SPARKA previous blog explored the verification of the formal hashed sets package in SPARKlib. This post will explain the techniques used to simplify the…
  40. Jun 02, 2026Ronan DesplanquesProving asymptotic time complexity bounds with SPARKThis blog explores whether SPARK be used to prove something about the time complexities of Linear_Search and Binary_Search
  41. Jun 11, 2026Tobias ReiherRunning cargo test on Bare Metal: Adding libtest Support to GNAT Pro for RustThis post walks through how we added libtest support to GNAT Pro for Rust using the AMD Zynq UltraScale+ MPSoC as the concrete example.
  42. Jun 16, 2026Jose RuizFrom Host to Target: Consolidating Code Coverage Across Execution EnvironmentsThis blog walks through a concrete example of how to get a unified code coverage picture from two separate execution environments.
  43. Feb 17, 2026Fabien ChouteauAda/SPARK Crate Of The Year 2025 Winners Announced!The annual Ada/SPARK Crate of the Year Awards celebrate the outstanding contributions made to the growing Ada/SPARK ecosystem through Alire.
  44. Feb 24, 2026Johannes KanigScalable SPARK ProofsThis blog post explains how a SPARK function for counting character occurrences was formally verified to ensure both absence of runtime errors and…
  45. Mar 02, 2026Mark HermelingGNATpolyglot: Mastering Multiple LanguagesThis blog introduces GNATpolyglot, a new capability in the GNAT Pro toolchain.
  46. Mar 03, 2026Mark HermelingFormal Methods To Improve Code QualityMemory safety is rightly a major focus in embedded systems. This article outlines the difference between static and dynamic memory safety, and how…
  47. Mar 05, 2026Frederic Leger, Nicolas RocheAdaCore Software Supply Chain Security EvolutionAdaCore has elevated its software supply chain practices and now generates its deliverables in a CMMC Level 2 and SLSA build level 3 compliant…
  48. Mar 10, 2026M. Anthony AielloGNAT IQAdaCore is delighted to announce unlimited access to GNAT IQ, AdaCore’s AI-powered GNAT documentation chatbot, for all of our current customers.
  49. Mar 19, 2026Kyriakos GeorgiouHardware-Driven Security: Can CHERI Fix the "Blind Spots" of Software Testing?This work combines fuzz testing with CHERI hardware. Unlike heuristic-based sanitizers, CHERI uses hardware-enforced capabilities - pointers with…
  50. Mar 24, 2026Tobias ReiherEnabling Rust on the AMD Zynq UltraScale+ MPSoCIn this post, we’re sharing our journey of building a dedicated crate that provides support for the AMD Zynq UltraScale+ MPSoC.
  51. Mar 26, 2026Olivier HenleyHow Evolutek Used Ada to Build Their CanSatAdaCore supports practical engineering projects that help students apply technical concepts to real-world problems. As part of this effort, AdaCore…
  52. Mar 31, 2026Mark HermelingMigrating C to Ada SPARK with Agentic AI: A Practical PlaybookAgentic AI can enable teams to re-use existing code bases and carefully decide which parts to translate into Ada SPARK, avoiding problems caused by…
  53. Apr 07, 2026Kyriakos GeorgiouFuzz Everything, Everywhere, All at Once: Scaling Security with GNATfuzzIf you are developing high-integrity systems, GNATfuzz can provide the extra layer of security analysis required by modern certification standards.
  54. Apr 09, 2026Mark HermelingEscaping the Haystack: CI/CD for Embedded SystemsHow fast feedback loops, smart abstraction, and disciplined pipelines change the way embedded software teams work and ship.
  55. Nov 25, 2025Andrea BristolHighlights from the High Integrity Software Conference 2025The High Integrity Software Conference (HISC) returned to the International Convention Centre Wales (ICC Wales) on 13 November 2025. HISC once again…
  56. Oct 08, 2025Elisa BellFrom Interns to New Hires: Writing the Next Chapter at AdaCoreMathéo Rome, Anne-Lise Magagnin, and Julian Coux share their experiences as interns at AdaCore, where they worked on independent projects while being…
  57. Oct 27, 2025Andrea BristolWhat would Ada think of the rise in Ada Language Popularity?This Ada Lovelace Day, we are celebrating what has been a positive year for the Ada Programming Language, and we ask ourselves, what would Ada think?…

2025 37

  1. Nov 03, 2025Ben BrosgolA New Booklet on AdaCore Technologies for Airborne SoftwareAdaCore has posted a new version of its booklet AdaCore Technologies for Airborne Software: Supporting certification and tool qualification for…
  2. Nov 18, 2025Andrea BristolProving Safety at Scale: SPARK, RISC-V, and NVIDIA’s Security Strategy
  3. Dec 01, 2025Fabien ChouteauAnnouncing Advent of Ada/SPARK 2025: Coding for a Cause!Advent of Ada/SPARK is back! Solve Advent of Code 2025 challenges in Ada/SPARK and help us raise up to $5,000 for Ada Developers Academy.
  4. Dec 11, 2025Mark HermelingMISRA for Memory SafetyMISRA is the top coding standard for C/C++ in embedded systems, but its full adherence is often impractical. Its rules can be split into three…
  5. Jan 08, 2026Andrea BristolSurprising Places Where Ada Is UsedAda has entered the top 10 of the PYPL index, reflecting renewed interest in a language long associated with safety-critical and real-time systems.…
  6. Dec 15, 2025Andrea BristolYear in Review 2025: A Transformative Year for High-Integrity Software at AdaCoreAs 2025 comes to a close, it’s clear that this has been one of the most significant years in AdaCore’s history. Our work to help organisations build…
  7. Jan 13, 2026Romain GoraRust Memory Management: The Playroom AnalogyThis article builds on 'Introduction to Ada: a project-based exploration with rosettas', which walked through the development of a fun, end-to-end…
  8. Jan 15, 2026Fabien ChouteauAdvent of Ada/SPARK 2025 ResultsOn December 1st, we called the Ada and SPARK programmers community to take on a challenge for a good cause. It is now time for the results!
  9. Feb 04, 2026Mark HermelingFormal Methods Practice and TheoryFormal methods offer a rigorous way to connect requirements to implementation, enabling developers to prove key properties such as the absence of…
  10. May 23, 2025Tobias ReiherBuilding a Virtual Mars Rover with SPARK and RustWe have taken our Ada Mars Rover demo, featuring a physical robot driven by formally verified SPARK software, to the next level by introducing a…
  11. Jun 10, 2025Charis Fisher, Cléa MendelewskiRegulating Innovation: A Day in the Life of an In-House Lawyer in TechAdaCore Senior Corporate Counsel, Sarah Wallace, explains why partnership and collaboration are integral to her role practicing in-house law in a…
  12. Jun 16, 2025Stephen HedrickNavigating Mars with Rust: Developing an Autonomous Pathfinding RoverThis blog showcases how Rust was used to implement the D*-Lite pathfinding algorithm for an autonomous Mars rover simulation. It highlights Rust’s…
  13. Jun 26, 2025Edgar DelaporteImproving SPARK Counter Examples with Fuzzing and Code AnalysisWhen analyzing a SPARK program with GNATprove, some verification conditions might remain unproven, whether because of a defect in the user’s code,…
  14. Jul 01, 2025Andrea BristolWhat’s All the Fuzz About?In this blog, we discover Fuzz Testing and how GNATFuzz can be used as part of AdaCore’s GNAT Dynamic Analysis Suite.
  15. Jul 08, 2025Fabien ChouteauSolving Sudoku with AdaSATOriginally, constraint solving in Libadalang was handled by several ad-hoc solvers built specifically for different parts of the type system. These…
  16. Jul 10, 2025Fabien ChouteauAnnouncing the 2025 Ada/SPARK Crate of the Year AwardWe're happy to announce the fifth edition of our programming awards, The Ada/SPARK Crate of the Year Award! The Alire package manager is a game…
  17. Jul 18, 2025M. Anthony AielloRevisiting the Mars Rover Safety MonitorIn the blog "Let's Write a Safety Monitor for a Mars Rover", I made a big assumption in the procedure that moves that Rover forward; here, I relax…
  18. Jul 31, 2025Andrea BristolAda and Rust are highlighted by the NSA and CISA in Memory Safe Language Information SheetGovernments trust memory-safe languages like Ada and Rust — so do we. See why memory safety is essential for secure systems.
  19. Aug 20, 2025Andrea BristolFormal Methods in Practice: Government Lessons in Resilience and Adoption ContextAs the software landscape grows ever more complex and interconnected, the demand for resilient, high-assurance systems continues to rise, especially…
  20. Sep 07, 2025Romain GoraIntroduction to Ada: a project-based exploration with rosettasDiscover Ada through a fun, project-based tutorial! Learn the language’s clarity, safety, and modern features while building an SVG rosetta…
  21. Sep 10, 2025Stephen HedrickNavigating Mars with Rust: Helping the Rover See In Computer VisionThis blog explores how Rust enables computer vision on a Mars rover, overcoming hardware limits to deliver reliable obstacle detection and autonomous…
  22. Feb 04, 2025Olivier HenleyOpen-Source Ada: From Gateware to ApplicationThe Neorv32 BIOS project demonstrates how Ada can serve as a powerful alternative to C in open-source embedded development. Using a fully open-source…
  23. Feb 18, 2025Ben BrosgolVerifying FACE® Conformance for Ada SoftwareThe FACE® approach (Future Airborne Capability Environment®) is a joint government-industry initiative to reduce system life cycle costs for airborne…
  24. Feb 21, 2025Justin SquirekA new math library for Ada: Neo.SIMDDeveloping a game engine often requires a highly optimized linear algebra library for tasks like physics, camera movement, and AI. While many…
  25. Mar 04, 2025Charis Fisher, Cléa MendelewskiBuilding the Future: My Path from Software Research to LeadershipTo celebrate Global Engineering Day, we’re looking at what it’s like to work as a truly global engineer, collaborating with international colleagues…
  26. Mar 12, 2025Pat RogersAda in Practice, a New Learn CourseA new Learn course is now available, focusing on how to use the Ada language to express common idioms, both language-dependent and -independent.
  27. Mar 21, 2025M. Anthony AielloLet’s Write a Safety Monitor for a Mars Rover!The Ada Mars Rover shouldn’t crash into obstacles. See how we formalized this property, discovered an unstated assumption in our remote-control mode…
  28. Apr 02, 2025Andrea BristolAda is back in the TIOBE Index top 20The March edition of the TIOBE Index shows Ada in the top 20, hitting position 18. This shows a renewed interest in Ada, perhaps due to the increased…
  29. Apr 08, 2025Johannes KliemannCheriBSD: A Showcase for Hardware-Supported SecurityOver the course of the last few years and as part of the 'Edge Avionics' project, funded by the Rapid Capabilities Office (RCO) of the UK Royal Air…
  30. Apr 17, 2025Quentin OchemLet's play '7 differences in Ada'Over the past few years, we've been progressively developing new GNAT extensions for the Ada programming language, which you can follow and…
  31. Apr 22, 2025Andrea BristolSafer with AdaWhat makes our software so vulnerable? The majority of today’s technical systems are largely composed of software. As such, the reliability and…
  32. May 09, 2025Andrea BristolFormal Methods for an Insecure WorldThis article unpacks what it means to be Secure by Design, outlining practical measures for integrating security into the software lifecycle. It…
  33. May 12, 2025Andrea BristolAdaCore and Lynx Software Technologies Reaffirm Longstanding PartnershipAdaCore and Lynx Software Technologies have reaffirmed their longstanding technology partnership to support avionics and defense customers developing…
  34. Oct 08, 2024Andrea BristolAdaCore Memories: the stories behind the first 30 years of AdaCoreAs part of our 30 years of AdaCore celebrations, we spoke to some of our founders to discover the stories that built what we are so proud of…
  35. Sep 27, 2024Quentin OchemShould I choose Ada, SPARK, or Rust over C/C++?At AdaCore, we’re in the business of supporting people who develop high-integrity software, in particular for embedded systems. In terms of…
  36. Oct 29, 2024Gustavo A. Hoffmannlearn.adacore.com: New Advanced Ada contentsSome time ago we announced updates to the learn website. Since then, we've published new contents to the Advanced Journey with Ada course, which we…
  37. Nov 22, 2024Léo GermondGNAT Static Analysis Suite Gitlab Integration - Scaling the pipeline upIn the previous blog post of this series, we set up a GNAT Static Analysis Suite (GNAT SAS) analysis pipeline. This post focuses on the pipeline's…

2024 38

  1. Nov 28, 2024Fabien ChouteauAnnouncing Advent of Ada 2024: Coding for a Cause!We're thrilled to kick off the holiday season with the third edition of Advent of Ada, a programming challenge that not only tests your coding skills…
  2. Dec 05, 2024Charis Fisher, Cléa MendelewskiShaping Success: My Journey from Intern to Managing DirectorEmma Adby discusses her career evolution at AdaCore - from intern in Paris to Global Head of Marketing and UK Managing Director.
  3. Dec 11, 2024Andrea BristolAdaCore’s 2024; Highlights from our 30th year in BusinessAs AdaCore celebrates the start of a new year in business, we reflect on 2024, a year of development and future-proofing combined with consolidating…
  4. Dec 17, 2024Paul ButcherBuilding Safety by Design: CHERI in Critical Systems DevelopmentPaul Butcher, the Secure Avioincs by Design Project Manager for AdaCore, discusses the usage of CHERI in safety-critical software.
  5. Jan 07, 2025César SagaertLearning Ada with raytraced teapotsIntroducing the Ada language with a fun 3D rendering project
  6. Jan 14, 2025Jose RuizGNAT Pro 25: New Features, Platforms, and Tools2025 is a new year of growth for the GNAT Pro family to help people develop safe, secure, and efficient code on a large variety of software and…
  7. Jan 30, 2025Fabien ChouteauAda/SPARK Crate Of The Year 2024 Winners Announced!In 2024 we announced our fourth Ada/SPARK Crate Of The Year Awards. We see the Alire source package manager as a game changer for Ada/SPARK, so we…
  8. Jan 30, 2025Fabien ChouteauAdvent of Ada/SPARK 2024 ResultsAt the end of November, we called the Ada and SPARK programmers community to take on a challenge for a good cause. For each person completing one of…
  9. Jun 17, 2024Fabien ChouteauAnnouncing the 2024 Ada/SPARK Crate of the Year AwardWe're happy to announce the fourth edition of our programming awards, The Ada/SPARK Crate of the Year Award! The Alire package manager is a game…
  10. Jun 24, 2024Charis Fisher, Cléa MendelewskiBuilding a Bright Future: Celebrating International Women in Engineering DayToday we’re showcasing Ashley Gay’s career and how her skills and accomplishments have evolved from an early interest in video games to cross…
  11. Jun 27, 2024AdaCoreAdaCore Experts Present Paris Tech DayJoin us in Paris on Thursday, September 26th, to learn about the latest advancements in high-integrity software from our AdaCore experts.
  12. Jul 22, 2024Kyriakos GeorgiouAdaCore for SCHEME — Safety-Critical Harsh Environment Micro-processing EvolutionAdaCore is excited to announce its participation in the SCHEME (Safety-Critical Harsh Environment Micro-processing Evolution) research project.…
  13. Aug 06, 2024Frederic LegerSecure Supply Chain and vulnerability reports at AdaCoreIn the past few years, attacks compromising software supply chains (MITRE ATT&CK T1195) have become more prominent, with cases such as NotPeya,…
  14. Aug 14, 2024Fabien ChouteauThe use of Ada Language in the Telecommunications IndustryIn this article, Fabien Chouteau explains the importance of secure software in the emerging telecommunications industry.
  15. Aug 22, 2024Jose RuizAdaCore Join Rust Enthusiasts in ParisOn June 25th, I attended the Rust Paris 2024 conference. Among around one hundred Rust enthusiasts and a program filled with captivating subjects and…
  16. Sep 05, 2024Olivier HenleyGetting Started with Renode: Simulating an Ada STM32F429disco Blinky Firmware.I recently watched the talks from the 28th Ada-Europe International Conference on Reliable Software Technologies (AEiC 2024), which was held in…
  17. Sep 13, 2024Fabien ChouteauAda GameDev Part 3: Enjoy Video Games Programming with RaylibIn April 2024 a streamer named Tsoding developed a video game from start to finish in Ada in 20 days. He seemed to have enjoyed the experience, to…
  18. Sep 17, 2024Fabien ChouteauHow GNATkp Safeguards Against Known Compiler IssuesGNAT Pro Assurance customers have access to a special variant of GNATcheck called GNATkp (GNAT Known Problems detector). This tool is packaged with…
  19. Sep 19, 2024Olivier HenleyA new year of Capstones: A Recap of the last ProjectsAs part of the AdaCore GNAT Academic Program, Capstones offers senior higher education students the opportunity to take on challenging and exciting…
  20. Sep 25, 2024Charis Fisher, Cléa MendelewskiThinking Outside The Box: My Journey From Engineer to Technical Account ManagerLearn more about Silvère To-Sah-Be-Nza's journey from Engineering graduate to working with software engineering customers in the field
  21. Feb 05, 2024Nicolas VennerDNSSEC and DMARC Compliance at AdaCoreWhile foundational to the internet, the traditional DNS system has its vulnerabilities. Threats such as DNS spoofing and cache poisoning pose…
  22. Feb 09, 2024Maxim ReznikEnhancing Ada Embedded Development: The Power of Real-Time Logging with RTTEfficient embedded development in Ada relies on powerful tools. Real-time logging plays a pivotal role, enabling live monitoring and analysis. Unlike…
  23. Feb 28, 2024M. Anthony AielloCo-Developing Programs and Their Proof of CorrectnessI am delighted to announce that the Communications of the ACM has published a paper on SPARK: “Co-Developing Programs and Their Proof of…
  24. Mar 06, 2024Fabien ChouteauBACK TO THE BUILDING BLOCKS: AdaCore’s Contributions to Secure and Measurable SoftwareThe focus on enhancing cybersecurity through various technological approaches and methodologies, as detailed in the White House Office of the…
  25. Mar 08, 2024Charis Fisher, Cléa MendelewskiInternational Women’s Day: My Career JourneyEvery 8th March, International Women’s Day is celebrated around the world - it’s a great opportunity to highlight women’s talents, their…
  26. Apr 04, 2024Yannick Moy, Nicolas Venner, Paul Sivac, Tracey GilbertAdaCore Contribution to Reducing GHG EmissionsLike any other company, AdaCore contributes to climate change through its activities. We recognize that it is our responsibility to reduce this…
  27. Apr 09, 2024Fabien ChouteauAda Programming like it's 1985A few days ago, someone posted a request for the Abacus Commodore 64 Ada compiler on the reddit Ada channel. After a quick look at the manual I…
  28. Apr 16, 2024Olivier Appéré, Josue Nava BelloA Fresh Take on DO-178C Software ReviewsThe software review is an essential part of the evidence required for certification according to DO-178C. In this blog post we reflect on the…
  29. May 17, 2024Charis Fisher, Cléa MendelewskiEngineering Abroad: My Global Career JourneyNicolas Setton, our Head of User Experience, has experienced working in multiple different AdaCore offices over his 20+ year engineering career. Find…
  30. May 21, 2024Michael FrankCreating Your Own Ada/SPARK Coding StandardMany of our customers ask if we have a "Coding Standard" that we can provide for writing code in Ada or SPARK. The answer has typically been: "We…
  31. May 24, 2024Jose RuizSecurity Considerations in Light Launcher SoftwareWhen Latitude began creating their small satellite launcher, Zephyr, they recognized the importance of selecting the correct programming language and…
  32. Jun 04, 2024Paul ButcherCYBERUK proves an excellent showcase for AdaCore and Secure Avionics by DesignAt this year's CYBERUK, AdaCore had the privilege of being part of the UKRI Digital Security by Design (DSbD) stand, demonstrating its part of Secure…
  33. Oct 26, 2023Olivier HenleyA little bit of Photoshop® using GNAT for CUDA®Today I want to go over some internal mechanisms of a Photoshop-like application to better illustrate an up-and-coming tech, GNAT for CUDA®,…
  34. Oct 30, 2023Joakim StrandbergAnnouncing Ada binding to the wolfSSL libraryToday, we at wolfSSL (https://www.wolfssl.com/) are happy to announce the availability of an Ada/SPARK binding that enables Ada applications to use…
  35. Nov 10, 2023Forough GoudarziAn Introduction to Memory Safety Concepts and ChallengesThis blog post explains the concept of memory safety and the most common memory errors. Then, it introduces three memory-safe languages that have…
  36. Nov 15, 2023Forough GoudarziMemory Safety in Ada and SPARK through Language Features and Tool SupportThis blog post describes how Ada and SPARK provide memory safety through a combination of language features, run-time checks, and static and dynamic…
  37. Nov 20, 2023Léo GermondBuilding a GNAT SAS analysis pipeline on GitLabThis is the first part of a series in which we’ll implement a GNAT SAS analysis pipeline for Ada code on GitLab by making use of GNAT SAS 24 new…
  38. Dec 01, 2023Fabien ChouteauAnnouncing Advent of Ada 2023: Coding for a Cause!We're thrilled to kick off the holiday season with the second edition of Advent of Ada, a programming challenge that not only tests your coding…

2023 32

  1. Jan 04, 2024Fabien ChouteauAdvent of Ada/SPARK 2023 ResultsAt the end of November we called the Ada and SPARK programmers community to take on a challenge for a good cause. For each person completing one of…
  2. Jan 05, 2024Gustavo A. HoffmannAnnouncing Updates to learn.adacore.comSome time ago, we announced some updates to the learn website. In the meantime, we published the Introduction To Embedded Systems Programming course…
  3. Jan 23, 2024Fabien ChouteauAdaCore Enhances GCC Security with Innovative FeaturesIn a significant stride towards bolstering the security of the open-source ecosystem, AdaCore has recently contributed a set of security hardening…
  4. Jan 29, 2024Ben BrosgolMemory Safety in RustInformally, memory safety in a program means that each data access is well behaved; i.e., is consistent with the item’s data type, does not impinge…
  5. Feb 01, 2024Fabien ChouteauAda/SPARK Crate Of The Year 2023 Winners Announced!In 2023 we announced the third edition of the Ada/SPARK Crate Of The Year Awards. We see the Alire source package manager as a game changer for…
  6. Feb 02, 2024Quentin Ochem, M. Anthony AielloGNAT Static Analysis Suite: A Vision for Static Analysis in AdaYou may have noticed that over the past two years, we have made significant updates to our CodePeer product - the most visible change being the…
  7. May 29, 2023Gustavo A. HoffmannAdvanced Journey with Ada: A Flight in ProgressWe are thrilled to announce the launch of our highly anticipated course, "Advanced Journey with Ada: A Flight in Progress," which explores the…
  8. Jun 30, 2023Claire DrossSPARK, Beyond Normal TerminationWhen teaching SPARK to my students, I generally explain the central position of contracts in formal verification in the following way: Contracts of…
  9. Jul 03, 2023Vadim GodunkoVSS: Cursors, Iterators and MarkersThe VSS (as an abbre­vi­a­tion for Vir­tu­al String Sub­sys­tem) library is designed to pro­vide advanced string and text pro­cess­ing…
  10. Jul 07, 2023Jose RuizGNAT Pro RoadmapEvery year the GNAT Pro product family acquires new members and capabilities, to help our customers develop safer, more secure and more efficient…
  11. Jul 19, 2023AdaCoreAnnouncements around RustAdaCore has two announcements about Rust that we’d like to share with you!
  12. Aug 01, 2023Thijs DreefDesigning a WebAssembly toolchain for Ada/SPARKWebAssembly (Wasm) is a binary instruction format for a stack-based virtual machine, which was designed as a portable compilation target for…
  13. Aug 16, 2023Elsa FerraraFormal Proof on Device Drivers with SPARKProgramming device drivers requires certain practices or operations. These include, for example, the multitude of volatile variables in the code. On…
  14. Aug 18, 2023Pat RogersExtending Priority Inheritance Beyond Protected OperationsThis blog entry shows how to define protected types that extend the language-defined priority inheritance for protected actions to the statements…
  15. Sep 29, 2023Fabien ChouteauAnnouncing the 2023 Ada/SPARK Crate of the Year AwardWe're happy to announce the third edition of our programming awards, The Ada/SPARK Crate of the Year Award! This time with a different approach as…
  16. Oct 03, 2023Elsa FerraraSPARK Tetris on the Raspberry Pi PicoTetris was the first computer game played in space but let's review our ambitions for the time and try to implement it on a Raspberry Pico first. …
  17. Oct 16, 2023Nicolas Roche, Olivier RamonatIdentifying and authorizing users at AdaCoreBack in the 90s when AdaCore was founded, the state of IT security was very different. A unique Unix login and password were enough to connect to a…
  18. Oct 20, 2023Jose RuizBare-metal C++ development environment for certifiable safety-critical applicationsWe are happy to announce the availability of GNAT Pro for C++, a versatile development environment for bare-metal targets capable of supporting…
  19. Jan 31, 2023Fabien ChouteauAda/SPARK Crate Of The Year 2022 Winners Announced!
  20. Feb 02, 2023Fabien ChouteauAdaCore at FOSDEM 2023
  21. Feb 07, 2023Fabien ChouteauAdaCore joins the Rust foundationLast year we announced our strategic partnership with Ferrous Systems, a technology company specializing in the Rust programming language. Today we…
  22. Mar 07, 2023Paul ButcherAutomated Assurance through Differential FuzzingThis blog describes the concept and benefits of differential fuzz testing. In addition, the post describes setting up, executing and analyzing the…
  23. Mar 16, 2023Fabien ChouteauGNAT Pro 21.6 for LYNX MOSA.ic for Avionics (MfA)
  24. Mar 23, 2023Maxim ReznikIntroduction to VSS libraryThe VSS (as an abbre­vi­a­tion for Vir­tu­al String Sub­sys­tem) library is designed to pro­vide advanced string and text pro­cess­ing…
  25. Mar 28, 2023Fabien ChouteauThe End of Binary Protocol Parser VulnerabilitiesThis week we announced a new tool called RecordFlux. The goal of RecordFlux is to address one of the most critical parts of the software stack in…
  26. Apr 01, 2023Yannick MoyThe Case for SPARK Evolution - an April First ParableSPARK already allows you to specify functional contracts by cases, and soon it will allow you to specify cases that lead to an exception. But what…
  27. Apr 04, 2023Yannick MoyExplainable Program ProofsEver wanted to understand why program proof is not as easy as telling ChatGPT "can you prove that program <code>stuff</code> is correct for me?" A…
  28. Apr 24, 2023Nicolas SettonReducing Ada code bases with adareducerHow we're using Libadalang to create an automated Ada code reducer.
  29. May 15, 2023Fabien ChouteauRecordFlux State MachinesIn a previous post we presented the RecordFlux specification language and toolset, illustrating how to design and generate formally proven binary…
  30. May 18, 2023Thomas CoudercFrom Desert Dunes to Humanitarian Aid: Inside the Epic Journey of the 4L Trophy RallyBack in February 2023, my friend David and I embarked on an exciting journey for a worthy cause. We finally got our old Renault 4l fully restored by…
  31. Aug 25, 2022Fabien ChouteauEmbedded Ada/SPARK, There's a ShortcutFor years in this blog my colleagues and I have published examples, demos, and how-to’s on Ada/SPARK embedded (as in bare-metal) development. Most of…
  32. Sep 02, 2022Paul ButcherFuzzing Out Bugs in Safety-Critical Embedded SoftwareFuzzing Out Bugs in Safety-Critical Embedded Software: Paul Butcher from AdaCore talks to Brandon Lewis from Embedded Toolbox

2022 26

  1. Sep 23, 2022Andry OgorodnikNew features for string literals and comments in GNAT StudioWe have added several new convenience features that help work with comments and string literals in Ada code.
  2. Oct 12, 2022Yannick MoyWhen Formal Verification with SPARK is the Strongest LinkSecurity is only as strong as its strongest link. That's important to keep in mind for software security, with its long chain of links, from design…
  3. Oct 25, 2022Johannes KliemannAdding Ada to RustWhile implementing application logic in Ada or SPARK is an improvement over a pure C project, its weakest link is still the C code in the SDK. On the…
  4. Nov 04, 2022Daniel KingAvoiding Vulnerabilities in Crypto Code with SPARK
  5. Nov 07, 2022Fabien ChouteauNVIDIA Security Team: “What if we just stopped using C?”Today I want to share a great story about why many NVIDIA products are now running formally verified SPARK code. This blog post is in part a teaser…
  6. Nov 24, 2022Fabien ChouteauTis the Season to be Giving falalalala lalalalaEvery year since 2015, a team of dedicated individuals led by Eric Wastl organizes an online programming challenge called: Advent of Code. The…
  7. Nov 28, 2022Pat RogersNew Learn Course: Introduction To Embedded Systems Programming
  8. Dec 06, 2022Fabien ChouteauCoroutines in Ada, a Clean but Heavy ImplementationA few months ago I was reading this article about coroutines in game development and how they are great tools for writing scripts (as in movie…
  9. Jan 10, 2023Fabien ChouteauOur Contribution to the Ada Logo DiscussionFrom time to time we see, here and there, discussions in the Ada community about the design and adoption of a common logo to represent the language.…
  10. Jan 12, 2023Fabien ChouteauAdvent of Ada/SPARK 2022 ResultsAt the end of November we called the Ada and SPARK programmers community to take on a challenge for a good cause. We are now in January and it is…
  11. Feb 28, 2022Fabien ChouteauAda GameDev Part 1: GEneric Sprite and Tile Engine (GESTE)In this first entry of the series, I want to present my GEneric Sprite and Tile Engine (GESTE) project. The goal of GESTE is to bring the rendering…
  12. Mar 02, 2022Manuel HatzlSPARK Crate of the Year: Unbounded containers in SPARKManuel Hatzl is the winner of the 2021 SPARK Crate of the year! In this blog post he shares his experience using Ada/​SPARK and how he created the…
  13. Mar 08, 2022Fabien ChouteauAda GameDev Part 2: Making 2D maps with TiledIn this second post of the Ada GameDev series we will see how to create game maps and export them to a format that is compatible with the GESTE…
  14. Mar 10, 2022Fabien Chouteau, Joffrey HuguetQuite Proved Image FormatA few weeks ago a piece of code went viral in the online dev community. The “Quite OK Image Format” (QOI) is a fast, lossless image compression…
  15. Mar 14, 2022Claire DrossHandling Aliasing through Pointers in SPARK
  16. Mar 17, 2022Paul JarrettAda Crate of the Year: Interactive code searchA retrospective on learning Ada and developing a tool with it in 2021 from 2021 Ada Crate of the Year Winner Paul Jarrett.
  17. Mar 22, 2022Gustavo A. HoffmannAnnouncing Updates to learn.adacore.com
  18. Jun 02, 2022Fabien ChouteauA New Era For Ada/SPARK Open Source CommunityToday we have two exciting announcements for the future of the Ada/SPARK ecosystem.
  19. Jun 23, 2022Yannick Moy, Lionel MatiasI can’t believe that I can prove that it can sortWhen an enthusiastic Ada programmer and a SPARK expert pair up to prove the most "stupid" sorting algorithm, lessons are learned! Join us in this…
  20. Jun 28, 2022Fabien ChouteauAnnouncing The 2022 Ada/SPARK Crate Of The Year AwardWe're happy to announce our the second edition of our programming competition, the Ada/SPARK Crate Of The Year Award! We believe the Alire package…
  21. Jul 26, 2022Quentin OchemAnnouncing Publication of the Draft Ferrocene Language SpecificationWe are pleased to announce the publication of the initial draft of the Ferrocene Language Specification (FLS) - a qualification-oriented document…
  22. Aug 09, 2022Paul ButcherJoin us at the High Integrity Software (HIS) Conference 2022!
  23. Sep 02, 2021Yannick MoyWhen the RISC-V ISA is the Weakest Link
  24. Sep 13, 2021Fabien ChouteauA design pattern for OOP in AdaWhen I do Object Oriented Programming with Ada, I tend to follow a design pattern that makes it easier for me and hopefully also for people reading…
  25. Oct 05, 2021Pat RogersTask Suspension with a Timeout in Ravenscar/JorvikThis blog entry shows how to define an abstract data type that allows tasks to block on objects of the type, waiting for resumption signals from…
  26. Oct 12, 2021Yannick MoyEnhancing the Security of a TCP Stack with SPARKThe developers of CycloneTCP library at Oryx Embedded partnered with AdaCore to replace the TCP part of the C codebase by SPARK code, and used the…

2021 24

  1. Oct 18, 2021Fabien ChouteauStarting micro-controller Ada drivers in the Alire ecosystemA few days ago, someone asked on the Ada Drivers Library repository how to add support for the SAMD21 micro-controller. Nowadays, I would rather…
  2. Nov 03, 2021Fabien ChouteauAn Embedded USB Device stack in AdaA couple years ago I started to tackle what was probably my most daunting project at the time, an embedded USB Device stack written 100% in Ada.
  3. Dec 06, 2021Paul ButcherFuzz Testing in International Aerospace GuidelinesThrough the HICLASS UK research group, AdaCore has been developing security-focused software development tools that are aligned with the objectives…
  4. Dec 15, 2021Yannick MoySPARKNaCl - Two Years of Optimizing Crypto Code in SPARK (and counting)SPARKNaCl is a SPARK ver­sion of the Tweet­Na­Cl cryp­to­graph­ic library, developed by formal methods and security expert Rod Chapman. For two years…
  5. Jan 27, 2022Fabien ChouteauAda/SPARK Crate Of The Year 2021 Winners Announced!
  6. Feb 01, 2022Fabien ChouteauAdaCore at FOSDEM 2022
  7. Feb 02, 2022Quentin Ochem, Florian GilcherAdaCore and Ferrous Systems Joining Forces to Support Rust
  8. Feb 10, 2022Yannick Moy, Claire DrossProving the Correctness of GNAT Light Runtime LibraryThe GNAT light runtime library is a version of the runtime library targeted at embedded platforms and certification, which has been certified for use…
  9. Feb 09, 2021Roderick ChapmanPerformance analysis and tuning of SPARKNaClThis blog goes into the details of both measuring and improving the runtime performance of SPARKNaCl on a real "bare metal" embedded target, and…
  10. Feb 18, 2021Roderick ChapmanDoubling the Performance of SPARKNaCl (again...)Following my last blog entry, further experiments show how the performance of SPARKNaCl can be doubled (again), plus analysis of worst-case stack…
  11. Feb 26, 2021Simon BuistShowing Global contracts with GNAT StudioIn the integrated development environment, GNAT Studio, there is now a plugin that inserts the generated Global contracts inline with the code.
  12. Apr 28, 2021Pat RogersOn the Benefits of Families ... (Entry Families)
  13. May 05, 2021Fabien ChouteauFrom Rust to SPARK: Formally Proven Bip-BuffersI am following the evolution of the embedded Rust community and in particular the work of James Munns from Ferrous-Systems. One of the projects that…
  14. May 26, 2021Pat RogersAn Introduction to Jorvik, the New Tasking Profile in Ada 2022The Ada 2022 draft defines a new tasking profile named Jorvik (pronounced “Yourvick”), based directly on the standard Ravenscar profile. Jorvik…
  15. Jun 01, 2021Fabien Chouteau, Nicolas SettonGNAT Community 2021 is here!
  16. Jun 03, 2021Arnaud CharletGoing beyond Ada 2022
  17. Jun 23, 2021Jessie GlocknerCelebrating Women Engineering Heroes - International Women in Engineering Day 2021
  18. Jun 25, 2021Roderick ChapmanSPARKNaCl with GNAT and SPARK Community 2021: Port, Proof and PerformanceThis post continues our adventures with SPARKNaCl - our verified SPARK version of the TweetNaCl cryptographic library. This time, we'll be looking at…
  19. Jun 28, 2021Fabien ChouteauAnnouncing The First Ada/SPARK Crate Of The Year AwardWe're happy to announce our new programming competition, the Ada/SPARK Crate Of The Year Award! We believe the Alire package manager is a game…
  20. Jul 08, 2021Kyriakos GeorgiouSecurity-Hardening Software Libraries with Ada and SPARK
  21. Oct 29, 2020Juliana SilvaMake With Ada 2020: High Integrity Sumobot
  22. Oct 29, 2020Arnaud CharletAda 202x support in GNAT
  23. Oct 30, 2020Fabien ChouteauFirst beta release of Alire, the package manager for Ada/SPARKA few years ago we realized that having a package manager for the Ada/SPARK community would be a game changer. Since then, AdaCore has been…
  24. Nov 03, 2020Fabien ChouteauAda for micro:bit Part 8: Music to my ears

2020 41

  1. Nov 05, 2020Juliana SilvaMake with Ada 2020: Ada Robot Car With Neural NetworkGuillermo Perez's project won a finalist prize in the Make with Ada 2019/20 competition. This project was originally posted on Hackster.io here. For…
  2. Nov 20, 2020Juliana SilvaMake with Ada 2020: The autonomous firetruckThe AFT (Autonomous FireTruck) is a prototype of an autonomous firetruck that can put out fire without risking people's lives. This project won a…
  3. Dec 07, 2020Juliana SilvaMake with Ada 2020: ADArrose
  4. Dec 17, 2020Paul ButcherFinding Vulnerabilities using Advanced Fuzz testing and AFLplusplus v3.0
  5. Jan 11, 2021Fabien ChouteauAda on any ARM Cortex-M device, in just a couple minutesIn this blog post I want to present a new tool that allows one to very quickly and easily start Ada programming on any ARM Cortex-M or RISC-V…
  6. Jan 22, 2021Léo GermondHow To: GNAT Pro with Docker
  7. Feb 04, 2021Fabien ChouteauAdaCore at FOSDEM 2021Like previous years, AdaCore will participate in FOSDEM. This time the event will be online only, but this won’t prevent us from celebrating Open…
  8. Feb 02, 2021Fabien ChouteauMini SAM M4 Ada BSPBeyond the great look, the Mini SAM M4 provide a powerful 120 Mhz Microchip SAMD51 Cortex-M microcontroller, a couple of LEDs and a user…
  9. Sep 08, 2020Pierre-Marie de RodatIntroducing source code instrumentation in GNATcoverageThis is the first post of a series about GNATcoverage and source code instrumentation.In order to make GNATcoverage viable in more contexts, we…
  10. Sep 10, 2020Pierre-Marie de RodatGNATcoverage: getting started with instrumentation
  11. Sep 15, 2020Fabien ChouteauAda for micro:bit Part 1: Getting Started
  12. Sep 22, 2020Fabien ChouteauAda for micro:bit Part 2: Push buttons
  13. Sep 28, 2020Michael FrankCode Obfuscator for Ada using Libadalang and SPARKA code obfuscator is a method of sharing coding discussions of real-world examples without giving away proprietary or classified information. This…
  14. Sep 29, 2020Fabien ChouteauAda for micro:bit Part 3: Pin OutputWelcome to the Ada for micro:bit series where we look at simple examples to learn how to program the BBC micro:bit with Ada.
  15. Oct 05, 2020Fabien Chouteau, Emma AdbyAdaCore Code of Conduct
  16. Oct 06, 2020Fabien ChouteauAda for micro:bit Part 4: Pin Input
  17. Oct 13, 2020Fabien ChouteauAda for micro:bit Part 5: Analog Output
  18. Oct 20, 2020Fabien ChouteauAda for micro:bit Part 6: Analog Input
  19. Oct 21, 2020Juliana SilvaMake with Ada 2020: CHIP-8 InterpreterLaurent Zhu's and Damien Grisonnet's project was accomplished for the EPITA Ada courses and won a finalist prize in the Make with Ada 2019/20…
  20. Oct 27, 2020Fabien ChouteauAda for micro:bit Part 7: Accelerometer
  21. Apr 07, 2020Martyn PikeA Trivial File Transfer Protocol Server written in AdaFor an upcoming project, I needed a simple way of transferring binary files over an Ethernet connection with minimal (if any at all) user…
  22. Apr 09, 2020Johannes KliemannAda on the ESP8266Not long ago, AdaCore published its LLVM frontend for GNAT. Also quite recently Espressif updated their LLVM backend to LLVM 9 which also happens to…
  23. Apr 21, 2020Abe CohenAn Introduction to Contract-Based Programming in Ada
  24. May 14, 2020Pat RogersFrom Ada to Platinum SPARK: A Case Study for Reusable Bounded StacksThis blog entry describes the transformation of an Ada stack ADT into a completely proven SPARK implementation that relies on static verification…
  25. May 26, 2020Nicolas SettonGNAT Community 2020 is here!We are happy to announce that the GNAT Community 2020 release is now available! Read the post for access to download and to find out about this…
  26. Jun 10, 2020Jon AndrewCuBit: A General-Purpose Operating System in SPARK/AdaLast year, I started evaluating programming languages for a formally-verified operating system. I've been developing software for a while, but only…
  27. Jun 11, 2020Emma AdbyMake with Ada 2020: The SmartBase - IoT Adjustable BedJohn Singleton's The SmartBase makes your existing adjustable bed safer and easier to use by adding voice control and safe (and fun!) LED underbed…
  28. Jun 25, 2020Emma AdbyMake with Ada 2020: CryptAda - (Nuclear) Crypto on Embedded DeviceTeam CryptAda's project collects entropy, manages an entropy pool, implements a homemade PRNG, and generates RSA keys directly on the board with an…
  29. Jul 09, 2020Emma AdbyMake with Ada 2020: Disaster Management with Smart Circuit BreakerShahariar's project ensures safety against electrical fire or shock during an earthquake, flood, gas leakage or fire breakout by disconnecting the…
  30. Jul 28, 2020Claire DrossRelaxing the Data Initialization Policy of SPARKSPARK always being under development, new language features make it in every release of the tool, be they previously unsupported Ada features (like…
  31. Aug 12, 2020Emma AdbyMake with Ada 2020: LoRaDa := Ada + LoRa;Hedley Rainnie's project combines 6 different SoCs all programmed in Ada performing as a LoRa network. He also showcases a BLE bridge to a LoRa…
  32. Sep 03, 2020Jessie Glockner, Ben BrosgolThe FACE™ open systems strategy gaining traction in the avionics industryThe FACE™ approach is a government-industry initiative for reducing defense system life cycle costs through portable and reusable software…
  33. Oct 17, 2019Alexander SenierRecordFlux: From Message Specifications to SPARK CodeHandling binary data is hard. Errors in parsers routinely lead to critical security vulnerabilities. In this post we show how the RecordFlux toolset…
  34. Nov 07, 2019Martyn PikeAn Expedition into Libadalang
  35. Dec 11, 2019Paul ButcherAdaCore for HICLASS - Enabling the Development of Complex and Secure Aerospace Systems
  36. Jan 21, 2020Quentin OchemWitnessing the Emergence of a New Ada Era
  37. Jan 23, 2020Fabien ChouteauAda on a FeatherI was quite happy to see AdaFruit release their first Feather format board including a micro-controller with plenty of Ada support, the STM32F4. I…
  38. Jan 30, 2020Fabien ChouteauAdaCore at FOSDEM 2020
  39. Feb 04, 2020Vadim GodunkoUsing GNAT-LLVM to target Ada to WebAssembly
  40. Feb 06, 2020Pierre-Marie de RodatA Further Expedition into Libadalang: Save Time with Libadalang.Helpers.App
  41. Mar 10, 2020Pat RogersMaking an RC Car with Ada and SPARK

2019 27

  1. Mar 12, 2020Maxim ReznikAndroid application with Ada and WebAssembly
  2. Mar 17, 2020Ghjuvan LacambreTime travel debugging in GNAT Studio with GDB and RRLearn how to use GDB and RR's advanced time traveling features in GNAT Studio.
  3. Apr 02, 2020Roderick ChapmanProving properties of constant-time crypto code in SPARKNaClOver the last few months, I developed a SPARK version of the TweetNaCl cryptographic library. This was made public on GitHub in February 2020, under…
  4. Jun 05, 2019Nicolas SettonGNAT Community 2019 is here!
  5. Jun 06, 2019Claire DrossUsing Pointers in SPARKIn this blog post, I will present one of the most interesting additions to the community 2019 version of SPARK: pointer support. One of the core…
  6. Jun 11, 2019Yannick Moy, Raphaël Amiard, Tucker TaftRFCs for Ada and SPARK evolution now on GitHubInterested in participating in the evolution of the Ada or SPARK languages? We have something for you.
  7. Jun 18, 2019Juan ZamoranoUsing Ada for a Spanish Satellite Project
  8. Jul 09, 2019Joffrey Huguet, Johannes KanigProving a simple program doing I/O ... with SPARKThe functionality of many security-critical programs is directly related to Input/Output (I/O). This includes command-line utilities such as gzip,…
  9. Sep 03, 2019Isabelle VialardSecure Use of Cryptographic Libraries: SPARK Binding for LibsodiumThe challenge faced by cryptography APIs is to make building functional and secure programs easy for the user. In this blog post I will present you…
  10. Sep 05, 2019Maxim Reznik, Yannick MoyFirst Ada Virtual Conference organized by and for the Ada communityThe Ada Community has gathered recently around a new exciting initiative - an Ada Virtual Conference, to present Ada-related topics in a 100% remote…
  11. Sep 12, 2019Emma AdbyThe Make with Ada competition is back!
  12. Oct 01, 2019Arnaud CharletCombining GNAT with LLVM
  13. Oct 08, 2019Claire DrossPointer Based Data-Structures in SPARKAs seen in a previous post, it is possible to use pointers (or access types) in SPARK provided the program abides by a strict memory ownership policy…
  14. Oct 10, 2019Michael FrankLearning SPARK via Conway's Game of LifeHow I learned to write SPARK-provable code using Conway's Game Of Life
  15. Oct 15, 2019Arnaud CharletThe Power of Technology Integration and Open Source
  16. Jan 08, 2019Quentin OchemProving Memory Operations - A SPARK Journey
  17. Feb 05, 2019Quentin OchemNVIDIA is joining the Ada and SPARK adopter wave
  18. Feb 12, 2019Rob TiceAdaFractal Part1: Ada with a Portable GUIThe is the first part of a multiple part post that covers the development of the AdaFractal project. The idea was to create fractals in Ada. Here we…
  19. Feb 14, 2019Rob TiceAdaFractal Part 2: Fixed Point and Floating Point Math Performance and Parallelization
  20. Feb 19, 2019Yannick Moy, Nicolas Roche, Pierre-Marie de Rodat, Fabien ChouteauAdaCore at FOSDEM 2019Like last year, we've sent a squad of AdaCore engineers to participate in the celebration of Open Source software at FOSDEM. Like last year, we had…
  21. Feb 21, 2019Yannick Moy, Nicolas Setton, Ben BrosgolA Readable Introduction to Both MISRA C and SPARK Ada
  22. Mar 02, 2019Peter ChapinTen Years of Using SPARK to Build CubeSat Nano Satellites With StudentsMy colleague, Carl Brandon, and I have been running the CubeSat Laboratory at Vermont Technical College (VTC) for over ten years. During that time we…
  23. Mar 05, 2019Arnaud CharletHow Do We Use CodePeer at AdaCore
  24. Mar 07, 2019Pamela TrevinoPublic Ada Training Paris June 3-7, 2019
  25. May 01, 2019Joffrey HuguetUsing SPARK to prove 255-bit Integer Arithmetic from Curve25519
  26. May 16, 2019Allan Ascanius, Per Dalgas JakobsenWinning DTU RoboCup with Ada and SPARKThe Danish Technical University has a yearly RoboCup where autonomous vehicles solve a number of challenges. We participated with RoadRunner, a 3D…
  27. May 30, 2019Boran CarBringing Ada To MultiZoneC is the dominant language of the embedded world, almost to the point of exclusivity. Due to its age, and its goal of being a “portable assembler”,…

2018 25

  1. Apr 18, 2018Thomas QuinotPolyORB now lives on Github
  2. May 08, 2018Johannes KanigTaking on a Challenge in SPARK
  3. May 29, 2018Yannick Moy, Roderick ChapmanHow Ada and SPARK Can Increase the Security of Your SoftwareThere is a long-standing debate about which phase in the Software Development Life Cycle causes the most bugs: is it the specification phase or the…
  4. Jun 25, 2018Yannick MoySecurity Agency Uses SPARK for Secure USB Key​ANSSI, the French national security agency, has published the results of their work since 2014 on designing and implementing an open-hardware &…
  5. Jun 26, 2018Emma Adby, Fabien ChouteauGNAT Community 2018 is here!
  6. Jul 25, 2018Fabien Chouteau, Emma Adby, Yannick MoyLearn.adacore.com is hereWe are very proud to announce the availability of our new Ada and SPARK learning platform learn.adacore.com, which will replace AdaCoreU(niversity)…
  7. Aug 08, 2018Pamela TrevinoAdaCore major sponsor at HIS 2018
  8. Sep 11, 2018Fabien ChouteauAda on FPGAs with PicoRV32When I bought the TinyFPGA-BX board, I thought it would be an opportunity to play a little bit with FPGA, learn some Verilog or VHDL. But when I…
  9. Sep 18, 2018Julia TeisslTrain control using Ada on a Raspberry Pi
  10. Oct 10, 2018Pamela TrevinoPublic Ada Training Paris, France Dec 3 - 7, 2018
  11. Oct 17, 2018Emma AdbyIt's time to Make with Ada!
  12. Oct 23, 2018Yannick Moy​Amazon Relies on Formal Methods for the Security of AWSByron Cook, who founded and leads the Automated Reasoning Group at Amazon Web Services (AWS) Security, gave a powerful talk at the Federated Logic…
  13. Feb 05, 2018Felix KrauseThe Road to a Thick OpenGL Binding for Ada: Part 1
  14. Feb 19, 2018Yannick MoyFor All Properties, There Exists a ProofWith the recent addition of a Manual Proof capability in SPARK 18, it is worth looking at an example which cannot be proved by automatic provers, to…
  15. Feb 15, 2018Johannes KanigBitcoin blockchain in Ada: Lady Ada meets Satoshi Nakamoto
  16. Feb 22, 2018Felix KrauseThe Road to a Thick OpenGL Binding for Ada: Part 2This blog post is part two of a tutorial based on the OpenGLAda project and will cover implementation details such as a type system for interfacing…
  17. Feb 23, 2018Yannick MoyTokeneer Fully Verified with SPARK 2014Tokeneer is a software for controlling physical access to a secure enclave by means of a fingerprint sensor. This software was created by Altran…
  18. Feb 26, 2018Fabien ChouteauAda on the micro:bit
  19. Mar 05, 2018Yannick MoySecure Software Architectures Based on Genode + SPARK​SPARK user Alexander Senier presented recently at BOB Konferenz​ in Germany their use of SPARK for building secure mobile architectures. What's nice…
  20. Mar 14, 2018Yannick MoyTwo 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…
  21. Mar 28, 2018Rob TiceSPARKZumo Part 1: Ada and SPARK on Any Platform
  22. Apr 01, 2018Fabien ChouteauGetting Rid of Rust with AdaThere 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…
  23. Apr 01, 2018Fabien Chouteau, Yannick Moy, Vasiliy Fofanov, Nicolas SettonA Modern Syntax for AdaOne of the most criticized aspect of the Ada language throughout the years has been its outdated syntax. Fortunately, AdaCore decided to tackle this…
  24. Apr 04, 2018Rob TiceSPARKZumo Part 2: Integrating the Arduino Build Environment Into GPSThis is part #2 of the SPARKZumo series of blog posts. This post covers the build system that was used to build the SPARKZumo project and how to…
  25. Aug 24, 2017Yannick MoyNew SPARK Cheat SheetOur good friend Martin Becker has produced a new cheat sheet for SPARK, that you may find useful for a quick reminder on syntax that you have not…

2017 45

  1. Sep 12, 2017Yannick MoySPARK Tutorial at FDL ConferenceResearcher Martin Becker is giving a SPARK tutorial next week at FDL conference. This post gives a link to his tutorial material (cookbook and…
  2. Oct 18, 2017Yannick MoyProve in the CloudWe have put together a byte (8 bits) of examples of SPARK code on a server in the cloud. The benefit with this webpage is that anyone can now…
  3. Nov 14, 2017Jonas AttertunMake with Ada 2017: Brushless DC Motor ControllerThis project involves the design of a software platform that provides a good basis when developing motor controllers for brushless DC motors…
  4. Nov 16, 2017Yannick Moy, Martin Becker, Emanuel RegnathPhysical Units Pass the Generic TestThe support for physical units in programming languages is a long-standing issue, which very few languages have even attempted to solve. This issue…
  5. Nov 22, 2017J. German RiveraMake with Ada 2017- A "Swiss Army Knife" Watch
  6. Nov 23, 2017Fabien ChouteauThere's a mini-RTOS in my language
  7. Nov 29, 2017Emma AdbyWelcoming New Members to the GNAT Pro Family
  8. Dec 13, 2017Manuel Iglesias AbbatermarcoMake with Ada 2017- Ada Based IoT Framework
  9. Dec 18, 2017Pierre-Marie de Rodat, Raphaël AmiardCross-referencing Ada with Libadalang
  10. Dec 19, 2017Lionel MatiasLeveraging Ada Run-Time Checks with Fuzz Testing in AFLFuzzing is a very popular bug finding method. The concept, very simple, is to continuously inject random (garbage) data as input of a software…
  11. Jan 18, 2018Pierre-Marie de Rodat, Yannick Moy, Fabien Chouteau, Raphaël AmiardAdaCore at FOSDEM 2018
  12. May 27, 2017Yannick MoyNew Guidance for Adoption of SPARKWhile SPARK has been used for years in companies like Altran UK, companies without the same know-how may find it intimidating to get started on…
  13. Jun 02, 2017Yannick MoyFrama-C & SPARK Day Slides and HighlightsThe Frama-C & SPARK Day this week was a very successful event gathering the people interested in formal program verification for C programs (with…
  14. Jun 08, 2017Yannick MoyResearch Corner - Floating-Point Computations in SPARKIt is notoriously hard to prove properties of floating-point computations, including the simpler bounding properties that state safe bounds on the…
  15. Jun 11, 2017Yannick MoyResearch Corner - FLOSS Glider Software in SPARKTwo years ago, we redeveloped the code of a small quadcopter called Crazyflie in SPARK, as a proof-of-concept to show it was possible to prove…
  16. Jun 13, 2017Fabien ChouteauAda on the first RISC-V microcontroller
  17. Jun 15, 2017Pierre-Marie de Rodat, Nicolas SettonGNAT GPL 2017 is out!
  18. Jun 20, 2017Rob TiceThe Adaroombot ProjectThe Adaroombot project consists of an iRobot CreateⓇ 2 and Ada running on a Raspberry Pi with a Linux OS. This is a great Intro-to-Ada project as it…
  19. Jun 29, 2017Yannick MoyApplied Formal Logic: Searching in StringsA friend pointed me to recent posts by Tommy M. McGuire, in which he describes how Frama-C can be used to functionally prove a brute force version of…
  20. Jul 18, 2017Yannick MoyResearch Corner - Focused Certification of SPARK in CoqThe SPARK toolset aims at giving guarantees to its users about the properties of the software analyzed, be it absence of runtime errors or more…
  21. Jul 20, 2017Yannick MoyProving Loops Without Loop InvariantsFor all the power that comes with proof technology, one sometimes has to pay the price of writing a loop invariant. Along the years, we've strived to…
  22. Jul 25, 2017Pierre-Marie de RodatPretty-Printing Ada Containers with GDB Scripts
  23. Aug 08, 2017Pierre-Marie de RodatHighlighting Ada with Libadalang
  24. Mar 27, 2017Jorge RealWriting on Air
  25. Mar 29, 2017Pierre-Marie de RodatGNATcoverage moves to GitHub
  26. Mar 30, 2017Yannick MoyTwo Projects to Compute Stats on Analysis ResultsTwo projects by Daniel King and Martin Becker facilitate the analysis of GNATprove results by exporting the results (either from the log or from the…
  27. Mar 31, 2017Jerome Guitton, Jérôme Lambourg, Joel BrobeckerSimics helps run 60 000 GNAT Pro tests in 24 hours
  28. Apr 04, 2017Emmanuel BriotNew strings package in GNATCOLLThis post describes the new GNATCOLL.Strings package, and the various optimizations it performs to provide improved performance.
  29. Apr 06, 2017Yannick MoyGNATprove Tips and Tricks: Proving the Ghost Common Divisor (GCD)Euclid's algorithm for computing the greatest common divisor of two numbers is one of the first ones we learn in school, and also one of the first…
  30. Apr 10, 2017Emmanuel BriotUser-friendly strings API
  31. Apr 19, 2017Anthony Leonardo GracioGPS for bare-metal developers
  32. Apr 28, 2017Yannick MoyVerifyThis Challenge in SPARKThis year again, the VerifyThis competition took place as part of ETAPS conferences. This is the occasion for builders and users of formal program…
  33. May 02, 2017Yannick Moy, Emmanuel Briot, Nicolas RocheA Usable Copy-Paste Detector in A Few Lines of PythonAfter we created lightweight checkers based on the recent Libadalang technology developed at AdaCore, a colleague gave us the challenge of creating a…
  34. May 05, 2017Yannick Moy(Many) More Low Hanging BugsWe reported in a previous post our initial experiments to create lightweight checkers for Ada source code, based on the new Libadalang technology.…
  35. May 16, 2017Fabien ChouteauDIY Coffee Alarm ClockA few weeks ago one of my colleagues shared this kickstarter project : The Barisieur. It’s an alarm clock coffee maker, promising to wake you up with…
  36. Dec 16, 2016Yannick MoySPARK Cheat Sheets (en & jp)The SPARK cheat sheet usually distributed in trainings has recently been translated to Japanese. Here they are, both in English and in Japanese. My…
  37. Dec 31, 2016Johannes KanigSPARK and CodePeer, a Good Match!It turns out that the CodePeer engine can be used as a powerful prover for SPARK programs. This feature will be available in the next version of…
  38. Jan 04, 2017Yannick MoyNew Year's Resolution for 2017: Use SPARK, Say Goodbye to Bugs​NIST has recently published a report called "Dramatically Reducing Software Vulnerabilities"​ in which they single out five approaches which have…
  39. Jan 23, 2017Raphaël Amiard, Pierre-Marie de RodatIntroducing LibadalangAdaCore is working on a host of tools that works on Ada code. The compiler, GNAT, is the most famous and prominent one, but it is far from being the…
  40. Jan 24, 2017Johannes KanigHash it and Cache itA new feature of SPARK2014 allows to use a memcached server to share proof results between runs of the SPARK tools and even between developers on…
  41. Jan 30, 2017Raphaël Amiard, Yannick Moy, Pierre-Marie de RodatGoing After the Low Hanging BugAt AdaCore, we have a strong expertise in deep static analysis tools (CodePeer and SPARK), and we have been relying on the compiler GNAT and our…
  42. Feb 10, 2017Yannick MoyProving Tetris With SPARK in 15 MinutesI gave last week a 15-minutes presentation at FOSDEM conference of how you can prove interesting properties of Tetris with SPARK. Here is the…
  43. Feb 14, 2017Pat RogersGetting started with the Ada Drivers Library device drivers
  44. Feb 22, 2017Emma AdbyAdaCore attends FOSDEMEarlier this month AdaCore attended FOSDEM in Brussels, an event focused on the use of free and open source software. Two members of our technical…
  45. Mar 07, 2017Yannick MoyRod Chapman on Software SecurityRod Chapman gave an impactful presentation at Bristech conference last year. His subject: programming Satan's computer! His way of pointing out how…

2016 45

  1. Mar 09, 2017Claire DrossResearch Corner - Auto-active Verification in SPARKGNATprove performs auto-active verification, that is, verification is done automatically, but usually requires annotations by the user to succeed. In…
  2. Mar 20, 2017Fabien Chouteau, Arnaud Charlet, Yannick MoySPARK Tetris on the Arduboy
  3. Nov 04, 2016Olivier RamonatSimplifying our product versioningLooking at the list of product versions that were expected for 2017 it became clear that we had to review the way we were handling product versioning.
  4. Nov 07, 2016Piotr TrojanekVerifying Tasking in Extended, Relaxed StyleTasking was one of the big features introduced in the previous release of SPARK 2014. However, GNATprove only supported tasking-related constructs…
  5. Nov 09, 2016Yannick MoyResearch Corner - SPARK on Lunar IceCube Micro SatelliteResearchers Carl Brandon and Peter Chapin recently presented during conference HILT 2016 their ongoing work to build a micro satellite called Lunar…
  6. Nov 10, 2016Pat RogersDriving a 3D Lunar Lander Model with ARM and Ada
  7. Nov 15, 2016Emmanuel BriotIntegrate new tools in GPSThis blog, the first in a series, explains the basic mechanisms that GPS (the GNAT Programming Studio) provides to integrate external tools. A small…
  8. Nov 17, 2016Yannick MoyGNATprove Tips and Tricks: What’s Provable for Real Now?One year ago, we presented on this blog what was provable about fixed-point and floating-point computations (the two forms of real types in SPARK).…
  9. Nov 21, 2016Claire DrossAutomatic Generation of Frame Conditions for Array ComponentsOne of the most important challenges for SPARK users is to come up with adequate contracts and annotations, allowing GNATprove to verify the expected…
  10. Nov 22, 2016Emmanuel BriotIntegrate new tools in GPS (2)
  11. Nov 28, 2016Sylvain DaillerGNATprove Tips and Tricks: a Lemma for Sorted ArraysWe report on the creation of the first lemma of a new lemma library on arrays: a lemma on transitivity of the order in arrays.
  12. Nov 29, 2016Emma AdbyMake With Ada Winners Announced!
  13. Dec 06, 2016Emma AdbyBuilding High-Assurance Software without Breaking the Bank
  14. Dec 12, 2016Fabien ChouteauMake with Ada: DIY instant cameraThere are moments in life where you find yourself with an AdaFruit thermal printer in one hand, and an OpenMV camera in the other.
  15. Jun 16, 2016Yannick MoyResearch Corner - Proving Security of Binary Programs with SPARKResearchers from Dependable Computing and Zephyr Software LLC have presented at the latest NASA Formal Methods conference last week their work on…
  16. Jun 21, 2016Emma AdbyIntroducing the Make With Ada competition!
  17. Jul 11, 2016Yannick MoyResearch Corner - SPARK 2014 vs Frama-C vs Why3Ready for a bloody comparison between technologies underlying the tools for SPARK 2014 vs Frama-C vs Why3? Nothing like that in that article we wrote…
  18. Jul 26, 2016Claire DrossAutomatic Generation of Frame Conditions for Record ComponentsFormal verification tools like GNATprove rely on the user to provide loop invariants to describe the actions performed inside loops. Though the…
  19. Sep 07, 2016Emmanuel BriotBookmarks in the GNAT Programming Studio (GPS)As we improve existing views in GPS, we discover new ways to use them. This post shows some of the improvements done recently in the Bookmarks view,…
  20. Sep 12, 2016Emmanuel BriotGNAT Programming Studio (GPS) on GitHubThe GPS source repository has been published on GitHub. This post briefly describes how you can access it, and hopefully contribute.
  21. Sep 19, 2016Quentin OchemUnity & AdaUsing Ada technologies to develop video games doesn’t sound like an an obvious choice - although it seems like there could be an argument to be made.…
  22. Sep 22, 2016Yannick MoyThe Most Obscure Arithmetic Run-Time Error ContestSomething that many developers do not realize is the number of run-time checks that occur in innocent looking arithmetic expressions. Of course,…
  23. Oct 05, 2016Emmanuel BriotDebugger improvements in GPS 17The GNAT Programming Studio support for the debugger has been enhanced. This post describes the various changes you can expect in this year's new…
  24. Oct 06, 2016Yannick MoyVerified, Trustworthy Code with SPARK and Frama-CLast week, a few of us at AdaCore have attended a one-day workshop organized at Thales Research and Technologies, around the topic of "Verified,…
  25. Oct 11, 2016Emmanuel BriotGNAT On macOS SierraGNAT and all the tools work great on the newly released macOS Sierra, but gdb needs some tweaking of the system.
  26. Oct 12, 2016Claire DrossSPARK 2014 Rationale: Support for Type InvariantsType invariants are used to model properties that should always hold for users of a data type but can be broken inside the data type implementation.…
  27. Mar 10, 2016Yannick MoyFormal Verification of Legacy Code
  28. Mar 10, 2016Emma AdbyCubeSat continues to orbit the Earth thanks to Ada & SPARK!
  29. Mar 16, 2016Emma AdbyProvably safe programming at Embedded World
  30. Apr 03, 2016Yannick MoyDid SPARK 2014 Rethink Formal Methods?David Parnas is a well-known researcher in formal methods, who famously contributed to the analysis of the shut-down software for the Darlington…
  31. Apr 07, 2016Emma AdbyVectorCAST/Ada: Ada 2012 Language Support
  32. Apr 13, 2016Jérôme LambourgEfficient use of Simics for testing
  33. Apr 18, 2016Emma AdbyCertification and Qualification
  34. Apr 21, 2016Florian SchandaSPARKSMT - An SMTLIB Processing Tool Written in SPARK - Part IToday I will write the first article in a short series about the development of an SMTLIB processing tool in SPARK. Instead of focusing on features,…
  35. May 17, 2016Claire DrossQuantifying over Elements of a ContainerContainers holding several items of the same type such as arrays, lists, or sets are a common occurrence in computer programs. Stating a property…
  36. May 25, 2016Yannick MoyGNATprove Tips and Tricks: Using the Lemma LibraryA well-know result of computing theory is that the theory of arithmetic is undecidable. This has practical consequences in automatic proof of…
  37. Jun 13, 2016Pierre-Marie de RodatC library bindings: GCC plugins to the rescue
  38. Jun 01, 2016Fabien ChouteauMake with Ada: ARM Cortex-M CNC controller
  39. Nov 16, 2015Emmanuel BriotCalling inherited subprograms in AdaThis short post describes an idiom that can be used to help maintain complex hierarchies of tagged types, when methods need to call the parent types…
  40. Nov 23, 2015Yannick MoySPARK 2014 Rationale: Support for RavenscarAs presented in a recent post by Pavlos, the upcoming release of SPARK Pro will support concurrency features of Ada, with the restrictions defined in…
  41. Nov 30, 2015Yannick MoyGNATprove Tips and Tricks: What’s Provable for Real?SPARK supports two ways of encoding reals in a program: the usual floating-point reals, following the standard IEEE 754, and the lesser known…
  42. Dec 14, 2015Emma AdbyDissimilar tools: Use cases and impact on tool qualification level
  43. Dec 18, 2015Yannick Moy, Emma AdbyAda Lovelace Bicentennial
  44. Jan 12, 2016Jérôme LambourgPorting the Ada Runtime to a new ARM boardA step by step tutorial to adapt the ARM runtime to new MCUs/boards.
  45. Jan 18, 2016Emma AdbyERTS and Embedded World conferences 2016

2015 54

  1. Jan 27, 2016Emma AdbyFormal Verification Made Easy!
  2. Feb 23, 2016Emma AdbyQGen 2.1 Release!
  3. Mar 02, 2016Emma AdbyEmbedded Product Line Updates
  4. Mar 03, 2016Fabien ChouteauMake with Ada: Candy dispenser, with a twist...
  5. Mar 04, 2016Yannick MoySPARK Prez at New Conference on Railway SystemsRSSR is a new conference focused on the development and verification of railway systems. We will present there how SPARK can be used to write…
  6. Sep 15, 2015Emmanuel BriotTraits-Based ContainersThis post describes the design of a new containers library. It highlights some of the limitations of the standard Ada containers, and proposes a new…
  7. Sep 21, 2015Yannick MoyThe Eight Reasons For Using SPARKBased on our many years of experience with our customers using SPARK in their projects, we have come up with a list of eight objectives that are most…
  8. Sep 23, 2015Emma AdbyAdaCore Tech Days 2015
  9. Sep 22, 2015Florian SchandaSPARK 2014 Rationale: Variables That Are ConstantThe SPARK tools now support yet another feature that allows users to better specify the intended behavior of their programs. This new feature enables…
  10. Oct 08, 2015Emma AdbyHIS Conference 2015, Bristol
  11. Oct 14, 2015Maxim Reznik, Nicolas SettonUsing reference types to handle persistent objects
  12. Oct 20, 2015Yannick MoyGNATprove Tips and Tricks: User ProfilesOne of the most difficult tasks when using proof techniques is to interact with provers, in particular to progressively increase proof power until…
  13. Oct 27, 2015Emma AdbyARM TechCon and NBAA Conference 2015
  14. Nov 03, 2015David HauzarSPARK 16: Generating Counterexamples for Failed ProofsWhile the analysis of failed proofs is one of the most challenging aspects of formal verification, it would be much easier if a tool would…
  15. Nov 03, 2015Emma AdbyModernizing Adacore's Open-Source Involvement
  16. Nov 10, 2015Fabien ChouteauMake with Ada: Formal proof on my wristWhen the Pebble Time kickstarter went through the roof, I looked at the specification and noticed the watch was running on an STM32F4, an ARM…
  17. Nov 12, 2015Florian SchandaSPARK 2016 Supports Ravenscar!The new big feature of the SPARK 2016 release is the support of the Ravenscar profile. Users can now use protected objects and tasks to write…
  18. May 13, 2015Emmanuel BriotLarger than it looks (storage pools)This post shows how to implement a special storage pool that allocates an extra header every time it allocates some memory. This can be used to store…
  19. May 21, 2015Emmanuel BriotCount them all (reference counting)
  20. May 22, 2015Yannick MoyHow Our Compiler Learnt From Our AnalyzersProgram analyzers interpret the source code of a program to compute some information. Hopefully, the way they interpret the program is consistent…
  21. May 28, 2015Anthony Leonardo GracioHow to prevent drone crashes using SPARKThe Crazyflie is a very small quadcopter sold as an open source development platform: both electronic schematics and source code are directly…
  22. Jun 01, 2015Yannick MoySPARKSkein: From tour-de-force to run-of-the-mill Formal VerificationIn 2010, Rod Chapman released an implementation in SPARK of the Skein cryptographic hash algorithm, and he proved that this implementation was free…
  23. Jun 19, 2015Fabien ChouteauMake with Ada: All that is useless is essentialA few weeks ago I discovered the wonderful world of solenoid engines. The idea is simple: take a piston engine and replace explosion with…
  24. Jul 02, 2015Cyrille ComarFarewell Robert...
  25. Jul 20, 2015Fabien ChouteauMake with Ada: "The Eagle has landed"July 20, 1969, 8:18 p.m. UTC, while a bunch of guys were about to turn blue on Earth, commander Neil A. Armstrong confirmed the landing of his Lunar…
  26. Jul 24, 2015Yannick MoySPARK 2014 Rationale: Type PredicatesPreconditions and postconditions define a very strong mechanism for specifying invariant properties over the program's control. What about similar…
  27. Jul 29, 2015Jack Mellor2015: A Space Ada‑sseyAdaCore has a long history of providing tools and support to develop mission critical applications for Space. Check out this video we made and showed…
  28. Aug 04, 2015Raphaël AmiardMake with Ada : From bits to music
  29. Sep 13, 2015Yannick MoyNew Book About SPARK 2014I am very pleased to announce that a book is now available for those who want to learn formal verification with SPARK 2014. This book was written by…
  30. Mar 05, 2015Olivier RamonatAdaCore Releases GNAT Pro 7.3, QGen 1.0 and GNATdashboard 1.0
  31. Mar 11, 2015Emma Adby20 years on...
  32. Mar 12, 2015Emma AdbyQGen on Embedded News TV
  33. Mar 16, 2015Clément FumexGNATprove Tips and Tricks: Bitwise OperationsThe ProofInUse joint laboratory is currently improving the way SPARK deals with modular types and bitwise operators. Until now the SPARK tool was…
  34. Mar 20, 2015Yannick MoyGNATprove Tips and Tricks: Minimizing ReworkAs automatic proof is time consuming, it is important that rework following a change in source code is minimized. GNATprove uses a combination of…
  35. Mar 25, 2015Yannick MoyA Building Code for Building CodeIn a recent article in Communications of the ACM, Carl Landwehr, a renowned scientific expert on security, defends the view that the software…
  36. Mar 27, 2015Martyn PikeThe latest Mixed Programming with Ada lectures at the AdaCore University
  37. Apr 15, 2015Claire DrossA quick glimpse at the translation of Ada integer types in GNATproveIn SPARK, as in most programming languages, there are a bunch of bounded integer types. On the other hand, Why3 only has mathematical integers and a…
  38. Apr 28, 2015Karen MasonThe Year for #AdaLove
  39. May 04, 2015Emma AdbyVerification on Ada code with Static and Dynamic Code Analysis - Webinar
  40. May 06, 2015Emma AdbyProject P Open Workshop
  41. May 11, 2015Karen MasonWhat's in the Box?
  42. Jan 07, 2015Cyrille ComarWelcome To AdaCore's BlogI'm proud, if not a bit nervous, to be the one firing the very first post on this brand new blog. Why are we starting a corporate blog at this time?…
  43. Jan 07, 2015Tristan Gingold, Yannick MoyTetris in SPARK on ARM Cortex M4
  44. Jan 09, 2015Introducing the AdaCore BlogWe’re pleased to announce the launch of the AdaCore Blog providing an insight into the AdaCore Ecosystem.
  45. Jan 14, 2015Yannick MoySPARK 2014 Rationale: Object Oriented ProgrammingObject Oriented Programming is known for making it particularly difficult to analyze programs, because the subprograms called are not always known…
  46. Jan 15, 2015Emma AdbyA Busy Schedule Ahead!
  47. Jan 21, 2015Yannick MoySPARK 2014 Rationale: Functional UpdateWhile attribute Old allows expressing inside postconditions the value of objects at subprogram entry, this is in general not enough to conveniently…
  48. Jan 23, 2015Lena ComarProofInUse is coming!
  49. Feb 06, 2015Yannick MoyGNATprove Tips and Tricks: Keeping Justifications Up-To-DateGNATprove supports the suppression of warnings and justification of check messages with pragmas inserted in the source code. But these justifications…
  50. Feb 10, 2015Tristan GingoldAdaCore at FOSDEM'15
  51. Feb 18, 2015Yannick MoyGNATprove Tips and Tricks: Catching Mistakes in ContractsContracts may be quite complex, as complex as code in fact, so it is not surprising that they contain errors sometimes. GNATprove can help by…
  52. Feb 20, 2015Johannes KanigTesting, Static Analysis, and Formal Verification
  53. Feb 19, 2015Yannick MoyAdaCore Tech Days Prez on SPARK
  54. Apr 30, 2014Yannick MoyUse of SPARK in a Certification ContextUsing SPARK or any other formal method in a certification requires that the applicant agrees with the certification authority on the verification…

2014 25

  1. May 19, 2014Gem #159 : GPRinstall - Part 2GPRinstall is a tool recently developed by AdaCore that provides an easy way to install a project, whether it be a standard project, a library…
  2. Jun 03, 2014Yannick MoyShort Video Demo of SPARK 2014New to SPARK? Want to "see" what's new in SPARK 2014? It's all in this 5 mn video demo!
  3. Jun 23, 2014Gem #160 : Developing unit tests with GNATtestNo one likes to spend the time on testing. It's tedious and boring writing the test harness, the tests themselves, and keeping them in sync with your…
  4. Jun 26, 2014Claire DrossManual Proof with Ghost Code in SPARK 2014Guiding automatic solvers by adding intermediate assertions is a commonly used technique. We can go further in this direction, by adding complete…
  5. Jul 25, 2014Claire DrossExternal Axiomatizations: a Trip Into SPARK’s InternalsThere are cases expressing all the specification of a package in SPARK is either impossible (for example if you need to link them to elements of the…
  6. Jul 29, 2014Johannes KanigExplicit Assumptions in SPARK 2014In this article, we provide a short introduction to our paper at the Test and Proof 2014 conference in York, UK.
  7. Aug 04, 2014Gem #161 : So long and thanks for all the memories!In this final Gem we look back over some highlights of the series, including the topics covered and your favorite Gems. We also look to the future…
  8. Aug 20, 2014Yannick MoyUsing SPARK to Prove AoRTE in Robot Navigation SoftwareCorrectness of robot software is a challenge. Just proving the absence of run-time errors (AoRTE) in robot software is a challenge big enough that…
  9. Oct 09, 2014Johannes KanigSPARK 15: Errors, Warnings and ChecksThe messages issued by the SPARK toolset will change a bit in the next version of both SPARK Pro and SPARK GPL. This post explains the change and the…
  10. Dec 05, 2014Yannick MoyUsing Coq to Verify SPARK 2014 CodeIn the first release of SPARK 2014, GNATprove only provided support for automatic provers, in particular Alt-Ergo. Automatic provers are very handy…
  11. Jan 07, 2015Yannick MoySPARK 2014 Rationale: Ghost CodeA common situation when proving properties about a program is that you end up writing additional code whose only purpose is to help proving the…
  12. Feb 04, 2014Gem #156: Listing Control in GNAT
  13. Mar 03, 2014Gem #157: Gprbuild and Code GenerationThis series of Gems explains how gprbuild can be configured to invoke code generators before it compiles the resulting code itself.
  14. Mar 02, 2014Yannick MoyGNATprove Tips and Tricks: How to Write Loop InvariantsHaving already presented in previous posts why loop invariants are necessary for formal verification of programs with loops, and what loop invariants…
  15. Mar 18, 2014Florian SchandaInformation Flo(w): Array Initialization in LoopsSPARK only supported array initialization using aggregates, as array initialization in loops raised a false alarm in flow analysis. Read on to learn…
  16. Mar 18, 2014Florian SchandaSPARK 2014 Rationale: Data DependenciesPrograms often use a few global variables. Global variables make passing common information between different parts of a program easier. By reading…
  17. Mar 19, 2014Johannes KanigA Little Exercise With StringsI recently looked at string manipulation functions in a library and tried to prove absence of run-time errors of one of them. Although the function…
  18. Mar 31, 2014Yannick MoyStudies of Contracts in PracticeTwo recent research papers focus on how program contracts are used in practice in open source projects, in three languages that support contracts…
  19. Apr 16, 2014Yannick MoyContextual Analysis of Subprograms Without ContractsWe have implemented a new feature in GNATprove for analyzing local subprograms in the context of their calls. This makes it possible to benefit from…
  20. Apr 11, 2014Johannes KanigProve in Parallel with SPARK 2014The article explains how we improved the performance of the SPARK 2014 toolset when multiple CPU cores are available for proof.
  21. Apr 25, 2014Claire DrossContracts of Functions in SPARK 2014In SPARK 2014, we can write a function F and annotate it with a pre and a postcondition. In this post, we explain how the SPARK 2014 proof tool…
  22. Apr 25, 2014Florian SchandaSPARK 2014 Rationale: Information FlowIn a previous blog post we described how aspect Global can be used to designate the specific global variables that a subprogram has to read and…
  23. Apr 28, 2014Gem #158: GPRinstall - Part 1GPRinstall is a tool recently developed by AdaCore that provides an easy way to install a project, whether it be a standard project, a library…
  24. Oct 09, 2013Gem #153: Multicore Maze Solving, Part 1
  25. Oct 20, 2013Yannick MoySPARK 2014 Rationale: Mixing SPARK and Ada CodeThe first step before any formal verification work with SPARK is to delimitate the part of the code that will be subject to formal verification…

2013 33

  1. Oct 28, 2013Gem #154: Multicore Maze Solving, Part 2
  2. Nov 13, 2013Yannick MoySPARK 2014 Rationale: Global StateGlobal variables are a common source of programming errors: they may fail to be initialized properly, they can be modified in unexpected ways,…
  3. Nov 20, 2013Yannick MoyGNATprove Tips and Tricks: Referring to Input in ContractsIn a previous post about pre-call values, I described how the Ada language rules implemented in the compiler prevent surprises when referring to…
  4. Nov 29, 2013Claire DrossSPARK 2014 Rationale: Formal ContainersSPARK 2014 excludes data structures based on pointers. Instead, one can use the library of formal containers. They are variant of the Ada 2012…
  5. Dec 05, 2013Yannick MoyRail, Space, Security: Three Case Studies for SPARK 2014We will present three case studies using SPARK 2014 at the upcoming Embedded Real Time Software and Systems conference in Toulouse in February 2014,…
  6. Dec 09, 2013Gem #155: Enhancing the GPRBuild Database for a New Language
  7. Dec 13, 2013Claire DrossSPARK 2014 Rationale: Expressing Properties over Formal ContainersWe saw in a previous post how formal containers can be used in SPARK code. In this post, I describe how to express properties over the content of…
  8. Dec 19, 2013Yannick MoyMuen Separation Kernel Written in SPARKThe University of Applied Sciences Rapperswil in Switzerland has released last week an open-source separation kernel written in SPARK, which has been…
  9. Jan 17, 2014Claire DrossSPARK 2014 Rationale: Verifying Properties over Formal ContainersWe saw in a previous post how we could express complex properties over formal containers using quantified expressions. In this post, I present how…
  10. Jan 21, 2014Yannick MoyCase Study for System to Software Integrity Includes SPARK 2014My colleague Matteo Bordin will present at the upcoming Embedded Real Time Software and Systems conference in Toulouse in February a case study…
  11. Jun 03, 2013Gem #149 : Asserting the truth, but (possibly) not the whole truth
  12. Jun 17, 2013Gem #150: Out and Uninitialized
  13. Jul 01, 2013Gem #151 : Specifying Mathematical Properties of Programs
  14. Jul 07, 2013Yannick MoySPARK 2014 Rationale: Contract CasesBesides the usual expression of a subprogram contract as a pair of a precondition and a postcondition, SPARK 2014 provides a way to express such a…
  15. Jul 07, 2013Johannes KanigSPARK 2014 goes to Space!David Lesens from Astrium was a member of the Hi-Lite project ("was" because the project is finished now, see the previous post), and has tried…
  16. Jul 15, 2013Yannick MoySPARK 2014 Rationale: Specification FunctionsSpecifying a program's behavior is seldom expressible in a satisfiable way without the capability of abstraction provided by function calls. Yet,…
  17. Jul 25, 2013Florian SchandaSPARK 2014 Flow AnalysisWe have nearly finished implementing a central component of the SPARK 2014 analysis tools: the flow analysis engine; so this is a good time to…
  18. Sep 14, 2013Yannick MoySPARK 2014 Rationale: Pre-call and Pre-loop ValuesSubprogram contracts are commonly presented as special assertions: the precondition is an assertion checked at subprogram entry, while the…
  19. Aug 04, 2013Yannick MoyMISRA-C 2012 vs SPARK 2014, the Subset Matching GameThe MISRA C subset of C defines around 150 rules that restrict C programs for critical software development. Of these, 27 rules are classified as…
  20. Sep 23, 2013Gem #152 : Defining a New Language in a Project File
  21. Sep 29, 2013Yannick MoySPARK 2014 Rationale: Loop InvariantsFormal verification tools like GNATprove rely on two main inputs from programmers: subprogram contracts (preconditions and postconditions) and loop…
  22. Oct 04, 2013Yannick MoySPARK 2014 Rationale: Loop VariantsLoop variants are the little-known cousins of the loop invariants, used for proving termination of subprograms. Although they may not look very…
  23. Dec 10, 2012Gem #138 : Master the Command Line - Part 1
  24. Jan 14, 2013Gem #139 : Master the Command Line - Part 2
  25. Jan 28, 2013Gem #140: Bridging the Endianness Gap
  26. Feb 11, 2013Gem #141 : Con-figure it out
  27. Feb 25, 2013Gem #142 : Exception-ally
  28. Mar 11, 2013Gem #143 : Return to the Sources
  29. Mar 25, 2013Gem #144: A Bit of Bytes: Characters and Encoding Schemes
  30. Apr 08, 2013Gem #145: Ada Quiz 3 - Statements
  31. Apr 22, 2013Gem #146 : Su(per)btypes in Ada 2012 - Part 1
  32. May 06, 2013Gem #147 : Su(per)btypes in Ada 2012 - Part 2
  33. May 20, 2013Gem #148 : Su(per)btypes in Ada 2012 - Part 3

2012 25

  1. Jun 02, 2013Yannick MoyProject Hi-Lite Wrap-upAfter three years of hard work, we have reached last week the end of project Hi-Lite, whose goal was to simplify the use of formal methods. We're…
  2. May 28, 2012Gem #126 : Aggregate Library Projects
  3. Jun 11, 2012Gem #127: Iterators in Ada 2012 - Part 1
  4. Jun 25, 2012Gem #128 : Iterators in Ada 2012 - Part 2
  5. Jul 09, 2012Gem #129 : Type-Safe Database API - Part 1
  6. Jul 23, 2012Gem #130 : Type-Safe Database API - Part 2
  7. Aug 07, 2012Gem #131 : Type-Safe Database API - Part 3
  8. Sep 10, 2012Gem #132 : Erroneous Execution - Part 1
  9. Sep 24, 2012Gem #133 : Erroneous Execution - Part 2
  10. Oct 15, 2012Gem #134 : Erroneous Execution - Part 3
  11. Oct 29, 2012Gem #135 : Erroneous Execution - Part 4
  12. Nov 12, 2012Gem #136: How tall is a kilogram?
  13. Nov 26, 2012Gem #137: Ada Quiz 2 - An Heir and a Spare?
  14. Feb 01, 2012Gem #114: Logging with GNATCOLL.Traces
  15. Feb 01, 2012Gem #115: Lego Mindstorms Ada Environment — Part 2
  16. Feb 01, 2012Gem #116: Ada and C++ Exceptions
  17. Feb 01, 2012Gem #117: Design Pattern: Overridable Class Attributes in Ada 2012
  18. Feb 27, 2012Gem #119 : GDB Scripting— Part 1
  19. Feb 13, 2012Gem #118: File-System Portability Issues and GNATCOLL.VFS
  20. Mar 12, 2012Gem #120 : GDB Scripting — Part 2
  21. Mar 12, 2012Gem #121 Breakpoint Commands — Part 1
  22. May 14, 2012Gem #125: Detecting infinite recursion with GDB's Python API
  23. Apr 30, 2012Gem #124 : Scripting GPS for Static Analysis
  24. Apr 17, 2012Gem #123: Implicit Dereferencing in Ada 2012
  25. Apr 10, 2012Gem #122: Breakpoint Commands — Part 2

2011 17

  1. Mar 28, 2011Gem #102: SOAP/WSDL client part
  2. Apr 11, 2011Gem #103: Code Archetypes for Real-Time Programming — Part 5
  3. Apr 26, 2011Gem #104: Gprbuild and Configuration Files — Part 1
  4. May 09, 2011Gem #105: Lady Ada Kisses Python — Part 1
  5. May 23, 2011Gem #106: Lady Ada Kisses Python — Part 2
  6. Jun 06, 2011Gem #107: Preventing Deallocation for Reference-counted Types
  7. Jun 17, 2011Gem #108: Gprbuild and Configuration Files — Part 2
  8. Sep 05, 2011Gem #109: Ada Plug-ins and Shared Libraries — Part 1
  9. Sep 21, 2011Gem #110: Ada Plug-ins and Shared Libraries — Part 2
  10. Oct 03, 2011Gem #111: The Distributed Systems Annex, Part 5 — Embedded Name Server
  11. Oct 17, 2011Gem #112: Lego Mindstorms Ada Environment — Part 1
  12. Nov 07, 2011Gem #113: Visitor Pattern in Ada
  13. Sep 14, 2010Gem #90: The Distributed Systems Annex, Part 4 — DSA and C
  14. Sep 27, 2010Gem #91: Smart Completion (Part 2 of 2)
  15. Oct 11, 2010Gem #92: Code Archetypes for Real-Time Programming - Part 2
  16. Oct 25, 2010Gem #93: High Performance Multi-core Programming - Part 1
  17. Nov 08, 2010Gem #94: Code Archetypes for Real-Time Programming - Part 3

2010 20

  1. Nov 22, 2010Gem #95: Dynamic Stack Analysis in GNAT
  2. Dec 06, 2010Gem #96: Code Archetypes for Real-Time Programming - Part 4
  3. Jan 17, 2011Gem #97: Reference Counting in Ada - Part 1
  4. Jan 31, 2011Gem #98: High Performance Multi-core Programming - Part 2
  5. Feb 14, 2011Gem #99: Reference Counting in Ada - Part 2: Task Safety
  6. Feb 28, 2011Gem #100: Reference Counting in Ada - Part 3: Weak References
  7. Mar 14, 2011Gem #101: SOAP/WSDL server part
  8. Jan 25, 2010Gem #78: Where did my memory go? (Part 2)
  9. Feb 08, 2010Gem #79: Where did my memory go? (Part 3)
  10. Feb 25, 2010Gem #80: Speedy Shift and Rotate in SPARK
  11. Mar 08, 2010Gem #81: GNAT Semaphores
  12. Mar 22, 2010Gem #82: Type-Based Security 1: Handling Tainted Data
  13. Apr 05, 2010Gem #83: Type-Based Security 2: Validating the Input
  14. Apr 19, 2010Gem #84: The Distributed Systems Annex 1 - Simple client/server
  15. May 03, 2010Gem #85:The Distributed Systems Annex 2 — Distributed Objects
  16. May 17, 2010Gem #86: Ada Quiz 1 - Basic Types
  17. Jun 02, 2010Gem #87: The Distributed Systems Annex, Part 3 — Mailboxes
  18. Jun 14, 2010Gem #88: GPS - Smart Completion (Part 1 of 2)
  19. Jun 22, 2010Gem #89: Code Archetypes for Real-Time Programming - Part 1
  20. Jun 01, 2009Gem #66: GPS's Key Shortcuts Editor

2009 21

  1. Jun 15, 2009Gem #67: Managing the GPS Workspace
  2. Jun 29, 2009Gem #68: Let's SPARK! — Part 1
  3. Sep 07, 2009Gem #69: Let's SPARK! — Part 2
  4. Sep 21, 2009Gem #70: The Scope Locks Idiom
  5. Oct 05, 2009Gem #71: Tokeneer Discovery - Lesson 1
  6. Oct 19, 2009Gem #72: Tokeneer Discovery - Lesson 2
  7. Nov 02, 2009Gem #73: Tokeneer Discovery - Lesson 3
  8. Nov 16, 2009Gem #74: Tokeneer Discovery - Lesson 4
  9. Nov 30, 2009Gem #75: Tokeneer Discovery - Lesson 5
  10. Dec 14, 2009Gem #76: Tokeneer Discovery - Lesson 6
  11. Jan 11, 2010Gem #77: Where did my memory go? (Part 1)
  12. Nov 24, 2008Gem #54: Scripting Capabilities in GNAT (Part 2)
  13. Dec 08, 2008Gem #55: Introduction to Ada / Java Interfacing
  14. Jan 12, 2009Gem #56: Creating Ada to Java calls using GNAT-AJIS
  15. Jan 26, 2009Gem #57: Ada / Java cross dispatching
  16. Feb 09, 2009Gem #58: Ada / Java exception handling
  17. Feb 23, 2009Gem #59: Generating Ada bindings for C headers
  18. Mar 09, 2009Gem #60: Generating Ada bindings for C++ headers
  19. Mar 23, 2009Gem #61: Interfacing with C++ constructors
  20. Apr 06, 2009Gem #62: C++ constructors and Ada 2005
  21. Apr 21, 2009Gem #63: The Effect of Pragma Suppress

2008 33

  1. May 04, 2009Gem #64: Handling Multiple-Unit Source Files
  2. May 18, 2009Gem #65: gprbuild
  3. Jul 07, 2008Gem #42: Safe and Secure Software : Chapter 6, Safe Object Construction
  4. Sep 08, 2008Gem #43: Safe and Secure Software : Chapter 7, Safe Memory Management
  5. Sep 15, 2008Gem #44: Accessibility Checks (Part III)
  6. Sep 22, 2008Gem #45: Safe and Secure Software : Chapter 8, Safe Startup
  7. Sep 29, 2008Gem #46: Incompatibilities between Ada 83 and Ada 95
  8. Oct 06, 2008Gem #47: Safe and Secure Software : Chapter 9, Safe Communication
  9. Oct 13, 2008Gem #48: Extending Interfaces in Ada 2005
  10. Oct 20, 2008Gem #49: Safe and Secure Software: Chapter 10, Safe Concurrency
  11. Oct 27, 2008Gem #50: Overload Resolution
  12. Nov 03, 2008Gem #51: Safe and Secure Software: Chapter 11, Certified Safe with SPARK
  13. Nov 10, 2008Gem #52: Scripting Capabilities in GNAT (Part 1)
  14. Nov 17, 2008Gem #53: Safe and Secure Software: Chapter 12: Conclusion
  15. Apr 08, 2008Gem #30: Safe and Secure Software : Introduction
  16. Apr 14, 2008Gem #31: Preconditions/postconditions
  17. Apr 21, 2008Gem #32: Safe and Secure Software : Chapter 1, Safe Syntax
  18. Apr 28, 2008Gem #33: Accessibility Checks (Part I: Ada95)
  19. May 05, 2008Gem #34: Safe and Secure Software : Chapter 2, Safe Typing
  20. May 12, 2008Gem #35: Bounded buffer package in GNAT hierarchy (Part 1)
  21. May 19, 2008Gem #36: Safe and Secure Software : Chapter 3, Safe Pointers
  22. May 26, 2008Gem #37: Bounded Buffer package in GNAT Hierarchy (Part 2)
  23. Jun 02, 2008Gem #38: Safe and Secure Software : Chapter 4, Safe Architecture
  24. Jun 09, 2008Gem #39: Efficient Stream I/O for Array Types
  25. Jun 16, 2008Gem #40: Safe and Secure Software : Chapter 5, Safe Object Oriented Programming
  26. Jun 30, 2008Gem #41: Accessibility Checks (Part II: Ada2005)
  27. Nov 19, 2007Gem #18: Warnings in GNAT
  28. Nov 26, 2007Gem #19: XML streaming of Ada objects
  29. Dec 03, 2007Gem #20: Using pragma Shared_Passive for data persistence
  30. Dec 10, 2007Gem #21: How to parse an XML text
  31. Dec 17, 2007Gem #22: Ada Speaks Many Languages
  32. Jan 14, 2008Gem #23: Null Considered Harmful
  33. Jan 28, 2008Gem #24: Null Considered Harmful (Part 2—Efficiency)

2007 22

  1. Feb 11, 2008Gem #25: How to Search Text
  2. Feb 25, 2008Gem #26: The Mod Attribute
  3. Mar 03, 2008Gem #27: Changing Data Representation (Part 1)
  4. Mar 17, 2008Gem #28: Changing Data Representation (Part 2)
  5. Mar 31, 2008Gem #29: Introduction to the Ada Web Server (AWS)
  6. Jun 18, 2007Gem #6: The Ada95 Multiple Views Idiom vs. Ada05 Interfaces
  7. Jun 25, 2007Gem #7: The Beauty of Numeric Literals in Ada
  8. Sep 10, 2007Gem #8: Factory Functions
  9. Sep 17, 2007Gem #9: Classwide Operations, Iterators, and Generic Algorithms
  10. Sep 24, 2007Gem #10: Limited Types in Ada 2005 — Extended Return Statements
  11. Oct 01, 2007Gem #11: Limited Types in Ada 2005 — Constructor Functions Part 2
  12. Oct 08, 2007Gem #12: Limited Types in Ada 2005 — <> Notation Part 2
  13. Oct 15, 2007Gem #13: Interrupt Handling Idioms (Part 1)
  14. Oct 22, 2007Gem #14: Interrupt Handling Idioms (Part 2)
  15. Oct 29, 2007Gem #15: Timers
  16. Nov 05, 2007Gem #16: Pragma No_Return
  17. Nov 12, 2007Gem #17: Pragma No_Return, Part 2 (functions)
  18. May 14, 2007Gem #1: Limited Types in Ada 2005 — Limited Aggregates
  19. May 21, 2007Gem #2: Limited Types in Ada 2005 — <> Notation in Aggregates
  20. May 28, 2007Gem #3: Limited Types in Ada 2005 — Constructor Functions
  21. Jun 04, 2007Gem #4: PWM Position Control for Radiocontrol Servos
  22. Jun 11, 2007Gem #5: Key-Based Searching In Set Containers