_config.yml

repository: 'testsmt/testsmt.github.io'
url: "https://testsmt.github.io"

markdown: kramdown
remote_theme: "mmistakes/minimal-mistakes@4.24.0"
plugins:
  - jekyll-redirect-from # see https://docs.github.com/en/enterprise/2.13/user/articles/redirects-on-github-pages
  - jekyll-include-cache # required by the minimal-mistakes theme

title: Project Yin-Yang for SMT Solver Testing # Can we find a better name?
url: "testsmt.github.io"


# Make stuff in _conferences accessible from /
collections:
  conferences:
    output: true
    permalink: /:path

# Apply the default layout to all files (= empty path)
defaults:
  - scope:
      path: ""
    values:
      layout: "single"
      classes: "wide"

logo: "./img/tool_logo.png"
teaser:  "./img/tool_logo.png"


twitter:
  username: "testsmtsolvers "

footer:
  links:
    - label: "Twitter"
      icon: "fab fa-fw fa-twitter-square"
      url: "https://twitter.com/mmistakes"
    - label: "GitHub"
      icon: "fab fa-fw fa-github"
      url: "https://github.com/mmistakes"
    - label: "Instagram"
      icon: "fab fa-fw fa-instagram"
      url: "https://instagram.com/mmistakes"

sidebar:
  nav: "docs"

locale                   : "en-US"
title                    : "Project Yin-Yang for SMT Solver Testing"
title_separator          : "-"
subtitle                 : # site tagline that appears below site title in masthead
description              : "Satisfiability Modulo Theory (SMT) solvers are foundational tools for many subareas of computer science, including formal verification, programming languages, and software engineering. Their reliability and robustness are crucial, especially for the safety-critical domains. However, effectively validating SMT solvers has been a longstanding challenge. The goal of Project Yin-Yang is to develop novel, effective, practical methods and techniques to help make SMT solvers more reliable, powerful, and usable. Our tools have demonstrated their remarkable effectiveness by having already found 1,500+ bugs in Z3 and CVC4/5, the two state-of-the-art SMT solvers."