diff --git a/css/styles.css.map b/css/styles.css.map index aa6d4c9..e394214 100644 --- a/css/styles.css.map +++ b/css/styles.css.map @@ -8,16 +8,18 @@ "themes/fmtools/assets/sass/_colors.sass", "themes/fmtools/assets/sass/_layout.sass", "themes/fmtools/assets/sass/_taxonomy.sass", - "themes/fmtools/assets/sass/_links.sass" + "themes/fmtools/assets/sass/_links.sass", + "themes/fmtools/assets/sass/_publications.sass" ], "sourcesContent": [ - "@import \"fonts\";\n@import \"colors\";\n@import \"layout\";\n@import \"taxonomy\";\n@import \"links\";\n", + "@import \"fonts\";\n@import \"colors\";\n@import \"layout\";\n@import \"taxonomy\";\n@import \"links\";\n@import \"publications\";\n", "$font-path: '/fonts/static/';\n\n@font-face {\n font-family: 'Source Sans 3';\n font-style: normal;\n font-display: swap;\n font-weight: 100;\n src: local('Source Sans 3 ExtraLight'), local('SourceSans3-ExtraLight'), url('#{$font-path}SourceSans3-ExtraLight.woff2') format('woff2'), url('#{$font-path}SourceSans3-ExtraLight.ttf') format('truetype'); }\n@font-face {\n font-family: 'Source Sans 3';\n font-style: normal;\n font-display: swap;\n font-weight: 200;\n src: local('Source Sans 3 ExtraLight'), local('SourceSans3-ExtraLight'), url('#{$font-path}SourceSans3-ExtraLight.woff2') format('woff2'), url('#{$font-path}SourceSans3-ExtraLight.ttf') format('truetype'); }\n\n@font-face {\n font-family: 'Source Sans 3';\n font-style: normal;\n font-display: swap;\n font-weight: 300;\n src: local('Source Sans 3 Light'), local('SourceSans3-Light'), url('#{$font-path}SourceSans3-Light.woff2') format('woff2'), url('#{$font-path}SourceSans3-Light.ttf') format('truetype'); }\n\n@font-face {\n font-family: 'Source Sans 3';\n font-style: normal;\n font-display: swap;\n font-weight: 400;\n src: local('Source Sans 3 Regular'), local('SourceSans3-Regular'), url('#{$font-path}SourceSans3-Regular.woff2') format('woff2'), url('#{$font-path}SourceSans3-Regular.ttf') format('truetype'); }\n\n@font-face {\n font-family: 'Source Sans 3';\n font-style: italic;\n font-display: swap;\n font-weight: 400;\n src: local('Source Sans 3 Italic'), local('SourceSans3-Italic'), url('#{$font-path}SourceSans3-Italic.woff2') format('woff2'), url('#{$font-path}SourceSans3-Italic.ttf') format('truetype'); }\n\n@font-face {\n font-family: 'Source Sans 3';\n font-style: normal;\n font-display: swap;\n font-weight: 500;\n src: local('Source Sans 3 Medium'), local('SourceSans3-Medium'), url('#{$font-path}SourceSans3-Medium.woff2') format('woff2'), url('#{$font-path}SourceSans3-Medium.ttf') format('truetype'); }\n\n@font-face {\n font-family: 'Source Sans 3';\n font-style: normal;\n font-display: swap;\n font-weight: 600;\n src: local('Source Sans 3 SemiBold'), local('SourceSans3-SemiBold'), url('#{$font-path}SourceSans3-SemiBold.woff2') format('woff2'), url('#{$font-path}SourceSans3-SemiBold.ttf') format('truetype'); }\n\n@font-face {\n font-family: 'Source Sans 3';\n font-style: normal;\n font-display: swap;\n font-weight: 700;\n src: local('Source Sans 3 Bold'), local('SourceSans3-Bold'), url('#{$font-path}SourceSans3-Bold.woff2') format('woff2'), url('#{$font-path}SourceSans3-Bold.ttf') format('truetype'); }\n\n@font-face {\n font-family: 'Source Sans 3';\n font-style: italic;\n font-display: swap;\n font-weight: 700;\n src: local('Source Sans 3 Bold Italic'), local('SourceSans3-BoldItalic'), url('#{$font-path}SourceSans3-BoldItalic.woff2') format('woff2'), url('#{$font-path}SourceSans3-BoldItalic.ttf') format('truetype'); }\n\n@font-face {\n font-family: 'Source Sans 3';\n font-style: normal;\n font-display: swap;\n font-weight: 800;\n src: local('Source Sans 3 ExtraBold'), local('SourceSans3-ExtraBold'), url('#{$font-path}SourceSans3-ExtraBold.woff2') format('woff2'), url('#{$font-path}SourceSans3-ExtraBold.ttf') format('truetype'); }\n\n@font-face {\n font-family: 'Source Sans 3';\n font-style: normal;\n font-display: swap;\n font-weight: 900;\n src: local('Source Sans 3 Black'), local('SourceSans3-Black'), url('#{$font-path}SourceSans3-Black.woff2') format('woff2'), url('#{$font-path}SourceSans3-Black.ttf') format('truetype'); }\n\n\n* {\n font-family: 'Source Sans 3', sans-serif; }\n", "//\n// _colors.sass\n// Attractive dark mode color scheme for fmtools\n//\n\n// Primary palette\n$primary: #3380ff;\n$primary-dark: #1a3e70;\n$primary-light: #8fc6ff;\n\n// Accent colors\n$accent: #1de9b6;\n$accent-dark: #00897b;\n$accent-light: #6fffd2;\n\n\n// Success, warning, error\n$success: #00e676;\n$warning: #ffd600;\n$error: #ff1744;\n\n// Neutral palette (dark mode)\n$darkest: #0a0c11;\n$background: #10131a;\n$surface: #1a1e29;\n$border: #3a4054;\n$text: #ffffff;\n$text-subtle: #bfc9e6;\n", - "/* _layout.sass */\n\n/* Variables */\n$spacing-unit: 1.5rem;\n$section-spacing: 2rem;\n$border-radius: 8px;\n\nhtml {\n background: darken($background, 3%); }\n\n/* Base Layout */\nbody {\n background: $background;\n color: $text;\n font-family: 'Segoe UI', 'Helvetica Neue', Arial, sans-serif;\n width: 100%;\n height: 100%;\n max-width: 1024px;\n margin: $spacing-unit auto;\n padding: $spacing-unit;\n box-sizing: border-box;\n border-radius: $border-radius; }\n\nheader {\n background: $surface;\n margin: $spacing-unit;\n padding: $spacing-unit;\n display: flex;\n flex-wrap: wrap;\n align-items: center;\n justify-content: space-between;\n border-radius: $border-radius;\n margin: 0 auto; }\n\nheader h1, header h1 a {\n margin: 0;\n font-size: 1.6rem;\n font-weight: 600;\n color: $text;\n text-decoration: none;\n padding: 0;\n transition: color 0.4s;\n &:hover, &:focus {\n color: $accent-light; } }\n\nnav {\n display: flex;\n gap: $spacing-unit;\n align-items: center; }\n\nnav ul {\n list-style: none;\n margin: 0;\n padding: 0;\n display: flex;\n gap: 0.5rem;\n flex-wrap: wrap; }\n\nnav ul li {\n margin: 0;\n padding: 0; }\n\nnav ul li a {\n padding: 0.4rem 0.6rem;\n border-radius: $border-radius;\n background: $primary-dark;\n color: $text;\n text-decoration: none;\n font-weight: 500;\n transition: background 0.4s;\n &:hover, &:focus {\n background: $accent-dark; } }\n\n@media (max-width: 600px) {\n header {\n flex-direction: column;\n align-items: flex-start;\n gap: $spacing-unit; }\n\n nav {\n width: 100%;\n justify-content: flex-start;\n margin-top: $spacing-unit; } }\n\nmain {\n margin: $spacing-unit 0;\n padding: $spacing-unit; }\n\nfooter {\n background: $surface;\n margin: $spacing-unit;\n padding: $spacing-unit;\n border-radius: $border-radius;\n margin: 0 auto;\n text-align: center; }\n\nfooter p {\n margin: 0;\n font-size: 0.9rem;\n color: $text-subtle;\n text-align: center; }\n\nsection {\n border-bottom: 3px solid $surface;\n margin: $section-spacing 0;\n padding-bottom: $section-spacing; }\n\n#page-header {\n border-bottom: 3px solid $surface;\n margin: $section-spacing 0;\n padding-bottom: $section-spacing;\n text-align: center;\n h1 {\n margin: 0; }\n .time {\n font-size: 0.8rem;\n color: $text-subtle; } }\n", - "\ntable#taxonomy-table {\n width: 100%;\n border-collapse: collapse;\n // border: 3px solid $darkest\n box-sizing: border-box;\n background: $surface;\n text-align: left;\n\n tr:nth-child(even) {\n background: darken($surface, 2%);\n transition: background 0.4s; }\n tr:nth-child(odd) {\n background: lighten($surface, 3%);\n transition: background 0.4s; }\n tr:hover, tr:focus {\n background: $border; } }\n\n#taxonomy-table thead {\n text-align: left;\n border: none;\n background: $darkest;\n border-radius: $border-radius $border-radius 0 0; }\n\n#taxonomy-table th {\n color: $text;\n padding: 0.6rem 0.6rem;\n text-align: left;\n font-weight: 600;\n border: none; }\n\n#taxonomy-table td {\n padding: 0.3rem 0.6rem;\n text-align: left;\n font-weight: 600;\n border: none; }\n\n#taxonomy-table tr {\n border-bottom: 3px solid $background;\n &:hover, &:focus {\n background: $primary-light; } }\n\n#taxonomy-table a.term-link {\n padding: 0.2rem 0.6rem;\n margin: 0.2rem;\n display: inline-block;\n border-radius: $border-radius;\n text-decoration: none;\n font-weight: 500;\n color: $text;\n transition: color 0.4s;\n &:hover, &:focus {\n color: $darkest; } }\n\n#taxonomy-table a.taxonomy-name {\n padding: 0;\n margin: 0.2rem;\n display: inline-block;\n border-radius: $border-radius;\n text-decoration: none;\n font-weight: 500;\n color: $text;\n transition: color 0.4s;\n &:hover, &:focus {\n color: $accent-light; } }\n\n#taxonomy-page a.term-link {\n padding: 0.3rem 1.2rem;\n margin: 0.2rem;\n display: inline-block;\n border-radius: $border-radius;\n text-decoration: none;\n font-weight: 500;\n color: $text;\n transition: color 0.4s;\n font-size: 1.2rem;\n &:hover, &:focus {\n color: $darkest; } }\n\n", - "/* _text.sass */\n\n#quick-links {\n text-align: left; }\n\n#link-list {\n display: flex;\n gap: $spacing-unit;\n align-items: left;\n margin: $spacing-unit 0; }\n\n#link-list h2 {\n flex: none; }\n\n#link-list ul {\n list-style: none;\n margin: 0;\n padding: 0;\n display: flex;\n gap: 1rem;\n flex-wrap: wrap; }\n\n#link-list ul li {\n margin: 0;\n padding: 0; }\n\n#link-list ul li a {\n padding: 0.3rem 0.6rem;\n border-radius: $border-radius;\n background: $primary-light;\n color: $darkest;\n text-decoration: none;\n font-weight: 500;\n transition: background 0.4s;\n &:hover, &:focus {\n background: $accent-light; } }\n" + "/* _layout.sass */\n\n/* Variables */\n$spacing-unit: 1.5rem;\n$section-spacing: 2rem;\n$border-radius: 8px;\n\nhtml {\n background: darken($background, 3%); }\n\n/* Base Layout */\nbody {\n background: $background;\n color: $text;\n font-family: 'Segoe UI', 'Helvetica Neue', Arial, sans-serif;\n width: 100%;\n height: 100%;\n max-width: 1024px;\n margin: $spacing-unit auto;\n padding: $spacing-unit;\n box-sizing: border-box;\n border-radius: $border-radius; }\n\nheader {\n background: $surface;\n margin: $spacing-unit;\n padding: $spacing-unit;\n display: flex;\n flex-wrap: wrap;\n align-items: center;\n justify-content: space-between;\n border-radius: $border-radius;\n margin: 0 auto; }\n\nheader h1, header h1 a {\n margin: 0;\n font-size: 1.6rem;\n font-weight: 600;\n color: $text;\n text-decoration: none;\n padding: 0;\n transition: color 0.4s ease-in-out;\n &:hover, &:focus {\n color: $accent-light; } }\n\nnav {\n display: flex;\n gap: $spacing-unit;\n align-items: center; }\n\nnav ul {\n list-style: none;\n margin: 0;\n padding: 0;\n display: flex;\n gap: 0.5rem;\n flex-wrap: wrap; }\n\nnav ul li {\n margin: 0;\n padding: 0; }\n\nnav ul li a {\n padding: 0.4rem 0.6rem;\n border-radius: $border-radius;\n background: $primary-dark;\n color: $text;\n text-decoration: none;\n font-weight: 500;\n transition: background 0.4s ease-in-out;\n &:hover, &:focus {\n background: $accent-dark;\n color: $text; } }\n\n@media (max-width: 600px) {\n header {\n flex-direction: column;\n align-items: flex-start;\n gap: $spacing-unit; }\n\n nav {\n width: 100%;\n justify-content: flex-start;\n margin-top: $spacing-unit; } }\n\nmain {\n margin: $spacing-unit 0;\n padding: $spacing-unit; }\n\nfooter {\n background: $surface;\n margin: $spacing-unit;\n padding: $spacing-unit;\n border-radius: $border-radius;\n margin: 0 auto;\n text-align: center; }\n\nfooter p {\n margin: 0;\n font-size: 0.9rem;\n color: $text-subtle;\n text-align: center; }\n\nsection {\n border-bottom: 3px solid $surface;\n margin: $section-spacing 0;\n padding-bottom: $section-spacing; }\n\n#page-header {\n border-bottom: 3px solid $surface;\n margin: $section-spacing 0;\n padding-bottom: $section-spacing;\n text-align: center;\n h1 {\n margin: 0; }\n .time {\n font-size: 0.8rem;\n color: $text-subtle; } }\n", + "\ntable#taxonomy-table {\n width: 100%;\n border-collapse: collapse;\n // border: 3px solid $darkest\n box-sizing: border-box;\n background: $surface;\n text-align: left;\n\n tr {\n border-bottom: 3px solid $background;\n &:nth-child(even) {\n background: darken($surface, 2%);\n transition: background 0.4s ease-in-out; }\n &:nth-child(odd) {\n background: lighten($surface, 3%);\n transition: background 0.4s ease-in-out; }\n &:hover, &:focus {\n background: $border; } }\n\n thead {\n text-align: left;\n border: none;\n background: $darkest;\n border-radius: $border-radius $border-radius 0 0; }\n\n th {\n color: $text;\n padding: 0.6rem 0.6rem;\n text-align: left;\n font-weight: 600;\n border: none; }\n\n td {\n padding: 0.3rem 0.6rem;\n text-align: left;\n font-weight: 600;\n border: none; }\n\n a.term-link {\n padding: 0.2rem 0.6rem;\n margin: 0.2rem;\n display: inline-block;\n border-radius: $border-radius;\n text-decoration: none;\n font-weight: 500;\n color: $text;\n transition: color 0.4s ease-in-out, background 0.4s ease-in-out;\n &:hover, &:focus {\n color: $darkest !important;\n background: $text-subtle !important; } }\n\n a.taxonomy-name {\n padding: 0;\n margin: 0.2rem;\n display: inline-block;\n border-radius: $border-radius;\n text-decoration: none;\n font-weight: 500;\n color: $text;\n transition: color 0.4s ease-in-out;\n &:hover, &:focus {\n color: $accent-light; } } }\n\n#taxonomy-page a.term-link {\n padding: 0.3rem 1.2rem;\n margin: 0.2rem;\n display: inline-block;\n border-radius: $border-radius;\n text-decoration: none;\n font-weight: 500;\n color: $text;\n transition: color 0.4s ease-in-out;\n font-size: 1.2rem;\n &:hover, &:focus {\n color: $darkest; } }\n\n", + "/* _text.sass */\n\na {\n color: $primary;\n text-decoration: underline;\n transition: color 0.3s ease-in-out;\n &:hover, &:focus {\n color: $accent; } }\n\n#quick-links {\n text-align: left; }\n\n#link-list {\n display: flex;\n gap: $spacing-unit;\n align-items: left;\n margin: $spacing-unit 0; }\n\n#link-list h2 {\n flex: none; }\n\n#link-list ul {\n list-style: none;\n margin: 0;\n padding: 0;\n display: flex;\n gap: 1rem;\n flex-wrap: wrap; }\n\n#link-list ul li {\n margin: 0;\n padding: 0; }\n\n#link-list ul li a {\n padding: 0.3rem 0.6rem;\n border-radius: $border-radius;\n background: $primary-light;\n color: $darkest;\n text-decoration: none;\n font-weight: 500;\n transition: background 0.3s ease-in-out;\n &:hover, &:focus {\n background: $accent-light; } }\n", + "#publications {\n ul {\n list-style: none;\n margin: 0;\n padding: 0;\n display: flex;\n flex-direction: column;\n gap: 1em;\n\n li {\n background: $surface;\n border-radius: 8px;\n padding: 1em 1.5em; } } }\n" ], "names": [], - "mappings": "ACEA,UAAU;EACN,WAAW,EAAE,eAAe;EAC5B,UAAU,EAAE,MAAM;EAClB,YAAY,EAAE,IAAI;EAClB,WAAW,EAAE,GAAG;EAChB,GAAG,EAAE,iCAAiC,EAAE,+BAA+B,EAAE,iDAA0D,CAAC,eAAe,EAAE,+CAAwD,CAAC,kBAAkB;;;AACpO,UAAU;EACN,WAAW,EAAE,eAAe;EAC5B,UAAU,EAAE,MAAM;EAClB,YAAY,EAAE,IAAI;EAClB,WAAW,EAAE,GAAG;EAChB,GAAG,EAAE,iCAAiC,EAAE,+BAA+B,EAAE,iDAA0D,CAAC,eAAe,EAAE,+CAAwD,CAAC,kBAAkB;;;AAEpO,UAAU;EACN,WAAW,EAAE,eAAe;EAC5B,UAAU,EAAE,MAAM;EAClB,YAAY,EAAE,IAAI;EAClB,WAAW,EAAE,GAAG;EAChB,GAAG,EAAE,4BAA4B,EAAE,0BAA0B,EAAE,4CAAqD,CAAC,eAAe,EAAE,0CAAmD,CAAC,kBAAkB;;;AAEhN,UAAU;EACN,WAAW,EAAE,eAAe;EAC5B,UAAU,EAAE,MAAM;EAClB,YAAY,EAAE,IAAI;EAClB,WAAW,EAAE,GAAG;EAChB,GAAG,EAAE,8BAA8B,EAAE,4BAA4B,EAAE,8CAAuD,CAAC,eAAe,EAAE,4CAAqD,CAAC,kBAAkB;;;AAExN,UAAU;EACN,WAAW,EAAE,eAAe;EAC5B,UAAU,EAAE,MAAM;EAClB,YAAY,EAAE,IAAI;EAClB,WAAW,EAAE,GAAG;EAChB,GAAG,EAAE,6BAA6B,EAAE,2BAA2B,EAAE,6CAAsD,CAAC,eAAe,EAAE,2CAAoD,CAAC,kBAAkB;;;AAEpN,UAAU;EACN,WAAW,EAAE,eAAe;EAC5B,UAAU,EAAE,MAAM;EAClB,YAAY,EAAE,IAAI;EAClB,WAAW,EAAE,GAAG;EAChB,GAAG,EAAE,6BAA6B,EAAE,2BAA2B,EAAE,6CAAsD,CAAC,eAAe,EAAE,2CAAoD,CAAC,kBAAkB;;;AAEpN,UAAU;EACN,WAAW,EAAE,eAAe;EAC5B,UAAU,EAAE,MAAM;EAClB,YAAY,EAAE,IAAI;EAClB,WAAW,EAAE,GAAG;EAChB,GAAG,EAAE,+BAA+B,EAAE,6BAA6B,EAAE,+CAAwD,CAAC,eAAe,EAAE,6CAAsD,CAAC,kBAAkB;;;AAE5N,UAAU;EACN,WAAW,EAAE,eAAe;EAC5B,UAAU,EAAE,MAAM;EAClB,YAAY,EAAE,IAAI;EAClB,WAAW,EAAE,GAAG;EAChB,GAAG,EAAE,2BAA2B,EAAE,yBAAyB,EAAE,2CAAoD,CAAC,eAAe,EAAE,yCAAkD,CAAC,kBAAkB;;;AAE5M,UAAU;EACN,WAAW,EAAE,eAAe;EAC5B,UAAU,EAAE,MAAM;EAClB,YAAY,EAAE,IAAI;EAClB,WAAW,EAAE,GAAG;EAChB,GAAG,EAAE,kCAAkC,EAAE,+BAA+B,EAAE,iDAA0D,CAAC,eAAe,EAAE,+CAAwD,CAAC,kBAAkB;;;AAErO,UAAU;EACN,WAAW,EAAE,eAAe;EAC5B,UAAU,EAAE,MAAM;EAClB,YAAY,EAAE,IAAI;EAClB,WAAW,EAAE,GAAG;EAChB,GAAG,EAAE,gCAAgC,EAAE,8BAA8B,EAAE,gDAAyD,CAAC,eAAe,EAAE,8CAAuD,CAAC,kBAAkB;;;AAEhO,UAAU;EACN,WAAW,EAAE,eAAe;EAC5B,UAAU,EAAE,MAAM;EAClB,YAAY,EAAE,IAAI;EAClB,WAAW,EAAE,GAAG;EAChB,GAAG,EAAE,4BAA4B,EAAE,0BAA0B,EAAE,4CAAqD,CAAC,eAAe,EAAE,0CAAmD,CAAC,kBAAkB;;;AAGhN,AAAA,CAAC,CAAC;EACE,WAAW,EAAE,2BAA2B;CAAG;;AEhF/C,kBAAkB;AAElB,eAAe;AAKf,AAAA,IAAI,CAAC;EACD,UAAU,EDeD,OAAO;CCfsB;;AAE1C,iBAAiB;AACjB,AAAA,IAAI,CAAC;EACD,UAAU,EDWD,OAAO;ECVhB,KAAK,EDaF,OAAO;ECZV,WAAW,EAAE,+CAA+C;EAC5D,KAAK,EAAE,IAAI;EACX,MAAM,EAAE,IAAI;EACZ,SAAS,EAAE,MAAM;EACjB,MAAM,EAfK,MAAM,CAeK,IAAI;EAC1B,OAAO,EAhBI,MAAM;EAiBjB,UAAU,EAAE,UAAU;EACtB,aAAa,EAhBD,GAAG;CAgBiB;;AAEpC,AAAA,MAAM,CAAC;EACH,UAAU,EDAJ,OAAO;ECCb,MAAM,EAtBK,MAAM;EAuBjB,OAAO,EAvBI,MAAM;EAwBjB,OAAO,EAAE,IAAI;EACb,SAAS,EAAE,IAAI;EACf,WAAW,EAAE,MAAM;EACnB,eAAe,EAAE,aAAa;EAC9B,aAAa,EA1BD,GAAG;EA2Bf,MAAM,EAAE,MAAM;CAAG;;AAErB,AAAA,MAAM,CAAC,EAAE,EAAE,MAAM,CAAC,EAAE,CAAC,CAAC,CAAC;EACnB,MAAM,EAAE,CAAC;EACT,SAAS,EAAE,MAAM;EACjB,WAAW,EAAE,GAAG;EAChB,KAAK,EDZF,OAAO;ECaV,eAAe,EAAE,IAAI;EACrB,OAAO,EAAE,CAAC;EACV,UAAU,EAAE,UAAU;CAEO;;AATjC,AAQI,MARE,CAAC,EAAE,CAQH,KAAK,EARX,MAAM,CAAC,EAAE,CAQM,KAAK,EART,MAAM,CAAC,EAAE,CAAC,CAAC,CAQhB,KAAK,EARA,MAAM,CAAC,EAAE,CAAC,CAAC,CAQP,KAAK,CAAC;EACb,KAAK,ED9BE,OAAO;CC8BS;;AAE/B,AAAA,GAAG,CAAC;EACA,OAAO,EAAE,IAAI;EACb,GAAG,EA5CQ,MAAM;EA6CjB,WAAW,EAAE,MAAM;CAAG;;AAE1B,AAAA,GAAG,CAAC,EAAE,CAAC;EACH,UAAU,EAAE,IAAI;EAChB,MAAM,EAAE,CAAC;EACT,OAAO,EAAE,CAAC;EACV,OAAO,EAAE,IAAI;EACb,GAAG,EAAE,MAAM;EACX,SAAS,EAAE,IAAI;CAAG;;AAEtB,AAAA,GAAG,CAAC,EAAE,CAAC,EAAE,CAAC;EACN,MAAM,EAAE,CAAC;EACT,OAAO,EAAE,CAAC;CAAG;;AAEjB,AAAA,GAAG,CAAC,EAAE,CAAC,EAAE,CAAC,CAAC,CAAC;EACR,OAAO,EAAE,aAAa;EACtB,aAAa,EA3DD,GAAG;EA4Df,UAAU,ED1DC,OAAO;EC2DlB,KAAK,EDxCF,OAAO;ECyCV,eAAe,EAAE,IAAI;EACrB,WAAW,EAAE,GAAG;EAChB,UAAU,EAAE,eAAe;CAEM;;AATrC,AAQI,GARD,CAAC,EAAE,CAAC,EAAE,CAAC,CAAC,CAQL,KAAK,EARX,GAAG,CAAC,EAAE,CAAC,EAAE,CAAC,CAAC,CAQI,KAAK,CAAC;EACb,UAAU,ED3DJ,OAAO;CC2Dc;;AAEnC,MAAM,mBACF;EAAA,AAAA,MAAM,CAAC;IACH,cAAc,EAAE,MAAM;IACtB,WAAW,EAAE,UAAU;IACvB,GAAG,EA1EI,MAAM;GA0EQ;EAEzB,AAAA,GAAG,CAAC;IACA,KAAK,EAAE,IAAI;IACX,eAAe,EAAE,UAAU;IAC3B,UAAU,EA/EH,MAAM;GA+Ee;CALP;;AAO7B,AAAA,IAAI,CAAC;EACD,MAAM,EAlFK,MAAM,CAkFK,CAAC;EACvB,OAAO,EAnFI,MAAM;CAmFQ;;AAE7B,AAAA,MAAM,CAAC;EACH,UAAU,EDjEJ,OAAO;ECkEb,MAAM,EAvFK,MAAM;EAwFjB,OAAO,EAxFI,MAAM;EAyFjB,aAAa,EAvFD,GAAG;EAwFf,MAAM,EAAE,MAAM;EACd,UAAU,EAAE,MAAM;CAAG;;AAEzB,AAAA,MAAM,CAAC,CAAC,CAAC;EACL,MAAM,EAAE,CAAC;EACT,SAAS,EAAE,MAAM;EACjB,KAAK,EDxEK,OAAO;ECyEjB,UAAU,EAAE,MAAM;CAAG;;AAEzB,AAAA,OAAO,CAAC;EACJ,aAAa,EAAE,GAAG,CAAC,KAAK,CD/ElB,OAAO;ECgFb,MAAM,EApGQ,IAAI,CAoGO,CAAC;EAC1B,cAAc,EArGA,IAAI;CAqGiB;;AAEvC,AAAA,YAAY,CAAC;EACT,aAAa,EAAE,GAAG,CAAC,KAAK,CDpFlB,OAAO;ECqFb,MAAM,EAzGQ,IAAI,CAyGO,CAAC;EAC1B,cAAc,EA1GA,IAAI;EA2GlB,UAAU,EAAE,MAAM;CAKU;;AAThC,AAKI,YALQ,CAKR,EAAE,CAAC;EACC,MAAM,EAAE,CAAC;CAAG;;AANpB,AAOI,YAPQ,CAOR,KAAK,CAAC;EACF,SAAS,EAAE,MAAM;EACjB,KAAK,EDzFC,OAAO;CCyFS;;ACnH9B,AAAA,KAAK,AAAA,eAAe,CAAC;EACjB,KAAK,EAAE,IAAI;EACX,eAAe,EAAE,QAAQ;EAEzB,UAAU,EAAE,UAAU;EACtB,UAAU,EFkBJ,OAAO;EEjBb,UAAU,EAAE,IAAI;CASY;;AAfhC,AAQI,KARC,AAAA,eAAe,CAQhB,EAAE,CAAC,SAAU,CAAA,IAAI,EAAE;EACf,UAAU,EFcR,OAAO;EEbT,UAAU,EAAE,eAAe;CAAG;;AAVtC,AAWI,KAXC,AAAA,eAAe,CAWhB,EAAE,CAAC,SAAU,CAAA,GAAG,EAAE;EACd,UAAU,EFWR,OAAO;EEVT,UAAU,EAAE,eAAe;CAAG;;AAbtC,AAcI,KAdC,AAAA,eAAe,CAchB,EAAE,CAAC,KAAK,EAdZ,KAAK,AAAA,eAAe,CAcN,EAAE,CAAC,KAAK,CAAC;EACf,UAAU,EFST,OAAO;CETc;;AAE9B,AAAA,eAAe,CAAC,KAAK,CAAC;EAClB,UAAU,EAAE,IAAI;EAChB,MAAM,EAAE,IAAI;EACZ,UAAU,EFCJ,OAAO;EEAb,aAAa,EDjBD,GAAG,CAAH,GAAG,CCiB8B,CAAC,CAAC,CAAC;CAAG;;AAEvD,AAAA,eAAe,CAAC,EAAE,CAAC;EACf,KAAK,EFCF,OAAO;EEAV,OAAO,EAAE,aAAa;EACtB,UAAU,EAAE,IAAI;EAChB,WAAW,EAAE,GAAG;EAChB,MAAM,EAAE,IAAI;CAAG;;AAEnB,AAAA,eAAe,CAAC,EAAE,CAAC;EACf,OAAO,EAAE,aAAa;EACtB,UAAU,EAAE,IAAI;EAChB,WAAW,EAAE,GAAG;EAChB,MAAM,EAAE,IAAI;CAAG;;AAEnB,AAAA,eAAe,CAAC,EAAE,CAAC;EACf,aAAa,EAAE,GAAG,CAAC,KAAK,CFff,OAAO;CEiBmB;;AAHvC,AAEI,eAFW,CAAC,EAAE,CAEZ,KAAK,EAFX,eAAe,CAAC,EAAE,CAEH,KAAK,CAAC;EACb,UAAU,EFhCF,OAAO;CEgCc;;AAErC,AAAA,eAAe,CAAC,CAAC,AAAA,UAAU,CAAC;EACxB,OAAO,EAAE,aAAa;EACtB,MAAM,EAAE,MAAM;EACd,OAAO,EAAE,YAAY;EACrB,aAAa,EDzCD,GAAG;EC0Cf,eAAe,EAAE,IAAI;EACrB,WAAW,EAAE,GAAG;EAChB,KAAK,EFvBF,OAAO;EEwBV,UAAU,EAAE,UAAU;CAEE;;AAV5B,AASI,eATW,CAAC,CAAC,AAAA,UAAU,CASrB,KAAK,EATX,eAAe,CAAC,CAAC,AAAA,UAAU,CASZ,KAAK,CAAC;EACb,KAAK,EF9BH,OAAO;CE8BS;;AAE1B,AAAA,eAAe,CAAC,CAAC,AAAA,cAAc,CAAC;EAC5B,OAAO,EAAE,CAAC;EACV,MAAM,EAAE,MAAM;EACd,OAAO,EAAE,YAAY;EACrB,aAAa,EDrDD,GAAG;ECsDf,eAAe,EAAE,IAAI;EACrB,WAAW,EAAE,GAAG;EAChB,KAAK,EFnCF,OAAO;EEoCV,UAAU,EAAE,UAAU;CAEO;;AAVjC,AASI,eATW,CAAC,CAAC,AAAA,cAAc,CASzB,KAAK,EATX,eAAe,CAAC,CAAC,AAAA,cAAc,CAShB,KAAK,CAAC;EACb,KAAK,EFnDE,OAAO;CEmDS;;AAE/B,AAAA,cAAc,CAAC,CAAC,AAAA,UAAU,CAAC;EACvB,OAAO,EAAE,aAAa;EACtB,MAAM,EAAE,MAAM;EACd,OAAO,EAAE,YAAY;EACrB,aAAa,EDjED,GAAG;ECkEf,eAAe,EAAE,IAAI;EACrB,WAAW,EAAE,GAAG;EAChB,KAAK,EF/CF,OAAO;EEgDV,UAAU,EAAE,UAAU;EACtB,SAAS,EAAE,MAAM;CAEO;;AAX5B,AAUI,cAVU,CAAC,CAAC,AAAA,UAAU,CAUpB,KAAK,EAVX,cAAc,CAAC,CAAC,AAAA,UAAU,CAUX,KAAK,CAAC;EACb,KAAK,EFvDH,OAAO;CEuDS;;AC7E1B,gBAAgB;AAEhB,AAAA,YAAY,CAAC;EACT,UAAU,EAAE,IAAI;CAAG;;AAEvB,AAAA,UAAU,CAAC;EACP,OAAO,EAAE,IAAI;EACb,GAAG,EFJQ,MAAM;EEKjB,WAAW,EAAE,IAAI;EACjB,MAAM,EFNK,MAAM,CEMK,CAAC;CAAG;;AAE9B,AAAA,UAAU,CAAC,EAAE,CAAC;EACV,IAAI,EAAE,IAAI;CAAG;;AAEjB,AAAA,UAAU,CAAC,EAAE,CAAC;EACV,UAAU,EAAE,IAAI;EAChB,MAAM,EAAE,CAAC;EACT,OAAO,EAAE,CAAC;EACV,OAAO,EAAE,IAAI;EACb,GAAG,EAAE,IAAI;EACT,SAAS,EAAE,IAAI;CAAG;;AAEtB,AAAA,UAAU,CAAC,EAAE,CAAC,EAAE,CAAC;EACb,MAAM,EAAE,CAAC;EACT,OAAO,EAAE,CAAC;CAAG;;AAEjB,AAAA,UAAU,CAAC,EAAE,CAAC,EAAE,CAAC,CAAC,CAAC;EACf,OAAO,EAAE,aAAa;EACtB,aAAa,EFvBD,GAAG;EEwBf,UAAU,EHrBE,OAAO;EGsBnB,KAAK,EHRC,OAAO;EGSb,eAAe,EAAE,IAAI;EACrB,WAAW,EAAE,GAAG;EAChB,UAAU,EAAE,eAAe;CAEO;;AATtC,AAQI,UARM,CAAC,EAAE,CAAC,EAAE,CAAC,CAAC,CAQZ,KAAK,EARX,UAAU,CAAC,EAAE,CAAC,EAAE,CAAC,CAAC,CAQH,KAAK,CAAC;EACb,UAAU,EHtBH,OAAO;CGsBc" + "mappings": "ACEA,UAAU;EACN,WAAW,EAAE,eAAe;EAC5B,UAAU,EAAE,MAAM;EAClB,YAAY,EAAE,IAAI;EAClB,WAAW,EAAE,GAAG;EAChB,GAAG,EAAE,iCAAiC,EAAE,+BAA+B,EAAE,iDAA0D,CAAC,eAAe,EAAE,+CAAwD,CAAC,kBAAkB;;;AACpO,UAAU;EACN,WAAW,EAAE,eAAe;EAC5B,UAAU,EAAE,MAAM;EAClB,YAAY,EAAE,IAAI;EAClB,WAAW,EAAE,GAAG;EAChB,GAAG,EAAE,iCAAiC,EAAE,+BAA+B,EAAE,iDAA0D,CAAC,eAAe,EAAE,+CAAwD,CAAC,kBAAkB;;;AAEpO,UAAU;EACN,WAAW,EAAE,eAAe;EAC5B,UAAU,EAAE,MAAM;EAClB,YAAY,EAAE,IAAI;EAClB,WAAW,EAAE,GAAG;EAChB,GAAG,EAAE,4BAA4B,EAAE,0BAA0B,EAAE,4CAAqD,CAAC,eAAe,EAAE,0CAAmD,CAAC,kBAAkB;;;AAEhN,UAAU;EACN,WAAW,EAAE,eAAe;EAC5B,UAAU,EAAE,MAAM;EAClB,YAAY,EAAE,IAAI;EAClB,WAAW,EAAE,GAAG;EAChB,GAAG,EAAE,8BAA8B,EAAE,4BAA4B,EAAE,8CAAuD,CAAC,eAAe,EAAE,4CAAqD,CAAC,kBAAkB;;;AAExN,UAAU;EACN,WAAW,EAAE,eAAe;EAC5B,UAAU,EAAE,MAAM;EAClB,YAAY,EAAE,IAAI;EAClB,WAAW,EAAE,GAAG;EAChB,GAAG,EAAE,6BAA6B,EAAE,2BAA2B,EAAE,6CAAsD,CAAC,eAAe,EAAE,2CAAoD,CAAC,kBAAkB;;;AAEpN,UAAU;EACN,WAAW,EAAE,eAAe;EAC5B,UAAU,EAAE,MAAM;EAClB,YAAY,EAAE,IAAI;EAClB,WAAW,EAAE,GAAG;EAChB,GAAG,EAAE,6BAA6B,EAAE,2BAA2B,EAAE,6CAAsD,CAAC,eAAe,EAAE,2CAAoD,CAAC,kBAAkB;;;AAEpN,UAAU;EACN,WAAW,EAAE,eAAe;EAC5B,UAAU,EAAE,MAAM;EAClB,YAAY,EAAE,IAAI;EAClB,WAAW,EAAE,GAAG;EAChB,GAAG,EAAE,+BAA+B,EAAE,6BAA6B,EAAE,+CAAwD,CAAC,eAAe,EAAE,6CAAsD,CAAC,kBAAkB;;;AAE5N,UAAU;EACN,WAAW,EAAE,eAAe;EAC5B,UAAU,EAAE,MAAM;EAClB,YAAY,EAAE,IAAI;EAClB,WAAW,EAAE,GAAG;EAChB,GAAG,EAAE,2BAA2B,EAAE,yBAAyB,EAAE,2CAAoD,CAAC,eAAe,EAAE,yCAAkD,CAAC,kBAAkB;;;AAE5M,UAAU;EACN,WAAW,EAAE,eAAe;EAC5B,UAAU,EAAE,MAAM;EAClB,YAAY,EAAE,IAAI;EAClB,WAAW,EAAE,GAAG;EAChB,GAAG,EAAE,kCAAkC,EAAE,+BAA+B,EAAE,iDAA0D,CAAC,eAAe,EAAE,+CAAwD,CAAC,kBAAkB;;;AAErO,UAAU;EACN,WAAW,EAAE,eAAe;EAC5B,UAAU,EAAE,MAAM;EAClB,YAAY,EAAE,IAAI;EAClB,WAAW,EAAE,GAAG;EAChB,GAAG,EAAE,gCAAgC,EAAE,8BAA8B,EAAE,gDAAyD,CAAC,eAAe,EAAE,8CAAuD,CAAC,kBAAkB;;;AAEhO,UAAU;EACN,WAAW,EAAE,eAAe;EAC5B,UAAU,EAAE,MAAM;EAClB,YAAY,EAAE,IAAI;EAClB,WAAW,EAAE,GAAG;EAChB,GAAG,EAAE,4BAA4B,EAAE,0BAA0B,EAAE,4CAAqD,CAAC,eAAe,EAAE,0CAAmD,CAAC,kBAAkB;;;AAGhN,AAAA,CAAC,CAAC;EACE,WAAW,EAAE,2BAA2B;CAAG;;AEhF/C,kBAAkB;AAElB,eAAe;AAKf,AAAA,IAAI,CAAC;EACD,UAAU,EDeD,OAAO;CCfsB;;AAE1C,iBAAiB;AACjB,AAAA,IAAI,CAAC;EACD,UAAU,EDWD,OAAO;ECVhB,KAAK,EDaF,OAAO;ECZV,WAAW,EAAE,+CAA+C;EAC5D,KAAK,EAAE,IAAI;EACX,MAAM,EAAE,IAAI;EACZ,SAAS,EAAE,MAAM;EACjB,MAAM,EAfK,MAAM,CAeK,IAAI;EAC1B,OAAO,EAhBI,MAAM;EAiBjB,UAAU,EAAE,UAAU;EACtB,aAAa,EAhBD,GAAG;CAgBiB;;AAEpC,AAAA,MAAM,CAAC;EACH,UAAU,EDAJ,OAAO;ECCb,MAAM,EAtBK,MAAM;EAuBjB,OAAO,EAvBI,MAAM;EAwBjB,OAAO,EAAE,IAAI;EACb,SAAS,EAAE,IAAI;EACf,WAAW,EAAE,MAAM;EACnB,eAAe,EAAE,aAAa;EAC9B,aAAa,EA1BD,GAAG;EA2Bf,MAAM,EAAE,MAAM;CAAG;;AAErB,AAAA,MAAM,CAAC,EAAE,EAAE,MAAM,CAAC,EAAE,CAAC,CAAC,CAAC;EACnB,MAAM,EAAE,CAAC;EACT,SAAS,EAAE,MAAM;EACjB,WAAW,EAAE,GAAG;EAChB,KAAK,EDZF,OAAO;ECaV,eAAe,EAAE,IAAI;EACrB,OAAO,EAAE,CAAC;EACV,UAAU,EAAE,sBAAsB;CAEL;;AATjC,AAQI,MARE,CAAC,EAAE,CAQH,KAAK,EARX,MAAM,CAAC,EAAE,CAQM,KAAK,EART,MAAM,CAAC,EAAE,CAAC,CAAC,CAQhB,KAAK,EARA,MAAM,CAAC,EAAE,CAAC,CAAC,CAQP,KAAK,CAAC;EACb,KAAK,ED9BE,OAAO;CC8BS;;AAE/B,AAAA,GAAG,CAAC;EACA,OAAO,EAAE,IAAI;EACb,GAAG,EA5CQ,MAAM;EA6CjB,WAAW,EAAE,MAAM;CAAG;;AAE1B,AAAA,GAAG,CAAC,EAAE,CAAC;EACH,UAAU,EAAE,IAAI;EAChB,MAAM,EAAE,CAAC;EACT,OAAO,EAAE,CAAC;EACV,OAAO,EAAE,IAAI;EACb,GAAG,EAAE,MAAM;EACX,SAAS,EAAE,IAAI;CAAG;;AAEtB,AAAA,GAAG,CAAC,EAAE,CAAC,EAAE,CAAC;EACN,MAAM,EAAE,CAAC;EACT,OAAO,EAAE,CAAC;CAAG;;AAEjB,AAAA,GAAG,CAAC,EAAE,CAAC,EAAE,CAAC,CAAC,CAAC;EACR,OAAO,EAAE,aAAa;EACtB,aAAa,EA3DD,GAAG;EA4Df,UAAU,ED1DC,OAAO;EC2DlB,KAAK,EDxCF,OAAO;ECyCV,eAAe,EAAE,IAAI;EACrB,WAAW,EAAE,GAAG;EAChB,UAAU,EAAE,2BAA2B;CAGlB;;AAVzB,AAQI,GARD,CAAC,EAAE,CAAC,EAAE,CAAC,CAAC,CAQL,KAAK,EARX,GAAG,CAAC,EAAE,CAAC,EAAE,CAAC,CAAC,CAQI,KAAK,CAAC;EACb,UAAU,ED3DJ,OAAO;EC4Db,KAAK,ED9CN,OAAO;CC8CS;;AAEvB,MAAM,mBACF;EAAA,AAAA,MAAM,CAAC;IACH,cAAc,EAAE,MAAM;IACtB,WAAW,EAAE,UAAU;IACvB,GAAG,EA3EI,MAAM;GA2EQ;EAEzB,AAAA,GAAG,CAAC;IACA,KAAK,EAAE,IAAI;IACX,eAAe,EAAE,UAAU;IAC3B,UAAU,EAhFH,MAAM;GAgFe;CALP;;AAO7B,AAAA,IAAI,CAAC;EACD,MAAM,EAnFK,MAAM,CAmFK,CAAC;EACvB,OAAO,EApFI,MAAM;CAoFQ;;AAE7B,AAAA,MAAM,CAAC;EACH,UAAU,EDlEJ,OAAO;ECmEb,MAAM,EAxFK,MAAM;EAyFjB,OAAO,EAzFI,MAAM;EA0FjB,aAAa,EAxFD,GAAG;EAyFf,MAAM,EAAE,MAAM;EACd,UAAU,EAAE,MAAM;CAAG;;AAEzB,AAAA,MAAM,CAAC,CAAC,CAAC;EACL,MAAM,EAAE,CAAC;EACT,SAAS,EAAE,MAAM;EACjB,KAAK,EDzEK,OAAO;EC0EjB,UAAU,EAAE,MAAM;CAAG;;AAEzB,AAAA,OAAO,CAAC;EACJ,aAAa,EAAE,GAAG,CAAC,KAAK,CDhFlB,OAAO;ECiFb,MAAM,EArGQ,IAAI,CAqGO,CAAC;EAC1B,cAAc,EAtGA,IAAI;CAsGiB;;AAEvC,AAAA,YAAY,CAAC;EACT,aAAa,EAAE,GAAG,CAAC,KAAK,CDrFlB,OAAO;ECsFb,MAAM,EA1GQ,IAAI,CA0GO,CAAC;EAC1B,cAAc,EA3GA,IAAI;EA4GlB,UAAU,EAAE,MAAM;CAKU;;AAThC,AAKI,YALQ,CAKR,EAAE,CAAC;EACC,MAAM,EAAE,CAAC;CAAG;;AANpB,AAOI,YAPQ,CAOR,KAAK,CAAC;EACF,SAAS,EAAE,MAAM;EACjB,KAAK,ED1FC,OAAO;CC0FS;;ACpH9B,AAAA,KAAK,AAAA,eAAe,CAAC;EACjB,KAAK,EAAE,IAAI;EACX,eAAe,EAAE,QAAQ;EAEzB,UAAU,EAAE,UAAU;EACtB,UAAU,EFkBJ,OAAO;EEjBb,UAAU,EAAE,IAAI;CAuDmB;;AA7DvC,AAQI,KARC,AAAA,eAAe,CAQhB,EAAE,CAAC;EACC,aAAa,EAAE,GAAG,CAAC,KAAK,CFanB,OAAO;CELgB;;AAjBpC,AAUQ,KAVH,AAAA,eAAe,CAQhB,EAAE,CAEI,SAAU,CAAA,IAAI,EAAE;EACd,UAAU,EFYZ,OAAO;EEXL,UAAU,EAAE,2BAA2B;CAAG;;AAZtD,AAaQ,KAbH,AAAA,eAAe,CAQhB,EAAE,CAKI,SAAU,CAAA,GAAG,EAAE;EACb,UAAU,EFSZ,OAAO;EERL,UAAU,EAAE,2BAA2B;CAAG;;AAftD,AAgBQ,KAhBH,AAAA,eAAe,CAQhB,EAAE,CAQI,KAAK,EAhBf,KAAK,AAAA,eAAe,CAQhB,EAAE,CAQa,KAAK,CAAC;EACb,UAAU,EFOb,OAAO;CEPkB;;AAjBlC,AAmBI,KAnBC,AAAA,eAAe,CAmBhB,KAAK,CAAC;EACF,UAAU,EAAE,IAAI;EAChB,MAAM,EAAE,IAAI;EACZ,UAAU,EFDR,OAAO;EEET,aAAa,EDnBL,GAAG,CAAH,GAAG,CCmBkC,CAAC,CAAC,CAAC;CAAG;;AAvB3D,AAyBI,KAzBC,AAAA,eAAe,CAyBhB,EAAE,CAAC;EACC,KAAK,EFDN,OAAO;EEEN,OAAO,EAAE,aAAa;EACtB,UAAU,EAAE,IAAI;EAChB,WAAW,EAAE,GAAG;EAChB,MAAM,EAAE,IAAI;CAAG;;AA9BvB,AAgCI,KAhCC,AAAA,eAAe,CAgChB,EAAE,CAAC;EACC,OAAO,EAAE,aAAa;EACtB,UAAU,EAAE,IAAI;EAChB,WAAW,EAAE,GAAG;EAChB,MAAM,EAAE,IAAI;CAAG;;AApCvB,AAsCI,KAtCC,AAAA,eAAe,CAsChB,CAAC,AAAA,UAAU,CAAC;EACR,OAAO,EAAE,aAAa;EACtB,MAAM,EAAE,MAAM;EACd,OAAO,EAAE,YAAY;EACrB,aAAa,EDtCL,GAAG;ECuCX,eAAe,EAAE,IAAI;EACrB,WAAW,EAAE,GAAG;EAChB,KAAK,EFpBN,OAAO;EEqBN,UAAU,EAAE,mDAAmD;CAGnB;;AAjDpD,AA+CQ,KA/CH,AAAA,eAAe,CAsChB,CAAC,AAAA,UAAU,CASL,KAAK,EA/Cf,KAAK,AAAA,eAAe,CAsChB,CAAC,AAAA,UAAU,CASI,KAAK,CAAC;EACb,KAAK,EF3BP,OAAO,CE2BW,UAAU;EAC1B,UAAU,EFvBR,OAAO,CEuBgB,UAAU;CAAG;;AAjDlD,AAmDI,KAnDC,AAAA,eAAe,CAmDhB,CAAC,AAAA,cAAc,CAAC;EACZ,OAAO,EAAE,CAAC;EACV,MAAM,EAAE,MAAM;EACd,OAAO,EAAE,YAAY;EACrB,aAAa,EDnDL,GAAG;ECoDX,eAAe,EAAE,IAAI;EACrB,WAAW,EAAE,GAAG;EAChB,KAAK,EFjCN,OAAO;EEkCN,UAAU,EAAE,sBAAsB;CAEL;;AA7DrC,AA4DQ,KA5DH,AAAA,eAAe,CAmDhB,CAAC,AAAA,cAAc,CAST,KAAK,EA5Df,KAAK,AAAA,eAAe,CAmDhB,CAAC,AAAA,cAAc,CASA,KAAK,CAAC;EACb,KAAK,EFjDF,OAAO;CEiDa;;AAEnC,AAAA,cAAc,CAAC,CAAC,AAAA,UAAU,CAAC;EACvB,OAAO,EAAE,aAAa;EACtB,MAAM,EAAE,MAAM;EACd,OAAO,EAAE,YAAY;EACrB,aAAa,ED/DD,GAAG;ECgEf,eAAe,EAAE,IAAI;EACrB,WAAW,EAAE,GAAG;EAChB,KAAK,EF7CF,OAAO;EE8CV,UAAU,EAAE,sBAAsB;EAClC,SAAS,EAAE,MAAM;CAEO;;AAX5B,AAUI,cAVU,CAAC,CAAC,AAAA,UAAU,CAUpB,KAAK,EAVX,cAAc,CAAC,CAAC,AAAA,UAAU,CAUX,KAAK,CAAC;EACb,KAAK,EFrDH,OAAO;CEqDS;;AC3E1B,gBAAgB;AAEhB,AAAA,CAAC,CAAC;EACE,KAAK,EHGC,OAAO;EGFb,eAAe,EAAE,SAAS;EAC1B,UAAU,EAAE,sBAAsB;CAEX;;AAL3B,AAII,CAJH,CAIK,KAAK,EAJX,CAAC,CAIc,KAAK,CAAC;EACb,KAAK,EHIJ,OAAO;CGJS;;AAEzB,AAAA,YAAY,CAAC;EACT,UAAU,EAAE,IAAI;CAAG;;AAEvB,AAAA,UAAU,CAAC;EACP,OAAO,EAAE,IAAI;EACb,GAAG,EFXQ,MAAM;EEYjB,WAAW,EAAE,IAAI;EACjB,MAAM,EFbK,MAAM,CEaK,CAAC;CAAG;;AAE9B,AAAA,UAAU,CAAC,EAAE,CAAC;EACV,IAAI,EAAE,IAAI;CAAG;;AAEjB,AAAA,UAAU,CAAC,EAAE,CAAC;EACV,UAAU,EAAE,IAAI;EAChB,MAAM,EAAE,CAAC;EACT,OAAO,EAAE,CAAC;EACV,OAAO,EAAE,IAAI;EACb,GAAG,EAAE,IAAI;EACT,SAAS,EAAE,IAAI;CAAG;;AAEtB,AAAA,UAAU,CAAC,EAAE,CAAC,EAAE,CAAC;EACb,MAAM,EAAE,CAAC;EACT,OAAO,EAAE,CAAC;CAAG;;AAEjB,AAAA,UAAU,CAAC,EAAE,CAAC,EAAE,CAAC,CAAC,CAAC;EACf,OAAO,EAAE,aAAa;EACtB,aAAa,EF9BD,GAAG;EE+Bf,UAAU,EH5BE,OAAO;EG6BnB,KAAK,EHfC,OAAO;EGgBb,eAAe,EAAE,IAAI;EACrB,WAAW,EAAE,GAAG;EAChB,UAAU,EAAE,2BAA2B;CAEL;;AATtC,AAQI,UARM,CAAC,EAAE,CAAC,EAAE,CAAC,CAAC,CAQZ,KAAK,EARX,UAAU,CAAC,EAAE,CAAC,EAAE,CAAC,CAAC,CAQH,KAAK,CAAC;EACb,UAAU,EH7BH,OAAO;CG6Bc;;AC1CpC,AACI,aADS,CACT,EAAE,CAAC;EACC,UAAU,EAAE,IAAI;EAChB,MAAM,EAAE,CAAC;EACT,OAAO,EAAE,CAAC;EACV,OAAO,EAAE,IAAI;EACb,cAAc,EAAE,MAAM;EACtB,GAAG,EAAE,GAAG;CAKmB;;AAZnC,AASQ,aATK,CACT,EAAE,CAQE,EAAE,CAAC;EACC,UAAU,EJcZ,OAAO;EIbL,aAAa,EAAE,GAAG;EAClB,OAAO,EAAE,SAAS;CAAG" } \ No newline at end of file diff --git a/css/styles.fc7cf65388be07f2e53293132dd0220e34d9861f57de4b336d64dd03a3502a9befbea05606442d0a501005442835a864361b9a51b4b51acbf28df37530f61f31.css b/css/styles.e3fcfb3452c69d09414fe512e9dca31d879e4a6c47d23010fbb07eb6693d447f645d3bd2d021c0d28d0f7b4fe6f32a10e599488cdb16c6750a9a126788131917.css similarity index 86% rename from css/styles.fc7cf65388be07f2e53293132dd0220e34d9861f57de4b336d64dd03a3502a9befbea05606442d0a501005442835a864361b9a51b4b51acbf28df37530f61f31.css rename to css/styles.e3fcfb3452c69d09414fe512e9dca31d879e4a6c47d23010fbb07eb6693d447f645d3bd2d021c0d28d0f7b4fe6f32a10e599488cdb16c6750a9a126788131917.css index 7c91143..0c6fe0e 100644 --- a/css/styles.fc7cf65388be07f2e53293132dd0220e34d9861f57de4b336d64dd03a3502a9befbea05606442d0a501005442835a864361b9a51b4b51acbf28df37530f61f31.css +++ b/css/styles.e3fcfb3452c69d09414fe512e9dca31d879e4a6c47d23010fbb07eb6693d447f645d3bd2d021c0d28d0f7b4fe6f32a10e599488cdb16c6750a9a126788131917.css @@ -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 */ \ No newline at end of file diff --git a/developers/index.html b/developers/index.html index 15f28cb..8e4b67c 100644 --- a/developers/index.html +++ b/developers/index.html @@ -1,6 +1,6 @@ - + @@ -13,16 +13,16 @@ - + - + - - - - + + + + - + @@ -70,10 +70,28 @@ - Test Dev + id="developers_microsoft-research" + style="background:rgba(38,15,27,0.4)" + href="/developers/microsoft-research"> + Microsoft Research + + + + + + + + + + + + + + SRI International diff --git a/developers/index.xml b/developers/index.xml index b5a137a..8a4c344 100644 --- a/developers/index.xml +++ b/developers/index.xml @@ -2,17 +2,24 @@ Developers on Formal Methods Tools - https://example.org/developers/ + http://localhost:1313/developers/ Recent content in Developers on Formal Methods Tools Hugo en-us Fri, 02 Feb 2024 04:14:54 -0800 - + - Test Dev - https://example.org/developers/test-dev/ + Microsoft Research + http://localhost:1313/developers/microsoft-research/ Fri, 02 Feb 2024 04:14:54 -0800 - https://example.org/developers/test-dev/ + http://localhost:1313/developers/microsoft-research/ + + + + SRI International + http://localhost:1313/developers/sri-international/ + Fri, 02 Feb 2024 04:14:54 -0800 + http://localhost:1313/developers/sri-international/ diff --git a/developers/microsoft-research/index.html b/developers/microsoft-research/index.html new file mode 100644 index 0000000..3f42e4b --- /dev/null +++ b/developers/microsoft-research/index.html @@ -0,0 +1,69 @@ + + + + + + + +Microsoft Research | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + +
+

Formal Methods Tools

+ + + + +
+
+ +

Microsoft Research

+ + +

Z3

+ + +
+ + + diff --git a/developers/microsoft-research/index.xml b/developers/microsoft-research/index.xml new file mode 100644 index 0000000..e584c28 --- /dev/null +++ b/developers/microsoft-research/index.xml @@ -0,0 +1,19 @@ + + + + Microsoft Research on Formal Methods Tools + http://localhost:1313/developers/microsoft-research/ + Recent content in Microsoft Research on Formal Methods Tools + Hugo + en-us + Fri, 02 Feb 2024 04:14:54 -0800 + + + Z3 + http://localhost:1313/tools/z3/ + Fri, 02 Feb 2024 04:14:54 -0800 + http://localhost:1313/tools/z3/ + <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> + + + diff --git a/developers/sri-international/index.html b/developers/sri-international/index.html new file mode 100644 index 0000000..04d7251 --- /dev/null +++ b/developers/sri-international/index.html @@ -0,0 +1,69 @@ + + + + + + + +SRI International | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + +
+

Formal Methods Tools

+ + + + +
+
+ +

SRI International

+ + +

Yices 2

+ + +
+ + + diff --git a/developers/sri-international/index.xml b/developers/sri-international/index.xml new file mode 100644 index 0000000..702e419 --- /dev/null +++ b/developers/sri-international/index.xml @@ -0,0 +1,19 @@ + + + + SRI International on Formal Methods Tools + http://localhost:1313/developers/sri-international/ + Recent content in SRI International on Formal Methods Tools + Hugo + en-us + Fri, 02 Feb 2024 04:14:54 -0800 + + + Yices 2 + http://localhost:1313/tools/yices/ + Fri, 02 Feb 2024 04:14:54 -0800 + http://localhost:1313/tools/yices/ + <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> + + + diff --git a/developers/test-dev/index.html b/developers/test-dev/index.html deleted file mode 100644 index a9e4c75..0000000 --- a/developers/test-dev/index.html +++ /dev/null @@ -1,69 +0,0 @@ - - - - - - - -Test Dev | Formal Methods Tools - - - - - - - - - - - - - - - - - - - - - - - - -
-

Formal Methods Tools

- - - - -
-
- -

Test Dev

- - -

Z3 Theorem Prover

- - -
- - - diff --git a/developers/test-dev/index.xml b/developers/test-dev/index.xml deleted file mode 100644 index d65ecfc..0000000 --- a/developers/test-dev/index.xml +++ /dev/null @@ -1,19 +0,0 @@ - - - - Test Dev on Formal Methods Tools - https://example.org/developers/test-dev/ - Recent content in Test Dev on Formal Methods Tools - Hugo - en-us - Fri, 02 Feb 2024 04:14:54 -0800 - - - Z3 Theorem Prover - https://example.org/tools/z3/ - Fri, 02 Feb 2024 04:14:54 -0800 - https://example.org/tools/z3/ - <p>desc</p> - - - diff --git a/domains/embedded-systems/index.html b/domains/embedded-systems/index.html new file mode 100644 index 0000000..cc471bc --- /dev/null +++ b/domains/embedded-systems/index.html @@ -0,0 +1,71 @@ + + + + + + + +Embedded Systems | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + +
+

Formal Methods Tools

+ + + + +
+
+ +

Embedded Systems

+ + +

Yices 2

+ +

Z3

+ + +
+ + + diff --git a/domains/embedded-systems/index.xml b/domains/embedded-systems/index.xml new file mode 100644 index 0000000..8f28794 --- /dev/null +++ b/domains/embedded-systems/index.xml @@ -0,0 +1,26 @@ + + + + Embedded Systems on Formal Methods Tools + http://localhost:1313/domains/embedded-systems/ + Recent content in Embedded Systems on Formal Methods Tools + Hugo + en-us + Fri, 02 Feb 2024 04:14:54 -0800 + + + Yices 2 + http://localhost:1313/tools/yices/ + Fri, 02 Feb 2024 04:14:54 -0800 + http://localhost:1313/tools/yices/ + <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> + + + Z3 + http://localhost:1313/tools/z3/ + Fri, 02 Feb 2024 04:14:54 -0800 + http://localhost:1313/tools/z3/ + <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> + + + diff --git a/domains/hardware-verification/index.html b/domains/hardware-verification/index.html new file mode 100644 index 0000000..1ae454f --- /dev/null +++ b/domains/hardware-verification/index.html @@ -0,0 +1,71 @@ + + + + + + + +Hardware Verification | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + +
+

Formal Methods Tools

+ + + + +
+
+ +

Hardware Verification

+ + +

Yices 2

+ +

Z3

+ + +
+ + + diff --git a/domains/hardware-verification/index.xml b/domains/hardware-verification/index.xml new file mode 100644 index 0000000..10f60fc --- /dev/null +++ b/domains/hardware-verification/index.xml @@ -0,0 +1,26 @@ + + + + Hardware Verification on Formal Methods Tools + http://localhost:1313/domains/hardware-verification/ + Recent content in Hardware Verification on Formal Methods Tools + Hugo + en-us + Fri, 02 Feb 2024 04:14:54 -0800 + + + Yices 2 + http://localhost:1313/tools/yices/ + Fri, 02 Feb 2024 04:14:54 -0800 + http://localhost:1313/tools/yices/ + <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> + + + Z3 + http://localhost:1313/tools/z3/ + Fri, 02 Feb 2024 04:14:54 -0800 + http://localhost:1313/tools/z3/ + <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> + + + diff --git a/domains/index.html b/domains/index.html index ee361be..9553ae2 100644 --- a/domains/index.html +++ b/domains/index.html @@ -1,6 +1,6 @@ - + @@ -13,16 +13,16 @@ - + - + - - - - + + + + - + @@ -70,10 +70,46 @@ - Tttt + id="domains_embedded-systems" + style="background:rgba(130,108,187,0.4)" + href="/domains/embedded-systems"> + Embedded Systems + + + + + + + + + + + + + + Hardware Verification + + + + + + + + + + + + + + Software Verification diff --git a/domains/index.xml b/domains/index.xml index 573b778..7aeb8fd 100644 --- a/domains/index.xml +++ b/domains/index.xml @@ -2,17 +2,31 @@ Domains on Formal Methods Tools - https://example.org/domains/ + http://localhost:1313/domains/ Recent content in Domains on Formal Methods Tools Hugo en-us Fri, 02 Feb 2024 04:14:54 -0800 - + - Tttt - https://example.org/domains/tttt/ + Embedded Systems + http://localhost:1313/domains/embedded-systems/ Fri, 02 Feb 2024 04:14:54 -0800 - https://example.org/domains/tttt/ + http://localhost:1313/domains/embedded-systems/ + + + + Hardware Verification + http://localhost:1313/domains/hardware-verification/ + Fri, 02 Feb 2024 04:14:54 -0800 + http://localhost:1313/domains/hardware-verification/ + + + + Software Verification + http://localhost:1313/domains/software-verification/ + Fri, 02 Feb 2024 04:14:54 -0800 + http://localhost:1313/domains/software-verification/ diff --git a/domains/software-verification/index.html b/domains/software-verification/index.html new file mode 100644 index 0000000..32fa444 --- /dev/null +++ b/domains/software-verification/index.html @@ -0,0 +1,71 @@ + + + + + + + +Software Verification | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + +
+

Formal Methods Tools

+ + + + +
+
+ +

Software Verification

+ + +

Yices 2

+ +

Z3

+ + +
+
+

Copyright 2025. All rights reserved.

+ +
+ + diff --git a/domains/software-verification/index.xml b/domains/software-verification/index.xml new file mode 100644 index 0000000..4798087 --- /dev/null +++ b/domains/software-verification/index.xml @@ -0,0 +1,26 @@ + + + + Software Verification on Formal Methods Tools + http://localhost:1313/domains/software-verification/ + Recent content in Software Verification on Formal Methods Tools + Hugo + en-us + Fri, 02 Feb 2024 04:14:54 -0800 + + + Yices 2 + http://localhost:1313/tools/yices/ + Fri, 02 Feb 2024 04:14:54 -0800 + http://localhost:1313/tools/yices/ + <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> + + + Z3 + http://localhost:1313/tools/z3/ + Fri, 02 Feb 2024 04:14:54 -0800 + http://localhost:1313/tools/z3/ + <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> + + + diff --git a/domains/tttt/index.html b/domains/tttt/index.html deleted file mode 100644 index d43f22e..0000000 --- a/domains/tttt/index.html +++ /dev/null @@ -1,69 +0,0 @@ - - - - - - - -Tttt | Formal Methods Tools - - - - - - - - - - - - - - - - - - - - - - - - -
-

Formal Methods Tools

- - - - -
-
- -

Tttt

- - -

Z3 Theorem Prover

- - -
-
-

Copyright 2025. All rights reserved.

- -
- - diff --git a/domains/tttt/index.xml b/domains/tttt/index.xml deleted file mode 100644 index e184980..0000000 --- a/domains/tttt/index.xml +++ /dev/null @@ -1,19 +0,0 @@ - - - - Tttt on Formal Methods Tools - https://example.org/domains/tttt/ - Recent content in Tttt on Formal Methods Tools - Hugo - en-us - Fri, 02 Feb 2024 04:14:54 -0800 - - - Z3 Theorem Prover - https://example.org/tools/z3/ - Fri, 02 Feb 2024 04:14:54 -0800 - https://example.org/tools/z3/ - <p>desc</p> - - - diff --git a/formalisms/arithmetic/index.html b/formalisms/arithmetic/index.html new file mode 100644 index 0000000..a462b86 --- /dev/null +++ b/formalisms/arithmetic/index.html @@ -0,0 +1,71 @@ + + + + + + + +Arithmetic | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + +
+

Formal Methods Tools

+ + + + +
+
+ +

Arithmetic

+ + +

Yices 2

+ +

Z3

+ + +
+
+

Copyright 2025. All rights reserved.

+ +
+ + diff --git a/formalisms/arithmetic/index.xml b/formalisms/arithmetic/index.xml new file mode 100644 index 0000000..62f96b8 --- /dev/null +++ b/formalisms/arithmetic/index.xml @@ -0,0 +1,26 @@ + + + + Arithmetic on Formal Methods Tools + http://localhost:1313/formalisms/arithmetic/ + Recent content in Arithmetic on Formal Methods Tools + Hugo + en-us + Fri, 02 Feb 2024 04:14:54 -0800 + + + Yices 2 + http://localhost:1313/tools/yices/ + Fri, 02 Feb 2024 04:14:54 -0800 + http://localhost:1313/tools/yices/ + <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> + + + Z3 + http://localhost:1313/tools/z3/ + Fri, 02 Feb 2024 04:14:54 -0800 + http://localhost:1313/tools/z3/ + <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> + + + diff --git a/formalisms/arrays/index.html b/formalisms/arrays/index.html new file mode 100644 index 0000000..f938286 --- /dev/null +++ b/formalisms/arrays/index.html @@ -0,0 +1,71 @@ + + + + + + + +Arrays | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + +
+

Formal Methods Tools

+ + + + +
+
+ +

Arrays

+ + +

Yices 2

+ +

Z3

+ + +
+
+

Copyright 2025. All rights reserved.

+ +
+ + diff --git a/formalisms/arrays/index.xml b/formalisms/arrays/index.xml new file mode 100644 index 0000000..9d6c1f5 --- /dev/null +++ b/formalisms/arrays/index.xml @@ -0,0 +1,26 @@ + + + + Arrays on Formal Methods Tools + http://localhost:1313/formalisms/arrays/ + Recent content in Arrays on Formal Methods Tools + Hugo + en-us + Fri, 02 Feb 2024 04:14:54 -0800 + + + Yices 2 + http://localhost:1313/tools/yices/ + Fri, 02 Feb 2024 04:14:54 -0800 + http://localhost:1313/tools/yices/ + <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> + + + Z3 + http://localhost:1313/tools/z3/ + Fri, 02 Feb 2024 04:14:54 -0800 + http://localhost:1313/tools/z3/ + <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> + + + diff --git a/formalisms/bit-vectors/index.html b/formalisms/bit-vectors/index.html new file mode 100644 index 0000000..01dbfd6 --- /dev/null +++ b/formalisms/bit-vectors/index.html @@ -0,0 +1,71 @@ + + + + + + + +Bit-Vectors | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + +
+

Formal Methods Tools

+ + + + +
+
+ +

Bit-Vectors

+ + +

Yices 2

+ +

Z3

+ + +
+
+

Copyright 2025. All rights reserved.

+ +
+ + diff --git a/formalisms/bit-vectors/index.xml b/formalisms/bit-vectors/index.xml new file mode 100644 index 0000000..917d870 --- /dev/null +++ b/formalisms/bit-vectors/index.xml @@ -0,0 +1,26 @@ + + + + Bit-Vectors on Formal Methods Tools + http://localhost:1313/formalisms/bit-vectors/ + Recent content in Bit-Vectors on Formal Methods Tools + Hugo + en-us + Fri, 02 Feb 2024 04:14:54 -0800 + + + Yices 2 + http://localhost:1313/tools/yices/ + Fri, 02 Feb 2024 04:14:54 -0800 + http://localhost:1313/tools/yices/ + <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> + + + Z3 + http://localhost:1313/tools/z3/ + Fri, 02 Feb 2024 04:14:54 -0800 + http://localhost:1313/tools/z3/ + <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> + + + diff --git a/formalisms/first-order-logic/index.html b/formalisms/first-order-logic/index.html new file mode 100644 index 0000000..0e3d086 --- /dev/null +++ b/formalisms/first-order-logic/index.html @@ -0,0 +1,71 @@ + + + + + + + +First-Order Logic | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + +
+

Formal Methods Tools

+ + + + +
+
+ +

First-Order Logic

+ + +

Yices 2

+ +

Z3

+ + +
+
+

Copyright 2025. All rights reserved.

+ +
+ + diff --git a/formalisms/first-order-logic/index.xml b/formalisms/first-order-logic/index.xml new file mode 100644 index 0000000..2d380e9 --- /dev/null +++ b/formalisms/first-order-logic/index.xml @@ -0,0 +1,26 @@ + + + + First-Order Logic on Formal Methods Tools + http://localhost:1313/formalisms/first-order-logic/ + Recent content in First-Order Logic on Formal Methods Tools + Hugo + en-us + Fri, 02 Feb 2024 04:14:54 -0800 + + + Yices 2 + http://localhost:1313/tools/yices/ + Fri, 02 Feb 2024 04:14:54 -0800 + http://localhost:1313/tools/yices/ + <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> + + + Z3 + http://localhost:1313/tools/z3/ + Fri, 02 Feb 2024 04:14:54 -0800 + http://localhost:1313/tools/z3/ + <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> + + + diff --git a/formalisms/index.html b/formalisms/index.html index 6b93092..0111324 100644 --- a/formalisms/index.html +++ b/formalisms/index.html @@ -1,6 +1,6 @@ - + @@ -13,16 +13,16 @@ - + - + - - - - + + + + - + @@ -70,10 +70,118 @@ - Tttt + id="formalisms_arithmetic" + style="background:rgba(155,143,9,0.4)" + href="/formalisms/arithmetic"> + Arithmetic + + + + + + + + + + + + + + Arrays + + + + + + + + + + + + + + Bit-Vectors + + + + + + + + + + + + + + First-Order Logic + + + + + + + + + + + + + + Quantifier Logic + + + + + + + + + + + + + + SMT-LIB + + + + + + + + + + + + + + Uninterpreted Functions diff --git a/formalisms/index.xml b/formalisms/index.xml index 936563b..4f275ba 100644 --- a/formalisms/index.xml +++ b/formalisms/index.xml @@ -2,17 +2,59 @@ Formalisms on Formal Methods Tools - https://example.org/formalisms/ + http://localhost:1313/formalisms/ Recent content in Formalisms on Formal Methods Tools Hugo en-us Fri, 02 Feb 2024 04:14:54 -0800 - + - Tttt - https://example.org/formalisms/tttt/ + Arithmetic + http://localhost:1313/formalisms/arithmetic/ Fri, 02 Feb 2024 04:14:54 -0800 - https://example.org/formalisms/tttt/ + http://localhost:1313/formalisms/arithmetic/ + + + + Arrays + http://localhost:1313/formalisms/arrays/ + Fri, 02 Feb 2024 04:14:54 -0800 + http://localhost:1313/formalisms/arrays/ + + + + Bit-Vectors + http://localhost:1313/formalisms/bit-vectors/ + Fri, 02 Feb 2024 04:14:54 -0800 + http://localhost:1313/formalisms/bit-vectors/ + + + + First-Order Logic + http://localhost:1313/formalisms/first-order-logic/ + Fri, 02 Feb 2024 04:14:54 -0800 + http://localhost:1313/formalisms/first-order-logic/ + + + + Quantifier Logic + http://localhost:1313/formalisms/quantifier-logic/ + Fri, 02 Feb 2024 04:14:54 -0800 + http://localhost:1313/formalisms/quantifier-logic/ + + + + SMT-LIB + http://localhost:1313/formalisms/smt-lib/ + Fri, 02 Feb 2024 04:14:54 -0800 + http://localhost:1313/formalisms/smt-lib/ + + + + Uninterpreted Functions + http://localhost:1313/formalisms/uninterpreted-functions/ + Fri, 02 Feb 2024 04:14:54 -0800 + http://localhost:1313/formalisms/uninterpreted-functions/ diff --git a/formalisms/quantifier-logic/index.html b/formalisms/quantifier-logic/index.html new file mode 100644 index 0000000..cbe4946 --- /dev/null +++ b/formalisms/quantifier-logic/index.html @@ -0,0 +1,71 @@ + + + + + + + +Quantifier Logic | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + +
+

Formal Methods Tools

+ + + + +
+
+ +

Quantifier Logic

+ + +

Yices 2

+ +

Z3

+ + +
+
+

Copyright 2025. All rights reserved.

+ +
+ + diff --git a/formalisms/quantifier-logic/index.xml b/formalisms/quantifier-logic/index.xml new file mode 100644 index 0000000..51bcf34 --- /dev/null +++ b/formalisms/quantifier-logic/index.xml @@ -0,0 +1,26 @@ + + + + Quantifier Logic on Formal Methods Tools + http://localhost:1313/formalisms/quantifier-logic/ + Recent content in Quantifier Logic on Formal Methods Tools + Hugo + en-us + Fri, 02 Feb 2024 04:14:54 -0800 + + + Yices 2 + http://localhost:1313/tools/yices/ + Fri, 02 Feb 2024 04:14:54 -0800 + http://localhost:1313/tools/yices/ + <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> + + + Z3 + http://localhost:1313/tools/z3/ + Fri, 02 Feb 2024 04:14:54 -0800 + http://localhost:1313/tools/z3/ + <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> + + + diff --git a/formalisms/smt-lib/index.html b/formalisms/smt-lib/index.html new file mode 100644 index 0000000..13782b5 --- /dev/null +++ b/formalisms/smt-lib/index.html @@ -0,0 +1,71 @@ + + + + + + + +SMT-LIB | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + +
+

Formal Methods Tools

+ + + + +
+
+ +

SMT-LIB

+ + +

Yices 2

+ +

Z3

+ + +
+
+

Copyright 2025. All rights reserved.

+ +
+ + diff --git a/formalisms/smt-lib/index.xml b/formalisms/smt-lib/index.xml new file mode 100644 index 0000000..d9e4164 --- /dev/null +++ b/formalisms/smt-lib/index.xml @@ -0,0 +1,26 @@ + + + + SMT-LIB on Formal Methods Tools + http://localhost:1313/formalisms/smt-lib/ + Recent content in SMT-LIB on Formal Methods Tools + Hugo + en-us + Fri, 02 Feb 2024 04:14:54 -0800 + + + Yices 2 + http://localhost:1313/tools/yices/ + Fri, 02 Feb 2024 04:14:54 -0800 + http://localhost:1313/tools/yices/ + <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> + + + Z3 + http://localhost:1313/tools/z3/ + Fri, 02 Feb 2024 04:14:54 -0800 + http://localhost:1313/tools/z3/ + <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> + + + diff --git a/formalisms/tttt/index.html b/formalisms/tttt/index.html deleted file mode 100644 index af64867..0000000 --- a/formalisms/tttt/index.html +++ /dev/null @@ -1,69 +0,0 @@ - - - - - - - -Tttt | Formal Methods Tools - - - - - - - - - - - - - - - - - - - - - - - - -
-

Formal Methods Tools

- - - - -
-
- -

Tttt

- - -

Z3 Theorem Prover

- - -
-
-

Copyright 2025. All rights reserved.

- -
- - diff --git a/formalisms/tttt/index.xml b/formalisms/tttt/index.xml deleted file mode 100644 index 9474395..0000000 --- a/formalisms/tttt/index.xml +++ /dev/null @@ -1,19 +0,0 @@ - - - - Tttt on Formal Methods Tools - https://example.org/formalisms/tttt/ - Recent content in Tttt on Formal Methods Tools - Hugo - en-us - Fri, 02 Feb 2024 04:14:54 -0800 - - - Z3 Theorem Prover - https://example.org/tools/z3/ - Fri, 02 Feb 2024 04:14:54 -0800 - https://example.org/tools/z3/ - <p>desc</p> - - - diff --git a/formalisms/uninterpreted-functions/index.html b/formalisms/uninterpreted-functions/index.html new file mode 100644 index 0000000..2c6bcf6 --- /dev/null +++ b/formalisms/uninterpreted-functions/index.html @@ -0,0 +1,71 @@ + + + + + + + +Uninterpreted Functions | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + +
+

Formal Methods Tools

+ + + + +
+
+ +

Uninterpreted Functions

+ + +

Yices 2

+ +

Z3

+ + +
+
+

Copyright 2025. All rights reserved.

+ +
+ + diff --git a/formalisms/uninterpreted-functions/index.xml b/formalisms/uninterpreted-functions/index.xml new file mode 100644 index 0000000..c10076e --- /dev/null +++ b/formalisms/uninterpreted-functions/index.xml @@ -0,0 +1,26 @@ + + + + Uninterpreted Functions on Formal Methods Tools + http://localhost:1313/formalisms/uninterpreted-functions/ + Recent content in Uninterpreted Functions on Formal Methods Tools + Hugo + en-us + Fri, 02 Feb 2024 04:14:54 -0800 + + + Yices 2 + http://localhost:1313/tools/yices/ + Fri, 02 Feb 2024 04:14:54 -0800 + http://localhost:1313/tools/yices/ + <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> + + + Z3 + http://localhost:1313/tools/z3/ + Fri, 02 Feb 2024 04:14:54 -0800 + http://localhost:1313/tools/z3/ + <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> + + + diff --git a/index.html b/index.html index 135b601..a522ec3 100644 --- a/index.html +++ b/index.html @@ -1,7 +1,7 @@ - + @@ -15,16 +15,16 @@ - + - + - - - - + + + + - + @@ -65,9 +65,13 @@ excepteur excepteur pariatur nostrud qui irure ullamco.

Featured Tools

-

Z3 Theorem Prover

-

desc

-

+

Z3

+

Z3 is a high-performance SMT solver and theorem prover developed by Microsoft Research. It is widely …

+
+ +
+

Yices 2

+

Yices is a high-performance SMT solver and theorem prover developed by SRI International. It is …

diff --git a/index.xml b/index.xml index 2c4f7f7..7300065 100644 --- a/index.xml +++ b/index.xml @@ -2,18 +2,25 @@ Home on Formal Methods Tools - https://example.org/ + http://localhost:1313/ Recent content in Home on Formal Methods Tools Hugo en-us Fri, 02 Feb 2024 04:14:54 -0800 - + - Z3 Theorem Prover - https://example.org/tools/z3/ + Yices 2 + http://localhost:1313/tools/yices/ Fri, 02 Feb 2024 04:14:54 -0800 - https://example.org/tools/z3/ - <p>desc</p> + http://localhost:1313/tools/yices/ + <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> + + + Z3 + http://localhost:1313/tools/z3/ + Fri, 02 Feb 2024 04:14:54 -0800 + http://localhost:1313/tools/z3/ + <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> diff --git a/interactions/araafafanpoasi/index.html b/interactions/araafafanpoasi/index.html deleted file mode 100644 index c25c355..0000000 --- a/interactions/araafafanpoasi/index.html +++ /dev/null @@ -1,69 +0,0 @@ - - - - - - - -Araafafanpoasi | Formal Methods Tools - - - - - - - - - - - - - - - - - - - - - - - - -
-

Formal Methods Tools

- - - - -
-
- -

Araafafanpoasi

- - -

Z3 Theorem Prover

- - -
-
-

Copyright 2025. All rights reserved.

- -
- - diff --git a/interactions/araafafanpoasi/index.xml b/interactions/araafafanpoasi/index.xml deleted file mode 100644 index bfabb3e..0000000 --- a/interactions/araafafanpoasi/index.xml +++ /dev/null @@ -1,19 +0,0 @@ - - - - Araafafanpoasi on Formal Methods Tools - https://example.org/interactions/araafafanpoasi/ - Recent content in Araafafanpoasi on Formal Methods Tools - Hugo - en-us - Fri, 02 Feb 2024 04:14:54 -0800 - - - Z3 Theorem Prover - https://example.org/tools/z3/ - Fri, 02 Feb 2024 04:14:54 -0800 - https://example.org/tools/z3/ - <p>desc</p> - - - diff --git a/interactions/aranapoasi/index.html b/interactions/aranapoasi/index.html deleted file mode 100644 index 9443d68..0000000 --- a/interactions/aranapoasi/index.html +++ /dev/null @@ -1,69 +0,0 @@ - - - - - - - -Aranapoasi | Formal Methods Tools - - - - - - - - - - - - - - - - - - - - - - - - -
-

Formal Methods Tools

- - - - -
-
- -

Aranapoasi

- - -

Z3 Theorem Prover

- - -
-
-

Copyright 2025. All rights reserved.

- -
- - diff --git a/interactions/aranapoasi/index.xml b/interactions/aranapoasi/index.xml deleted file mode 100644 index eef77aa..0000000 --- a/interactions/aranapoasi/index.xml +++ /dev/null @@ -1,19 +0,0 @@ - - - - Aranapoasi on Formal Methods Tools - https://example.org/interactions/aranapoasi/ - Recent content in Aranapoasi on Formal Methods Tools - Hugo - en-us - Fri, 02 Feb 2024 04:14:54 -0800 - - - Z3 Theorem Prover - https://example.org/tools/z3/ - Fri, 02 Feb 2024 04:14:54 -0800 - https://example.org/tools/z3/ - <p>desc</p> - - - diff --git a/interactions/aranpoasadfsi/index.html b/interactions/aranpoasadfsi/index.html deleted file mode 100644 index 00e4677..0000000 --- a/interactions/aranpoasadfsi/index.html +++ /dev/null @@ -1,69 +0,0 @@ - - - - - - - -Aranpoasadfsi | Formal Methods Tools - - - - - - - - - - - - - - - - - - - - - - - - -
-

Formal Methods Tools

- - - - -
-
- -

Aranpoasadfsi

- - -

Z3 Theorem Prover

- - -
-
-

Copyright 2025. All rights reserved.

- -
- - diff --git a/interactions/aranpoasadfsi/index.xml b/interactions/aranpoasadfsi/index.xml deleted file mode 100644 index 88808c3..0000000 --- a/interactions/aranpoasadfsi/index.xml +++ /dev/null @@ -1,19 +0,0 @@ - - - - Aranpoasadfsi on Formal Methods Tools - https://example.org/interactions/aranpoasadfsi/ - Recent content in Aranpoasadfsi on Formal Methods Tools - Hugo - en-us - Fri, 02 Feb 2024 04:14:54 -0800 - - - Z3 Theorem Prover - https://example.org/tools/z3/ - Fri, 02 Feb 2024 04:14:54 -0800 - https://example.org/tools/z3/ - <p>desc</p> - - - diff --git a/interactions/aranpoasai/index.html b/interactions/aranpoasai/index.html deleted file mode 100644 index e71e84b..0000000 --- a/interactions/aranpoasai/index.html +++ /dev/null @@ -1,69 +0,0 @@ - - - - - - - -Aranpoasai | Formal Methods Tools - - - - - - - - - - - - - - - - - - - - - - - - -
-

Formal Methods Tools

- - - - -
-
- -

Aranpoasai

- - -

Z3 Theorem Prover

- - -
-
-

Copyright 2025. All rights reserved.

- -
- - diff --git a/interactions/aranpoasai/index.xml b/interactions/aranpoasai/index.xml deleted file mode 100644 index 3572935..0000000 --- a/interactions/aranpoasai/index.xml +++ /dev/null @@ -1,19 +0,0 @@ - - - - Aranpoasai on Formal Methods Tools - https://example.org/interactions/aranpoasai/ - Recent content in Aranpoasai on Formal Methods Tools - Hugo - en-us - Fri, 02 Feb 2024 04:14:54 -0800 - - - Z3 Theorem Prover - https://example.org/tools/z3/ - Fri, 02 Feb 2024 04:14:54 -0800 - https://example.org/tools/z3/ - <p>desc</p> - - - diff --git a/interactions/aranpoasasdfasfasdfasdfi/index.html b/interactions/aranpoasasdfasfasdfasdfi/index.html deleted file mode 100644 index 49977ea..0000000 --- a/interactions/aranpoasasdfasfasdfasdfi/index.html +++ /dev/null @@ -1,69 +0,0 @@ - - - - - - - -Aranpoasasdfasfasdfasdfi | Formal Methods Tools - - - - - - - - - - - - - - - - - - - - - - - - -
-

Formal Methods Tools

- - - - -
-
- -

Aranpoasasdfasfasdfasdfi

- - -

Z3 Theorem Prover

- - -
-
-

Copyright 2025. All rights reserved.

- -
- - diff --git a/interactions/aranpoasasdfasfasdfasdfi/index.xml b/interactions/aranpoasasdfasfasdfasdfi/index.xml deleted file mode 100644 index dd79c75..0000000 --- a/interactions/aranpoasasdfasfasdfasdfi/index.xml +++ /dev/null @@ -1,19 +0,0 @@ - - - - Aranpoasasdfasfasdfasdfi on Formal Methods Tools - https://example.org/interactions/aranpoasasdfasfasdfasdfi/ - Recent content in Aranpoasasdfasfasdfasdfi on Formal Methods Tools - Hugo - en-us - Fri, 02 Feb 2024 04:14:54 -0800 - - - Z3 Theorem Prover - https://example.org/tools/z3/ - Fri, 02 Feb 2024 04:14:54 -0800 - https://example.org/tools/z3/ - <p>desc</p> - - - diff --git a/interactions/aranpoasi/index.html b/interactions/aranpoasi/index.html deleted file mode 100644 index 961e392..0000000 --- a/interactions/aranpoasi/index.html +++ /dev/null @@ -1,69 +0,0 @@ - - - - - - - -Aranpoasi | Formal Methods Tools - - - - - - - - - - - - - - - - - - - - - - - - -
-

Formal Methods Tools

- - - - -
-
- -

Aranpoasi

- - -

Z3 Theorem Prover

- - -
-
-

Copyright 2025. All rights reserved.

- -
- - diff --git a/interactions/aranpoasi/index.xml b/interactions/aranpoasi/index.xml deleted file mode 100644 index bf49c55..0000000 --- a/interactions/aranpoasi/index.xml +++ /dev/null @@ -1,19 +0,0 @@ - - - - Aranpoasi on Formal Methods Tools - https://example.org/interactions/aranpoasi/ - Recent content in Aranpoasi on Formal Methods Tools - Hugo - en-us - Fri, 02 Feb 2024 04:14:54 -0800 - - - Z3 Theorem Prover - https://example.org/tools/z3/ - Fri, 02 Feb 2024 04:14:54 -0800 - https://example.org/tools/z3/ - <p>desc</p> - - - diff --git a/interactions/aranpoaswei/index.html b/interactions/aranpoaswei/index.html deleted file mode 100644 index 28eaca9..0000000 --- a/interactions/aranpoaswei/index.html +++ /dev/null @@ -1,69 +0,0 @@ - - - - - - - -Aranpoaswei | Formal Methods Tools - - - - - - - - - - - - - - - - - - - - - - - - -
-

Formal Methods Tools

- - - - -
-
- -

Aranpoaswei

- - -

Z3 Theorem Prover

- - -
-
-

Copyright 2025. All rights reserved.

- -
- - diff --git a/interactions/aranpoaswei/index.xml b/interactions/aranpoaswei/index.xml deleted file mode 100644 index dde025f..0000000 --- a/interactions/aranpoaswei/index.xml +++ /dev/null @@ -1,19 +0,0 @@ - - - - Aranpoaswei on Formal Methods Tools - https://example.org/interactions/aranpoaswei/ - Recent content in Aranpoaswei on Formal Methods Tools - Hugo - en-us - Fri, 02 Feb 2024 04:14:54 -0800 - - - Z3 Theorem Prover - https://example.org/tools/z3/ - Fri, 02 Feb 2024 04:14:54 -0800 - https://example.org/tools/z3/ - <p>desc</p> - - - diff --git a/interactions/aranpoxasi/index.html b/interactions/aranpoxasi/index.html deleted file mode 100644 index b737bd8..0000000 --- a/interactions/aranpoxasi/index.html +++ /dev/null @@ -1,69 +0,0 @@ - - - - - - - -Aranpoxasi | Formal Methods Tools - - - - - - - - - - - - - - - - - - - - - - - - -
-

Formal Methods Tools

- - - - -
-
- -

Aranpoxasi

- - -

Z3 Theorem Prover

- - -
-
-

Copyright 2025. All rights reserved.

- -
- - diff --git a/interactions/aranpoxasi/index.xml b/interactions/aranpoxasi/index.xml deleted file mode 100644 index 34c0409..0000000 --- a/interactions/aranpoxasi/index.xml +++ /dev/null @@ -1,19 +0,0 @@ - - - - Aranpoxasi on Formal Methods Tools - https://example.org/interactions/aranpoxasi/ - Recent content in Aranpoxasi on Formal Methods Tools - Hugo - en-us - Fri, 02 Feb 2024 04:14:54 -0800 - - - Z3 Theorem Prover - https://example.org/tools/z3/ - Fri, 02 Feb 2024 04:14:54 -0800 - https://example.org/tools/z3/ - <p>desc</p> - - - diff --git a/interactions/aranpsoasi/index.html b/interactions/aranpsoasi/index.html deleted file mode 100644 index 1f0abf9..0000000 --- a/interactions/aranpsoasi/index.html +++ /dev/null @@ -1,69 +0,0 @@ - - - - - - - -Aranpsoasi | Formal Methods Tools - - - - - - - - - - - - - - - - - - - - - - - - -
-

Formal Methods Tools

- - - - -
-
- -

Aranpsoasi

- - -

Z3 Theorem Prover

- - -
-
-

Copyright 2025. All rights reserved.

- -
- - diff --git a/interactions/aranpsoasi/index.xml b/interactions/aranpsoasi/index.xml deleted file mode 100644 index 74062b8..0000000 --- a/interactions/aranpsoasi/index.xml +++ /dev/null @@ -1,19 +0,0 @@ - - - - Aranpsoasi on Formal Methods Tools - https://example.org/interactions/aranpsoasi/ - Recent content in Aranpsoasi on Formal Methods Tools - Hugo - en-us - Fri, 02 Feb 2024 04:14:54 -0800 - - - Z3 Theorem Prover - https://example.org/tools/z3/ - Fri, 02 Feb 2024 04:14:54 -0800 - https://example.org/tools/z3/ - <p>desc</p> - - - diff --git a/interactions/aransdpoasi/index.html b/interactions/aransdpoasi/index.html deleted file mode 100644 index bd6cfa6..0000000 --- a/interactions/aransdpoasi/index.html +++ /dev/null @@ -1,69 +0,0 @@ - - - - - - - -Aransdpoasi | Formal Methods Tools - - - - - - - - - - - - - - - - - - - - - - - - -
-

Formal Methods Tools

- - - - -
-
- -

Aransdpoasi

- - -

Z3 Theorem Prover

- - -
-
-

Copyright 2025. All rights reserved.

- -
- - diff --git a/interactions/aransdpoasi/index.xml b/interactions/aransdpoasi/index.xml deleted file mode 100644 index 32ec4b1..0000000 --- a/interactions/aransdpoasi/index.xml +++ /dev/null @@ -1,19 +0,0 @@ - - - - Aransdpoasi on Formal Methods Tools - https://example.org/interactions/aransdpoasi/ - Recent content in Aransdpoasi on Formal Methods Tools - Hugo - en-us - Fri, 02 Feb 2024 04:14:54 -0800 - - - Z3 Theorem Prover - https://example.org/tools/z3/ - Fri, 02 Feb 2024 04:14:54 -0800 - https://example.org/tools/z3/ - <p>desc</p> - - - diff --git a/interactions/c-api/index.html b/interactions/c-api/index.html new file mode 100644 index 0000000..d97979d --- /dev/null +++ b/interactions/c-api/index.html @@ -0,0 +1,69 @@ + + + + + + + +C API | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + +
+

Formal Methods Tools

+ + + + +
+
+ +

C API

+ + +

Yices 2

+ + +
+
+

Copyright 2025. All rights reserved.

+ +
+ + diff --git a/interactions/c-api/index.xml b/interactions/c-api/index.xml new file mode 100644 index 0000000..2332848 --- /dev/null +++ b/interactions/c-api/index.xml @@ -0,0 +1,19 @@ + + + + C API on Formal Methods Tools + http://localhost:1313/interactions/c-api/ + Recent content in C API on Formal Methods Tools + Hugo + en-us + Fri, 02 Feb 2024 04:14:54 -0800 + + + Yices 2 + http://localhost:1313/tools/yices/ + Fri, 02 Feb 2024 04:14:54 -0800 + http://localhost:1313/tools/yices/ + <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> + + + diff --git a/interactions/cli/index.html b/interactions/cli/index.html new file mode 100644 index 0000000..476f52a --- /dev/null +++ b/interactions/cli/index.html @@ -0,0 +1,71 @@ + + + + + + + +CLI | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + +
+

Formal Methods Tools

+ + + + +
+
+ +

CLI

+ + +

Yices 2

+ +

Z3

+ + +
+
+

Copyright 2025. All rights reserved.

+ +
+ + diff --git a/interactions/cli/index.xml b/interactions/cli/index.xml new file mode 100644 index 0000000..75b75a0 --- /dev/null +++ b/interactions/cli/index.xml @@ -0,0 +1,26 @@ + + + + CLI on Formal Methods Tools + http://localhost:1313/interactions/cli/ + Recent content in CLI on Formal Methods Tools + Hugo + en-us + Fri, 02 Feb 2024 04:14:54 -0800 + + + Yices 2 + http://localhost:1313/tools/yices/ + Fri, 02 Feb 2024 04:14:54 -0800 + http://localhost:1313/tools/yices/ + <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> + + + Z3 + http://localhost:1313/tools/z3/ + Fri, 02 Feb 2024 04:14:54 -0800 + http://localhost:1313/tools/z3/ + <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> + + + diff --git a/interactions/index.html b/interactions/index.html index 094987f..f5b2491 100644 --- a/interactions/index.html +++ b/interactions/index.html @@ -1,6 +1,6 @@ - + @@ -13,16 +13,16 @@ - + - + - - - - + + + + - + @@ -70,10 +70,10 @@ - Araafafanpoasi + id="interactions_c-api" + style="background:rgba(19,205,141,0.4)" + href="/interactions/c-api"> + C API @@ -88,10 +88,10 @@ - Aranapoasi + id="interactions_cli" + style="background:rgba(145,175,87,0.4)" + href="/interactions/cli"> + CLI @@ -106,10 +106,10 @@ - Aranpoasadfsi + id="interactions_ocaml-api" + style="background:rgba(54,250,207,0.4)" + href="/interactions/ocaml-api"> + OCaml API @@ -124,10 +124,10 @@ - Aranpoasai + id="interactions_playground" + style="background:rgba(165,254,219,0.4)" + href="/interactions/playground"> + Playground @@ -142,10 +142,10 @@ - Aranpoasasdfasfasdfasdfi + id="interactions_python-api" + style="background:rgba(2,212,135,0.4)" + href="/interactions/python-api"> + Python API @@ -160,10 +160,10 @@ - Aranpoasi + id="interactions_python-bindings" + style="background:rgba(37,32,133,0.4)" + href="/interactions/python-bindings"> + Python Bindings @@ -178,82 +178,10 @@ - Aranpoaswei - - - - - - - - - - - - - - Aranpoxasi - - - - - - - - - - - - - - Aranpsoasi - - - - - - - - - - - - - - Aransdpoasi - - - - - - - - - - - - - - Lorem Ipsum + id="interactions_rust-bindings" + style="background:rgba(124,204,243,0.4)" + href="/interactions/rust-bindings"> + Rust Bindings diff --git a/interactions/index.xml b/interactions/index.xml index f7feab3..2569d8f 100644 --- a/interactions/index.xml +++ b/interactions/index.xml @@ -2,87 +2,59 @@ Interactions on Formal Methods Tools - https://example.org/interactions/ + http://localhost:1313/interactions/ Recent content in Interactions on Formal Methods Tools Hugo en-us Fri, 02 Feb 2024 04:14:54 -0800 - + - Araafafanpoasi - https://example.org/interactions/araafafanpoasi/ + C API + http://localhost:1313/interactions/c-api/ Fri, 02 Feb 2024 04:14:54 -0800 - https://example.org/interactions/araafafanpoasi/ + http://localhost:1313/interactions/c-api/ - Aranapoasi - https://example.org/interactions/aranapoasi/ + CLI + http://localhost:1313/interactions/cli/ Fri, 02 Feb 2024 04:14:54 -0800 - https://example.org/interactions/aranapoasi/ + http://localhost:1313/interactions/cli/ - Aranpoasadfsi - https://example.org/interactions/aranpoasadfsi/ + OCaml API + http://localhost:1313/interactions/ocaml-api/ Fri, 02 Feb 2024 04:14:54 -0800 - https://example.org/interactions/aranpoasadfsi/ + http://localhost:1313/interactions/ocaml-api/ - Aranpoasai - https://example.org/interactions/aranpoasai/ + Playground + http://localhost:1313/interactions/playground/ Fri, 02 Feb 2024 04:14:54 -0800 - https://example.org/interactions/aranpoasai/ + http://localhost:1313/interactions/playground/ - Aranpoasasdfasfasdfasdfi - https://example.org/interactions/aranpoasasdfasfasdfasdfi/ + Python API + http://localhost:1313/interactions/python-api/ Fri, 02 Feb 2024 04:14:54 -0800 - https://example.org/interactions/aranpoasasdfasfasdfasdfi/ + http://localhost:1313/interactions/python-api/ - Aranpoasi - https://example.org/interactions/aranpoasi/ + Python Bindings + http://localhost:1313/interactions/python-bindings/ Fri, 02 Feb 2024 04:14:54 -0800 - https://example.org/interactions/aranpoasi/ + http://localhost:1313/interactions/python-bindings/ - Aranpoaswei - https://example.org/interactions/aranpoaswei/ + Rust Bindings + http://localhost:1313/interactions/rust-bindings/ Fri, 02 Feb 2024 04:14:54 -0800 - https://example.org/interactions/aranpoaswei/ - - - - Aranpoxasi - https://example.org/interactions/aranpoxasi/ - Fri, 02 Feb 2024 04:14:54 -0800 - https://example.org/interactions/aranpoxasi/ - - - - Aranpsoasi - https://example.org/interactions/aranpsoasi/ - Fri, 02 Feb 2024 04:14:54 -0800 - https://example.org/interactions/aranpsoasi/ - - - - Aransdpoasi - https://example.org/interactions/aransdpoasi/ - Fri, 02 Feb 2024 04:14:54 -0800 - https://example.org/interactions/aransdpoasi/ - - - - Lorem Ipsum - https://example.org/interactions/lorem-ipsum/ - Fri, 02 Feb 2024 04:14:54 -0800 - https://example.org/interactions/lorem-ipsum/ + http://localhost:1313/interactions/rust-bindings/ diff --git a/interactions/lorem-ipsum/index.html b/interactions/lorem-ipsum/index.html deleted file mode 100644 index 0023727..0000000 --- a/interactions/lorem-ipsum/index.html +++ /dev/null @@ -1,69 +0,0 @@ - - - - - - - -Lorem Ipsum | Formal Methods Tools - - - - - - - - - - - - - - - - - - - - - - - - -
-

Formal Methods Tools

- - - - -
-
- -

Lorem Ipsum

- - -

Z3 Theorem Prover

- - -
-
-

Copyright 2025. All rights reserved.

- -
- - diff --git a/interactions/lorem-ipsum/index.xml b/interactions/lorem-ipsum/index.xml deleted file mode 100644 index 7fb4355..0000000 --- a/interactions/lorem-ipsum/index.xml +++ /dev/null @@ -1,19 +0,0 @@ - - - - Lorem Ipsum on Formal Methods Tools - https://example.org/interactions/lorem-ipsum/ - Recent content in Lorem Ipsum on Formal Methods Tools - Hugo - en-us - Fri, 02 Feb 2024 04:14:54 -0800 - - - Z3 Theorem Prover - https://example.org/tools/z3/ - Fri, 02 Feb 2024 04:14:54 -0800 - https://example.org/tools/z3/ - <p>desc</p> - - - diff --git a/interactions/ocaml-api/index.html b/interactions/ocaml-api/index.html new file mode 100644 index 0000000..cde6cd2 --- /dev/null +++ b/interactions/ocaml-api/index.html @@ -0,0 +1,69 @@ + + + + + + + +OCaml API | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + +
+

Formal Methods Tools

+ + + + +
+
+ +

OCaml API

+ + +

Yices 2

+ + +
+
+

Copyright 2025. All rights reserved.

+ +
+ + diff --git a/interactions/ocaml-api/index.xml b/interactions/ocaml-api/index.xml new file mode 100644 index 0000000..3a45e91 --- /dev/null +++ b/interactions/ocaml-api/index.xml @@ -0,0 +1,19 @@ + + + + OCaml API on Formal Methods Tools + http://localhost:1313/interactions/ocaml-api/ + Recent content in OCaml API on Formal Methods Tools + Hugo + en-us + Fri, 02 Feb 2024 04:14:54 -0800 + + + Yices 2 + http://localhost:1313/tools/yices/ + Fri, 02 Feb 2024 04:14:54 -0800 + http://localhost:1313/tools/yices/ + <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> + + + diff --git a/interactions/playground/index.html b/interactions/playground/index.html new file mode 100644 index 0000000..792fb59 --- /dev/null +++ b/interactions/playground/index.html @@ -0,0 +1,69 @@ + + + + + + + +Playground | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + +
+

Formal Methods Tools

+ + + + +
+
+ +

Playground

+ + +

Z3

+ + +
+
+

Copyright 2025. All rights reserved.

+ +
+ + diff --git a/interactions/playground/index.xml b/interactions/playground/index.xml new file mode 100644 index 0000000..81fa3aa --- /dev/null +++ b/interactions/playground/index.xml @@ -0,0 +1,19 @@ + + + + Playground on Formal Methods Tools + http://localhost:1313/interactions/playground/ + Recent content in Playground on Formal Methods Tools + Hugo + en-us + Fri, 02 Feb 2024 04:14:54 -0800 + + + Z3 + http://localhost:1313/tools/z3/ + Fri, 02 Feb 2024 04:14:54 -0800 + http://localhost:1313/tools/z3/ + <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> + + + diff --git a/interactions/python-api/index.html b/interactions/python-api/index.html new file mode 100644 index 0000000..3e66383 --- /dev/null +++ b/interactions/python-api/index.html @@ -0,0 +1,69 @@ + + + + + + + +Python API | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + +
+

Formal Methods Tools

+ + + + +
+
+ +

Python API

+ + +

Z3

+ + +
+
+

Copyright 2025. All rights reserved.

+ +
+ + diff --git a/interactions/python-api/index.xml b/interactions/python-api/index.xml new file mode 100644 index 0000000..bb180a6 --- /dev/null +++ b/interactions/python-api/index.xml @@ -0,0 +1,19 @@ + + + + Python API on Formal Methods Tools + http://localhost:1313/interactions/python-api/ + Recent content in Python API on Formal Methods Tools + Hugo + en-us + Fri, 02 Feb 2024 04:14:54 -0800 + + + Z3 + http://localhost:1313/tools/z3/ + Fri, 02 Feb 2024 04:14:54 -0800 + http://localhost:1313/tools/z3/ + <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> + + + diff --git a/interactions/python-bindings/index.html b/interactions/python-bindings/index.html new file mode 100644 index 0000000..8c5017a --- /dev/null +++ b/interactions/python-bindings/index.html @@ -0,0 +1,69 @@ + + + + + + + +Python Bindings | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + +
+

Formal Methods Tools

+ + + + +
+
+ +

Python Bindings

+ + +

Yices 2

+ + +
+
+

Copyright 2025. All rights reserved.

+ +
+ + diff --git a/interactions/python-bindings/index.xml b/interactions/python-bindings/index.xml new file mode 100644 index 0000000..f3afaa3 --- /dev/null +++ b/interactions/python-bindings/index.xml @@ -0,0 +1,19 @@ + + + + Python Bindings on Formal Methods Tools + http://localhost:1313/interactions/python-bindings/ + Recent content in Python Bindings on Formal Methods Tools + Hugo + en-us + Fri, 02 Feb 2024 04:14:54 -0800 + + + Yices 2 + http://localhost:1313/tools/yices/ + Fri, 02 Feb 2024 04:14:54 -0800 + http://localhost:1313/tools/yices/ + <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> + + + diff --git a/interactions/rust-bindings/index.html b/interactions/rust-bindings/index.html new file mode 100644 index 0000000..23f6bfe --- /dev/null +++ b/interactions/rust-bindings/index.html @@ -0,0 +1,69 @@ + + + + + + + +Rust Bindings | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + +
+

Formal Methods Tools

+ + + + +
+
+ +

Rust Bindings

+ + +

Z3

+ + +
+
+

Copyright 2025. All rights reserved.

+ +
+ + diff --git a/interactions/rust-bindings/index.xml b/interactions/rust-bindings/index.xml new file mode 100644 index 0000000..baf0b34 --- /dev/null +++ b/interactions/rust-bindings/index.xml @@ -0,0 +1,19 @@ + + + + Rust Bindings on Formal Methods Tools + http://localhost:1313/interactions/rust-bindings/ + Recent content in Rust Bindings on Formal Methods Tools + Hugo + en-us + Fri, 02 Feb 2024 04:14:54 -0800 + + + Z3 + http://localhost:1313/tools/z3/ + Fri, 02 Feb 2024 04:14:54 -0800 + http://localhost:1313/tools/z3/ + <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> + + + diff --git a/languages/c#/index.html b/languages/c#/index.html new file mode 100644 index 0000000..5ad8073 --- /dev/null +++ b/languages/c#/index.html @@ -0,0 +1,69 @@ + + + + + + + +C# | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + +
+

Formal Methods Tools

+ + + + +
+
+ +

C#

+ + +

Z3

+ + +
+
+

Copyright 2025. All rights reserved.

+ +
+ + diff --git a/languages/c#/index.xml b/languages/c#/index.xml new file mode 100644 index 0000000..82a46c1 --- /dev/null +++ b/languages/c#/index.xml @@ -0,0 +1,19 @@ + + + + C# on Formal Methods Tools + http://localhost:1313/languages/c%23/ + Recent content in C# on Formal Methods Tools + Hugo + en-us + Fri, 02 Feb 2024 04:14:54 -0800 + + + Z3 + http://localhost:1313/tools/z3/ + Fri, 02 Feb 2024 04:14:54 -0800 + http://localhost:1313/tools/z3/ + <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> + + + diff --git a/languages/c++/index.html b/languages/c++/index.html new file mode 100644 index 0000000..c091834 --- /dev/null +++ b/languages/c++/index.html @@ -0,0 +1,69 @@ + + + + + + + +C++ | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + +
+

Formal Methods Tools

+ + + + +
+
+ +

C++

+ + +

Z3

+ + +
+
+

Copyright 2025. All rights reserved.

+ +
+ + diff --git a/languages/c++/index.xml b/languages/c++/index.xml new file mode 100644 index 0000000..251c438 --- /dev/null +++ b/languages/c++/index.xml @@ -0,0 +1,19 @@ + + + + C++ on Formal Methods Tools + http://localhost:1313/languages/c++/ + Recent content in C++ on Formal Methods Tools + Hugo + en-us + Fri, 02 Feb 2024 04:14:54 -0800 + + + Z3 + http://localhost:1313/tools/z3/ + Fri, 02 Feb 2024 04:14:54 -0800 + http://localhost:1313/tools/z3/ + <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> + + + diff --git a/languages/c/index.html b/languages/c/index.html new file mode 100644 index 0000000..1ba497d --- /dev/null +++ b/languages/c/index.html @@ -0,0 +1,69 @@ + + + + + + + +C | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + +
+

Formal Methods Tools

+ + + + +
+
+ +

C

+ + +

Yices 2

+ + +
+
+

Copyright 2025. All rights reserved.

+ +
+ + diff --git a/languages/c/index.xml b/languages/c/index.xml new file mode 100644 index 0000000..76c9146 --- /dev/null +++ b/languages/c/index.xml @@ -0,0 +1,19 @@ + + + + C on Formal Methods Tools + http://localhost:1313/languages/c/ + Recent content in C on Formal Methods Tools + Hugo + en-us + Fri, 02 Feb 2024 04:14:54 -0800 + + + Yices 2 + http://localhost:1313/tools/yices/ + Fri, 02 Feb 2024 04:14:54 -0800 + http://localhost:1313/tools/yices/ + <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> + + + diff --git a/languages/index.html b/languages/index.html index 19a75e0..7ab0656 100644 --- a/languages/index.html +++ b/languages/index.html @@ -1,6 +1,6 @@ - + @@ -13,16 +13,16 @@ - + - + - - - - + + + + - + @@ -70,10 +70,136 @@ - Tttt + id="languages_c" + style="background:rgba(13,97,248,0.4)" + href="/languages/c"> + C + + + + + + + + + + + + + + C# + + + + + + + + + + + + + + C++ + + + + + + + + + + + + + + Java + + + + + + + + + + + + + + OCaml + + + + + + + + + + + + + + Python + + + + + + + + + + + + + + SMT-LIB + + + + + + + + + + + + + + Yices Language diff --git a/languages/index.xml b/languages/index.xml index 5bd71ac..ab4c8d2 100644 --- a/languages/index.xml +++ b/languages/index.xml @@ -2,17 +2,66 @@ Languages on Formal Methods Tools - https://example.org/languages/ + http://localhost:1313/languages/ Recent content in Languages on Formal Methods Tools Hugo en-us Fri, 02 Feb 2024 04:14:54 -0800 - + - Tttt - https://example.org/languages/tttt/ + C + http://localhost:1313/languages/c/ Fri, 02 Feb 2024 04:14:54 -0800 - https://example.org/languages/tttt/ + http://localhost:1313/languages/c/ + + + + C# + http://localhost:1313/languages/c%23/ + Fri, 02 Feb 2024 04:14:54 -0800 + http://localhost:1313/languages/c%23/ + + + + C++ + http://localhost:1313/languages/c++/ + Fri, 02 Feb 2024 04:14:54 -0800 + http://localhost:1313/languages/c++/ + + + + Java + http://localhost:1313/languages/java/ + Fri, 02 Feb 2024 04:14:54 -0800 + http://localhost:1313/languages/java/ + + + + OCaml + http://localhost:1313/languages/ocaml/ + Fri, 02 Feb 2024 04:14:54 -0800 + http://localhost:1313/languages/ocaml/ + + + + Python + http://localhost:1313/languages/python/ + Fri, 02 Feb 2024 04:14:54 -0800 + http://localhost:1313/languages/python/ + + + + SMT-LIB + http://localhost:1313/languages/smt-lib/ + Fri, 02 Feb 2024 04:14:54 -0800 + http://localhost:1313/languages/smt-lib/ + + + + Yices Language + http://localhost:1313/languages/yices-language/ + Fri, 02 Feb 2024 04:14:54 -0800 + http://localhost:1313/languages/yices-language/ diff --git a/languages/java/index.html b/languages/java/index.html new file mode 100644 index 0000000..6d8f347 --- /dev/null +++ b/languages/java/index.html @@ -0,0 +1,69 @@ + + + + + + + +Java | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + +
+

Formal Methods Tools

+ + + + +
+
+ +

Java

+ + +

Z3

+ + +
+
+

Copyright 2025. All rights reserved.

+ +
+ + diff --git a/languages/java/index.xml b/languages/java/index.xml new file mode 100644 index 0000000..da5ab95 --- /dev/null +++ b/languages/java/index.xml @@ -0,0 +1,19 @@ + + + + Java on Formal Methods Tools + http://localhost:1313/languages/java/ + Recent content in Java on Formal Methods Tools + Hugo + en-us + Fri, 02 Feb 2024 04:14:54 -0800 + + + Z3 + http://localhost:1313/tools/z3/ + Fri, 02 Feb 2024 04:14:54 -0800 + http://localhost:1313/tools/z3/ + <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> + + + diff --git a/languages/ocaml/index.html b/languages/ocaml/index.html new file mode 100644 index 0000000..e5edb2a --- /dev/null +++ b/languages/ocaml/index.html @@ -0,0 +1,69 @@ + + + + + + + +OCaml | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + +
+

Formal Methods Tools

+ + + + +
+
+ +

OCaml

+ + +

Yices 2

+ + +
+
+

Copyright 2025. All rights reserved.

+ +
+ + diff --git a/languages/ocaml/index.xml b/languages/ocaml/index.xml new file mode 100644 index 0000000..cf4e164 --- /dev/null +++ b/languages/ocaml/index.xml @@ -0,0 +1,19 @@ + + + + OCaml on Formal Methods Tools + http://localhost:1313/languages/ocaml/ + Recent content in OCaml on Formal Methods Tools + Hugo + en-us + Fri, 02 Feb 2024 04:14:54 -0800 + + + Yices 2 + http://localhost:1313/tools/yices/ + Fri, 02 Feb 2024 04:14:54 -0800 + http://localhost:1313/tools/yices/ + <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> + + + diff --git a/languages/python/index.html b/languages/python/index.html new file mode 100644 index 0000000..2dd29a9 --- /dev/null +++ b/languages/python/index.html @@ -0,0 +1,71 @@ + + + + + + + +Python | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + +
+

Formal Methods Tools

+ + + + +
+
+ +

Python

+ + +

Yices 2

+ +

Z3

+ + +
+
+

Copyright 2025. All rights reserved.

+ +
+ + diff --git a/languages/python/index.xml b/languages/python/index.xml new file mode 100644 index 0000000..e24fd5f --- /dev/null +++ b/languages/python/index.xml @@ -0,0 +1,26 @@ + + + + Python on Formal Methods Tools + http://localhost:1313/languages/python/ + Recent content in Python on Formal Methods Tools + Hugo + en-us + Fri, 02 Feb 2024 04:14:54 -0800 + + + Yices 2 + http://localhost:1313/tools/yices/ + Fri, 02 Feb 2024 04:14:54 -0800 + http://localhost:1313/tools/yices/ + <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> + + + Z3 + http://localhost:1313/tools/z3/ + Fri, 02 Feb 2024 04:14:54 -0800 + http://localhost:1313/tools/z3/ + <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> + + + diff --git a/languages/smt-lib/index.html b/languages/smt-lib/index.html new file mode 100644 index 0000000..d324528 --- /dev/null +++ b/languages/smt-lib/index.html @@ -0,0 +1,71 @@ + + + + + + + +SMT-LIB | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + +
+

Formal Methods Tools

+ + + + +
+
+ +

SMT-LIB

+ + +

Yices 2

+ +

Z3

+ + +
+
+

Copyright 2025. All rights reserved.

+ +
+ + diff --git a/languages/smt-lib/index.xml b/languages/smt-lib/index.xml new file mode 100644 index 0000000..616d2fe --- /dev/null +++ b/languages/smt-lib/index.xml @@ -0,0 +1,26 @@ + + + + SMT-LIB on Formal Methods Tools + http://localhost:1313/languages/smt-lib/ + Recent content in SMT-LIB on Formal Methods Tools + Hugo + en-us + Fri, 02 Feb 2024 04:14:54 -0800 + + + Yices 2 + http://localhost:1313/tools/yices/ + Fri, 02 Feb 2024 04:14:54 -0800 + http://localhost:1313/tools/yices/ + <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> + + + Z3 + http://localhost:1313/tools/z3/ + Fri, 02 Feb 2024 04:14:54 -0800 + http://localhost:1313/tools/z3/ + <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> + + + diff --git a/languages/tttt/index.html b/languages/tttt/index.html deleted file mode 100644 index ec4ade0..0000000 --- a/languages/tttt/index.html +++ /dev/null @@ -1,69 +0,0 @@ - - - - - - - -Tttt | Formal Methods Tools - - - - - - - - - - - - - - - - - - - - - - - - -
-

Formal Methods Tools

- - - - -
-
- -

Tttt

- - -

Z3 Theorem Prover

- - -
-
-

Copyright 2025. All rights reserved.

- -
- - diff --git a/languages/tttt/index.xml b/languages/tttt/index.xml deleted file mode 100644 index ab8beee..0000000 --- a/languages/tttt/index.xml +++ /dev/null @@ -1,19 +0,0 @@ - - - - Tttt on Formal Methods Tools - https://example.org/languages/tttt/ - Recent content in Tttt on Formal Methods Tools - Hugo - en-us - Fri, 02 Feb 2024 04:14:54 -0800 - - - Z3 Theorem Prover - https://example.org/tools/z3/ - Fri, 02 Feb 2024 04:14:54 -0800 - https://example.org/tools/z3/ - <p>desc</p> - - - diff --git a/languages/yices-language/index.html b/languages/yices-language/index.html new file mode 100644 index 0000000..41bd731 --- /dev/null +++ b/languages/yices-language/index.html @@ -0,0 +1,69 @@ + + + + + + + +Yices Language | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + +
+

Formal Methods Tools

+ + + + +
+
+ +

Yices Language

+ + +

Yices 2

+ + +
+
+

Copyright 2025. All rights reserved.

+ +
+ + diff --git a/languages/yices-language/index.xml b/languages/yices-language/index.xml new file mode 100644 index 0000000..4816f81 --- /dev/null +++ b/languages/yices-language/index.xml @@ -0,0 +1,19 @@ + + + + Yices Language on Formal Methods Tools + http://localhost:1313/languages/yices-language/ + Recent content in Yices Language on Formal Methods Tools + Hugo + en-us + Fri, 02 Feb 2024 04:14:54 -0800 + + + Yices 2 + http://localhost:1313/tools/yices/ + Fri, 02 Feb 2024 04:14:54 -0800 + http://localhost:1313/tools/yices/ + <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> + + + diff --git a/purposes/analysis-tools/index.html b/purposes/analysis-tools/index.html new file mode 100644 index 0000000..af962de --- /dev/null +++ b/purposes/analysis-tools/index.html @@ -0,0 +1,71 @@ + + + + + + + +Analysis Tools | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + +
+

Formal Methods Tools

+ + + + +
+
+ +

Analysis Tools

+ + +

Yices 2

+ +

Z3

+ + +
+
+

Copyright 2025. All rights reserved.

+ +
+ + diff --git a/purposes/analysis-tools/index.xml b/purposes/analysis-tools/index.xml new file mode 100644 index 0000000..32fa4c8 --- /dev/null +++ b/purposes/analysis-tools/index.xml @@ -0,0 +1,26 @@ + + + + Analysis Tools on Formal Methods Tools + http://localhost:1313/purposes/analysis-tools/ + Recent content in Analysis Tools on Formal Methods Tools + Hugo + en-us + Fri, 02 Feb 2024 04:14:54 -0800 + + + Yices 2 + http://localhost:1313/tools/yices/ + Fri, 02 Feb 2024 04:14:54 -0800 + http://localhost:1313/tools/yices/ + <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> + + + Z3 + http://localhost:1313/tools/z3/ + Fri, 02 Feb 2024 04:14:54 -0800 + http://localhost:1313/tools/z3/ + <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> + + + diff --git a/purposes/index.html b/purposes/index.html index 96488b5..9415e10 100644 --- a/purposes/index.html +++ b/purposes/index.html @@ -1,6 +1,6 @@ - + @@ -13,16 +13,16 @@ - + - + - - - - + + + + - + @@ -70,10 +70,28 @@ - Test + id="purposes_analysis-tools" + style="background:rgba(26,123,112,0.4)" + href="/purposes/analysis-tools"> + Analysis Tools + + + + + + + + + + + + + + Verification Tools diff --git a/purposes/index.xml b/purposes/index.xml index 47552d6..a083457 100644 --- a/purposes/index.xml +++ b/purposes/index.xml @@ -2,17 +2,24 @@ Purposes on Formal Methods Tools - https://example.org/purposes/ + http://localhost:1313/purposes/ Recent content in Purposes on Formal Methods Tools Hugo en-us Fri, 02 Feb 2024 04:14:54 -0800 - + - Test - https://example.org/purposes/test/ + Analysis Tools + http://localhost:1313/purposes/analysis-tools/ Fri, 02 Feb 2024 04:14:54 -0800 - https://example.org/purposes/test/ + http://localhost:1313/purposes/analysis-tools/ + + + + Verification Tools + http://localhost:1313/purposes/verification-tools/ + Fri, 02 Feb 2024 04:14:54 -0800 + http://localhost:1313/purposes/verification-tools/ diff --git a/purposes/test/index.html b/purposes/test/index.html deleted file mode 100644 index baba283..0000000 --- a/purposes/test/index.html +++ /dev/null @@ -1,69 +0,0 @@ - - - - - - - -Test | Formal Methods Tools - - - - - - - - - - - - - - - - - - - - - - - - -
-

Formal Methods Tools

- - - - -
-
- -

Test

- - -

Z3 Theorem Prover

- - -
-
-

Copyright 2025. All rights reserved.

- -
- - diff --git a/purposes/test/index.xml b/purposes/test/index.xml deleted file mode 100644 index 6382bd4..0000000 --- a/purposes/test/index.xml +++ /dev/null @@ -1,19 +0,0 @@ - - - - Test on Formal Methods Tools - https://example.org/purposes/test/ - Recent content in Test on Formal Methods Tools - Hugo - en-us - Fri, 02 Feb 2024 04:14:54 -0800 - - - Z3 Theorem Prover - https://example.org/tools/z3/ - Fri, 02 Feb 2024 04:14:54 -0800 - https://example.org/tools/z3/ - <p>desc</p> - - - diff --git a/purposes/verification-tools/index.html b/purposes/verification-tools/index.html new file mode 100644 index 0000000..f908d58 --- /dev/null +++ b/purposes/verification-tools/index.html @@ -0,0 +1,71 @@ + + + + + + + +Verification Tools | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + +
+

Formal Methods Tools

+ + + + +
+
+ +

Verification Tools

+ + +

Yices 2

+ +

Z3

+ + +
+
+

Copyright 2025. All rights reserved.

+ +
+ + diff --git a/purposes/verification-tools/index.xml b/purposes/verification-tools/index.xml new file mode 100644 index 0000000..b24521e --- /dev/null +++ b/purposes/verification-tools/index.xml @@ -0,0 +1,26 @@ + + + + Verification Tools on Formal Methods Tools + http://localhost:1313/purposes/verification-tools/ + Recent content in Verification Tools on Formal Methods Tools + Hugo + en-us + Fri, 02 Feb 2024 04:14:54 -0800 + + + Yices 2 + http://localhost:1313/tools/yices/ + Fri, 02 Feb 2024 04:14:54 -0800 + http://localhost:1313/tools/yices/ + <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> + + + Z3 + http://localhost:1313/tools/z3/ + Fri, 02 Feb 2024 04:14:54 -0800 + http://localhost:1313/tools/z3/ + <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> + + + diff --git a/sitemap.xml b/sitemap.xml index 538de4c..be95fc6 100644 --- a/sitemap.xml +++ b/sitemap.xml @@ -2,93 +2,144 @@ - https://example.org/tools/z3/ + http://localhost:1313/purposes/analysis-tools/ 2024-02-02T04:14:54-08:00 - https://example.org/techniques/aaa/ + http://localhost:1313/formalisms/arithmetic/ 2024-02-02T04:14:54-08:00 - https://example.org/interactions/araafafanpoasi/ + http://localhost:1313/formalisms/arrays/ 2024-02-02T04:14:54-08:00 - https://example.org/interactions/aranapoasi/ + http://localhost:1313/formalisms/bit-vectors/ 2024-02-02T04:14:54-08:00 - https://example.org/interactions/aranpoasadfsi/ + http://localhost:1313/languages/c/ 2024-02-02T04:14:54-08:00 - https://example.org/interactions/aranpoasai/ + http://localhost:1313/interactions/c-api/ 2024-02-02T04:14:54-08:00 - https://example.org/interactions/aranpoasasdfasfasdfasdfi/ + http://localhost:1313/languages/c%23/ 2024-02-02T04:14:54-08:00 - https://example.org/interactions/aranpoasi/ + http://localhost:1313/languages/c++/ 2024-02-02T04:14:54-08:00 - https://example.org/interactions/aranpoaswei/ + http://localhost:1313/interactions/cli/ 2024-02-02T04:14:54-08:00 - https://example.org/interactions/aranpoxasi/ + http://localhost:1313/systems/concurrent-systems/ 2024-02-02T04:14:54-08:00 - https://example.org/interactions/aranpsoasi/ + http://localhost:1313/developers/ 2024-02-02T04:14:54-08:00 - https://example.org/interactions/aransdpoasi/ + http://localhost:1313/systems/discrete-systems/ 2024-02-02T04:14:54-08:00 - https://example.org/developers/ + http://localhost:1313/domains/ 2024-02-02T04:14:54-08:00 - https://example.org/domains/ + http://localhost:1313/domains/embedded-systems/ 2024-02-02T04:14:54-08:00 - https://example.org/formalisms/ + http://localhost:1313/formalisms/first-order-logic/ 2024-02-02T04:14:54-08:00 - https://example.org/interactions/ + http://localhost:1313/formalisms/ 2024-02-02T04:14:54-08:00 - https://example.org/languages/ + http://localhost:1313/domains/hardware-verification/ 2024-02-02T04:14:54-08:00 - https://example.org/interactions/lorem-ipsum/ + http://localhost:1313/interactions/ 2024-02-02T04:14:54-08:00 - https://example.org/purposes/ + http://localhost:1313/languages/java/ 2024-02-02T04:14:54-08:00 - https://example.org/systems/ + http://localhost:1313/languages/ 2024-02-02T04:14:54-08:00 - https://example.org/techniques/ + http://localhost:1313/developers/microsoft-research/ 2024-02-02T04:14:54-08:00 - https://example.org/purposes/test/ + http://localhost:1313/techniques/model-checking/ 2024-02-02T04:14:54-08:00 - https://example.org/developers/test-dev/ + http://localhost:1313/languages/ocaml/ 2024-02-02T04:14:54-08:00 - https://example.org/tools/ + http://localhost:1313/interactions/ocaml-api/ 2024-02-02T04:14:54-08:00 - https://example.org/domains/tttt/ + http://localhost:1313/interactions/playground/ 2024-02-02T04:14:54-08:00 - https://example.org/formalisms/tttt/ + http://localhost:1313/purposes/ 2024-02-02T04:14:54-08:00 - https://example.org/languages/tttt/ + http://localhost:1313/languages/python/ 2024-02-02T04:14:54-08:00 - https://example.org/systems/tttt/ + http://localhost:1313/interactions/python-api/ 2024-02-02T04:14:54-08:00 - https://example.org/ + http://localhost:1313/interactions/python-bindings/ + 2024-02-02T04:14:54-08:00 + + http://localhost:1313/formalisms/quantifier-logic/ + 2024-02-02T04:14:54-08:00 + + http://localhost:1313/interactions/rust-bindings/ + 2024-02-02T04:14:54-08:00 + + http://localhost:1313/techniques/smt-solving/ + 2024-02-02T04:14:54-08:00 + + http://localhost:1313/formalisms/smt-lib/ + 2024-02-02T04:14:54-08:00 + + http://localhost:1313/languages/smt-lib/ + 2024-02-02T04:14:54-08:00 + + http://localhost:1313/domains/software-verification/ + 2024-02-02T04:14:54-08:00 + + http://localhost:1313/developers/sri-international/ + 2024-02-02T04:14:54-08:00 + + http://localhost:1313/systems/ + 2024-02-02T04:14:54-08:00 + + http://localhost:1313/techniques/ + 2024-02-02T04:14:54-08:00 + + http://localhost:1313/techniques/theorem-proving/ + 2024-02-02T04:14:54-08:00 + + http://localhost:1313/tools/ + 2024-02-02T04:14:54-08:00 + + http://localhost:1313/formalisms/uninterpreted-functions/ + 2024-02-02T04:14:54-08:00 + + http://localhost:1313/purposes/verification-tools/ + 2024-02-02T04:14:54-08:00 + + http://localhost:1313/tools/yices/ + 2024-02-02T04:14:54-08:00 + + http://localhost:1313/languages/yices-language/ + 2024-02-02T04:14:54-08:00 + + http://localhost:1313/tools/z3/ + 2024-02-02T04:14:54-08:00 + + http://localhost:1313/ 2023-01-01T08:00:00-07:00 - https://example.org/taxonomies/ + http://localhost:1313/taxonomies/ diff --git a/systems/concurrent-systems/index.html b/systems/concurrent-systems/index.html new file mode 100644 index 0000000..4e15c24 --- /dev/null +++ b/systems/concurrent-systems/index.html @@ -0,0 +1,71 @@ + + + + + + + +Concurrent Systems | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + +
+

Formal Methods Tools

+ + + + +
+
+ +

Concurrent Systems

+ + +

Yices 2

+ +

Z3

+ + +
+
+

Copyright 2025. All rights reserved.

+ +
+ + diff --git a/systems/concurrent-systems/index.xml b/systems/concurrent-systems/index.xml new file mode 100644 index 0000000..f60f8be --- /dev/null +++ b/systems/concurrent-systems/index.xml @@ -0,0 +1,26 @@ + + + + Concurrent Systems on Formal Methods Tools + http://localhost:1313/systems/concurrent-systems/ + Recent content in Concurrent Systems on Formal Methods Tools + Hugo + en-us + Fri, 02 Feb 2024 04:14:54 -0800 + + + Yices 2 + http://localhost:1313/tools/yices/ + Fri, 02 Feb 2024 04:14:54 -0800 + http://localhost:1313/tools/yices/ + <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> + + + Z3 + http://localhost:1313/tools/z3/ + Fri, 02 Feb 2024 04:14:54 -0800 + http://localhost:1313/tools/z3/ + <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> + + + diff --git a/systems/discrete-systems/index.html b/systems/discrete-systems/index.html new file mode 100644 index 0000000..66f3e4e --- /dev/null +++ b/systems/discrete-systems/index.html @@ -0,0 +1,71 @@ + + + + + + + +Discrete Systems | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + +
+

Formal Methods Tools

+ + + + +
+
+ +

Discrete Systems

+ + +

Yices 2

+ +

Z3

+ + +
+
+

Copyright 2025. All rights reserved.

+ +
+ + diff --git a/systems/discrete-systems/index.xml b/systems/discrete-systems/index.xml new file mode 100644 index 0000000..4779862 --- /dev/null +++ b/systems/discrete-systems/index.xml @@ -0,0 +1,26 @@ + + + + Discrete Systems on Formal Methods Tools + http://localhost:1313/systems/discrete-systems/ + Recent content in Discrete Systems on Formal Methods Tools + Hugo + en-us + Fri, 02 Feb 2024 04:14:54 -0800 + + + Yices 2 + http://localhost:1313/tools/yices/ + Fri, 02 Feb 2024 04:14:54 -0800 + http://localhost:1313/tools/yices/ + <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> + + + Z3 + http://localhost:1313/tools/z3/ + Fri, 02 Feb 2024 04:14:54 -0800 + http://localhost:1313/tools/z3/ + <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> + + + diff --git a/systems/index.html b/systems/index.html index 0d27c52..65986d0 100644 --- a/systems/index.html +++ b/systems/index.html @@ -1,6 +1,6 @@ - + @@ -13,16 +13,16 @@ - + - + - - - - + + + + - + @@ -70,10 +70,28 @@ - Tttt + id="systems_concurrent-systems" + style="background:rgba(14,80,100,0.4)" + href="/systems/concurrent-systems"> + Concurrent Systems + + + + + + + + + + + + + + Discrete Systems diff --git a/systems/index.xml b/systems/index.xml index a0db358..2ceae9f 100644 --- a/systems/index.xml +++ b/systems/index.xml @@ -2,17 +2,24 @@ Systems on Formal Methods Tools - https://example.org/systems/ + http://localhost:1313/systems/ Recent content in Systems on Formal Methods Tools Hugo en-us Fri, 02 Feb 2024 04:14:54 -0800 - + - Tttt - https://example.org/systems/tttt/ + Concurrent Systems + http://localhost:1313/systems/concurrent-systems/ Fri, 02 Feb 2024 04:14:54 -0800 - https://example.org/systems/tttt/ + http://localhost:1313/systems/concurrent-systems/ + + + + Discrete Systems + http://localhost:1313/systems/discrete-systems/ + Fri, 02 Feb 2024 04:14:54 -0800 + http://localhost:1313/systems/discrete-systems/ diff --git a/systems/tttt/index.html b/systems/tttt/index.html deleted file mode 100644 index 28566f1..0000000 --- a/systems/tttt/index.html +++ /dev/null @@ -1,69 +0,0 @@ - - - - - - - -Tttt | Formal Methods Tools - - - - - - - - - - - - - - - - - - - - - - - - -
-

Formal Methods Tools

- - - - -
-
- -

Tttt

- - -

Z3 Theorem Prover

- - -
-
-

Copyright 2025. All rights reserved.

- -
- - diff --git a/systems/tttt/index.xml b/systems/tttt/index.xml deleted file mode 100644 index 3591f9d..0000000 --- a/systems/tttt/index.xml +++ /dev/null @@ -1,19 +0,0 @@ - - - - Tttt on Formal Methods Tools - https://example.org/systems/tttt/ - Recent content in Tttt on Formal Methods Tools - Hugo - en-us - Fri, 02 Feb 2024 04:14:54 -0800 - - - Z3 Theorem Prover - https://example.org/tools/z3/ - Fri, 02 Feb 2024 04:14:54 -0800 - https://example.org/tools/z3/ - <p>desc</p> - - - diff --git a/taxonomies/index.html b/taxonomies/index.html index 06e4eda..e3030d9 100644 --- a/taxonomies/index.html +++ b/taxonomies/index.html @@ -1,6 +1,6 @@ - + @@ -13,16 +13,16 @@ - + - + - - - - + + + + - + @@ -83,10 +83,27 @@ - test dev + id="developers_microsoft-research" + style="background:rgba(62,86,189,0.4)" + href="/developers/microsoft-research"> + microsoft research + + + + + + + + + + + + + sri international @@ -115,10 +132,44 @@ - tttt + id="domains_embedded-systems" + style="background:rgba(23,145,141,0.4)" + href="/domains/embedded-systems"> + embedded systems + + + + + + + + + + + + + hardware verification + + + + + + + + + + + + + software verification @@ -147,10 +198,112 @@ - tttt + id="formalisms_arithmetic" + style="background:rgba(38,232,22,0.4)" + href="/formalisms/arithmetic"> + arithmetic + + + + + + + + + + + + + arrays + + + + + + + + + + + + + bit-vectors + + + + + + + + + + + + + first-order logic + + + + + + + + + + + + + quantifier logic + + + + + + + + + + + + + smt-lib + + + + + + + + + + + + + uninterpreted functions @@ -179,10 +332,10 @@ - araafafanpoasi + id="interactions_c-api" + style="background:rgba(238,156,248,0.4)" + href="/interactions/c-api"> + c api @@ -196,10 +349,10 @@ - aranapoasi + id="interactions_cli" + style="background:rgba(8,152,178,0.4)" + href="/interactions/cli"> + cli @@ -213,10 +366,10 @@ - aranpoasadfsi + id="interactions_ocaml-api" + style="background:rgba(69,109,89,0.4)" + href="/interactions/ocaml-api"> + ocaml api @@ -230,10 +383,10 @@ - aranpoasai + id="interactions_playground" + style="background:rgba(150,199,11,0.4)" + href="/interactions/playground"> + playground @@ -247,10 +400,10 @@ - aranpoasasdfasfasdfasdfi + id="interactions_python-api" + style="background:rgba(59,100,239,0.4)" + href="/interactions/python-api"> + python api @@ -264,10 +417,10 @@ - aranpoasi + id="interactions_python-bindings" + style="background:rgba(36,110,8,0.4)" + href="/interactions/python-bindings"> + python bindings @@ -281,78 +434,10 @@ - aranpoaswei - - - - - - - - - - - - - aranpoxasi - - - - - - - - - - - - - aranpsoasi - - - - - - - - - - - - - aransdpoasi - - - - - - - - - - - - - lorem ipsum + id="interactions_rust-bindings" + style="background:rgba(216,195,118,0.4)" + href="/interactions/rust-bindings"> + rust bindings @@ -381,10 +466,129 @@ - tttt + id="languages_c" + style="background:rgba(74,138,8,0.4)" + href="/languages/c"> + c + + + + + + + + + + + + + c# + + + + + + + + + + + + + c++ + + + + + + + + + + + + + java + + + + + + + + + + + + + ocaml + + + + + + + + + + + + + python + + + + + + + + + + + + + smt-lib + + + + + + + + + + + + + yices language @@ -413,10 +617,27 @@ - test + id="purposes_analysis-tools" + style="background:rgba(87,35,209,0.4)" + href="/purposes/analysis-tools"> + analysis tools + + + + + + + + + + + + + verification tools @@ -445,10 +666,27 @@ - tttt + id="systems_concurrent-systems" + style="background:rgba(9,52,204,0.4)" + href="/systems/concurrent-systems"> + concurrent systems + + + + + + + + + + + + + discrete systems @@ -477,10 +715,44 @@ - aaa + id="techniques_model-checking" + style="background:rgba(142,80,237,0.4)" + href="/techniques/model-checking"> + model checking + + + + + + + + + + + + + smt solving + + + + + + + + + + + + + theorem proving diff --git a/taxonomies/index.xml b/taxonomies/index.xml index 19d5fe8..02bdae5 100644 --- a/taxonomies/index.xml +++ b/taxonomies/index.xml @@ -2,10 +2,10 @@ All Taxonomy Data on Formal Methods Tools - https://example.org/taxonomies/ + http://localhost:1313/taxonomies/ Recent content in All Taxonomy Data on Formal Methods Tools Hugo en-us - + diff --git a/techniques/aaa/index.html b/techniques/aaa/index.html deleted file mode 100644 index 5fb748a..0000000 --- a/techniques/aaa/index.html +++ /dev/null @@ -1,69 +0,0 @@ - - - - - - - -Aaa | Formal Methods Tools - - - - - - - - - - - - - - - - - - - - - - - - -
-

Formal Methods Tools

- - - - -
-
- -

Aaa

- - -

Z3 Theorem Prover

- - -
-
-

Copyright 2025. All rights reserved.

- -
- - diff --git a/techniques/aaa/index.xml b/techniques/aaa/index.xml deleted file mode 100644 index 938e122..0000000 --- a/techniques/aaa/index.xml +++ /dev/null @@ -1,19 +0,0 @@ - - - - Aaa on Formal Methods Tools - https://example.org/techniques/aaa/ - Recent content in Aaa on Formal Methods Tools - Hugo - en-us - Fri, 02 Feb 2024 04:14:54 -0800 - - - Z3 Theorem Prover - https://example.org/tools/z3/ - Fri, 02 Feb 2024 04:14:54 -0800 - https://example.org/tools/z3/ - <p>desc</p> - - - diff --git a/techniques/index.html b/techniques/index.html index 29b7aa5..1bc81b1 100644 --- a/techniques/index.html +++ b/techniques/index.html @@ -1,6 +1,6 @@ - + @@ -13,16 +13,16 @@ - + - + - - - - + + + + - + @@ -70,10 +70,46 @@ - Aaa + id="techniques_model-checking" + style="background:rgba(125,56,99,0.4)" + href="/techniques/model-checking"> + Model Checking + + + + + + + + + + + + + + SMT Solving + + + + + + + + + + + + + + Theorem Proving diff --git a/techniques/index.xml b/techniques/index.xml index 7712681..1ed1812 100644 --- a/techniques/index.xml +++ b/techniques/index.xml @@ -2,17 +2,31 @@ Techniques on Formal Methods Tools - https://example.org/techniques/ + http://localhost:1313/techniques/ Recent content in Techniques on Formal Methods Tools Hugo en-us Fri, 02 Feb 2024 04:14:54 -0800 - + - Aaa - https://example.org/techniques/aaa/ + Model Checking + http://localhost:1313/techniques/model-checking/ Fri, 02 Feb 2024 04:14:54 -0800 - https://example.org/techniques/aaa/ + http://localhost:1313/techniques/model-checking/ + + + + SMT Solving + http://localhost:1313/techniques/smt-solving/ + Fri, 02 Feb 2024 04:14:54 -0800 + http://localhost:1313/techniques/smt-solving/ + + + + Theorem Proving + http://localhost:1313/techniques/theorem-proving/ + Fri, 02 Feb 2024 04:14:54 -0800 + http://localhost:1313/techniques/theorem-proving/ diff --git a/techniques/model-checking/index.html b/techniques/model-checking/index.html new file mode 100644 index 0000000..753681f --- /dev/null +++ b/techniques/model-checking/index.html @@ -0,0 +1,71 @@ + + + + + + + +Model Checking | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + +
+

Formal Methods Tools

+ + + + +
+
+ +

Model Checking

+ + +

Yices 2

+ +

Z3

+ + +
+
+

Copyright 2025. All rights reserved.

+ +
+ + diff --git a/techniques/model-checking/index.xml b/techniques/model-checking/index.xml new file mode 100644 index 0000000..ad16e3a --- /dev/null +++ b/techniques/model-checking/index.xml @@ -0,0 +1,26 @@ + + + + Model Checking on Formal Methods Tools + http://localhost:1313/techniques/model-checking/ + Recent content in Model Checking on Formal Methods Tools + Hugo + en-us + Fri, 02 Feb 2024 04:14:54 -0800 + + + Yices 2 + http://localhost:1313/tools/yices/ + Fri, 02 Feb 2024 04:14:54 -0800 + http://localhost:1313/tools/yices/ + <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> + + + Z3 + http://localhost:1313/tools/z3/ + Fri, 02 Feb 2024 04:14:54 -0800 + http://localhost:1313/tools/z3/ + <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> + + + diff --git a/techniques/smt-solving/index.html b/techniques/smt-solving/index.html new file mode 100644 index 0000000..4a4f41a --- /dev/null +++ b/techniques/smt-solving/index.html @@ -0,0 +1,71 @@ + + + + + + + +SMT Solving | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + +
+

Formal Methods Tools

+ + + + +
+
+ +

SMT Solving

+ + +

Yices 2

+ +

Z3

+ + +
+
+

Copyright 2025. All rights reserved.

+ +
+ + diff --git a/techniques/smt-solving/index.xml b/techniques/smt-solving/index.xml new file mode 100644 index 0000000..b205f2e --- /dev/null +++ b/techniques/smt-solving/index.xml @@ -0,0 +1,26 @@ + + + + SMT Solving on Formal Methods Tools + http://localhost:1313/techniques/smt-solving/ + Recent content in SMT Solving on Formal Methods Tools + Hugo + en-us + Fri, 02 Feb 2024 04:14:54 -0800 + + + Yices 2 + http://localhost:1313/tools/yices/ + Fri, 02 Feb 2024 04:14:54 -0800 + http://localhost:1313/tools/yices/ + <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> + + + Z3 + http://localhost:1313/tools/z3/ + Fri, 02 Feb 2024 04:14:54 -0800 + http://localhost:1313/tools/z3/ + <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> + + + diff --git a/techniques/theorem-proving/index.html b/techniques/theorem-proving/index.html new file mode 100644 index 0000000..2557d5d --- /dev/null +++ b/techniques/theorem-proving/index.html @@ -0,0 +1,71 @@ + + + + + + + +Theorem Proving | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + +
+

Formal Methods Tools

+ + + + +
+
+ +

Theorem Proving

+ + +

Yices 2

+ +

Z3

+ + +
+
+

Copyright 2025. All rights reserved.

+ +
+ + diff --git a/techniques/theorem-proving/index.xml b/techniques/theorem-proving/index.xml new file mode 100644 index 0000000..16bf111 --- /dev/null +++ b/techniques/theorem-proving/index.xml @@ -0,0 +1,26 @@ + + + + Theorem Proving on Formal Methods Tools + http://localhost:1313/techniques/theorem-proving/ + Recent content in Theorem Proving on Formal Methods Tools + Hugo + en-us + Fri, 02 Feb 2024 04:14:54 -0800 + + + Yices 2 + http://localhost:1313/tools/yices/ + Fri, 02 Feb 2024 04:14:54 -0800 + http://localhost:1313/tools/yices/ + <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> + + + Z3 + http://localhost:1313/tools/z3/ + Fri, 02 Feb 2024 04:14:54 -0800 + http://localhost:1313/tools/z3/ + <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> + + + diff --git a/tools/index.html b/tools/index.html index 981de3e..7418958 100644 --- a/tools/index.html +++ b/tools/index.html @@ -1,6 +1,6 @@ - + @@ -13,16 +13,16 @@ - + - + - - - - + + + + - + @@ -59,9 +59,13 @@
-

Z3 Theorem Prover

-

desc

-

+

Yices 2

+

Yices is a high-performance SMT solver and theorem prover developed by SRI International. It is …

+
+ +
+

Z3

+

Z3 is a high-performance SMT solver and theorem prover developed by Microsoft Research. It is widely …

diff --git a/tools/index.xml b/tools/index.xml index 557e8a3..80f923f 100644 --- a/tools/index.xml +++ b/tools/index.xml @@ -2,18 +2,25 @@ Tools on Formal Methods Tools - https://example.org/tools/ + http://localhost:1313/tools/ Recent content in Tools on Formal Methods Tools Hugo en-us Fri, 02 Feb 2024 04:14:54 -0800 - + - Z3 Theorem Prover - https://example.org/tools/z3/ + Yices 2 + http://localhost:1313/tools/yices/ Fri, 02 Feb 2024 04:14:54 -0800 - https://example.org/tools/z3/ - <p>desc</p> + http://localhost:1313/tools/yices/ + <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> + + + Z3 + http://localhost:1313/tools/z3/ + Fri, 02 Feb 2024 04:14:54 -0800 + http://localhost:1313/tools/z3/ + <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> diff --git a/tools/yices/index.html b/tools/yices/index.html new file mode 100644 index 0000000..e277abc --- /dev/null +++ b/tools/yices/index.html @@ -0,0 +1,740 @@ + + + + + + + +Yices 2 | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + +
+

Formal Methods Tools

+ + + + +
+
+ + +
+

Yices 2

+ + + + Updated + +
+ + + + + +
+

At a Glance

+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
+ + Developers + + + + + + + + + + + + + SRI International + + + +
+ + Domains + + + + + + + + + + + + + Software Verification + + + + + + + + + + + + + Hardware Verification + + + + + + + + + + + + + Embedded Systems + + + +
+ + Formalisms + + + + + + + + + + + + + first-order logic + + + + + + + + + + + + + SMT-LIB + + + + + + + + + + + + + quantifier logic + + + + + + + + + + + + + bit-vectors + + + + + + + + + + + + + arrays + + + + + + + + + + + + + uninterpreted functions + + + + + + + + + + + + + arithmetic + + + +
+ + Interactions + + + + + + + + + + + + + CLI + + + + + + + + + + + + + C API + + + + + + + + + + + + + OCaml API + + + + + + + + + + + + + Python Bindings + + + +
+ + Languages + + + + + + + + + + + + + SMT-LIB + + + + + + + + + + + + + Yices language + + + + + + + + + + + + + C + + + + + + + + + + + + + OCaml + + + + + + + + + + + + + Python + + + +
+ + Purposes + + + + + + + + + + + + + Verification Tools + + + + + + + + + + + + + Analysis Tools + + + +
+ + Systems + + + + + + + + + + + + + Discrete Systems + + + + + + + + + + + + + Concurrent Systems + + + +
+ + Techniques + + + + + + + + + + + + + Theorem Proving + + + + + + + + + + + + + SMT Solving + + + + + + + + + + + + + Model Checking + + + +
+
+ +
+

Description

+

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.

+

Features

+
    +
  • SMT Solver: Supports a wide range of theories and quantifiers.
    • +
  • Multi-language APIs: C, OCaml, Python, and more.
    • +
  • Cross-platform: Available on Windows, Linux, and macOS.
    • +
  • Active development: Open source and maintained by SRI International.
    • +
+ +
+ + +
+

Publications

+
    + + + + + + + + + +
  • + Yices 2.2 + + + (July 2014) + + + by Dutertre, Bruno + | Appears in Computer-Aided Verification + (737-744) + + | Volume 8559 + | Published by Springer + +
    • + + + + + + + +
+
+ + + +
+
+

Copyright 2025. All rights reserved.

+ +
+ + diff --git a/tools/z3/index.html b/tools/z3/index.html index 4253502..88bbd42 100644 --- a/tools/z3/index.html +++ b/tools/z3/index.html @@ -1,28 +1,28 @@ - + -Z3 Theorem Prover | Formal Methods Tools +Z3 | Formal Methods Tools - - - + + + - + - - - - + + + + - + @@ -56,7 +56,7 @@
-

Z3 Theorem Prover

+

Z3

@@ -70,11 +70,15 @@ @@ -87,14 +91,16 @@ - - - + + Developers - + @@ -107,10 +113,10 @@ - test dev + id="developers_microsoft-research" + style="background:rgba(38,15,27,0.4)" + href="/developers/microsoft-research"> + Microsoft Research @@ -118,15 +124,16 @@ - - - - + + Domains - + @@ -139,10 +146,44 @@ - tttt + id="domains_software-verification" + style="background:rgba(127,54,56,0.4)" + href="/domains/software-verification"> + Software Verification + + + + + + + + + + + + + Hardware Verification + + + + + + + + + + + + + Embedded Systems @@ -150,15 +191,16 @@ - - - - + + Formalisms - + @@ -171,10 +213,112 @@ - tttt + id="formalisms_first-order-logic" + style="background:rgba(184,51,102,0.4)" + href="/formalisms/first-order-logic"> + first-order logic + + + + + + + + + + + + + SMT-LIB + + + + + + + + + + + + + quantifier logic + + + + + + + + + + + + + bit-vectors + + + + + + + + + + + + + arrays + + + + + + + + + + + + + uninterpreted functions + + + + + + + + + + + + + arithmetic @@ -182,15 +326,16 @@ - - - - + + Interactions - + @@ -203,10 +348,10 @@ - araafafanpoasi + id="interactions_cli" + style="background:rgba(145,175,87,0.4)" + href="/interactions/cli"> + CLI @@ -220,10 +365,10 @@ - aranapoasi + id="interactions_python-api" + style="background:rgba(2,212,135,0.4)" + href="/interactions/python-api"> + Python API @@ -237,10 +382,10 @@ - aranpoasadfsi + id="interactions_rust-bindings" + style="background:rgba(124,204,243,0.4)" + href="/interactions/rust-bindings"> + Rust Bindings @@ -254,129 +399,10 @@ - aranpoasai - - - - - - - - - - - - - aranpoasasdfasfasdfasdfi - - - - - - - - - - - - - aranpoasi - - - - - - - - - - - - - aranpoaswei - - - - - - - - - - - - - aranpoxasi - - - - - - - - - - - - - aranpsoasi - - - - - - - - - - - - - aransdpoasi - - - - - - - - - - - - - lorem ipsum + id="interactions_playground" + style="background:rgba(150,199,11,0.4)" + href="/interactions/playground"> + playground @@ -384,15 +410,16 @@ - - - - + + Languages - + @@ -405,10 +432,78 @@ - tttt + id="languages_smt-lib" + style="background:rgba(62,225,228,0.4)" + href="/languages/smt-lib"> + SMT-LIB + + + + + + + + + + + + + Python + + + + + + + + + + + + + C++ + + + + + + + + + + + + + Java + + + + + + + + + + + + + C# @@ -416,15 +511,16 @@ - - - - + + Purposes - + @@ -437,10 +533,27 @@ - test + id="purposes_verification-tools" + style="background:rgba(229,94,239,0.4)" + href="/purposes/verification-tools"> + Verification Tools + + + + + + + + + + + + + Analysis Tools @@ -448,15 +561,16 @@ - - - - + + Systems - + @@ -469,10 +583,27 @@ - tttt + id="systems_discrete-systems" + style="background:rgba(151,241,175,0.4)" + href="/systems/discrete-systems"> + Discrete Systems + + + + + + + + + + + + + Concurrent Systems @@ -480,15 +611,16 @@ - - - - + + Techniques - + @@ -501,10 +633,44 @@ - aaa + id="techniques_theorem-proving" + style="background:rgba(162,224,131,0.4)" + href="/techniques/theorem-proving"> + Theorem Proving + + + + + + + + + + + + + SMT Solving + + + + + + + + + + + + + Model Checking @@ -518,32 +684,54 @@

Description

-

desc

+

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.

+

Features

+
    +
  • SMT Solver: Supports a wide range of theories and quantifiers.
    • +
  • Multi-language APIs: Python, C++, Java, .NET, and more.
    • +
  • Cross-platform: Available on Windows, Linux, and macOS.
    • +
  • Active development: Open source and maintained by Microsoft Research.
    • +
  • Web Playground: Try Z3 online at Rise4Fun.
    • +
-
+

Publications

    + + + + + + + + + +
  • - 2023: - Cycle and Commute: Rare-Event Probability Verification for Chemical Reaction Networks -
    by Taylor, Landon | Israelsen, Bryant | Zhang, Zhen -
    Appears in Formal Methods in Computer-Aided Design + Z3: An Efficient SMT Solver - (284--293) -
    DOI: 10.34727/2023/isbn.978-3-85448-060-0_37 + (March 2008) + + + by de Moura, Leonardo et. al. + | Appears in TACAS + + + + | Published by Springer, Berlin, Heidelberg +
    10.1007/978-3-540-78800-3_24 +
    • - -