Compare commits
1 Commits
15707a906e
...
65f174e314
| Author | SHA1 | Date | |
|---|---|---|---|
| 65f174e314 |
File diff suppressed because one or more lines are too long
@@ -129,7 +129,7 @@ header h1, header h1 a {
|
||||
color: #ffffff;
|
||||
text-decoration: none;
|
||||
padding: 0;
|
||||
transition: color 0.4s;
|
||||
transition: color 0.4s ease-in-out;
|
||||
}
|
||||
|
||||
header h1:hover, header h1:focus, header h1 a:hover, header h1 a:focus {
|
||||
@@ -163,11 +163,12 @@ nav ul li a {
|
||||
color: #ffffff;
|
||||
text-decoration: none;
|
||||
font-weight: 500;
|
||||
transition: background 0.4s;
|
||||
transition: background 0.4s ease-in-out;
|
||||
}
|
||||
|
||||
nav ul li a:hover, nav ul li a:focus {
|
||||
background: #00897b;
|
||||
color: #ffffff;
|
||||
}
|
||||
|
||||
@media (max-width: 600px) {
|
||||
@@ -234,28 +235,32 @@ table#taxonomy-table {
|
||||
text-align: left;
|
||||
}
|
||||
|
||||
table#taxonomy-table tr {
|
||||
border-bottom: 3px solid #10131a;
|
||||
}
|
||||
|
||||
table#taxonomy-table tr:nth-child(even) {
|
||||
background: #161923;
|
||||
transition: background 0.4s;
|
||||
transition: background 0.4s ease-in-out;
|
||||
}
|
||||
|
||||
table#taxonomy-table tr:nth-child(odd) {
|
||||
background: #202532;
|
||||
transition: background 0.4s;
|
||||
transition: background 0.4s ease-in-out;
|
||||
}
|
||||
|
||||
table#taxonomy-table tr:hover, table#taxonomy-table tr:focus {
|
||||
background: #3a4054;
|
||||
}
|
||||
|
||||
#taxonomy-table thead {
|
||||
table#taxonomy-table thead {
|
||||
text-align: left;
|
||||
border: none;
|
||||
background: #0a0c11;
|
||||
border-radius: 8px 8px 0 0;
|
||||
}
|
||||
|
||||
#taxonomy-table th {
|
||||
table#taxonomy-table th {
|
||||
color: #ffffff;
|
||||
padding: 0.6rem 0.6rem;
|
||||
text-align: left;
|
||||
@@ -263,22 +268,14 @@ table#taxonomy-table tr:hover, table#taxonomy-table tr:focus {
|
||||
border: none;
|
||||
}
|
||||
|
||||
#taxonomy-table td {
|
||||
table#taxonomy-table td {
|
||||
padding: 0.3rem 0.6rem;
|
||||
text-align: left;
|
||||
font-weight: 600;
|
||||
border: none;
|
||||
}
|
||||
|
||||
#taxonomy-table tr {
|
||||
border-bottom: 3px solid #10131a;
|
||||
}
|
||||
|
||||
#taxonomy-table tr:hover, #taxonomy-table tr:focus {
|
||||
background: #8fc6ff;
|
||||
}
|
||||
|
||||
#taxonomy-table a.term-link {
|
||||
table#taxonomy-table a.term-link {
|
||||
padding: 0.2rem 0.6rem;
|
||||
margin: 0.2rem;
|
||||
display: inline-block;
|
||||
@@ -286,14 +283,15 @@ table#taxonomy-table tr:hover, table#taxonomy-table tr:focus {
|
||||
text-decoration: none;
|
||||
font-weight: 500;
|
||||
color: #ffffff;
|
||||
transition: color 0.4s;
|
||||
transition: color 0.4s ease-in-out, background 0.4s ease-in-out;
|
||||
}
|
||||
|
||||
#taxonomy-table a.term-link:hover, #taxonomy-table a.term-link:focus {
|
||||
color: #0a0c11;
|
||||
table#taxonomy-table a.term-link:hover, table#taxonomy-table a.term-link:focus {
|
||||
color: #0a0c11 !important;
|
||||
background: #bfc9e6 !important;
|
||||
}
|
||||
|
||||
#taxonomy-table a.taxonomy-name {
|
||||
table#taxonomy-table a.taxonomy-name {
|
||||
padding: 0;
|
||||
margin: 0.2rem;
|
||||
display: inline-block;
|
||||
@@ -301,10 +299,10 @@ table#taxonomy-table tr:hover, table#taxonomy-table tr:focus {
|
||||
text-decoration: none;
|
||||
font-weight: 500;
|
||||
color: #ffffff;
|
||||
transition: color 0.4s;
|
||||
transition: color 0.4s ease-in-out;
|
||||
}
|
||||
|
||||
#taxonomy-table a.taxonomy-name:hover, #taxonomy-table a.taxonomy-name:focus {
|
||||
table#taxonomy-table a.taxonomy-name:hover, table#taxonomy-table a.taxonomy-name:focus {
|
||||
color: #6fffd2;
|
||||
}
|
||||
|
||||
@@ -316,7 +314,7 @@ table#taxonomy-table tr:hover, table#taxonomy-table tr:focus {
|
||||
text-decoration: none;
|
||||
font-weight: 500;
|
||||
color: #ffffff;
|
||||
transition: color 0.4s;
|
||||
transition: color 0.4s ease-in-out;
|
||||
font-size: 1.2rem;
|
||||
}
|
||||
|
||||
@@ -325,6 +323,16 @@ table#taxonomy-table tr:hover, table#taxonomy-table tr:focus {
|
||||
}
|
||||
|
||||
/* _text.sass */
|
||||
a {
|
||||
color: #3380ff;
|
||||
text-decoration: underline;
|
||||
transition: color 0.3s ease-in-out;
|
||||
}
|
||||
|
||||
a:hover, a:focus {
|
||||
color: #1de9b6;
|
||||
}
|
||||
|
||||
#quick-links {
|
||||
text-align: left;
|
||||
}
|
||||
@@ -361,11 +369,26 @@ table#taxonomy-table tr:hover, table#taxonomy-table tr:focus {
|
||||
color: #0a0c11;
|
||||
text-decoration: none;
|
||||
font-weight: 500;
|
||||
transition: background 0.4s;
|
||||
transition: background 0.3s ease-in-out;
|
||||
}
|
||||
|
||||
#link-list ul li a:hover, #link-list ul li a:focus {
|
||||
background: #6fffd2;
|
||||
}
|
||||
|
||||
#publications ul {
|
||||
list-style: none;
|
||||
margin: 0;
|
||||
padding: 0;
|
||||
display: flex;
|
||||
flex-direction: column;
|
||||
gap: 1em;
|
||||
}
|
||||
|
||||
#publications ul li {
|
||||
background: #1a1e29;
|
||||
border-radius: 8px;
|
||||
padding: 1em 1.5em;
|
||||
}
|
||||
|
||||
/*# sourceMappingURL=styles.css.map */
|
||||
@@ -1,6 +1,6 @@
|
||||
<!DOCTYPE html>
|
||||
<html lang="en-us" dir="ltr">
|
||||
<head>
|
||||
<head><script src="/livereload.js?mindelay=10&v=2&port=1313&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">
|
||||
@@ -13,16 +13,16 @@
|
||||
<meta property="og:type" content="article">
|
||||
<meta property="og:title" content="Developers">
|
||||
<meta property="og:description" content="">
|
||||
<meta property="og:url" content="https://example.org/developers/">
|
||||
<meta property="og:url" content="http://localhost:1313/developers/">
|
||||
<meta property="og:image" content="images/%!s(<nil>)">
|
||||
<link rel="canonical" href="https://example.org/developers/">
|
||||
<link rel="canonical" href="http://localhost:1313/developers/">
|
||||
|
||||
<link rel="apple-touch-icon" sizes="180x180" href='https://example.org/apple-touch-icon.png'>
|
||||
<link rel="icon" type="image/png" sizes="32x32" href='https://example.org/favicon-32x32.png'>
|
||||
<link rel="icon" type="image/png" sizes='16x16' href='https://example.org/favicon-16x16.png'>
|
||||
<link rel="manifest" href='https://example.org/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://example.org/css/styles.fc7cf65388be07f2e53293132dd0220e34d9861f57de4b336d64dd03a3502a9befbea05606442d0a501005442835a864361b9a51b4b51acbf28df37530f61f31.css" integrity="sha512-/Hz2U4i+B/LlMpMTLdAiDjTZhh9X3kszbWTdA6NQKpvvvqBWBkQtClAQBUQoNahkNhuaUbS1GsvyjfN1MPYfMQ==">
|
||||
<link rel="stylesheet" href="http://localhost:1313/css/styles.e3fcfb3452c69d09414fe512e9dca31d879e4a6c47d23010fbb07eb6693d447f645d3bd2d021c0d28d0f7b4fe6f32a10e599488cdb16c6750a9a126788131917.css" integrity="sha512-4/z7NFLGnQlBT+US6dyjHYeeSmxH0jAQ+7B+tmk9RH9kXTvS0CHA0o0Pe0/m8yoQ5ZlIjNsWxnUKmhJniBMZFw==">
|
||||
|
||||
|
||||
|
||||
@@ -70,10 +70,28 @@
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="developers_test-dev"
|
||||
style="background:rgba(103,246,64,0.4)"
|
||||
href="/developers/test-dev">
|
||||
Test Dev
|
||||
id="developers_microsoft-research"
|
||||
style="background:rgba(38,15,27,0.4)"
|
||||
href="/developers/microsoft-research">
|
||||
Microsoft Research
|
||||
</a>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="developers_sri-international"
|
||||
style="background:rgba(97,35,218,0.4)"
|
||||
href="/developers/sri-international">
|
||||
SRI International
|
||||
</a>
|
||||
|
||||
|
||||
|
||||
@@ -2,17 +2,24 @@
|
||||
<rss version="2.0" xmlns:atom="http://www.w3.org/2005/Atom">
|
||||
<channel>
|
||||
<title>Developers on Formal Methods Tools</title>
|
||||
<link>https://example.org/developers/</link>
|
||||
<link>http://localhost:1313/developers/</link>
|
||||
<description>Recent content in Developers on Formal Methods Tools</description>
|
||||
<generator>Hugo</generator>
|
||||
<language>en-us</language>
|
||||
<lastBuildDate>Fri, 02 Feb 2024 04:14:54 -0800</lastBuildDate>
|
||||
<atom:link href="https://example.org/developers/index.xml" rel="self" type="application/rss+xml" />
|
||||
<atom:link href="http://localhost:1313/developers/index.xml" rel="self" type="application/rss+xml" />
|
||||
<item>
|
||||
<title>Test Dev</title>
|
||||
<link>https://example.org/developers/test-dev/</link>
|
||||
<title>Microsoft Research</title>
|
||||
<link>http://localhost:1313/developers/microsoft-research/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>https://example.org/developers/test-dev/</guid>
|
||||
<guid>http://localhost:1313/developers/microsoft-research/</guid>
|
||||
<description></description>
|
||||
</item>
|
||||
<item>
|
||||
<title>SRI International</title>
|
||||
<link>http://localhost:1313/developers/sri-international/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>http://localhost:1313/developers/sri-international/</guid>
|
||||
<description></description>
|
||||
</item>
|
||||
</channel>
|
||||
|
||||
69
developers/microsoft-research/index.html
Normal file
69
developers/microsoft-research/index.html
Normal file
@@ -0,0 +1,69 @@
|
||||
<!DOCTYPE html>
|
||||
<html lang="en-us" dir="ltr">
|
||||
<head><script src="/livereload.js?mindelay=10&v=2&port=1313&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">
|
||||
<meta http-equiv="X-UA-Compatible" content="IE=edge">
|
||||
<title>Microsoft Research | Formal Methods Tools</title>
|
||||
|
||||
|
||||
<meta name="keywords" content="Formal Methods Tools">
|
||||
<meta property="og:locale" content='en_US'>
|
||||
<meta property="og:type" content="article">
|
||||
<meta property="og:title" content="Microsoft Research">
|
||||
<meta property="og:description" content="">
|
||||
<meta property="og:url" content="http://localhost:1313/developers/microsoft-research/">
|
||||
<meta property="og:image" content="images/%!s(<nil>)">
|
||||
<link rel="canonical" href="http://localhost:1313/developers/microsoft-research/">
|
||||
|
||||
<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="http://localhost:1313/css/styles.e3fcfb3452c69d09414fe512e9dca31d879e4a6c47d23010fbb07eb6693d447f645d3bd2d021c0d28d0f7b4fe6f32a10e599488cdb16c6750a9a126788131917.css" integrity="sha512-4/z7NFLGnQlBT+US6dyjHYeeSmxH0jAQ+7B+tmk9RH9kXTvS0CHA0o0Pe0/m8yoQ5ZlIjNsWxnUKmhJniBMZFw==">
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</head>
|
||||
<body>
|
||||
<header>
|
||||
<h1><a href="/">Formal Methods Tools</a></h1>
|
||||
|
||||
<nav>
|
||||
<ul>
|
||||
<li>
|
||||
<a href="/">Home</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/tools/">Tools</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/taxonomies/">Taxonomies</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/about/">About</a>
|
||||
</li>
|
||||
</ul>
|
||||
</nav>
|
||||
|
||||
|
||||
</header>
|
||||
<main>
|
||||
|
||||
<h1>Microsoft Research</h1>
|
||||
|
||||
|
||||
<h2><a href="/tools/z3/">Z3</a></h2>
|
||||
|
||||
|
||||
</main>
|
||||
<footer>
|
||||
<p>Copyright 2025. All rights reserved.</p>
|
||||
|
||||
</footer>
|
||||
</body>
|
||||
</html>
|
||||
19
developers/microsoft-research/index.xml
Normal file
19
developers/microsoft-research/index.xml
Normal file
@@ -0,0 +1,19 @@
|
||||
<?xml version="1.0" encoding="utf-8" standalone="yes"?>
|
||||
<rss version="2.0" xmlns:atom="http://www.w3.org/2005/Atom">
|
||||
<channel>
|
||||
<title>Microsoft Research on Formal Methods Tools</title>
|
||||
<link>http://localhost:1313/developers/microsoft-research/</link>
|
||||
<description>Recent content in Microsoft Research on Formal Methods Tools</description>
|
||||
<generator>Hugo</generator>
|
||||
<language>en-us</language>
|
||||
<lastBuildDate>Fri, 02 Feb 2024 04:14:54 -0800</lastBuildDate>
|
||||
<atom:link href="http://localhost:1313/developers/microsoft-research/index.xml" rel="self" type="application/rss+xml" />
|
||||
<item>
|
||||
<title>Z3</title>
|
||||
<link>http://localhost:1313/tools/z3/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>http://localhost:1313/tools/z3/</guid>
|
||||
<description><p>Z3 is a high-performance SMT solver and theorem prover developed by Microsoft Research. It is widely used for checking the satisfiability of logical formulas over various theories, including arithmetic, bit-vectors, arrays, and uninterpreted functions. Z3 supports the SMT-LIB standard and provides APIs for several programming languages, making it suitable for integration into formal verification, program analysis, and constraint solving tools.</p>
<h3 id="features">Features</h3>
<ul>
<li><strong>SMT Solver:</strong> Supports a wide range of theories and quantifiers.</li>
<li><strong>Multi-language APIs:</strong> Python, C++, Java, .NET, and more.</li>
<li><strong>Cross-platform:</strong> Available on Windows, Linux, and macOS.</li>
<li><strong>Active development:</strong> Open source and maintained by Microsoft Research.</li>
<li><strong>Web Playground:</strong> Try Z3 online at <a href="https://rise4fun.com/z3">Rise4Fun</a>.</li>
</ul></description>
|
||||
</item>
|
||||
</channel>
|
||||
</rss>
|
||||
69
developers/sri-international/index.html
Normal file
69
developers/sri-international/index.html
Normal file
@@ -0,0 +1,69 @@
|
||||
<!DOCTYPE html>
|
||||
<html lang="en-us" dir="ltr">
|
||||
<head><script src="/livereload.js?mindelay=10&v=2&port=1313&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">
|
||||
<meta http-equiv="X-UA-Compatible" content="IE=edge">
|
||||
<title>SRI International | Formal Methods Tools</title>
|
||||
|
||||
|
||||
<meta name="keywords" content="Formal Methods Tools">
|
||||
<meta property="og:locale" content='en_US'>
|
||||
<meta property="og:type" content="article">
|
||||
<meta property="og:title" content="SRI International">
|
||||
<meta property="og:description" content="">
|
||||
<meta property="og:url" content="http://localhost:1313/developers/sri-international/">
|
||||
<meta property="og:image" content="images/%!s(<nil>)">
|
||||
<link rel="canonical" href="http://localhost:1313/developers/sri-international/">
|
||||
|
||||
<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="http://localhost:1313/css/styles.e3fcfb3452c69d09414fe512e9dca31d879e4a6c47d23010fbb07eb6693d447f645d3bd2d021c0d28d0f7b4fe6f32a10e599488cdb16c6750a9a126788131917.css" integrity="sha512-4/z7NFLGnQlBT+US6dyjHYeeSmxH0jAQ+7B+tmk9RH9kXTvS0CHA0o0Pe0/m8yoQ5ZlIjNsWxnUKmhJniBMZFw==">
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</head>
|
||||
<body>
|
||||
<header>
|
||||
<h1><a href="/">Formal Methods Tools</a></h1>
|
||||
|
||||
<nav>
|
||||
<ul>
|
||||
<li>
|
||||
<a href="/">Home</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/tools/">Tools</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/taxonomies/">Taxonomies</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/about/">About</a>
|
||||
</li>
|
||||
</ul>
|
||||
</nav>
|
||||
|
||||
|
||||
</header>
|
||||
<main>
|
||||
|
||||
<h1>SRI International</h1>
|
||||
|
||||
|
||||
<h2><a href="/tools/yices/">Yices 2</a></h2>
|
||||
|
||||
|
||||
</main>
|
||||
<footer>
|
||||
<p>Copyright 2025. All rights reserved.</p>
|
||||
|
||||
</footer>
|
||||
</body>
|
||||
</html>
|
||||
19
developers/sri-international/index.xml
Normal file
19
developers/sri-international/index.xml
Normal file
@@ -0,0 +1,19 @@
|
||||
<?xml version="1.0" encoding="utf-8" standalone="yes"?>
|
||||
<rss version="2.0" xmlns:atom="http://www.w3.org/2005/Atom">
|
||||
<channel>
|
||||
<title>SRI International on Formal Methods Tools</title>
|
||||
<link>http://localhost:1313/developers/sri-international/</link>
|
||||
<description>Recent content in SRI International on Formal Methods Tools</description>
|
||||
<generator>Hugo</generator>
|
||||
<language>en-us</language>
|
||||
<lastBuildDate>Fri, 02 Feb 2024 04:14:54 -0800</lastBuildDate>
|
||||
<atom:link href="http://localhost:1313/developers/sri-international/index.xml" rel="self" type="application/rss+xml" />
|
||||
<item>
|
||||
<title>Yices 2</title>
|
||||
<link>http://localhost:1313/tools/yices/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>http://localhost:1313/tools/yices/</guid>
|
||||
<description><p>Yices is a high-performance SMT solver and theorem prover developed by SRI International. It is widely used for checking the satisfiability of logical formulas over various theories, including arithmetic, bit-vectors, arrays, and uninterpreted functions. Yices supports the SMT-LIB standard and its own input language, and provides APIs for several programming languages, making it suitable for integration into formal verification, program analysis, and constraint solving tools.</p>
<h3 id="features">Features</h3>
<ul>
<li><strong>SMT Solver:</strong> Supports a wide range of theories and quantifiers.</li>
<li><strong>Multi-language APIs:</strong> C, OCaml, Python, and more.</li>
<li><strong>Cross-platform:</strong> Available on Windows, Linux, and macOS.</li>
<li><strong>Active development:</strong> Open source and maintained by SRI International.</li>
</ul></description>
|
||||
</item>
|
||||
</channel>
|
||||
</rss>
|
||||
@@ -1,69 +0,0 @@
|
||||
<!DOCTYPE html>
|
||||
<html lang="en-us" dir="ltr">
|
||||
<head>
|
||||
<meta charset="utf-8">
|
||||
|
||||
<meta name="viewport" content ="width=device-width, initial-scale=1.0, maximum-scale=1.0, user-scalable=no">
|
||||
<meta http-equiv="X-UA-Compatible" content="IE=edge">
|
||||
<title>Test Dev | Formal Methods Tools</title>
|
||||
|
||||
|
||||
<meta name="keywords" content="Formal Methods Tools">
|
||||
<meta property="og:locale" content='en_US'>
|
||||
<meta property="og:type" content="article">
|
||||
<meta property="og:title" content="Test Dev">
|
||||
<meta property="og:description" content="">
|
||||
<meta property="og:url" content="https://example.org/developers/test-dev/">
|
||||
<meta property="og:image" content="images/%!s(<nil>)">
|
||||
<link rel="canonical" href="https://example.org/developers/test-dev/">
|
||||
|
||||
<link rel="apple-touch-icon" sizes="180x180" href='https://example.org/apple-touch-icon.png'>
|
||||
<link rel="icon" type="image/png" sizes="32x32" href='https://example.org/favicon-32x32.png'>
|
||||
<link rel="icon" type="image/png" sizes='16x16' href='https://example.org/favicon-16x16.png'>
|
||||
<link rel="manifest" href='https://example.org/site.webmanifest'>
|
||||
|
||||
<link rel="stylesheet" href="https://example.org/css/styles.fc7cf65388be07f2e53293132dd0220e34d9861f57de4b336d64dd03a3502a9befbea05606442d0a501005442835a864361b9a51b4b51acbf28df37530f61f31.css" integrity="sha512-/Hz2U4i+B/LlMpMTLdAiDjTZhh9X3kszbWTdA6NQKpvvvqBWBkQtClAQBUQoNahkNhuaUbS1GsvyjfN1MPYfMQ==">
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</head>
|
||||
<body>
|
||||
<header>
|
||||
<h1><a href="/">Formal Methods Tools</a></h1>
|
||||
|
||||
<nav>
|
||||
<ul>
|
||||
<li>
|
||||
<a href="/">Home</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/tools/">Tools</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/taxonomies/">Taxonomies</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/about/">About</a>
|
||||
</li>
|
||||
</ul>
|
||||
</nav>
|
||||
|
||||
|
||||
</header>
|
||||
<main>
|
||||
|
||||
<h1>Test Dev</h1>
|
||||
|
||||
|
||||
<h2><a href="/tools/z3/">Z3 Theorem Prover</a></h2>
|
||||
|
||||
|
||||
</main>
|
||||
<footer>
|
||||
<p>Copyright 2025. All rights reserved.</p>
|
||||
|
||||
</footer>
|
||||
</body>
|
||||
</html>
|
||||
@@ -1,19 +0,0 @@
|
||||
<?xml version="1.0" encoding="utf-8" standalone="yes"?>
|
||||
<rss version="2.0" xmlns:atom="http://www.w3.org/2005/Atom">
|
||||
<channel>
|
||||
<title>Test Dev on Formal Methods Tools</title>
|
||||
<link>https://example.org/developers/test-dev/</link>
|
||||
<description>Recent content in Test Dev on Formal Methods Tools</description>
|
||||
<generator>Hugo</generator>
|
||||
<language>en-us</language>
|
||||
<lastBuildDate>Fri, 02 Feb 2024 04:14:54 -0800</lastBuildDate>
|
||||
<atom:link href="https://example.org/developers/test-dev/index.xml" rel="self" type="application/rss+xml" />
|
||||
<item>
|
||||
<title>Z3 Theorem Prover</title>
|
||||
<link>https://example.org/tools/z3/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>https://example.org/tools/z3/</guid>
|
||||
<description><p>desc</p></description>
|
||||
</item>
|
||||
</channel>
|
||||
</rss>
|
||||
71
domains/embedded-systems/index.html
Normal file
71
domains/embedded-systems/index.html
Normal file
@@ -0,0 +1,71 @@
|
||||
<!DOCTYPE html>
|
||||
<html lang="en-us" dir="ltr">
|
||||
<head><script src="/livereload.js?mindelay=10&v=2&port=1313&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">
|
||||
<meta http-equiv="X-UA-Compatible" content="IE=edge">
|
||||
<title>Embedded Systems | Formal Methods Tools</title>
|
||||
|
||||
|
||||
<meta name="keywords" content="Formal Methods Tools">
|
||||
<meta property="og:locale" content='en_US'>
|
||||
<meta property="og:type" content="article">
|
||||
<meta property="og:title" content="Embedded Systems">
|
||||
<meta property="og:description" content="">
|
||||
<meta property="og:url" content="http://localhost:1313/domains/embedded-systems/">
|
||||
<meta property="og:image" content="images/%!s(<nil>)">
|
||||
<link rel="canonical" href="http://localhost:1313/domains/embedded-systems/">
|
||||
|
||||
<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="http://localhost:1313/css/styles.e3fcfb3452c69d09414fe512e9dca31d879e4a6c47d23010fbb07eb6693d447f645d3bd2d021c0d28d0f7b4fe6f32a10e599488cdb16c6750a9a126788131917.css" integrity="sha512-4/z7NFLGnQlBT+US6dyjHYeeSmxH0jAQ+7B+tmk9RH9kXTvS0CHA0o0Pe0/m8yoQ5ZlIjNsWxnUKmhJniBMZFw==">
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</head>
|
||||
<body>
|
||||
<header>
|
||||
<h1><a href="/">Formal Methods Tools</a></h1>
|
||||
|
||||
<nav>
|
||||
<ul>
|
||||
<li>
|
||||
<a href="/">Home</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/tools/">Tools</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/taxonomies/">Taxonomies</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/about/">About</a>
|
||||
</li>
|
||||
</ul>
|
||||
</nav>
|
||||
|
||||
|
||||
</header>
|
||||
<main>
|
||||
|
||||
<h1>Embedded Systems</h1>
|
||||
|
||||
|
||||
<h2><a href="/tools/yices/">Yices 2</a></h2>
|
||||
|
||||
<h2><a href="/tools/z3/">Z3</a></h2>
|
||||
|
||||
|
||||
</main>
|
||||
<footer>
|
||||
<p>Copyright 2025. All rights reserved.</p>
|
||||
|
||||
</footer>
|
||||
</body>
|
||||
</html>
|
||||
26
domains/embedded-systems/index.xml
Normal file
26
domains/embedded-systems/index.xml
Normal file
@@ -0,0 +1,26 @@
|
||||
<?xml version="1.0" encoding="utf-8" standalone="yes"?>
|
||||
<rss version="2.0" xmlns:atom="http://www.w3.org/2005/Atom">
|
||||
<channel>
|
||||
<title>Embedded Systems on Formal Methods Tools</title>
|
||||
<link>http://localhost:1313/domains/embedded-systems/</link>
|
||||
<description>Recent content in Embedded Systems on Formal Methods Tools</description>
|
||||
<generator>Hugo</generator>
|
||||
<language>en-us</language>
|
||||
<lastBuildDate>Fri, 02 Feb 2024 04:14:54 -0800</lastBuildDate>
|
||||
<atom:link href="http://localhost:1313/domains/embedded-systems/index.xml" rel="self" type="application/rss+xml" />
|
||||
<item>
|
||||
<title>Yices 2</title>
|
||||
<link>http://localhost:1313/tools/yices/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>http://localhost:1313/tools/yices/</guid>
|
||||
<description><p>Yices is a high-performance SMT solver and theorem prover developed by SRI International. It is widely used for checking the satisfiability of logical formulas over various theories, including arithmetic, bit-vectors, arrays, and uninterpreted functions. Yices supports the SMT-LIB standard and its own input language, and provides APIs for several programming languages, making it suitable for integration into formal verification, program analysis, and constraint solving tools.</p>
<h3 id="features">Features</h3>
<ul>
<li><strong>SMT Solver:</strong> Supports a wide range of theories and quantifiers.</li>
<li><strong>Multi-language APIs:</strong> C, OCaml, Python, and more.</li>
<li><strong>Cross-platform:</strong> Available on Windows, Linux, and macOS.</li>
<li><strong>Active development:</strong> Open source and maintained by SRI International.</li>
</ul></description>
|
||||
</item>
|
||||
<item>
|
||||
<title>Z3</title>
|
||||
<link>http://localhost:1313/tools/z3/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>http://localhost:1313/tools/z3/</guid>
|
||||
<description><p>Z3 is a high-performance SMT solver and theorem prover developed by Microsoft Research. It is widely used for checking the satisfiability of logical formulas over various theories, including arithmetic, bit-vectors, arrays, and uninterpreted functions. Z3 supports the SMT-LIB standard and provides APIs for several programming languages, making it suitable for integration into formal verification, program analysis, and constraint solving tools.</p>
<h3 id="features">Features</h3>
<ul>
<li><strong>SMT Solver:</strong> Supports a wide range of theories and quantifiers.</li>
<li><strong>Multi-language APIs:</strong> Python, C++, Java, .NET, and more.</li>
<li><strong>Cross-platform:</strong> Available on Windows, Linux, and macOS.</li>
<li><strong>Active development:</strong> Open source and maintained by Microsoft Research.</li>
<li><strong>Web Playground:</strong> Try Z3 online at <a href="https://rise4fun.com/z3">Rise4Fun</a>.</li>
</ul></description>
|
||||
</item>
|
||||
</channel>
|
||||
</rss>
|
||||
71
domains/hardware-verification/index.html
Normal file
71
domains/hardware-verification/index.html
Normal file
@@ -0,0 +1,71 @@
|
||||
<!DOCTYPE html>
|
||||
<html lang="en-us" dir="ltr">
|
||||
<head><script src="/livereload.js?mindelay=10&v=2&port=1313&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">
|
||||
<meta http-equiv="X-UA-Compatible" content="IE=edge">
|
||||
<title>Hardware Verification | Formal Methods Tools</title>
|
||||
|
||||
|
||||
<meta name="keywords" content="Formal Methods Tools">
|
||||
<meta property="og:locale" content='en_US'>
|
||||
<meta property="og:type" content="article">
|
||||
<meta property="og:title" content="Hardware Verification">
|
||||
<meta property="og:description" content="">
|
||||
<meta property="og:url" content="http://localhost:1313/domains/hardware-verification/">
|
||||
<meta property="og:image" content="images/%!s(<nil>)">
|
||||
<link rel="canonical" href="http://localhost:1313/domains/hardware-verification/">
|
||||
|
||||
<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="http://localhost:1313/css/styles.e3fcfb3452c69d09414fe512e9dca31d879e4a6c47d23010fbb07eb6693d447f645d3bd2d021c0d28d0f7b4fe6f32a10e599488cdb16c6750a9a126788131917.css" integrity="sha512-4/z7NFLGnQlBT+US6dyjHYeeSmxH0jAQ+7B+tmk9RH9kXTvS0CHA0o0Pe0/m8yoQ5ZlIjNsWxnUKmhJniBMZFw==">
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</head>
|
||||
<body>
|
||||
<header>
|
||||
<h1><a href="/">Formal Methods Tools</a></h1>
|
||||
|
||||
<nav>
|
||||
<ul>
|
||||
<li>
|
||||
<a href="/">Home</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/tools/">Tools</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/taxonomies/">Taxonomies</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/about/">About</a>
|
||||
</li>
|
||||
</ul>
|
||||
</nav>
|
||||
|
||||
|
||||
</header>
|
||||
<main>
|
||||
|
||||
<h1>Hardware Verification</h1>
|
||||
|
||||
|
||||
<h2><a href="/tools/yices/">Yices 2</a></h2>
|
||||
|
||||
<h2><a href="/tools/z3/">Z3</a></h2>
|
||||
|
||||
|
||||
</main>
|
||||
<footer>
|
||||
<p>Copyright 2025. All rights reserved.</p>
|
||||
|
||||
</footer>
|
||||
</body>
|
||||
</html>
|
||||
26
domains/hardware-verification/index.xml
Normal file
26
domains/hardware-verification/index.xml
Normal file
@@ -0,0 +1,26 @@
|
||||
<?xml version="1.0" encoding="utf-8" standalone="yes"?>
|
||||
<rss version="2.0" xmlns:atom="http://www.w3.org/2005/Atom">
|
||||
<channel>
|
||||
<title>Hardware Verification on Formal Methods Tools</title>
|
||||
<link>http://localhost:1313/domains/hardware-verification/</link>
|
||||
<description>Recent content in Hardware Verification on Formal Methods Tools</description>
|
||||
<generator>Hugo</generator>
|
||||
<language>en-us</language>
|
||||
<lastBuildDate>Fri, 02 Feb 2024 04:14:54 -0800</lastBuildDate>
|
||||
<atom:link href="http://localhost:1313/domains/hardware-verification/index.xml" rel="self" type="application/rss+xml" />
|
||||
<item>
|
||||
<title>Yices 2</title>
|
||||
<link>http://localhost:1313/tools/yices/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>http://localhost:1313/tools/yices/</guid>
|
||||
<description><p>Yices is a high-performance SMT solver and theorem prover developed by SRI International. It is widely used for checking the satisfiability of logical formulas over various theories, including arithmetic, bit-vectors, arrays, and uninterpreted functions. Yices supports the SMT-LIB standard and its own input language, and provides APIs for several programming languages, making it suitable for integration into formal verification, program analysis, and constraint solving tools.</p>
<h3 id="features">Features</h3>
<ul>
<li><strong>SMT Solver:</strong> Supports a wide range of theories and quantifiers.</li>
<li><strong>Multi-language APIs:</strong> C, OCaml, Python, and more.</li>
<li><strong>Cross-platform:</strong> Available on Windows, Linux, and macOS.</li>
<li><strong>Active development:</strong> Open source and maintained by SRI International.</li>
</ul></description>
|
||||
</item>
|
||||
<item>
|
||||
<title>Z3</title>
|
||||
<link>http://localhost:1313/tools/z3/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>http://localhost:1313/tools/z3/</guid>
|
||||
<description><p>Z3 is a high-performance SMT solver and theorem prover developed by Microsoft Research. It is widely used for checking the satisfiability of logical formulas over various theories, including arithmetic, bit-vectors, arrays, and uninterpreted functions. Z3 supports the SMT-LIB standard and provides APIs for several programming languages, making it suitable for integration into formal verification, program analysis, and constraint solving tools.</p>
<h3 id="features">Features</h3>
<ul>
<li><strong>SMT Solver:</strong> Supports a wide range of theories and quantifiers.</li>
<li><strong>Multi-language APIs:</strong> Python, C++, Java, .NET, and more.</li>
<li><strong>Cross-platform:</strong> Available on Windows, Linux, and macOS.</li>
<li><strong>Active development:</strong> Open source and maintained by Microsoft Research.</li>
<li><strong>Web Playground:</strong> Try Z3 online at <a href="https://rise4fun.com/z3">Rise4Fun</a>.</li>
</ul></description>
|
||||
</item>
|
||||
</channel>
|
||||
</rss>
|
||||
@@ -1,6 +1,6 @@
|
||||
<!DOCTYPE html>
|
||||
<html lang="en-us" dir="ltr">
|
||||
<head>
|
||||
<head><script src="/livereload.js?mindelay=10&v=2&port=1313&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">
|
||||
@@ -13,16 +13,16 @@
|
||||
<meta property="og:type" content="article">
|
||||
<meta property="og:title" content="Domains">
|
||||
<meta property="og:description" content="">
|
||||
<meta property="og:url" content="https://example.org/domains/">
|
||||
<meta property="og:url" content="http://localhost:1313/domains/">
|
||||
<meta property="og:image" content="images/%!s(<nil>)">
|
||||
<link rel="canonical" href="https://example.org/domains/">
|
||||
<link rel="canonical" href="http://localhost:1313/domains/">
|
||||
|
||||
<link rel="apple-touch-icon" sizes="180x180" href='https://example.org/apple-touch-icon.png'>
|
||||
<link rel="icon" type="image/png" sizes="32x32" href='https://example.org/favicon-32x32.png'>
|
||||
<link rel="icon" type="image/png" sizes='16x16' href='https://example.org/favicon-16x16.png'>
|
||||
<link rel="manifest" href='https://example.org/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://example.org/css/styles.fc7cf65388be07f2e53293132dd0220e34d9861f57de4b336d64dd03a3502a9befbea05606442d0a501005442835a864361b9a51b4b51acbf28df37530f61f31.css" integrity="sha512-/Hz2U4i+B/LlMpMTLdAiDjTZhh9X3kszbWTdA6NQKpvvvqBWBkQtClAQBUQoNahkNhuaUbS1GsvyjfN1MPYfMQ==">
|
||||
<link rel="stylesheet" href="http://localhost:1313/css/styles.e3fcfb3452c69d09414fe512e9dca31d879e4a6c47d23010fbb07eb6693d447f645d3bd2d021c0d28d0f7b4fe6f32a10e599488cdb16c6750a9a126788131917.css" integrity="sha512-4/z7NFLGnQlBT+US6dyjHYeeSmxH0jAQ+7B+tmk9RH9kXTvS0CHA0o0Pe0/m8yoQ5ZlIjNsWxnUKmhJniBMZFw==">
|
||||
|
||||
|
||||
|
||||
@@ -70,10 +70,46 @@
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="domains_tttt"
|
||||
style="background:rgba(229,115,100,0.4)"
|
||||
href="/domains/tttt">
|
||||
Tttt
|
||||
id="domains_embedded-systems"
|
||||
style="background:rgba(130,108,187,0.4)"
|
||||
href="/domains/embedded-systems">
|
||||
Embedded Systems
|
||||
</a>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="domains_hardware-verification"
|
||||
style="background:rgba(35,59,44,0.4)"
|
||||
href="/domains/hardware-verification">
|
||||
Hardware Verification
|
||||
</a>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="domains_software-verification"
|
||||
style="background:rgba(127,54,56,0.4)"
|
||||
href="/domains/software-verification">
|
||||
Software Verification
|
||||
</a>
|
||||
|
||||
|
||||
|
||||
@@ -2,17 +2,31 @@
|
||||
<rss version="2.0" xmlns:atom="http://www.w3.org/2005/Atom">
|
||||
<channel>
|
||||
<title>Domains on Formal Methods Tools</title>
|
||||
<link>https://example.org/domains/</link>
|
||||
<link>http://localhost:1313/domains/</link>
|
||||
<description>Recent content in Domains on Formal Methods Tools</description>
|
||||
<generator>Hugo</generator>
|
||||
<language>en-us</language>
|
||||
<lastBuildDate>Fri, 02 Feb 2024 04:14:54 -0800</lastBuildDate>
|
||||
<atom:link href="https://example.org/domains/index.xml" rel="self" type="application/rss+xml" />
|
||||
<atom:link href="http://localhost:1313/domains/index.xml" rel="self" type="application/rss+xml" />
|
||||
<item>
|
||||
<title>Tttt</title>
|
||||
<link>https://example.org/domains/tttt/</link>
|
||||
<title>Embedded Systems</title>
|
||||
<link>http://localhost:1313/domains/embedded-systems/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>https://example.org/domains/tttt/</guid>
|
||||
<guid>http://localhost:1313/domains/embedded-systems/</guid>
|
||||
<description></description>
|
||||
</item>
|
||||
<item>
|
||||
<title>Hardware Verification</title>
|
||||
<link>http://localhost:1313/domains/hardware-verification/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>http://localhost:1313/domains/hardware-verification/</guid>
|
||||
<description></description>
|
||||
</item>
|
||||
<item>
|
||||
<title>Software Verification</title>
|
||||
<link>http://localhost:1313/domains/software-verification/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>http://localhost:1313/domains/software-verification/</guid>
|
||||
<description></description>
|
||||
</item>
|
||||
</channel>
|
||||
|
||||
71
domains/software-verification/index.html
Normal file
71
domains/software-verification/index.html
Normal file
@@ -0,0 +1,71 @@
|
||||
<!DOCTYPE html>
|
||||
<html lang="en-us" dir="ltr">
|
||||
<head><script src="/livereload.js?mindelay=10&v=2&port=1313&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">
|
||||
<meta http-equiv="X-UA-Compatible" content="IE=edge">
|
||||
<title>Software Verification | Formal Methods Tools</title>
|
||||
|
||||
|
||||
<meta name="keywords" content="Formal Methods Tools">
|
||||
<meta property="og:locale" content='en_US'>
|
||||
<meta property="og:type" content="article">
|
||||
<meta property="og:title" content="Software Verification">
|
||||
<meta property="og:description" content="">
|
||||
<meta property="og:url" content="http://localhost:1313/domains/software-verification/">
|
||||
<meta property="og:image" content="images/%!s(<nil>)">
|
||||
<link rel="canonical" href="http://localhost:1313/domains/software-verification/">
|
||||
|
||||
<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="http://localhost:1313/css/styles.e3fcfb3452c69d09414fe512e9dca31d879e4a6c47d23010fbb07eb6693d447f645d3bd2d021c0d28d0f7b4fe6f32a10e599488cdb16c6750a9a126788131917.css" integrity="sha512-4/z7NFLGnQlBT+US6dyjHYeeSmxH0jAQ+7B+tmk9RH9kXTvS0CHA0o0Pe0/m8yoQ5ZlIjNsWxnUKmhJniBMZFw==">
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</head>
|
||||
<body>
|
||||
<header>
|
||||
<h1><a href="/">Formal Methods Tools</a></h1>
|
||||
|
||||
<nav>
|
||||
<ul>
|
||||
<li>
|
||||
<a href="/">Home</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/tools/">Tools</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/taxonomies/">Taxonomies</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/about/">About</a>
|
||||
</li>
|
||||
</ul>
|
||||
</nav>
|
||||
|
||||
|
||||
</header>
|
||||
<main>
|
||||
|
||||
<h1>Software Verification</h1>
|
||||
|
||||
|
||||
<h2><a href="/tools/yices/">Yices 2</a></h2>
|
||||
|
||||
<h2><a href="/tools/z3/">Z3</a></h2>
|
||||
|
||||
|
||||
</main>
|
||||
<footer>
|
||||
<p>Copyright 2025. All rights reserved.</p>
|
||||
|
||||
</footer>
|
||||
</body>
|
||||
</html>
|
||||
26
domains/software-verification/index.xml
Normal file
26
domains/software-verification/index.xml
Normal file
@@ -0,0 +1,26 @@
|
||||
<?xml version="1.0" encoding="utf-8" standalone="yes"?>
|
||||
<rss version="2.0" xmlns:atom="http://www.w3.org/2005/Atom">
|
||||
<channel>
|
||||
<title>Software Verification on Formal Methods Tools</title>
|
||||
<link>http://localhost:1313/domains/software-verification/</link>
|
||||
<description>Recent content in Software Verification on Formal Methods Tools</description>
|
||||
<generator>Hugo</generator>
|
||||
<language>en-us</language>
|
||||
<lastBuildDate>Fri, 02 Feb 2024 04:14:54 -0800</lastBuildDate>
|
||||
<atom:link href="http://localhost:1313/domains/software-verification/index.xml" rel="self" type="application/rss+xml" />
|
||||
<item>
|
||||
<title>Yices 2</title>
|
||||
<link>http://localhost:1313/tools/yices/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>http://localhost:1313/tools/yices/</guid>
|
||||
<description><p>Yices is a high-performance SMT solver and theorem prover developed by SRI International. It is widely used for checking the satisfiability of logical formulas over various theories, including arithmetic, bit-vectors, arrays, and uninterpreted functions. Yices supports the SMT-LIB standard and its own input language, and provides APIs for several programming languages, making it suitable for integration into formal verification, program analysis, and constraint solving tools.</p>
<h3 id="features">Features</h3>
<ul>
<li><strong>SMT Solver:</strong> Supports a wide range of theories and quantifiers.</li>
<li><strong>Multi-language APIs:</strong> C, OCaml, Python, and more.</li>
<li><strong>Cross-platform:</strong> Available on Windows, Linux, and macOS.</li>
<li><strong>Active development:</strong> Open source and maintained by SRI International.</li>
</ul></description>
|
||||
</item>
|
||||
<item>
|
||||
<title>Z3</title>
|
||||
<link>http://localhost:1313/tools/z3/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>http://localhost:1313/tools/z3/</guid>
|
||||
<description><p>Z3 is a high-performance SMT solver and theorem prover developed by Microsoft Research. It is widely used for checking the satisfiability of logical formulas over various theories, including arithmetic, bit-vectors, arrays, and uninterpreted functions. Z3 supports the SMT-LIB standard and provides APIs for several programming languages, making it suitable for integration into formal verification, program analysis, and constraint solving tools.</p>
<h3 id="features">Features</h3>
<ul>
<li><strong>SMT Solver:</strong> Supports a wide range of theories and quantifiers.</li>
<li><strong>Multi-language APIs:</strong> Python, C++, Java, .NET, and more.</li>
<li><strong>Cross-platform:</strong> Available on Windows, Linux, and macOS.</li>
<li><strong>Active development:</strong> Open source and maintained by Microsoft Research.</li>
<li><strong>Web Playground:</strong> Try Z3 online at <a href="https://rise4fun.com/z3">Rise4Fun</a>.</li>
</ul></description>
|
||||
</item>
|
||||
</channel>
|
||||
</rss>
|
||||
@@ -1,69 +0,0 @@
|
||||
<!DOCTYPE html>
|
||||
<html lang="en-us" dir="ltr">
|
||||
<head>
|
||||
<meta charset="utf-8">
|
||||
|
||||
<meta name="viewport" content ="width=device-width, initial-scale=1.0, maximum-scale=1.0, user-scalable=no">
|
||||
<meta http-equiv="X-UA-Compatible" content="IE=edge">
|
||||
<title>Tttt | Formal Methods Tools</title>
|
||||
|
||||
|
||||
<meta name="keywords" content="Formal Methods Tools">
|
||||
<meta property="og:locale" content='en_US'>
|
||||
<meta property="og:type" content="article">
|
||||
<meta property="og:title" content="Tttt">
|
||||
<meta property="og:description" content="">
|
||||
<meta property="og:url" content="https://example.org/domains/tttt/">
|
||||
<meta property="og:image" content="images/%!s(<nil>)">
|
||||
<link rel="canonical" href="https://example.org/domains/tttt/">
|
||||
|
||||
<link rel="apple-touch-icon" sizes="180x180" href='https://example.org/apple-touch-icon.png'>
|
||||
<link rel="icon" type="image/png" sizes="32x32" href='https://example.org/favicon-32x32.png'>
|
||||
<link rel="icon" type="image/png" sizes='16x16' href='https://example.org/favicon-16x16.png'>
|
||||
<link rel="manifest" href='https://example.org/site.webmanifest'>
|
||||
|
||||
<link rel="stylesheet" href="https://example.org/css/styles.fc7cf65388be07f2e53293132dd0220e34d9861f57de4b336d64dd03a3502a9befbea05606442d0a501005442835a864361b9a51b4b51acbf28df37530f61f31.css" integrity="sha512-/Hz2U4i+B/LlMpMTLdAiDjTZhh9X3kszbWTdA6NQKpvvvqBWBkQtClAQBUQoNahkNhuaUbS1GsvyjfN1MPYfMQ==">
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</head>
|
||||
<body>
|
||||
<header>
|
||||
<h1><a href="/">Formal Methods Tools</a></h1>
|
||||
|
||||
<nav>
|
||||
<ul>
|
||||
<li>
|
||||
<a href="/">Home</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/tools/">Tools</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/taxonomies/">Taxonomies</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/about/">About</a>
|
||||
</li>
|
||||
</ul>
|
||||
</nav>
|
||||
|
||||
|
||||
</header>
|
||||
<main>
|
||||
|
||||
<h1>Tttt</h1>
|
||||
|
||||
|
||||
<h2><a href="/tools/z3/">Z3 Theorem Prover</a></h2>
|
||||
|
||||
|
||||
</main>
|
||||
<footer>
|
||||
<p>Copyright 2025. All rights reserved.</p>
|
||||
|
||||
</footer>
|
||||
</body>
|
||||
</html>
|
||||
@@ -1,19 +0,0 @@
|
||||
<?xml version="1.0" encoding="utf-8" standalone="yes"?>
|
||||
<rss version="2.0" xmlns:atom="http://www.w3.org/2005/Atom">
|
||||
<channel>
|
||||
<title>Tttt on Formal Methods Tools</title>
|
||||
<link>https://example.org/domains/tttt/</link>
|
||||
<description>Recent content in Tttt on Formal Methods Tools</description>
|
||||
<generator>Hugo</generator>
|
||||
<language>en-us</language>
|
||||
<lastBuildDate>Fri, 02 Feb 2024 04:14:54 -0800</lastBuildDate>
|
||||
<atom:link href="https://example.org/domains/tttt/index.xml" rel="self" type="application/rss+xml" />
|
||||
<item>
|
||||
<title>Z3 Theorem Prover</title>
|
||||
<link>https://example.org/tools/z3/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>https://example.org/tools/z3/</guid>
|
||||
<description><p>desc</p></description>
|
||||
</item>
|
||||
</channel>
|
||||
</rss>
|
||||
71
formalisms/arithmetic/index.html
Normal file
71
formalisms/arithmetic/index.html
Normal file
@@ -0,0 +1,71 @@
|
||||
<!DOCTYPE html>
|
||||
<html lang="en-us" dir="ltr">
|
||||
<head><script src="/livereload.js?mindelay=10&v=2&port=1313&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">
|
||||
<meta http-equiv="X-UA-Compatible" content="IE=edge">
|
||||
<title>Arithmetic | Formal Methods Tools</title>
|
||||
|
||||
|
||||
<meta name="keywords" content="Formal Methods Tools">
|
||||
<meta property="og:locale" content='en_US'>
|
||||
<meta property="og:type" content="article">
|
||||
<meta property="og:title" content="Arithmetic">
|
||||
<meta property="og:description" content="">
|
||||
<meta property="og:url" content="http://localhost:1313/formalisms/arithmetic/">
|
||||
<meta property="og:image" content="images/%!s(<nil>)">
|
||||
<link rel="canonical" href="http://localhost:1313/formalisms/arithmetic/">
|
||||
|
||||
<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="http://localhost:1313/css/styles.e3fcfb3452c69d09414fe512e9dca31d879e4a6c47d23010fbb07eb6693d447f645d3bd2d021c0d28d0f7b4fe6f32a10e599488cdb16c6750a9a126788131917.css" integrity="sha512-4/z7NFLGnQlBT+US6dyjHYeeSmxH0jAQ+7B+tmk9RH9kXTvS0CHA0o0Pe0/m8yoQ5ZlIjNsWxnUKmhJniBMZFw==">
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</head>
|
||||
<body>
|
||||
<header>
|
||||
<h1><a href="/">Formal Methods Tools</a></h1>
|
||||
|
||||
<nav>
|
||||
<ul>
|
||||
<li>
|
||||
<a href="/">Home</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/tools/">Tools</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/taxonomies/">Taxonomies</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/about/">About</a>
|
||||
</li>
|
||||
</ul>
|
||||
</nav>
|
||||
|
||||
|
||||
</header>
|
||||
<main>
|
||||
|
||||
<h1>Arithmetic</h1>
|
||||
|
||||
|
||||
<h2><a href="/tools/yices/">Yices 2</a></h2>
|
||||
|
||||
<h2><a href="/tools/z3/">Z3</a></h2>
|
||||
|
||||
|
||||
</main>
|
||||
<footer>
|
||||
<p>Copyright 2025. All rights reserved.</p>
|
||||
|
||||
</footer>
|
||||
</body>
|
||||
</html>
|
||||
26
formalisms/arithmetic/index.xml
Normal file
26
formalisms/arithmetic/index.xml
Normal file
@@ -0,0 +1,26 @@
|
||||
<?xml version="1.0" encoding="utf-8" standalone="yes"?>
|
||||
<rss version="2.0" xmlns:atom="http://www.w3.org/2005/Atom">
|
||||
<channel>
|
||||
<title>Arithmetic on Formal Methods Tools</title>
|
||||
<link>http://localhost:1313/formalisms/arithmetic/</link>
|
||||
<description>Recent content in Arithmetic on Formal Methods Tools</description>
|
||||
<generator>Hugo</generator>
|
||||
<language>en-us</language>
|
||||
<lastBuildDate>Fri, 02 Feb 2024 04:14:54 -0800</lastBuildDate>
|
||||
<atom:link href="http://localhost:1313/formalisms/arithmetic/index.xml" rel="self" type="application/rss+xml" />
|
||||
<item>
|
||||
<title>Yices 2</title>
|
||||
<link>http://localhost:1313/tools/yices/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>http://localhost:1313/tools/yices/</guid>
|
||||
<description><p>Yices is a high-performance SMT solver and theorem prover developed by SRI International. It is widely used for checking the satisfiability of logical formulas over various theories, including arithmetic, bit-vectors, arrays, and uninterpreted functions. Yices supports the SMT-LIB standard and its own input language, and provides APIs for several programming languages, making it suitable for integration into formal verification, program analysis, and constraint solving tools.</p>
<h3 id="features">Features</h3>
<ul>
<li><strong>SMT Solver:</strong> Supports a wide range of theories and quantifiers.</li>
<li><strong>Multi-language APIs:</strong> C, OCaml, Python, and more.</li>
<li><strong>Cross-platform:</strong> Available on Windows, Linux, and macOS.</li>
<li><strong>Active development:</strong> Open source and maintained by SRI International.</li>
</ul></description>
|
||||
</item>
|
||||
<item>
|
||||
<title>Z3</title>
|
||||
<link>http://localhost:1313/tools/z3/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>http://localhost:1313/tools/z3/</guid>
|
||||
<description><p>Z3 is a high-performance SMT solver and theorem prover developed by Microsoft Research. It is widely used for checking the satisfiability of logical formulas over various theories, including arithmetic, bit-vectors, arrays, and uninterpreted functions. Z3 supports the SMT-LIB standard and provides APIs for several programming languages, making it suitable for integration into formal verification, program analysis, and constraint solving tools.</p>
<h3 id="features">Features</h3>
<ul>
<li><strong>SMT Solver:</strong> Supports a wide range of theories and quantifiers.</li>
<li><strong>Multi-language APIs:</strong> Python, C++, Java, .NET, and more.</li>
<li><strong>Cross-platform:</strong> Available on Windows, Linux, and macOS.</li>
<li><strong>Active development:</strong> Open source and maintained by Microsoft Research.</li>
<li><strong>Web Playground:</strong> Try Z3 online at <a href="https://rise4fun.com/z3">Rise4Fun</a>.</li>
</ul></description>
|
||||
</item>
|
||||
</channel>
|
||||
</rss>
|
||||
71
formalisms/arrays/index.html
Normal file
71
formalisms/arrays/index.html
Normal file
@@ -0,0 +1,71 @@
|
||||
<!DOCTYPE html>
|
||||
<html lang="en-us" dir="ltr">
|
||||
<head><script src="/livereload.js?mindelay=10&v=2&port=1313&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">
|
||||
<meta http-equiv="X-UA-Compatible" content="IE=edge">
|
||||
<title>Arrays | Formal Methods Tools</title>
|
||||
|
||||
|
||||
<meta name="keywords" content="Formal Methods Tools">
|
||||
<meta property="og:locale" content='en_US'>
|
||||
<meta property="og:type" content="article">
|
||||
<meta property="og:title" content="Arrays">
|
||||
<meta property="og:description" content="">
|
||||
<meta property="og:url" content="http://localhost:1313/formalisms/arrays/">
|
||||
<meta property="og:image" content="images/%!s(<nil>)">
|
||||
<link rel="canonical" href="http://localhost:1313/formalisms/arrays/">
|
||||
|
||||
<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="http://localhost:1313/css/styles.e3fcfb3452c69d09414fe512e9dca31d879e4a6c47d23010fbb07eb6693d447f645d3bd2d021c0d28d0f7b4fe6f32a10e599488cdb16c6750a9a126788131917.css" integrity="sha512-4/z7NFLGnQlBT+US6dyjHYeeSmxH0jAQ+7B+tmk9RH9kXTvS0CHA0o0Pe0/m8yoQ5ZlIjNsWxnUKmhJniBMZFw==">
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</head>
|
||||
<body>
|
||||
<header>
|
||||
<h1><a href="/">Formal Methods Tools</a></h1>
|
||||
|
||||
<nav>
|
||||
<ul>
|
||||
<li>
|
||||
<a href="/">Home</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/tools/">Tools</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/taxonomies/">Taxonomies</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/about/">About</a>
|
||||
</li>
|
||||
</ul>
|
||||
</nav>
|
||||
|
||||
|
||||
</header>
|
||||
<main>
|
||||
|
||||
<h1>Arrays</h1>
|
||||
|
||||
|
||||
<h2><a href="/tools/yices/">Yices 2</a></h2>
|
||||
|
||||
<h2><a href="/tools/z3/">Z3</a></h2>
|
||||
|
||||
|
||||
</main>
|
||||
<footer>
|
||||
<p>Copyright 2025. All rights reserved.</p>
|
||||
|
||||
</footer>
|
||||
</body>
|
||||
</html>
|
||||
26
formalisms/arrays/index.xml
Normal file
26
formalisms/arrays/index.xml
Normal file
@@ -0,0 +1,26 @@
|
||||
<?xml version="1.0" encoding="utf-8" standalone="yes"?>
|
||||
<rss version="2.0" xmlns:atom="http://www.w3.org/2005/Atom">
|
||||
<channel>
|
||||
<title>Arrays on Formal Methods Tools</title>
|
||||
<link>http://localhost:1313/formalisms/arrays/</link>
|
||||
<description>Recent content in Arrays on Formal Methods Tools</description>
|
||||
<generator>Hugo</generator>
|
||||
<language>en-us</language>
|
||||
<lastBuildDate>Fri, 02 Feb 2024 04:14:54 -0800</lastBuildDate>
|
||||
<atom:link href="http://localhost:1313/formalisms/arrays/index.xml" rel="self" type="application/rss+xml" />
|
||||
<item>
|
||||
<title>Yices 2</title>
|
||||
<link>http://localhost:1313/tools/yices/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>http://localhost:1313/tools/yices/</guid>
|
||||
<description><p>Yices is a high-performance SMT solver and theorem prover developed by SRI International. It is widely used for checking the satisfiability of logical formulas over various theories, including arithmetic, bit-vectors, arrays, and uninterpreted functions. Yices supports the SMT-LIB standard and its own input language, and provides APIs for several programming languages, making it suitable for integration into formal verification, program analysis, and constraint solving tools.</p>
<h3 id="features">Features</h3>
<ul>
<li><strong>SMT Solver:</strong> Supports a wide range of theories and quantifiers.</li>
<li><strong>Multi-language APIs:</strong> C, OCaml, Python, and more.</li>
<li><strong>Cross-platform:</strong> Available on Windows, Linux, and macOS.</li>
<li><strong>Active development:</strong> Open source and maintained by SRI International.</li>
</ul></description>
|
||||
</item>
|
||||
<item>
|
||||
<title>Z3</title>
|
||||
<link>http://localhost:1313/tools/z3/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>http://localhost:1313/tools/z3/</guid>
|
||||
<description><p>Z3 is a high-performance SMT solver and theorem prover developed by Microsoft Research. It is widely used for checking the satisfiability of logical formulas over various theories, including arithmetic, bit-vectors, arrays, and uninterpreted functions. Z3 supports the SMT-LIB standard and provides APIs for several programming languages, making it suitable for integration into formal verification, program analysis, and constraint solving tools.</p>
<h3 id="features">Features</h3>
<ul>
<li><strong>SMT Solver:</strong> Supports a wide range of theories and quantifiers.</li>
<li><strong>Multi-language APIs:</strong> Python, C++, Java, .NET, and more.</li>
<li><strong>Cross-platform:</strong> Available on Windows, Linux, and macOS.</li>
<li><strong>Active development:</strong> Open source and maintained by Microsoft Research.</li>
<li><strong>Web Playground:</strong> Try Z3 online at <a href="https://rise4fun.com/z3">Rise4Fun</a>.</li>
</ul></description>
|
||||
</item>
|
||||
</channel>
|
||||
</rss>
|
||||
71
formalisms/bit-vectors/index.html
Normal file
71
formalisms/bit-vectors/index.html
Normal file
@@ -0,0 +1,71 @@
|
||||
<!DOCTYPE html>
|
||||
<html lang="en-us" dir="ltr">
|
||||
<head><script src="/livereload.js?mindelay=10&v=2&port=1313&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">
|
||||
<meta http-equiv="X-UA-Compatible" content="IE=edge">
|
||||
<title>Bit-Vectors | Formal Methods Tools</title>
|
||||
|
||||
|
||||
<meta name="keywords" content="Formal Methods Tools">
|
||||
<meta property="og:locale" content='en_US'>
|
||||
<meta property="og:type" content="article">
|
||||
<meta property="og:title" content="Bit-Vectors">
|
||||
<meta property="og:description" content="">
|
||||
<meta property="og:url" content="http://localhost:1313/formalisms/bit-vectors/">
|
||||
<meta property="og:image" content="images/%!s(<nil>)">
|
||||
<link rel="canonical" href="http://localhost:1313/formalisms/bit-vectors/">
|
||||
|
||||
<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="http://localhost:1313/css/styles.e3fcfb3452c69d09414fe512e9dca31d879e4a6c47d23010fbb07eb6693d447f645d3bd2d021c0d28d0f7b4fe6f32a10e599488cdb16c6750a9a126788131917.css" integrity="sha512-4/z7NFLGnQlBT+US6dyjHYeeSmxH0jAQ+7B+tmk9RH9kXTvS0CHA0o0Pe0/m8yoQ5ZlIjNsWxnUKmhJniBMZFw==">
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</head>
|
||||
<body>
|
||||
<header>
|
||||
<h1><a href="/">Formal Methods Tools</a></h1>
|
||||
|
||||
<nav>
|
||||
<ul>
|
||||
<li>
|
||||
<a href="/">Home</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/tools/">Tools</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/taxonomies/">Taxonomies</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/about/">About</a>
|
||||
</li>
|
||||
</ul>
|
||||
</nav>
|
||||
|
||||
|
||||
</header>
|
||||
<main>
|
||||
|
||||
<h1>Bit-Vectors</h1>
|
||||
|
||||
|
||||
<h2><a href="/tools/yices/">Yices 2</a></h2>
|
||||
|
||||
<h2><a href="/tools/z3/">Z3</a></h2>
|
||||
|
||||
|
||||
</main>
|
||||
<footer>
|
||||
<p>Copyright 2025. All rights reserved.</p>
|
||||
|
||||
</footer>
|
||||
</body>
|
||||
</html>
|
||||
26
formalisms/bit-vectors/index.xml
Normal file
26
formalisms/bit-vectors/index.xml
Normal file
@@ -0,0 +1,26 @@
|
||||
<?xml version="1.0" encoding="utf-8" standalone="yes"?>
|
||||
<rss version="2.0" xmlns:atom="http://www.w3.org/2005/Atom">
|
||||
<channel>
|
||||
<title>Bit-Vectors on Formal Methods Tools</title>
|
||||
<link>http://localhost:1313/formalisms/bit-vectors/</link>
|
||||
<description>Recent content in Bit-Vectors on Formal Methods Tools</description>
|
||||
<generator>Hugo</generator>
|
||||
<language>en-us</language>
|
||||
<lastBuildDate>Fri, 02 Feb 2024 04:14:54 -0800</lastBuildDate>
|
||||
<atom:link href="http://localhost:1313/formalisms/bit-vectors/index.xml" rel="self" type="application/rss+xml" />
|
||||
<item>
|
||||
<title>Yices 2</title>
|
||||
<link>http://localhost:1313/tools/yices/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>http://localhost:1313/tools/yices/</guid>
|
||||
<description><p>Yices is a high-performance SMT solver and theorem prover developed by SRI International. It is widely used for checking the satisfiability of logical formulas over various theories, including arithmetic, bit-vectors, arrays, and uninterpreted functions. Yices supports the SMT-LIB standard and its own input language, and provides APIs for several programming languages, making it suitable for integration into formal verification, program analysis, and constraint solving tools.</p>
<h3 id="features">Features</h3>
<ul>
<li><strong>SMT Solver:</strong> Supports a wide range of theories and quantifiers.</li>
<li><strong>Multi-language APIs:</strong> C, OCaml, Python, and more.</li>
<li><strong>Cross-platform:</strong> Available on Windows, Linux, and macOS.</li>
<li><strong>Active development:</strong> Open source and maintained by SRI International.</li>
</ul></description>
|
||||
</item>
|
||||
<item>
|
||||
<title>Z3</title>
|
||||
<link>http://localhost:1313/tools/z3/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>http://localhost:1313/tools/z3/</guid>
|
||||
<description><p>Z3 is a high-performance SMT solver and theorem prover developed by Microsoft Research. It is widely used for checking the satisfiability of logical formulas over various theories, including arithmetic, bit-vectors, arrays, and uninterpreted functions. Z3 supports the SMT-LIB standard and provides APIs for several programming languages, making it suitable for integration into formal verification, program analysis, and constraint solving tools.</p>
<h3 id="features">Features</h3>
<ul>
<li><strong>SMT Solver:</strong> Supports a wide range of theories and quantifiers.</li>
<li><strong>Multi-language APIs:</strong> Python, C++, Java, .NET, and more.</li>
<li><strong>Cross-platform:</strong> Available on Windows, Linux, and macOS.</li>
<li><strong>Active development:</strong> Open source and maintained by Microsoft Research.</li>
<li><strong>Web Playground:</strong> Try Z3 online at <a href="https://rise4fun.com/z3">Rise4Fun</a>.</li>
</ul></description>
|
||||
</item>
|
||||
</channel>
|
||||
</rss>
|
||||
71
formalisms/first-order-logic/index.html
Normal file
71
formalisms/first-order-logic/index.html
Normal file
@@ -0,0 +1,71 @@
|
||||
<!DOCTYPE html>
|
||||
<html lang="en-us" dir="ltr">
|
||||
<head><script src="/livereload.js?mindelay=10&v=2&port=1313&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">
|
||||
<meta http-equiv="X-UA-Compatible" content="IE=edge">
|
||||
<title>First-Order Logic | Formal Methods Tools</title>
|
||||
|
||||
|
||||
<meta name="keywords" content="Formal Methods Tools">
|
||||
<meta property="og:locale" content='en_US'>
|
||||
<meta property="og:type" content="article">
|
||||
<meta property="og:title" content="First-Order Logic">
|
||||
<meta property="og:description" content="">
|
||||
<meta property="og:url" content="http://localhost:1313/formalisms/first-order-logic/">
|
||||
<meta property="og:image" content="images/%!s(<nil>)">
|
||||
<link rel="canonical" href="http://localhost:1313/formalisms/first-order-logic/">
|
||||
|
||||
<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="http://localhost:1313/css/styles.e3fcfb3452c69d09414fe512e9dca31d879e4a6c47d23010fbb07eb6693d447f645d3bd2d021c0d28d0f7b4fe6f32a10e599488cdb16c6750a9a126788131917.css" integrity="sha512-4/z7NFLGnQlBT+US6dyjHYeeSmxH0jAQ+7B+tmk9RH9kXTvS0CHA0o0Pe0/m8yoQ5ZlIjNsWxnUKmhJniBMZFw==">
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</head>
|
||||
<body>
|
||||
<header>
|
||||
<h1><a href="/">Formal Methods Tools</a></h1>
|
||||
|
||||
<nav>
|
||||
<ul>
|
||||
<li>
|
||||
<a href="/">Home</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/tools/">Tools</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/taxonomies/">Taxonomies</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/about/">About</a>
|
||||
</li>
|
||||
</ul>
|
||||
</nav>
|
||||
|
||||
|
||||
</header>
|
||||
<main>
|
||||
|
||||
<h1>First-Order Logic</h1>
|
||||
|
||||
|
||||
<h2><a href="/tools/yices/">Yices 2</a></h2>
|
||||
|
||||
<h2><a href="/tools/z3/">Z3</a></h2>
|
||||
|
||||
|
||||
</main>
|
||||
<footer>
|
||||
<p>Copyright 2025. All rights reserved.</p>
|
||||
|
||||
</footer>
|
||||
</body>
|
||||
</html>
|
||||
26
formalisms/first-order-logic/index.xml
Normal file
26
formalisms/first-order-logic/index.xml
Normal file
@@ -0,0 +1,26 @@
|
||||
<?xml version="1.0" encoding="utf-8" standalone="yes"?>
|
||||
<rss version="2.0" xmlns:atom="http://www.w3.org/2005/Atom">
|
||||
<channel>
|
||||
<title>First-Order Logic on Formal Methods Tools</title>
|
||||
<link>http://localhost:1313/formalisms/first-order-logic/</link>
|
||||
<description>Recent content in First-Order Logic on Formal Methods Tools</description>
|
||||
<generator>Hugo</generator>
|
||||
<language>en-us</language>
|
||||
<lastBuildDate>Fri, 02 Feb 2024 04:14:54 -0800</lastBuildDate>
|
||||
<atom:link href="http://localhost:1313/formalisms/first-order-logic/index.xml" rel="self" type="application/rss+xml" />
|
||||
<item>
|
||||
<title>Yices 2</title>
|
||||
<link>http://localhost:1313/tools/yices/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>http://localhost:1313/tools/yices/</guid>
|
||||
<description><p>Yices is a high-performance SMT solver and theorem prover developed by SRI International. It is widely used for checking the satisfiability of logical formulas over various theories, including arithmetic, bit-vectors, arrays, and uninterpreted functions. Yices supports the SMT-LIB standard and its own input language, and provides APIs for several programming languages, making it suitable for integration into formal verification, program analysis, and constraint solving tools.</p>
<h3 id="features">Features</h3>
<ul>
<li><strong>SMT Solver:</strong> Supports a wide range of theories and quantifiers.</li>
<li><strong>Multi-language APIs:</strong> C, OCaml, Python, and more.</li>
<li><strong>Cross-platform:</strong> Available on Windows, Linux, and macOS.</li>
<li><strong>Active development:</strong> Open source and maintained by SRI International.</li>
</ul></description>
|
||||
</item>
|
||||
<item>
|
||||
<title>Z3</title>
|
||||
<link>http://localhost:1313/tools/z3/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>http://localhost:1313/tools/z3/</guid>
|
||||
<description><p>Z3 is a high-performance SMT solver and theorem prover developed by Microsoft Research. It is widely used for checking the satisfiability of logical formulas over various theories, including arithmetic, bit-vectors, arrays, and uninterpreted functions. Z3 supports the SMT-LIB standard and provides APIs for several programming languages, making it suitable for integration into formal verification, program analysis, and constraint solving tools.</p>
<h3 id="features">Features</h3>
<ul>
<li><strong>SMT Solver:</strong> Supports a wide range of theories and quantifiers.</li>
<li><strong>Multi-language APIs:</strong> Python, C++, Java, .NET, and more.</li>
<li><strong>Cross-platform:</strong> Available on Windows, Linux, and macOS.</li>
<li><strong>Active development:</strong> Open source and maintained by Microsoft Research.</li>
<li><strong>Web Playground:</strong> Try Z3 online at <a href="https://rise4fun.com/z3">Rise4Fun</a>.</li>
</ul></description>
|
||||
</item>
|
||||
</channel>
|
||||
</rss>
|
||||
@@ -1,6 +1,6 @@
|
||||
<!DOCTYPE html>
|
||||
<html lang="en-us" dir="ltr">
|
||||
<head>
|
||||
<head><script src="/livereload.js?mindelay=10&v=2&port=1313&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">
|
||||
@@ -13,16 +13,16 @@
|
||||
<meta property="og:type" content="article">
|
||||
<meta property="og:title" content="Formalisms">
|
||||
<meta property="og:description" content="">
|
||||
<meta property="og:url" content="https://example.org/formalisms/">
|
||||
<meta property="og:url" content="http://localhost:1313/formalisms/">
|
||||
<meta property="og:image" content="images/%!s(<nil>)">
|
||||
<link rel="canonical" href="https://example.org/formalisms/">
|
||||
<link rel="canonical" href="http://localhost:1313/formalisms/">
|
||||
|
||||
<link rel="apple-touch-icon" sizes="180x180" href='https://example.org/apple-touch-icon.png'>
|
||||
<link rel="icon" type="image/png" sizes="32x32" href='https://example.org/favicon-32x32.png'>
|
||||
<link rel="icon" type="image/png" sizes='16x16' href='https://example.org/favicon-16x16.png'>
|
||||
<link rel="manifest" href='https://example.org/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://example.org/css/styles.fc7cf65388be07f2e53293132dd0220e34d9861f57de4b336d64dd03a3502a9befbea05606442d0a501005442835a864361b9a51b4b51acbf28df37530f61f31.css" integrity="sha512-/Hz2U4i+B/LlMpMTLdAiDjTZhh9X3kszbWTdA6NQKpvvvqBWBkQtClAQBUQoNahkNhuaUbS1GsvyjfN1MPYfMQ==">
|
||||
<link rel="stylesheet" href="http://localhost:1313/css/styles.e3fcfb3452c69d09414fe512e9dca31d879e4a6c47d23010fbb07eb6693d447f645d3bd2d021c0d28d0f7b4fe6f32a10e599488cdb16c6750a9a126788131917.css" integrity="sha512-4/z7NFLGnQlBT+US6dyjHYeeSmxH0jAQ+7B+tmk9RH9kXTvS0CHA0o0Pe0/m8yoQ5ZlIjNsWxnUKmhJniBMZFw==">
|
||||
|
||||
|
||||
|
||||
@@ -70,10 +70,118 @@
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="formalisms_tttt"
|
||||
style="background:rgba(229,115,100,0.4)"
|
||||
href="/formalisms/tttt">
|
||||
Tttt
|
||||
id="formalisms_arithmetic"
|
||||
style="background:rgba(155,143,9,0.4)"
|
||||
href="/formalisms/arithmetic">
|
||||
Arithmetic
|
||||
</a>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="formalisms_arrays"
|
||||
style="background:rgba(255,67,184,0.4)"
|
||||
href="/formalisms/arrays">
|
||||
Arrays
|
||||
</a>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="formalisms_bit-vectors"
|
||||
style="background:rgba(208,146,168,0.4)"
|
||||
href="/formalisms/bit-vectors">
|
||||
Bit-Vectors
|
||||
</a>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="formalisms_first-order-logic"
|
||||
style="background:rgba(134,17,227,0.4)"
|
||||
href="/formalisms/first-order-logic">
|
||||
First-Order Logic
|
||||
</a>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="formalisms_quantifier-logic"
|
||||
style="background:rgba(79,36,129,0.4)"
|
||||
href="/formalisms/quantifier-logic">
|
||||
Quantifier Logic
|
||||
</a>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="formalisms_smt-lib"
|
||||
style="background:rgba(62,225,228,0.4)"
|
||||
href="/formalisms/smt-lib">
|
||||
SMT-LIB
|
||||
</a>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="formalisms_uninterpreted-functions"
|
||||
style="background:rgba(11,45,80,0.4)"
|
||||
href="/formalisms/uninterpreted-functions">
|
||||
Uninterpreted Functions
|
||||
</a>
|
||||
|
||||
|
||||
|
||||
@@ -2,17 +2,59 @@
|
||||
<rss version="2.0" xmlns:atom="http://www.w3.org/2005/Atom">
|
||||
<channel>
|
||||
<title>Formalisms on Formal Methods Tools</title>
|
||||
<link>https://example.org/formalisms/</link>
|
||||
<link>http://localhost:1313/formalisms/</link>
|
||||
<description>Recent content in Formalisms on Formal Methods Tools</description>
|
||||
<generator>Hugo</generator>
|
||||
<language>en-us</language>
|
||||
<lastBuildDate>Fri, 02 Feb 2024 04:14:54 -0800</lastBuildDate>
|
||||
<atom:link href="https://example.org/formalisms/index.xml" rel="self" type="application/rss+xml" />
|
||||
<atom:link href="http://localhost:1313/formalisms/index.xml" rel="self" type="application/rss+xml" />
|
||||
<item>
|
||||
<title>Tttt</title>
|
||||
<link>https://example.org/formalisms/tttt/</link>
|
||||
<title>Arithmetic</title>
|
||||
<link>http://localhost:1313/formalisms/arithmetic/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>https://example.org/formalisms/tttt/</guid>
|
||||
<guid>http://localhost:1313/formalisms/arithmetic/</guid>
|
||||
<description></description>
|
||||
</item>
|
||||
<item>
|
||||
<title>Arrays</title>
|
||||
<link>http://localhost:1313/formalisms/arrays/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>http://localhost:1313/formalisms/arrays/</guid>
|
||||
<description></description>
|
||||
</item>
|
||||
<item>
|
||||
<title>Bit-Vectors</title>
|
||||
<link>http://localhost:1313/formalisms/bit-vectors/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>http://localhost:1313/formalisms/bit-vectors/</guid>
|
||||
<description></description>
|
||||
</item>
|
||||
<item>
|
||||
<title>First-Order Logic</title>
|
||||
<link>http://localhost:1313/formalisms/first-order-logic/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>http://localhost:1313/formalisms/first-order-logic/</guid>
|
||||
<description></description>
|
||||
</item>
|
||||
<item>
|
||||
<title>Quantifier Logic</title>
|
||||
<link>http://localhost:1313/formalisms/quantifier-logic/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>http://localhost:1313/formalisms/quantifier-logic/</guid>
|
||||
<description></description>
|
||||
</item>
|
||||
<item>
|
||||
<title>SMT-LIB</title>
|
||||
<link>http://localhost:1313/formalisms/smt-lib/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>http://localhost:1313/formalisms/smt-lib/</guid>
|
||||
<description></description>
|
||||
</item>
|
||||
<item>
|
||||
<title>Uninterpreted Functions</title>
|
||||
<link>http://localhost:1313/formalisms/uninterpreted-functions/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>http://localhost:1313/formalisms/uninterpreted-functions/</guid>
|
||||
<description></description>
|
||||
</item>
|
||||
</channel>
|
||||
|
||||
71
formalisms/quantifier-logic/index.html
Normal file
71
formalisms/quantifier-logic/index.html
Normal file
@@ -0,0 +1,71 @@
|
||||
<!DOCTYPE html>
|
||||
<html lang="en-us" dir="ltr">
|
||||
<head><script src="/livereload.js?mindelay=10&v=2&port=1313&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">
|
||||
<meta http-equiv="X-UA-Compatible" content="IE=edge">
|
||||
<title>Quantifier Logic | Formal Methods Tools</title>
|
||||
|
||||
|
||||
<meta name="keywords" content="Formal Methods Tools">
|
||||
<meta property="og:locale" content='en_US'>
|
||||
<meta property="og:type" content="article">
|
||||
<meta property="og:title" content="Quantifier Logic">
|
||||
<meta property="og:description" content="">
|
||||
<meta property="og:url" content="http://localhost:1313/formalisms/quantifier-logic/">
|
||||
<meta property="og:image" content="images/%!s(<nil>)">
|
||||
<link rel="canonical" href="http://localhost:1313/formalisms/quantifier-logic/">
|
||||
|
||||
<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="http://localhost:1313/css/styles.e3fcfb3452c69d09414fe512e9dca31d879e4a6c47d23010fbb07eb6693d447f645d3bd2d021c0d28d0f7b4fe6f32a10e599488cdb16c6750a9a126788131917.css" integrity="sha512-4/z7NFLGnQlBT+US6dyjHYeeSmxH0jAQ+7B+tmk9RH9kXTvS0CHA0o0Pe0/m8yoQ5ZlIjNsWxnUKmhJniBMZFw==">
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</head>
|
||||
<body>
|
||||
<header>
|
||||
<h1><a href="/">Formal Methods Tools</a></h1>
|
||||
|
||||
<nav>
|
||||
<ul>
|
||||
<li>
|
||||
<a href="/">Home</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/tools/">Tools</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/taxonomies/">Taxonomies</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/about/">About</a>
|
||||
</li>
|
||||
</ul>
|
||||
</nav>
|
||||
|
||||
|
||||
</header>
|
||||
<main>
|
||||
|
||||
<h1>Quantifier Logic</h1>
|
||||
|
||||
|
||||
<h2><a href="/tools/yices/">Yices 2</a></h2>
|
||||
|
||||
<h2><a href="/tools/z3/">Z3</a></h2>
|
||||
|
||||
|
||||
</main>
|
||||
<footer>
|
||||
<p>Copyright 2025. All rights reserved.</p>
|
||||
|
||||
</footer>
|
||||
</body>
|
||||
</html>
|
||||
26
formalisms/quantifier-logic/index.xml
Normal file
26
formalisms/quantifier-logic/index.xml
Normal file
@@ -0,0 +1,26 @@
|
||||
<?xml version="1.0" encoding="utf-8" standalone="yes"?>
|
||||
<rss version="2.0" xmlns:atom="http://www.w3.org/2005/Atom">
|
||||
<channel>
|
||||
<title>Quantifier Logic on Formal Methods Tools</title>
|
||||
<link>http://localhost:1313/formalisms/quantifier-logic/</link>
|
||||
<description>Recent content in Quantifier Logic on Formal Methods Tools</description>
|
||||
<generator>Hugo</generator>
|
||||
<language>en-us</language>
|
||||
<lastBuildDate>Fri, 02 Feb 2024 04:14:54 -0800</lastBuildDate>
|
||||
<atom:link href="http://localhost:1313/formalisms/quantifier-logic/index.xml" rel="self" type="application/rss+xml" />
|
||||
<item>
|
||||
<title>Yices 2</title>
|
||||
<link>http://localhost:1313/tools/yices/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>http://localhost:1313/tools/yices/</guid>
|
||||
<description><p>Yices is a high-performance SMT solver and theorem prover developed by SRI International. It is widely used for checking the satisfiability of logical formulas over various theories, including arithmetic, bit-vectors, arrays, and uninterpreted functions. Yices supports the SMT-LIB standard and its own input language, and provides APIs for several programming languages, making it suitable for integration into formal verification, program analysis, and constraint solving tools.</p>
<h3 id="features">Features</h3>
<ul>
<li><strong>SMT Solver:</strong> Supports a wide range of theories and quantifiers.</li>
<li><strong>Multi-language APIs:</strong> C, OCaml, Python, and more.</li>
<li><strong>Cross-platform:</strong> Available on Windows, Linux, and macOS.</li>
<li><strong>Active development:</strong> Open source and maintained by SRI International.</li>
</ul></description>
|
||||
</item>
|
||||
<item>
|
||||
<title>Z3</title>
|
||||
<link>http://localhost:1313/tools/z3/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>http://localhost:1313/tools/z3/</guid>
|
||||
<description><p>Z3 is a high-performance SMT solver and theorem prover developed by Microsoft Research. It is widely used for checking the satisfiability of logical formulas over various theories, including arithmetic, bit-vectors, arrays, and uninterpreted functions. Z3 supports the SMT-LIB standard and provides APIs for several programming languages, making it suitable for integration into formal verification, program analysis, and constraint solving tools.</p>
<h3 id="features">Features</h3>
<ul>
<li><strong>SMT Solver:</strong> Supports a wide range of theories and quantifiers.</li>
<li><strong>Multi-language APIs:</strong> Python, C++, Java, .NET, and more.</li>
<li><strong>Cross-platform:</strong> Available on Windows, Linux, and macOS.</li>
<li><strong>Active development:</strong> Open source and maintained by Microsoft Research.</li>
<li><strong>Web Playground:</strong> Try Z3 online at <a href="https://rise4fun.com/z3">Rise4Fun</a>.</li>
</ul></description>
|
||||
</item>
|
||||
</channel>
|
||||
</rss>
|
||||
71
formalisms/smt-lib/index.html
Normal file
71
formalisms/smt-lib/index.html
Normal file
@@ -0,0 +1,71 @@
|
||||
<!DOCTYPE html>
|
||||
<html lang="en-us" dir="ltr">
|
||||
<head><script src="/livereload.js?mindelay=10&v=2&port=1313&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">
|
||||
<meta http-equiv="X-UA-Compatible" content="IE=edge">
|
||||
<title>SMT-LIB | Formal Methods Tools</title>
|
||||
|
||||
|
||||
<meta name="keywords" content="Formal Methods Tools">
|
||||
<meta property="og:locale" content='en_US'>
|
||||
<meta property="og:type" content="article">
|
||||
<meta property="og:title" content="SMT-LIB">
|
||||
<meta property="og:description" content="">
|
||||
<meta property="og:url" content="http://localhost:1313/formalisms/smt-lib/">
|
||||
<meta property="og:image" content="images/%!s(<nil>)">
|
||||
<link rel="canonical" href="http://localhost:1313/formalisms/smt-lib/">
|
||||
|
||||
<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="http://localhost:1313/css/styles.e3fcfb3452c69d09414fe512e9dca31d879e4a6c47d23010fbb07eb6693d447f645d3bd2d021c0d28d0f7b4fe6f32a10e599488cdb16c6750a9a126788131917.css" integrity="sha512-4/z7NFLGnQlBT+US6dyjHYeeSmxH0jAQ+7B+tmk9RH9kXTvS0CHA0o0Pe0/m8yoQ5ZlIjNsWxnUKmhJniBMZFw==">
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</head>
|
||||
<body>
|
||||
<header>
|
||||
<h1><a href="/">Formal Methods Tools</a></h1>
|
||||
|
||||
<nav>
|
||||
<ul>
|
||||
<li>
|
||||
<a href="/">Home</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/tools/">Tools</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/taxonomies/">Taxonomies</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/about/">About</a>
|
||||
</li>
|
||||
</ul>
|
||||
</nav>
|
||||
|
||||
|
||||
</header>
|
||||
<main>
|
||||
|
||||
<h1>SMT-LIB</h1>
|
||||
|
||||
|
||||
<h2><a href="/tools/yices/">Yices 2</a></h2>
|
||||
|
||||
<h2><a href="/tools/z3/">Z3</a></h2>
|
||||
|
||||
|
||||
</main>
|
||||
<footer>
|
||||
<p>Copyright 2025. All rights reserved.</p>
|
||||
|
||||
</footer>
|
||||
</body>
|
||||
</html>
|
||||
26
formalisms/smt-lib/index.xml
Normal file
26
formalisms/smt-lib/index.xml
Normal file
@@ -0,0 +1,26 @@
|
||||
<?xml version="1.0" encoding="utf-8" standalone="yes"?>
|
||||
<rss version="2.0" xmlns:atom="http://www.w3.org/2005/Atom">
|
||||
<channel>
|
||||
<title>SMT-LIB on Formal Methods Tools</title>
|
||||
<link>http://localhost:1313/formalisms/smt-lib/</link>
|
||||
<description>Recent content in SMT-LIB on Formal Methods Tools</description>
|
||||
<generator>Hugo</generator>
|
||||
<language>en-us</language>
|
||||
<lastBuildDate>Fri, 02 Feb 2024 04:14:54 -0800</lastBuildDate>
|
||||
<atom:link href="http://localhost:1313/formalisms/smt-lib/index.xml" rel="self" type="application/rss+xml" />
|
||||
<item>
|
||||
<title>Yices 2</title>
|
||||
<link>http://localhost:1313/tools/yices/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>http://localhost:1313/tools/yices/</guid>
|
||||
<description><p>Yices is a high-performance SMT solver and theorem prover developed by SRI International. It is widely used for checking the satisfiability of logical formulas over various theories, including arithmetic, bit-vectors, arrays, and uninterpreted functions. Yices supports the SMT-LIB standard and its own input language, and provides APIs for several programming languages, making it suitable for integration into formal verification, program analysis, and constraint solving tools.</p>
<h3 id="features">Features</h3>
<ul>
<li><strong>SMT Solver:</strong> Supports a wide range of theories and quantifiers.</li>
<li><strong>Multi-language APIs:</strong> C, OCaml, Python, and more.</li>
<li><strong>Cross-platform:</strong> Available on Windows, Linux, and macOS.</li>
<li><strong>Active development:</strong> Open source and maintained by SRI International.</li>
</ul></description>
|
||||
</item>
|
||||
<item>
|
||||
<title>Z3</title>
|
||||
<link>http://localhost:1313/tools/z3/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>http://localhost:1313/tools/z3/</guid>
|
||||
<description><p>Z3 is a high-performance SMT solver and theorem prover developed by Microsoft Research. It is widely used for checking the satisfiability of logical formulas over various theories, including arithmetic, bit-vectors, arrays, and uninterpreted functions. Z3 supports the SMT-LIB standard and provides APIs for several programming languages, making it suitable for integration into formal verification, program analysis, and constraint solving tools.</p>
<h3 id="features">Features</h3>
<ul>
<li><strong>SMT Solver:</strong> Supports a wide range of theories and quantifiers.</li>
<li><strong>Multi-language APIs:</strong> Python, C++, Java, .NET, and more.</li>
<li><strong>Cross-platform:</strong> Available on Windows, Linux, and macOS.</li>
<li><strong>Active development:</strong> Open source and maintained by Microsoft Research.</li>
<li><strong>Web Playground:</strong> Try Z3 online at <a href="https://rise4fun.com/z3">Rise4Fun</a>.</li>
</ul></description>
|
||||
</item>
|
||||
</channel>
|
||||
</rss>
|
||||
@@ -1,69 +0,0 @@
|
||||
<!DOCTYPE html>
|
||||
<html lang="en-us" dir="ltr">
|
||||
<head>
|
||||
<meta charset="utf-8">
|
||||
|
||||
<meta name="viewport" content ="width=device-width, initial-scale=1.0, maximum-scale=1.0, user-scalable=no">
|
||||
<meta http-equiv="X-UA-Compatible" content="IE=edge">
|
||||
<title>Tttt | Formal Methods Tools</title>
|
||||
|
||||
|
||||
<meta name="keywords" content="Formal Methods Tools">
|
||||
<meta property="og:locale" content='en_US'>
|
||||
<meta property="og:type" content="article">
|
||||
<meta property="og:title" content="Tttt">
|
||||
<meta property="og:description" content="">
|
||||
<meta property="og:url" content="https://example.org/formalisms/tttt/">
|
||||
<meta property="og:image" content="images/%!s(<nil>)">
|
||||
<link rel="canonical" href="https://example.org/formalisms/tttt/">
|
||||
|
||||
<link rel="apple-touch-icon" sizes="180x180" href='https://example.org/apple-touch-icon.png'>
|
||||
<link rel="icon" type="image/png" sizes="32x32" href='https://example.org/favicon-32x32.png'>
|
||||
<link rel="icon" type="image/png" sizes='16x16' href='https://example.org/favicon-16x16.png'>
|
||||
<link rel="manifest" href='https://example.org/site.webmanifest'>
|
||||
|
||||
<link rel="stylesheet" href="https://example.org/css/styles.fc7cf65388be07f2e53293132dd0220e34d9861f57de4b336d64dd03a3502a9befbea05606442d0a501005442835a864361b9a51b4b51acbf28df37530f61f31.css" integrity="sha512-/Hz2U4i+B/LlMpMTLdAiDjTZhh9X3kszbWTdA6NQKpvvvqBWBkQtClAQBUQoNahkNhuaUbS1GsvyjfN1MPYfMQ==">
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</head>
|
||||
<body>
|
||||
<header>
|
||||
<h1><a href="/">Formal Methods Tools</a></h1>
|
||||
|
||||
<nav>
|
||||
<ul>
|
||||
<li>
|
||||
<a href="/">Home</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/tools/">Tools</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/taxonomies/">Taxonomies</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/about/">About</a>
|
||||
</li>
|
||||
</ul>
|
||||
</nav>
|
||||
|
||||
|
||||
</header>
|
||||
<main>
|
||||
|
||||
<h1>Tttt</h1>
|
||||
|
||||
|
||||
<h2><a href="/tools/z3/">Z3 Theorem Prover</a></h2>
|
||||
|
||||
|
||||
</main>
|
||||
<footer>
|
||||
<p>Copyright 2025. All rights reserved.</p>
|
||||
|
||||
</footer>
|
||||
</body>
|
||||
</html>
|
||||
@@ -1,19 +0,0 @@
|
||||
<?xml version="1.0" encoding="utf-8" standalone="yes"?>
|
||||
<rss version="2.0" xmlns:atom="http://www.w3.org/2005/Atom">
|
||||
<channel>
|
||||
<title>Tttt on Formal Methods Tools</title>
|
||||
<link>https://example.org/formalisms/tttt/</link>
|
||||
<description>Recent content in Tttt on Formal Methods Tools</description>
|
||||
<generator>Hugo</generator>
|
||||
<language>en-us</language>
|
||||
<lastBuildDate>Fri, 02 Feb 2024 04:14:54 -0800</lastBuildDate>
|
||||
<atom:link href="https://example.org/formalisms/tttt/index.xml" rel="self" type="application/rss+xml" />
|
||||
<item>
|
||||
<title>Z3 Theorem Prover</title>
|
||||
<link>https://example.org/tools/z3/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>https://example.org/tools/z3/</guid>
|
||||
<description><p>desc</p></description>
|
||||
</item>
|
||||
</channel>
|
||||
</rss>
|
||||
71
formalisms/uninterpreted-functions/index.html
Normal file
71
formalisms/uninterpreted-functions/index.html
Normal file
@@ -0,0 +1,71 @@
|
||||
<!DOCTYPE html>
|
||||
<html lang="en-us" dir="ltr">
|
||||
<head><script src="/livereload.js?mindelay=10&v=2&port=1313&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">
|
||||
<meta http-equiv="X-UA-Compatible" content="IE=edge">
|
||||
<title>Uninterpreted Functions | Formal Methods Tools</title>
|
||||
|
||||
|
||||
<meta name="keywords" content="Formal Methods Tools">
|
||||
<meta property="og:locale" content='en_US'>
|
||||
<meta property="og:type" content="article">
|
||||
<meta property="og:title" content="Uninterpreted Functions">
|
||||
<meta property="og:description" content="">
|
||||
<meta property="og:url" content="http://localhost:1313/formalisms/uninterpreted-functions/">
|
||||
<meta property="og:image" content="images/%!s(<nil>)">
|
||||
<link rel="canonical" href="http://localhost:1313/formalisms/uninterpreted-functions/">
|
||||
|
||||
<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="http://localhost:1313/css/styles.e3fcfb3452c69d09414fe512e9dca31d879e4a6c47d23010fbb07eb6693d447f645d3bd2d021c0d28d0f7b4fe6f32a10e599488cdb16c6750a9a126788131917.css" integrity="sha512-4/z7NFLGnQlBT+US6dyjHYeeSmxH0jAQ+7B+tmk9RH9kXTvS0CHA0o0Pe0/m8yoQ5ZlIjNsWxnUKmhJniBMZFw==">
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</head>
|
||||
<body>
|
||||
<header>
|
||||
<h1><a href="/">Formal Methods Tools</a></h1>
|
||||
|
||||
<nav>
|
||||
<ul>
|
||||
<li>
|
||||
<a href="/">Home</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/tools/">Tools</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/taxonomies/">Taxonomies</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/about/">About</a>
|
||||
</li>
|
||||
</ul>
|
||||
</nav>
|
||||
|
||||
|
||||
</header>
|
||||
<main>
|
||||
|
||||
<h1>Uninterpreted Functions</h1>
|
||||
|
||||
|
||||
<h2><a href="/tools/yices/">Yices 2</a></h2>
|
||||
|
||||
<h2><a href="/tools/z3/">Z3</a></h2>
|
||||
|
||||
|
||||
</main>
|
||||
<footer>
|
||||
<p>Copyright 2025. All rights reserved.</p>
|
||||
|
||||
</footer>
|
||||
</body>
|
||||
</html>
|
||||
26
formalisms/uninterpreted-functions/index.xml
Normal file
26
formalisms/uninterpreted-functions/index.xml
Normal file
@@ -0,0 +1,26 @@
|
||||
<?xml version="1.0" encoding="utf-8" standalone="yes"?>
|
||||
<rss version="2.0" xmlns:atom="http://www.w3.org/2005/Atom">
|
||||
<channel>
|
||||
<title>Uninterpreted Functions on Formal Methods Tools</title>
|
||||
<link>http://localhost:1313/formalisms/uninterpreted-functions/</link>
|
||||
<description>Recent content in Uninterpreted Functions on Formal Methods Tools</description>
|
||||
<generator>Hugo</generator>
|
||||
<language>en-us</language>
|
||||
<lastBuildDate>Fri, 02 Feb 2024 04:14:54 -0800</lastBuildDate>
|
||||
<atom:link href="http://localhost:1313/formalisms/uninterpreted-functions/index.xml" rel="self" type="application/rss+xml" />
|
||||
<item>
|
||||
<title>Yices 2</title>
|
||||
<link>http://localhost:1313/tools/yices/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>http://localhost:1313/tools/yices/</guid>
|
||||
<description><p>Yices is a high-performance SMT solver and theorem prover developed by SRI International. It is widely used for checking the satisfiability of logical formulas over various theories, including arithmetic, bit-vectors, arrays, and uninterpreted functions. Yices supports the SMT-LIB standard and its own input language, and provides APIs for several programming languages, making it suitable for integration into formal verification, program analysis, and constraint solving tools.</p>
<h3 id="features">Features</h3>
<ul>
<li><strong>SMT Solver:</strong> Supports a wide range of theories and quantifiers.</li>
<li><strong>Multi-language APIs:</strong> C, OCaml, Python, and more.</li>
<li><strong>Cross-platform:</strong> Available on Windows, Linux, and macOS.</li>
<li><strong>Active development:</strong> Open source and maintained by SRI International.</li>
</ul></description>
|
||||
</item>
|
||||
<item>
|
||||
<title>Z3</title>
|
||||
<link>http://localhost:1313/tools/z3/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>http://localhost:1313/tools/z3/</guid>
|
||||
<description><p>Z3 is a high-performance SMT solver and theorem prover developed by Microsoft Research. It is widely used for checking the satisfiability of logical formulas over various theories, including arithmetic, bit-vectors, arrays, and uninterpreted functions. Z3 supports the SMT-LIB standard and provides APIs for several programming languages, making it suitable for integration into formal verification, program analysis, and constraint solving tools.</p>
<h3 id="features">Features</h3>
<ul>
<li><strong>SMT Solver:</strong> Supports a wide range of theories and quantifiers.</li>
<li><strong>Multi-language APIs:</strong> Python, C++, Java, .NET, and more.</li>
<li><strong>Cross-platform:</strong> Available on Windows, Linux, and macOS.</li>
<li><strong>Active development:</strong> Open source and maintained by Microsoft Research.</li>
<li><strong>Web Playground:</strong> Try Z3 online at <a href="https://rise4fun.com/z3">Rise4Fun</a>.</li>
</ul></description>
|
||||
</item>
|
||||
</channel>
|
||||
</rss>
|
||||
26
index.html
26
index.html
@@ -1,7 +1,7 @@
|
||||
<!DOCTYPE html>
|
||||
<html lang="en-us" dir="ltr">
|
||||
<head>
|
||||
<meta name="generator" content="Hugo 0.147.7">
|
||||
<meta name="generator" content="Hugo 0.147.7"><script src="/livereload.js?mindelay=10&v=2&port=1313&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">
|
||||
@@ -15,16 +15,16 @@
|
||||
<meta property="og:title" content="Home">
|
||||
<meta property="og:description" content="Laborum voluptate pariatur ex culpa magna nostrud est incididunt fugiat
|
||||
pariatur do dolor ipsum enim. Consequat tempor do dolor eu. Non id id anim anim">
|
||||
<meta property="og:url" content="https://example.org/">
|
||||
<meta property="og:url" content="http://localhost:1313/">
|
||||
<meta property="og:image" content="images/%!s(<nil>)">
|
||||
<link rel="canonical" href="https://example.org/">
|
||||
<link rel="canonical" href="http://localhost:1313/">
|
||||
|
||||
<link rel="apple-touch-icon" sizes="180x180" href='https://example.org/apple-touch-icon.png'>
|
||||
<link rel="icon" type="image/png" sizes="32x32" href='https://example.org/favicon-32x32.png'>
|
||||
<link rel="icon" type="image/png" sizes='16x16' href='https://example.org/favicon-16x16.png'>
|
||||
<link rel="manifest" href='https://example.org/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://example.org/css/styles.fc7cf65388be07f2e53293132dd0220e34d9861f57de4b336d64dd03a3502a9befbea05606442d0a501005442835a864361b9a51b4b51acbf28df37530f61f31.css" integrity="sha512-/Hz2U4i+B/LlMpMTLdAiDjTZhh9X3kszbWTdA6NQKpvvvqBWBkQtClAQBUQoNahkNhuaUbS1GsvyjfN1MPYfMQ==">
|
||||
<link rel="stylesheet" href="http://localhost:1313/css/styles.e3fcfb3452c69d09414fe512e9dca31d879e4a6c47d23010fbb07eb6693d447f645d3bd2d021c0d28d0f7b4fe6f32a10e599488cdb16c6750a9a126788131917.css" integrity="sha512-4/z7NFLGnQlBT+US6dyjHYeeSmxH0jAQ+7B+tmk9RH9kXTvS0CHA0o0Pe0/m8yoQ5ZlIjNsWxnUKmhJniBMZFw==">
|
||||
|
||||
|
||||
|
||||
@@ -65,9 +65,13 @@ excepteur excepteur pariatur nostrud qui irure ullamco.</p>
|
||||
<h2>Featured Tools</h2>
|
||||
|
||||
<article>
|
||||
<h3><a href="/tools/z3/">Z3 Theorem Prover</a></h3>
|
||||
<p><p>desc</p>
|
||||
</p>
|
||||
<h3><a href="/tools/z3/">Z3</a></h3>
|
||||
<p><p>Z3 is a high-performance SMT solver and theorem prover developed by Microsoft Research. It is widely …</p></p>
|
||||
</article>
|
||||
|
||||
<article>
|
||||
<h3><a href="/tools/yices/">Yices 2</a></h3>
|
||||
<p><p>Yices is a high-performance SMT solver and theorem prover developed by SRI International. It is …</p></p>
|
||||
</article>
|
||||
|
||||
</section>
|
||||
|
||||
19
index.xml
19
index.xml
@@ -2,18 +2,25 @@
|
||||
<rss version="2.0" xmlns:atom="http://www.w3.org/2005/Atom">
|
||||
<channel>
|
||||
<title>Home on Formal Methods Tools</title>
|
||||
<link>https://example.org/</link>
|
||||
<link>http://localhost:1313/</link>
|
||||
<description>Recent content in Home on Formal Methods Tools</description>
|
||||
<generator>Hugo</generator>
|
||||
<language>en-us</language>
|
||||
<lastBuildDate>Fri, 02 Feb 2024 04:14:54 -0800</lastBuildDate>
|
||||
<atom:link href="https://example.org/index.xml" rel="self" type="application/rss+xml" />
|
||||
<atom:link href="http://localhost:1313/index.xml" rel="self" type="application/rss+xml" />
|
||||
<item>
|
||||
<title>Z3 Theorem Prover</title>
|
||||
<link>https://example.org/tools/z3/</link>
|
||||
<title>Yices 2</title>
|
||||
<link>http://localhost:1313/tools/yices/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>https://example.org/tools/z3/</guid>
|
||||
<description><p>desc</p></description>
|
||||
<guid>http://localhost:1313/tools/yices/</guid>
|
||||
<description><p>Yices is a high-performance SMT solver and theorem prover developed by SRI International. It is widely used for checking the satisfiability of logical formulas over various theories, including arithmetic, bit-vectors, arrays, and uninterpreted functions. Yices supports the SMT-LIB standard and its own input language, and provides APIs for several programming languages, making it suitable for integration into formal verification, program analysis, and constraint solving tools.</p>
<h3 id="features">Features</h3>
<ul>
<li><strong>SMT Solver:</strong> Supports a wide range of theories and quantifiers.</li>
<li><strong>Multi-language APIs:</strong> C, OCaml, Python, and more.</li>
<li><strong>Cross-platform:</strong> Available on Windows, Linux, and macOS.</li>
<li><strong>Active development:</strong> Open source and maintained by SRI International.</li>
</ul></description>
|
||||
</item>
|
||||
<item>
|
||||
<title>Z3</title>
|
||||
<link>http://localhost:1313/tools/z3/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>http://localhost:1313/tools/z3/</guid>
|
||||
<description><p>Z3 is a high-performance SMT solver and theorem prover developed by Microsoft Research. It is widely used for checking the satisfiability of logical formulas over various theories, including arithmetic, bit-vectors, arrays, and uninterpreted functions. Z3 supports the SMT-LIB standard and provides APIs for several programming languages, making it suitable for integration into formal verification, program analysis, and constraint solving tools.</p>
<h3 id="features">Features</h3>
<ul>
<li><strong>SMT Solver:</strong> Supports a wide range of theories and quantifiers.</li>
<li><strong>Multi-language APIs:</strong> Python, C++, Java, .NET, and more.</li>
<li><strong>Cross-platform:</strong> Available on Windows, Linux, and macOS.</li>
<li><strong>Active development:</strong> Open source and maintained by Microsoft Research.</li>
<li><strong>Web Playground:</strong> Try Z3 online at <a href="https://rise4fun.com/z3">Rise4Fun</a>.</li>
</ul></description>
|
||||
</item>
|
||||
</channel>
|
||||
</rss>
|
||||
|
||||
@@ -1,69 +0,0 @@
|
||||
<!DOCTYPE html>
|
||||
<html lang="en-us" dir="ltr">
|
||||
<head>
|
||||
<meta charset="utf-8">
|
||||
|
||||
<meta name="viewport" content ="width=device-width, initial-scale=1.0, maximum-scale=1.0, user-scalable=no">
|
||||
<meta http-equiv="X-UA-Compatible" content="IE=edge">
|
||||
<title>Araafafanpoasi | Formal Methods Tools</title>
|
||||
|
||||
|
||||
<meta name="keywords" content="Formal Methods Tools">
|
||||
<meta property="og:locale" content='en_US'>
|
||||
<meta property="og:type" content="article">
|
||||
<meta property="og:title" content="Araafafanpoasi">
|
||||
<meta property="og:description" content="">
|
||||
<meta property="og:url" content="https://example.org/interactions/araafafanpoasi/">
|
||||
<meta property="og:image" content="images/%!s(<nil>)">
|
||||
<link rel="canonical" href="https://example.org/interactions/araafafanpoasi/">
|
||||
|
||||
<link rel="apple-touch-icon" sizes="180x180" href='https://example.org/apple-touch-icon.png'>
|
||||
<link rel="icon" type="image/png" sizes="32x32" href='https://example.org/favicon-32x32.png'>
|
||||
<link rel="icon" type="image/png" sizes='16x16' href='https://example.org/favicon-16x16.png'>
|
||||
<link rel="manifest" href='https://example.org/site.webmanifest'>
|
||||
|
||||
<link rel="stylesheet" href="https://example.org/css/styles.fc7cf65388be07f2e53293132dd0220e34d9861f57de4b336d64dd03a3502a9befbea05606442d0a501005442835a864361b9a51b4b51acbf28df37530f61f31.css" integrity="sha512-/Hz2U4i+B/LlMpMTLdAiDjTZhh9X3kszbWTdA6NQKpvvvqBWBkQtClAQBUQoNahkNhuaUbS1GsvyjfN1MPYfMQ==">
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</head>
|
||||
<body>
|
||||
<header>
|
||||
<h1><a href="/">Formal Methods Tools</a></h1>
|
||||
|
||||
<nav>
|
||||
<ul>
|
||||
<li>
|
||||
<a href="/">Home</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/tools/">Tools</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/taxonomies/">Taxonomies</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/about/">About</a>
|
||||
</li>
|
||||
</ul>
|
||||
</nav>
|
||||
|
||||
|
||||
</header>
|
||||
<main>
|
||||
|
||||
<h1>Araafafanpoasi</h1>
|
||||
|
||||
|
||||
<h2><a href="/tools/z3/">Z3 Theorem Prover</a></h2>
|
||||
|
||||
|
||||
</main>
|
||||
<footer>
|
||||
<p>Copyright 2025. All rights reserved.</p>
|
||||
|
||||
</footer>
|
||||
</body>
|
||||
</html>
|
||||
@@ -1,19 +0,0 @@
|
||||
<?xml version="1.0" encoding="utf-8" standalone="yes"?>
|
||||
<rss version="2.0" xmlns:atom="http://www.w3.org/2005/Atom">
|
||||
<channel>
|
||||
<title>Araafafanpoasi on Formal Methods Tools</title>
|
||||
<link>https://example.org/interactions/araafafanpoasi/</link>
|
||||
<description>Recent content in Araafafanpoasi on Formal Methods Tools</description>
|
||||
<generator>Hugo</generator>
|
||||
<language>en-us</language>
|
||||
<lastBuildDate>Fri, 02 Feb 2024 04:14:54 -0800</lastBuildDate>
|
||||
<atom:link href="https://example.org/interactions/araafafanpoasi/index.xml" rel="self" type="application/rss+xml" />
|
||||
<item>
|
||||
<title>Z3 Theorem Prover</title>
|
||||
<link>https://example.org/tools/z3/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>https://example.org/tools/z3/</guid>
|
||||
<description><p>desc</p></description>
|
||||
</item>
|
||||
</channel>
|
||||
</rss>
|
||||
@@ -1,69 +0,0 @@
|
||||
<!DOCTYPE html>
|
||||
<html lang="en-us" dir="ltr">
|
||||
<head>
|
||||
<meta charset="utf-8">
|
||||
|
||||
<meta name="viewport" content ="width=device-width, initial-scale=1.0, maximum-scale=1.0, user-scalable=no">
|
||||
<meta http-equiv="X-UA-Compatible" content="IE=edge">
|
||||
<title>Aranapoasi | Formal Methods Tools</title>
|
||||
|
||||
|
||||
<meta name="keywords" content="Formal Methods Tools">
|
||||
<meta property="og:locale" content='en_US'>
|
||||
<meta property="og:type" content="article">
|
||||
<meta property="og:title" content="Aranapoasi">
|
||||
<meta property="og:description" content="">
|
||||
<meta property="og:url" content="https://example.org/interactions/aranapoasi/">
|
||||
<meta property="og:image" content="images/%!s(<nil>)">
|
||||
<link rel="canonical" href="https://example.org/interactions/aranapoasi/">
|
||||
|
||||
<link rel="apple-touch-icon" sizes="180x180" href='https://example.org/apple-touch-icon.png'>
|
||||
<link rel="icon" type="image/png" sizes="32x32" href='https://example.org/favicon-32x32.png'>
|
||||
<link rel="icon" type="image/png" sizes='16x16' href='https://example.org/favicon-16x16.png'>
|
||||
<link rel="manifest" href='https://example.org/site.webmanifest'>
|
||||
|
||||
<link rel="stylesheet" href="https://example.org/css/styles.fc7cf65388be07f2e53293132dd0220e34d9861f57de4b336d64dd03a3502a9befbea05606442d0a501005442835a864361b9a51b4b51acbf28df37530f61f31.css" integrity="sha512-/Hz2U4i+B/LlMpMTLdAiDjTZhh9X3kszbWTdA6NQKpvvvqBWBkQtClAQBUQoNahkNhuaUbS1GsvyjfN1MPYfMQ==">
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</head>
|
||||
<body>
|
||||
<header>
|
||||
<h1><a href="/">Formal Methods Tools</a></h1>
|
||||
|
||||
<nav>
|
||||
<ul>
|
||||
<li>
|
||||
<a href="/">Home</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/tools/">Tools</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/taxonomies/">Taxonomies</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/about/">About</a>
|
||||
</li>
|
||||
</ul>
|
||||
</nav>
|
||||
|
||||
|
||||
</header>
|
||||
<main>
|
||||
|
||||
<h1>Aranapoasi</h1>
|
||||
|
||||
|
||||
<h2><a href="/tools/z3/">Z3 Theorem Prover</a></h2>
|
||||
|
||||
|
||||
</main>
|
||||
<footer>
|
||||
<p>Copyright 2025. All rights reserved.</p>
|
||||
|
||||
</footer>
|
||||
</body>
|
||||
</html>
|
||||
@@ -1,19 +0,0 @@
|
||||
<?xml version="1.0" encoding="utf-8" standalone="yes"?>
|
||||
<rss version="2.0" xmlns:atom="http://www.w3.org/2005/Atom">
|
||||
<channel>
|
||||
<title>Aranapoasi on Formal Methods Tools</title>
|
||||
<link>https://example.org/interactions/aranapoasi/</link>
|
||||
<description>Recent content in Aranapoasi on Formal Methods Tools</description>
|
||||
<generator>Hugo</generator>
|
||||
<language>en-us</language>
|
||||
<lastBuildDate>Fri, 02 Feb 2024 04:14:54 -0800</lastBuildDate>
|
||||
<atom:link href="https://example.org/interactions/aranapoasi/index.xml" rel="self" type="application/rss+xml" />
|
||||
<item>
|
||||
<title>Z3 Theorem Prover</title>
|
||||
<link>https://example.org/tools/z3/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>https://example.org/tools/z3/</guid>
|
||||
<description><p>desc</p></description>
|
||||
</item>
|
||||
</channel>
|
||||
</rss>
|
||||
@@ -1,69 +0,0 @@
|
||||
<!DOCTYPE html>
|
||||
<html lang="en-us" dir="ltr">
|
||||
<head>
|
||||
<meta charset="utf-8">
|
||||
|
||||
<meta name="viewport" content ="width=device-width, initial-scale=1.0, maximum-scale=1.0, user-scalable=no">
|
||||
<meta http-equiv="X-UA-Compatible" content="IE=edge">
|
||||
<title>Aranpoasadfsi | Formal Methods Tools</title>
|
||||
|
||||
|
||||
<meta name="keywords" content="Formal Methods Tools">
|
||||
<meta property="og:locale" content='en_US'>
|
||||
<meta property="og:type" content="article">
|
||||
<meta property="og:title" content="Aranpoasadfsi">
|
||||
<meta property="og:description" content="">
|
||||
<meta property="og:url" content="https://example.org/interactions/aranpoasadfsi/">
|
||||
<meta property="og:image" content="images/%!s(<nil>)">
|
||||
<link rel="canonical" href="https://example.org/interactions/aranpoasadfsi/">
|
||||
|
||||
<link rel="apple-touch-icon" sizes="180x180" href='https://example.org/apple-touch-icon.png'>
|
||||
<link rel="icon" type="image/png" sizes="32x32" href='https://example.org/favicon-32x32.png'>
|
||||
<link rel="icon" type="image/png" sizes='16x16' href='https://example.org/favicon-16x16.png'>
|
||||
<link rel="manifest" href='https://example.org/site.webmanifest'>
|
||||
|
||||
<link rel="stylesheet" href="https://example.org/css/styles.fc7cf65388be07f2e53293132dd0220e34d9861f57de4b336d64dd03a3502a9befbea05606442d0a501005442835a864361b9a51b4b51acbf28df37530f61f31.css" integrity="sha512-/Hz2U4i+B/LlMpMTLdAiDjTZhh9X3kszbWTdA6NQKpvvvqBWBkQtClAQBUQoNahkNhuaUbS1GsvyjfN1MPYfMQ==">
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</head>
|
||||
<body>
|
||||
<header>
|
||||
<h1><a href="/">Formal Methods Tools</a></h1>
|
||||
|
||||
<nav>
|
||||
<ul>
|
||||
<li>
|
||||
<a href="/">Home</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/tools/">Tools</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/taxonomies/">Taxonomies</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/about/">About</a>
|
||||
</li>
|
||||
</ul>
|
||||
</nav>
|
||||
|
||||
|
||||
</header>
|
||||
<main>
|
||||
|
||||
<h1>Aranpoasadfsi</h1>
|
||||
|
||||
|
||||
<h2><a href="/tools/z3/">Z3 Theorem Prover</a></h2>
|
||||
|
||||
|
||||
</main>
|
||||
<footer>
|
||||
<p>Copyright 2025. All rights reserved.</p>
|
||||
|
||||
</footer>
|
||||
</body>
|
||||
</html>
|
||||
@@ -1,19 +0,0 @@
|
||||
<?xml version="1.0" encoding="utf-8" standalone="yes"?>
|
||||
<rss version="2.0" xmlns:atom="http://www.w3.org/2005/Atom">
|
||||
<channel>
|
||||
<title>Aranpoasadfsi on Formal Methods Tools</title>
|
||||
<link>https://example.org/interactions/aranpoasadfsi/</link>
|
||||
<description>Recent content in Aranpoasadfsi on Formal Methods Tools</description>
|
||||
<generator>Hugo</generator>
|
||||
<language>en-us</language>
|
||||
<lastBuildDate>Fri, 02 Feb 2024 04:14:54 -0800</lastBuildDate>
|
||||
<atom:link href="https://example.org/interactions/aranpoasadfsi/index.xml" rel="self" type="application/rss+xml" />
|
||||
<item>
|
||||
<title>Z3 Theorem Prover</title>
|
||||
<link>https://example.org/tools/z3/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>https://example.org/tools/z3/</guid>
|
||||
<description><p>desc</p></description>
|
||||
</item>
|
||||
</channel>
|
||||
</rss>
|
||||
@@ -1,69 +0,0 @@
|
||||
<!DOCTYPE html>
|
||||
<html lang="en-us" dir="ltr">
|
||||
<head>
|
||||
<meta charset="utf-8">
|
||||
|
||||
<meta name="viewport" content ="width=device-width, initial-scale=1.0, maximum-scale=1.0, user-scalable=no">
|
||||
<meta http-equiv="X-UA-Compatible" content="IE=edge">
|
||||
<title>Aranpoasai | Formal Methods Tools</title>
|
||||
|
||||
|
||||
<meta name="keywords" content="Formal Methods Tools">
|
||||
<meta property="og:locale" content='en_US'>
|
||||
<meta property="og:type" content="article">
|
||||
<meta property="og:title" content="Aranpoasai">
|
||||
<meta property="og:description" content="">
|
||||
<meta property="og:url" content="https://example.org/interactions/aranpoasai/">
|
||||
<meta property="og:image" content="images/%!s(<nil>)">
|
||||
<link rel="canonical" href="https://example.org/interactions/aranpoasai/">
|
||||
|
||||
<link rel="apple-touch-icon" sizes="180x180" href='https://example.org/apple-touch-icon.png'>
|
||||
<link rel="icon" type="image/png" sizes="32x32" href='https://example.org/favicon-32x32.png'>
|
||||
<link rel="icon" type="image/png" sizes='16x16' href='https://example.org/favicon-16x16.png'>
|
||||
<link rel="manifest" href='https://example.org/site.webmanifest'>
|
||||
|
||||
<link rel="stylesheet" href="https://example.org/css/styles.fc7cf65388be07f2e53293132dd0220e34d9861f57de4b336d64dd03a3502a9befbea05606442d0a501005442835a864361b9a51b4b51acbf28df37530f61f31.css" integrity="sha512-/Hz2U4i+B/LlMpMTLdAiDjTZhh9X3kszbWTdA6NQKpvvvqBWBkQtClAQBUQoNahkNhuaUbS1GsvyjfN1MPYfMQ==">
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</head>
|
||||
<body>
|
||||
<header>
|
||||
<h1><a href="/">Formal Methods Tools</a></h1>
|
||||
|
||||
<nav>
|
||||
<ul>
|
||||
<li>
|
||||
<a href="/">Home</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/tools/">Tools</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/taxonomies/">Taxonomies</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/about/">About</a>
|
||||
</li>
|
||||
</ul>
|
||||
</nav>
|
||||
|
||||
|
||||
</header>
|
||||
<main>
|
||||
|
||||
<h1>Aranpoasai</h1>
|
||||
|
||||
|
||||
<h2><a href="/tools/z3/">Z3 Theorem Prover</a></h2>
|
||||
|
||||
|
||||
</main>
|
||||
<footer>
|
||||
<p>Copyright 2025. All rights reserved.</p>
|
||||
|
||||
</footer>
|
||||
</body>
|
||||
</html>
|
||||
@@ -1,19 +0,0 @@
|
||||
<?xml version="1.0" encoding="utf-8" standalone="yes"?>
|
||||
<rss version="2.0" xmlns:atom="http://www.w3.org/2005/Atom">
|
||||
<channel>
|
||||
<title>Aranpoasai on Formal Methods Tools</title>
|
||||
<link>https://example.org/interactions/aranpoasai/</link>
|
||||
<description>Recent content in Aranpoasai on Formal Methods Tools</description>
|
||||
<generator>Hugo</generator>
|
||||
<language>en-us</language>
|
||||
<lastBuildDate>Fri, 02 Feb 2024 04:14:54 -0800</lastBuildDate>
|
||||
<atom:link href="https://example.org/interactions/aranpoasai/index.xml" rel="self" type="application/rss+xml" />
|
||||
<item>
|
||||
<title>Z3 Theorem Prover</title>
|
||||
<link>https://example.org/tools/z3/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>https://example.org/tools/z3/</guid>
|
||||
<description><p>desc</p></description>
|
||||
</item>
|
||||
</channel>
|
||||
</rss>
|
||||
@@ -1,69 +0,0 @@
|
||||
<!DOCTYPE html>
|
||||
<html lang="en-us" dir="ltr">
|
||||
<head>
|
||||
<meta charset="utf-8">
|
||||
|
||||
<meta name="viewport" content ="width=device-width, initial-scale=1.0, maximum-scale=1.0, user-scalable=no">
|
||||
<meta http-equiv="X-UA-Compatible" content="IE=edge">
|
||||
<title>Aranpoasasdfasfasdfasdfi | Formal Methods Tools</title>
|
||||
|
||||
|
||||
<meta name="keywords" content="Formal Methods Tools">
|
||||
<meta property="og:locale" content='en_US'>
|
||||
<meta property="og:type" content="article">
|
||||
<meta property="og:title" content="Aranpoasasdfasfasdfasdfi">
|
||||
<meta property="og:description" content="">
|
||||
<meta property="og:url" content="https://example.org/interactions/aranpoasasdfasfasdfasdfi/">
|
||||
<meta property="og:image" content="images/%!s(<nil>)">
|
||||
<link rel="canonical" href="https://example.org/interactions/aranpoasasdfasfasdfasdfi/">
|
||||
|
||||
<link rel="apple-touch-icon" sizes="180x180" href='https://example.org/apple-touch-icon.png'>
|
||||
<link rel="icon" type="image/png" sizes="32x32" href='https://example.org/favicon-32x32.png'>
|
||||
<link rel="icon" type="image/png" sizes='16x16' href='https://example.org/favicon-16x16.png'>
|
||||
<link rel="manifest" href='https://example.org/site.webmanifest'>
|
||||
|
||||
<link rel="stylesheet" href="https://example.org/css/styles.fc7cf65388be07f2e53293132dd0220e34d9861f57de4b336d64dd03a3502a9befbea05606442d0a501005442835a864361b9a51b4b51acbf28df37530f61f31.css" integrity="sha512-/Hz2U4i+B/LlMpMTLdAiDjTZhh9X3kszbWTdA6NQKpvvvqBWBkQtClAQBUQoNahkNhuaUbS1GsvyjfN1MPYfMQ==">
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</head>
|
||||
<body>
|
||||
<header>
|
||||
<h1><a href="/">Formal Methods Tools</a></h1>
|
||||
|
||||
<nav>
|
||||
<ul>
|
||||
<li>
|
||||
<a href="/">Home</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/tools/">Tools</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/taxonomies/">Taxonomies</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/about/">About</a>
|
||||
</li>
|
||||
</ul>
|
||||
</nav>
|
||||
|
||||
|
||||
</header>
|
||||
<main>
|
||||
|
||||
<h1>Aranpoasasdfasfasdfasdfi</h1>
|
||||
|
||||
|
||||
<h2><a href="/tools/z3/">Z3 Theorem Prover</a></h2>
|
||||
|
||||
|
||||
</main>
|
||||
<footer>
|
||||
<p>Copyright 2025. All rights reserved.</p>
|
||||
|
||||
</footer>
|
||||
</body>
|
||||
</html>
|
||||
@@ -1,19 +0,0 @@
|
||||
<?xml version="1.0" encoding="utf-8" standalone="yes"?>
|
||||
<rss version="2.0" xmlns:atom="http://www.w3.org/2005/Atom">
|
||||
<channel>
|
||||
<title>Aranpoasasdfasfasdfasdfi on Formal Methods Tools</title>
|
||||
<link>https://example.org/interactions/aranpoasasdfasfasdfasdfi/</link>
|
||||
<description>Recent content in Aranpoasasdfasfasdfasdfi on Formal Methods Tools</description>
|
||||
<generator>Hugo</generator>
|
||||
<language>en-us</language>
|
||||
<lastBuildDate>Fri, 02 Feb 2024 04:14:54 -0800</lastBuildDate>
|
||||
<atom:link href="https://example.org/interactions/aranpoasasdfasfasdfasdfi/index.xml" rel="self" type="application/rss+xml" />
|
||||
<item>
|
||||
<title>Z3 Theorem Prover</title>
|
||||
<link>https://example.org/tools/z3/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>https://example.org/tools/z3/</guid>
|
||||
<description><p>desc</p></description>
|
||||
</item>
|
||||
</channel>
|
||||
</rss>
|
||||
@@ -1,69 +0,0 @@
|
||||
<!DOCTYPE html>
|
||||
<html lang="en-us" dir="ltr">
|
||||
<head>
|
||||
<meta charset="utf-8">
|
||||
|
||||
<meta name="viewport" content ="width=device-width, initial-scale=1.0, maximum-scale=1.0, user-scalable=no">
|
||||
<meta http-equiv="X-UA-Compatible" content="IE=edge">
|
||||
<title>Aranpoasi | Formal Methods Tools</title>
|
||||
|
||||
|
||||
<meta name="keywords" content="Formal Methods Tools">
|
||||
<meta property="og:locale" content='en_US'>
|
||||
<meta property="og:type" content="article">
|
||||
<meta property="og:title" content="Aranpoasi">
|
||||
<meta property="og:description" content="">
|
||||
<meta property="og:url" content="https://example.org/interactions/aranpoasi/">
|
||||
<meta property="og:image" content="images/%!s(<nil>)">
|
||||
<link rel="canonical" href="https://example.org/interactions/aranpoasi/">
|
||||
|
||||
<link rel="apple-touch-icon" sizes="180x180" href='https://example.org/apple-touch-icon.png'>
|
||||
<link rel="icon" type="image/png" sizes="32x32" href='https://example.org/favicon-32x32.png'>
|
||||
<link rel="icon" type="image/png" sizes='16x16' href='https://example.org/favicon-16x16.png'>
|
||||
<link rel="manifest" href='https://example.org/site.webmanifest'>
|
||||
|
||||
<link rel="stylesheet" href="https://example.org/css/styles.fc7cf65388be07f2e53293132dd0220e34d9861f57de4b336d64dd03a3502a9befbea05606442d0a501005442835a864361b9a51b4b51acbf28df37530f61f31.css" integrity="sha512-/Hz2U4i+B/LlMpMTLdAiDjTZhh9X3kszbWTdA6NQKpvvvqBWBkQtClAQBUQoNahkNhuaUbS1GsvyjfN1MPYfMQ==">
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</head>
|
||||
<body>
|
||||
<header>
|
||||
<h1><a href="/">Formal Methods Tools</a></h1>
|
||||
|
||||
<nav>
|
||||
<ul>
|
||||
<li>
|
||||
<a href="/">Home</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/tools/">Tools</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/taxonomies/">Taxonomies</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/about/">About</a>
|
||||
</li>
|
||||
</ul>
|
||||
</nav>
|
||||
|
||||
|
||||
</header>
|
||||
<main>
|
||||
|
||||
<h1>Aranpoasi</h1>
|
||||
|
||||
|
||||
<h2><a href="/tools/z3/">Z3 Theorem Prover</a></h2>
|
||||
|
||||
|
||||
</main>
|
||||
<footer>
|
||||
<p>Copyright 2025. All rights reserved.</p>
|
||||
|
||||
</footer>
|
||||
</body>
|
||||
</html>
|
||||
@@ -1,19 +0,0 @@
|
||||
<?xml version="1.0" encoding="utf-8" standalone="yes"?>
|
||||
<rss version="2.0" xmlns:atom="http://www.w3.org/2005/Atom">
|
||||
<channel>
|
||||
<title>Aranpoasi on Formal Methods Tools</title>
|
||||
<link>https://example.org/interactions/aranpoasi/</link>
|
||||
<description>Recent content in Aranpoasi on Formal Methods Tools</description>
|
||||
<generator>Hugo</generator>
|
||||
<language>en-us</language>
|
||||
<lastBuildDate>Fri, 02 Feb 2024 04:14:54 -0800</lastBuildDate>
|
||||
<atom:link href="https://example.org/interactions/aranpoasi/index.xml" rel="self" type="application/rss+xml" />
|
||||
<item>
|
||||
<title>Z3 Theorem Prover</title>
|
||||
<link>https://example.org/tools/z3/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>https://example.org/tools/z3/</guid>
|
||||
<description><p>desc</p></description>
|
||||
</item>
|
||||
</channel>
|
||||
</rss>
|
||||
@@ -1,69 +0,0 @@
|
||||
<!DOCTYPE html>
|
||||
<html lang="en-us" dir="ltr">
|
||||
<head>
|
||||
<meta charset="utf-8">
|
||||
|
||||
<meta name="viewport" content ="width=device-width, initial-scale=1.0, maximum-scale=1.0, user-scalable=no">
|
||||
<meta http-equiv="X-UA-Compatible" content="IE=edge">
|
||||
<title>Aranpoaswei | Formal Methods Tools</title>
|
||||
|
||||
|
||||
<meta name="keywords" content="Formal Methods Tools">
|
||||
<meta property="og:locale" content='en_US'>
|
||||
<meta property="og:type" content="article">
|
||||
<meta property="og:title" content="Aranpoaswei">
|
||||
<meta property="og:description" content="">
|
||||
<meta property="og:url" content="https://example.org/interactions/aranpoaswei/">
|
||||
<meta property="og:image" content="images/%!s(<nil>)">
|
||||
<link rel="canonical" href="https://example.org/interactions/aranpoaswei/">
|
||||
|
||||
<link rel="apple-touch-icon" sizes="180x180" href='https://example.org/apple-touch-icon.png'>
|
||||
<link rel="icon" type="image/png" sizes="32x32" href='https://example.org/favicon-32x32.png'>
|
||||
<link rel="icon" type="image/png" sizes='16x16' href='https://example.org/favicon-16x16.png'>
|
||||
<link rel="manifest" href='https://example.org/site.webmanifest'>
|
||||
|
||||
<link rel="stylesheet" href="https://example.org/css/styles.fc7cf65388be07f2e53293132dd0220e34d9861f57de4b336d64dd03a3502a9befbea05606442d0a501005442835a864361b9a51b4b51acbf28df37530f61f31.css" integrity="sha512-/Hz2U4i+B/LlMpMTLdAiDjTZhh9X3kszbWTdA6NQKpvvvqBWBkQtClAQBUQoNahkNhuaUbS1GsvyjfN1MPYfMQ==">
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</head>
|
||||
<body>
|
||||
<header>
|
||||
<h1><a href="/">Formal Methods Tools</a></h1>
|
||||
|
||||
<nav>
|
||||
<ul>
|
||||
<li>
|
||||
<a href="/">Home</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/tools/">Tools</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/taxonomies/">Taxonomies</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/about/">About</a>
|
||||
</li>
|
||||
</ul>
|
||||
</nav>
|
||||
|
||||
|
||||
</header>
|
||||
<main>
|
||||
|
||||
<h1>Aranpoaswei</h1>
|
||||
|
||||
|
||||
<h2><a href="/tools/z3/">Z3 Theorem Prover</a></h2>
|
||||
|
||||
|
||||
</main>
|
||||
<footer>
|
||||
<p>Copyright 2025. All rights reserved.</p>
|
||||
|
||||
</footer>
|
||||
</body>
|
||||
</html>
|
||||
@@ -1,19 +0,0 @@
|
||||
<?xml version="1.0" encoding="utf-8" standalone="yes"?>
|
||||
<rss version="2.0" xmlns:atom="http://www.w3.org/2005/Atom">
|
||||
<channel>
|
||||
<title>Aranpoaswei on Formal Methods Tools</title>
|
||||
<link>https://example.org/interactions/aranpoaswei/</link>
|
||||
<description>Recent content in Aranpoaswei on Formal Methods Tools</description>
|
||||
<generator>Hugo</generator>
|
||||
<language>en-us</language>
|
||||
<lastBuildDate>Fri, 02 Feb 2024 04:14:54 -0800</lastBuildDate>
|
||||
<atom:link href="https://example.org/interactions/aranpoaswei/index.xml" rel="self" type="application/rss+xml" />
|
||||
<item>
|
||||
<title>Z3 Theorem Prover</title>
|
||||
<link>https://example.org/tools/z3/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>https://example.org/tools/z3/</guid>
|
||||
<description><p>desc</p></description>
|
||||
</item>
|
||||
</channel>
|
||||
</rss>
|
||||
@@ -1,69 +0,0 @@
|
||||
<!DOCTYPE html>
|
||||
<html lang="en-us" dir="ltr">
|
||||
<head>
|
||||
<meta charset="utf-8">
|
||||
|
||||
<meta name="viewport" content ="width=device-width, initial-scale=1.0, maximum-scale=1.0, user-scalable=no">
|
||||
<meta http-equiv="X-UA-Compatible" content="IE=edge">
|
||||
<title>Aranpoxasi | Formal Methods Tools</title>
|
||||
|
||||
|
||||
<meta name="keywords" content="Formal Methods Tools">
|
||||
<meta property="og:locale" content='en_US'>
|
||||
<meta property="og:type" content="article">
|
||||
<meta property="og:title" content="Aranpoxasi">
|
||||
<meta property="og:description" content="">
|
||||
<meta property="og:url" content="https://example.org/interactions/aranpoxasi/">
|
||||
<meta property="og:image" content="images/%!s(<nil>)">
|
||||
<link rel="canonical" href="https://example.org/interactions/aranpoxasi/">
|
||||
|
||||
<link rel="apple-touch-icon" sizes="180x180" href='https://example.org/apple-touch-icon.png'>
|
||||
<link rel="icon" type="image/png" sizes="32x32" href='https://example.org/favicon-32x32.png'>
|
||||
<link rel="icon" type="image/png" sizes='16x16' href='https://example.org/favicon-16x16.png'>
|
||||
<link rel="manifest" href='https://example.org/site.webmanifest'>
|
||||
|
||||
<link rel="stylesheet" href="https://example.org/css/styles.fc7cf65388be07f2e53293132dd0220e34d9861f57de4b336d64dd03a3502a9befbea05606442d0a501005442835a864361b9a51b4b51acbf28df37530f61f31.css" integrity="sha512-/Hz2U4i+B/LlMpMTLdAiDjTZhh9X3kszbWTdA6NQKpvvvqBWBkQtClAQBUQoNahkNhuaUbS1GsvyjfN1MPYfMQ==">
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</head>
|
||||
<body>
|
||||
<header>
|
||||
<h1><a href="/">Formal Methods Tools</a></h1>
|
||||
|
||||
<nav>
|
||||
<ul>
|
||||
<li>
|
||||
<a href="/">Home</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/tools/">Tools</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/taxonomies/">Taxonomies</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/about/">About</a>
|
||||
</li>
|
||||
</ul>
|
||||
</nav>
|
||||
|
||||
|
||||
</header>
|
||||
<main>
|
||||
|
||||
<h1>Aranpoxasi</h1>
|
||||
|
||||
|
||||
<h2><a href="/tools/z3/">Z3 Theorem Prover</a></h2>
|
||||
|
||||
|
||||
</main>
|
||||
<footer>
|
||||
<p>Copyright 2025. All rights reserved.</p>
|
||||
|
||||
</footer>
|
||||
</body>
|
||||
</html>
|
||||
@@ -1,19 +0,0 @@
|
||||
<?xml version="1.0" encoding="utf-8" standalone="yes"?>
|
||||
<rss version="2.0" xmlns:atom="http://www.w3.org/2005/Atom">
|
||||
<channel>
|
||||
<title>Aranpoxasi on Formal Methods Tools</title>
|
||||
<link>https://example.org/interactions/aranpoxasi/</link>
|
||||
<description>Recent content in Aranpoxasi on Formal Methods Tools</description>
|
||||
<generator>Hugo</generator>
|
||||
<language>en-us</language>
|
||||
<lastBuildDate>Fri, 02 Feb 2024 04:14:54 -0800</lastBuildDate>
|
||||
<atom:link href="https://example.org/interactions/aranpoxasi/index.xml" rel="self" type="application/rss+xml" />
|
||||
<item>
|
||||
<title>Z3 Theorem Prover</title>
|
||||
<link>https://example.org/tools/z3/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>https://example.org/tools/z3/</guid>
|
||||
<description><p>desc</p></description>
|
||||
</item>
|
||||
</channel>
|
||||
</rss>
|
||||
@@ -1,69 +0,0 @@
|
||||
<!DOCTYPE html>
|
||||
<html lang="en-us" dir="ltr">
|
||||
<head>
|
||||
<meta charset="utf-8">
|
||||
|
||||
<meta name="viewport" content ="width=device-width, initial-scale=1.0, maximum-scale=1.0, user-scalable=no">
|
||||
<meta http-equiv="X-UA-Compatible" content="IE=edge">
|
||||
<title>Aranpsoasi | Formal Methods Tools</title>
|
||||
|
||||
|
||||
<meta name="keywords" content="Formal Methods Tools">
|
||||
<meta property="og:locale" content='en_US'>
|
||||
<meta property="og:type" content="article">
|
||||
<meta property="og:title" content="Aranpsoasi">
|
||||
<meta property="og:description" content="">
|
||||
<meta property="og:url" content="https://example.org/interactions/aranpsoasi/">
|
||||
<meta property="og:image" content="images/%!s(<nil>)">
|
||||
<link rel="canonical" href="https://example.org/interactions/aranpsoasi/">
|
||||
|
||||
<link rel="apple-touch-icon" sizes="180x180" href='https://example.org/apple-touch-icon.png'>
|
||||
<link rel="icon" type="image/png" sizes="32x32" href='https://example.org/favicon-32x32.png'>
|
||||
<link rel="icon" type="image/png" sizes='16x16' href='https://example.org/favicon-16x16.png'>
|
||||
<link rel="manifest" href='https://example.org/site.webmanifest'>
|
||||
|
||||
<link rel="stylesheet" href="https://example.org/css/styles.fc7cf65388be07f2e53293132dd0220e34d9861f57de4b336d64dd03a3502a9befbea05606442d0a501005442835a864361b9a51b4b51acbf28df37530f61f31.css" integrity="sha512-/Hz2U4i+B/LlMpMTLdAiDjTZhh9X3kszbWTdA6NQKpvvvqBWBkQtClAQBUQoNahkNhuaUbS1GsvyjfN1MPYfMQ==">
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</head>
|
||||
<body>
|
||||
<header>
|
||||
<h1><a href="/">Formal Methods Tools</a></h1>
|
||||
|
||||
<nav>
|
||||
<ul>
|
||||
<li>
|
||||
<a href="/">Home</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/tools/">Tools</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/taxonomies/">Taxonomies</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/about/">About</a>
|
||||
</li>
|
||||
</ul>
|
||||
</nav>
|
||||
|
||||
|
||||
</header>
|
||||
<main>
|
||||
|
||||
<h1>Aranpsoasi</h1>
|
||||
|
||||
|
||||
<h2><a href="/tools/z3/">Z3 Theorem Prover</a></h2>
|
||||
|
||||
|
||||
</main>
|
||||
<footer>
|
||||
<p>Copyright 2025. All rights reserved.</p>
|
||||
|
||||
</footer>
|
||||
</body>
|
||||
</html>
|
||||
@@ -1,19 +0,0 @@
|
||||
<?xml version="1.0" encoding="utf-8" standalone="yes"?>
|
||||
<rss version="2.0" xmlns:atom="http://www.w3.org/2005/Atom">
|
||||
<channel>
|
||||
<title>Aranpsoasi on Formal Methods Tools</title>
|
||||
<link>https://example.org/interactions/aranpsoasi/</link>
|
||||
<description>Recent content in Aranpsoasi on Formal Methods Tools</description>
|
||||
<generator>Hugo</generator>
|
||||
<language>en-us</language>
|
||||
<lastBuildDate>Fri, 02 Feb 2024 04:14:54 -0800</lastBuildDate>
|
||||
<atom:link href="https://example.org/interactions/aranpsoasi/index.xml" rel="self" type="application/rss+xml" />
|
||||
<item>
|
||||
<title>Z3 Theorem Prover</title>
|
||||
<link>https://example.org/tools/z3/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>https://example.org/tools/z3/</guid>
|
||||
<description><p>desc</p></description>
|
||||
</item>
|
||||
</channel>
|
||||
</rss>
|
||||
@@ -1,69 +0,0 @@
|
||||
<!DOCTYPE html>
|
||||
<html lang="en-us" dir="ltr">
|
||||
<head>
|
||||
<meta charset="utf-8">
|
||||
|
||||
<meta name="viewport" content ="width=device-width, initial-scale=1.0, maximum-scale=1.0, user-scalable=no">
|
||||
<meta http-equiv="X-UA-Compatible" content="IE=edge">
|
||||
<title>Aransdpoasi | Formal Methods Tools</title>
|
||||
|
||||
|
||||
<meta name="keywords" content="Formal Methods Tools">
|
||||
<meta property="og:locale" content='en_US'>
|
||||
<meta property="og:type" content="article">
|
||||
<meta property="og:title" content="Aransdpoasi">
|
||||
<meta property="og:description" content="">
|
||||
<meta property="og:url" content="https://example.org/interactions/aransdpoasi/">
|
||||
<meta property="og:image" content="images/%!s(<nil>)">
|
||||
<link rel="canonical" href="https://example.org/interactions/aransdpoasi/">
|
||||
|
||||
<link rel="apple-touch-icon" sizes="180x180" href='https://example.org/apple-touch-icon.png'>
|
||||
<link rel="icon" type="image/png" sizes="32x32" href='https://example.org/favicon-32x32.png'>
|
||||
<link rel="icon" type="image/png" sizes='16x16' href='https://example.org/favicon-16x16.png'>
|
||||
<link rel="manifest" href='https://example.org/site.webmanifest'>
|
||||
|
||||
<link rel="stylesheet" href="https://example.org/css/styles.fc7cf65388be07f2e53293132dd0220e34d9861f57de4b336d64dd03a3502a9befbea05606442d0a501005442835a864361b9a51b4b51acbf28df37530f61f31.css" integrity="sha512-/Hz2U4i+B/LlMpMTLdAiDjTZhh9X3kszbWTdA6NQKpvvvqBWBkQtClAQBUQoNahkNhuaUbS1GsvyjfN1MPYfMQ==">
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</head>
|
||||
<body>
|
||||
<header>
|
||||
<h1><a href="/">Formal Methods Tools</a></h1>
|
||||
|
||||
<nav>
|
||||
<ul>
|
||||
<li>
|
||||
<a href="/">Home</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/tools/">Tools</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/taxonomies/">Taxonomies</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/about/">About</a>
|
||||
</li>
|
||||
</ul>
|
||||
</nav>
|
||||
|
||||
|
||||
</header>
|
||||
<main>
|
||||
|
||||
<h1>Aransdpoasi</h1>
|
||||
|
||||
|
||||
<h2><a href="/tools/z3/">Z3 Theorem Prover</a></h2>
|
||||
|
||||
|
||||
</main>
|
||||
<footer>
|
||||
<p>Copyright 2025. All rights reserved.</p>
|
||||
|
||||
</footer>
|
||||
</body>
|
||||
</html>
|
||||
@@ -1,19 +0,0 @@
|
||||
<?xml version="1.0" encoding="utf-8" standalone="yes"?>
|
||||
<rss version="2.0" xmlns:atom="http://www.w3.org/2005/Atom">
|
||||
<channel>
|
||||
<title>Aransdpoasi on Formal Methods Tools</title>
|
||||
<link>https://example.org/interactions/aransdpoasi/</link>
|
||||
<description>Recent content in Aransdpoasi on Formal Methods Tools</description>
|
||||
<generator>Hugo</generator>
|
||||
<language>en-us</language>
|
||||
<lastBuildDate>Fri, 02 Feb 2024 04:14:54 -0800</lastBuildDate>
|
||||
<atom:link href="https://example.org/interactions/aransdpoasi/index.xml" rel="self" type="application/rss+xml" />
|
||||
<item>
|
||||
<title>Z3 Theorem Prover</title>
|
||||
<link>https://example.org/tools/z3/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>https://example.org/tools/z3/</guid>
|
||||
<description><p>desc</p></description>
|
||||
</item>
|
||||
</channel>
|
||||
</rss>
|
||||
69
interactions/c-api/index.html
Normal file
69
interactions/c-api/index.html
Normal file
@@ -0,0 +1,69 @@
|
||||
<!DOCTYPE html>
|
||||
<html lang="en-us" dir="ltr">
|
||||
<head><script src="/livereload.js?mindelay=10&v=2&port=1313&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">
|
||||
<meta http-equiv="X-UA-Compatible" content="IE=edge">
|
||||
<title>C API | Formal Methods Tools</title>
|
||||
|
||||
|
||||
<meta name="keywords" content="Formal Methods Tools">
|
||||
<meta property="og:locale" content='en_US'>
|
||||
<meta property="og:type" content="article">
|
||||
<meta property="og:title" content="C API">
|
||||
<meta property="og:description" content="">
|
||||
<meta property="og:url" content="http://localhost:1313/interactions/c-api/">
|
||||
<meta property="og:image" content="images/%!s(<nil>)">
|
||||
<link rel="canonical" href="http://localhost:1313/interactions/c-api/">
|
||||
|
||||
<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="http://localhost:1313/css/styles.e3fcfb3452c69d09414fe512e9dca31d879e4a6c47d23010fbb07eb6693d447f645d3bd2d021c0d28d0f7b4fe6f32a10e599488cdb16c6750a9a126788131917.css" integrity="sha512-4/z7NFLGnQlBT+US6dyjHYeeSmxH0jAQ+7B+tmk9RH9kXTvS0CHA0o0Pe0/m8yoQ5ZlIjNsWxnUKmhJniBMZFw==">
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</head>
|
||||
<body>
|
||||
<header>
|
||||
<h1><a href="/">Formal Methods Tools</a></h1>
|
||||
|
||||
<nav>
|
||||
<ul>
|
||||
<li>
|
||||
<a href="/">Home</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/tools/">Tools</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/taxonomies/">Taxonomies</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/about/">About</a>
|
||||
</li>
|
||||
</ul>
|
||||
</nav>
|
||||
|
||||
|
||||
</header>
|
||||
<main>
|
||||
|
||||
<h1>C API</h1>
|
||||
|
||||
|
||||
<h2><a href="/tools/yices/">Yices 2</a></h2>
|
||||
|
||||
|
||||
</main>
|
||||
<footer>
|
||||
<p>Copyright 2025. All rights reserved.</p>
|
||||
|
||||
</footer>
|
||||
</body>
|
||||
</html>
|
||||
19
interactions/c-api/index.xml
Normal file
19
interactions/c-api/index.xml
Normal file
@@ -0,0 +1,19 @@
|
||||
<?xml version="1.0" encoding="utf-8" standalone="yes"?>
|
||||
<rss version="2.0" xmlns:atom="http://www.w3.org/2005/Atom">
|
||||
<channel>
|
||||
<title>C API on Formal Methods Tools</title>
|
||||
<link>http://localhost:1313/interactions/c-api/</link>
|
||||
<description>Recent content in C API on Formal Methods Tools</description>
|
||||
<generator>Hugo</generator>
|
||||
<language>en-us</language>
|
||||
<lastBuildDate>Fri, 02 Feb 2024 04:14:54 -0800</lastBuildDate>
|
||||
<atom:link href="http://localhost:1313/interactions/c-api/index.xml" rel="self" type="application/rss+xml" />
|
||||
<item>
|
||||
<title>Yices 2</title>
|
||||
<link>http://localhost:1313/tools/yices/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>http://localhost:1313/tools/yices/</guid>
|
||||
<description><p>Yices is a high-performance SMT solver and theorem prover developed by SRI International. It is widely used for checking the satisfiability of logical formulas over various theories, including arithmetic, bit-vectors, arrays, and uninterpreted functions. Yices supports the SMT-LIB standard and its own input language, and provides APIs for several programming languages, making it suitable for integration into formal verification, program analysis, and constraint solving tools.</p>
<h3 id="features">Features</h3>
<ul>
<li><strong>SMT Solver:</strong> Supports a wide range of theories and quantifiers.</li>
<li><strong>Multi-language APIs:</strong> C, OCaml, Python, and more.</li>
<li><strong>Cross-platform:</strong> Available on Windows, Linux, and macOS.</li>
<li><strong>Active development:</strong> Open source and maintained by SRI International.</li>
</ul></description>
|
||||
</item>
|
||||
</channel>
|
||||
</rss>
|
||||
71
interactions/cli/index.html
Normal file
71
interactions/cli/index.html
Normal file
@@ -0,0 +1,71 @@
|
||||
<!DOCTYPE html>
|
||||
<html lang="en-us" dir="ltr">
|
||||
<head><script src="/livereload.js?mindelay=10&v=2&port=1313&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">
|
||||
<meta http-equiv="X-UA-Compatible" content="IE=edge">
|
||||
<title>CLI | Formal Methods Tools</title>
|
||||
|
||||
|
||||
<meta name="keywords" content="Formal Methods Tools">
|
||||
<meta property="og:locale" content='en_US'>
|
||||
<meta property="og:type" content="article">
|
||||
<meta property="og:title" content="CLI">
|
||||
<meta property="og:description" content="">
|
||||
<meta property="og:url" content="http://localhost:1313/interactions/cli/">
|
||||
<meta property="og:image" content="images/%!s(<nil>)">
|
||||
<link rel="canonical" href="http://localhost:1313/interactions/cli/">
|
||||
|
||||
<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="http://localhost:1313/css/styles.e3fcfb3452c69d09414fe512e9dca31d879e4a6c47d23010fbb07eb6693d447f645d3bd2d021c0d28d0f7b4fe6f32a10e599488cdb16c6750a9a126788131917.css" integrity="sha512-4/z7NFLGnQlBT+US6dyjHYeeSmxH0jAQ+7B+tmk9RH9kXTvS0CHA0o0Pe0/m8yoQ5ZlIjNsWxnUKmhJniBMZFw==">
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</head>
|
||||
<body>
|
||||
<header>
|
||||
<h1><a href="/">Formal Methods Tools</a></h1>
|
||||
|
||||
<nav>
|
||||
<ul>
|
||||
<li>
|
||||
<a href="/">Home</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/tools/">Tools</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/taxonomies/">Taxonomies</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/about/">About</a>
|
||||
</li>
|
||||
</ul>
|
||||
</nav>
|
||||
|
||||
|
||||
</header>
|
||||
<main>
|
||||
|
||||
<h1>CLI</h1>
|
||||
|
||||
|
||||
<h2><a href="/tools/yices/">Yices 2</a></h2>
|
||||
|
||||
<h2><a href="/tools/z3/">Z3</a></h2>
|
||||
|
||||
|
||||
</main>
|
||||
<footer>
|
||||
<p>Copyright 2025. All rights reserved.</p>
|
||||
|
||||
</footer>
|
||||
</body>
|
||||
</html>
|
||||
26
interactions/cli/index.xml
Normal file
26
interactions/cli/index.xml
Normal file
@@ -0,0 +1,26 @@
|
||||
<?xml version="1.0" encoding="utf-8" standalone="yes"?>
|
||||
<rss version="2.0" xmlns:atom="http://www.w3.org/2005/Atom">
|
||||
<channel>
|
||||
<title>CLI on Formal Methods Tools</title>
|
||||
<link>http://localhost:1313/interactions/cli/</link>
|
||||
<description>Recent content in CLI on Formal Methods Tools</description>
|
||||
<generator>Hugo</generator>
|
||||
<language>en-us</language>
|
||||
<lastBuildDate>Fri, 02 Feb 2024 04:14:54 -0800</lastBuildDate>
|
||||
<atom:link href="http://localhost:1313/interactions/cli/index.xml" rel="self" type="application/rss+xml" />
|
||||
<item>
|
||||
<title>Yices 2</title>
|
||||
<link>http://localhost:1313/tools/yices/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>http://localhost:1313/tools/yices/</guid>
|
||||
<description><p>Yices is a high-performance SMT solver and theorem prover developed by SRI International. It is widely used for checking the satisfiability of logical formulas over various theories, including arithmetic, bit-vectors, arrays, and uninterpreted functions. Yices supports the SMT-LIB standard and its own input language, and provides APIs for several programming languages, making it suitable for integration into formal verification, program analysis, and constraint solving tools.</p>
<h3 id="features">Features</h3>
<ul>
<li><strong>SMT Solver:</strong> Supports a wide range of theories and quantifiers.</li>
<li><strong>Multi-language APIs:</strong> C, OCaml, Python, and more.</li>
<li><strong>Cross-platform:</strong> Available on Windows, Linux, and macOS.</li>
<li><strong>Active development:</strong> Open source and maintained by SRI International.</li>
</ul></description>
|
||||
</item>
|
||||
<item>
|
||||
<title>Z3</title>
|
||||
<link>http://localhost:1313/tools/z3/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>http://localhost:1313/tools/z3/</guid>
|
||||
<description><p>Z3 is a high-performance SMT solver and theorem prover developed by Microsoft Research. It is widely used for checking the satisfiability of logical formulas over various theories, including arithmetic, bit-vectors, arrays, and uninterpreted functions. Z3 supports the SMT-LIB standard and provides APIs for several programming languages, making it suitable for integration into formal verification, program analysis, and constraint solving tools.</p>
<h3 id="features">Features</h3>
<ul>
<li><strong>SMT Solver:</strong> Supports a wide range of theories and quantifiers.</li>
<li><strong>Multi-language APIs:</strong> Python, C++, Java, .NET, and more.</li>
<li><strong>Cross-platform:</strong> Available on Windows, Linux, and macOS.</li>
<li><strong>Active development:</strong> Open source and maintained by Microsoft Research.</li>
<li><strong>Web Playground:</strong> Try Z3 online at <a href="https://rise4fun.com/z3">Rise4Fun</a>.</li>
</ul></description>
|
||||
</item>
|
||||
</channel>
|
||||
</rss>
|
||||
@@ -1,6 +1,6 @@
|
||||
<!DOCTYPE html>
|
||||
<html lang="en-us" dir="ltr">
|
||||
<head>
|
||||
<head><script src="/livereload.js?mindelay=10&v=2&port=1313&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">
|
||||
@@ -13,16 +13,16 @@
|
||||
<meta property="og:type" content="article">
|
||||
<meta property="og:title" content="Interactions">
|
||||
<meta property="og:description" content="">
|
||||
<meta property="og:url" content="https://example.org/interactions/">
|
||||
<meta property="og:url" content="http://localhost:1313/interactions/">
|
||||
<meta property="og:image" content="images/%!s(<nil>)">
|
||||
<link rel="canonical" href="https://example.org/interactions/">
|
||||
<link rel="canonical" href="http://localhost:1313/interactions/">
|
||||
|
||||
<link rel="apple-touch-icon" sizes="180x180" href='https://example.org/apple-touch-icon.png'>
|
||||
<link rel="icon" type="image/png" sizes="32x32" href='https://example.org/favicon-32x32.png'>
|
||||
<link rel="icon" type="image/png" sizes='16x16' href='https://example.org/favicon-16x16.png'>
|
||||
<link rel="manifest" href='https://example.org/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://example.org/css/styles.fc7cf65388be07f2e53293132dd0220e34d9861f57de4b336d64dd03a3502a9befbea05606442d0a501005442835a864361b9a51b4b51acbf28df37530f61f31.css" integrity="sha512-/Hz2U4i+B/LlMpMTLdAiDjTZhh9X3kszbWTdA6NQKpvvvqBWBkQtClAQBUQoNahkNhuaUbS1GsvyjfN1MPYfMQ==">
|
||||
<link rel="stylesheet" href="http://localhost:1313/css/styles.e3fcfb3452c69d09414fe512e9dca31d879e4a6c47d23010fbb07eb6693d447f645d3bd2d021c0d28d0f7b4fe6f32a10e599488cdb16c6750a9a126788131917.css" integrity="sha512-4/z7NFLGnQlBT+US6dyjHYeeSmxH0jAQ+7B+tmk9RH9kXTvS0CHA0o0Pe0/m8yoQ5ZlIjNsWxnUKmhJniBMZFw==">
|
||||
|
||||
|
||||
|
||||
@@ -70,10 +70,10 @@
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="interactions_araafafanpoasi"
|
||||
style="background:rgba(41,113,12,0.4)"
|
||||
href="/interactions/araafafanpoasi">
|
||||
Araafafanpoasi
|
||||
id="interactions_c-api"
|
||||
style="background:rgba(19,205,141,0.4)"
|
||||
href="/interactions/c-api">
|
||||
C API
|
||||
</a>
|
||||
|
||||
|
||||
@@ -88,10 +88,10 @@
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="interactions_aranapoasi"
|
||||
style="background:rgba(197,104,26,0.4)"
|
||||
href="/interactions/aranapoasi">
|
||||
Aranapoasi
|
||||
id="interactions_cli"
|
||||
style="background:rgba(145,175,87,0.4)"
|
||||
href="/interactions/cli">
|
||||
CLI
|
||||
</a>
|
||||
|
||||
|
||||
@@ -106,10 +106,10 @@
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="interactions_aranpoasadfsi"
|
||||
style="background:rgba(216,112,108,0.4)"
|
||||
href="/interactions/aranpoasadfsi">
|
||||
Aranpoasadfsi
|
||||
id="interactions_ocaml-api"
|
||||
style="background:rgba(54,250,207,0.4)"
|
||||
href="/interactions/ocaml-api">
|
||||
OCaml API
|
||||
</a>
|
||||
|
||||
|
||||
@@ -124,10 +124,10 @@
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="interactions_aranpoasai"
|
||||
style="background:rgba(131,31,234,0.4)"
|
||||
href="/interactions/aranpoasai">
|
||||
Aranpoasai
|
||||
id="interactions_playground"
|
||||
style="background:rgba(165,254,219,0.4)"
|
||||
href="/interactions/playground">
|
||||
Playground
|
||||
</a>
|
||||
|
||||
|
||||
@@ -142,10 +142,10 @@
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="interactions_aranpoasasdfasfasdfasdfi"
|
||||
style="background:rgba(237,71,214,0.4)"
|
||||
href="/interactions/aranpoasasdfasfasdfasdfi">
|
||||
Aranpoasasdfasfasdfasdfi
|
||||
id="interactions_python-api"
|
||||
style="background:rgba(2,212,135,0.4)"
|
||||
href="/interactions/python-api">
|
||||
Python API
|
||||
</a>
|
||||
|
||||
|
||||
@@ -160,10 +160,10 @@
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="interactions_aranpoasi"
|
||||
style="background:rgba(44,147,98,0.4)"
|
||||
href="/interactions/aranpoasi">
|
||||
Aranpoasi
|
||||
id="interactions_python-bindings"
|
||||
style="background:rgba(37,32,133,0.4)"
|
||||
href="/interactions/python-bindings">
|
||||
Python Bindings
|
||||
</a>
|
||||
|
||||
|
||||
@@ -178,82 +178,10 @@
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="interactions_aranpoaswei"
|
||||
style="background:rgba(193,42,7,0.4)"
|
||||
href="/interactions/aranpoaswei">
|
||||
Aranpoaswei
|
||||
</a>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="interactions_aranpoxasi"
|
||||
style="background:rgba(215,16,49,0.4)"
|
||||
href="/interactions/aranpoxasi">
|
||||
Aranpoxasi
|
||||
</a>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="interactions_aranpsoasi"
|
||||
style="background:rgba(18,156,157,0.4)"
|
||||
href="/interactions/aranpsoasi">
|
||||
Aranpsoasi
|
||||
</a>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="interactions_aransdpoasi"
|
||||
style="background:rgba(169,198,121,0.4)"
|
||||
href="/interactions/aransdpoasi">
|
||||
Aransdpoasi
|
||||
</a>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="interactions_lorem-ipsum"
|
||||
style="background:rgba(109,189,1,0.4)"
|
||||
href="/interactions/lorem-ipsum">
|
||||
Lorem Ipsum
|
||||
id="interactions_rust-bindings"
|
||||
style="background:rgba(124,204,243,0.4)"
|
||||
href="/interactions/rust-bindings">
|
||||
Rust Bindings
|
||||
</a>
|
||||
|
||||
|
||||
|
||||
@@ -2,87 +2,59 @@
|
||||
<rss version="2.0" xmlns:atom="http://www.w3.org/2005/Atom">
|
||||
<channel>
|
||||
<title>Interactions on Formal Methods Tools</title>
|
||||
<link>https://example.org/interactions/</link>
|
||||
<link>http://localhost:1313/interactions/</link>
|
||||
<description>Recent content in Interactions on Formal Methods Tools</description>
|
||||
<generator>Hugo</generator>
|
||||
<language>en-us</language>
|
||||
<lastBuildDate>Fri, 02 Feb 2024 04:14:54 -0800</lastBuildDate>
|
||||
<atom:link href="https://example.org/interactions/index.xml" rel="self" type="application/rss+xml" />
|
||||
<atom:link href="http://localhost:1313/interactions/index.xml" rel="self" type="application/rss+xml" />
|
||||
<item>
|
||||
<title>Araafafanpoasi</title>
|
||||
<link>https://example.org/interactions/araafafanpoasi/</link>
|
||||
<title>C API</title>
|
||||
<link>http://localhost:1313/interactions/c-api/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>https://example.org/interactions/araafafanpoasi/</guid>
|
||||
<guid>http://localhost:1313/interactions/c-api/</guid>
|
||||
<description></description>
|
||||
</item>
|
||||
<item>
|
||||
<title>Aranapoasi</title>
|
||||
<link>https://example.org/interactions/aranapoasi/</link>
|
||||
<title>CLI</title>
|
||||
<link>http://localhost:1313/interactions/cli/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>https://example.org/interactions/aranapoasi/</guid>
|
||||
<guid>http://localhost:1313/interactions/cli/</guid>
|
||||
<description></description>
|
||||
</item>
|
||||
<item>
|
||||
<title>Aranpoasadfsi</title>
|
||||
<link>https://example.org/interactions/aranpoasadfsi/</link>
|
||||
<title>OCaml API</title>
|
||||
<link>http://localhost:1313/interactions/ocaml-api/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>https://example.org/interactions/aranpoasadfsi/</guid>
|
||||
<guid>http://localhost:1313/interactions/ocaml-api/</guid>
|
||||
<description></description>
|
||||
</item>
|
||||
<item>
|
||||
<title>Aranpoasai</title>
|
||||
<link>https://example.org/interactions/aranpoasai/</link>
|
||||
<title>Playground</title>
|
||||
<link>http://localhost:1313/interactions/playground/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>https://example.org/interactions/aranpoasai/</guid>
|
||||
<guid>http://localhost:1313/interactions/playground/</guid>
|
||||
<description></description>
|
||||
</item>
|
||||
<item>
|
||||
<title>Aranpoasasdfasfasdfasdfi</title>
|
||||
<link>https://example.org/interactions/aranpoasasdfasfasdfasdfi/</link>
|
||||
<title>Python API</title>
|
||||
<link>http://localhost:1313/interactions/python-api/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>https://example.org/interactions/aranpoasasdfasfasdfasdfi/</guid>
|
||||
<guid>http://localhost:1313/interactions/python-api/</guid>
|
||||
<description></description>
|
||||
</item>
|
||||
<item>
|
||||
<title>Aranpoasi</title>
|
||||
<link>https://example.org/interactions/aranpoasi/</link>
|
||||
<title>Python Bindings</title>
|
||||
<link>http://localhost:1313/interactions/python-bindings/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>https://example.org/interactions/aranpoasi/</guid>
|
||||
<guid>http://localhost:1313/interactions/python-bindings/</guid>
|
||||
<description></description>
|
||||
</item>
|
||||
<item>
|
||||
<title>Aranpoaswei</title>
|
||||
<link>https://example.org/interactions/aranpoaswei/</link>
|
||||
<title>Rust Bindings</title>
|
||||
<link>http://localhost:1313/interactions/rust-bindings/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>https://example.org/interactions/aranpoaswei/</guid>
|
||||
<description></description>
|
||||
</item>
|
||||
<item>
|
||||
<title>Aranpoxasi</title>
|
||||
<link>https://example.org/interactions/aranpoxasi/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>https://example.org/interactions/aranpoxasi/</guid>
|
||||
<description></description>
|
||||
</item>
|
||||
<item>
|
||||
<title>Aranpsoasi</title>
|
||||
<link>https://example.org/interactions/aranpsoasi/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>https://example.org/interactions/aranpsoasi/</guid>
|
||||
<description></description>
|
||||
</item>
|
||||
<item>
|
||||
<title>Aransdpoasi</title>
|
||||
<link>https://example.org/interactions/aransdpoasi/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>https://example.org/interactions/aransdpoasi/</guid>
|
||||
<description></description>
|
||||
</item>
|
||||
<item>
|
||||
<title>Lorem Ipsum</title>
|
||||
<link>https://example.org/interactions/lorem-ipsum/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>https://example.org/interactions/lorem-ipsum/</guid>
|
||||
<guid>http://localhost:1313/interactions/rust-bindings/</guid>
|
||||
<description></description>
|
||||
</item>
|
||||
</channel>
|
||||
|
||||
@@ -1,69 +0,0 @@
|
||||
<!DOCTYPE html>
|
||||
<html lang="en-us" dir="ltr">
|
||||
<head>
|
||||
<meta charset="utf-8">
|
||||
|
||||
<meta name="viewport" content ="width=device-width, initial-scale=1.0, maximum-scale=1.0, user-scalable=no">
|
||||
<meta http-equiv="X-UA-Compatible" content="IE=edge">
|
||||
<title>Lorem Ipsum | Formal Methods Tools</title>
|
||||
|
||||
|
||||
<meta name="keywords" content="Formal Methods Tools">
|
||||
<meta property="og:locale" content='en_US'>
|
||||
<meta property="og:type" content="article">
|
||||
<meta property="og:title" content="Lorem Ipsum">
|
||||
<meta property="og:description" content="">
|
||||
<meta property="og:url" content="https://example.org/interactions/lorem-ipsum/">
|
||||
<meta property="og:image" content="images/%!s(<nil>)">
|
||||
<link rel="canonical" href="https://example.org/interactions/lorem-ipsum/">
|
||||
|
||||
<link rel="apple-touch-icon" sizes="180x180" href='https://example.org/apple-touch-icon.png'>
|
||||
<link rel="icon" type="image/png" sizes="32x32" href='https://example.org/favicon-32x32.png'>
|
||||
<link rel="icon" type="image/png" sizes='16x16' href='https://example.org/favicon-16x16.png'>
|
||||
<link rel="manifest" href='https://example.org/site.webmanifest'>
|
||||
|
||||
<link rel="stylesheet" href="https://example.org/css/styles.fc7cf65388be07f2e53293132dd0220e34d9861f57de4b336d64dd03a3502a9befbea05606442d0a501005442835a864361b9a51b4b51acbf28df37530f61f31.css" integrity="sha512-/Hz2U4i+B/LlMpMTLdAiDjTZhh9X3kszbWTdA6NQKpvvvqBWBkQtClAQBUQoNahkNhuaUbS1GsvyjfN1MPYfMQ==">
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</head>
|
||||
<body>
|
||||
<header>
|
||||
<h1><a href="/">Formal Methods Tools</a></h1>
|
||||
|
||||
<nav>
|
||||
<ul>
|
||||
<li>
|
||||
<a href="/">Home</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/tools/">Tools</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/taxonomies/">Taxonomies</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/about/">About</a>
|
||||
</li>
|
||||
</ul>
|
||||
</nav>
|
||||
|
||||
|
||||
</header>
|
||||
<main>
|
||||
|
||||
<h1>Lorem Ipsum</h1>
|
||||
|
||||
|
||||
<h2><a href="/tools/z3/">Z3 Theorem Prover</a></h2>
|
||||
|
||||
|
||||
</main>
|
||||
<footer>
|
||||
<p>Copyright 2025. All rights reserved.</p>
|
||||
|
||||
</footer>
|
||||
</body>
|
||||
</html>
|
||||
@@ -1,19 +0,0 @@
|
||||
<?xml version="1.0" encoding="utf-8" standalone="yes"?>
|
||||
<rss version="2.0" xmlns:atom="http://www.w3.org/2005/Atom">
|
||||
<channel>
|
||||
<title>Lorem Ipsum on Formal Methods Tools</title>
|
||||
<link>https://example.org/interactions/lorem-ipsum/</link>
|
||||
<description>Recent content in Lorem Ipsum on Formal Methods Tools</description>
|
||||
<generator>Hugo</generator>
|
||||
<language>en-us</language>
|
||||
<lastBuildDate>Fri, 02 Feb 2024 04:14:54 -0800</lastBuildDate>
|
||||
<atom:link href="https://example.org/interactions/lorem-ipsum/index.xml" rel="self" type="application/rss+xml" />
|
||||
<item>
|
||||
<title>Z3 Theorem Prover</title>
|
||||
<link>https://example.org/tools/z3/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>https://example.org/tools/z3/</guid>
|
||||
<description><p>desc</p></description>
|
||||
</item>
|
||||
</channel>
|
||||
</rss>
|
||||
69
interactions/ocaml-api/index.html
Normal file
69
interactions/ocaml-api/index.html
Normal file
@@ -0,0 +1,69 @@
|
||||
<!DOCTYPE html>
|
||||
<html lang="en-us" dir="ltr">
|
||||
<head><script src="/livereload.js?mindelay=10&v=2&port=1313&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">
|
||||
<meta http-equiv="X-UA-Compatible" content="IE=edge">
|
||||
<title>OCaml API | Formal Methods Tools</title>
|
||||
|
||||
|
||||
<meta name="keywords" content="Formal Methods Tools">
|
||||
<meta property="og:locale" content='en_US'>
|
||||
<meta property="og:type" content="article">
|
||||
<meta property="og:title" content="OCaml API">
|
||||
<meta property="og:description" content="">
|
||||
<meta property="og:url" content="http://localhost:1313/interactions/ocaml-api/">
|
||||
<meta property="og:image" content="images/%!s(<nil>)">
|
||||
<link rel="canonical" href="http://localhost:1313/interactions/ocaml-api/">
|
||||
|
||||
<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="http://localhost:1313/css/styles.e3fcfb3452c69d09414fe512e9dca31d879e4a6c47d23010fbb07eb6693d447f645d3bd2d021c0d28d0f7b4fe6f32a10e599488cdb16c6750a9a126788131917.css" integrity="sha512-4/z7NFLGnQlBT+US6dyjHYeeSmxH0jAQ+7B+tmk9RH9kXTvS0CHA0o0Pe0/m8yoQ5ZlIjNsWxnUKmhJniBMZFw==">
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</head>
|
||||
<body>
|
||||
<header>
|
||||
<h1><a href="/">Formal Methods Tools</a></h1>
|
||||
|
||||
<nav>
|
||||
<ul>
|
||||
<li>
|
||||
<a href="/">Home</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/tools/">Tools</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/taxonomies/">Taxonomies</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/about/">About</a>
|
||||
</li>
|
||||
</ul>
|
||||
</nav>
|
||||
|
||||
|
||||
</header>
|
||||
<main>
|
||||
|
||||
<h1>OCaml API</h1>
|
||||
|
||||
|
||||
<h2><a href="/tools/yices/">Yices 2</a></h2>
|
||||
|
||||
|
||||
</main>
|
||||
<footer>
|
||||
<p>Copyright 2025. All rights reserved.</p>
|
||||
|
||||
</footer>
|
||||
</body>
|
||||
</html>
|
||||
19
interactions/ocaml-api/index.xml
Normal file
19
interactions/ocaml-api/index.xml
Normal file
@@ -0,0 +1,19 @@
|
||||
<?xml version="1.0" encoding="utf-8" standalone="yes"?>
|
||||
<rss version="2.0" xmlns:atom="http://www.w3.org/2005/Atom">
|
||||
<channel>
|
||||
<title>OCaml API on Formal Methods Tools</title>
|
||||
<link>http://localhost:1313/interactions/ocaml-api/</link>
|
||||
<description>Recent content in OCaml API on Formal Methods Tools</description>
|
||||
<generator>Hugo</generator>
|
||||
<language>en-us</language>
|
||||
<lastBuildDate>Fri, 02 Feb 2024 04:14:54 -0800</lastBuildDate>
|
||||
<atom:link href="http://localhost:1313/interactions/ocaml-api/index.xml" rel="self" type="application/rss+xml" />
|
||||
<item>
|
||||
<title>Yices 2</title>
|
||||
<link>http://localhost:1313/tools/yices/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>http://localhost:1313/tools/yices/</guid>
|
||||
<description><p>Yices is a high-performance SMT solver and theorem prover developed by SRI International. It is widely used for checking the satisfiability of logical formulas over various theories, including arithmetic, bit-vectors, arrays, and uninterpreted functions. Yices supports the SMT-LIB standard and its own input language, and provides APIs for several programming languages, making it suitable for integration into formal verification, program analysis, and constraint solving tools.</p>
<h3 id="features">Features</h3>
<ul>
<li><strong>SMT Solver:</strong> Supports a wide range of theories and quantifiers.</li>
<li><strong>Multi-language APIs:</strong> C, OCaml, Python, and more.</li>
<li><strong>Cross-platform:</strong> Available on Windows, Linux, and macOS.</li>
<li><strong>Active development:</strong> Open source and maintained by SRI International.</li>
</ul></description>
|
||||
</item>
|
||||
</channel>
|
||||
</rss>
|
||||
69
interactions/playground/index.html
Normal file
69
interactions/playground/index.html
Normal file
@@ -0,0 +1,69 @@
|
||||
<!DOCTYPE html>
|
||||
<html lang="en-us" dir="ltr">
|
||||
<head><script src="/livereload.js?mindelay=10&v=2&port=1313&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">
|
||||
<meta http-equiv="X-UA-Compatible" content="IE=edge">
|
||||
<title>Playground | Formal Methods Tools</title>
|
||||
|
||||
|
||||
<meta name="keywords" content="Formal Methods Tools">
|
||||
<meta property="og:locale" content='en_US'>
|
||||
<meta property="og:type" content="article">
|
||||
<meta property="og:title" content="Playground">
|
||||
<meta property="og:description" content="">
|
||||
<meta property="og:url" content="http://localhost:1313/interactions/playground/">
|
||||
<meta property="og:image" content="images/%!s(<nil>)">
|
||||
<link rel="canonical" href="http://localhost:1313/interactions/playground/">
|
||||
|
||||
<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="http://localhost:1313/css/styles.e3fcfb3452c69d09414fe512e9dca31d879e4a6c47d23010fbb07eb6693d447f645d3bd2d021c0d28d0f7b4fe6f32a10e599488cdb16c6750a9a126788131917.css" integrity="sha512-4/z7NFLGnQlBT+US6dyjHYeeSmxH0jAQ+7B+tmk9RH9kXTvS0CHA0o0Pe0/m8yoQ5ZlIjNsWxnUKmhJniBMZFw==">
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</head>
|
||||
<body>
|
||||
<header>
|
||||
<h1><a href="/">Formal Methods Tools</a></h1>
|
||||
|
||||
<nav>
|
||||
<ul>
|
||||
<li>
|
||||
<a href="/">Home</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/tools/">Tools</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/taxonomies/">Taxonomies</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/about/">About</a>
|
||||
</li>
|
||||
</ul>
|
||||
</nav>
|
||||
|
||||
|
||||
</header>
|
||||
<main>
|
||||
|
||||
<h1>Playground</h1>
|
||||
|
||||
|
||||
<h2><a href="/tools/z3/">Z3</a></h2>
|
||||
|
||||
|
||||
</main>
|
||||
<footer>
|
||||
<p>Copyright 2025. All rights reserved.</p>
|
||||
|
||||
</footer>
|
||||
</body>
|
||||
</html>
|
||||
19
interactions/playground/index.xml
Normal file
19
interactions/playground/index.xml
Normal file
@@ -0,0 +1,19 @@
|
||||
<?xml version="1.0" encoding="utf-8" standalone="yes"?>
|
||||
<rss version="2.0" xmlns:atom="http://www.w3.org/2005/Atom">
|
||||
<channel>
|
||||
<title>Playground on Formal Methods Tools</title>
|
||||
<link>http://localhost:1313/interactions/playground/</link>
|
||||
<description>Recent content in Playground on Formal Methods Tools</description>
|
||||
<generator>Hugo</generator>
|
||||
<language>en-us</language>
|
||||
<lastBuildDate>Fri, 02 Feb 2024 04:14:54 -0800</lastBuildDate>
|
||||
<atom:link href="http://localhost:1313/interactions/playground/index.xml" rel="self" type="application/rss+xml" />
|
||||
<item>
|
||||
<title>Z3</title>
|
||||
<link>http://localhost:1313/tools/z3/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>http://localhost:1313/tools/z3/</guid>
|
||||
<description><p>Z3 is a high-performance SMT solver and theorem prover developed by Microsoft Research. It is widely used for checking the satisfiability of logical formulas over various theories, including arithmetic, bit-vectors, arrays, and uninterpreted functions. Z3 supports the SMT-LIB standard and provides APIs for several programming languages, making it suitable for integration into formal verification, program analysis, and constraint solving tools.</p>
<h3 id="features">Features</h3>
<ul>
<li><strong>SMT Solver:</strong> Supports a wide range of theories and quantifiers.</li>
<li><strong>Multi-language APIs:</strong> Python, C++, Java, .NET, and more.</li>
<li><strong>Cross-platform:</strong> Available on Windows, Linux, and macOS.</li>
<li><strong>Active development:</strong> Open source and maintained by Microsoft Research.</li>
<li><strong>Web Playground:</strong> Try Z3 online at <a href="https://rise4fun.com/z3">Rise4Fun</a>.</li>
</ul></description>
|
||||
</item>
|
||||
</channel>
|
||||
</rss>
|
||||
69
interactions/python-api/index.html
Normal file
69
interactions/python-api/index.html
Normal file
@@ -0,0 +1,69 @@
|
||||
<!DOCTYPE html>
|
||||
<html lang="en-us" dir="ltr">
|
||||
<head><script src="/livereload.js?mindelay=10&v=2&port=1313&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">
|
||||
<meta http-equiv="X-UA-Compatible" content="IE=edge">
|
||||
<title>Python API | Formal Methods Tools</title>
|
||||
|
||||
|
||||
<meta name="keywords" content="Formal Methods Tools">
|
||||
<meta property="og:locale" content='en_US'>
|
||||
<meta property="og:type" content="article">
|
||||
<meta property="og:title" content="Python API">
|
||||
<meta property="og:description" content="">
|
||||
<meta property="og:url" content="http://localhost:1313/interactions/python-api/">
|
||||
<meta property="og:image" content="images/%!s(<nil>)">
|
||||
<link rel="canonical" href="http://localhost:1313/interactions/python-api/">
|
||||
|
||||
<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="http://localhost:1313/css/styles.e3fcfb3452c69d09414fe512e9dca31d879e4a6c47d23010fbb07eb6693d447f645d3bd2d021c0d28d0f7b4fe6f32a10e599488cdb16c6750a9a126788131917.css" integrity="sha512-4/z7NFLGnQlBT+US6dyjHYeeSmxH0jAQ+7B+tmk9RH9kXTvS0CHA0o0Pe0/m8yoQ5ZlIjNsWxnUKmhJniBMZFw==">
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</head>
|
||||
<body>
|
||||
<header>
|
||||
<h1><a href="/">Formal Methods Tools</a></h1>
|
||||
|
||||
<nav>
|
||||
<ul>
|
||||
<li>
|
||||
<a href="/">Home</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/tools/">Tools</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/taxonomies/">Taxonomies</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/about/">About</a>
|
||||
</li>
|
||||
</ul>
|
||||
</nav>
|
||||
|
||||
|
||||
</header>
|
||||
<main>
|
||||
|
||||
<h1>Python API</h1>
|
||||
|
||||
|
||||
<h2><a href="/tools/z3/">Z3</a></h2>
|
||||
|
||||
|
||||
</main>
|
||||
<footer>
|
||||
<p>Copyright 2025. All rights reserved.</p>
|
||||
|
||||
</footer>
|
||||
</body>
|
||||
</html>
|
||||
19
interactions/python-api/index.xml
Normal file
19
interactions/python-api/index.xml
Normal file
@@ -0,0 +1,19 @@
|
||||
<?xml version="1.0" encoding="utf-8" standalone="yes"?>
|
||||
<rss version="2.0" xmlns:atom="http://www.w3.org/2005/Atom">
|
||||
<channel>
|
||||
<title>Python API on Formal Methods Tools</title>
|
||||
<link>http://localhost:1313/interactions/python-api/</link>
|
||||
<description>Recent content in Python API on Formal Methods Tools</description>
|
||||
<generator>Hugo</generator>
|
||||
<language>en-us</language>
|
||||
<lastBuildDate>Fri, 02 Feb 2024 04:14:54 -0800</lastBuildDate>
|
||||
<atom:link href="http://localhost:1313/interactions/python-api/index.xml" rel="self" type="application/rss+xml" />
|
||||
<item>
|
||||
<title>Z3</title>
|
||||
<link>http://localhost:1313/tools/z3/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>http://localhost:1313/tools/z3/</guid>
|
||||
<description><p>Z3 is a high-performance SMT solver and theorem prover developed by Microsoft Research. It is widely used for checking the satisfiability of logical formulas over various theories, including arithmetic, bit-vectors, arrays, and uninterpreted functions. Z3 supports the SMT-LIB standard and provides APIs for several programming languages, making it suitable for integration into formal verification, program analysis, and constraint solving tools.</p>
<h3 id="features">Features</h3>
<ul>
<li><strong>SMT Solver:</strong> Supports a wide range of theories and quantifiers.</li>
<li><strong>Multi-language APIs:</strong> Python, C++, Java, .NET, and more.</li>
<li><strong>Cross-platform:</strong> Available on Windows, Linux, and macOS.</li>
<li><strong>Active development:</strong> Open source and maintained by Microsoft Research.</li>
<li><strong>Web Playground:</strong> Try Z3 online at <a href="https://rise4fun.com/z3">Rise4Fun</a>.</li>
</ul></description>
|
||||
</item>
|
||||
</channel>
|
||||
</rss>
|
||||
69
interactions/python-bindings/index.html
Normal file
69
interactions/python-bindings/index.html
Normal file
@@ -0,0 +1,69 @@
|
||||
<!DOCTYPE html>
|
||||
<html lang="en-us" dir="ltr">
|
||||
<head><script src="/livereload.js?mindelay=10&v=2&port=1313&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">
|
||||
<meta http-equiv="X-UA-Compatible" content="IE=edge">
|
||||
<title>Python Bindings | Formal Methods Tools</title>
|
||||
|
||||
|
||||
<meta name="keywords" content="Formal Methods Tools">
|
||||
<meta property="og:locale" content='en_US'>
|
||||
<meta property="og:type" content="article">
|
||||
<meta property="og:title" content="Python Bindings">
|
||||
<meta property="og:description" content="">
|
||||
<meta property="og:url" content="http://localhost:1313/interactions/python-bindings/">
|
||||
<meta property="og:image" content="images/%!s(<nil>)">
|
||||
<link rel="canonical" href="http://localhost:1313/interactions/python-bindings/">
|
||||
|
||||
<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="http://localhost:1313/css/styles.e3fcfb3452c69d09414fe512e9dca31d879e4a6c47d23010fbb07eb6693d447f645d3bd2d021c0d28d0f7b4fe6f32a10e599488cdb16c6750a9a126788131917.css" integrity="sha512-4/z7NFLGnQlBT+US6dyjHYeeSmxH0jAQ+7B+tmk9RH9kXTvS0CHA0o0Pe0/m8yoQ5ZlIjNsWxnUKmhJniBMZFw==">
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</head>
|
||||
<body>
|
||||
<header>
|
||||
<h1><a href="/">Formal Methods Tools</a></h1>
|
||||
|
||||
<nav>
|
||||
<ul>
|
||||
<li>
|
||||
<a href="/">Home</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/tools/">Tools</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/taxonomies/">Taxonomies</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/about/">About</a>
|
||||
</li>
|
||||
</ul>
|
||||
</nav>
|
||||
|
||||
|
||||
</header>
|
||||
<main>
|
||||
|
||||
<h1>Python Bindings</h1>
|
||||
|
||||
|
||||
<h2><a href="/tools/yices/">Yices 2</a></h2>
|
||||
|
||||
|
||||
</main>
|
||||
<footer>
|
||||
<p>Copyright 2025. All rights reserved.</p>
|
||||
|
||||
</footer>
|
||||
</body>
|
||||
</html>
|
||||
19
interactions/python-bindings/index.xml
Normal file
19
interactions/python-bindings/index.xml
Normal file
@@ -0,0 +1,19 @@
|
||||
<?xml version="1.0" encoding="utf-8" standalone="yes"?>
|
||||
<rss version="2.0" xmlns:atom="http://www.w3.org/2005/Atom">
|
||||
<channel>
|
||||
<title>Python Bindings on Formal Methods Tools</title>
|
||||
<link>http://localhost:1313/interactions/python-bindings/</link>
|
||||
<description>Recent content in Python Bindings on Formal Methods Tools</description>
|
||||
<generator>Hugo</generator>
|
||||
<language>en-us</language>
|
||||
<lastBuildDate>Fri, 02 Feb 2024 04:14:54 -0800</lastBuildDate>
|
||||
<atom:link href="http://localhost:1313/interactions/python-bindings/index.xml" rel="self" type="application/rss+xml" />
|
||||
<item>
|
||||
<title>Yices 2</title>
|
||||
<link>http://localhost:1313/tools/yices/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>http://localhost:1313/tools/yices/</guid>
|
||||
<description><p>Yices is a high-performance SMT solver and theorem prover developed by SRI International. It is widely used for checking the satisfiability of logical formulas over various theories, including arithmetic, bit-vectors, arrays, and uninterpreted functions. Yices supports the SMT-LIB standard and its own input language, and provides APIs for several programming languages, making it suitable for integration into formal verification, program analysis, and constraint solving tools.</p>
<h3 id="features">Features</h3>
<ul>
<li><strong>SMT Solver:</strong> Supports a wide range of theories and quantifiers.</li>
<li><strong>Multi-language APIs:</strong> C, OCaml, Python, and more.</li>
<li><strong>Cross-platform:</strong> Available on Windows, Linux, and macOS.</li>
<li><strong>Active development:</strong> Open source and maintained by SRI International.</li>
</ul></description>
|
||||
</item>
|
||||
</channel>
|
||||
</rss>
|
||||
69
interactions/rust-bindings/index.html
Normal file
69
interactions/rust-bindings/index.html
Normal file
@@ -0,0 +1,69 @@
|
||||
<!DOCTYPE html>
|
||||
<html lang="en-us" dir="ltr">
|
||||
<head><script src="/livereload.js?mindelay=10&v=2&port=1313&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">
|
||||
<meta http-equiv="X-UA-Compatible" content="IE=edge">
|
||||
<title>Rust Bindings | Formal Methods Tools</title>
|
||||
|
||||
|
||||
<meta name="keywords" content="Formal Methods Tools">
|
||||
<meta property="og:locale" content='en_US'>
|
||||
<meta property="og:type" content="article">
|
||||
<meta property="og:title" content="Rust Bindings">
|
||||
<meta property="og:description" content="">
|
||||
<meta property="og:url" content="http://localhost:1313/interactions/rust-bindings/">
|
||||
<meta property="og:image" content="images/%!s(<nil>)">
|
||||
<link rel="canonical" href="http://localhost:1313/interactions/rust-bindings/">
|
||||
|
||||
<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="http://localhost:1313/css/styles.e3fcfb3452c69d09414fe512e9dca31d879e4a6c47d23010fbb07eb6693d447f645d3bd2d021c0d28d0f7b4fe6f32a10e599488cdb16c6750a9a126788131917.css" integrity="sha512-4/z7NFLGnQlBT+US6dyjHYeeSmxH0jAQ+7B+tmk9RH9kXTvS0CHA0o0Pe0/m8yoQ5ZlIjNsWxnUKmhJniBMZFw==">
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</head>
|
||||
<body>
|
||||
<header>
|
||||
<h1><a href="/">Formal Methods Tools</a></h1>
|
||||
|
||||
<nav>
|
||||
<ul>
|
||||
<li>
|
||||
<a href="/">Home</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/tools/">Tools</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/taxonomies/">Taxonomies</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/about/">About</a>
|
||||
</li>
|
||||
</ul>
|
||||
</nav>
|
||||
|
||||
|
||||
</header>
|
||||
<main>
|
||||
|
||||
<h1>Rust Bindings</h1>
|
||||
|
||||
|
||||
<h2><a href="/tools/z3/">Z3</a></h2>
|
||||
|
||||
|
||||
</main>
|
||||
<footer>
|
||||
<p>Copyright 2025. All rights reserved.</p>
|
||||
|
||||
</footer>
|
||||
</body>
|
||||
</html>
|
||||
19
interactions/rust-bindings/index.xml
Normal file
19
interactions/rust-bindings/index.xml
Normal file
@@ -0,0 +1,19 @@
|
||||
<?xml version="1.0" encoding="utf-8" standalone="yes"?>
|
||||
<rss version="2.0" xmlns:atom="http://www.w3.org/2005/Atom">
|
||||
<channel>
|
||||
<title>Rust Bindings on Formal Methods Tools</title>
|
||||
<link>http://localhost:1313/interactions/rust-bindings/</link>
|
||||
<description>Recent content in Rust Bindings on Formal Methods Tools</description>
|
||||
<generator>Hugo</generator>
|
||||
<language>en-us</language>
|
||||
<lastBuildDate>Fri, 02 Feb 2024 04:14:54 -0800</lastBuildDate>
|
||||
<atom:link href="http://localhost:1313/interactions/rust-bindings/index.xml" rel="self" type="application/rss+xml" />
|
||||
<item>
|
||||
<title>Z3</title>
|
||||
<link>http://localhost:1313/tools/z3/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>http://localhost:1313/tools/z3/</guid>
|
||||
<description><p>Z3 is a high-performance SMT solver and theorem prover developed by Microsoft Research. It is widely used for checking the satisfiability of logical formulas over various theories, including arithmetic, bit-vectors, arrays, and uninterpreted functions. Z3 supports the SMT-LIB standard and provides APIs for several programming languages, making it suitable for integration into formal verification, program analysis, and constraint solving tools.</p>
<h3 id="features">Features</h3>
<ul>
<li><strong>SMT Solver:</strong> Supports a wide range of theories and quantifiers.</li>
<li><strong>Multi-language APIs:</strong> Python, C++, Java, .NET, and more.</li>
<li><strong>Cross-platform:</strong> Available on Windows, Linux, and macOS.</li>
<li><strong>Active development:</strong> Open source and maintained by Microsoft Research.</li>
<li><strong>Web Playground:</strong> Try Z3 online at <a href="https://rise4fun.com/z3">Rise4Fun</a>.</li>
</ul></description>
|
||||
</item>
|
||||
</channel>
|
||||
</rss>
|
||||
69
languages/c#/index.html
Normal file
69
languages/c#/index.html
Normal file
@@ -0,0 +1,69 @@
|
||||
<!DOCTYPE html>
|
||||
<html lang="en-us" dir="ltr">
|
||||
<head><script src="/livereload.js?mindelay=10&v=2&port=1313&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">
|
||||
<meta http-equiv="X-UA-Compatible" content="IE=edge">
|
||||
<title>C# | Formal Methods Tools</title>
|
||||
|
||||
|
||||
<meta name="keywords" content="Formal Methods Tools">
|
||||
<meta property="og:locale" content='en_US'>
|
||||
<meta property="og:type" content="article">
|
||||
<meta property="og:title" content="C#">
|
||||
<meta property="og:description" content="">
|
||||
<meta property="og:url" content="http://localhost:1313/languages/c%23/">
|
||||
<meta property="og:image" content="images/%!s(<nil>)">
|
||||
<link rel="canonical" href="http://localhost:1313/languages/c%23/">
|
||||
|
||||
<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="http://localhost:1313/css/styles.e3fcfb3452c69d09414fe512e9dca31d879e4a6c47d23010fbb07eb6693d447f645d3bd2d021c0d28d0f7b4fe6f32a10e599488cdb16c6750a9a126788131917.css" integrity="sha512-4/z7NFLGnQlBT+US6dyjHYeeSmxH0jAQ+7B+tmk9RH9kXTvS0CHA0o0Pe0/m8yoQ5ZlIjNsWxnUKmhJniBMZFw==">
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</head>
|
||||
<body>
|
||||
<header>
|
||||
<h1><a href="/">Formal Methods Tools</a></h1>
|
||||
|
||||
<nav>
|
||||
<ul>
|
||||
<li>
|
||||
<a href="/">Home</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/tools/">Tools</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/taxonomies/">Taxonomies</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/about/">About</a>
|
||||
</li>
|
||||
</ul>
|
||||
</nav>
|
||||
|
||||
|
||||
</header>
|
||||
<main>
|
||||
|
||||
<h1>C#</h1>
|
||||
|
||||
|
||||
<h2><a href="/tools/z3/">Z3</a></h2>
|
||||
|
||||
|
||||
</main>
|
||||
<footer>
|
||||
<p>Copyright 2025. All rights reserved.</p>
|
||||
|
||||
</footer>
|
||||
</body>
|
||||
</html>
|
||||
19
languages/c#/index.xml
Normal file
19
languages/c#/index.xml
Normal file
@@ -0,0 +1,19 @@
|
||||
<?xml version="1.0" encoding="utf-8" standalone="yes"?>
|
||||
<rss version="2.0" xmlns:atom="http://www.w3.org/2005/Atom">
|
||||
<channel>
|
||||
<title>C# on Formal Methods Tools</title>
|
||||
<link>http://localhost:1313/languages/c%23/</link>
|
||||
<description>Recent content in C# on Formal Methods Tools</description>
|
||||
<generator>Hugo</generator>
|
||||
<language>en-us</language>
|
||||
<lastBuildDate>Fri, 02 Feb 2024 04:14:54 -0800</lastBuildDate>
|
||||
<atom:link href="http://localhost:1313/languages/c%23/index.xml" rel="self" type="application/rss+xml" />
|
||||
<item>
|
||||
<title>Z3</title>
|
||||
<link>http://localhost:1313/tools/z3/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>http://localhost:1313/tools/z3/</guid>
|
||||
<description><p>Z3 is a high-performance SMT solver and theorem prover developed by Microsoft Research. It is widely used for checking the satisfiability of logical formulas over various theories, including arithmetic, bit-vectors, arrays, and uninterpreted functions. Z3 supports the SMT-LIB standard and provides APIs for several programming languages, making it suitable for integration into formal verification, program analysis, and constraint solving tools.</p>
<h3 id="features">Features</h3>
<ul>
<li><strong>SMT Solver:</strong> Supports a wide range of theories and quantifiers.</li>
<li><strong>Multi-language APIs:</strong> Python, C++, Java, .NET, and more.</li>
<li><strong>Cross-platform:</strong> Available on Windows, Linux, and macOS.</li>
<li><strong>Active development:</strong> Open source and maintained by Microsoft Research.</li>
<li><strong>Web Playground:</strong> Try Z3 online at <a href="https://rise4fun.com/z3">Rise4Fun</a>.</li>
</ul></description>
|
||||
</item>
|
||||
</channel>
|
||||
</rss>
|
||||
69
languages/c++/index.html
Normal file
69
languages/c++/index.html
Normal file
@@ -0,0 +1,69 @@
|
||||
<!DOCTYPE html>
|
||||
<html lang="en-us" dir="ltr">
|
||||
<head><script src="/livereload.js?mindelay=10&v=2&port=1313&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">
|
||||
<meta http-equiv="X-UA-Compatible" content="IE=edge">
|
||||
<title>C++ | Formal Methods Tools</title>
|
||||
|
||||
|
||||
<meta name="keywords" content="Formal Methods Tools">
|
||||
<meta property="og:locale" content='en_US'>
|
||||
<meta property="og:type" content="article">
|
||||
<meta property="og:title" content="C++">
|
||||
<meta property="og:description" content="">
|
||||
<meta property="og:url" content="http://localhost:1313/languages/c++/">
|
||||
<meta property="og:image" content="images/%!s(<nil>)">
|
||||
<link rel="canonical" href="http://localhost:1313/languages/c++/">
|
||||
|
||||
<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="http://localhost:1313/css/styles.e3fcfb3452c69d09414fe512e9dca31d879e4a6c47d23010fbb07eb6693d447f645d3bd2d021c0d28d0f7b4fe6f32a10e599488cdb16c6750a9a126788131917.css" integrity="sha512-4/z7NFLGnQlBT+US6dyjHYeeSmxH0jAQ+7B+tmk9RH9kXTvS0CHA0o0Pe0/m8yoQ5ZlIjNsWxnUKmhJniBMZFw==">
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</head>
|
||||
<body>
|
||||
<header>
|
||||
<h1><a href="/">Formal Methods Tools</a></h1>
|
||||
|
||||
<nav>
|
||||
<ul>
|
||||
<li>
|
||||
<a href="/">Home</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/tools/">Tools</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/taxonomies/">Taxonomies</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/about/">About</a>
|
||||
</li>
|
||||
</ul>
|
||||
</nav>
|
||||
|
||||
|
||||
</header>
|
||||
<main>
|
||||
|
||||
<h1>C++</h1>
|
||||
|
||||
|
||||
<h2><a href="/tools/z3/">Z3</a></h2>
|
||||
|
||||
|
||||
</main>
|
||||
<footer>
|
||||
<p>Copyright 2025. All rights reserved.</p>
|
||||
|
||||
</footer>
|
||||
</body>
|
||||
</html>
|
||||
19
languages/c++/index.xml
Normal file
19
languages/c++/index.xml
Normal file
@@ -0,0 +1,19 @@
|
||||
<?xml version="1.0" encoding="utf-8" standalone="yes"?>
|
||||
<rss version="2.0" xmlns:atom="http://www.w3.org/2005/Atom">
|
||||
<channel>
|
||||
<title>C++ on Formal Methods Tools</title>
|
||||
<link>http://localhost:1313/languages/c++/</link>
|
||||
<description>Recent content in C++ on Formal Methods Tools</description>
|
||||
<generator>Hugo</generator>
|
||||
<language>en-us</language>
|
||||
<lastBuildDate>Fri, 02 Feb 2024 04:14:54 -0800</lastBuildDate>
|
||||
<atom:link href="http://localhost:1313/languages/c++/index.xml" rel="self" type="application/rss+xml" />
|
||||
<item>
|
||||
<title>Z3</title>
|
||||
<link>http://localhost:1313/tools/z3/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>http://localhost:1313/tools/z3/</guid>
|
||||
<description><p>Z3 is a high-performance SMT solver and theorem prover developed by Microsoft Research. It is widely used for checking the satisfiability of logical formulas over various theories, including arithmetic, bit-vectors, arrays, and uninterpreted functions. Z3 supports the SMT-LIB standard and provides APIs for several programming languages, making it suitable for integration into formal verification, program analysis, and constraint solving tools.</p>
<h3 id="features">Features</h3>
<ul>
<li><strong>SMT Solver:</strong> Supports a wide range of theories and quantifiers.</li>
<li><strong>Multi-language APIs:</strong> Python, C++, Java, .NET, and more.</li>
<li><strong>Cross-platform:</strong> Available on Windows, Linux, and macOS.</li>
<li><strong>Active development:</strong> Open source and maintained by Microsoft Research.</li>
<li><strong>Web Playground:</strong> Try Z3 online at <a href="https://rise4fun.com/z3">Rise4Fun</a>.</li>
</ul></description>
|
||||
</item>
|
||||
</channel>
|
||||
</rss>
|
||||
69
languages/c/index.html
Normal file
69
languages/c/index.html
Normal file
@@ -0,0 +1,69 @@
|
||||
<!DOCTYPE html>
|
||||
<html lang="en-us" dir="ltr">
|
||||
<head><script src="/livereload.js?mindelay=10&v=2&port=1313&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">
|
||||
<meta http-equiv="X-UA-Compatible" content="IE=edge">
|
||||
<title>C | Formal Methods Tools</title>
|
||||
|
||||
|
||||
<meta name="keywords" content="Formal Methods Tools">
|
||||
<meta property="og:locale" content='en_US'>
|
||||
<meta property="og:type" content="article">
|
||||
<meta property="og:title" content="C">
|
||||
<meta property="og:description" content="">
|
||||
<meta property="og:url" content="http://localhost:1313/languages/c/">
|
||||
<meta property="og:image" content="images/%!s(<nil>)">
|
||||
<link rel="canonical" href="http://localhost:1313/languages/c/">
|
||||
|
||||
<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="http://localhost:1313/css/styles.e3fcfb3452c69d09414fe512e9dca31d879e4a6c47d23010fbb07eb6693d447f645d3bd2d021c0d28d0f7b4fe6f32a10e599488cdb16c6750a9a126788131917.css" integrity="sha512-4/z7NFLGnQlBT+US6dyjHYeeSmxH0jAQ+7B+tmk9RH9kXTvS0CHA0o0Pe0/m8yoQ5ZlIjNsWxnUKmhJniBMZFw==">
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</head>
|
||||
<body>
|
||||
<header>
|
||||
<h1><a href="/">Formal Methods Tools</a></h1>
|
||||
|
||||
<nav>
|
||||
<ul>
|
||||
<li>
|
||||
<a href="/">Home</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/tools/">Tools</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/taxonomies/">Taxonomies</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/about/">About</a>
|
||||
</li>
|
||||
</ul>
|
||||
</nav>
|
||||
|
||||
|
||||
</header>
|
||||
<main>
|
||||
|
||||
<h1>C</h1>
|
||||
|
||||
|
||||
<h2><a href="/tools/yices/">Yices 2</a></h2>
|
||||
|
||||
|
||||
</main>
|
||||
<footer>
|
||||
<p>Copyright 2025. All rights reserved.</p>
|
||||
|
||||
</footer>
|
||||
</body>
|
||||
</html>
|
||||
19
languages/c/index.xml
Normal file
19
languages/c/index.xml
Normal file
@@ -0,0 +1,19 @@
|
||||
<?xml version="1.0" encoding="utf-8" standalone="yes"?>
|
||||
<rss version="2.0" xmlns:atom="http://www.w3.org/2005/Atom">
|
||||
<channel>
|
||||
<title>C on Formal Methods Tools</title>
|
||||
<link>http://localhost:1313/languages/c/</link>
|
||||
<description>Recent content in C on Formal Methods Tools</description>
|
||||
<generator>Hugo</generator>
|
||||
<language>en-us</language>
|
||||
<lastBuildDate>Fri, 02 Feb 2024 04:14:54 -0800</lastBuildDate>
|
||||
<atom:link href="http://localhost:1313/languages/c/index.xml" rel="self" type="application/rss+xml" />
|
||||
<item>
|
||||
<title>Yices 2</title>
|
||||
<link>http://localhost:1313/tools/yices/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>http://localhost:1313/tools/yices/</guid>
|
||||
<description><p>Yices is a high-performance SMT solver and theorem prover developed by SRI International. It is widely used for checking the satisfiability of logical formulas over various theories, including arithmetic, bit-vectors, arrays, and uninterpreted functions. Yices supports the SMT-LIB standard and its own input language, and provides APIs for several programming languages, making it suitable for integration into formal verification, program analysis, and constraint solving tools.</p>
<h3 id="features">Features</h3>
<ul>
<li><strong>SMT Solver:</strong> Supports a wide range of theories and quantifiers.</li>
<li><strong>Multi-language APIs:</strong> C, OCaml, Python, and more.</li>
<li><strong>Cross-platform:</strong> Available on Windows, Linux, and macOS.</li>
<li><strong>Active development:</strong> Open source and maintained by SRI International.</li>
</ul></description>
|
||||
</item>
|
||||
</channel>
|
||||
</rss>
|
||||
@@ -1,6 +1,6 @@
|
||||
<!DOCTYPE html>
|
||||
<html lang="en-us" dir="ltr">
|
||||
<head>
|
||||
<head><script src="/livereload.js?mindelay=10&v=2&port=1313&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">
|
||||
@@ -13,16 +13,16 @@
|
||||
<meta property="og:type" content="article">
|
||||
<meta property="og:title" content="Languages">
|
||||
<meta property="og:description" content="">
|
||||
<meta property="og:url" content="https://example.org/languages/">
|
||||
<meta property="og:url" content="http://localhost:1313/languages/">
|
||||
<meta property="og:image" content="images/%!s(<nil>)">
|
||||
<link rel="canonical" href="https://example.org/languages/">
|
||||
<link rel="canonical" href="http://localhost:1313/languages/">
|
||||
|
||||
<link rel="apple-touch-icon" sizes="180x180" href='https://example.org/apple-touch-icon.png'>
|
||||
<link rel="icon" type="image/png" sizes="32x32" href='https://example.org/favicon-32x32.png'>
|
||||
<link rel="icon" type="image/png" sizes='16x16' href='https://example.org/favicon-16x16.png'>
|
||||
<link rel="manifest" href='https://example.org/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://example.org/css/styles.fc7cf65388be07f2e53293132dd0220e34d9861f57de4b336d64dd03a3502a9befbea05606442d0a501005442835a864361b9a51b4b51acbf28df37530f61f31.css" integrity="sha512-/Hz2U4i+B/LlMpMTLdAiDjTZhh9X3kszbWTdA6NQKpvvvqBWBkQtClAQBUQoNahkNhuaUbS1GsvyjfN1MPYfMQ==">
|
||||
<link rel="stylesheet" href="http://localhost:1313/css/styles.e3fcfb3452c69d09414fe512e9dca31d879e4a6c47d23010fbb07eb6693d447f645d3bd2d021c0d28d0f7b4fe6f32a10e599488cdb16c6750a9a126788131917.css" integrity="sha512-4/z7NFLGnQlBT+US6dyjHYeeSmxH0jAQ+7B+tmk9RH9kXTvS0CHA0o0Pe0/m8yoQ5ZlIjNsWxnUKmhJniBMZFw==">
|
||||
|
||||
|
||||
|
||||
@@ -70,10 +70,136 @@
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="languages_tttt"
|
||||
style="background:rgba(229,115,100,0.4)"
|
||||
href="/languages/tttt">
|
||||
Tttt
|
||||
id="languages_c"
|
||||
style="background:rgba(13,97,248,0.4)"
|
||||
href="/languages/c">
|
||||
C
|
||||
</a>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="languages_c"
|
||||
style="background:rgba(215,239,161,0.4)"
|
||||
href="/languages/c">
|
||||
C#
|
||||
</a>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="languages_c++"
|
||||
style="background:rgba(246,248,124,0.4)"
|
||||
href="/languages/c++">
|
||||
C++
|
||||
</a>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="languages_java"
|
||||
style="background:rgba(213,35,135,0.4)"
|
||||
href="/languages/java">
|
||||
Java
|
||||
</a>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="languages_ocaml"
|
||||
style="background:rgba(29,22,137,0.4)"
|
||||
href="/languages/ocaml">
|
||||
OCaml
|
||||
</a>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="languages_python"
|
||||
style="background:rgba(167,245,243,0.4)"
|
||||
href="/languages/python">
|
||||
Python
|
||||
</a>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="languages_smt-lib"
|
||||
style="background:rgba(62,225,228,0.4)"
|
||||
href="/languages/smt-lib">
|
||||
SMT-LIB
|
||||
</a>
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
<a
|
||||
class="term-link"
|
||||
id="languages_yices-language"
|
||||
style="background:rgba(54,179,229,0.4)"
|
||||
href="/languages/yices-language">
|
||||
Yices Language
|
||||
</a>
|
||||
|
||||
|
||||
|
||||
@@ -2,17 +2,66 @@
|
||||
<rss version="2.0" xmlns:atom="http://www.w3.org/2005/Atom">
|
||||
<channel>
|
||||
<title>Languages on Formal Methods Tools</title>
|
||||
<link>https://example.org/languages/</link>
|
||||
<link>http://localhost:1313/languages/</link>
|
||||
<description>Recent content in Languages on Formal Methods Tools</description>
|
||||
<generator>Hugo</generator>
|
||||
<language>en-us</language>
|
||||
<lastBuildDate>Fri, 02 Feb 2024 04:14:54 -0800</lastBuildDate>
|
||||
<atom:link href="https://example.org/languages/index.xml" rel="self" type="application/rss+xml" />
|
||||
<atom:link href="http://localhost:1313/languages/index.xml" rel="self" type="application/rss+xml" />
|
||||
<item>
|
||||
<title>Tttt</title>
|
||||
<link>https://example.org/languages/tttt/</link>
|
||||
<title>C</title>
|
||||
<link>http://localhost:1313/languages/c/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>https://example.org/languages/tttt/</guid>
|
||||
<guid>http://localhost:1313/languages/c/</guid>
|
||||
<description></description>
|
||||
</item>
|
||||
<item>
|
||||
<title>C#</title>
|
||||
<link>http://localhost:1313/languages/c%23/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>http://localhost:1313/languages/c%23/</guid>
|
||||
<description></description>
|
||||
</item>
|
||||
<item>
|
||||
<title>C++</title>
|
||||
<link>http://localhost:1313/languages/c++/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>http://localhost:1313/languages/c++/</guid>
|
||||
<description></description>
|
||||
</item>
|
||||
<item>
|
||||
<title>Java</title>
|
||||
<link>http://localhost:1313/languages/java/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>http://localhost:1313/languages/java/</guid>
|
||||
<description></description>
|
||||
</item>
|
||||
<item>
|
||||
<title>OCaml</title>
|
||||
<link>http://localhost:1313/languages/ocaml/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>http://localhost:1313/languages/ocaml/</guid>
|
||||
<description></description>
|
||||
</item>
|
||||
<item>
|
||||
<title>Python</title>
|
||||
<link>http://localhost:1313/languages/python/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>http://localhost:1313/languages/python/</guid>
|
||||
<description></description>
|
||||
</item>
|
||||
<item>
|
||||
<title>SMT-LIB</title>
|
||||
<link>http://localhost:1313/languages/smt-lib/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>http://localhost:1313/languages/smt-lib/</guid>
|
||||
<description></description>
|
||||
</item>
|
||||
<item>
|
||||
<title>Yices Language</title>
|
||||
<link>http://localhost:1313/languages/yices-language/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>http://localhost:1313/languages/yices-language/</guid>
|
||||
<description></description>
|
||||
</item>
|
||||
</channel>
|
||||
|
||||
69
languages/java/index.html
Normal file
69
languages/java/index.html
Normal file
@@ -0,0 +1,69 @@
|
||||
<!DOCTYPE html>
|
||||
<html lang="en-us" dir="ltr">
|
||||
<head><script src="/livereload.js?mindelay=10&v=2&port=1313&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">
|
||||
<meta http-equiv="X-UA-Compatible" content="IE=edge">
|
||||
<title>Java | Formal Methods Tools</title>
|
||||
|
||||
|
||||
<meta name="keywords" content="Formal Methods Tools">
|
||||
<meta property="og:locale" content='en_US'>
|
||||
<meta property="og:type" content="article">
|
||||
<meta property="og:title" content="Java">
|
||||
<meta property="og:description" content="">
|
||||
<meta property="og:url" content="http://localhost:1313/languages/java/">
|
||||
<meta property="og:image" content="images/%!s(<nil>)">
|
||||
<link rel="canonical" href="http://localhost:1313/languages/java/">
|
||||
|
||||
<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="http://localhost:1313/css/styles.e3fcfb3452c69d09414fe512e9dca31d879e4a6c47d23010fbb07eb6693d447f645d3bd2d021c0d28d0f7b4fe6f32a10e599488cdb16c6750a9a126788131917.css" integrity="sha512-4/z7NFLGnQlBT+US6dyjHYeeSmxH0jAQ+7B+tmk9RH9kXTvS0CHA0o0Pe0/m8yoQ5ZlIjNsWxnUKmhJniBMZFw==">
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</head>
|
||||
<body>
|
||||
<header>
|
||||
<h1><a href="/">Formal Methods Tools</a></h1>
|
||||
|
||||
<nav>
|
||||
<ul>
|
||||
<li>
|
||||
<a href="/">Home</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/tools/">Tools</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/taxonomies/">Taxonomies</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/about/">About</a>
|
||||
</li>
|
||||
</ul>
|
||||
</nav>
|
||||
|
||||
|
||||
</header>
|
||||
<main>
|
||||
|
||||
<h1>Java</h1>
|
||||
|
||||
|
||||
<h2><a href="/tools/z3/">Z3</a></h2>
|
||||
|
||||
|
||||
</main>
|
||||
<footer>
|
||||
<p>Copyright 2025. All rights reserved.</p>
|
||||
|
||||
</footer>
|
||||
</body>
|
||||
</html>
|
||||
19
languages/java/index.xml
Normal file
19
languages/java/index.xml
Normal file
@@ -0,0 +1,19 @@
|
||||
<?xml version="1.0" encoding="utf-8" standalone="yes"?>
|
||||
<rss version="2.0" xmlns:atom="http://www.w3.org/2005/Atom">
|
||||
<channel>
|
||||
<title>Java on Formal Methods Tools</title>
|
||||
<link>http://localhost:1313/languages/java/</link>
|
||||
<description>Recent content in Java on Formal Methods Tools</description>
|
||||
<generator>Hugo</generator>
|
||||
<language>en-us</language>
|
||||
<lastBuildDate>Fri, 02 Feb 2024 04:14:54 -0800</lastBuildDate>
|
||||
<atom:link href="http://localhost:1313/languages/java/index.xml" rel="self" type="application/rss+xml" />
|
||||
<item>
|
||||
<title>Z3</title>
|
||||
<link>http://localhost:1313/tools/z3/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>http://localhost:1313/tools/z3/</guid>
|
||||
<description><p>Z3 is a high-performance SMT solver and theorem prover developed by Microsoft Research. It is widely used for checking the satisfiability of logical formulas over various theories, including arithmetic, bit-vectors, arrays, and uninterpreted functions. Z3 supports the SMT-LIB standard and provides APIs for several programming languages, making it suitable for integration into formal verification, program analysis, and constraint solving tools.</p>
<h3 id="features">Features</h3>
<ul>
<li><strong>SMT Solver:</strong> Supports a wide range of theories and quantifiers.</li>
<li><strong>Multi-language APIs:</strong> Python, C++, Java, .NET, and more.</li>
<li><strong>Cross-platform:</strong> Available on Windows, Linux, and macOS.</li>
<li><strong>Active development:</strong> Open source and maintained by Microsoft Research.</li>
<li><strong>Web Playground:</strong> Try Z3 online at <a href="https://rise4fun.com/z3">Rise4Fun</a>.</li>
</ul></description>
|
||||
</item>
|
||||
</channel>
|
||||
</rss>
|
||||
69
languages/ocaml/index.html
Normal file
69
languages/ocaml/index.html
Normal file
@@ -0,0 +1,69 @@
|
||||
<!DOCTYPE html>
|
||||
<html lang="en-us" dir="ltr">
|
||||
<head><script src="/livereload.js?mindelay=10&v=2&port=1313&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">
|
||||
<meta http-equiv="X-UA-Compatible" content="IE=edge">
|
||||
<title>OCaml | Formal Methods Tools</title>
|
||||
|
||||
|
||||
<meta name="keywords" content="Formal Methods Tools">
|
||||
<meta property="og:locale" content='en_US'>
|
||||
<meta property="og:type" content="article">
|
||||
<meta property="og:title" content="OCaml">
|
||||
<meta property="og:description" content="">
|
||||
<meta property="og:url" content="http://localhost:1313/languages/ocaml/">
|
||||
<meta property="og:image" content="images/%!s(<nil>)">
|
||||
<link rel="canonical" href="http://localhost:1313/languages/ocaml/">
|
||||
|
||||
<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="http://localhost:1313/css/styles.e3fcfb3452c69d09414fe512e9dca31d879e4a6c47d23010fbb07eb6693d447f645d3bd2d021c0d28d0f7b4fe6f32a10e599488cdb16c6750a9a126788131917.css" integrity="sha512-4/z7NFLGnQlBT+US6dyjHYeeSmxH0jAQ+7B+tmk9RH9kXTvS0CHA0o0Pe0/m8yoQ5ZlIjNsWxnUKmhJniBMZFw==">
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</head>
|
||||
<body>
|
||||
<header>
|
||||
<h1><a href="/">Formal Methods Tools</a></h1>
|
||||
|
||||
<nav>
|
||||
<ul>
|
||||
<li>
|
||||
<a href="/">Home</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/tools/">Tools</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/taxonomies/">Taxonomies</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/about/">About</a>
|
||||
</li>
|
||||
</ul>
|
||||
</nav>
|
||||
|
||||
|
||||
</header>
|
||||
<main>
|
||||
|
||||
<h1>OCaml</h1>
|
||||
|
||||
|
||||
<h2><a href="/tools/yices/">Yices 2</a></h2>
|
||||
|
||||
|
||||
</main>
|
||||
<footer>
|
||||
<p>Copyright 2025. All rights reserved.</p>
|
||||
|
||||
</footer>
|
||||
</body>
|
||||
</html>
|
||||
19
languages/ocaml/index.xml
Normal file
19
languages/ocaml/index.xml
Normal file
@@ -0,0 +1,19 @@
|
||||
<?xml version="1.0" encoding="utf-8" standalone="yes"?>
|
||||
<rss version="2.0" xmlns:atom="http://www.w3.org/2005/Atom">
|
||||
<channel>
|
||||
<title>OCaml on Formal Methods Tools</title>
|
||||
<link>http://localhost:1313/languages/ocaml/</link>
|
||||
<description>Recent content in OCaml on Formal Methods Tools</description>
|
||||
<generator>Hugo</generator>
|
||||
<language>en-us</language>
|
||||
<lastBuildDate>Fri, 02 Feb 2024 04:14:54 -0800</lastBuildDate>
|
||||
<atom:link href="http://localhost:1313/languages/ocaml/index.xml" rel="self" type="application/rss+xml" />
|
||||
<item>
|
||||
<title>Yices 2</title>
|
||||
<link>http://localhost:1313/tools/yices/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>http://localhost:1313/tools/yices/</guid>
|
||||
<description><p>Yices is a high-performance SMT solver and theorem prover developed by SRI International. It is widely used for checking the satisfiability of logical formulas over various theories, including arithmetic, bit-vectors, arrays, and uninterpreted functions. Yices supports the SMT-LIB standard and its own input language, and provides APIs for several programming languages, making it suitable for integration into formal verification, program analysis, and constraint solving tools.</p>
<h3 id="features">Features</h3>
<ul>
<li><strong>SMT Solver:</strong> Supports a wide range of theories and quantifiers.</li>
<li><strong>Multi-language APIs:</strong> C, OCaml, Python, and more.</li>
<li><strong>Cross-platform:</strong> Available on Windows, Linux, and macOS.</li>
<li><strong>Active development:</strong> Open source and maintained by SRI International.</li>
</ul></description>
|
||||
</item>
|
||||
</channel>
|
||||
</rss>
|
||||
71
languages/python/index.html
Normal file
71
languages/python/index.html
Normal file
@@ -0,0 +1,71 @@
|
||||
<!DOCTYPE html>
|
||||
<html lang="en-us" dir="ltr">
|
||||
<head><script src="/livereload.js?mindelay=10&v=2&port=1313&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">
|
||||
<meta http-equiv="X-UA-Compatible" content="IE=edge">
|
||||
<title>Python | Formal Methods Tools</title>
|
||||
|
||||
|
||||
<meta name="keywords" content="Formal Methods Tools">
|
||||
<meta property="og:locale" content='en_US'>
|
||||
<meta property="og:type" content="article">
|
||||
<meta property="og:title" content="Python">
|
||||
<meta property="og:description" content="">
|
||||
<meta property="og:url" content="http://localhost:1313/languages/python/">
|
||||
<meta property="og:image" content="images/%!s(<nil>)">
|
||||
<link rel="canonical" href="http://localhost:1313/languages/python/">
|
||||
|
||||
<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="http://localhost:1313/css/styles.e3fcfb3452c69d09414fe512e9dca31d879e4a6c47d23010fbb07eb6693d447f645d3bd2d021c0d28d0f7b4fe6f32a10e599488cdb16c6750a9a126788131917.css" integrity="sha512-4/z7NFLGnQlBT+US6dyjHYeeSmxH0jAQ+7B+tmk9RH9kXTvS0CHA0o0Pe0/m8yoQ5ZlIjNsWxnUKmhJniBMZFw==">
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</head>
|
||||
<body>
|
||||
<header>
|
||||
<h1><a href="/">Formal Methods Tools</a></h1>
|
||||
|
||||
<nav>
|
||||
<ul>
|
||||
<li>
|
||||
<a href="/">Home</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/tools/">Tools</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/taxonomies/">Taxonomies</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/about/">About</a>
|
||||
</li>
|
||||
</ul>
|
||||
</nav>
|
||||
|
||||
|
||||
</header>
|
||||
<main>
|
||||
|
||||
<h1>Python</h1>
|
||||
|
||||
|
||||
<h2><a href="/tools/yices/">Yices 2</a></h2>
|
||||
|
||||
<h2><a href="/tools/z3/">Z3</a></h2>
|
||||
|
||||
|
||||
</main>
|
||||
<footer>
|
||||
<p>Copyright 2025. All rights reserved.</p>
|
||||
|
||||
</footer>
|
||||
</body>
|
||||
</html>
|
||||
26
languages/python/index.xml
Normal file
26
languages/python/index.xml
Normal file
@@ -0,0 +1,26 @@
|
||||
<?xml version="1.0" encoding="utf-8" standalone="yes"?>
|
||||
<rss version="2.0" xmlns:atom="http://www.w3.org/2005/Atom">
|
||||
<channel>
|
||||
<title>Python on Formal Methods Tools</title>
|
||||
<link>http://localhost:1313/languages/python/</link>
|
||||
<description>Recent content in Python on Formal Methods Tools</description>
|
||||
<generator>Hugo</generator>
|
||||
<language>en-us</language>
|
||||
<lastBuildDate>Fri, 02 Feb 2024 04:14:54 -0800</lastBuildDate>
|
||||
<atom:link href="http://localhost:1313/languages/python/index.xml" rel="self" type="application/rss+xml" />
|
||||
<item>
|
||||
<title>Yices 2</title>
|
||||
<link>http://localhost:1313/tools/yices/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>http://localhost:1313/tools/yices/</guid>
|
||||
<description><p>Yices is a high-performance SMT solver and theorem prover developed by SRI International. It is widely used for checking the satisfiability of logical formulas over various theories, including arithmetic, bit-vectors, arrays, and uninterpreted functions. Yices supports the SMT-LIB standard and its own input language, and provides APIs for several programming languages, making it suitable for integration into formal verification, program analysis, and constraint solving tools.</p>
<h3 id="features">Features</h3>
<ul>
<li><strong>SMT Solver:</strong> Supports a wide range of theories and quantifiers.</li>
<li><strong>Multi-language APIs:</strong> C, OCaml, Python, and more.</li>
<li><strong>Cross-platform:</strong> Available on Windows, Linux, and macOS.</li>
<li><strong>Active development:</strong> Open source and maintained by SRI International.</li>
</ul></description>
|
||||
</item>
|
||||
<item>
|
||||
<title>Z3</title>
|
||||
<link>http://localhost:1313/tools/z3/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>http://localhost:1313/tools/z3/</guid>
|
||||
<description><p>Z3 is a high-performance SMT solver and theorem prover developed by Microsoft Research. It is widely used for checking the satisfiability of logical formulas over various theories, including arithmetic, bit-vectors, arrays, and uninterpreted functions. Z3 supports the SMT-LIB standard and provides APIs for several programming languages, making it suitable for integration into formal verification, program analysis, and constraint solving tools.</p>
<h3 id="features">Features</h3>
<ul>
<li><strong>SMT Solver:</strong> Supports a wide range of theories and quantifiers.</li>
<li><strong>Multi-language APIs:</strong> Python, C++, Java, .NET, and more.</li>
<li><strong>Cross-platform:</strong> Available on Windows, Linux, and macOS.</li>
<li><strong>Active development:</strong> Open source and maintained by Microsoft Research.</li>
<li><strong>Web Playground:</strong> Try Z3 online at <a href="https://rise4fun.com/z3">Rise4Fun</a>.</li>
</ul></description>
|
||||
</item>
|
||||
</channel>
|
||||
</rss>
|
||||
71
languages/smt-lib/index.html
Normal file
71
languages/smt-lib/index.html
Normal file
@@ -0,0 +1,71 @@
|
||||
<!DOCTYPE html>
|
||||
<html lang="en-us" dir="ltr">
|
||||
<head><script src="/livereload.js?mindelay=10&v=2&port=1313&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">
|
||||
<meta http-equiv="X-UA-Compatible" content="IE=edge">
|
||||
<title>SMT-LIB | Formal Methods Tools</title>
|
||||
|
||||
|
||||
<meta name="keywords" content="Formal Methods Tools">
|
||||
<meta property="og:locale" content='en_US'>
|
||||
<meta property="og:type" content="article">
|
||||
<meta property="og:title" content="SMT-LIB">
|
||||
<meta property="og:description" content="">
|
||||
<meta property="og:url" content="http://localhost:1313/languages/smt-lib/">
|
||||
<meta property="og:image" content="images/%!s(<nil>)">
|
||||
<link rel="canonical" href="http://localhost:1313/languages/smt-lib/">
|
||||
|
||||
<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="http://localhost:1313/css/styles.e3fcfb3452c69d09414fe512e9dca31d879e4a6c47d23010fbb07eb6693d447f645d3bd2d021c0d28d0f7b4fe6f32a10e599488cdb16c6750a9a126788131917.css" integrity="sha512-4/z7NFLGnQlBT+US6dyjHYeeSmxH0jAQ+7B+tmk9RH9kXTvS0CHA0o0Pe0/m8yoQ5ZlIjNsWxnUKmhJniBMZFw==">
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</head>
|
||||
<body>
|
||||
<header>
|
||||
<h1><a href="/">Formal Methods Tools</a></h1>
|
||||
|
||||
<nav>
|
||||
<ul>
|
||||
<li>
|
||||
<a href="/">Home</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/tools/">Tools</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/taxonomies/">Taxonomies</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/about/">About</a>
|
||||
</li>
|
||||
</ul>
|
||||
</nav>
|
||||
|
||||
|
||||
</header>
|
||||
<main>
|
||||
|
||||
<h1>SMT-LIB</h1>
|
||||
|
||||
|
||||
<h2><a href="/tools/yices/">Yices 2</a></h2>
|
||||
|
||||
<h2><a href="/tools/z3/">Z3</a></h2>
|
||||
|
||||
|
||||
</main>
|
||||
<footer>
|
||||
<p>Copyright 2025. All rights reserved.</p>
|
||||
|
||||
</footer>
|
||||
</body>
|
||||
</html>
|
||||
26
languages/smt-lib/index.xml
Normal file
26
languages/smt-lib/index.xml
Normal file
@@ -0,0 +1,26 @@
|
||||
<?xml version="1.0" encoding="utf-8" standalone="yes"?>
|
||||
<rss version="2.0" xmlns:atom="http://www.w3.org/2005/Atom">
|
||||
<channel>
|
||||
<title>SMT-LIB on Formal Methods Tools</title>
|
||||
<link>http://localhost:1313/languages/smt-lib/</link>
|
||||
<description>Recent content in SMT-LIB on Formal Methods Tools</description>
|
||||
<generator>Hugo</generator>
|
||||
<language>en-us</language>
|
||||
<lastBuildDate>Fri, 02 Feb 2024 04:14:54 -0800</lastBuildDate>
|
||||
<atom:link href="http://localhost:1313/languages/smt-lib/index.xml" rel="self" type="application/rss+xml" />
|
||||
<item>
|
||||
<title>Yices 2</title>
|
||||
<link>http://localhost:1313/tools/yices/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>http://localhost:1313/tools/yices/</guid>
|
||||
<description><p>Yices is a high-performance SMT solver and theorem prover developed by SRI International. It is widely used for checking the satisfiability of logical formulas over various theories, including arithmetic, bit-vectors, arrays, and uninterpreted functions. Yices supports the SMT-LIB standard and its own input language, and provides APIs for several programming languages, making it suitable for integration into formal verification, program analysis, and constraint solving tools.</p>
<h3 id="features">Features</h3>
<ul>
<li><strong>SMT Solver:</strong> Supports a wide range of theories and quantifiers.</li>
<li><strong>Multi-language APIs:</strong> C, OCaml, Python, and more.</li>
<li><strong>Cross-platform:</strong> Available on Windows, Linux, and macOS.</li>
<li><strong>Active development:</strong> Open source and maintained by SRI International.</li>
</ul></description>
|
||||
</item>
|
||||
<item>
|
||||
<title>Z3</title>
|
||||
<link>http://localhost:1313/tools/z3/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>http://localhost:1313/tools/z3/</guid>
|
||||
<description><p>Z3 is a high-performance SMT solver and theorem prover developed by Microsoft Research. It is widely used for checking the satisfiability of logical formulas over various theories, including arithmetic, bit-vectors, arrays, and uninterpreted functions. Z3 supports the SMT-LIB standard and provides APIs for several programming languages, making it suitable for integration into formal verification, program analysis, and constraint solving tools.</p>
<h3 id="features">Features</h3>
<ul>
<li><strong>SMT Solver:</strong> Supports a wide range of theories and quantifiers.</li>
<li><strong>Multi-language APIs:</strong> Python, C++, Java, .NET, and more.</li>
<li><strong>Cross-platform:</strong> Available on Windows, Linux, and macOS.</li>
<li><strong>Active development:</strong> Open source and maintained by Microsoft Research.</li>
<li><strong>Web Playground:</strong> Try Z3 online at <a href="https://rise4fun.com/z3">Rise4Fun</a>.</li>
</ul></description>
|
||||
</item>
|
||||
</channel>
|
||||
</rss>
|
||||
@@ -1,69 +0,0 @@
|
||||
<!DOCTYPE html>
|
||||
<html lang="en-us" dir="ltr">
|
||||
<head>
|
||||
<meta charset="utf-8">
|
||||
|
||||
<meta name="viewport" content ="width=device-width, initial-scale=1.0, maximum-scale=1.0, user-scalable=no">
|
||||
<meta http-equiv="X-UA-Compatible" content="IE=edge">
|
||||
<title>Tttt | Formal Methods Tools</title>
|
||||
|
||||
|
||||
<meta name="keywords" content="Formal Methods Tools">
|
||||
<meta property="og:locale" content='en_US'>
|
||||
<meta property="og:type" content="article">
|
||||
<meta property="og:title" content="Tttt">
|
||||
<meta property="og:description" content="">
|
||||
<meta property="og:url" content="https://example.org/languages/tttt/">
|
||||
<meta property="og:image" content="images/%!s(<nil>)">
|
||||
<link rel="canonical" href="https://example.org/languages/tttt/">
|
||||
|
||||
<link rel="apple-touch-icon" sizes="180x180" href='https://example.org/apple-touch-icon.png'>
|
||||
<link rel="icon" type="image/png" sizes="32x32" href='https://example.org/favicon-32x32.png'>
|
||||
<link rel="icon" type="image/png" sizes='16x16' href='https://example.org/favicon-16x16.png'>
|
||||
<link rel="manifest" href='https://example.org/site.webmanifest'>
|
||||
|
||||
<link rel="stylesheet" href="https://example.org/css/styles.fc7cf65388be07f2e53293132dd0220e34d9861f57de4b336d64dd03a3502a9befbea05606442d0a501005442835a864361b9a51b4b51acbf28df37530f61f31.css" integrity="sha512-/Hz2U4i+B/LlMpMTLdAiDjTZhh9X3kszbWTdA6NQKpvvvqBWBkQtClAQBUQoNahkNhuaUbS1GsvyjfN1MPYfMQ==">
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</head>
|
||||
<body>
|
||||
<header>
|
||||
<h1><a href="/">Formal Methods Tools</a></h1>
|
||||
|
||||
<nav>
|
||||
<ul>
|
||||
<li>
|
||||
<a href="/">Home</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/tools/">Tools</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/taxonomies/">Taxonomies</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/about/">About</a>
|
||||
</li>
|
||||
</ul>
|
||||
</nav>
|
||||
|
||||
|
||||
</header>
|
||||
<main>
|
||||
|
||||
<h1>Tttt</h1>
|
||||
|
||||
|
||||
<h2><a href="/tools/z3/">Z3 Theorem Prover</a></h2>
|
||||
|
||||
|
||||
</main>
|
||||
<footer>
|
||||
<p>Copyright 2025. All rights reserved.</p>
|
||||
|
||||
</footer>
|
||||
</body>
|
||||
</html>
|
||||
@@ -1,19 +0,0 @@
|
||||
<?xml version="1.0" encoding="utf-8" standalone="yes"?>
|
||||
<rss version="2.0" xmlns:atom="http://www.w3.org/2005/Atom">
|
||||
<channel>
|
||||
<title>Tttt on Formal Methods Tools</title>
|
||||
<link>https://example.org/languages/tttt/</link>
|
||||
<description>Recent content in Tttt on Formal Methods Tools</description>
|
||||
<generator>Hugo</generator>
|
||||
<language>en-us</language>
|
||||
<lastBuildDate>Fri, 02 Feb 2024 04:14:54 -0800</lastBuildDate>
|
||||
<atom:link href="https://example.org/languages/tttt/index.xml" rel="self" type="application/rss+xml" />
|
||||
<item>
|
||||
<title>Z3 Theorem Prover</title>
|
||||
<link>https://example.org/tools/z3/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>https://example.org/tools/z3/</guid>
|
||||
<description><p>desc</p></description>
|
||||
</item>
|
||||
</channel>
|
||||
</rss>
|
||||
69
languages/yices-language/index.html
Normal file
69
languages/yices-language/index.html
Normal file
@@ -0,0 +1,69 @@
|
||||
<!DOCTYPE html>
|
||||
<html lang="en-us" dir="ltr">
|
||||
<head><script src="/livereload.js?mindelay=10&v=2&port=1313&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">
|
||||
<meta http-equiv="X-UA-Compatible" content="IE=edge">
|
||||
<title>Yices Language | Formal Methods Tools</title>
|
||||
|
||||
|
||||
<meta name="keywords" content="Formal Methods Tools">
|
||||
<meta property="og:locale" content='en_US'>
|
||||
<meta property="og:type" content="article">
|
||||
<meta property="og:title" content="Yices Language">
|
||||
<meta property="og:description" content="">
|
||||
<meta property="og:url" content="http://localhost:1313/languages/yices-language/">
|
||||
<meta property="og:image" content="images/%!s(<nil>)">
|
||||
<link rel="canonical" href="http://localhost:1313/languages/yices-language/">
|
||||
|
||||
<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="http://localhost:1313/css/styles.e3fcfb3452c69d09414fe512e9dca31d879e4a6c47d23010fbb07eb6693d447f645d3bd2d021c0d28d0f7b4fe6f32a10e599488cdb16c6750a9a126788131917.css" integrity="sha512-4/z7NFLGnQlBT+US6dyjHYeeSmxH0jAQ+7B+tmk9RH9kXTvS0CHA0o0Pe0/m8yoQ5ZlIjNsWxnUKmhJniBMZFw==">
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</head>
|
||||
<body>
|
||||
<header>
|
||||
<h1><a href="/">Formal Methods Tools</a></h1>
|
||||
|
||||
<nav>
|
||||
<ul>
|
||||
<li>
|
||||
<a href="/">Home</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/tools/">Tools</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/taxonomies/">Taxonomies</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/about/">About</a>
|
||||
</li>
|
||||
</ul>
|
||||
</nav>
|
||||
|
||||
|
||||
</header>
|
||||
<main>
|
||||
|
||||
<h1>Yices Language</h1>
|
||||
|
||||
|
||||
<h2><a href="/tools/yices/">Yices 2</a></h2>
|
||||
|
||||
|
||||
</main>
|
||||
<footer>
|
||||
<p>Copyright 2025. All rights reserved.</p>
|
||||
|
||||
</footer>
|
||||
</body>
|
||||
</html>
|
||||
19
languages/yices-language/index.xml
Normal file
19
languages/yices-language/index.xml
Normal file
@@ -0,0 +1,19 @@
|
||||
<?xml version="1.0" encoding="utf-8" standalone="yes"?>
|
||||
<rss version="2.0" xmlns:atom="http://www.w3.org/2005/Atom">
|
||||
<channel>
|
||||
<title>Yices Language on Formal Methods Tools</title>
|
||||
<link>http://localhost:1313/languages/yices-language/</link>
|
||||
<description>Recent content in Yices Language on Formal Methods Tools</description>
|
||||
<generator>Hugo</generator>
|
||||
<language>en-us</language>
|
||||
<lastBuildDate>Fri, 02 Feb 2024 04:14:54 -0800</lastBuildDate>
|
||||
<atom:link href="http://localhost:1313/languages/yices-language/index.xml" rel="self" type="application/rss+xml" />
|
||||
<item>
|
||||
<title>Yices 2</title>
|
||||
<link>http://localhost:1313/tools/yices/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>http://localhost:1313/tools/yices/</guid>
|
||||
<description><p>Yices is a high-performance SMT solver and theorem prover developed by SRI International. It is widely used for checking the satisfiability of logical formulas over various theories, including arithmetic, bit-vectors, arrays, and uninterpreted functions. Yices supports the SMT-LIB standard and its own input language, and provides APIs for several programming languages, making it suitable for integration into formal verification, program analysis, and constraint solving tools.</p>
<h3 id="features">Features</h3>
<ul>
<li><strong>SMT Solver:</strong> Supports a wide range of theories and quantifiers.</li>
<li><strong>Multi-language APIs:</strong> C, OCaml, Python, and more.</li>
<li><strong>Cross-platform:</strong> Available on Windows, Linux, and macOS.</li>
<li><strong>Active development:</strong> Open source and maintained by SRI International.</li>
</ul></description>
|
||||
</item>
|
||||
</channel>
|
||||
</rss>
|
||||
71
purposes/analysis-tools/index.html
Normal file
71
purposes/analysis-tools/index.html
Normal file
@@ -0,0 +1,71 @@
|
||||
<!DOCTYPE html>
|
||||
<html lang="en-us" dir="ltr">
|
||||
<head><script src="/livereload.js?mindelay=10&v=2&port=1313&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">
|
||||
<meta http-equiv="X-UA-Compatible" content="IE=edge">
|
||||
<title>Analysis Tools | Formal Methods Tools</title>
|
||||
|
||||
|
||||
<meta name="keywords" content="Formal Methods Tools">
|
||||
<meta property="og:locale" content='en_US'>
|
||||
<meta property="og:type" content="article">
|
||||
<meta property="og:title" content="Analysis Tools">
|
||||
<meta property="og:description" content="">
|
||||
<meta property="og:url" content="http://localhost:1313/purposes/analysis-tools/">
|
||||
<meta property="og:image" content="images/%!s(<nil>)">
|
||||
<link rel="canonical" href="http://localhost:1313/purposes/analysis-tools/">
|
||||
|
||||
<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="http://localhost:1313/css/styles.e3fcfb3452c69d09414fe512e9dca31d879e4a6c47d23010fbb07eb6693d447f645d3bd2d021c0d28d0f7b4fe6f32a10e599488cdb16c6750a9a126788131917.css" integrity="sha512-4/z7NFLGnQlBT+US6dyjHYeeSmxH0jAQ+7B+tmk9RH9kXTvS0CHA0o0Pe0/m8yoQ5ZlIjNsWxnUKmhJniBMZFw==">
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
</head>
|
||||
<body>
|
||||
<header>
|
||||
<h1><a href="/">Formal Methods Tools</a></h1>
|
||||
|
||||
<nav>
|
||||
<ul>
|
||||
<li>
|
||||
<a href="/">Home</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/tools/">Tools</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/taxonomies/">Taxonomies</a>
|
||||
</li>
|
||||
<li>
|
||||
<a href="/about/">About</a>
|
||||
</li>
|
||||
</ul>
|
||||
</nav>
|
||||
|
||||
|
||||
</header>
|
||||
<main>
|
||||
|
||||
<h1>Analysis Tools</h1>
|
||||
|
||||
|
||||
<h2><a href="/tools/yices/">Yices 2</a></h2>
|
||||
|
||||
<h2><a href="/tools/z3/">Z3</a></h2>
|
||||
|
||||
|
||||
</main>
|
||||
<footer>
|
||||
<p>Copyright 2025. All rights reserved.</p>
|
||||
|
||||
</footer>
|
||||
</body>
|
||||
</html>
|
||||
26
purposes/analysis-tools/index.xml
Normal file
26
purposes/analysis-tools/index.xml
Normal file
@@ -0,0 +1,26 @@
|
||||
<?xml version="1.0" encoding="utf-8" standalone="yes"?>
|
||||
<rss version="2.0" xmlns:atom="http://www.w3.org/2005/Atom">
|
||||
<channel>
|
||||
<title>Analysis Tools on Formal Methods Tools</title>
|
||||
<link>http://localhost:1313/purposes/analysis-tools/</link>
|
||||
<description>Recent content in Analysis Tools on Formal Methods Tools</description>
|
||||
<generator>Hugo</generator>
|
||||
<language>en-us</language>
|
||||
<lastBuildDate>Fri, 02 Feb 2024 04:14:54 -0800</lastBuildDate>
|
||||
<atom:link href="http://localhost:1313/purposes/analysis-tools/index.xml" rel="self" type="application/rss+xml" />
|
||||
<item>
|
||||
<title>Yices 2</title>
|
||||
<link>http://localhost:1313/tools/yices/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>http://localhost:1313/tools/yices/</guid>
|
||||
<description><p>Yices is a high-performance SMT solver and theorem prover developed by SRI International. It is widely used for checking the satisfiability of logical formulas over various theories, including arithmetic, bit-vectors, arrays, and uninterpreted functions. Yices supports the SMT-LIB standard and its own input language, and provides APIs for several programming languages, making it suitable for integration into formal verification, program analysis, and constraint solving tools.</p>
<h3 id="features">Features</h3>
<ul>
<li><strong>SMT Solver:</strong> Supports a wide range of theories and quantifiers.</li>
<li><strong>Multi-language APIs:</strong> C, OCaml, Python, and more.</li>
<li><strong>Cross-platform:</strong> Available on Windows, Linux, and macOS.</li>
<li><strong>Active development:</strong> Open source and maintained by SRI International.</li>
</ul></description>
|
||||
</item>
|
||||
<item>
|
||||
<title>Z3</title>
|
||||
<link>http://localhost:1313/tools/z3/</link>
|
||||
<pubDate>Fri, 02 Feb 2024 04:14:54 -0800</pubDate>
|
||||
<guid>http://localhost:1313/tools/z3/</guid>
|
||||
<description><p>Z3 is a high-performance SMT solver and theorem prover developed by Microsoft Research. It is widely used for checking the satisfiability of logical formulas over various theories, including arithmetic, bit-vectors, arrays, and uninterpreted functions. Z3 supports the SMT-LIB standard and provides APIs for several programming languages, making it suitable for integration into formal verification, program analysis, and constraint solving tools.</p>
<h3 id="features">Features</h3>
<ul>
<li><strong>SMT Solver:</strong> Supports a wide range of theories and quantifiers.</li>
<li><strong>Multi-language APIs:</strong> Python, C++, Java, .NET, and more.</li>
<li><strong>Cross-platform:</strong> Available on Windows, Linux, and macOS.</li>
<li><strong>Active development:</strong> Open source and maintained by Microsoft Research.</li>
<li><strong>Web Playground:</strong> Try Z3 online at <a href="https://rise4fun.com/z3">Rise4Fun</a>.</li>
</ul></description>
|
||||
</item>
|
||||
</channel>
|
||||
</rss>
|
||||
Some files were not shown because too many files have changed in this diff Show More
Reference in New Issue
Block a user