Using the SPARK toolset for showing the absence of run-time errors in safety-critical software. This paper reports the results of a study into the effectiveness of the SPARK toolset for showing the absence of run-time errors in safety-critical Ada software. In particular, the toolset is examined to determine how effective it is in finding run-time errors in a SPARK program, and how much of the process of proving freedom from run-time errors can be performed automatically. The study identifies areas where automatic run-time checks are not so effective and, where possible, gives recommendations about the design of the software so that the toolset is as effective as possible in automatically proving absence of run-time errors.par The results will be of interest to anyone contemplating the use of the SPARK toolset for ensuring the absence of run-time errors, both as guidance in planning the effort required, and for practical advice on making the best use of the toolset.

References in zbMATH (referenced in 48 articles , 1 standard article )

Showing results 1 to 20 of 48.
Sorted by year (citations)

1 2 3 next

  1. Grigoriy Volkov, Mikhail Mandrykin, Denis Efremov: Lemma Functions for Frama-C: C Programs as Proofs (2018) arXiv
  2. Belo Lourenço, Cláudio; João Frade, Maria; Sousa Pinto, Jorge: Formalizing single-assignment program verification: an adaptation-complete approach (2016)
  3. Bartoletti, Massimo; Castellani, Ilaria; Deniélou, Pierre-Malo; Dezani-Ciancaglini, Mariangiola; Ghilezan, Silvia; Pantovic, Jovanka; Pérez, Jorge A.; Thiemann, Peter; Toninho, Bernardo; Vieira, Hugo Torres: Combining behavioural types with security analysis (2015)
  4. McCormick, John W.; Chapin, Peter C.: Building high integrity applications with SPARK (2015)
  5. Duracz, Jan; Konečný, Michal: Polynomial function intervals for floating-point software verification (2014)
  6. Miyazawa, Alvaro; Cavalcanti, Ana: Refinement-based verification of implementations of Stateflow charts (2014) ioport
  7. Cavalcanti, Ana; Wellings, Andy; Woodcock, Jim: The safety-critical Java memory model formalised (2013)
  8. Carlsson, Mats; Mildner, Per: SICStus Prolog -- the first 25 years (2012)
  9. Crolard, T.; Polonowski, E.: Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control (2012)
  10. Beringer, Lennart: Relational decomposition (2011)
  11. Chapman, Roderick; Botcazou, Eric; Wallenburg, Angela: SPARKSkein: a formal and fast reference implementation of Skein (2011) ioport
  12. Amtoft, Torben; Hatcliff, John; Rodríguez, Edwin: Precise and automated contract-based reasoning for verification and certification of information flow properties of programs with arrays (2010)
  13. Böhme, Sascha; Moskal, Michał; Schulte, Wolfram; Wolff, Burkhart: HOL-Boogie -- an interactive prover-backend for the verifying C compiler (2010)
  14. Bornat, Richard; Amjad, Hasan: Inter-process buffers in separation logic with rely-guarantee (2010)
  15. Lesens, David: Using static analysis in space: why doing so? (2010) ioport
  16. Russo, Alejandro; Sabelfeld, Andrei; Li, Keqin: Implicit flows in malicious and nonmalicious code (2010)
  17. Dévai, G.; Pataki, N.: A tool for formally specifying the (C++) standard template library (2009)
  18. Laski, Janusz; Stanley, William: Software verification and analysis. An integrated, hands-on approach (2009)
  19. Singhoff, Frank; Plantec, Alain; Dissaux, Pierre; Legrand, Jérôme: Investigating the usability of real-time scheduling theory with the Cheddar project (2009)
  20. Dévai, Gergely: Programming language elements for correctness proofs (2008)

1 2 3 next