This talk will give a brief overview of the Satisfiability Modulo Theories (SMT) approach to automated reasoning and its applications, including potentially less familiar applications at Intel. Next we will introduce the Decision Procedure Toolkit (DPT), a new SMT solver developed at Intel and available under an open source license. We will discuss the current state of DPT, our plans for the future, and the opportunities it presents.
Sava Krstic, Jim Grundy, and Amit Goel are Portland, Oregon based Research Scientists with the Logic Verification team of Intel Corporation's Strategic CAD Labs. Their research interests encompass the tools, methods, and theories for the specification, development and verification of hardware and software systems. Together they develop the DPT system of cooperating decision procedures.
Fei Xie