5 Motivation for SMT solvers, and combination of decision procedures (1185841), страница 5

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 5)

(2011)2-counter machines reduced towords with single quantifier alter.Decidability (PSPACE) of QFTheory of Word EquationsMakanin (1977)Makanin result very difficultPlandowski (1996, 2002/06) Simplified by PlandowskiDecidability (PSPACEcomplete) of QF Theory ofWord Equations + RESchultz (1992)RE membership predicateQF word equations + Length()Matiyasevich (1971)(?)UnsolvedReduction to DiophantineQF word equations in solvedform + Length() + REPracticalVijay GaneshWednesday, 16 January, 13G. (2011)82Future of HAMPI & STP• HAMPI will be combined with STP• Bit-vectors and Arrays• Integer/Real Linear Arithmetic• Uninterpreted Functions• Strings• Floating Point• Non-linear• Additional features planned in STP• UNSAT Core• Quantifiers• Incremental• DPLL(T)• Parallel STP• MAXSMT?• Extensibility and hackability by non-expertVijay GaneshWednesday, 16 January, 1383Future of Strings• Strings SMTization effort started• Nikolaj Bjorner, G.• Andrei Voronkov, Ruzica Piskac, Ting Zhang• Cesare Tinelli, Clark Barrett, Dawn Song, Prateek Saxena, Pieter Hooimeijer, Tim Hinrichs• SMT Theory of Strings• Alphabet (UTF, Unicode,...)• String Constants and String Vars (parameterized by length)• Concat, Extract, Replace, Length Functions• Regular Expressions, CFGs (Extended BNF)• Equality, Membership Predicate, Contains Predicate• Applications• Static/Dynamic Analysis for Vulnerability Detection• Security Testing using Concolic Idea• Formal Methods• SynthesisVijay GaneshWednesday, 16 January, 1384Conclusions & Take Away• SMT solvers essential for testing, analysis, verification,...• Core SMT ideas• Combinations• DPLL(T)• Over/Under approximations (CEGAR,...)• SAT solvers• Future of SMT solvers• SMT + Languages• SMT + Synthesis• Parallel SAT/SMT• Demand for even richer theories• Attribute grammars• String theories with lengthVijay GaneshWednesday, 16 January, 1385Modern SMT Solver ReferencesThese websites and handbook have all the references you will need1.

Armin Bierre, Marijn Heule, Hans van Maaren, and Toby Walsh (Editors). Handbook of Satisfiability. 2009. IOS Press. http://www.st.ewi.tudelft.nl/sat/handbook/2. SAT Live: http://www.satlive.org/3. SMT LIB: http://www.smtlib.org/4. SAT/SMT summer school: http://people.csail.mit.edu/vganesh/summerschool/Vijay GaneshWednesday, 16 January, 1386Topics CoveredTopics covered in Lecture 1Motivation for SAT/SMT solvers in software engineering• Software engineering (SE) problems reduced to logic problems• Automation, engineering, usability of SE tools through solversHigh-level description of the SAT/SMT problem & logics• Rich logics close to program semantics• Demonstrably easy to solve in many practical casesModern SAT solver architecture & techniques• DPLL search, shortcomings• Modern CDCL SAT solver: propagate (BCP), decide (VSIDS), conflict analysis, clause learn, backJump,• Termination, correctness• Big lesson: learning from mistakesTopics covered in Lecture 2Modern SMT solver architecture & techniques• Rich logics closer to program semantics• DPLL(T), Combinations of solvers, Over/under approximationsMy own contributions: STP & HAMPI• Abstraction-refinement for solving• Bounded logicsSAT/SMT-based applications• Dynamic systematic testing• Static, dynamic analysis for vulnerability detectionFuture of SAT/SMT solversVijay GaneshWednesday, 16 January, 1387Key Contributionshttp://people.csail.mit.edu/vganeshNameKey ConceptImpactPubsSTPBit-vector & Array Solver1,2Abstraction-refinementfor SolvingConcolicTestingCAV 2007CCS 2006TISSEC 2008HAMPIString Solver1App-driven Bounding for Analysis ofSolvingWeb AppsISSTA 20093TOSEM 2011(CAV 2011)Taint-based FuzzingInformation flow ischeaper than concolicScales betterthan concolicICSE 2009Acceptability Envelope:Fix the input, not theprogramNew way ofUnderapproaching SE SubmissionAutomatic InputRectification1.

100+ research projects use STP and HAMPI2. STP won the SMTCOMP 2006 and 2010 competitions for bit-vector solvers3. HAMPI: ACM Best Paper Award 20094. Retargetable Compiler (DATE 1999)5. Proof-producing decision procedures (TACAS 2003)6. Error-finding in ARBAC policies (CCS 2011)Vijay Ganesh, Dagstuhl, Aug 8-12, 2011Wednesday, 16 January, 1388.

Характеристики

Список файлов лекций