dgpv/miniscript-alloy-spec

Formal specification for Miniscript in Alloy

Language: Alloy - Size: 163 KB - Last synced at: 2 months ago - Pushed at: over 4 years ago - Stars: 8 - Forks: 5

sal-sin/kafka-alloy

A formal specification of Apache Kafka's architecture and temporal behavior, developed using Alloy 6

Language: Alloy - Size: 276 KB - Last synced at: about 1 year ago - Pushed at: about 1 year ago - Stars: 0 - Forks: 0

Componolit/SXML

Formally verified, bounded-stack XML library

Language: Ada - Size: 69.3 MB - Last synced at: 9 months ago - Pushed at: almost 5 years ago - Stars: 21 - Forks: 2

ncatanoc/cyber_resilience

Program synthesis for cyber-resilience. Generation of certified code for architectural tactics, for which we use Event-B and EventB2Java. We show how testing can be used to animate and check the generated code.

Size: 901 KB - Last synced at: 9 months ago - Pushed at: over 3 years ago - Stars: 1 - Forks: 0

imandra-ai/cme-mdp

Imandra Modelling Language CME MDP Model

Language: Jupyter Notebook - Size: 2.17 MB - Last synced at: about 1 month ago - Pushed at: about 5 years ago - Stars: 13 - Forks: 3

RuFerdZ/Snakes-and-Ladders

🪜 B Specification Program for snakes and ladders game as a part of 6SENG001W Reasoning About Programs Coursework 02 (2021/22) 🐍

Size: 717 KB - Last synced at: 2 months ago - Pushed at: over 2 years ago - Stars: 4 - Forks: 0

RuFerdZ/Spaceships-Asteroids

🚀 B Specification Program for Spaceships & Asteroids game as a part of 6SENG001W Reasoning About Programs Coursework 01 (2021/22) 🪨

Size: 575 KB - Last synced at: 2 months ago - Pushed at: over 2 years ago - Stars: 4 - Forks: 1

GabryV00/iPSTL_AnomalyDetector

Temporal Logic for Learning and Detection of Anomalous behaviours

Size: 3.68 MB - Last synced at: 2 months ago - Pushed at: over 1 year ago - Stars: 0 - Forks: 0

SuperSonicHub1/gorr-language

A toy specification language designed for my high school's senior capstone project.

Language: HTML - Size: 14.9 MB - Last synced at: about 2 months ago - Pushed at: over 1 year ago - Stars: 1 - Forks: 0

eliyaoo32/DepSynt

Tools for dependent variables in Linear Temporal Logic (LTL), including: Finding Dependent variables, Synthesis exploiting dependency.

Language: C - Size: 158 MB - Last synced at: over 1 year ago - Pushed at: over 1 year ago - Stars: 0 - Forks: 0

guodong/nanobdd

First-ever high-performance thread-safe BDD library

Language: C++ - Size: 99.6 KB - Last synced at: over 1 year ago - Pushed at: over 1 year ago - Stars: 7 - Forks: 4

Vanille-N/tree-borrows

Overview of the Tree Borrows rules for detecting violations of the aliasing discipline in Rust

Language: TeX - Size: 3.44 MB - Last synced at: about 1 year ago - Pushed at: about 1 year ago - Stars: 18 - Forks: 0

Amrita-TIFAC-Cyber-Blockchain/Formal-Methods-Blockchain

Formal Methods for Blockchain & Smart Contracts

Size: 6.45 MB - Last synced at: about 1 year ago - Pushed at: over 2 years ago - Stars: 2 - Forks: 2

zekissel/automata-sim

Logical simulator for deterministic, non-deterministic, and generalized finite automata and turing machines.

Language: Python - Size: 705 KB - Last synced at: over 1 year ago - Pushed at: over 1 year ago - Stars: 0 - Forks: 0

TAPAAL/TAPAAL

TAPAAL is a tool for modelling, simulation and verification of Timed-Arc Petri nets

Size: 6.84 KB - Last synced at: over 1 year ago - Pushed at: over 1 year ago - Stars: 5 - Forks: 0

Flunzmas/gym-autokey

An OpenAI gym environment for automated rule-based deductive program verification in KeY.

Language: Java - Size: 41.1 MB - Last synced at: over 1 year ago - Pushed at: over 4 years ago - Stars: 6 - Forks: 0

ningit/vaed

Verifying Algorithms and Data Structures in Dafny (TFG)

Language: C# - Size: 90.8 KB - Last synced at: over 1 year ago - Pushed at: over 7 years ago - Stars: 1 - Forks: 2

tobiasstraub/treffpunkt-fomeda 📦

:bulb: TREFFpunkt FoMeDa

Language: Java - Size: 2.45 MB - Last synced at: over 1 year ago - Pushed at: over 8 years ago - Stars: 0 - Forks: 0

timewinder-dev/timewinder

Temporal Logic of Actions in Rust via Starlark

Language: Starlark - Size: 397 KB - Last synced at: over 1 year ago - Pushed at: over 1 year ago - Stars: 0 - Forks: 0

jgaltidor/sudoku_solver_service_inez

A sudoku solver web service utilizing SMT/ILP solver Inez

Language: OCaml - Size: 80.1 KB - Last synced at: over 1 year ago - Pushed at: over 2 years ago - Stars: 0 - Forks: 0

Skar0/pareto-rational-verification

Implementation of verification algorithms for the Pareto-Rational Verification problem (PRV problem).

Language: Python - Size: 96.6 MB - Last synced at: over 1 year ago - Pushed at: about 3 years ago - Stars: 1 - Forks: 1

mkhaled87/SENSE

SENSE (Symbolic controlEr Networked SystEms) is a C++ toolbox for constructing symbolic abstractions as well as synthesizing symbolic controllers for networked control systems. The tool has MATLAB and OMNet++ interfaces for closed loop simulation.

Language: C++ - Size: 95.4 MB - Last synced at: over 1 year ago - Pushed at: over 4 years ago - Stars: 3 - Forks: 0

CLEARSY/CSSP-Programming-Handbook

The CLEARSY Safety Platform Programming Handbook

Language: TeX - Size: 19.6 MB - Last synced at: 3 months ago - Pushed at: about 5 years ago - Stars: 4 - Forks: 0

VTrelat/Hopcroft_verif

Formal verification in Isabelle(HOL) of Hopcroft's algorithm for minimizing DFAs including runtime analysis

Language: Isabelle - Size: 16.2 MB - Last synced at: over 1 year ago - Pushed at: over 1 year ago - Stars: 1 - Forks: 0

AtticusKuhn/parallel-algorithms

Proving the correctness and performance of certain parallel algorithms

Language: TeX - Size: 111 KB - Last synced at: about 1 month ago - Pushed at: over 1 year ago - Stars: 4 - Forks: 0

maurofama99/formal-methods-project

Formal Digital Twin of a Lego Mindstorms production plant

Language: Python - Size: 3.44 MB - Last synced at: over 1 year ago - Pushed at: over 1 year ago - Stars: 0 - Forks: 0

dfava/readingclub

Reading club on programming languages and formal methods

Language: Jupyter Notebook - Size: 3.4 MB - Last synced at: over 1 year ago - Pushed at: about 6 years ago - Stars: 7 - Forks: 1

timewinder-dev/timewinder-prototype

Temporal Logic of Actions Modeling for Python

Language: Python - Size: 176 KB - Last synced at: over 1 year ago - Pushed at: about 4 years ago - Stars: 11 - Forks: 1

input-output-hk/utxo-wallet-specification 📦

Formal specification for a UTxO wallet

Language: TeX - Size: 537 KB - Last synced at: 2 months ago - Pushed at: over 6 years ago - Stars: 1 - Forks: 0

spidermoy/OnTheFly_ModelChecking

Efficient On-the-Fly Model Checking for LTL and CTL★.

Language: Haskell - Size: 21.5 KB - Last synced at: 8 months ago - Pushed at: over 5 years ago - Stars: 5 - Forks: 0

matt-kukla/mvl

Multivalued logic systems in OCaml.

Language: OCaml - Size: 38.1 KB - Last synced at: over 1 year ago - Pushed at: over 1 year ago - Stars: 2 - Forks: 0

facumolina/ga-optodeclspecs

A Genetic Algorithm to translate Operational to Declarative Specifications

Language: Alloy - Size: 21.6 MB - Last synced at: over 1 year ago - Pushed at: over 6 years ago - Stars: 1 - Forks: 0

Sophietje/Verification-Tool-Overview

Information about verification tools. Browse the data at https://slebok.github.io/proverb/

Language: Python - Size: 1.06 MB - Last synced at: over 1 year ago - Pushed at: almost 2 years ago - Stars: 13 - Forks: 2

davidlazar/llvm-semantics

Formal semantics of LLVM IR in K

Language: LLVM - Size: 14.4 MB - Last synced at: over 1 year ago - Pushed at: almost 10 years ago - Stars: 41 - Forks: 9

behnaaz/constreofy

Proof of concept

Language: Java - Size: 6.76 MB - Last synced at: over 1 year ago - Pushed at: almost 4 years ago - Stars: 1 - Forks: 0

ArthurSudbrackIbarra/Trab1-Metodos-Formais

Trabalho 1 de Métodos Formais.

Language: Dafny - Size: 83 KB - Last synced at: about 2 months ago - Pushed at: almost 2 years ago - Stars: 1 - Forks: 0

dfirsov/easycrypt-one-time-blt-signature

Verified Security of BLT Signature Scheme

Language: eC - Size: 59.6 KB - Last synced at: over 1 year ago - Pushed at: almost 3 years ago - Stars: 0 - Forks: 0

dfirsov/easycrypt-multiple-time-blt-signature

Verified Multiple-Time Signature Scheme from One-Time Signatures and Timestamping

Language: eC - Size: 35.2 KB - Last synced at: over 1 year ago - Pushed at: almost 3 years ago - Stars: 0 - Forks: 0

sillydan1/aaltitoad

Extendable verification engine and simulator for Tick Tock Automata constructs

Language: C++ - Size: 5.01 MB - Last synced at: 3 months ago - Pushed at: 3 months ago - Stars: 6 - Forks: 1

eltonvs/uno-b

A formally specified UNO game using B-Method

Language: C - Size: 34.2 KB - Last synced at: over 1 year ago - Pushed at: almost 7 years ago - Stars: 2 - Forks: 0

cister-labs/fvoca2223

Web page hosting the pedagocical material prepared in the scope of the FVOCA class of the MESCC MSc

Language: HTML - Size: 2.11 MB - Last synced at: almost 2 years ago - Pushed at: over 2 years ago - Stars: 0 - Forks: 0

joffreyhuguet/curve25519-spark2014

An attempt to verify functions from Curve25519 implementation in SPARK2014

Language: Ada - Size: 93.8 KB - Last synced at: almost 2 years ago - Pushed at: almost 6 years ago - Stars: 3 - Forks: 1

raketenstadt/raketenstadt.github.io

static site materials

Language: HTML - Size: 0 Bytes - Last synced at: almost 2 years ago - Pushed at: almost 2 years ago - Stars: 0 - Forks: 0

Davetbutler/formalising-mpc-isabelle

Formalisation of MPC in Isabelle/HOL

Language: Isabelle - Size: 55.7 KB - Last synced at: almost 2 years ago - Pushed at: almost 3 years ago - Stars: 1 - Forks: 1

epfl-lara/SystemFR

System FR: Formalized Foundations for Stainless

Language: Coq - Size: 2.23 MB - Last synced at: 10 months ago - Pushed at: over 3 years ago - Stars: 9 - Forks: 3

xsk07/NSSK-protocol-PRISM

Needham-Schroeder Symmetric-Key (NSSK) Protocol modelling and model checking using PRISM

Size: 379 KB - Last synced at: almost 2 years ago - Pushed at: almost 2 years ago - Stars: 0 - Forks: 0

KASTEL-CSSDA/SolidityAccessControlEnforcement

Modeling and formally enforcing role-based access control policies for smart contracts

Language: Java - Size: 927 KB - Last synced at: almost 2 years ago - Pushed at: almost 2 years ago - Stars: 1 - Forks: 1

mcpeixoto/CiberPhysicsComputing

Ciber Physics Computing Class 2022/23

Language: Haskell - Size: 1.82 MB - Last synced at: almost 2 years ago - Pushed at: almost 2 years ago - Stars: 0 - Forks: 0

ACassimiro/TSNsched

Automated Schedule Generation for Time-Sensitive Networks (TSN).

Language: Java - Size: 260 MB - Last synced at: almost 2 years ago - Pushed at: almost 2 years ago - Stars: 69 - Forks: 29

huanhulan/alloy-exercises

my exercises for Alloy tool

Language: Alloy - Size: 108 KB - Last synced at: 2 months ago - Pushed at: about 5 years ago - Stars: 5 - Forks: 0

input-output-hk/high-assurance-legacy 📦

Legacy code connected to the high-assurance implementation of the Ouroboros protocol family

Language: Haskell - Size: 4.53 MB - Last synced at: 2 months ago - Pushed at: over 3 years ago - Stars: 78 - Forks: 16

stefanomarrone/performingrail

This repository constitutes the modelling baseline for the WP2 of the PerformingRail EU project.

Language: D - Size: 103 MB - Last synced at: over 1 year ago - Pushed at: over 2 years ago - Stars: 2 - Forks: 0

Componolit/gneiss 📦

Framework for platform-independent SPARK components

Language: Ada - Size: 1.48 MB - Last synced at: 4 months ago - Pushed at: over 4 years ago - Stars: 22 - Forks: 2

sr-lab/skeptic-lang

A DSL for asserting password composition policy effectiveness.

Language: Idris - Size: 45.9 KB - Last synced at: 2 months ago - Pushed at: over 5 years ago - Stars: 1 - Forks: 0

courses-at-nju-by-hfwei/problem-solving-class-coq

Rock on Coq for the Problem Solving Class at Nanjing University

Language: HTML - Size: 5.83 MB - Last synced at: 11 days ago - Pushed at: over 5 years ago - Stars: 6 - Forks: 7

d-corsi/NetworkVerifier

A set of algorithms for the formal verification and analysis of Neural Networks, implemented in Python.

Language: Python - Size: 96.7 KB - Last synced at: about 2 years ago - Pushed at: about 2 years ago - Stars: 3 - Forks: 2

input-output-hk/network-equivalences

Formal proofs of equivalences of different kinds of networks

Language: Isabelle - Size: 243 KB - Last synced at: 2 months ago - Pushed at: over 1 year ago - Stars: 2 - Forks: 1

rhaidiz/wafex

Web Application Formal Exploiter.

Language: Python - Size: 5.16 MB - Last synced at: 27 days ago - Pushed at: over 7 years ago - Stars: 6 - Forks: 2

matt-kukla/ltl

Linear temporal logic.

Language: OCaml - Size: 48.8 KB - Last synced at: almost 2 years ago - Pushed at: about 2 years ago - Stars: 1 - Forks: 0

rasheedja/LPPaver

An automated prover targeting problems that involve nonlinear real arithmetic.

Language: JavaScript - Size: 1.62 MB - Last synced at: 1 day ago - Pushed at: over 1 year ago - Stars: 5 - Forks: 0

suhr/advent-of-tla

AoC goals in TLA+

Language: TLA - Size: 9.77 KB - Last synced at: about 1 year ago - Pushed at: over 3 years ago - Stars: 6 - Forks: 1

skius/imp

Big-step, small-step and axiomatic semantics for the IMP language (unofficial)

Language: Rust - Size: 146 KB - Last synced at: about 2 months ago - Pushed at: over 3 years ago - Stars: 3 - Forks: 0

songlarknet/lark

The Songlark Toolchain for high-assurance software

Language: Scala - Size: 591 KB - Last synced at: about 2 years ago - Pushed at: about 2 years ago - Stars: 2 - Forks: 0

felixlinker/ifc-rv-thesis

My master thesis on information flow control on a minimal version of the RISC-V architecture with a model checker

Language: TeX - Size: 2.11 MB - Last synced at: about 2 years ago - Pushed at: over 4 years ago - Stars: 3 - Forks: 0

mbrcknl/puzzle-parity-permutations

Schrödinger's hats: a puzzle about parities and permutations

Language: Isabelle - Size: 12.3 MB - Last synced at: about 1 month ago - Pushed at: about 8 years ago - Stars: 2 - Forks: 0

nrfulton/scuba-release

Formal verification of a SCUBA ascent protocol.

Size: 14.6 KB - Last synced at: about 2 years ago - Pushed at: about 5 years ago - Stars: 1 - Forks: 1

sgomber/traffic-controller-NuSMV

Project done for my B.Tech course on Formal Methods for System Verification

Size: 354 KB - Last synced at: about 2 years ago - Pushed at: over 3 years ago - Stars: 5 - Forks: 0

WilfredTA/symbolic-stack-machines

Library for building symbolically executable stack-based virtual machines

Language: Rust - Size: 125 KB - Last synced at: about 2 years ago - Pushed at: over 2 years ago - Stars: 68 - Forks: 8

marcofavorito/pythogic 📦

A Python package for deal with logical formulas and formal systems (e.g. FOL)

Language: Python - Size: 660 KB - Last synced at: 7 months ago - Pushed at: over 6 years ago - Stars: 5 - Forks: 0

msramalho/feup-mfes 📦

Alloy4fun from 0 to reality

Language: JavaScript - Size: 9.73 MB - Last synced at: about 2 years ago - Pushed at: about 5 years ago - Stars: 2 - Forks: 0

FlorianCassayre/semester-project 📦

Semester Project at LARA (EPFL)

Language: Scala - Size: 301 KB - Last synced at: 2 days ago - Pushed at: over 4 years ago - Stars: 0 - Forks: 1

mgrabovsky/cryptoverif-py-lib 📦

Python implementations for CryptoVerif – Python library and examples. No longer maintained.

Language: Python - Size: 1.2 MB - Last synced at: about 2 years ago - Pushed at: almost 4 years ago - Stars: 1 - Forks: 0

mgrabovsky/cryptoverif 📦

Python implementations for CryptoVerif 1.23 (outdated)

Language: OCaml - Size: 6.94 MB - Last synced at: about 2 years ago - Pushed at: over 8 years ago - Stars: 2 - Forks: 2

afonsojramos/feup-mfes 📦

Formal modelling of GitHub in VDM++ - Software Engineering Formal Methods

Language: TeX - Size: 1.1 MB - Last synced at: about 11 hours ago - Pushed at: over 6 years ago - Stars: 0 - Forks: 0

michailmarkou1995/Java

ADVANCED PROGRAMMING (CN5120) + FORMAL METHODS (CN6006) + ADVANCED TOPICS IN COMPUTER SCIENCE (6008)

Language: Java - Size: 168 MB - Last synced at: about 2 years ago - Pushed at: almost 3 years ago - Stars: 4 - Forks: 1

zenprotocol/zen-wallet

Node and GUI for the Zen Protocol.

Language: C# - Size: 119 MB - Last synced at: about 2 years ago - Pushed at: over 7 years ago - Stars: 33 - Forks: 13

joshua-morris/concrete-semantics

Concrete Semantics in Isabelle/HOL

Language: Isabelle - Size: 25.4 KB - Last synced at: 2 months ago - Pushed at: over 5 years ago - Stars: 0 - Forks: 0

mr-desilva/Robot-Maze-Coursework-2022

Moving robot around a maze, developed with B language for final year Formal Methods Module

Size: 3.78 MB - Last synced at: about 1 year ago - Pushed at: over 2 years ago - Stars: 0 - Forks: 0

jeltsch/order-maintenance-correctness

Proof of correctness of the Jeltsch–Firsov order maintenance algorithm

Size: 24.4 KB - Last synced at: about 2 years ago - Pushed at: about 4 years ago - Stars: 0 - Forks: 0

maxvonhippel/AttackerSynthesis

🤖KORG: Tool, Models, and Supplementary Materials for Attacker Synthesis

Language: Python - Size: 1.65 MB - Last synced at: about 2 years ago - Pushed at: almost 3 years ago - Stars: 12 - Forks: 1

robkorn/plutus-experimental-smart-contracts

Experimental Smart Contracts In Plutus.

Language: Haskell - Size: 68.4 KB - Last synced at: about 2 years ago - Pushed at: about 6 years ago - Stars: 34 - Forks: 8

ssrg-vt/renee-artifacts

Language: C - Size: 46.9 MB - Last synced at: about 2 years ago - Pushed at: about 5 years ago - Stars: 4 - Forks: 1

yashanand1910/nicebook

Project repository for CMU Formal Methods (17614)

Language: Alloy - Size: 4.48 MB - Last synced at: about 2 years ago - Pushed at: over 2 years ago - Stars: 0 - Forks: 0

jdnklau/fm-ml

Collection of resources for research concerning Machine Learning and Formal Methods.

Language: TeX - Size: 54.7 KB - Last synced at: about 2 years ago - Pushed at: over 3 years ago - Stars: 14 - Forks: 3

orsinium-labs/simple-tla

Collection of useful "operators" (functions) to make TLA+ easier to learn and to use

Language: TLA - Size: 19.5 KB - Last synced at: about 2 months ago - Pushed at: over 2 years ago - Stars: 1 - Forks: 0

wtakuo/spin-env

Docker image for Spin model checker

Language: Dockerfile - Size: 1000 Bytes - Last synced at: about 2 years ago - Pushed at: over 4 years ago - Stars: 1 - Forks: 0

luizaugustogarcia/euclidean-algorithm

Demonstration, in Coq, that the Euclidean Algorithm can be efficiently used to compute the greatest common divisor of two numbers

Language: Makefile - Size: 19.5 KB - Last synced at: about 2 years ago - Pushed at: over 2 years ago - Stars: 0 - Forks: 0

arcadio/ajcontract

Design by contract extension to Java using annotations and bytecode injection

Language: Java - Size: 20.5 KB - Last synced at: about 2 years ago - Pushed at: over 2 years ago - Stars: 1 - Forks: 0

BSI-Bund/CafeOBJ-PACE

CafeOBJ proof of Key Secrecy of PACE with OTS/CafeOBJ.

Language: AMPL - Size: 58.6 KB - Last synced at: about 2 years ago - Pushed at: about 4 years ago - Stars: 5 - Forks: 0

modass/linearization

Linearization of non-linear dynamic systems for reachability analysis

Language: C++ - Size: 893 KB - Last synced at: almost 2 years ago - Pushed at: over 2 years ago - Stars: 0 - Forks: 0

greybrunix/Projeto_CP

Projeto de Calculo de Programas (cadeira de 2º ano LCC 2021/2022)

Language: Haskell - Size: 1.35 MB - Last synced at: about 2 years ago - Pushed at: almost 3 years ago - Stars: 1 - Forks: 0

Alex-Amarandei/FMSE-2022-2023

A repository containing all the laboratories developed for the Formal Methods in Software Engineering Course, part of the Master's Degree in Software Engineering.

Language: Dafny - Size: 23.4 KB - Last synced at: about 2 years ago - Pushed at: over 2 years ago - Stars: 0 - Forks: 0

owl-toolkit/owl

Language: Java - Size: 10.8 MB - Last synced at: about 2 years ago - Pushed at: over 2 years ago - Stars: 4 - Forks: 0

cristiandaniele/Human-errors-within-formal-verification

The repo presents the approaches to model human errors within protocol verification

Size: 4.88 KB - Last synced at: almost 2 years ago - Pushed at: over 2 years ago - Stars: 0 - Forks: 0

maniospas/pySynthesis

Automatic method synthesis based on similar code blocks and comments.

Language: Python - Size: 12.7 MB - Last synced at: about 2 years ago - Pushed at: over 2 years ago - Stars: 1 - Forks: 0

fluentverification/stamina-prism

STAMINA - STochastic Approximate Model-checker for INfinite-state Analysis, integrated with the PRISM model checking engine

Language: Java - Size: 23.4 MB - Last synced at: about 1 year ago - Pushed at: almost 2 years ago - Stars: 4 - Forks: 3

veracruz-project/supervisionary

The Supervisionary proof-checking kernel for higher-order logic

Language: Rust - Size: 827 KB - Last synced at: 10 months ago - Pushed at: about 3 years ago - Stars: 3 - Forks: 0

vasilisp/pb-sat

SAT-based Pseudo-Boolean Solver

Language: Common Lisp - Size: 16.6 KB - Last synced at: about 1 month ago - Pushed at: over 6 years ago - Stars: 1 - Forks: 0

medpaf/game-of-life

Pygame implementation of the infamous Conway's Game of Life

Language: Python - Size: 18.6 KB - Last synced at: about 2 years ago - Pushed at: almost 3 years ago - Stars: 2 - Forks: 0

jimmysitu/jmACL2

JM's ACL2 playground

Language: Common Lisp - Size: 90.8 KB - Last synced at: over 1 year ago - Pushed at: almost 2 years ago - Stars: 0 - Forks: 0