This commit is contained in:
2025-06-13 14:27:42 -06:00
parent e12ec64c22
commit a43350989a
236 changed files with 5144 additions and 1865 deletions

View File

@ -1,6 +1,6 @@
<!DOCTYPE html>
<html lang="en-us" dir="ltr">
<head>
<head><script src="/livereload.js?mindelay=10&amp;v=2&amp;port=1313&amp;path=livereload" data-no-instant defer></script>
<meta charset="utf-8">
<meta name="viewport" content ="width=device-width, initial-scale=1.0, maximum-scale=1.0, user-scalable=no">
@ -14,21 +14,39 @@
<meta property="og:type" content="article">
<meta property="og:title" content=".NET">
<meta property="og:description" content="">
<meta property="og:url" content="https://fmtools.fyi/interfaces/.net/">
<meta property="og:url" content="http://localhost:1313/interfaces/.net/">
<meta property="og:image" content="images/%!s(&lt;nil&gt;)">
<link rel="canonical" href="https://fmtools.fyi/interfaces/.net/">
<link rel="canonical" href="http://localhost:1313/interfaces/.net/">
<link rel="apple-touch-icon" sizes="180x180" href='https://fmtools.fyi/apple-touch-icon.png'>
<link rel="icon" type="image/png" sizes="32x32" href='https://fmtools.fyi/favicon-32x32.png'>
<link rel="icon" type="image/png" sizes='16x16' href='https://fmtools.fyi/favicon-16x16.png'>
<link rel="manifest" href='https://fmtools.fyi/site.webmanifest'>
<link rel="apple-touch-icon" sizes="180x180" href='http://localhost:1313/apple-touch-icon.png'>
<link rel="icon" type="image/png" sizes="32x32" href='http://localhost:1313/favicon-32x32.png'>
<link rel="icon" type="image/png" sizes='16x16' href='http://localhost:1313/favicon-16x16.png'>
<link rel="manifest" href='http://localhost:1313/site.webmanifest'>
<link rel="stylesheet" href="https://fmtools.fyi/css/styles.9d797fdbc9887767b3ad88393155cb84288660765fe6e18c89e2e00fd5ecfb0b9f46384188a0ae4e8b63f4c81526872e0ff61d1d5204287a0c3c8b6e8e34b6b9.css" integrity="sha512-nXl/28mId2ezrYg5MVXLhCiGYHZf5uGMieLgD9Xs&#43;wufRjhBiKCuTotj9MgVJocuD/YdHVIEKHoMPItujjS2uQ==">
<link rel="stylesheet" href="http://localhost:1313/css/styles.9d797fdbc9887767b3ad88393155cb84288660765fe6e18c89e2e00fd5ecfb0b9f46384188a0ae4e8b63f4c81526872e0ff61d1d5204287a0c3c8b6e8e34b6b9.css" integrity="sha512-nXl/28mId2ezrYg5MVXLhCiGYHZf5uGMieLgD9Xs&#43;wufRjhBiKCuTotj9MgVJocuD/YdHVIEKHoMPItujjS2uQ==">
<link href="/css/fontawesome.css" rel="stylesheet" />
<link href="/css/brands.css" rel="stylesheet" />
<link href="/css/solid.css" rel="stylesheet" />
<link rel="apple-touch-icon" sizes="57x57" href="/apple-icon-57x57.png">
<link rel="apple-touch-icon" sizes="60x60" href="/apple-icon-60x60.png">
<link rel="apple-touch-icon" sizes="72x72" href="/apple-icon-72x72.png">
<link rel="apple-touch-icon" sizes="76x76" href="/apple-icon-76x76.png">
<link rel="apple-touch-icon" sizes="114x114" href="/apple-icon-114x114.png">
<link rel="apple-touch-icon" sizes="120x120" href="/apple-icon-120x120.png">
<link rel="apple-touch-icon" sizes="144x144" href="/apple-icon-144x144.png">
<link rel="apple-touch-icon" sizes="152x152" href="/apple-icon-152x152.png">
<link rel="apple-touch-icon" sizes="180x180" href="/apple-icon-180x180.png">
<link rel="icon" type="image/png" sizes="192x192" href="/android-icon-192x192.png">
<link rel="icon" type="image/png" sizes="32x32" href="/favicon-32x32.png">
<link rel="icon" type="image/png" sizes="96x96" href="/favicon-96x96.png">
<link rel="icon" type="image/png" sizes="16x16" href="/favicon-16x16.png">
<link rel="manifest" href="/manifest.json">
<meta name="msapplication-TileColor" content="#ffffff">
<meta name="msapplication-TileImage" content="/ms-icon-144x144.png">
<meta name="theme-color" content="#ffffff">

View File

@ -2,17 +2,17 @@
<rss version="2.0" xmlns:atom="http://www.w3.org/2005/Atom">
<channel>
<title>.NET on Formal Methods Tools</title>
<link>https://fmtools.fyi/interfaces/.net/</link>
<link>http://localhost:1313/interfaces/.net/</link>
<description>Recent content in .NET on Formal Methods Tools</description>
<generator>Hugo</generator>
<language>en-us</language>
<lastBuildDate>Sat, 07 Jun 2025 00:00:00 +0000</lastBuildDate>
<atom:link href="https://fmtools.fyi/interfaces/.net/index.xml" rel="self" type="application/rss+xml" />
<atom:link href="http://localhost:1313/interfaces/.net/index.xml" rel="self" type="application/rss+xml" />
<item>
<title>Z3</title>
<link>https://fmtools.fyi/tools/sat-smt/z3/</link>
<link>http://localhost:1313/tools/sat-smt/z3/</link>
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
<guid>https://fmtools.fyi/tools/sat-smt/z3/</guid>
<guid>http://localhost:1313/tools/sat-smt/z3/</guid>
<description>&lt;p&gt;Z3 is a general-purpose theorem prover widely used for SAT &amp;amp; SMT solving.&lt;/p&gt;&#xA;&lt;h2 id=&#34;apis-and-bindings&#34;&gt;APIs and Bindings&lt;/h2&gt;&#xA;&lt;p&gt;This tool is available through the following interfaces:&lt;/p&gt;&#xA;&lt;ul&gt;&#xA;&lt;li&gt;&lt;strong&gt;C API:&lt;/strong&gt; &lt;a href=&#34;https://z3prover.github.io/api/html/group__capi.html&#34; target=&#34;_blank&#34; &gt;Z3 C API Reference&lt;/a&gt;&lt;/li&gt;&#xA;&lt;li&gt;&lt;strong&gt;C++ API:&lt;/strong&gt; &lt;a href=&#34;https://z3prover.github.io/api/html/namespacez3.html&#34; target=&#34;_blank&#34; &gt;Z3 C++ Namespace Reference&lt;/a&gt;&lt;/li&gt;&#xA;&lt;li&gt;&lt;strong&gt;.NET API:&lt;/strong&gt; &lt;a href=&#34;https://z3prover.github.io/api/html/namespace_microsoft_1_1_z3.html&#34; target=&#34;_blank&#34; &gt;Z3 .NET Namespace Reference&lt;/a&gt;&lt;/li&gt;&#xA;&lt;li&gt;&lt;strong&gt;Java API:&lt;/strong&gt; &lt;a href=&#34;https://z3prover.github.io/api/html/namespacecom_1_1microsoft_1_1z3.html&#34; target=&#34;_blank&#34; &gt;Z3 Java API Reference&lt;/a&gt;&lt;/li&gt;&#xA;&lt;li&gt;&lt;strong&gt;Python bindings:&lt;/strong&gt; &lt;a href=&#34;https://pypi.org/project/z3-solver/&#34; target=&#34;_blank&#34; &gt;z3-solver PyPI package&lt;/a&gt; (&lt;a href=&#34;https://z3prover.github.io/api/html/z3.html&#34; target=&#34;_blank&#34; &gt;Documentation&lt;/a&gt;)&lt;/li&gt;&#xA;&lt;li&gt;&lt;strong&gt;Rust bindings:&lt;/strong&gt; &lt;a href=&#34;https://crates.io/crates/z3&#34; target=&#34;_blank&#34; &gt;z3 crate on crates.io&lt;/a&gt;&lt;/li&gt;&#xA;&lt;/ul&gt;</description>
</item>
</channel>

View File

@ -1,6 +1,6 @@
<!DOCTYPE html>
<html lang="en-us" dir="ltr">
<head>
<head><script src="/livereload.js?mindelay=10&amp;v=2&amp;port=1313&amp;path=livereload" data-no-instant defer></script>
<meta charset="utf-8">
<meta name="viewport" content ="width=device-width, initial-scale=1.0, maximum-scale=1.0, user-scalable=no">
@ -14,21 +14,39 @@
<meta property="og:type" content="article">
<meta property="og:title" content="C&#43;&#43;">
<meta property="og:description" content="">
<meta property="og:url" content="https://fmtools.fyi/interfaces/c&#43;&#43;/">
<meta property="og:url" content="http://localhost:1313/interfaces/c&#43;&#43;/">
<meta property="og:image" content="images/%!s(&lt;nil&gt;)">
<link rel="canonical" href="https://fmtools.fyi/interfaces/c&#43;&#43;/">
<link rel="canonical" href="http://localhost:1313/interfaces/c&#43;&#43;/">
<link rel="apple-touch-icon" sizes="180x180" href='https://fmtools.fyi/apple-touch-icon.png'>
<link rel="icon" type="image/png" sizes="32x32" href='https://fmtools.fyi/favicon-32x32.png'>
<link rel="icon" type="image/png" sizes='16x16' href='https://fmtools.fyi/favicon-16x16.png'>
<link rel="manifest" href='https://fmtools.fyi/site.webmanifest'>
<link rel="apple-touch-icon" sizes="180x180" href='http://localhost:1313/apple-touch-icon.png'>
<link rel="icon" type="image/png" sizes="32x32" href='http://localhost:1313/favicon-32x32.png'>
<link rel="icon" type="image/png" sizes='16x16' href='http://localhost:1313/favicon-16x16.png'>
<link rel="manifest" href='http://localhost:1313/site.webmanifest'>
<link rel="stylesheet" href="https://fmtools.fyi/css/styles.9d797fdbc9887767b3ad88393155cb84288660765fe6e18c89e2e00fd5ecfb0b9f46384188a0ae4e8b63f4c81526872e0ff61d1d5204287a0c3c8b6e8e34b6b9.css" integrity="sha512-nXl/28mId2ezrYg5MVXLhCiGYHZf5uGMieLgD9Xs&#43;wufRjhBiKCuTotj9MgVJocuD/YdHVIEKHoMPItujjS2uQ==">
<link rel="stylesheet" href="http://localhost:1313/css/styles.9d797fdbc9887767b3ad88393155cb84288660765fe6e18c89e2e00fd5ecfb0b9f46384188a0ae4e8b63f4c81526872e0ff61d1d5204287a0c3c8b6e8e34b6b9.css" integrity="sha512-nXl/28mId2ezrYg5MVXLhCiGYHZf5uGMieLgD9Xs&#43;wufRjhBiKCuTotj9MgVJocuD/YdHVIEKHoMPItujjS2uQ==">
<link href="/css/fontawesome.css" rel="stylesheet" />
<link href="/css/brands.css" rel="stylesheet" />
<link href="/css/solid.css" rel="stylesheet" />
<link rel="apple-touch-icon" sizes="57x57" href="/apple-icon-57x57.png">
<link rel="apple-touch-icon" sizes="60x60" href="/apple-icon-60x60.png">
<link rel="apple-touch-icon" sizes="72x72" href="/apple-icon-72x72.png">
<link rel="apple-touch-icon" sizes="76x76" href="/apple-icon-76x76.png">
<link rel="apple-touch-icon" sizes="114x114" href="/apple-icon-114x114.png">
<link rel="apple-touch-icon" sizes="120x120" href="/apple-icon-120x120.png">
<link rel="apple-touch-icon" sizes="144x144" href="/apple-icon-144x144.png">
<link rel="apple-touch-icon" sizes="152x152" href="/apple-icon-152x152.png">
<link rel="apple-touch-icon" sizes="180x180" href="/apple-icon-180x180.png">
<link rel="icon" type="image/png" sizes="192x192" href="/android-icon-192x192.png">
<link rel="icon" type="image/png" sizes="32x32" href="/favicon-32x32.png">
<link rel="icon" type="image/png" sizes="96x96" href="/favicon-96x96.png">
<link rel="icon" type="image/png" sizes="16x16" href="/favicon-16x16.png">
<link rel="manifest" href="/manifest.json">
<meta name="msapplication-TileColor" content="#ffffff">
<meta name="msapplication-TileImage" content="/ms-icon-144x144.png">
<meta name="theme-color" content="#ffffff">

View File

@ -2,38 +2,38 @@
<rss version="2.0" xmlns:atom="http://www.w3.org/2005/Atom">
<channel>
<title>C&#43;&#43; on Formal Methods Tools</title>
<link>https://fmtools.fyi/interfaces/c&#43;&#43;/</link>
<link>http://localhost:1313/interfaces/c&#43;&#43;/</link>
<description>Recent content in C&#43;&#43; on Formal Methods Tools</description>
<generator>Hugo</generator>
<language>en-us</language>
<lastBuildDate>Sat, 07 Jun 2025 00:00:00 +0000</lastBuildDate>
<atom:link href="https://fmtools.fyi/interfaces/c++/index.xml" rel="self" type="application/rss+xml" />
<atom:link href="http://localhost:1313/interfaces/c++/index.xml" rel="self" type="application/rss+xml" />
<item>
<title>CryptoMiniSat</title>
<link>https://fmtools.fyi/tools/sat-smt/cryptominisat/</link>
<link>http://localhost:1313/tools/sat-smt/cryptominisat/</link>
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
<guid>https://fmtools.fyi/tools/sat-smt/cryptominisat/</guid>
<guid>http://localhost:1313/tools/sat-smt/cryptominisat/</guid>
<description>&lt;p&gt;CryptoMiniSat is a SAT solver.&lt;/p&gt;&#xA;&lt;h2 id=&#34;apis-and-bindings&#34;&gt;APIs and Bindings&lt;/h2&gt;&#xA;&lt;p&gt;This tool is available through the following interfaces:&lt;/p&gt;&#xA;&lt;ul&gt;&#xA;&lt;li&gt;&lt;strong&gt;C++ Namespace:&lt;/strong&gt; Documentation on &lt;a href=&#34;https://www.msoos.org/cryptominisat5/&#34; target=&#34;_blank&#34; &gt;homepage&lt;/a&gt;&lt;/li&gt;&#xA;&lt;li&gt;&lt;strong&gt;Python package:&lt;/strong&gt; &lt;a href=&#34;https://pypi.org/project/pycryptosat/&#34; target=&#34;_blank&#34; &gt;PyPI package&lt;/a&gt;&lt;/li&gt;&#xA;&lt;/ul&gt;</description>
</item>
<item>
<title>SMT-RAT</title>
<link>https://fmtools.fyi/tools/sat-smt/smt-rat/</link>
<link>http://localhost:1313/tools/sat-smt/smt-rat/</link>
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
<guid>https://fmtools.fyi/tools/sat-smt/smt-rat/</guid>
<guid>http://localhost:1313/tools/sat-smt/smt-rat/</guid>
<description>&lt;p&gt;SMT-RAT is an SMT Real Algebra Toolbox.&lt;/p&gt;&#xA;&lt;h2 id=&#34;apis-and-bindings&#34;&gt;APIs and Bindings&lt;/h2&gt;&#xA;&lt;p&gt;This tool is available through the following interfaces:&lt;/p&gt;&#xA;&lt;ul&gt;&#xA;&lt;li&gt;&lt;strong&gt;C++ API:&lt;/strong&gt; &lt;a href=&#34;https://ths-rwth.github.io/smtrat/dc/dad/md__builds_ths_smt_smtrat_doc_markdown_07_using_smtrat.html#autotoc_md25&#34; target=&#34;_blank&#34; &gt;C++ API Reference&lt;/a&gt;&lt;/li&gt;&#xA;&lt;/ul&gt;</description>
</item>
<item>
<title>Storm</title>
<link>https://fmtools.fyi/tools/prob/storm/</link>
<link>http://localhost:1313/tools/prob/storm/</link>
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
<guid>https://fmtools.fyi/tools/prob/storm/</guid>
<guid>http://localhost:1313/tools/prob/storm/</guid>
<description>&lt;p&gt;Storm is a tool for the analysis of systems involving random or probabilistic phenomena.&lt;/p&gt;</description>
</item>
<item>
<title>Z3</title>
<link>https://fmtools.fyi/tools/sat-smt/z3/</link>
<link>http://localhost:1313/tools/sat-smt/z3/</link>
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
<guid>https://fmtools.fyi/tools/sat-smt/z3/</guid>
<guid>http://localhost:1313/tools/sat-smt/z3/</guid>
<description>&lt;p&gt;Z3 is a general-purpose theorem prover widely used for SAT &amp;amp; SMT solving.&lt;/p&gt;&#xA;&lt;h2 id=&#34;apis-and-bindings&#34;&gt;APIs and Bindings&lt;/h2&gt;&#xA;&lt;p&gt;This tool is available through the following interfaces:&lt;/p&gt;&#xA;&lt;ul&gt;&#xA;&lt;li&gt;&lt;strong&gt;C API:&lt;/strong&gt; &lt;a href=&#34;https://z3prover.github.io/api/html/group__capi.html&#34; target=&#34;_blank&#34; &gt;Z3 C API Reference&lt;/a&gt;&lt;/li&gt;&#xA;&lt;li&gt;&lt;strong&gt;C++ API:&lt;/strong&gt; &lt;a href=&#34;https://z3prover.github.io/api/html/namespacez3.html&#34; target=&#34;_blank&#34; &gt;Z3 C++ Namespace Reference&lt;/a&gt;&lt;/li&gt;&#xA;&lt;li&gt;&lt;strong&gt;.NET API:&lt;/strong&gt; &lt;a href=&#34;https://z3prover.github.io/api/html/namespace_microsoft_1_1_z3.html&#34; target=&#34;_blank&#34; &gt;Z3 .NET Namespace Reference&lt;/a&gt;&lt;/li&gt;&#xA;&lt;li&gt;&lt;strong&gt;Java API:&lt;/strong&gt; &lt;a href=&#34;https://z3prover.github.io/api/html/namespacecom_1_1microsoft_1_1z3.html&#34; target=&#34;_blank&#34; &gt;Z3 Java API Reference&lt;/a&gt;&lt;/li&gt;&#xA;&lt;li&gt;&lt;strong&gt;Python bindings:&lt;/strong&gt; &lt;a href=&#34;https://pypi.org/project/z3-solver/&#34; target=&#34;_blank&#34; &gt;z3-solver PyPI package&lt;/a&gt; (&lt;a href=&#34;https://z3prover.github.io/api/html/z3.html&#34; target=&#34;_blank&#34; &gt;Documentation&lt;/a&gt;)&lt;/li&gt;&#xA;&lt;li&gt;&lt;strong&gt;Rust bindings:&lt;/strong&gt; &lt;a href=&#34;https://crates.io/crates/z3&#34; target=&#34;_blank&#34; &gt;z3 crate on crates.io&lt;/a&gt;&lt;/li&gt;&#xA;&lt;/ul&gt;</description>
</item>
</channel>

View File

@ -1,6 +1,6 @@
<!DOCTYPE html>
<html lang="en-us" dir="ltr">
<head>
<head><script src="/livereload.js?mindelay=10&amp;v=2&amp;port=1313&amp;path=livereload" data-no-instant defer></script>
<meta charset="utf-8">
<meta name="viewport" content ="width=device-width, initial-scale=1.0, maximum-scale=1.0, user-scalable=no">
@ -14,21 +14,39 @@
<meta property="og:type" content="article">
<meta property="og:title" content="C">
<meta property="og:description" content="">
<meta property="og:url" content="https://fmtools.fyi/interfaces/c/">
<meta property="og:url" content="http://localhost:1313/interfaces/c/">
<meta property="og:image" content="images/%!s(&lt;nil&gt;)">
<link rel="canonical" href="https://fmtools.fyi/interfaces/c/">
<link rel="canonical" href="http://localhost:1313/interfaces/c/">
<link rel="apple-touch-icon" sizes="180x180" href='https://fmtools.fyi/apple-touch-icon.png'>
<link rel="icon" type="image/png" sizes="32x32" href='https://fmtools.fyi/favicon-32x32.png'>
<link rel="icon" type="image/png" sizes='16x16' href='https://fmtools.fyi/favicon-16x16.png'>
<link rel="manifest" href='https://fmtools.fyi/site.webmanifest'>
<link rel="apple-touch-icon" sizes="180x180" href='http://localhost:1313/apple-touch-icon.png'>
<link rel="icon" type="image/png" sizes="32x32" href='http://localhost:1313/favicon-32x32.png'>
<link rel="icon" type="image/png" sizes='16x16' href='http://localhost:1313/favicon-16x16.png'>
<link rel="manifest" href='http://localhost:1313/site.webmanifest'>
<link rel="stylesheet" href="https://fmtools.fyi/css/styles.9d797fdbc9887767b3ad88393155cb84288660765fe6e18c89e2e00fd5ecfb0b9f46384188a0ae4e8b63f4c81526872e0ff61d1d5204287a0c3c8b6e8e34b6b9.css" integrity="sha512-nXl/28mId2ezrYg5MVXLhCiGYHZf5uGMieLgD9Xs&#43;wufRjhBiKCuTotj9MgVJocuD/YdHVIEKHoMPItujjS2uQ==">
<link rel="stylesheet" href="http://localhost:1313/css/styles.9d797fdbc9887767b3ad88393155cb84288660765fe6e18c89e2e00fd5ecfb0b9f46384188a0ae4e8b63f4c81526872e0ff61d1d5204287a0c3c8b6e8e34b6b9.css" integrity="sha512-nXl/28mId2ezrYg5MVXLhCiGYHZf5uGMieLgD9Xs&#43;wufRjhBiKCuTotj9MgVJocuD/YdHVIEKHoMPItujjS2uQ==">
<link href="/css/fontawesome.css" rel="stylesheet" />
<link href="/css/brands.css" rel="stylesheet" />
<link href="/css/solid.css" rel="stylesheet" />
<link rel="apple-touch-icon" sizes="57x57" href="/apple-icon-57x57.png">
<link rel="apple-touch-icon" sizes="60x60" href="/apple-icon-60x60.png">
<link rel="apple-touch-icon" sizes="72x72" href="/apple-icon-72x72.png">
<link rel="apple-touch-icon" sizes="76x76" href="/apple-icon-76x76.png">
<link rel="apple-touch-icon" sizes="114x114" href="/apple-icon-114x114.png">
<link rel="apple-touch-icon" sizes="120x120" href="/apple-icon-120x120.png">
<link rel="apple-touch-icon" sizes="144x144" href="/apple-icon-144x144.png">
<link rel="apple-touch-icon" sizes="152x152" href="/apple-icon-152x152.png">
<link rel="apple-touch-icon" sizes="180x180" href="/apple-icon-180x180.png">
<link rel="icon" type="image/png" sizes="192x192" href="/android-icon-192x192.png">
<link rel="icon" type="image/png" sizes="32x32" href="/favicon-32x32.png">
<link rel="icon" type="image/png" sizes="96x96" href="/favicon-96x96.png">
<link rel="icon" type="image/png" sizes="16x16" href="/favicon-16x16.png">
<link rel="manifest" href="/manifest.json">
<meta name="msapplication-TileColor" content="#ffffff">
<meta name="msapplication-TileImage" content="/ms-icon-144x144.png">
<meta name="theme-color" content="#ffffff">

View File

@ -2,24 +2,24 @@
<rss version="2.0" xmlns:atom="http://www.w3.org/2005/Atom">
<channel>
<title>C on Formal Methods Tools</title>
<link>https://fmtools.fyi/interfaces/c/</link>
<link>http://localhost:1313/interfaces/c/</link>
<description>Recent content in C on Formal Methods Tools</description>
<generator>Hugo</generator>
<language>en-us</language>
<lastBuildDate>Sat, 07 Jun 2025 00:00:00 +0000</lastBuildDate>
<atom:link href="https://fmtools.fyi/interfaces/c/index.xml" rel="self" type="application/rss+xml" />
<atom:link href="http://localhost:1313/interfaces/c/index.xml" rel="self" type="application/rss+xml" />
<item>
<title>STP</title>
<link>https://fmtools.fyi/tools/sat-smt/stp/</link>
<link>http://localhost:1313/tools/sat-smt/stp/</link>
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
<guid>https://fmtools.fyi/tools/sat-smt/stp/</guid>
<guid>http://localhost:1313/tools/sat-smt/stp/</guid>
<description>&lt;p&gt;STP is a constraint solver for quantifier-free bitvectors.&lt;/p&gt;&#xA;&lt;h2 id=&#34;apis-and-bindings&#34;&gt;APIs and Bindings&lt;/h2&gt;&#xA;&lt;p&gt;This tool is available through the following interfaces:&lt;/p&gt;&#xA;&lt;ul&gt;&#xA;&lt;li&gt;&lt;strong&gt;C API:&lt;/strong&gt; &lt;a href=&#34;https://stp.readthedocs.io/en/latest/#c-library-usage&#34; target=&#34;_blank&#34; &gt;stp C API Reference&lt;/a&gt;&lt;/li&gt;&#xA;&lt;li&gt;&lt;strong&gt;Python bindings:&lt;/strong&gt; &lt;a href=&#34;https://stp.readthedocs.io/en/latest/#python-usage&#34; target=&#34;_blank&#34; &gt;stp PyPI package&lt;/a&gt;&lt;/li&gt;&#xA;&lt;/ul&gt;</description>
</item>
<item>
<title>Z3</title>
<link>https://fmtools.fyi/tools/sat-smt/z3/</link>
<link>http://localhost:1313/tools/sat-smt/z3/</link>
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
<guid>https://fmtools.fyi/tools/sat-smt/z3/</guid>
<guid>http://localhost:1313/tools/sat-smt/z3/</guid>
<description>&lt;p&gt;Z3 is a general-purpose theorem prover widely used for SAT &amp;amp; SMT solving.&lt;/p&gt;&#xA;&lt;h2 id=&#34;apis-and-bindings&#34;&gt;APIs and Bindings&lt;/h2&gt;&#xA;&lt;p&gt;This tool is available through the following interfaces:&lt;/p&gt;&#xA;&lt;ul&gt;&#xA;&lt;li&gt;&lt;strong&gt;C API:&lt;/strong&gt; &lt;a href=&#34;https://z3prover.github.io/api/html/group__capi.html&#34; target=&#34;_blank&#34; &gt;Z3 C API Reference&lt;/a&gt;&lt;/li&gt;&#xA;&lt;li&gt;&lt;strong&gt;C++ API:&lt;/strong&gt; &lt;a href=&#34;https://z3prover.github.io/api/html/namespacez3.html&#34; target=&#34;_blank&#34; &gt;Z3 C++ Namespace Reference&lt;/a&gt;&lt;/li&gt;&#xA;&lt;li&gt;&lt;strong&gt;.NET API:&lt;/strong&gt; &lt;a href=&#34;https://z3prover.github.io/api/html/namespace_microsoft_1_1_z3.html&#34; target=&#34;_blank&#34; &gt;Z3 .NET Namespace Reference&lt;/a&gt;&lt;/li&gt;&#xA;&lt;li&gt;&lt;strong&gt;Java API:&lt;/strong&gt; &lt;a href=&#34;https://z3prover.github.io/api/html/namespacecom_1_1microsoft_1_1z3.html&#34; target=&#34;_blank&#34; &gt;Z3 Java API Reference&lt;/a&gt;&lt;/li&gt;&#xA;&lt;li&gt;&lt;strong&gt;Python bindings:&lt;/strong&gt; &lt;a href=&#34;https://pypi.org/project/z3-solver/&#34; target=&#34;_blank&#34; &gt;z3-solver PyPI package&lt;/a&gt; (&lt;a href=&#34;https://z3prover.github.io/api/html/z3.html&#34; target=&#34;_blank&#34; &gt;Documentation&lt;/a&gt;)&lt;/li&gt;&#xA;&lt;li&gt;&lt;strong&gt;Rust bindings:&lt;/strong&gt; &lt;a href=&#34;https://crates.io/crates/z3&#34; target=&#34;_blank&#34; &gt;z3 crate on crates.io&lt;/a&gt;&lt;/li&gt;&#xA;&lt;/ul&gt;</description>
</item>
</channel>

View File

@ -1,6 +1,6 @@
<!DOCTYPE html>
<html lang="en-us" dir="ltr">
<head>
<head><script src="/livereload.js?mindelay=10&amp;v=2&amp;port=1313&amp;path=livereload" data-no-instant defer></script>
<meta charset="utf-8">
<meta name="viewport" content ="width=device-width, initial-scale=1.0, maximum-scale=1.0, user-scalable=no">
@ -14,21 +14,39 @@
<meta property="og:type" content="article">
<meta property="og:title" content="CLI">
<meta property="og:description" content="">
<meta property="og:url" content="https://fmtools.fyi/interfaces/cli/">
<meta property="og:url" content="http://localhost:1313/interfaces/cli/">
<meta property="og:image" content="images/%!s(&lt;nil&gt;)">
<link rel="canonical" href="https://fmtools.fyi/interfaces/cli/">
<link rel="canonical" href="http://localhost:1313/interfaces/cli/">
<link rel="apple-touch-icon" sizes="180x180" href='https://fmtools.fyi/apple-touch-icon.png'>
<link rel="icon" type="image/png" sizes="32x32" href='https://fmtools.fyi/favicon-32x32.png'>
<link rel="icon" type="image/png" sizes='16x16' href='https://fmtools.fyi/favicon-16x16.png'>
<link rel="manifest" href='https://fmtools.fyi/site.webmanifest'>
<link rel="apple-touch-icon" sizes="180x180" href='http://localhost:1313/apple-touch-icon.png'>
<link rel="icon" type="image/png" sizes="32x32" href='http://localhost:1313/favicon-32x32.png'>
<link rel="icon" type="image/png" sizes='16x16' href='http://localhost:1313/favicon-16x16.png'>
<link rel="manifest" href='http://localhost:1313/site.webmanifest'>
<link rel="stylesheet" href="https://fmtools.fyi/css/styles.9d797fdbc9887767b3ad88393155cb84288660765fe6e18c89e2e00fd5ecfb0b9f46384188a0ae4e8b63f4c81526872e0ff61d1d5204287a0c3c8b6e8e34b6b9.css" integrity="sha512-nXl/28mId2ezrYg5MVXLhCiGYHZf5uGMieLgD9Xs&#43;wufRjhBiKCuTotj9MgVJocuD/YdHVIEKHoMPItujjS2uQ==">
<link rel="stylesheet" href="http://localhost:1313/css/styles.9d797fdbc9887767b3ad88393155cb84288660765fe6e18c89e2e00fd5ecfb0b9f46384188a0ae4e8b63f4c81526872e0ff61d1d5204287a0c3c8b6e8e34b6b9.css" integrity="sha512-nXl/28mId2ezrYg5MVXLhCiGYHZf5uGMieLgD9Xs&#43;wufRjhBiKCuTotj9MgVJocuD/YdHVIEKHoMPItujjS2uQ==">
<link href="/css/fontawesome.css" rel="stylesheet" />
<link href="/css/brands.css" rel="stylesheet" />
<link href="/css/solid.css" rel="stylesheet" />
<link rel="apple-touch-icon" sizes="57x57" href="/apple-icon-57x57.png">
<link rel="apple-touch-icon" sizes="60x60" href="/apple-icon-60x60.png">
<link rel="apple-touch-icon" sizes="72x72" href="/apple-icon-72x72.png">
<link rel="apple-touch-icon" sizes="76x76" href="/apple-icon-76x76.png">
<link rel="apple-touch-icon" sizes="114x114" href="/apple-icon-114x114.png">
<link rel="apple-touch-icon" sizes="120x120" href="/apple-icon-120x120.png">
<link rel="apple-touch-icon" sizes="144x144" href="/apple-icon-144x144.png">
<link rel="apple-touch-icon" sizes="152x152" href="/apple-icon-152x152.png">
<link rel="apple-touch-icon" sizes="180x180" href="/apple-icon-180x180.png">
<link rel="icon" type="image/png" sizes="192x192" href="/android-icon-192x192.png">
<link rel="icon" type="image/png" sizes="32x32" href="/favicon-32x32.png">
<link rel="icon" type="image/png" sizes="96x96" href="/favicon-96x96.png">
<link rel="icon" type="image/png" sizes="16x16" href="/favicon-16x16.png">
<link rel="manifest" href="/manifest.json">
<meta name="msapplication-TileColor" content="#ffffff">
<meta name="msapplication-TileImage" content="/ms-icon-144x144.png">
<meta name="theme-color" content="#ffffff">
@ -89,6 +107,14 @@
</thead>
<tbody>
<tr onclick="window.location='\/tools\/sat-smt\/alt-ergo\/'" style="cursor:pointer;">
<td class="tool"><a href="/tools/sat-smt/alt-ergo/">Alt-Ergo</a></td>
<td class="description">Alt-Ergo is an automatic prover of mathematical formulas used behind software verification tools …</td>
</tr>
<tr onclick="window.location='\/tools\/sat-smt\/bitwuzla\/'" style="cursor:pointer;">
<td class="tool"><a href="/tools/sat-smt/bitwuzla/">Bitwuzla</a></td>
<td class="description">Bitwuzla is a Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size …</td>

View File

@ -2,185 +2,192 @@
<rss version="2.0" xmlns:atom="http://www.w3.org/2005/Atom">
<channel>
<title>CLI on Formal Methods Tools</title>
<link>https://fmtools.fyi/interfaces/cli/</link>
<link>http://localhost:1313/interfaces/cli/</link>
<description>Recent content in CLI on Formal Methods Tools</description>
<generator>Hugo</generator>
<language>en-us</language>
<lastBuildDate>Sat, 07 Jun 2025 00:00:00 +0000</lastBuildDate>
<atom:link href="https://fmtools.fyi/interfaces/cli/index.xml" rel="self" type="application/rss+xml" />
<atom:link href="http://localhost:1313/interfaces/cli/index.xml" rel="self" type="application/rss+xml" />
<item>
<title>Alt-Ergo</title>
<link>http://localhost:1313/tools/sat-smt/alt-ergo/</link>
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
<guid>http://localhost:1313/tools/sat-smt/alt-ergo/</guid>
<description>&lt;p&gt;Alt-Ergo is an automatic prover of mathematical formulas used behind software verification tools such as Frama-C, SPARK, Why3, Atelier-B and Caveat.&lt;/p&gt;</description>
</item>
<item>
<title>Bitwuzla</title>
<link>https://fmtools.fyi/tools/sat-smt/bitwuzla/</link>
<link>http://localhost:1313/tools/sat-smt/bitwuzla/</link>
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
<guid>https://fmtools.fyi/tools/sat-smt/bitwuzla/</guid>
<guid>http://localhost:1313/tools/sat-smt/bitwuzla/</guid>
<description>&lt;p&gt;Bitwuzla is a Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, floating-point arithmetic, arrays, uninterpreted functions and their combinations.&lt;/p&gt;</description>
</item>
<item>
<title>Boolector</title>
<link>https://fmtools.fyi/tools/sat-smt/boolector/</link>
<link>http://localhost:1313/tools/sat-smt/boolector/</link>
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
<guid>https://fmtools.fyi/tools/sat-smt/boolector/</guid>
<guid>http://localhost:1313/tools/sat-smt/boolector/</guid>
<description>&lt;p&gt;&#xA;&#xA;&lt;div style=&#34;display: flex; align-items: center; gap: 8px;&#34;&gt;&#xA; &lt;span style=&#34;display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);&#34;&gt;&lt;/span&gt;&#xA; &lt;span style=&#34;display:none&#34;&gt;[&lt;/span&gt;&#xA; &#xA; &lt;span style=&#34;color: rgb(240, 85, 85); font-size: 1rem;&#34;&gt;Not Maintained Since 2024&lt;/span&gt;&#xA; &#xA; &lt;span style=&#34;display:none&#34;&gt;]&lt;/span&gt;&#xA;&lt;/div&gt;&#xA;Boolector is a Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, arrays and uninterpreted functions.&#xA;Succeeded by &lt;a href=&#34;../bitwuzla&#34; &gt;Bitwuzla&lt;/a&gt;&lt;/p&gt;</description>
</item>
<item>
<title>Colibri</title>
<link>https://fmtools.fyi/tools/sat-smt/colibri/</link>
<link>http://localhost:1313/tools/sat-smt/colibri/</link>
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
<guid>https://fmtools.fyi/tools/sat-smt/colibri/</guid>
<guid>http://localhost:1313/tools/sat-smt/colibri/</guid>
<description>&lt;p&gt;Colibri is an SMT solver.&lt;/p&gt;</description>
</item>
<item>
<title>CryptoMiniSat</title>
<link>https://fmtools.fyi/tools/sat-smt/cryptominisat/</link>
<link>http://localhost:1313/tools/sat-smt/cryptominisat/</link>
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
<guid>https://fmtools.fyi/tools/sat-smt/cryptominisat/</guid>
<guid>http://localhost:1313/tools/sat-smt/cryptominisat/</guid>
<description>&lt;p&gt;CryptoMiniSat is a SAT solver.&lt;/p&gt;&#xA;&lt;h2 id=&#34;apis-and-bindings&#34;&gt;APIs and Bindings&lt;/h2&gt;&#xA;&lt;p&gt;This tool is available through the following interfaces:&lt;/p&gt;&#xA;&lt;ul&gt;&#xA;&lt;li&gt;&lt;strong&gt;C++ Namespace:&lt;/strong&gt; Documentation on &lt;a href=&#34;https://www.msoos.org/cryptominisat5/&#34; target=&#34;_blank&#34; &gt;homepage&lt;/a&gt;&lt;/li&gt;&#xA;&lt;li&gt;&lt;strong&gt;Python package:&lt;/strong&gt; &lt;a href=&#34;https://pypi.org/project/pycryptosat/&#34; target=&#34;_blank&#34; &gt;PyPI package&lt;/a&gt;&lt;/li&gt;&#xA;&lt;/ul&gt;</description>
</item>
<item>
<title>cvc4</title>
<link>https://fmtools.fyi/tools/sat-smt/cvc4/</link>
<link>http://localhost:1313/tools/sat-smt/cvc4/</link>
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
<guid>https://fmtools.fyi/tools/sat-smt/cvc4/</guid>
<guid>http://localhost:1313/tools/sat-smt/cvc4/</guid>
<description>&lt;p&gt;&#xA;&#xA;&lt;div style=&#34;display: flex; align-items: center; gap: 8px;&#34;&gt;&#xA; &lt;span style=&#34;display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);&#34;&gt;&lt;/span&gt;&#xA; &lt;span style=&#34;display:none&#34;&gt;[&lt;/span&gt;&#xA; &#xA; &lt;span style=&#34;color: rgb(240, 85, 85); font-size: 1rem;&#34;&gt;Not Maintained Since 2021&lt;/span&gt;&#xA; &#xA; &lt;span style=&#34;display:none&#34;&gt;]&lt;/span&gt;&#xA;&lt;/div&gt;&#xA;cvc4 is an automatic theorem prover for SMT problems. It is succeeded by &lt;a href=&#34;../cvc5&#34; &gt;cvc5&lt;/a&gt;&lt;/p&gt;</description>
</item>
<item>
<title>cvc5</title>
<link>https://fmtools.fyi/tools/sat-smt/cvc5/</link>
<link>http://localhost:1313/tools/sat-smt/cvc5/</link>
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
<guid>https://fmtools.fyi/tools/sat-smt/cvc5/</guid>
<guid>http://localhost:1313/tools/sat-smt/cvc5/</guid>
<description>&lt;p&gt;cvc5 is an automatic theorem prover for SMT problems.&lt;/p&gt;</description>
</item>
<item>
<title>dReal</title>
<link>https://fmtools.fyi/tools/sat-smt/dreal/</link>
<link>http://localhost:1313/tools/sat-smt/dreal/</link>
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
<guid>https://fmtools.fyi/tools/sat-smt/dreal/</guid>
<guid>http://localhost:1313/tools/sat-smt/dreal/</guid>
<description>&lt;p&gt;&#xA;&#xA;&lt;div style=&#34;display: flex; align-items: center; gap: 8px;&#34;&gt;&#xA; &lt;span style=&#34;display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);&#34;&gt;&lt;/span&gt;&#xA; &lt;span style=&#34;display:none&#34;&gt;[&lt;/span&gt;&#xA; &#xA; &lt;span style=&#34;color: rgb(240, 85, 85); font-size: 1rem;&#34;&gt;Not Maintained Since 2023&lt;/span&gt;&#xA; &#xA; &lt;span style=&#34;display:none&#34;&gt;]&lt;/span&gt;&#xA;&lt;/div&gt;&#xA;dReal is an automated reasoning tool. It focuses on solving problems that can be encoded as first-order logic formulas over the real numbers. Its special strength is in handling problems that involve a wide range of nonlinear real functions.&lt;/p&gt;</description>
</item>
<item>
<title>Glucose</title>
<link>https://fmtools.fyi/tools/sat-smt/glucose/</link>
<link>http://localhost:1313/tools/sat-smt/glucose/</link>
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
<guid>https://fmtools.fyi/tools/sat-smt/glucose/</guid>
<guid>http://localhost:1313/tools/sat-smt/glucose/</guid>
<description>&lt;p&gt;Glucose is a SAT solver.&lt;/p&gt;</description>
</item>
<item>
<title>Lingeling</title>
<link>https://fmtools.fyi/tools/sat-smt/lingeling/</link>
<link>http://localhost:1313/tools/sat-smt/lingeling/</link>
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
<guid>https://fmtools.fyi/tools/sat-smt/lingeling/</guid>
<guid>http://localhost:1313/tools/sat-smt/lingeling/</guid>
<description>&lt;p&gt;Lingeling is a SAT solver.&lt;/p&gt;</description>
</item>
<item>
<title>MathSAT</title>
<link>https://fmtools.fyi/tools/sat-smt/mathsat/</link>
<link>http://localhost:1313/tools/sat-smt/mathsat/</link>
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
<guid>https://fmtools.fyi/tools/sat-smt/mathsat/</guid>
<guid>http://localhost:1313/tools/sat-smt/mathsat/</guid>
<description>&lt;p&gt;&lt;div style=&#34;display: flex; align-items: center; gap: 8px;&#34;&gt;&#xA; &lt;span style=&#34;display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(226, 181, 59);&#34;&gt;&lt;/span&gt;&#xA; &lt;span style=&#34;display:none&#34;&gt;[&lt;/span&gt;&#xA; &lt;span style=&#34;color: rgb(226, 181, 59); font-size: 1rem;&#34;&gt;Closed-Source Tool&lt;/span&gt;&#xA; &lt;span style=&#34;display:none&#34;&gt;]&amp;nbsp;&lt;/span&gt;&#xA;&lt;/div&gt;&#xA;MiniSat is a minimalistic, open-source SAT solver, developed to help researchers and developers alike to get started on SAT.&lt;/p&gt;</description>
</item>
<item>
<title>MiniSat</title>
<link>https://fmtools.fyi/tools/sat-smt/minisat/</link>
<link>http://localhost:1313/tools/sat-smt/minisat/</link>
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
<guid>https://fmtools.fyi/tools/sat-smt/minisat/</guid>
<guid>http://localhost:1313/tools/sat-smt/minisat/</guid>
<description>&lt;p&gt;&#xA;&#xA;&lt;div style=&#34;display: flex; align-items: center; gap: 8px;&#34;&gt;&#xA; &lt;span style=&#34;display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);&#34;&gt;&lt;/span&gt;&#xA; &lt;span style=&#34;display:none&#34;&gt;[&lt;/span&gt;&#xA; &#xA; &lt;span style=&#34;color: rgb(240, 85, 85); font-size: 1rem;&#34;&gt;Not Maintained Since 2013&lt;/span&gt;&#xA; &#xA; &lt;span style=&#34;display:none&#34;&gt;]&lt;/span&gt;&#xA;&lt;/div&gt;&#xA;MiniSat is a minimalistic, open-source SAT solver, developed to help researchers and developers alike to get started on SAT.&lt;/p&gt;</description>
</item>
<item>
<title>OpenSMT</title>
<link>https://fmtools.fyi/tools/sat-smt/opensmt/</link>
<link>http://localhost:1313/tools/sat-smt/opensmt/</link>
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
<guid>https://fmtools.fyi/tools/sat-smt/opensmt/</guid>
<description>&lt;p&gt;OpenSMT is a compact and open-source SMT-solver written in C++, with the main goal of making SMT-Solvers easy to understand and use as a computational engine for formal verification. OpenSMT is built on top of &lt;a href=&#34;https://fmtools.fyi/tools/minisat&#34; &gt;MiniSAT&lt;/a&gt;.&lt;/p&gt;</description>
<guid>http://localhost:1313/tools/sat-smt/opensmt/</guid>
<description>&lt;p&gt;OpenSMT is a compact and open-source SMT-solver written in C++, with the main goal of making SMT-Solvers easy to understand and use as a computational engine for formal verification. OpenSMT is built on top of &lt;a href=&#34;http://localhost:1313/tools/minisat&#34; &gt;MiniSAT&lt;/a&gt;.&lt;/p&gt;</description>
</item>
<item>
<title>ParaFROST</title>
<link>https://fmtools.fyi/tools/sat-smt/parafrost/</link>
<link>http://localhost:1313/tools/sat-smt/parafrost/</link>
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
<guid>https://fmtools.fyi/tools/sat-smt/parafrost/</guid>
<guid>http://localhost:1313/tools/sat-smt/parafrost/</guid>
<description>&lt;p&gt;ParaFROST is a parallel SAT solver with GPU-accelerated inprocessing capable of harnessing NVIDIA CUDA-enabled GPUs in applying modern inprocessing tecnhiques in parallel.&lt;/p&gt;&#xA;&lt;h2 id=&#34;apis-and-bindings&#34;&gt;APIs and Bindings&lt;/h2&gt;&#xA;&lt;p&gt;This tool is available through the following interfaces:&lt;/p&gt;&#xA;&lt;ul&gt;&#xA;&lt;li&gt;&lt;strong&gt;C API:&lt;/strong&gt; &lt;a href=&#34;https://z3prover.github.io/api/html/group__capi.html&#34; target=&#34;_blank&#34; &gt;Z3 C API Reference&lt;/a&gt;&lt;/li&gt;&#xA;&lt;li&gt;&lt;strong&gt;C++ API:&lt;/strong&gt; &lt;a href=&#34;https://z3prover.github.io/api/html/namespacez3.html&#34; target=&#34;_blank&#34; &gt;Z3 C++ Namespace Reference&lt;/a&gt;&lt;/li&gt;&#xA;&lt;li&gt;&lt;strong&gt;.NET API:&lt;/strong&gt; &lt;a href=&#34;https://z3prover.github.io/api/html/namespace_microsoft_1_1_z3.html&#34; target=&#34;_blank&#34; &gt;Z3 .NET Namespace Reference&lt;/a&gt;&lt;/li&gt;&#xA;&lt;li&gt;&lt;strong&gt;Java API:&lt;/strong&gt; &lt;a href=&#34;https://z3prover.github.io/api/html/namespacecom_1_1microsoft_1_1z3.html&#34; target=&#34;_blank&#34; &gt;Z3 Java API Reference&lt;/a&gt;&lt;/li&gt;&#xA;&lt;li&gt;&lt;strong&gt;Python bindings:&lt;/strong&gt; &lt;a href=&#34;https://pypi.org/project/z3-solver/&#34; target=&#34;_blank&#34; &gt;z3-solver PyPI package&lt;/a&gt; (&lt;a href=&#34;https://z3prover.github.io/api/html/z3.html&#34; target=&#34;_blank&#34; &gt;Documentation&lt;/a&gt;)&lt;/li&gt;&#xA;&lt;li&gt;&lt;strong&gt;Rust bindings:&lt;/strong&gt; &lt;a href=&#34;https://crates.io/crates/z3&#34; target=&#34;_blank&#34; &gt;z3 crate on crates.io&lt;/a&gt;&lt;/li&gt;&#xA;&lt;/ul&gt;</description>
</item>
<item>
<title>PRISM</title>
<link>https://fmtools.fyi/tools/prob/prism/</link>
<link>http://localhost:1313/tools/prob/prism/</link>
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
<guid>https://fmtools.fyi/tools/prob/prism/</guid>
<guid>http://localhost:1313/tools/prob/prism/</guid>
<description>&lt;p&gt;PRISM is a probabilistic model checker, a tool for formal modelling and analysis of systems that exhibit random or probabilistic behaviour.&lt;/p&gt;</description>
</item>
<item>
<title>Q3B</title>
<link>https://fmtools.fyi/tools/sat-smt/q3b/</link>
<link>http://localhost:1313/tools/sat-smt/q3b/</link>
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
<guid>https://fmtools.fyi/tools/sat-smt/q3b/</guid>
<guid>http://localhost:1313/tools/sat-smt/q3b/</guid>
<description>&lt;p&gt;&#xA;&#xA;&lt;div style=&#34;display: flex; align-items: center; gap: 8px;&#34;&gt;&#xA; &lt;span style=&#34;display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);&#34;&gt;&lt;/span&gt;&#xA; &lt;span style=&#34;display:none&#34;&gt;[&lt;/span&gt;&#xA; &#xA; &lt;span style=&#34;color: rgb(240, 85, 85); font-size: 1rem;&#34;&gt;Not Maintained Since 2023&lt;/span&gt;&#xA; &#xA; &lt;span style=&#34;display:none&#34;&gt;]&lt;/span&gt;&#xA;&lt;/div&gt;&#xA;Q3B is an SMT solver for the quantified bit-vector formulas which uses BDDs.&lt;/p&gt;</description>
</item>
<item>
<title>Riss</title>
<link>https://fmtools.fyi/tools/sat-smt/riss/</link>
<link>http://localhost:1313/tools/sat-smt/riss/</link>
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
<guid>https://fmtools.fyi/tools/sat-smt/riss/</guid>
<guid>http://localhost:1313/tools/sat-smt/riss/</guid>
<description>&lt;p&gt;&#xA;&#xA;&lt;div style=&#34;display: flex; align-items: center; gap: 8px;&#34;&gt;&#xA; &lt;span style=&#34;display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);&#34;&gt;&lt;/span&gt;&#xA; &lt;span style=&#34;display:none&#34;&gt;[&lt;/span&gt;&#xA; &#xA; &lt;span style=&#34;color: rgb(240, 85, 85); font-size: 1rem;&#34;&gt;Not Maintained Since 2017&lt;/span&gt;&#xA; &#xA; &lt;span style=&#34;display:none&#34;&gt;]&lt;/span&gt;&#xA;&lt;/div&gt;&#xA;Riss is a SAT solving tool collection.&lt;/p&gt;</description>
</item>
<item>
<title>Sally</title>
<link>https://fmtools.fyi/tools/mc/sally/</link>
<link>http://localhost:1313/tools/mc/sally/</link>
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
<guid>https://fmtools.fyi/tools/mc/sally/</guid>
<guid>http://localhost:1313/tools/mc/sally/</guid>
<description>&lt;p&gt;Sally is a model checker for infinite state systems described as transition systems.&lt;/p&gt;</description>
</item>
<item>
<title>SMT-RAT</title>
<link>https://fmtools.fyi/tools/sat-smt/smt-rat/</link>
<link>http://localhost:1313/tools/sat-smt/smt-rat/</link>
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
<guid>https://fmtools.fyi/tools/sat-smt/smt-rat/</guid>
<guid>http://localhost:1313/tools/sat-smt/smt-rat/</guid>
<description>&lt;p&gt;SMT-RAT is an SMT Real Algebra Toolbox.&lt;/p&gt;&#xA;&lt;h2 id=&#34;apis-and-bindings&#34;&gt;APIs and Bindings&lt;/h2&gt;&#xA;&lt;p&gt;This tool is available through the following interfaces:&lt;/p&gt;&#xA;&lt;ul&gt;&#xA;&lt;li&gt;&lt;strong&gt;C++ API:&lt;/strong&gt; &lt;a href=&#34;https://ths-rwth.github.io/smtrat/dc/dad/md__builds_ths_smt_smtrat_doc_markdown_07_using_smtrat.html#autotoc_md25&#34; target=&#34;_blank&#34; &gt;C++ API Reference&lt;/a&gt;&lt;/li&gt;&#xA;&lt;/ul&gt;</description>
</item>
<item>
<title>SMTInterpol</title>
<link>https://fmtools.fyi/tools/sat-smt/smtinterpol/</link>
<link>http://localhost:1313/tools/sat-smt/smtinterpol/</link>
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
<guid>https://fmtools.fyi/tools/sat-smt/smtinterpol/</guid>
<guid>http://localhost:1313/tools/sat-smt/smtinterpol/</guid>
<description>&lt;p&gt;SMTInterpol is an SMT Solver that can compute Craig interpolants for various theories.&lt;/p&gt;&#xA;&lt;h2 id=&#34;apis-and-bindings&#34;&gt;APIs and Bindings&lt;/h2&gt;&#xA;&lt;p&gt;This tool is available through the following interfaces:&lt;/p&gt;&#xA;&lt;ul&gt;&#xA;&lt;li&gt;&lt;strong&gt;Java API:&lt;/strong&gt; &lt;a href=&#34;https://ultimate.informatik.uni-freiburg.de/smtinterpol/doc/index.html&#34; target=&#34;_blank&#34; &gt;Java API Reference&lt;/a&gt;&lt;/li&gt;&#xA;&lt;/ul&gt;</description>
</item>
<item>
<title>STAMINA</title>
<link>https://fmtools.fyi/tools/prob/stamina/</link>
<link>http://localhost:1313/tools/prob/stamina/</link>
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
<guid>https://fmtools.fyi/tools/prob/stamina/</guid>
<guid>http://localhost:1313/tools/prob/stamina/</guid>
<description>&lt;p&gt;A state-space truncation tool for Markov-Chains that can analyze infinite-sized models. Intefaces with either &lt;a href=&#34;../storm&#34; &gt;Storm&lt;/a&gt; or &lt;a href=&#34;../prism&#34; &gt;PRISM&lt;/a&gt;.&lt;/p&gt;</description>
</item>
<item>
<title>Storm</title>
<link>https://fmtools.fyi/tools/prob/storm/</link>
<link>http://localhost:1313/tools/prob/storm/</link>
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
<guid>https://fmtools.fyi/tools/prob/storm/</guid>
<guid>http://localhost:1313/tools/prob/storm/</guid>
<description>&lt;p&gt;Storm is a tool for the analysis of systems involving random or probabilistic phenomena.&lt;/p&gt;</description>
</item>
<item>
<title>STP</title>
<link>https://fmtools.fyi/tools/sat-smt/stp/</link>
<link>http://localhost:1313/tools/sat-smt/stp/</link>
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
<guid>https://fmtools.fyi/tools/sat-smt/stp/</guid>
<guid>http://localhost:1313/tools/sat-smt/stp/</guid>
<description>&lt;p&gt;STP is a constraint solver for quantifier-free bitvectors.&lt;/p&gt;&#xA;&lt;h2 id=&#34;apis-and-bindings&#34;&gt;APIs and Bindings&lt;/h2&gt;&#xA;&lt;p&gt;This tool is available through the following interfaces:&lt;/p&gt;&#xA;&lt;ul&gt;&#xA;&lt;li&gt;&lt;strong&gt;C API:&lt;/strong&gt; &lt;a href=&#34;https://stp.readthedocs.io/en/latest/#c-library-usage&#34; target=&#34;_blank&#34; &gt;stp C API Reference&lt;/a&gt;&lt;/li&gt;&#xA;&lt;li&gt;&lt;strong&gt;Python bindings:&lt;/strong&gt; &lt;a href=&#34;https://stp.readthedocs.io/en/latest/#python-usage&#34; target=&#34;_blank&#34; &gt;stp PyPI package&lt;/a&gt;&lt;/li&gt;&#xA;&lt;/ul&gt;</description>
</item>
<item>
<title>veriT</title>
<link>https://fmtools.fyi/tools/sat-smt/verit/</link>
<link>http://localhost:1313/tools/sat-smt/verit/</link>
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
<guid>https://fmtools.fyi/tools/sat-smt/verit/</guid>
<guid>http://localhost:1313/tools/sat-smt/verit/</guid>
<description>&lt;p&gt;veriT is an SMT solver developed by LORIA and ULiege. It supports a wide range of theories and is designed for use in formal verification, automated reasoning, and related research areas. veriT accepts input in SMT-LIB2 and DIMACS formats and provides a command-line interface for ease of integration into verification workflows. The solver is actively maintained and distributed under the BSD license, making it suitable for both academic and industrial applications.&lt;/p&gt;</description>
</item>
<item>
<title>Yices 2</title>
<link>https://fmtools.fyi/tools/sat-smt/yices/</link>
<link>http://localhost:1313/tools/sat-smt/yices/</link>
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
<guid>https://fmtools.fyi/tools/sat-smt/yices/</guid>
<guid>http://localhost:1313/tools/sat-smt/yices/</guid>
<description>&lt;p&gt;Yices is an SMT solver developed by SRI International. It is widely used for checking the satisfiability of logical formulas over various theories. It supports the SMT-LIB standard and its own input language, and provides APIs for several programming languages, making it suitable for research and industrial applications in software and hardware verification.&lt;/p&gt;&#xA;&lt;h2 id=&#34;apis-and-bindings&#34;&gt;APIs and Bindings&lt;/h2&gt;&#xA;&lt;p&gt;This tool is available through the following interfaces:&lt;/p&gt;&#xA;&lt;ul&gt;&#xA;&lt;li&gt;&lt;strong&gt;General API:&lt;/strong&gt; &lt;a href=&#34;https://yices.csl.sri.com/doc/index.html&#34; target=&#34;_blank&#34; &gt;Yices API Reference&lt;/a&gt;&lt;/li&gt;&#xA;&lt;li&gt;&lt;strong&gt;Python bindings:&lt;/strong&gt; &lt;a href=&#34;https://pypi.org/project/yices/&#34; target=&#34;_blank&#34; &gt;yices2 PyPI package&lt;/a&gt;&lt;/li&gt;&#xA;&lt;li&gt;&lt;strong&gt;Rust bindings:&lt;/strong&gt; &lt;a href=&#34;https://crates.io/crates/yices2&#34; target=&#34;_blank&#34; &gt;yices2 crate on crates.io&lt;/a&gt;&lt;/li&gt;&#xA;&lt;/ul&gt;</description>
</item>
<item>
<title>Z3</title>
<link>https://fmtools.fyi/tools/sat-smt/z3/</link>
<link>http://localhost:1313/tools/sat-smt/z3/</link>
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
<guid>https://fmtools.fyi/tools/sat-smt/z3/</guid>
<guid>http://localhost:1313/tools/sat-smt/z3/</guid>
<description>&lt;p&gt;Z3 is a general-purpose theorem prover widely used for SAT &amp;amp; SMT solving.&lt;/p&gt;&#xA;&lt;h2 id=&#34;apis-and-bindings&#34;&gt;APIs and Bindings&lt;/h2&gt;&#xA;&lt;p&gt;This tool is available through the following interfaces:&lt;/p&gt;&#xA;&lt;ul&gt;&#xA;&lt;li&gt;&lt;strong&gt;C API:&lt;/strong&gt; &lt;a href=&#34;https://z3prover.github.io/api/html/group__capi.html&#34; target=&#34;_blank&#34; &gt;Z3 C API Reference&lt;/a&gt;&lt;/li&gt;&#xA;&lt;li&gt;&lt;strong&gt;C++ API:&lt;/strong&gt; &lt;a href=&#34;https://z3prover.github.io/api/html/namespacez3.html&#34; target=&#34;_blank&#34; &gt;Z3 C++ Namespace Reference&lt;/a&gt;&lt;/li&gt;&#xA;&lt;li&gt;&lt;strong&gt;.NET API:&lt;/strong&gt; &lt;a href=&#34;https://z3prover.github.io/api/html/namespace_microsoft_1_1_z3.html&#34; target=&#34;_blank&#34; &gt;Z3 .NET Namespace Reference&lt;/a&gt;&lt;/li&gt;&#xA;&lt;li&gt;&lt;strong&gt;Java API:&lt;/strong&gt; &lt;a href=&#34;https://z3prover.github.io/api/html/namespacecom_1_1microsoft_1_1z3.html&#34; target=&#34;_blank&#34; &gt;Z3 Java API Reference&lt;/a&gt;&lt;/li&gt;&#xA;&lt;li&gt;&lt;strong&gt;Python bindings:&lt;/strong&gt; &lt;a href=&#34;https://pypi.org/project/z3-solver/&#34; target=&#34;_blank&#34; &gt;z3-solver PyPI package&lt;/a&gt; (&lt;a href=&#34;https://z3prover.github.io/api/html/z3.html&#34; target=&#34;_blank&#34; &gt;Documentation&lt;/a&gt;)&lt;/li&gt;&#xA;&lt;li&gt;&lt;strong&gt;Rust bindings:&lt;/strong&gt; &lt;a href=&#34;https://crates.io/crates/z3&#34; target=&#34;_blank&#34; &gt;z3 crate on crates.io&lt;/a&gt;&lt;/li&gt;&#xA;&lt;/ul&gt;</description>
</item>
</channel>

View File

@ -1,6 +1,6 @@
<!DOCTYPE html>
<html lang="en-us" dir="ltr">
<head>
<head><script src="/livereload.js?mindelay=10&amp;v=2&amp;port=1313&amp;path=livereload" data-no-instant defer></script>
<meta charset="utf-8">
<meta name="viewport" content ="width=device-width, initial-scale=1.0, maximum-scale=1.0, user-scalable=no">
@ -14,21 +14,39 @@
<meta property="og:type" content="article">
<meta property="og:title" content="Interfaces">
<meta property="og:description" content="">
<meta property="og:url" content="https://fmtools.fyi/interfaces/">
<meta property="og:url" content="http://localhost:1313/interfaces/">
<meta property="og:image" content="images/%!s(&lt;nil&gt;)">
<link rel="canonical" href="https://fmtools.fyi/interfaces/">
<link rel="canonical" href="http://localhost:1313/interfaces/">
<link rel="apple-touch-icon" sizes="180x180" href='https://fmtools.fyi/apple-touch-icon.png'>
<link rel="icon" type="image/png" sizes="32x32" href='https://fmtools.fyi/favicon-32x32.png'>
<link rel="icon" type="image/png" sizes='16x16' href='https://fmtools.fyi/favicon-16x16.png'>
<link rel="manifest" href='https://fmtools.fyi/site.webmanifest'>
<link rel="apple-touch-icon" sizes="180x180" href='http://localhost:1313/apple-touch-icon.png'>
<link rel="icon" type="image/png" sizes="32x32" href='http://localhost:1313/favicon-32x32.png'>
<link rel="icon" type="image/png" sizes='16x16' href='http://localhost:1313/favicon-16x16.png'>
<link rel="manifest" href='http://localhost:1313/site.webmanifest'>
<link rel="stylesheet" href="https://fmtools.fyi/css/styles.9d797fdbc9887767b3ad88393155cb84288660765fe6e18c89e2e00fd5ecfb0b9f46384188a0ae4e8b63f4c81526872e0ff61d1d5204287a0c3c8b6e8e34b6b9.css" integrity="sha512-nXl/28mId2ezrYg5MVXLhCiGYHZf5uGMieLgD9Xs&#43;wufRjhBiKCuTotj9MgVJocuD/YdHVIEKHoMPItujjS2uQ==">
<link rel="stylesheet" href="http://localhost:1313/css/styles.9d797fdbc9887767b3ad88393155cb84288660765fe6e18c89e2e00fd5ecfb0b9f46384188a0ae4e8b63f4c81526872e0ff61d1d5204287a0c3c8b6e8e34b6b9.css" integrity="sha512-nXl/28mId2ezrYg5MVXLhCiGYHZf5uGMieLgD9Xs&#43;wufRjhBiKCuTotj9MgVJocuD/YdHVIEKHoMPItujjS2uQ==">
<link href="/css/fontawesome.css" rel="stylesheet" />
<link href="/css/brands.css" rel="stylesheet" />
<link href="/css/solid.css" rel="stylesheet" />
<link rel="apple-touch-icon" sizes="57x57" href="/apple-icon-57x57.png">
<link rel="apple-touch-icon" sizes="60x60" href="/apple-icon-60x60.png">
<link rel="apple-touch-icon" sizes="72x72" href="/apple-icon-72x72.png">
<link rel="apple-touch-icon" sizes="76x76" href="/apple-icon-76x76.png">
<link rel="apple-touch-icon" sizes="114x114" href="/apple-icon-114x114.png">
<link rel="apple-touch-icon" sizes="120x120" href="/apple-icon-120x120.png">
<link rel="apple-touch-icon" sizes="144x144" href="/apple-icon-144x144.png">
<link rel="apple-touch-icon" sizes="152x152" href="/apple-icon-152x152.png">
<link rel="apple-touch-icon" sizes="180x180" href="/apple-icon-180x180.png">
<link rel="icon" type="image/png" sizes="192x192" href="/android-icon-192x192.png">
<link rel="icon" type="image/png" sizes="32x32" href="/favicon-32x32.png">
<link rel="icon" type="image/png" sizes="96x96" href="/favicon-96x96.png">
<link rel="icon" type="image/png" sizes="16x16" href="/favicon-16x16.png">
<link rel="manifest" href="/manifest.json">
<meta name="msapplication-TileColor" content="#ffffff">
<meta name="msapplication-TileImage" content="/ms-icon-144x144.png">
<meta name="theme-color" content="#ffffff">

View File

@ -2,66 +2,66 @@
<rss version="2.0" xmlns:atom="http://www.w3.org/2005/Atom">
<channel>
<title>Interfaces on Formal Methods Tools</title>
<link>https://fmtools.fyi/interfaces/</link>
<link>http://localhost:1313/interfaces/</link>
<description>Recent content in Interfaces on Formal Methods Tools</description>
<generator>Hugo</generator>
<language>en-us</language>
<lastBuildDate>Sat, 07 Jun 2025 00:00:00 +0000</lastBuildDate>
<atom:link href="https://fmtools.fyi/interfaces/index.xml" rel="self" type="application/rss+xml" />
<atom:link href="http://localhost:1313/interfaces/index.xml" rel="self" type="application/rss+xml" />
<item>
<title>.NET</title>
<link>https://fmtools.fyi/interfaces/.net/</link>
<link>http://localhost:1313/interfaces/.net/</link>
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
<guid>https://fmtools.fyi/interfaces/.net/</guid>
<guid>http://localhost:1313/interfaces/.net/</guid>
<description></description>
</item>
<item>
<title>C</title>
<link>https://fmtools.fyi/interfaces/c/</link>
<link>http://localhost:1313/interfaces/c/</link>
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
<guid>https://fmtools.fyi/interfaces/c/</guid>
<guid>http://localhost:1313/interfaces/c/</guid>
<description></description>
</item>
<item>
<title>C&#43;&#43;</title>
<link>https://fmtools.fyi/interfaces/c&#43;&#43;/</link>
<link>http://localhost:1313/interfaces/c&#43;&#43;/</link>
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
<guid>https://fmtools.fyi/interfaces/c&#43;&#43;/</guid>
<guid>http://localhost:1313/interfaces/c&#43;&#43;/</guid>
<description></description>
</item>
<item>
<title>CLI</title>
<link>https://fmtools.fyi/interfaces/cli/</link>
<link>http://localhost:1313/interfaces/cli/</link>
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
<guid>https://fmtools.fyi/interfaces/cli/</guid>
<guid>http://localhost:1313/interfaces/cli/</guid>
<description></description>
</item>
<item>
<title>Java</title>
<link>https://fmtools.fyi/interfaces/java/</link>
<link>http://localhost:1313/interfaces/java/</link>
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
<guid>https://fmtools.fyi/interfaces/java/</guid>
<guid>http://localhost:1313/interfaces/java/</guid>
<description></description>
</item>
<item>
<title>Online</title>
<link>https://fmtools.fyi/interfaces/online/</link>
<link>http://localhost:1313/interfaces/online/</link>
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
<guid>https://fmtools.fyi/interfaces/online/</guid>
<guid>http://localhost:1313/interfaces/online/</guid>
<description></description>
</item>
<item>
<title>Python</title>
<link>https://fmtools.fyi/interfaces/python/</link>
<link>http://localhost:1313/interfaces/python/</link>
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
<guid>https://fmtools.fyi/interfaces/python/</guid>
<guid>http://localhost:1313/interfaces/python/</guid>
<description></description>
</item>
<item>
<title>Rust</title>
<link>https://fmtools.fyi/interfaces/rust/</link>
<link>http://localhost:1313/interfaces/rust/</link>
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
<guid>https://fmtools.fyi/interfaces/rust/</guid>
<guid>http://localhost:1313/interfaces/rust/</guid>
<description></description>
</item>
</channel>

View File

@ -1,6 +1,6 @@
<!DOCTYPE html>
<html lang="en-us" dir="ltr">
<head>
<head><script src="/livereload.js?mindelay=10&amp;v=2&amp;port=1313&amp;path=livereload" data-no-instant defer></script>
<meta charset="utf-8">
<meta name="viewport" content ="width=device-width, initial-scale=1.0, maximum-scale=1.0, user-scalable=no">
@ -14,21 +14,39 @@
<meta property="og:type" content="article">
<meta property="og:title" content="Java">
<meta property="og:description" content="">
<meta property="og:url" content="https://fmtools.fyi/interfaces/java/">
<meta property="og:url" content="http://localhost:1313/interfaces/java/">
<meta property="og:image" content="images/%!s(&lt;nil&gt;)">
<link rel="canonical" href="https://fmtools.fyi/interfaces/java/">
<link rel="canonical" href="http://localhost:1313/interfaces/java/">
<link rel="apple-touch-icon" sizes="180x180" href='https://fmtools.fyi/apple-touch-icon.png'>
<link rel="icon" type="image/png" sizes="32x32" href='https://fmtools.fyi/favicon-32x32.png'>
<link rel="icon" type="image/png" sizes='16x16' href='https://fmtools.fyi/favicon-16x16.png'>
<link rel="manifest" href='https://fmtools.fyi/site.webmanifest'>
<link rel="apple-touch-icon" sizes="180x180" href='http://localhost:1313/apple-touch-icon.png'>
<link rel="icon" type="image/png" sizes="32x32" href='http://localhost:1313/favicon-32x32.png'>
<link rel="icon" type="image/png" sizes='16x16' href='http://localhost:1313/favicon-16x16.png'>
<link rel="manifest" href='http://localhost:1313/site.webmanifest'>
<link rel="stylesheet" href="https://fmtools.fyi/css/styles.9d797fdbc9887767b3ad88393155cb84288660765fe6e18c89e2e00fd5ecfb0b9f46384188a0ae4e8b63f4c81526872e0ff61d1d5204287a0c3c8b6e8e34b6b9.css" integrity="sha512-nXl/28mId2ezrYg5MVXLhCiGYHZf5uGMieLgD9Xs&#43;wufRjhBiKCuTotj9MgVJocuD/YdHVIEKHoMPItujjS2uQ==">
<link rel="stylesheet" href="http://localhost:1313/css/styles.9d797fdbc9887767b3ad88393155cb84288660765fe6e18c89e2e00fd5ecfb0b9f46384188a0ae4e8b63f4c81526872e0ff61d1d5204287a0c3c8b6e8e34b6b9.css" integrity="sha512-nXl/28mId2ezrYg5MVXLhCiGYHZf5uGMieLgD9Xs&#43;wufRjhBiKCuTotj9MgVJocuD/YdHVIEKHoMPItujjS2uQ==">
<link href="/css/fontawesome.css" rel="stylesheet" />
<link href="/css/brands.css" rel="stylesheet" />
<link href="/css/solid.css" rel="stylesheet" />
<link rel="apple-touch-icon" sizes="57x57" href="/apple-icon-57x57.png">
<link rel="apple-touch-icon" sizes="60x60" href="/apple-icon-60x60.png">
<link rel="apple-touch-icon" sizes="72x72" href="/apple-icon-72x72.png">
<link rel="apple-touch-icon" sizes="76x76" href="/apple-icon-76x76.png">
<link rel="apple-touch-icon" sizes="114x114" href="/apple-icon-114x114.png">
<link rel="apple-touch-icon" sizes="120x120" href="/apple-icon-120x120.png">
<link rel="apple-touch-icon" sizes="144x144" href="/apple-icon-144x144.png">
<link rel="apple-touch-icon" sizes="152x152" href="/apple-icon-152x152.png">
<link rel="apple-touch-icon" sizes="180x180" href="/apple-icon-180x180.png">
<link rel="icon" type="image/png" sizes="192x192" href="/android-icon-192x192.png">
<link rel="icon" type="image/png" sizes="32x32" href="/favicon-32x32.png">
<link rel="icon" type="image/png" sizes="96x96" href="/favicon-96x96.png">
<link rel="icon" type="image/png" sizes="16x16" href="/favicon-16x16.png">
<link rel="manifest" href="/manifest.json">
<meta name="msapplication-TileColor" content="#ffffff">
<meta name="msapplication-TileImage" content="/ms-icon-144x144.png">
<meta name="theme-color" content="#ffffff">

View File

@ -2,31 +2,31 @@
<rss version="2.0" xmlns:atom="http://www.w3.org/2005/Atom">
<channel>
<title>Java on Formal Methods Tools</title>
<link>https://fmtools.fyi/interfaces/java/</link>
<link>http://localhost:1313/interfaces/java/</link>
<description>Recent content in Java on Formal Methods Tools</description>
<generator>Hugo</generator>
<language>en-us</language>
<lastBuildDate>Sat, 07 Jun 2025 00:00:00 +0000</lastBuildDate>
<atom:link href="https://fmtools.fyi/interfaces/java/index.xml" rel="self" type="application/rss+xml" />
<atom:link href="http://localhost:1313/interfaces/java/index.xml" rel="self" type="application/rss+xml" />
<item>
<title>PRISM</title>
<link>https://fmtools.fyi/tools/prob/prism/</link>
<link>http://localhost:1313/tools/prob/prism/</link>
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
<guid>https://fmtools.fyi/tools/prob/prism/</guid>
<guid>http://localhost:1313/tools/prob/prism/</guid>
<description>&lt;p&gt;PRISM is a probabilistic model checker, a tool for formal modelling and analysis of systems that exhibit random or probabilistic behaviour.&lt;/p&gt;</description>
</item>
<item>
<title>SMTInterpol</title>
<link>https://fmtools.fyi/tools/sat-smt/smtinterpol/</link>
<link>http://localhost:1313/tools/sat-smt/smtinterpol/</link>
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
<guid>https://fmtools.fyi/tools/sat-smt/smtinterpol/</guid>
<guid>http://localhost:1313/tools/sat-smt/smtinterpol/</guid>
<description>&lt;p&gt;SMTInterpol is an SMT Solver that can compute Craig interpolants for various theories.&lt;/p&gt;&#xA;&lt;h2 id=&#34;apis-and-bindings&#34;&gt;APIs and Bindings&lt;/h2&gt;&#xA;&lt;p&gt;This tool is available through the following interfaces:&lt;/p&gt;&#xA;&lt;ul&gt;&#xA;&lt;li&gt;&lt;strong&gt;Java API:&lt;/strong&gt; &lt;a href=&#34;https://ultimate.informatik.uni-freiburg.de/smtinterpol/doc/index.html&#34; target=&#34;_blank&#34; &gt;Java API Reference&lt;/a&gt;&lt;/li&gt;&#xA;&lt;/ul&gt;</description>
</item>
<item>
<title>Z3</title>
<link>https://fmtools.fyi/tools/sat-smt/z3/</link>
<link>http://localhost:1313/tools/sat-smt/z3/</link>
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
<guid>https://fmtools.fyi/tools/sat-smt/z3/</guid>
<guid>http://localhost:1313/tools/sat-smt/z3/</guid>
<description>&lt;p&gt;Z3 is a general-purpose theorem prover widely used for SAT &amp;amp; SMT solving.&lt;/p&gt;&#xA;&lt;h2 id=&#34;apis-and-bindings&#34;&gt;APIs and Bindings&lt;/h2&gt;&#xA;&lt;p&gt;This tool is available through the following interfaces:&lt;/p&gt;&#xA;&lt;ul&gt;&#xA;&lt;li&gt;&lt;strong&gt;C API:&lt;/strong&gt; &lt;a href=&#34;https://z3prover.github.io/api/html/group__capi.html&#34; target=&#34;_blank&#34; &gt;Z3 C API Reference&lt;/a&gt;&lt;/li&gt;&#xA;&lt;li&gt;&lt;strong&gt;C++ API:&lt;/strong&gt; &lt;a href=&#34;https://z3prover.github.io/api/html/namespacez3.html&#34; target=&#34;_blank&#34; &gt;Z3 C++ Namespace Reference&lt;/a&gt;&lt;/li&gt;&#xA;&lt;li&gt;&lt;strong&gt;.NET API:&lt;/strong&gt; &lt;a href=&#34;https://z3prover.github.io/api/html/namespace_microsoft_1_1_z3.html&#34; target=&#34;_blank&#34; &gt;Z3 .NET Namespace Reference&lt;/a&gt;&lt;/li&gt;&#xA;&lt;li&gt;&lt;strong&gt;Java API:&lt;/strong&gt; &lt;a href=&#34;https://z3prover.github.io/api/html/namespacecom_1_1microsoft_1_1z3.html&#34; target=&#34;_blank&#34; &gt;Z3 Java API Reference&lt;/a&gt;&lt;/li&gt;&#xA;&lt;li&gt;&lt;strong&gt;Python bindings:&lt;/strong&gt; &lt;a href=&#34;https://pypi.org/project/z3-solver/&#34; target=&#34;_blank&#34; &gt;z3-solver PyPI package&lt;/a&gt; (&lt;a href=&#34;https://z3prover.github.io/api/html/z3.html&#34; target=&#34;_blank&#34; &gt;Documentation&lt;/a&gt;)&lt;/li&gt;&#xA;&lt;li&gt;&lt;strong&gt;Rust bindings:&lt;/strong&gt; &lt;a href=&#34;https://crates.io/crates/z3&#34; target=&#34;_blank&#34; &gt;z3 crate on crates.io&lt;/a&gt;&lt;/li&gt;&#xA;&lt;/ul&gt;</description>
</item>
</channel>

View File

@ -1,6 +1,6 @@
<!DOCTYPE html>
<html lang="en-us" dir="ltr">
<head>
<head><script src="/livereload.js?mindelay=10&amp;v=2&amp;port=1313&amp;path=livereload" data-no-instant defer></script>
<meta charset="utf-8">
<meta name="viewport" content ="width=device-width, initial-scale=1.0, maximum-scale=1.0, user-scalable=no">
@ -14,21 +14,39 @@
<meta property="og:type" content="article">
<meta property="og:title" content="Online">
<meta property="og:description" content="">
<meta property="og:url" content="https://fmtools.fyi/interfaces/online/">
<meta property="og:url" content="http://localhost:1313/interfaces/online/">
<meta property="og:image" content="images/%!s(&lt;nil&gt;)">
<link rel="canonical" href="https://fmtools.fyi/interfaces/online/">
<link rel="canonical" href="http://localhost:1313/interfaces/online/">
<link rel="apple-touch-icon" sizes="180x180" href='https://fmtools.fyi/apple-touch-icon.png'>
<link rel="icon" type="image/png" sizes="32x32" href='https://fmtools.fyi/favicon-32x32.png'>
<link rel="icon" type="image/png" sizes='16x16' href='https://fmtools.fyi/favicon-16x16.png'>
<link rel="manifest" href='https://fmtools.fyi/site.webmanifest'>
<link rel="apple-touch-icon" sizes="180x180" href='http://localhost:1313/apple-touch-icon.png'>
<link rel="icon" type="image/png" sizes="32x32" href='http://localhost:1313/favicon-32x32.png'>
<link rel="icon" type="image/png" sizes='16x16' href='http://localhost:1313/favicon-16x16.png'>
<link rel="manifest" href='http://localhost:1313/site.webmanifest'>
<link rel="stylesheet" href="https://fmtools.fyi/css/styles.9d797fdbc9887767b3ad88393155cb84288660765fe6e18c89e2e00fd5ecfb0b9f46384188a0ae4e8b63f4c81526872e0ff61d1d5204287a0c3c8b6e8e34b6b9.css" integrity="sha512-nXl/28mId2ezrYg5MVXLhCiGYHZf5uGMieLgD9Xs&#43;wufRjhBiKCuTotj9MgVJocuD/YdHVIEKHoMPItujjS2uQ==">
<link rel="stylesheet" href="http://localhost:1313/css/styles.9d797fdbc9887767b3ad88393155cb84288660765fe6e18c89e2e00fd5ecfb0b9f46384188a0ae4e8b63f4c81526872e0ff61d1d5204287a0c3c8b6e8e34b6b9.css" integrity="sha512-nXl/28mId2ezrYg5MVXLhCiGYHZf5uGMieLgD9Xs&#43;wufRjhBiKCuTotj9MgVJocuD/YdHVIEKHoMPItujjS2uQ==">
<link href="/css/fontawesome.css" rel="stylesheet" />
<link href="/css/brands.css" rel="stylesheet" />
<link href="/css/solid.css" rel="stylesheet" />
<link rel="apple-touch-icon" sizes="57x57" href="/apple-icon-57x57.png">
<link rel="apple-touch-icon" sizes="60x60" href="/apple-icon-60x60.png">
<link rel="apple-touch-icon" sizes="72x72" href="/apple-icon-72x72.png">
<link rel="apple-touch-icon" sizes="76x76" href="/apple-icon-76x76.png">
<link rel="apple-touch-icon" sizes="114x114" href="/apple-icon-114x114.png">
<link rel="apple-touch-icon" sizes="120x120" href="/apple-icon-120x120.png">
<link rel="apple-touch-icon" sizes="144x144" href="/apple-icon-144x144.png">
<link rel="apple-touch-icon" sizes="152x152" href="/apple-icon-152x152.png">
<link rel="apple-touch-icon" sizes="180x180" href="/apple-icon-180x180.png">
<link rel="icon" type="image/png" sizes="192x192" href="/android-icon-192x192.png">
<link rel="icon" type="image/png" sizes="32x32" href="/favicon-32x32.png">
<link rel="icon" type="image/png" sizes="96x96" href="/favicon-96x96.png">
<link rel="icon" type="image/png" sizes="16x16" href="/favicon-16x16.png">
<link rel="manifest" href="/manifest.json">
<meta name="msapplication-TileColor" content="#ffffff">
<meta name="msapplication-TileImage" content="/ms-icon-144x144.png">
<meta name="theme-color" content="#ffffff">
@ -89,6 +107,14 @@
</thead>
<tbody>
<tr onclick="window.location='\/tools\/sat-smt\/alt-ergo\/'" style="cursor:pointer;">
<td class="tool"><a href="/tools/sat-smt/alt-ergo/">Alt-Ergo</a></td>
<td class="description">Alt-Ergo is an automatic prover of mathematical formulas used behind software verification tools …</td>
</tr>
<tr onclick="window.location='\/tools\/sat-smt\/cvc4\/'" style="cursor:pointer;">
<td class="tool"><a href="/tools/sat-smt/cvc4/">cvc4</a></td>
<td class="description"> [ Not Maintained Since 2021 ] cvc4 is an automatic theorem prover for SMT problems. It is succeeded …</td>

View File

@ -2,38 +2,45 @@
<rss version="2.0" xmlns:atom="http://www.w3.org/2005/Atom">
<channel>
<title>Online on Formal Methods Tools</title>
<link>https://fmtools.fyi/interfaces/online/</link>
<link>http://localhost:1313/interfaces/online/</link>
<description>Recent content in Online on Formal Methods Tools</description>
<generator>Hugo</generator>
<language>en-us</language>
<lastBuildDate>Sat, 07 Jun 2025 00:00:00 +0000</lastBuildDate>
<atom:link href="https://fmtools.fyi/interfaces/online/index.xml" rel="self" type="application/rss+xml" />
<atom:link href="http://localhost:1313/interfaces/online/index.xml" rel="self" type="application/rss+xml" />
<item>
<title>Alt-Ergo</title>
<link>http://localhost:1313/tools/sat-smt/alt-ergo/</link>
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
<guid>http://localhost:1313/tools/sat-smt/alt-ergo/</guid>
<description>&lt;p&gt;Alt-Ergo is an automatic prover of mathematical formulas used behind software verification tools such as Frama-C, SPARK, Why3, Atelier-B and Caveat.&lt;/p&gt;</description>
</item>
<item>
<title>cvc4</title>
<link>https://fmtools.fyi/tools/sat-smt/cvc4/</link>
<link>http://localhost:1313/tools/sat-smt/cvc4/</link>
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
<guid>https://fmtools.fyi/tools/sat-smt/cvc4/</guid>
<guid>http://localhost:1313/tools/sat-smt/cvc4/</guid>
<description>&lt;p&gt;&#xA;&#xA;&lt;div style=&#34;display: flex; align-items: center; gap: 8px;&#34;&gt;&#xA; &lt;span style=&#34;display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);&#34;&gt;&lt;/span&gt;&#xA; &lt;span style=&#34;display:none&#34;&gt;[&lt;/span&gt;&#xA; &#xA; &lt;span style=&#34;color: rgb(240, 85, 85); font-size: 1rem;&#34;&gt;Not Maintained Since 2021&lt;/span&gt;&#xA; &#xA; &lt;span style=&#34;display:none&#34;&gt;]&lt;/span&gt;&#xA;&lt;/div&gt;&#xA;cvc4 is an automatic theorem prover for SMT problems. It is succeeded by &lt;a href=&#34;../cvc5&#34; &gt;cvc5&lt;/a&gt;&lt;/p&gt;</description>
</item>
<item>
<title>cvc5</title>
<link>https://fmtools.fyi/tools/sat-smt/cvc5/</link>
<link>http://localhost:1313/tools/sat-smt/cvc5/</link>
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
<guid>https://fmtools.fyi/tools/sat-smt/cvc5/</guid>
<guid>http://localhost:1313/tools/sat-smt/cvc5/</guid>
<description>&lt;p&gt;cvc5 is an automatic theorem prover for SMT problems.&lt;/p&gt;</description>
</item>
<item>
<title>STAMINA</title>
<link>https://fmtools.fyi/tools/prob/stamina/</link>
<link>http://localhost:1313/tools/prob/stamina/</link>
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
<guid>https://fmtools.fyi/tools/prob/stamina/</guid>
<guid>http://localhost:1313/tools/prob/stamina/</guid>
<description>&lt;p&gt;A state-space truncation tool for Markov-Chains that can analyze infinite-sized models. Intefaces with either &lt;a href=&#34;../storm&#34; &gt;Storm&lt;/a&gt; or &lt;a href=&#34;../prism&#34; &gt;PRISM&lt;/a&gt;.&lt;/p&gt;</description>
</item>
<item>
<title>Z3</title>
<link>https://fmtools.fyi/tools/sat-smt/z3/</link>
<link>http://localhost:1313/tools/sat-smt/z3/</link>
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
<guid>https://fmtools.fyi/tools/sat-smt/z3/</guid>
<guid>http://localhost:1313/tools/sat-smt/z3/</guid>
<description>&lt;p&gt;Z3 is a general-purpose theorem prover widely used for SAT &amp;amp; SMT solving.&lt;/p&gt;&#xA;&lt;h2 id=&#34;apis-and-bindings&#34;&gt;APIs and Bindings&lt;/h2&gt;&#xA;&lt;p&gt;This tool is available through the following interfaces:&lt;/p&gt;&#xA;&lt;ul&gt;&#xA;&lt;li&gt;&lt;strong&gt;C API:&lt;/strong&gt; &lt;a href=&#34;https://z3prover.github.io/api/html/group__capi.html&#34; target=&#34;_blank&#34; &gt;Z3 C API Reference&lt;/a&gt;&lt;/li&gt;&#xA;&lt;li&gt;&lt;strong&gt;C++ API:&lt;/strong&gt; &lt;a href=&#34;https://z3prover.github.io/api/html/namespacez3.html&#34; target=&#34;_blank&#34; &gt;Z3 C++ Namespace Reference&lt;/a&gt;&lt;/li&gt;&#xA;&lt;li&gt;&lt;strong&gt;.NET API:&lt;/strong&gt; &lt;a href=&#34;https://z3prover.github.io/api/html/namespace_microsoft_1_1_z3.html&#34; target=&#34;_blank&#34; &gt;Z3 .NET Namespace Reference&lt;/a&gt;&lt;/li&gt;&#xA;&lt;li&gt;&lt;strong&gt;Java API:&lt;/strong&gt; &lt;a href=&#34;https://z3prover.github.io/api/html/namespacecom_1_1microsoft_1_1z3.html&#34; target=&#34;_blank&#34; &gt;Z3 Java API Reference&lt;/a&gt;&lt;/li&gt;&#xA;&lt;li&gt;&lt;strong&gt;Python bindings:&lt;/strong&gt; &lt;a href=&#34;https://pypi.org/project/z3-solver/&#34; target=&#34;_blank&#34; &gt;z3-solver PyPI package&lt;/a&gt; (&lt;a href=&#34;https://z3prover.github.io/api/html/z3.html&#34; target=&#34;_blank&#34; &gt;Documentation&lt;/a&gt;)&lt;/li&gt;&#xA;&lt;li&gt;&lt;strong&gt;Rust bindings:&lt;/strong&gt; &lt;a href=&#34;https://crates.io/crates/z3&#34; target=&#34;_blank&#34; &gt;z3 crate on crates.io&lt;/a&gt;&lt;/li&gt;&#xA;&lt;/ul&gt;</description>
</item>
</channel>

View File

@ -1,6 +1,6 @@
<!DOCTYPE html>
<html lang="en-us" dir="ltr">
<head>
<head><script src="/livereload.js?mindelay=10&amp;v=2&amp;port=1313&amp;path=livereload" data-no-instant defer></script>
<meta charset="utf-8">
<meta name="viewport" content ="width=device-width, initial-scale=1.0, maximum-scale=1.0, user-scalable=no">
@ -14,21 +14,39 @@
<meta property="og:type" content="article">
<meta property="og:title" content="Python">
<meta property="og:description" content="">
<meta property="og:url" content="https://fmtools.fyi/interfaces/python/">
<meta property="og:url" content="http://localhost:1313/interfaces/python/">
<meta property="og:image" content="images/%!s(&lt;nil&gt;)">
<link rel="canonical" href="https://fmtools.fyi/interfaces/python/">
<link rel="canonical" href="http://localhost:1313/interfaces/python/">
<link rel="apple-touch-icon" sizes="180x180" href='https://fmtools.fyi/apple-touch-icon.png'>
<link rel="icon" type="image/png" sizes="32x32" href='https://fmtools.fyi/favicon-32x32.png'>
<link rel="icon" type="image/png" sizes='16x16' href='https://fmtools.fyi/favicon-16x16.png'>
<link rel="manifest" href='https://fmtools.fyi/site.webmanifest'>
<link rel="apple-touch-icon" sizes="180x180" href='http://localhost:1313/apple-touch-icon.png'>
<link rel="icon" type="image/png" sizes="32x32" href='http://localhost:1313/favicon-32x32.png'>
<link rel="icon" type="image/png" sizes='16x16' href='http://localhost:1313/favicon-16x16.png'>
<link rel="manifest" href='http://localhost:1313/site.webmanifest'>
<link rel="stylesheet" href="https://fmtools.fyi/css/styles.9d797fdbc9887767b3ad88393155cb84288660765fe6e18c89e2e00fd5ecfb0b9f46384188a0ae4e8b63f4c81526872e0ff61d1d5204287a0c3c8b6e8e34b6b9.css" integrity="sha512-nXl/28mId2ezrYg5MVXLhCiGYHZf5uGMieLgD9Xs&#43;wufRjhBiKCuTotj9MgVJocuD/YdHVIEKHoMPItujjS2uQ==">
<link rel="stylesheet" href="http://localhost:1313/css/styles.9d797fdbc9887767b3ad88393155cb84288660765fe6e18c89e2e00fd5ecfb0b9f46384188a0ae4e8b63f4c81526872e0ff61d1d5204287a0c3c8b6e8e34b6b9.css" integrity="sha512-nXl/28mId2ezrYg5MVXLhCiGYHZf5uGMieLgD9Xs&#43;wufRjhBiKCuTotj9MgVJocuD/YdHVIEKHoMPItujjS2uQ==">
<link href="/css/fontawesome.css" rel="stylesheet" />
<link href="/css/brands.css" rel="stylesheet" />
<link href="/css/solid.css" rel="stylesheet" />
<link rel="apple-touch-icon" sizes="57x57" href="/apple-icon-57x57.png">
<link rel="apple-touch-icon" sizes="60x60" href="/apple-icon-60x60.png">
<link rel="apple-touch-icon" sizes="72x72" href="/apple-icon-72x72.png">
<link rel="apple-touch-icon" sizes="76x76" href="/apple-icon-76x76.png">
<link rel="apple-touch-icon" sizes="114x114" href="/apple-icon-114x114.png">
<link rel="apple-touch-icon" sizes="120x120" href="/apple-icon-120x120.png">
<link rel="apple-touch-icon" sizes="144x144" href="/apple-icon-144x144.png">
<link rel="apple-touch-icon" sizes="152x152" href="/apple-icon-152x152.png">
<link rel="apple-touch-icon" sizes="180x180" href="/apple-icon-180x180.png">
<link rel="icon" type="image/png" sizes="192x192" href="/android-icon-192x192.png">
<link rel="icon" type="image/png" sizes="32x32" href="/favicon-32x32.png">
<link rel="icon" type="image/png" sizes="96x96" href="/favicon-96x96.png">
<link rel="icon" type="image/png" sizes="16x16" href="/favicon-16x16.png">
<link rel="manifest" href="/manifest.json">
<meta name="msapplication-TileColor" content="#ffffff">
<meta name="msapplication-TileImage" content="/ms-icon-144x144.png">
<meta name="theme-color" content="#ffffff">

View File

@ -2,45 +2,45 @@
<rss version="2.0" xmlns:atom="http://www.w3.org/2005/Atom">
<channel>
<title>Python on Formal Methods Tools</title>
<link>https://fmtools.fyi/interfaces/python/</link>
<link>http://localhost:1313/interfaces/python/</link>
<description>Recent content in Python on Formal Methods Tools</description>
<generator>Hugo</generator>
<language>en-us</language>
<lastBuildDate>Sat, 07 Jun 2025 00:00:00 +0000</lastBuildDate>
<atom:link href="https://fmtools.fyi/interfaces/python/index.xml" rel="self" type="application/rss+xml" />
<atom:link href="http://localhost:1313/interfaces/python/index.xml" rel="self" type="application/rss+xml" />
<item>
<title>CryptoMiniSat</title>
<link>https://fmtools.fyi/tools/sat-smt/cryptominisat/</link>
<link>http://localhost:1313/tools/sat-smt/cryptominisat/</link>
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
<guid>https://fmtools.fyi/tools/sat-smt/cryptominisat/</guid>
<guid>http://localhost:1313/tools/sat-smt/cryptominisat/</guid>
<description>&lt;p&gt;CryptoMiniSat is a SAT solver.&lt;/p&gt;&#xA;&lt;h2 id=&#34;apis-and-bindings&#34;&gt;APIs and Bindings&lt;/h2&gt;&#xA;&lt;p&gt;This tool is available through the following interfaces:&lt;/p&gt;&#xA;&lt;ul&gt;&#xA;&lt;li&gt;&lt;strong&gt;C++ Namespace:&lt;/strong&gt; Documentation on &lt;a href=&#34;https://www.msoos.org/cryptominisat5/&#34; target=&#34;_blank&#34; &gt;homepage&lt;/a&gt;&lt;/li&gt;&#xA;&lt;li&gt;&lt;strong&gt;Python package:&lt;/strong&gt; &lt;a href=&#34;https://pypi.org/project/pycryptosat/&#34; target=&#34;_blank&#34; &gt;PyPI package&lt;/a&gt;&lt;/li&gt;&#xA;&lt;/ul&gt;</description>
</item>
<item>
<title>Storm</title>
<link>https://fmtools.fyi/tools/prob/storm/</link>
<link>http://localhost:1313/tools/prob/storm/</link>
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
<guid>https://fmtools.fyi/tools/prob/storm/</guid>
<guid>http://localhost:1313/tools/prob/storm/</guid>
<description>&lt;p&gt;Storm is a tool for the analysis of systems involving random or probabilistic phenomena.&lt;/p&gt;</description>
</item>
<item>
<title>STP</title>
<link>https://fmtools.fyi/tools/sat-smt/stp/</link>
<link>http://localhost:1313/tools/sat-smt/stp/</link>
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
<guid>https://fmtools.fyi/tools/sat-smt/stp/</guid>
<guid>http://localhost:1313/tools/sat-smt/stp/</guid>
<description>&lt;p&gt;STP is a constraint solver for quantifier-free bitvectors.&lt;/p&gt;&#xA;&lt;h2 id=&#34;apis-and-bindings&#34;&gt;APIs and Bindings&lt;/h2&gt;&#xA;&lt;p&gt;This tool is available through the following interfaces:&lt;/p&gt;&#xA;&lt;ul&gt;&#xA;&lt;li&gt;&lt;strong&gt;C API:&lt;/strong&gt; &lt;a href=&#34;https://stp.readthedocs.io/en/latest/#c-library-usage&#34; target=&#34;_blank&#34; &gt;stp C API Reference&lt;/a&gt;&lt;/li&gt;&#xA;&lt;li&gt;&lt;strong&gt;Python bindings:&lt;/strong&gt; &lt;a href=&#34;https://stp.readthedocs.io/en/latest/#python-usage&#34; target=&#34;_blank&#34; &gt;stp PyPI package&lt;/a&gt;&lt;/li&gt;&#xA;&lt;/ul&gt;</description>
</item>
<item>
<title>Yices 2</title>
<link>https://fmtools.fyi/tools/sat-smt/yices/</link>
<link>http://localhost:1313/tools/sat-smt/yices/</link>
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
<guid>https://fmtools.fyi/tools/sat-smt/yices/</guid>
<guid>http://localhost:1313/tools/sat-smt/yices/</guid>
<description>&lt;p&gt;Yices is an SMT solver developed by SRI International. It is widely used for checking the satisfiability of logical formulas over various theories. It supports the SMT-LIB standard and its own input language, and provides APIs for several programming languages, making it suitable for research and industrial applications in software and hardware verification.&lt;/p&gt;&#xA;&lt;h2 id=&#34;apis-and-bindings&#34;&gt;APIs and Bindings&lt;/h2&gt;&#xA;&lt;p&gt;This tool is available through the following interfaces:&lt;/p&gt;&#xA;&lt;ul&gt;&#xA;&lt;li&gt;&lt;strong&gt;General API:&lt;/strong&gt; &lt;a href=&#34;https://yices.csl.sri.com/doc/index.html&#34; target=&#34;_blank&#34; &gt;Yices API Reference&lt;/a&gt;&lt;/li&gt;&#xA;&lt;li&gt;&lt;strong&gt;Python bindings:&lt;/strong&gt; &lt;a href=&#34;https://pypi.org/project/yices/&#34; target=&#34;_blank&#34; &gt;yices2 PyPI package&lt;/a&gt;&lt;/li&gt;&#xA;&lt;li&gt;&lt;strong&gt;Rust bindings:&lt;/strong&gt; &lt;a href=&#34;https://crates.io/crates/yices2&#34; target=&#34;_blank&#34; &gt;yices2 crate on crates.io&lt;/a&gt;&lt;/li&gt;&#xA;&lt;/ul&gt;</description>
</item>
<item>
<title>Z3</title>
<link>https://fmtools.fyi/tools/sat-smt/z3/</link>
<link>http://localhost:1313/tools/sat-smt/z3/</link>
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
<guid>https://fmtools.fyi/tools/sat-smt/z3/</guid>
<guid>http://localhost:1313/tools/sat-smt/z3/</guid>
<description>&lt;p&gt;Z3 is a general-purpose theorem prover widely used for SAT &amp;amp; SMT solving.&lt;/p&gt;&#xA;&lt;h2 id=&#34;apis-and-bindings&#34;&gt;APIs and Bindings&lt;/h2&gt;&#xA;&lt;p&gt;This tool is available through the following interfaces:&lt;/p&gt;&#xA;&lt;ul&gt;&#xA;&lt;li&gt;&lt;strong&gt;C API:&lt;/strong&gt; &lt;a href=&#34;https://z3prover.github.io/api/html/group__capi.html&#34; target=&#34;_blank&#34; &gt;Z3 C API Reference&lt;/a&gt;&lt;/li&gt;&#xA;&lt;li&gt;&lt;strong&gt;C++ API:&lt;/strong&gt; &lt;a href=&#34;https://z3prover.github.io/api/html/namespacez3.html&#34; target=&#34;_blank&#34; &gt;Z3 C++ Namespace Reference&lt;/a&gt;&lt;/li&gt;&#xA;&lt;li&gt;&lt;strong&gt;.NET API:&lt;/strong&gt; &lt;a href=&#34;https://z3prover.github.io/api/html/namespace_microsoft_1_1_z3.html&#34; target=&#34;_blank&#34; &gt;Z3 .NET Namespace Reference&lt;/a&gt;&lt;/li&gt;&#xA;&lt;li&gt;&lt;strong&gt;Java API:&lt;/strong&gt; &lt;a href=&#34;https://z3prover.github.io/api/html/namespacecom_1_1microsoft_1_1z3.html&#34; target=&#34;_blank&#34; &gt;Z3 Java API Reference&lt;/a&gt;&lt;/li&gt;&#xA;&lt;li&gt;&lt;strong&gt;Python bindings:&lt;/strong&gt; &lt;a href=&#34;https://pypi.org/project/z3-solver/&#34; target=&#34;_blank&#34; &gt;z3-solver PyPI package&lt;/a&gt; (&lt;a href=&#34;https://z3prover.github.io/api/html/z3.html&#34; target=&#34;_blank&#34; &gt;Documentation&lt;/a&gt;)&lt;/li&gt;&#xA;&lt;li&gt;&lt;strong&gt;Rust bindings:&lt;/strong&gt; &lt;a href=&#34;https://crates.io/crates/z3&#34; target=&#34;_blank&#34; &gt;z3 crate on crates.io&lt;/a&gt;&lt;/li&gt;&#xA;&lt;/ul&gt;</description>
</item>
</channel>

View File

@ -1,6 +1,6 @@
<!DOCTYPE html>
<html lang="en-us" dir="ltr">
<head>
<head><script src="/livereload.js?mindelay=10&amp;v=2&amp;port=1313&amp;path=livereload" data-no-instant defer></script>
<meta charset="utf-8">
<meta name="viewport" content ="width=device-width, initial-scale=1.0, maximum-scale=1.0, user-scalable=no">
@ -14,21 +14,39 @@
<meta property="og:type" content="article">
<meta property="og:title" content="Rust">
<meta property="og:description" content="">
<meta property="og:url" content="https://fmtools.fyi/interfaces/rust/">
<meta property="og:url" content="http://localhost:1313/interfaces/rust/">
<meta property="og:image" content="images/%!s(&lt;nil&gt;)">
<link rel="canonical" href="https://fmtools.fyi/interfaces/rust/">
<link rel="canonical" href="http://localhost:1313/interfaces/rust/">
<link rel="apple-touch-icon" sizes="180x180" href='https://fmtools.fyi/apple-touch-icon.png'>
<link rel="icon" type="image/png" sizes="32x32" href='https://fmtools.fyi/favicon-32x32.png'>
<link rel="icon" type="image/png" sizes='16x16' href='https://fmtools.fyi/favicon-16x16.png'>
<link rel="manifest" href='https://fmtools.fyi/site.webmanifest'>
<link rel="apple-touch-icon" sizes="180x180" href='http://localhost:1313/apple-touch-icon.png'>
<link rel="icon" type="image/png" sizes="32x32" href='http://localhost:1313/favicon-32x32.png'>
<link rel="icon" type="image/png" sizes='16x16' href='http://localhost:1313/favicon-16x16.png'>
<link rel="manifest" href='http://localhost:1313/site.webmanifest'>
<link rel="stylesheet" href="https://fmtools.fyi/css/styles.9d797fdbc9887767b3ad88393155cb84288660765fe6e18c89e2e00fd5ecfb0b9f46384188a0ae4e8b63f4c81526872e0ff61d1d5204287a0c3c8b6e8e34b6b9.css" integrity="sha512-nXl/28mId2ezrYg5MVXLhCiGYHZf5uGMieLgD9Xs&#43;wufRjhBiKCuTotj9MgVJocuD/YdHVIEKHoMPItujjS2uQ==">
<link rel="stylesheet" href="http://localhost:1313/css/styles.9d797fdbc9887767b3ad88393155cb84288660765fe6e18c89e2e00fd5ecfb0b9f46384188a0ae4e8b63f4c81526872e0ff61d1d5204287a0c3c8b6e8e34b6b9.css" integrity="sha512-nXl/28mId2ezrYg5MVXLhCiGYHZf5uGMieLgD9Xs&#43;wufRjhBiKCuTotj9MgVJocuD/YdHVIEKHoMPItujjS2uQ==">
<link href="/css/fontawesome.css" rel="stylesheet" />
<link href="/css/brands.css" rel="stylesheet" />
<link href="/css/solid.css" rel="stylesheet" />
<link rel="apple-touch-icon" sizes="57x57" href="/apple-icon-57x57.png">
<link rel="apple-touch-icon" sizes="60x60" href="/apple-icon-60x60.png">
<link rel="apple-touch-icon" sizes="72x72" href="/apple-icon-72x72.png">
<link rel="apple-touch-icon" sizes="76x76" href="/apple-icon-76x76.png">
<link rel="apple-touch-icon" sizes="114x114" href="/apple-icon-114x114.png">
<link rel="apple-touch-icon" sizes="120x120" href="/apple-icon-120x120.png">
<link rel="apple-touch-icon" sizes="144x144" href="/apple-icon-144x144.png">
<link rel="apple-touch-icon" sizes="152x152" href="/apple-icon-152x152.png">
<link rel="apple-touch-icon" sizes="180x180" href="/apple-icon-180x180.png">
<link rel="icon" type="image/png" sizes="192x192" href="/android-icon-192x192.png">
<link rel="icon" type="image/png" sizes="32x32" href="/favicon-32x32.png">
<link rel="icon" type="image/png" sizes="96x96" href="/favicon-96x96.png">
<link rel="icon" type="image/png" sizes="16x16" href="/favicon-16x16.png">
<link rel="manifest" href="/manifest.json">
<meta name="msapplication-TileColor" content="#ffffff">
<meta name="msapplication-TileImage" content="/ms-icon-144x144.png">
<meta name="theme-color" content="#ffffff">

View File

@ -2,24 +2,24 @@
<rss version="2.0" xmlns:atom="http://www.w3.org/2005/Atom">
<channel>
<title>Rust on Formal Methods Tools</title>
<link>https://fmtools.fyi/interfaces/rust/</link>
<link>http://localhost:1313/interfaces/rust/</link>
<description>Recent content in Rust on Formal Methods Tools</description>
<generator>Hugo</generator>
<language>en-us</language>
<lastBuildDate>Sat, 07 Jun 2025 00:00:00 +0000</lastBuildDate>
<atom:link href="https://fmtools.fyi/interfaces/rust/index.xml" rel="self" type="application/rss+xml" />
<atom:link href="http://localhost:1313/interfaces/rust/index.xml" rel="self" type="application/rss+xml" />
<item>
<title>Yices 2</title>
<link>https://fmtools.fyi/tools/sat-smt/yices/</link>
<link>http://localhost:1313/tools/sat-smt/yices/</link>
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
<guid>https://fmtools.fyi/tools/sat-smt/yices/</guid>
<guid>http://localhost:1313/tools/sat-smt/yices/</guid>
<description>&lt;p&gt;Yices is an SMT solver developed by SRI International. It is widely used for checking the satisfiability of logical formulas over various theories. It supports the SMT-LIB standard and its own input language, and provides APIs for several programming languages, making it suitable for research and industrial applications in software and hardware verification.&lt;/p&gt;&#xA;&lt;h2 id=&#34;apis-and-bindings&#34;&gt;APIs and Bindings&lt;/h2&gt;&#xA;&lt;p&gt;This tool is available through the following interfaces:&lt;/p&gt;&#xA;&lt;ul&gt;&#xA;&lt;li&gt;&lt;strong&gt;General API:&lt;/strong&gt; &lt;a href=&#34;https://yices.csl.sri.com/doc/index.html&#34; target=&#34;_blank&#34; &gt;Yices API Reference&lt;/a&gt;&lt;/li&gt;&#xA;&lt;li&gt;&lt;strong&gt;Python bindings:&lt;/strong&gt; &lt;a href=&#34;https://pypi.org/project/yices/&#34; target=&#34;_blank&#34; &gt;yices2 PyPI package&lt;/a&gt;&lt;/li&gt;&#xA;&lt;li&gt;&lt;strong&gt;Rust bindings:&lt;/strong&gt; &lt;a href=&#34;https://crates.io/crates/yices2&#34; target=&#34;_blank&#34; &gt;yices2 crate on crates.io&lt;/a&gt;&lt;/li&gt;&#xA;&lt;/ul&gt;</description>
</item>
<item>
<title>Z3</title>
<link>https://fmtools.fyi/tools/sat-smt/z3/</link>
<link>http://localhost:1313/tools/sat-smt/z3/</link>
<pubDate>Sat, 07 Jun 2025 00:00:00 +0000</pubDate>
<guid>https://fmtools.fyi/tools/sat-smt/z3/</guid>
<guid>http://localhost:1313/tools/sat-smt/z3/</guid>
<description>&lt;p&gt;Z3 is a general-purpose theorem prover widely used for SAT &amp;amp; SMT solving.&lt;/p&gt;&#xA;&lt;h2 id=&#34;apis-and-bindings&#34;&gt;APIs and Bindings&lt;/h2&gt;&#xA;&lt;p&gt;This tool is available through the following interfaces:&lt;/p&gt;&#xA;&lt;ul&gt;&#xA;&lt;li&gt;&lt;strong&gt;C API:&lt;/strong&gt; &lt;a href=&#34;https://z3prover.github.io/api/html/group__capi.html&#34; target=&#34;_blank&#34; &gt;Z3 C API Reference&lt;/a&gt;&lt;/li&gt;&#xA;&lt;li&gt;&lt;strong&gt;C++ API:&lt;/strong&gt; &lt;a href=&#34;https://z3prover.github.io/api/html/namespacez3.html&#34; target=&#34;_blank&#34; &gt;Z3 C++ Namespace Reference&lt;/a&gt;&lt;/li&gt;&#xA;&lt;li&gt;&lt;strong&gt;.NET API:&lt;/strong&gt; &lt;a href=&#34;https://z3prover.github.io/api/html/namespace_microsoft_1_1_z3.html&#34; target=&#34;_blank&#34; &gt;Z3 .NET Namespace Reference&lt;/a&gt;&lt;/li&gt;&#xA;&lt;li&gt;&lt;strong&gt;Java API:&lt;/strong&gt; &lt;a href=&#34;https://z3prover.github.io/api/html/namespacecom_1_1microsoft_1_1z3.html&#34; target=&#34;_blank&#34; &gt;Z3 Java API Reference&lt;/a&gt;&lt;/li&gt;&#xA;&lt;li&gt;&lt;strong&gt;Python bindings:&lt;/strong&gt; &lt;a href=&#34;https://pypi.org/project/z3-solver/&#34; target=&#34;_blank&#34; &gt;z3-solver PyPI package&lt;/a&gt; (&lt;a href=&#34;https://z3prover.github.io/api/html/z3.html&#34; target=&#34;_blank&#34; &gt;Documentation&lt;/a&gt;)&lt;/li&gt;&#xA;&lt;li&gt;&lt;strong&gt;Rust bindings:&lt;/strong&gt; &lt;a href=&#34;https://crates.io/crates/z3&#34; target=&#34;_blank&#34; &gt;z3 crate on crates.io&lt;/a&gt;&lt;/li&gt;&#xA;&lt;/ul&gt;</description>
</item>
</channel>