BEGIN:VCALENDAR
VERSION:2.0
PRODID:ILLC Website
X-WR-TIMEZONE:Europe/Amsterdam
BEGIN:VTIMEZONE
TZID:Europe/Amsterdam
X-LIC-LOCATION:Europe/Amsterdam
BEGIN:DAYLIGHT
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
TZNAME:CEST
DTSTART:19700329T020000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
TZNAME:CET
DTSTART:19701025T030000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
UID:/NewsandEvents/Archives/2007/newsitem/1645/1-2
 -July-2007-5th-International-Workshop-on-Satisfiab
 ility-Modulo-Theories-SMT-07-Berlin-Germany
DTSTAMP:20061210T000000
SUMMARY:5th International Workshop on Satisfiabili
 ty Modulo Theories (SMT '07), Berlin, Germany
DTSTART;VALUE=DATE:20070701
DTEND;VALUE=DATE:20070702
LOCATION:Berlin, Germany
DESCRIPTION:Deciding the satisfiability of first-o
 rder formulas modulo background theories, known as
  the Satisfiability Modulo Theories (SMT) problem,
  has proved to be useful in verification, compiler
  optimization, scheduling, and other areas. The su
 ccess of SMT techniques depends on the development
  of both domain-specific decision procedures for e
 ach concrete theory (e.g. linear arithmetic, the t
 heory of arrays, or the theory of bit-vectors) and
  combination methods that allow one to obtain more
  versatile SMT tools. These two ingredients togeth
 er make SMT techniques well-suited for use in larg
 er automated reasoning and formal verification eff
 orts.    The aim of the workshop is to bring toget
 her researchers and users of SMT tools and techniq
 ues. Continuing with the PDPAR tradition, we espec
 ially encourage submission of papers focused on pr
 agmatic aspects.   For more information, see http:
 //www.lsi.upc.edu/~oliveras/smt07   The Programme 
 Committee cordially invites all researchers to sub
 mit their papers for presentation. Submission dead
 line : 23 April
X-ALT-DESC;FMTTYPE=text/html:<div>\n      <p>Decid
 ing the satisfiability of first-order formulas mod
 ulo background\n        theories, known as the Sat
 isfiability Modulo Theories (SMT) problem,\n      
   has proved to be useful in verification, compile
 r optimization,\n        scheduling, and other are
 as.\n        The success of SMT techniques  depend
 s on the\n        development of both domain-speci
 fic decision procedures for each\n        concrete
  theory (e.g. linear arithmetic, the theory of arr
 ays, or the\n        theory of bit-vectors) and co
 mbination methods that allow one to\n        obtai
 n more versatile SMT tools. These two ingredients 
 together make\n        SMT techniques well-suited 
 for use in larger automated reasoning and\n       
  formal verification efforts.\n      </p>\n      <
 p>\n        The aim of the workshop is to bring to
 gether researchers and users of\n        SMT tools
  and techniques. Continuing with the PDPAR traditi
 on, we\n        especially encourage submission of
  papers focused on pragmatic\n        aspects.\n  
     </p>\n    \n      \n      <p>For more informat
 ion, see\n        <a target="_blank" href="http://
 www.lsi.upc.edu/~oliveras/smt07">http://www.lsi.up
 c.edu/~oliveras/smt07</a>\n      </p>\n    </div><
 div>\n      <p>\n        The Programme Committee c
 ordially invites all researchers\n        to submi
 t their\n        papers for presentation.\n       
  Submission deadline                  : 23 April\n
       </p>\n      </div>
URL:/NewsandEvents/Archives/2007/newsitem/1645/1-2
 -July-2007-5th-International-Workshop-on-Satisfiab
 ility-Modulo-Theories-SMT-07-Berlin-Germany
END:VEVENT
END:VCALENDAR
