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 1, 2019 - Ada
#
formal-specification
Here are 39 public repositories matching this topic...
Public snapshots of "ACSL by Example"
-
Updated
Apr 30, 2020 - C
Example implementation of Arm's Architecture Specification Language (ASL)
-
Updated
Aug 30, 2019 - OCaml
Galois RISC-V ISA Formal Tools
-
Updated
Apr 16, 2020 - Haskell
Linux kernel library functions formally verified.
-
Updated
Mar 30, 2020 - C
DanGardnerr
commented
Apr 15, 2016
Version Number: 3.0.9
OS: Windows 10 64 bit x64
Currently when editing properties in the "Property Editor" panel you can't use Tab to move between boxes. This makes quick editing of x and y values particularly tedious as you have to click away from one box to apply that change and into then next.
This is solc-verify, a modular verifier for Solidity.
-
Updated
Jun 29, 2020 - C++
Frama-C and WP tutorial
-
Updated
Jul 2, 2020 - TeX
Klever Git repository read-only mirror
c
static-analysis
verification
specification
model-checking
formal-methods
software-verification
formal-verification
formal-specification
-
Updated
Jul 3, 2020 - 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 11, 2020 - OCaml
ViennaTalk, a LIVE IDE for VDM-SL based on Pharo Smalltalk
-
Updated
Jun 24, 2020 - Smalltalk
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
Nov 12, 2019 - C++
Evrostos: The rLTL Verifier
verification
ltl
formal-methods
acm
formal-verification
nusmv
robustness
formal-specification
verification-programming
rltl-verifier
rltl-specification
hscc
-
Updated
Apr 6, 2020 - 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
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
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
An implementation of a reactive GR(1) contract
-
Updated
May 13, 2019 - Python
VDM-SL execution library using public/private VDMPad servers.
-
Updated
Jun 9, 2015 - Python
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
Jan 12, 2020 - Python
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
A model checking specification written in NuSMV that specifies a model of a single lift elevator system.
-
Updated
Apr 22, 2017 - Batchfile
Formal specification for student class written in VDM++
-
Updated
Dec 21, 2017
Integration of the mCRL2 toolset into Spacemacs with Syntax highlighting.
-
Updated
Apr 22, 2019 - Emacs Lisp
LTL to Control Synthesis (using formal methods concepts) Framework for a Basic Highway Driving Scenario
-
Updated
Aug 1, 2019 - Python
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."
When building the IP sniffer test, I forgot to run
Verify_Messagebefore checkingStructural_Valid_Message. While this was not a correctness issue (the context of cause was invalid), it took me some time to realize that. I wonder if we should add a predicate to those convenience operations that work on a whole message that states/requires that a verification has been attempted on a context. Th