From 52735b97c63816e06a75fea22b6cedd55ee2dbc3 Mon Sep 17 00:00:00 2001 From: Landon Taylor Date: Fri, 22 Aug 2025 13:00:04 -0600 Subject: [PATCH] Close #20 --- new-tool.md | 1 + tools/runtime/_index.md | 10 ++++++++++ tools/runtime/contractlarva.md | 16 ++++++++++++++++ tools/runtime/copilot.md | 18 ++++++++++++++++++ tools/runtime/detecter.md | 18 ++++++++++++++++++ tools/runtime/easyrte.md | 16 ++++++++++++++++ tools/runtime/hlola.md | 15 +++++++++++++++ tools/runtime/ivoryrtverification.md | 19 +++++++++++++++++++ tools/runtime/javamop.md | 19 +++++++++++++++++++ tools/runtime/mesa.md | 16 ++++++++++++++++ tools/runtime/paranoidscientist.md | 16 ++++++++++++++++ tools/runtime/qea.md | 19 +++++++++++++++++++ tools/runtime/r2u2.md | 19 +++++++++++++++++++ tools/runtime/rosmonitoring.md | 16 ++++++++++++++++ tools/runtime/rosrv.md | 19 +++++++++++++++++++ tools/runtime/rvhyper.md | 21 +++++++++++++++++++++ 16 files changed, 258 insertions(+) create mode 100644 tools/runtime/_index.md create mode 100644 tools/runtime/contractlarva.md create mode 100644 tools/runtime/copilot.md create mode 100644 tools/runtime/detecter.md create mode 100644 tools/runtime/easyrte.md create mode 100644 tools/runtime/hlola.md create mode 100644 tools/runtime/ivoryrtverification.md create mode 100644 tools/runtime/javamop.md create mode 100644 tools/runtime/mesa.md create mode 100644 tools/runtime/paranoidscientist.md create mode 100644 tools/runtime/qea.md create mode 100644 tools/runtime/r2u2.md create mode 100644 tools/runtime/rosmonitoring.md create mode 100644 tools/runtime/rosrv.md create mode 100644 tools/runtime/rvhyper.md diff --git a/new-tool.md b/new-tool.md index ec5c36b..7ede67a 100644 --- a/new-tool.md +++ b/new-tool.md @@ -239,6 +239,7 @@ function getCheckedApplications() { + document.getElementById('licenses').addEventListener('change', function() { document.getElementById('licenses-hidden').value = this.value; diff --git a/tools/runtime/_index.md b/tools/runtime/_index.md new file mode 100644 index 0000000..7643970 --- /dev/null +++ b/tools/runtime/_index.md @@ -0,0 +1,10 @@ ++++ +title = "Runtime Verifiers" +layout = "section" ++++ + +This page lists all of the Runtime Verifiers on this site in alphabetical order. +Click a tool name in the first column to view tool details. +Click a colorful item in the second column to view all the tools for which that term applies. +Item colors mean nothing and are intended to make it easy to skim the page. +Colors are generated by hashing each term's name and converting it to RGB color values. \ No newline at end of file diff --git a/tools/runtime/contractlarva.md b/tools/runtime/contractlarva.md new file mode 100644 index 0000000..929ae85 --- /dev/null +++ b/tools/runtime/contractlarva.md @@ -0,0 +1,16 @@ ++++ +title = 'contractLarva' +subtitle = 'Runtime Verifier' +links = [ { title = "Source Code", url = "https://github.com/gordonpace/contractLarva", icon = 'fa-solid fa-code' }, +] +applications = ["Runtime Verifier"] +developers = [] +licenses = ["Apache-2.0"] +inputs = [] +interfaces = ["CLI"] +maintenance = ["Actively Maintained"] +draft = false +date = 2025-08-22 ++++ + +contractLarva is a runtime verification tool for Solidity contracts. For more details about the tool check out the user manual in the docs folder. \ No newline at end of file diff --git a/tools/runtime/copilot.md b/tools/runtime/copilot.md new file mode 100644 index 0000000..9c32f17 --- /dev/null +++ b/tools/runtime/copilot.md @@ -0,0 +1,18 @@ ++++ +title = 'Copilot' +subtitle = 'Runtime Verifier' +links = [ + { title = "Homepage", url = "https://copilot-language.github.io/", icon = 'fa-solid fa-home' }, + { title = "Source Code", url = "https://github.com/Copilot-Language/copilot", icon = 'fa-solid fa-code' }, +] +applications = ["Runtime Verifier"] +developers = [] +licenses = [] +inputs = [] +interfaces = ["CLI"] +maintenance = ["Actively Maintained"] +draft = false +date = 2025-08-22 ++++ + +Copilot is a runtime verification framework for hard real-time systems. \ No newline at end of file diff --git a/tools/runtime/detecter.md b/tools/runtime/detecter.md new file mode 100644 index 0000000..f6401b8 --- /dev/null +++ b/tools/runtime/detecter.md @@ -0,0 +1,18 @@ ++++ +title = 'detectEr' +subtitle = 'Runtime Verifier' +links = [ + { title = "Homepage", url = "https://duncanatt.github.io/detecter/", icon = 'fa-solid fa-home' }, + { title = "Source Code", url = "https://github.com/duncanatt/detecter", icon = 'fa-solid fa-code' }, +] +applications = ["Runtime Verifier"] +developers = [] +licenses = ["GPL-3.0"] +inputs = [] +interfaces = ["CLI"] +maintenance = ["Actively Maintained"] +draft = false +date = 2025-08-22 ++++ + +A runtime verification tool for monitoring asynchronous component systems. \ No newline at end of file diff --git a/tools/runtime/easyrte.md b/tools/runtime/easyrte.md new file mode 100644 index 0000000..fcd6e78 --- /dev/null +++ b/tools/runtime/easyrte.md @@ -0,0 +1,16 @@ ++++ +title = 'easy-rte' +subtitle = 'Runtime Verifier' +links = [ { title = "Source Code", url = "https://github.com/PRETgroup/easy-rte", icon = 'fa-solid fa-code' }, +] +applications = ["Runtime Verifier"] +developers = [] +licenses = ["MIT"] +inputs = [] +interfaces = ["CLI"] +maintenance = ["Actively Maintained"] +draft = false +date = 2025-08-22 ++++ + + Toolchain to automatically generate and verify HW or SW runtime enforcers from text-based framework \ No newline at end of file diff --git a/tools/runtime/hlola.md b/tools/runtime/hlola.md new file mode 100644 index 0000000..efa77f4 --- /dev/null +++ b/tools/runtime/hlola.md @@ -0,0 +1,15 @@ ++++ +title = 'hlola' +subtitle = 'Runtime Verifier' +links = [ { title = "Source Code", url = "https://github.com/imdea-software/hlola", icon = 'fa-solid fa-code' }, +] +applications = ["Runtime Verifier"] +developers = [] +licenses = ["MIT"] +inputs = [] +interfaces = ["CLI"] +maintenance = ["Actively Maintained"] +draft = false +date = 2025-08-22 ++++ + diff --git a/tools/runtime/ivoryrtverification.md b/tools/runtime/ivoryrtverification.md new file mode 100644 index 0000000..72cedac --- /dev/null +++ b/tools/runtime/ivoryrtverification.md @@ -0,0 +1,19 @@ ++++ +title = 'ivory-rtverification' +subtitle = 'Runtime Verifier' +links = [ { title = "Source Code", url = "https://github.com/GaloisInc/ivory-rtverification", icon = 'fa-solid fa-code' }, +] +applications = ["Runtime Verifier"] +developers = [] +licenses = ["BSD-3-Clause"] +inputs = [] +interfaces = ["CLI"] +maintenance = ["Not Maintained"] +updated_year = 2014 +draft = false +date = 2025-08-22 ++++ + +{{}} + +Runtime verification for C code via a GCC plugin architecture. \ No newline at end of file diff --git a/tools/runtime/javamop.md b/tools/runtime/javamop.md new file mode 100644 index 0000000..3c0b476 --- /dev/null +++ b/tools/runtime/javamop.md @@ -0,0 +1,19 @@ ++++ +title = 'JavaMOP' +subtitle = 'Runtime Verifier' +links = [ { title = "Source Code", url = "https://github.com/runtimeverification/javamop", icon = 'fa-solid fa-code' }, +] +applications = ["Runtime Verifier"] +developers = [] +licenses = [] +inputs = [] +interfaces = ["CLI"] +maintenance = ["Not Maintained"] +updated_year = 2019 +draft = false +date = 2025-08-22 ++++ + +{{}} + + Runtime verification system for Java, using AspectJ for instrumentation. \ No newline at end of file diff --git a/tools/runtime/mesa.md b/tools/runtime/mesa.md new file mode 100644 index 0000000..f30e611 --- /dev/null +++ b/tools/runtime/mesa.md @@ -0,0 +1,16 @@ ++++ +title = 'MESA' +subtitle = 'Runtime Verifier' +links = [ { title = "Source Code", url = "https://github.com/NASA-SW-VnV/mesa", icon = 'fa-solid fa-code' }, +] +applications = ["Runtime Verifier"] +developers = [] +licenses = ["NASA Open Source"] +inputs = [] +interfaces = ["CLI"] +maintenance = ["Actively Maintained"] +draft = false +date = 2025-08-22 ++++ + +MESA is a framework that provides runtime verification of distributed systems in a nonintrusive manner. \ No newline at end of file diff --git a/tools/runtime/paranoidscientist.md b/tools/runtime/paranoidscientist.md new file mode 100644 index 0000000..f8f1c64 --- /dev/null +++ b/tools/runtime/paranoidscientist.md @@ -0,0 +1,16 @@ ++++ +title = 'Paranoid Scientist' +subtitle = 'Runtime Verifier' +links = [ { title = "Source Code", url = "https://github.com/mwshinn/paranoidscientist", icon = 'fa-solid fa-code' }, +] +applications = ["Runtime Verifier"] +developers = [] +licenses = ["MIT"] +inputs = [] +interfaces = ["Library"] +maintenance = ["Actively Maintained"] +draft = false +date = 2025-08-22 ++++ + + Runtime software verification and automated testing for scientific software in Python \ No newline at end of file diff --git a/tools/runtime/qea.md b/tools/runtime/qea.md new file mode 100644 index 0000000..f908e89 --- /dev/null +++ b/tools/runtime/qea.md @@ -0,0 +1,19 @@ ++++ +title = 'QEA' +subtitle = 'Runtime Verifier' +links = [ { title = "Source Code", url = "https://github.com/selig/qea", icon = 'fa-solid fa-code' }, +] +applications = ["Runtime Verifier","Specification Language"] +developers = [] +licenses = ["MIT"] +inputs = [] +interfaces = ["CLI"] +maintenance = ["Not Maintained"] +updated_year = 2019 +draft = false +date = 2025-08-22 ++++ + +{{}} + +Quantified Event Automata (QEA) is a specification formalism developed for runtime monitoring. This project is a reimplementation and extension of QEA monitoring techniques (explored in Giles Reger’s PhD work) by Master’s student Helena Cuenca. \ No newline at end of file diff --git a/tools/runtime/r2u2.md b/tools/runtime/r2u2.md new file mode 100644 index 0000000..03f9faf --- /dev/null +++ b/tools/runtime/r2u2.md @@ -0,0 +1,19 @@ ++++ +title = 'R2U2' +subtitle = 'Runtime Verifier' +links = [ + { title = "Homepage", url = "https://r2u2.temporallogic.org/", icon = 'fa-solid fa-home' }, + { title = "Source Code", url = "https://github.com/R2U2/r2u2", icon = 'fa-solid fa-code' }, + { title = "Playground", url = "https://r2u2.temporallogic.org/playground/", icon = 'fa-solid fa-gamepad' } +] +applications = ["Runtime Verifier"] +developers = ["Iowa State University"] +licenses = ["MIT", "Apache-2.0"] +inputs = [] +interfaces = ["Web","CLI"] +maintenance = ["Actively Maintained"] +draft = false +date = 2025-08-22 ++++ + + The Realizable Responsive Unobtrusive Unit is an online runtime monitor framework. \ No newline at end of file diff --git a/tools/runtime/rosmonitoring.md b/tools/runtime/rosmonitoring.md new file mode 100644 index 0000000..29874a9 --- /dev/null +++ b/tools/runtime/rosmonitoring.md @@ -0,0 +1,16 @@ ++++ +title = 'ROSMonitoring' +subtitle = 'Runtime Verifier' +links = [ { title = "Source Code", url = "https://github.com/autonomy-and-verification-uol/ROSMonitoring", icon = 'fa-solid fa-code' }, +] +applications = ["Runtime Verifier"] +developers = [] +licenses = ["MIT"] +inputs = [] +interfaces = ["CLI"] +maintenance = ["Actively Maintained"] +draft = false +date = 2025-08-22 ++++ + +ROSMonitoring is a framework developed for verifying at runtime the messages exchanged in a ROS system. \ No newline at end of file diff --git a/tools/runtime/rosrv.md b/tools/runtime/rosrv.md new file mode 100644 index 0000000..6fa51f6 --- /dev/null +++ b/tools/runtime/rosrv.md @@ -0,0 +1,19 @@ ++++ +title = 'ROSRV' +subtitle = 'Runtime Verifier' +links = [ { title = "Source Code", url = "https://github.com/cansuerdogan/ROSRV", icon = 'fa-solid fa-code' }, +] +applications = ["Runtime Verifier"] +developers = [] +licenses = [] +inputs = [] +interfaces = ["CLI"] +maintenance = ["Not Maintained"] +updated_year = 2014 +draft = false +date = 2025-08-22 ++++ + +{{}} + +ROSRV is a runtime verification framework for the Robot Operating System (ROS). \ No newline at end of file diff --git a/tools/runtime/rvhyper.md b/tools/runtime/rvhyper.md new file mode 100644 index 0000000..802a179 --- /dev/null +++ b/tools/runtime/rvhyper.md @@ -0,0 +1,21 @@ ++++ +title = 'RVHyper' +subtitle = 'Runtime Verifier' +links = [ + { title = "Homepage", url = "https://www.react.uni-saarland.de/tools/rvhyper/", icon = 'fa-solid fa-home' }, + { title = "Source Code", url = "https://github.com/reactive-systems/rvhyper", icon = 'fa-solid fa-code' }, +] +applications = ["Runtime Verifier"] +developers = [] +licenses = ["GPL-3.0"] +inputs = [] +interfaces = ["CLI"] +maintenance = ["Not Maintained"] +updated_year = 2019 +draft = false +date = 2025-08-22 ++++ + +{{}} + + RVHyper - A Runtime Verification Tool for Temporal Hyperproperties. \ No newline at end of file