• DocumentCode
    2997199
  • Title

    Integrating test and proof in the verifiable spark 2014 language using contracts and SMT solvers

  • Author

    Taft, Tucker

  • Author_Institution
    AdaCore Inc., Lexington, MA, USA
  • fYear
    2013
  • fDate
    5-10 Oct. 2013
  • Firstpage
    1
  • Lastpage
    21
  • Abstract
    Cost of testing greater than cost of development. 100/0 increase each year for avionics software (Boeing META Project). Uneven partitioning, uneven quality: 800/0 of errors traced to 200/0 of code. Need to reduce and focus the cost of testing. Formal methods might be the primary source of evidence for the satisfaction of many of the objectives concerned with development and verification.
  • Keywords
    aerospace computing; avionics; computability; contracts; formal languages; formal verification; program testing; SMT solvers; Verifiable Spark 2014 Language; avionics software; contracts; cost of development; cost of testing; cost reduction; formal methods; uneven partitioning; uneven quality; Aerospace electronics; Multicore processing; Software; Testing;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    Digital Avionics Systems Conference (DASC), 2013 IEEE/AIAA 32nd
  • Conference_Location
    East Syracuse, NY
  • ISSN
    2155-7195
  • Print_ISBN
    978-1-4799-1536-1
  • Type

    conf

  • DOI
    10.1109/DASC.2013.6719720
  • Filename
    6719720
    • Link To Document
    https://search.isc.ac/dl/search/defaultta.aspx?DTC=49&DC=2997199