Aerospace & Defence
Airborne & Space Software Verification
Formal verification for DO-178C, DO-330, and ARP4754A. We help avionics and space software teams produce the rigorous evidence that certification authorities demand.
The challenge
Regulators demand formal evidence, not test reports
DO-178C certification at DAL A requires that every safety requirement is verified by an independent means — and that coverage is formally demonstrated. Test suites cannot achieve this in isolation. The standard is increasingly interpreted to require formal methods as part of the assurance case.
ESBMC produces formal verification evidence — a mathematical proof or a concrete counterexample — that is directly usable as a DO-178C verification artefact. This is evidence that a test report simply cannot provide.
Target sectors
Compliance
Standards we address
DO-178C
Software Considerations in Airborne Systems and Equipment Certification — the primary standard for airborne software assurance at DAL A–E.
DO-330
Software Tool Qualification Standard — required to qualify ESBMC as a verification tool in your DO-178C workflow.
ARP4754A
Guidelines for Development of Civil Aircraft and Systems — system-level development assurance.
DO-254
Design Assurance Guidance for Airborne Electronic Hardware — hardware-level formal methods.
Our role
How we help
Safety property definition
We work with your safety engineers to encode the safety requirements from your system specification as verifiable ESBMC properties.
DO-330 tool qualification
We provide the support documentation needed to qualify ESBMC as a verification tool under DO-330, including tool operational requirements and validation evidence.
MCDC & coverage evidence
ESBMC can produce formal evidence of Modified Condition/Decision Coverage — admissible in DAL A and B software verification plans.
Counterexample-driven debugging
When ESBMC finds a property violation, it produces a concrete execution trace — giving your engineers a reproducible test case, not just a warning.
Working toward DO-178C certification?
Let's discuss how ESBMC-based formal verification fits into your assurance plan. We work with avionics teams from DAL C through DAL A.