\n

<
div>\n 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

\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 \n \n \nFor more informat ion, see\n http://www.lsi.up c.edu/~oliveras/smt07\n

\n\n The Programme Committee c ordially invites all researchers\n to submi t their\n papers for presentation.\n Submission deadline : 23 April\n

\n URL:/NewsandEvents/Events/Conferences/newsitem/164 5/1-2-July-2007-5th-International-Workshop-on-Sati sfiability-Modulo-Theories-SMT-07-Berlin-Germany END:VEVENT END:VCALENDAR