[SMT-LIB] ITP 2017 - 2nd Call for Papers

Geoff Sutcliffe geoff at cs.miami.edu
Mon Jan 23 13:02:50 EST 2017


                         SECOND CALL FOR PAPERS

                                   ITP 2017
8th International Conference on Interactive Theorem Proving
                                  Brasilia, Brazil
                           September 26-29, 2017
                          http://itp2017.cic.unb.br


SUBMISSION DEADLINES
* April 3, 2017 (abstracts)
* April 10, 2017 (full papers)

GENERAL INFORMATION
The ITP conference series is concerned with all topics related to
interactive theorem proving, ranging from theoretical foundations to
implementation aspects and applications in program verification,
security, and formalization of mathematics. ITP is the evolution of
the TPHOLs conference series to the broad field of interactive theorem
proving. TPHOLs meetings took place every year from 1988 until
2009. The eighth ITP conference, ITP 2017, will be held at
Universidade de Brasilia, September 26-29, 2017.

SCOPE OF CONFERENCE
ITP welcomes submissions describing original research on all aspects
of interactive theorem proving and its applications. Suggested topics
include but are not limited to the following:

*  formal aspects of hardware and software
*  formalizations of mathematics
*  improvements in theorem prover technology
*  user interfaces for interactive theorem provers
*  formalizations of computational models
*  verification of security algorithms
*  use of theorem provers in education
*  industrial applications of interactive theorem provers
*  concise and elegant worked examples of formalizations (proof pearls)

PUBLICATION DETAILS
The proceedings of the symposium will be published in the
Springer's LNCS series.

PAPER SUBMISSIONS
All submissions must be original, unpublished, and not submitted
concurrently for publication elsewhere. Furthermore, when appropriate,
submissions are expected to be accompanied by verifiable evidence of
a suitable implementation, such as the source files of a formalization
for the proof assistant used. Submissions should be no more than
16 pages in length and are to be submitted in PDF via EasyChair at
the following address:

   https://easychair.org/conferences/?conf=itp2017

Submissions must conform to the LNCS style in LaTeX. Authors of
accepted papers are expected to present their paper at the conference
and will be required to a sign copyright release form.

In addition to regular papers, described above, there will be a rough
diamond section. Rough diamond submissions are limited to 6 pages
and may consist of an extended abstract. They will be refereed and be
expected to present innovative and promising ideas, possibly in an
early form and without supporting evidence. Accepted diamonds will be
published in the main proceedings and will be presented as short
talks.

After the conference the authors of selected papers will be invited to
submit revised papers for a special issue of the Journal of Automated
Reasoning.

IMPORTANT DATES
Abstract submission deadline: April 3, 2017
Full paper submission deadline: April 10, 2017
Author notification:  June 2, 2017
Camera-ready papers:  June 30, 2017
Workshops & Tutorials:  September 23-25, 2017
Conference:  September 26-29, 2017

INVITED SPEAKERS
   Moa Johansson, Chalmers University of Technology, Sweden
   Leonardo de Moura, Microsoft Research
   Katalin Bimbo, University of Alberta, Canada (joint with TABLEAUX and 
FroCos)
   Jasmin Blanchette  Inria and LORIA, Nancy, France (joint with TABLEAUX 
and FroCos)
   Cesary Kaliszyk    Universitaet Innsbruck, Austria (joint with 
TABLEAUX and FroCos)

WORKSHOPS AND TUTORIALS
   There will be a three-day programme of four workshops and four
   tutorials from 23-25 September.

   Workshops:
     12th Logical and Semantic Frameworks with Applications (LSFA 2017)
     Sandra Alves, Renata Wassermann, Flavio L. C. de Moura
     23 and 24 September 2017

     Proof eXchange for Theorem Proving (PxTP)
     Catherine Dubois, Bruno Woltzenlogel Paleo
     23 and 24 September 2017

     EPS - Encyclopedia of Proof Systems
     Giselle Reis, Bruno Woltzenlogel Paleo
     24 and 25 September 2017

     DaLi - Dynamic Logic: new trends and applications
     Mario Benevides, Alexandre Madeira
     24 September 2017

   Tutorials:

     General methods in proof theory for modal and substructural logics
     Bjoern Lellmann, Revantha Ramanayake
     23 September 2017

     From proof systems to complexity bounds
     Anupam Das
     24 September 2017

     Proof Compressions and the conjecture NP =3D PSPACE
     Lew Gordeev, Edward Hermann Haeusler
     25 September 2017

     PVS for Computer Scientists
     Cesar Munoz, Mauricio Ayala-Rincon, Mariano Moscato
     25 September 2017

   Details will be published in separate calls and on the conference
   website.

PROGRAM COMMITTEE CHAIRS
Mauricio Ayala-Rincon, U. Brasilia
Cesar Munoz, NASA

PROGRAM COMMITTEE CHAIRS
Maria Alpuente, T.U. Valencia
Vander Alves, U.  Brasilia
June Andronick, Data61, CSIRO, UNSW
Jeremy Avigad, Carnegie Mellon U.
Sylvie Boldo, INRIA LRI
Ana Bove, Chalmers & Gothenburg U.
Adam Chlipala, MIT
Gilles Dowek, INRIA, ENS Cachan
Aaron Dutle, NASA
Amy Felty, U. Ottawa
Marcelo Frias, I.T. Buenos Aires
Ruben Gamboa, U. Wyoming
Herman Geuvers, Radboud U.
Elsa Gunter, U. Illinois U.C.
John Harrison, Intel Corporation
Nao Hirokawa, JAIST
Matt Kaufmann, U. Texas Austin
Mark Lawford, McMaster U.
Andreas Lochbihler, ETH Zurich
Assia Mahboubi, INRIA
Panagiotis Manolios, Northeastern U.
Gopalan Nadathur, U. Minnesota
Keiko Nakata, SAP Potsdam
Adam Naumowicz, U. Bialystok
Tobias Nipkow, T.U. Munich
Scott Owens, U. Kent
Sam Owre, SRI
Lawrence Paulson, U. Cambridge
Leila Ribeiro, U.F.  Rio Grande do Sul
Claudio Sacerdoti Coen, U. Bologna
Augusto Sampaio, U.F. Pernambuco
Monika Seisenberger, Swansea U.
Christian Sternagel, U. Innsbruck
Sofiene Tahar,  Concordia U.
Christian Urban, King's College London
Josef Urban, Czech T.U. Prague

CONTACT INFORMATION
Cesar Munoz
Mauricio Ayala-Rincon
itp2017 at easychair.org
http://itp2017.cic.unb.br

--=_95f4dcfdb35fac895ee33829c21e831b
Content-Transfer-Encoding: base64
Content-Type: text/plain;
 name=ITP_cfp_2.txt
Content-Disposition: attachment;
 filename=ITP_cfp_2.txt;
 size=6089

ICAgICAgICAgICoqKiBBcG9sb2dpZXMgZm9yIG11bHRpcGxlIGNvcGllcywgcGxlYXNlIHJlZGlz
dHJpYnV0ZSAqKioKICAKICAgICAgICAgICAgICAgICAgICAgICAgU0VDT05EIENBTEwgRk9SIFBB
UEVSUwoKICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIElUUCAyMDE3Cjh0aCBJbnRl
cm5hdGlvbmFsIENvbmZlcmVuY2Ugb24gSW50ZXJhY3RpdmUgVGhlb3JlbSBQcm92aW5nCiAgICAg
ICAgICAgICAgICAgICAgICAgICAgICAgICAgIEJyYXNpbGlhLCBCcmF6aWwKICAgICAgICAgICAg
ICAgICAgICAgICAgICBTZXB0ZW1iZXIgMjYtMjksIDIwMTcKICAgICAgICAgICAgICAgICAgICAg
ICAgIGh0dHA6Ly9pdHAyMDE3LmNpYy51bmIuYnIKCgpTVUJNSVNTSU9OIERFQURMSU5FUwoqIEFw
cmlsIDMsIDIwMTcgKGFic3RyYWN0cykgCiogQXByaWwgMTAsIDIwMTcgKGZ1bGwgcGFwZXJzKQoK
R0VORVJBTCBJTkZPUk1BVElPTgpUaGUgSVRQIGNvbmZlcmVuY2Ugc2VyaWVzIGlzIGNvbmNlcm5l
ZCB3aXRoIGFsbCB0b3BpY3MgcmVsYXRlZCB0bwppbnRlcmFjdGl2ZSB0aGVvcmVtIHByb3Zpbmcs
IHJhbmdpbmcgZnJvbSB0aGVvcmV0aWNhbCBmb3VuZGF0aW9ucyB0bwppbXBsZW1lbnRhdGlvbiBh
c3BlY3RzIGFuZCBhcHBsaWNhdGlvbnMgaW4gcHJvZ3JhbSB2ZXJpZmljYXRpb24sCnNlY3VyaXR5
LCBhbmQgZm9ybWFsaXphdGlvbiBvZiBtYXRoZW1hdGljcy4gSVRQIGlzIHRoZSBldm9sdXRpb24g
b2YKdGhlIFRQSE9McyBjb25mZXJlbmNlIHNlcmllcyB0byB0aGUgYnJvYWQgZmllbGQgb2YgaW50
ZXJhY3RpdmUgdGhlb3JlbQpwcm92aW5nLiBUUEhPTHMgbWVldGluZ3MgdG9vayBwbGFjZSBldmVy
eSB5ZWFyIGZyb20gMTk4OCB1bnRpbAoyMDA5LiBUaGUgZWlnaHRoIElUUCBjb25mZXJlbmNlLCBJ
VFAgMjAxNywgd2lsbCBiZSBoZWxkIGF0ClVuaXZlcnNpZGFkZSBkZSBCcmFzaWxpYSwgU2VwdGVt
YmVyIDI2LTI5LCAyMDE3LgoKU0NPUEUgT0YgQ09ORkVSRU5DRSAKSVRQIHdlbGNvbWVzIHN1Ym1p
c3Npb25zIGRlc2NyaWJpbmcgb3JpZ2luYWwgcmVzZWFyY2ggb24gYWxsIGFzcGVjdHMKb2YgaW50
ZXJhY3RpdmUgdGhlb3JlbSBwcm92aW5nIGFuZCBpdHMgYXBwbGljYXRpb25zLiBTdWdnZXN0ZWQg
dG9waWNzCmluY2x1ZGUgYnV0IGFyZSBub3QgbGltaXRlZCB0byB0aGUgZm9sbG93aW5nOiAKCiog
IGZvcm1hbCBhc3BlY3RzIG9mIGhhcmR3YXJlIGFuZCBzb2Z0d2FyZQoqICBmb3JtYWxpemF0aW9u
cyBvZiBtYXRoZW1hdGljcwoqICBpbXByb3ZlbWVudHMgaW4gdGhlb3JlbSBwcm92ZXIgdGVjaG5v
bG9neQoqICB1c2VyIGludGVyZmFjZXMgZm9yIGludGVyYWN0aXZlIHRoZW9yZW0gcHJvdmVycwoq
ICBmb3JtYWxpemF0aW9ucyBvZiBjb21wdXRhdGlvbmFsIG1vZGVscwoqICB2ZXJpZmljYXRpb24g
b2Ygc2VjdXJpdHkgYWxnb3JpdGhtcwoqICB1c2Ugb2YgdGhlb3JlbSBwcm92ZXJzIGluIGVkdWNh
dGlvbgoqICBpbmR1c3RyaWFsIGFwcGxpY2F0aW9ucyBvZiBpbnRlcmFjdGl2ZSB0aGVvcmVtIHBy
b3ZlcnMKKiAgY29uY2lzZSBhbmQgZWxlZ2FudCB3b3JrZWQgZXhhbXBsZXMgb2YgZm9ybWFsaXph
dGlvbnMgKHByb29mIHBlYXJscykKClBVQkxJQ0FUSU9OIERFVEFJTFMKVGhlIHByb2NlZWRpbmdz
IG9mIHRoZSBzeW1wb3NpdW0gd2lsbCBiZSBwdWJsaXNoZWQgaW4gdGhlClNwcmluZ2VyJ3MgTE5D
UyBzZXJpZXMuCgpQQVBFUiBTVUJNSVNTSU9OUwpBbGwgc3VibWlzc2lvbnMgbXVzdCBiZSBvcmln
aW5hbCwgdW5wdWJsaXNoZWQsIGFuZCBub3Qgc3VibWl0dGVkCmNvbmN1cnJlbnRseSBmb3IgcHVi
bGljYXRpb24gZWxzZXdoZXJlLiBGdXJ0aGVybW9yZSwgd2hlbiBhcHByb3ByaWF0ZSwKc3VibWlz
c2lvbnMgYXJlIGV4cGVjdGVkIHRvIGJlIGFjY29tcGFuaWVkIGJ5IHZlcmlmaWFibGUgZXZpZGVu
Y2Ugb2YKYSBzdWl0YWJsZSBpbXBsZW1lbnRhdGlvbiwgc3VjaCBhcyB0aGUgc291cmNlIGZpbGVz
IG9mIGEgZm9ybWFsaXphdGlvbiAKZm9yIHRoZSBwcm9vZiBhc3Npc3RhbnQgdXNlZC4gU3VibWlz
c2lvbnMgc2hvdWxkIGJlIG5vIG1vcmUgdGhhbiAKMTYgcGFnZXMgaW4gbGVuZ3RoIGFuZCBhcmUg
dG8gYmUgc3VibWl0dGVkIGluIFBERiB2aWEgRWFzeUNoYWlyIGF0IAp0aGUgZm9sbG93aW5nIGFk
ZHJlc3M6CgogIGh0dHBzOi8vZWFzeWNoYWlyLm9yZy9jb25mZXJlbmNlcy8/Y29uZj1pdHAyMDE3
CgpTdWJtaXNzaW9ucyBtdXN0IGNvbmZvcm0gdG8gdGhlIExOQ1Mgc3R5bGUgaW4gTGFUZVguIEF1
dGhvcnMgb2YKYWNjZXB0ZWQgcGFwZXJzIGFyZSBleHBlY3RlZCB0byBwcmVzZW50IHRoZWlyIHBh
cGVyIGF0IHRoZSBjb25mZXJlbmNlCmFuZCB3aWxsIGJlIHJlcXVpcmVkIHRvIGEgc2lnbiBjb3B5
cmlnaHQgcmVsZWFzZSBmb3JtLgogCkluIGFkZGl0aW9uIHRvIHJlZ3VsYXIgcGFwZXJzLCBkZXNj
cmliZWQgYWJvdmUsIHRoZXJlIHdpbGwgYmUgYSByb3VnaApkaWFtb25kIHNlY3Rpb24uIFJvdWdo
IGRpYW1vbmQgc3VibWlzc2lvbnMgYXJlIGxpbWl0ZWQgdG8gNiBwYWdlcyAKYW5kIG1heSBjb25z
aXN0IG9mIGFuIGV4dGVuZGVkIGFic3RyYWN0LiBUaGV5IHdpbGwgYmUgcmVmZXJlZWQgYW5kIGJl
CmV4cGVjdGVkIHRvIHByZXNlbnQgaW5ub3ZhdGl2ZSBhbmQgcHJvbWlzaW5nIGlkZWFzLCBwb3Nz
aWJseSBpbiBhbgplYXJseSBmb3JtIGFuZCB3aXRob3V0IHN1cHBvcnRpbmcgZXZpZGVuY2UuIEFj
Y2VwdGVkIGRpYW1vbmRzIHdpbGwgYmUKcHVibGlzaGVkIGluIHRoZSBtYWluIHByb2NlZWRpbmdz
IGFuZCB3aWxsIGJlIHByZXNlbnRlZCBhcyBzaG9ydAp0YWxrcy4KCkFmdGVyIHRoZSBjb25mZXJl
bmNlIHRoZSBhdXRob3JzIG9mIHNlbGVjdGVkIHBhcGVycyB3aWxsIGJlIGludml0ZWQgdG8Kc3Vi
bWl0IHJldmlzZWQgcGFwZXJzIGZvciBhIHNwZWNpYWwgaXNzdWUgb2YgdGhlIEpvdXJuYWwgb2Yg
QXV0b21hdGVkClJlYXNvbmluZy4KCklNUE9SVEFOVCBEQVRFUyAKQWJzdHJhY3Qgc3VibWlzc2lv
biBkZWFkbGluZTogQXByaWwgMywgMjAxNwpGdWxsIHBhcGVyIHN1Ym1pc3Npb24gZGVhZGxpbmU6
IEFwcmlsIDEwLCAyMDE3CkF1dGhvciBub3RpZmljYXRpb246ICBKdW5lIDIsIDIwMTcKQ2FtZXJh
LXJlYWR5IHBhcGVyczogIEp1bmUgMzAsIDIwMTcKV29ya3Nob3BzICYgVHV0b3JpYWxzOiAgU2Vw
dGVtYmVyIDIzLTI1LCAyMDE3CkNvbmZlcmVuY2U6ICBTZXB0ZW1iZXIgMjYtMjksIDIwMTcKCklO
VklURUQgU1BFQUtFUlMKICBNb2EgSm9oYW5zc29uLCBDaGFsbWVycyBVbml2ZXJzaXR5IG9mIFRl
Y2hub2xvZ3ksIFN3ZWRlbgogIExlb25hcmRvIGRlIE1vdXJhLCBNaWNyb3NvZnQgUmVzZWFyY2gg
CiAgS2F0YWxpbiBCaW1ibywgVW5pdmVyc2l0eSBvZiBBbGJlcnRhLCBDYW5hZGEgKGpvaW50IHdp
dGggVEFCTEVBVVggYW5kIEZyb0NvcykKICBKYXNtaW4gQmxhbmNoZXR0ZSAgSW5yaWEgYW5kIExP
UklBLCBOYW5jeSwgRnJhbmNlIChqb2ludCB3aXRoIFRBQkxFQVVYIGFuZCBGcm9Db3MpCiAgQ2Vz
YXJ5IEthbGlzenlrICAgIFVuaXZlcnNpdGFldCBJbm5zYnJ1Y2ssIEF1c3RyaWEgKGpvaW50IHdp
dGggVEFCTEVBVVggYW5kIEZyb0NvcykgCgpXT1JLU0hPUFMgQU5EIFRVVE9SSUFMUwogIFRoZXJl
IHdpbGwgYmUgYSB0aHJlZS1kYXkgcHJvZ3JhbW1lIG9mIGZvdXIgd29ya3Nob3BzIGFuZCBmb3Vy
CiAgdHV0b3JpYWxzIGZyb20gMjMtMjUgU2VwdGVtYmVyLgoKICBXb3Jrc2hvcHM6CiAgICAxMnRo
IExvZ2ljYWwgYW5kIFNlbWFudGljIEZyYW1ld29ya3Mgd2l0aCBBcHBsaWNhdGlvbnMgKExTRkEg
MjAxNykKICAgIFNhbmRyYSBBbHZlcywgUmVuYXRhIFdhc3Nlcm1hbm4sIEZsYXZpbyBMLiBDLiBk
ZSBNb3VyYQogICAgMjMgYW5kIDI0IFNlcHRlbWJlciAyMDE3CgogICAgUHJvb2YgZVhjaGFuZ2Ug
Zm9yIFRoZW9yZW0gUHJvdmluZyAoUHhUUCkKICAgIENhdGhlcmluZSBEdWJvaXMsIEJydW5vIFdv
bHR6ZW5sb2dlbCBQYWxlbwogICAgMjMgYW5kIDI0IFNlcHRlbWJlciAyMDE3CgogICAgRVBTIC0g
RW5jeWNsb3BlZGlhIG9mIFByb29mIFN5c3RlbXMKICAgIEdpc2VsbGUgUmVpcywgQnJ1bm8gV29s
dHplbmxvZ2VsIFBhbGVvCiAgICAyNCBhbmQgMjUgU2VwdGVtYmVyIDIwMTcKCiAgICBEYUxpIC0g
RHluYW1pYyBMb2dpYzogbmV3IHRyZW5kcyBhbmQgYXBwbGljYXRpb25zCiAgICBNYXJpbyBCZW5l
dmlkZXMsIEFsZXhhbmRyZSBNYWRlaXJhCiAgICAyNCBTZXB0ZW1iZXIgMjAxNwoKICBUdXRvcmlh
bHM6CgogICAgR2VuZXJhbCBtZXRob2RzIGluIHByb29mIHRoZW9yeSBmb3IgbW9kYWwgYW5kIHN1
YnN0cnVjdHVyYWwgbG9naWNzCiAgICBCam9lcm4gTGVsbG1hbm4sIFJldmFudGhhIFJhbWFuYXlh
a2UKICAgIDIzIFNlcHRlbWJlciAyMDE3CgogICAgRnJvbSBwcm9vZiBzeXN0ZW1zIHRvIGNvbXBs
ZXhpdHkgYm91bmRzCiAgICBBbnVwYW0gRGFzCiAgICAyNCBTZXB0ZW1iZXIgMjAxNwoKICAgIFBy
b29mIENvbXByZXNzaW9ucyBhbmQgdGhlIGNvbmplY3R1cmUgTlAgPTNEIFBTUEFDRQogICAgTGV3
IEdvcmRlZXYsIEVkd2FyZCBIZXJtYW5uIEhhZXVzbGVyCiAgICAyNSBTZXB0ZW1iZXIgMjAxNwoK
ICAgIFBWUyBmb3IgQ29tcHV0ZXIgU2NpZW50aXN0cwogICAgQ2VzYXIgTXVub3osIE1hdXJpY2lv
IEF5YWxhLVJpbmNvbiwgTWFyaWFubyBNb3NjYXRvCiAgICAyNSBTZXB0ZW1iZXIgMjAxNwoKICBE
ZXRhaWxzIHdpbGwgYmUgcHVibGlzaGVkIGluIHNlcGFyYXRlIGNhbGxzIGFuZCBvbiB0aGUgY29u
ZmVyZW5jZQogIHdlYnNpdGUuCgpQUk9HUkFNIENPTU1JVFRFRSBDSEFJUlMgCk1hdXJpY2lvIEF5
YWxhLVJpbmNvbiwgVS4gQnJhc2lsaWEgCkNlc2FyIE11bm96LCBOQVNBIAoKUFJPR1JBTSBDT01N
SVRURUUgQ0hBSVJTICAKTWFyaWEgQWxwdWVudGUsIFQuVS4gVmFsZW5jaWEgClZhbmRlciBBbHZl
cywgVS4gIEJyYXNpbGlhIApKdW5lIEFuZHJvbmljaywgRGF0YTYxLCBDU0lSTywgVU5TVwpKZXJl
bXkgQXZpZ2FkLCBDYXJuZWdpZSBNZWxsb24gVS4gClN5bHZpZSBCb2xkbywgSU5SSUEgTFJJIApB
bmEgQm92ZSwgQ2hhbG1lcnMgJiBHb3RoZW5idXJnIFUuIApBZGFtIENobGlwYWxhLCBNSVQgCkdp
bGxlcyBEb3dlaywgSU5SSUEsIEVOUyBDYWNoYW4gCkFhcm9uIER1dGxlLCBOQVNBICAKQW15IEZl
bHR5LCBVLiBPdHRhd2EgCk1hcmNlbG8gRnJpYXMsIEkuVC4gQnVlbm9zIEFpcmVzClJ1YmVuIEdh
bWJvYSwgVS4gV3lvbWluZyAKSGVybWFuIEdldXZlcnMsIFJhZGJvdWQgVS4KRWxzYSBHdW50ZXIs
IFUuIElsbGlub2lzIFUuQy4gCkpvaG4gSGFycmlzb24sIEludGVsIENvcnBvcmF0aW9uIApOYW8g
SGlyb2thd2EsIEpBSVNUCk1hdHQgS2F1Zm1hbm4sIFUuIFRleGFzIEF1c3RpbgpNYXJrIExhd2Zv
cmQsIE1jTWFzdGVyIFUuIApBbmRyZWFzIExvY2hiaWhsZXIsIEVUSCBadXJpY2ggCkFzc2lhIE1h
aGJvdWJpLCBJTlJJQSAKUGFuYWdpb3RpcyBNYW5vbGlvcywgTm9ydGhlYXN0ZXJuIFUuIApHb3Bh
bGFuIE5hZGF0aHVyLCBVLiBNaW5uZXNvdGEgCktlaWtvIE5ha2F0YSwgU0FQIFBvdHNkYW0KQWRh
bSBOYXVtb3dpY3osIFUuIEJpYWx5c3RvawpUb2JpYXMgTmlwa293LCBULlUuIE11bmljaCAKU2Nv
dHQgT3dlbnMsIFUuIEtlbnQgClNhbSBPd3JlLCBTUkkKTGF3cmVuY2UgUGF1bHNvbiwgVS4gQ2Ft
YnJpZGdlIApMZWlsYSBSaWJlaXJvLCBVLkYuICBSaW8gR3JhbmRlIGRvIFN1bCAKQ2xhdWRpbyBT
YWNlcmRvdGkgQ29lbiwgVS4gQm9sb2duYSAKQXVndXN0byBTYW1wYWlvLCBVLkYuIFBlcm5hbWJ1
Y28gCk1vbmlrYSBTZWlzZW5iZXJnZXIsIFN3YW5zZWEgVS4KQ2hyaXN0aWFuIFN0ZXJuYWdlbCwg
VS4gSW5uc2JydWNrIApTb2ZpZW5lIFRhaGFyLCAgQ29uY29yZGlhIFUuCkNocmlzdGlhbiBVcmJh
biwgS2luZydzIENvbGxlZ2UgTG9uZG9uIApKb3NlZiBVcmJhbiwgQ3plY2ggVC5VLiBQcmFndWUK
CkNPTlRBQ1QgSU5GT1JNQVRJT04gCkNlc2FyIE11bm96Ck1hdXJpY2lvIEF5YWxhLVJpbmNvbgpp
dHAyMDE3QGVhc3ljaGFpci5vcmcKaHR0cDovL2l0cDIwMTcuY2ljLnVuYi5icgo=
--=_95f4dcfdb35fac895ee33829c21e831b--



More information about the SMT-LIB mailing list