SPARK

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 46 articles , 1 standard article )

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

1 2 3 next

  1. 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)
  2. McCormick, John W.; Chapin, Peter C.: Building high integrity applications with SPARK (2015)
  3. Duracz, Jan; Konečný, Michal: Polynomial function intervals for floating-point software verification (2014)
  4. Miyazawa, Alvaro; Cavalcanti, Ana: Refinement-based verification of implementations of Stateflow charts (2014)
  5. Cavalcanti, Ana; Wellings, Andy; Woodcock, Jim: The safety-critical Java memory model formalised (2013)
  6. Crolard, T.; Polonowski, E.: Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control (2012)
  7. Chapman, Roderick; Botcazou, Eric; Wallenburg, Angela: SPARKSkein: A formal and fast reference implementation of Skein (2011)
  8. 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)
  9. Böhme, Sascha; Moskal, Michał; Schulte, Wolfram; Wolff, Burkhart: HOL-Boogie -- an interactive prover-backend for the verifying C compiler (2010)
  10. Bornat, Richard; Amjad, Hasan: Inter-process buffers in separation logic with rely-guarantee (2010)
  11. Lesens, David: Using static analysis in space: why doing so? (2010)
  12. Russo, Alejandro; Sabelfeld, Andrei; Li, Keqin: Implicit flows in malicious and nonmalicious code (2010)
  13. Cohen, Ernie; Moskal, Michal; Tobies, Stephan; Schulte, Wolfram: A precise yet efficient memory model for C (2009)
  14. Dévai, G.; Pataki, N.: A tool for formally specifying the $C++$ standard template library (2009)
  15. Heitmeyer, Constance L.: On the role of formal methods in software certification: an experience report (2009)
  16. Laski, Janusz; Stanley, William: Software verification and analysis. An integrated, hands-on approach (2009)
  17. Singhoff, Frank; Plantec, Alain; Dissaux, Pierre; Legrand, Jér^ome: Investigating the usability of real-time scheduling theory with the Cheddar project (2009)
  18. Dévai, Gergely: Programming language elements for correctness proofs (2008)
  19. Henzinger, Thomas A.; Hottelier, Thibaud; Kovács, Laura: Valigator: A verification tool with bound and invariant generation (2008)
  20. Nanevski, Aleksandar; Morrisett, Greg; Birkedal, Lars: Hoare type theory, polymorphism and separation (2008)

1 2 3 next