Everything we do at AdaCore is centered around helping developers build the safest, most secure open-source software.
For over 25 years, we've worked with global leaders across avionics, aerospace and defense industries, building tools and providing services that ease the complex and difficult process of developing high-integrity software. As the need for truly secure and reliable applications expands into industries such as automotive, medical, energy, and IOT, we’re advancing our time-tested technologies to bring expertise and services to help a whole new generation of developers.
Our 150 experts worldwide in the US (New York), France (Paris, Toulouse, Grenoble and Vannes), the UK, Estonia and Germany all play a role in developing bleeding edge technologies to meet the highest grade of software development.
Joining AdaCore is about joining a culture of innovation, openness, collaboration and dependability, which defines how we work together, with our customers and partners.
Developed at AdaCore, CodePeer (https://www.adacore.com/codepeer) is an Ada source code analyzer that detects run-time and logic errors before program execution, serving as an automated peer reviewer. The analysis is static, in the sense that only the source code is considered -- the program is never executed.
We have recently integrated the open-source static analyzer Infer (https://fbinfer.com), developed by Facebook, in CodePeer. This includes a state-of-the-art modular Ada frontend, and some changes to the core of Infer. This integration offers us the possibility of having more lightweight analyses that complement well the initial capabilities of CodePeer. We want to pursue the exploration of the new results available through Infer.
Infer provides quite a few analyses that are not currently deployed in CodePeer. This page lists all of them, in the section “Analyses and Issue Types”. Currently, we only deploy Pulse. (We also used to launch BufferOverrun, but it was ultimately removed in favor of Pulse.) We want to experiment with the other existing analyses to decide:
Whether they would bring something to Ada users
Whether they are compatible with the current Ada frontend
What kind of adaptations are needed if they are deemed useful but not compatible
The intern will be responsible for assessing the points above. For Infer’s analyses that require “configuration”, such as Topl, he or she will also design the automata that describe the properties to check. Depending on the intern’s taste for Ada, new or derived analyses may be written to check properties currently not covered by CodePeer. Finally, the intern will experiment with these new analyses on large Ada codebases coming from AdaCore and its customers.
Skills required/nice to have:
Interest for experimentation
Experience/interest in static analysis and/or compilation
Some knowledge of OCaml would be a plus
During 2023 - 6 months