spark-by-example
Formal verification adapter
An adaptation of ACSL by Example for SPARK 2014 to verify Ada programs with formal methods
SPARK by Example is an adaptation of ACSL by Example for SPARK 2014, a programming language which is a formally verified subset of Ada
152 stars
15 watching
16 forks
Language: Ada
last commit: over 2 years ago
Linked from 1 awesome list
adaformal-methodsformal-specificationformal-verification
ohenley/awesome-adaRelated projects:
| Repository | Description | Stars |
|---|---|---|
 rocher/ob-ada-spark | Supports Ada and SPARK programming languages in Emacs org-babel for compiling, running, and formal verification of code | 8 |
 jklmnn/continuous-verification | Automates Ada software verification with continuous testing and proofing | 9 |
 jhumphry/ascon_spark | An implementation of the Ascon AEAD algorithm in Ada 2012 / SPARK 2014 for cryptographic encryption and decryption. | 3 |
 rod-chapman/sparknacl | Re-implementation of the TweetNaCl crypto library in Ada with static type safety and performance optimization. | 114 |
 adacore/spark_railway_simulation_demo | Demonstrates a railway network simulation with SPARK Ada to ensure train collision prevention through formal verification. | 5 |
| adacore/spark2014 | A software development technology designed to produce ultra-low defect software | 248 |
| jhumphry/spark_norx | An implementation of a widely used authenticated encryption algorithm | 8 |
| adacore/rc_car_demo | Demonstrates robotics with Ada and SPARK in an embedded environment using Lego sensors and effectors on a custom-built RC car. | 6 |
 ada-actions/toolchain | Automates installation of an Ada development environment. | 20 |
 alex-gamper/ada-languageserver | An LSP client prototype for Visual Studio 2017 implementing support for the Ada programming language | 1 |
| jklmnn/stotp | A time-based one-time pad implementation library for two-factor authentication | 8 |
 uwplse/cheerios | A formally verified serialization library for Coq | 23 |
 atalii/adage | A simple and secure alternative to sudo and doas for running commands with elevated privileges. | 6 |
 sol/doctest | Tools for verifying and validating Haskell code examples | 373 |
| adacore/tictactoe | A tictactoe game written in Ada using the SPARK language and proven at runtime | 3 |