AdaCore Blog

Alexander Senier

Alexander Senier is founder and CEO of Componolit, a company dedicated to the development of highly trustworthy systems. Since he started programming, he has been looking for concepts, tools and technologies to develop better software. Consequently, he is a strong advocate of component-based architectures and has used SPARK as his preferred language for more than a decade. Componolit produces open source libraries and tools for building security-critical components and provides consulting to customers in the areas of high security, mobile security and industrial IoT.

1 entries written by Alexander Senier

by Alexander Senier

RecordFlux: From Message Specifications to SPARK Code

Handling binary data is hard. Errors in parsers routinely lead to critical security vulnerabilities. In this post we show how the RecordFlux toolset eases the creation of formally verified binary parsers in SPARK.

#Formal Verification    #Formal Methods    #SPARK