From 51a0ce1565f6aea8f248d98f091ee7796195857d Mon Sep 17 00:00:00 2001 From: Landon Taylor Date: Tue, 10 Jun 2025 14:13:14 -0600 Subject: [PATCH] add tools --- opensmt.yaml | 0 parafrost.yaml | 15 +++++++++++++++ q3b.yaml | 13 +++++++++++++ smt-rat.yaml | 13 +++++++++++++ smtinterpol.yaml | 9 +++++++++ stp.yaml | 24 ++++++++++++++++++++++++ template.yaml | 12 ++++++++++++ z3.yaml | 2 +- 8 files changed, 87 insertions(+), 1 deletion(-) create mode 100644 opensmt.yaml create mode 100644 parafrost.yaml create mode 100644 q3b.yaml create mode 100644 smt-rat.yaml create mode 100644 smtinterpol.yaml create mode 100644 stp.yaml create mode 100644 template.yaml diff --git a/opensmt.yaml b/opensmt.yaml new file mode 100644 index 0000000..e69de29 diff --git a/parafrost.yaml b/parafrost.yaml new file mode 100644 index 0000000..3bca5dd --- /dev/null +++ b/parafrost.yaml @@ -0,0 +1,15 @@ +- key: Osama2024 + title: Certified SAT solving with GPU accelerated inprocessing + author: + - Osama, Muhammad + - Wijs, Anton + - Biere, Armin + year: 2024 + # journal: x + booktitle: FMSD 2024 + volume: 62 + pages: 79-118 + publisher: Springer + doi: 10.1007/s10703-023-00432-z + # url: x + \ No newline at end of file diff --git a/q3b.yaml b/q3b.yaml new file mode 100644 index 0000000..1dd6958 --- /dev/null +++ b/q3b.yaml @@ -0,0 +1,13 @@ +- key: Jonas2016 + title: Solving Quantified Bit-Vector Formulas Using Binary Decision Diagrams + author: + - Jonáš, Martin + - Strejček, Jan + year: 2016 + # journal: x + booktitle: SAT 2016 + # volume: 1 + pages: 267-283 + publisher: Springer + doi: 10.1007/978-3-319-40970-2_17 + # url: x \ No newline at end of file diff --git a/smt-rat.yaml b/smt-rat.yaml new file mode 100644 index 0000000..e1e0511 --- /dev/null +++ b/smt-rat.yaml @@ -0,0 +1,13 @@ +- key: Corzilius2015 + title: "SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving" + author: + - Corzilius, Florian + - Kremer, Gereon + - Junges, Sebastian + - Schupp, Stefan + - 'Ábrahám, Erika' + year: 2015 + booktitle: "SAT 2015" + pages: 360-368 + publisher: Springer + doi: 10.1007/978-3-319-24318-4_26 \ No newline at end of file diff --git a/smtinterpol.yaml b/smtinterpol.yaml new file mode 100644 index 0000000..f0ecfc0 --- /dev/null +++ b/smtinterpol.yaml @@ -0,0 +1,9 @@ +- key: Henkel2021 + title: Proof Tree Preserving Sequence Interpolation of Quantified Formulas in the Theory of Equality + author: + - Henkel, Elisabeth + - Hoenicke, Jochen + - Schindler, Tanja + year: 2021 + booktitle: SMT 2021 + url: "https://ceur-ws.org/Vol-2908/short12.pdf" diff --git a/stp.yaml b/stp.yaml new file mode 100644 index 0000000..7977159 --- /dev/null +++ b/stp.yaml @@ -0,0 +1,24 @@ +- key: Ganesh2007 + title: 'A Decision Procedure for Bit-Vectors and Arrays' + author: + - Ganesh, Vijay + - Dill, David L. + year: 2007 + booktitle: CAV 2007 + month: July + publisher: Springer + doi: 10.1007/978-3-540-73368-3_52 + +- key: Cadar2006 + title: 'EXE: Automatically Generating Inputs of Death' + author: + - Cadar, Cristian + - Ganesh, Vijay + - Pawlowski, Peter + - Engler, Dawson + - Dill, David + year: 2006 + booktitle: CCS 2006 + month: October + publisher: ACM + doi: 10.1145/1455518.1455522 diff --git a/template.yaml b/template.yaml new file mode 100644 index 0000000..9cb3969 --- /dev/null +++ b/template.yaml @@ -0,0 +1,12 @@ +- key: x + title: x + author: + - y, x + year: 1 + journal: x + booktitle: CONF 2000 + volume: 1 + pages: 1-2 + publisher: x + doi: x + url: x \ No newline at end of file diff --git a/z3.yaml b/z3.yaml index 1b3e5a5..bd7e6fb 100644 --- a/z3.yaml +++ b/z3.yaml @@ -2,7 +2,7 @@ author: - de Moura, Leonardo - Bjørner, Nikolaj - booktitle: TACAS + booktitle: TACAS 2008 copyright: https://www.microsoft.com/en-us/research/publication/z3-an-efficient-smt-solver/ doi: 10.1007/978-3-540-78800-3_24 langid: english