SPARK by Example is an adaptation of ACSL by Example for SPARK 2014, a programming language which is a formally verified subset of Ada
-
Updated
Jul 2, 2021 - Ada
#
formal-specification
Here are 42 public repositories matching this topic...
Public snapshots of "ACSL by Example"
-
Updated
Jun 17, 2021 - TeX
Example implementation of Arm's Architecture Specification Language (ASL)
-
Updated
Aug 30, 2019 - OCaml
Formal message specification and generation of verifiable binary parsers and message generators
-
Updated
Aug 6, 2021 - Python
Galois RISC-V ISA Formal Tools
-
Updated
May 14, 2021 - Haskell
Linux kernel library functions formally verified.
-
Updated
Feb 11, 2021 - C
Toolset to capture, simulate, synthesize and verify graph models
fsm
async
simulation
eda
cad
petri-nets
circuit
formal-verification
logic-synthesis
stg
formal-specification
-
Updated
Aug 5, 2021 - Java
This is solc-verify, a modular verifier for Solidity.
-
Updated
Jan 27, 2021 - C++
Frama-C and WP tutorial
-
Updated
Jul 28, 2021 - TeX
Klever Git repository read-only mirror
c
static-analysis
verification
specification
model-checking
formal-methods
software-verification
formal-verification
formal-specification
-
Updated
Aug 6, 2021 - Python
A TLA+ implementation of the Avalanche Protocol Family, both for learning Avalanche and TLA+
-
Updated
May 8, 2020 - TLA
Formal analysis for the Electrod formal specification language
-
Updated
Jun 2, 2021 - OCaml
ViennaTalk, a LIVE IDE for VDM-SL based on Pharo Smalltalk
-
Updated
Aug 3, 2021 - Smalltalk
Formal specification for Miniscript in Alloy
-
Updated
Dec 15, 2020 - Alloy
Formal models of vac protocols
-
Updated
Mar 18, 2020 - TLA
A Tool for Timed Patten Matching with Automata-Based Acceleration
automata
monitoring
regular-expression
data-streaming
monitoring-tool
runtime-verification
formal-specification
-
Updated
Jun 8, 2021 - C++
A code generator from high-level formal specifications for monitoring and pattern matching sequential/temporal data.
monitoring
data-stream
regular-expression
stream-processing
temporal-logic
code-generation
monitoring-tool
temporal-data
runtime-verification
formal-specification
-
Updated
Dec 20, 2019 - Python
An implementation of a reactive GR(1) contract
-
Updated
Nov 13, 2020 - Python
Evrostos: The rLTL Verifier
verification
ltl
formal-methods
acm
spin
formal-verification
nusmv
robustness
formal-specification
verification-programming
rltl-verifier
rltl-specification
hscc
-
Updated
Feb 1, 2021 - C
Paxos algorithm specified and proved in TLA+/PlusCal, with separate processes and invariants for proposers and acceptors.
distributed-systems
verification
paxos
formal-verification
tla
formal-specification
formal-proofs
pluscal
tlaplus
-
Updated
Sep 19, 2018 - TLA
Shellcode synthesizer
-
Updated
Jan 27, 2021 - OCaml
VDM-SL execution library using public/private VDMPad servers.
-
Updated
Jun 9, 2015 - Python
A formal specification written in Event-B notation that formally specifies the behaviour of a multi-lift elevator system.
-
Updated
Apr 22, 2017
A formally specified UNO game using B-Method
-
Updated
Jun 19, 2018 - C
-
Updated
Dec 20, 2019 - TeX
A repository that describes my explorations on formal verification using Dafny, techniques from programming language theory such as CYK parsing, Earley parsing, type-theoretic things like lambda calculus etc.
lambda-calculus
lambda-expressions
dafny
earley-algorithm
formal-verification
earley-parser
turing-completeness
formal-specification
loop-invariants
weakest-preconditions
cyk-algorithm
church-thesis
-
Updated
Jun 23, 2021 - Python
Examples of formal verifications written in Dafny.
-
Updated
May 10, 2021 - Dafny
Extended concepts and for testing software, combining technologies such as Unit / Integration Tests, Interface Testing or Formal Methods such as Model Checking.
testing
unit-testing
integration-testing
software
model-checking
formal-methods
formal-verification
formal-specification
formal-proofs
interface-testing
-
Updated
Apr 17, 2020
security
social-network
credit-card
set-theory
rbac
formal-methods
role-based-access-control
access-control
formal-verification
formal-languages
role-based
access-control-list
formal-specification
mandatory-access-control
formal-models
alloy-analyzer
z-notation
access-control-patterns
barber-paradox
discretionary-access-control
-
Updated
Jul 12, 2020 - Alloy
JSON parser/printer for VDM-SL
-
Updated
Dec 25, 2013
Improve this page
Add a description, image, and links to the formal-specification topic page so that developers can more easily learn about it.
Add this topic to your repo
To associate your repository with the formal-specification topic, visit your repo's landing page and select "manage topics."