slides-afm-tutorial

Satisfiability Modulo Theories (SMT) Applications of SMT YicesSMT is the problem of determining satisfiability of formulas modulo Extended Static Checking Yices is an SMT Solver developed at SRI International.Yices 1.0: An Efficient SMT Solverbackground theories.Equivalence Checking (Hardware) Yices is not ICS.AFM’06 TutorialExamples of background theories:Bounded Model Checking (e.g., sal-inf-bmc) It is used in SAL, PVS, and CALO.Leonardo de Moura (joint work with Bruno Dutertre)linear arithmetic: x+1≤ yPredicate Abstraction It is a complete reimplementation of SRI’s previous SMT solvers.{demoura, bruno}@csl.sri.com.arrays: a[i := v ][j]=v1 2It has a new architecture, and uses new algorithms.Symbolic Simulationuninterpreted functions: f(f(f(x))) = xComputer Science LaboratoryCounterexamples and Unsatisfiable Cores.Test Case Generation (e.g., sal-atg)SRI International datatypes: car(cons(v ,v )) = v1 3 2Incremental: push, pop, and retract.AI Planning & SchedulingMenlo Park, CAbitvectors: concat(bv ,bv)=bv1 2 3Weighted MaxSAT/MaxSMT.Embedded in Theorem Provers (e.g., PVS)Example of formula:Supports all theories in SMT-LIB and much more.i−1=j+2,f(i+3)= f(j+6)Yices: An Efficient SMT Solver – p.1 Yices: An Efficient SMT Solver – p.2 Yices: An Efficient SMT Solver – p.3 Yices: An Efficient SMT Solver – p.4Supported Features Using Yices First Example Checkassert gets only trivial inconsistencies.Uninterpreted functions Starting yices shell:./yices ...