Development Log in categories Formal Methods

  • Introducing the CVC4 SMT solver - AdaCore internal seminar

    AdaCore Internal Seminar - Monday November 19, 2012.

    François Bobot of the ProVal team at INRIA, will come to the AdaCore Paris offices to give an introduction to the CVC4 SMT solver.

    AdaCore, from time to time, organizes seminars in the Paris offices. If you are interested in a particular talk, please send email to

  • Safe and reliable embedded linux programming

    Dr José Ruiz gave this talk at yesterday's Embed with Linux conference in Lorient, France. The talk provides an overview of techniques to design and implement reliable embedded applications. The goal is to achieve safe and analyzable behavior by construction, including handling parallel multiprocessor systems in an efficient and predictable way. The means to attain this objective is to statically configure the application to run on embedded linux platforms, and then to use run-time support to enforce constraints imposed to the system.


  • Formal Methods
    Mar 18th, 2012

    Integrating Formal Program Verification with Testing

    Access the paper here.

    Verification activities mandated for critical software are essential to achieve the required level of confidence expected in life-critical or business-critical software. They are becoming increasingly costly as, over time, they require the development and maintenance of a large body of functional and robustness tests on larger and more complex applications. Formal program verification offers a way to reduce these costs while providing stronger guarantees than testing. Addressing verification activities with formal verification is supported by upcoming standards such as do-178c for software development in avionics. In the Hi-Lite project, we pursue the integration of formal verification with testing for projects developed in C or Ada. In this paper, we discuss the conditions under which this integration is at least as strong as testing alone. We describe associated costs and benefits, using a simple banking database application as a case study.