High Integrity Software - The SPARK Approach to Safety and Security

By J. Barnes. 2003

434 citations recorded by the source corpus.

View Paper: https://www.semanticscholar.org/paper/1e14c528475719d57d31e13147912c5c3c59f3b2

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

Citations in the corpus

Verifiable functional purity in java (2008, background): “Similarly, both Euclid [14] and SPARK [2] define two distinct constructs for routines: procedures can have side effects, while functions are only able to compute a value (and thus are guaranteed to be free of side effects).”
A Survey of Automated Techniques for Formal Software Verification (2008, background): “They are useful for computing inequality constraints about integer variables and for deriving such invariants for nested program loops.”
The Spec# Programming System: An Overview (2004, background): “SPARK offers a selection of static tools, from lightweight sanity checking to full verification with an interactive theorem prover.”
A Hardware Design Language for Timing-Sensitive Information-Flow Security (2015, background): “Programming languages that provide the ability to label variables have been developed before [6, 25, 36], but their labels are not expressive enough to handle practical hardware designs where resources need to be shared across security levels.”
An overview of JML tools and applications (2003, background): “com, [4]) is an initiative similar to JML in many respects, but much more mature, and targeting Ada rather than Java.”
Formal methods: Practice and experience (2009, unknown): “The core functionality of the system was written in SPARK, a subset of Ada with an accompanying tool-set, which was speci.cally designed for writing software for high-integrity applications [Barnes 2003].”