-
Notifications
You must be signed in to change notification settings - Fork 0
/
contact.shtml
157 lines (144 loc) · 6.43 KB
/
contact.shtml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<title>SMT-LIB The Satisfiability Modulo Theories Library</title>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8" />
<link href="style.css" rel="stylesheet" type="text/css" />
<!-- CuFon: Enables smooth pretty custom font rendering. 100% SEO friendly. To disable, remove this section -->
<script type="text/javascript" src="js/cufon-yui.js"></script>
<script type="text/javascript" src="js/arial.js"></script>
<script type="text/javascript" src="js/cuf_run.js"></script>
<!-- CuFon ends -->
<link href="code-prettify/prettify.css" type="text/css" rel="stylesheet" />
<script src="code-prettify/run_prettify.js?lang=smtlib&skin=desert"></script>
</head>
<body>
<div class="main">
<div class="header">
<div class="header_resize">
<div class="menu_nav">
<ul>
<li><a href="index.shtml">Home</a></li>
<li><a href="about.shtml">About</a></li>
<li><a href="news.shtml">News</a></li>
<li><a href="standard.shtml">Standard</a></li>
<li><a href="benchmarks.shtml">Benchmarks</a></li>
<li><a href="software.shtml">Software</a></li>
<li><a href="credits.shtml">Credits</a></li>
</ul>
</div>
<div class="clr"></div>
<div class="logo">
<h1><a href="index.shtml">SMT-LIB <br/>
<small>The Satisfiability Modulo Theories Library</small></a>
</h1>
</div>
</div>
</div>
<div class="content">
<div class="content_resize">
<div class="mainbar">
<div class="article">
<h2>Contacts and Contributions</h2>
<p>
For feedback, comments, and inquiries
please send an email to one of co-ordinators:
<a href="http://www.cs.stanford.edu/~barrett/">
Clark Barrett</a>,
<a href="http://www.loria.fr/~fontaine/">
Pascal Fontaine</a>, and
<a href="http://www.cs.uiowa.edu/%7Etinelli">
Cesare Tinelli</a>.
</p>
<h3>Discussion Forum</h3>
<p>There is a discussion forum dedicated to discussing the SMT-LIB standard and proposed extensions, as well as any other matter regarding the library:
<a href="https://groups.google.com/d/forum/smt-lib">https://groups.google.com/d/forum/smt-lib</a>.
<br>
You can follow or join the discussion by subscribing to the forum.
</p>
<p><b>Note:</b>
The discussion forum is not an appropriate one for announcements such as calls for papers, positions, and so on. For that, please use <a href="https://groups.google.com/d/forum/smt-announce">https://groups.google.com/d/forum/smt-announce</a> instead.
</p>
<p>Until May 30, 2017, the discussion list was on a different server. You can access its archived messages at <a href="http://www.cs.nyu.edu/pipermail/smt-lib">http://www.cs.nyu.edu/pipermail/smt-lib</a>.
</p>
<h3>Benchmarks</h3>
<p>The success of this initiative depends on collecting and maintaining a large and varied collection of benchmarks.
If you would like to contribute your benchmarks to SMT-LIB please contact one of the organizers above.
</p>
<h3>Extensions</h3>
<p>The SMT-LIB standard is driven by the needs of the community.
If you would like to propose any extensions to the standard (new theories or logics, or new features for the SMT-LIB language) please contact the organizers first.
For non-minor extensions, the usual process is the following:
<ol>
<li>A person or group of people decides to propose an extension.</li>
<li>They contact the organizers or they bring up the issue during the SMT-LIB discussion session at the <a href="http://smt-workshop.org/">SMT workshop</a>.
<li>In either case, there in an initial discussion to see whether
<ul>
<li>the proposed extension is within the scope of the initiative and the SMT-LIB language;</li>
<li>it is of interest to enough people;</li>
<li>there are applications that would generate enough benchmarks using the extension.</li>
</ul>
</li>
<li>If the extension is deemed feasible, a work group is formed, with participation open to any interested people. At least one of the SMT-LIB co-organizers joins the work group at some point to make sure that the technical aspects of the proposal are sound.
</li>
<li>The work group discusses the extension in depth and prepares a detailed proposal.
</li>
<li>The proposal is presented to the SMT-LIB community through the discussion list above.</li>
<li>Feedback from the community is used to improve the final version of the proposal.</li>
<li>The proposed extension is officially incorporated into the standard and documented on this site.</li>
</ol>
</p>
</div>
</div>
<div class="sidebar">
<div class="gadget">
<ul class="sb_menu">
<li><a href="index.shtml">Home</a></li>
<li><a href="about.shtml">About</a></li>
<li><a href="news.shtml">News</a></li>
<li>Standard
<ul class="ex_menu">
<li><a href="language.shtml">Language</a>
<li><a href="theories.shtml">Theories</a>
<li><a href="logics.shtml">Logics</a>
<li><a href="examples.shtml">Examples</a>
</ul>
</li>
<li><a href="benchmarks.shtml">Benchmarks</a></li>
<li>Software
<ul class="ex_menu">
<li><a href="solvers.shtml">Solvers</a></li>
<li><a href="utilities.shtml">Utilities</a></li>
</ul>
</li>
<li><a href="contact.shtml">Contact</a></li>
<li><a href="related.shtml">Related</a></li>
<li><a href="credits.shtml">Credits</a></li>
</ul>
</div>
</div>
</div>
</div>
<div class="clr"></div>
<div class="footer">
<div class="footer_resize">
<p class="lf">
© Copyright The SMT-LIB Initiative <br>
Based on a design by
Blue <a href="http://www.bluewebtemplates.com">Web Templates</a>
</p>
<ul class="fmenu">
<li><a href="index.shtml">Home</a></li>
<li><a href="about.shtml">About</a></li>
<li><a href="news.shtml">News</a></li>
<li><a href="standard.shtml">Standard</a></li>
<li><a href="benchmarks.shtml">Benchmarks</a></li>
<li><a href="software.shtml">Software</a></li>
<li><a href="credits.shtml">Credits</a></li>
</ul>
<div class="clr"></div>
</div>
</div>
</div>
</body>
</html>