Select a tag to browse associated projects and drill deeper into the tag cloud.
Coloane
Analyzed about 19 hours ago
Coloane is a free Eclipse based editor dedicated to systems modeling using different formalisms like Petri Nets. With Coloane you can design your models and connect them to the FrameKit platform. This platform provides you a huge set of tools you can use to verify properties on your models (i.e. "Does my model have a deadlock?")
Licenses:
eclipse
RUDDER
Analyzed about 17 hours ago
Continuous Auditing & Configuration
Licenses:
apache_2, CC-BY-SA-2_0, gpl3
Why3
Analyzed about 17 hours ago
Why3 is the next generation of the Why software verification platform. Why3 clearly separates the purely logical specification apart from generation of verification conditions for programs. It features a rich library of proof task transformations that can be chained to produce a suitable input for a
VUnit HDL
Analyzed about 1 hour ago
VUnit is an open source unit testing framework for VHDL/SystemVerilog released under the terms of Mozilla Public License, v. 2.0. It features the functionality needed to realize continuous and automated testing of your HDL code. VUnit doesn't replace but rather complements traditional testing
Licenses:
mozilla_p...
Gappa
G
No analysis available
The Gappa tool helps developers to verify arithmetic properties on their numerical programs (either floating-point or fixed-point computations). It can also generate formal proofs of the properties for extra confidence. It has been successfully used with several projects, e.g. for writing some
Mostly written in language not available
Licenses:
gpl
OSVVM
O
Analyzed about 21 hours ago
Open Source VHDL Verification Methodology (OSVVM) is an intelligent testbench methodology that allows mixing of “Intelligent Coverage” (coverage driven randomization) with directed, algorithmic, file based, and constrained random test approaches. The methodology can be adopted in part or in whole as
Licenses:
apache_2
DIVINE
Analyzed about 2 months ago
DIVINE is a modern explicit-state model checker. Building on high-performance algorithms and data structures, it offers unparalleled versatility, scaling from a typical developer’s laptop, up to a high-end compute cluster. What more, it can verify a wide range of languages, including C and C++.
Licenses:
bsd_2clau...
seL4
Analyzed about 3 hours ago
The seL4 microkernel
The world's first operating-system kernel with an end-to-end proof of implementation correctness and security enforcement.
Licenses:
GNU_Gener...
PolyBoRi
P
No analysis available
PolyBoRi is implemented as a C++ library for Polynomials over Boolean Rings, which provides high-level data types for Boolean polynomials. A python-interface yields extensible algorithms for computing Groebner bases over Boolean Rings.
Mostly written in language not available
Licenses:
No declared licenses
Muen Separation Kernel
Analyzed about 6 hours ago
Muen is a Separation Kernel implemented in the SPARK programming language. It runs on the Intel x86/64 architecture employing hardware-assisted virtualization (VT-x and VT-d) as the fundamental separation mechanism. The goal of the Muen project is the development of a trustworthy open-source