Transcription
Software Verification withSatisfiability Modulo TheoriesNikolaj BjørnerMicrosoft ResearchSSFT 2014, Menlo Park
ContentsA primer on SMT with Z3SMT & Verification by Assertion Checking- Boogie GC, Quantifiers, TheoriesSMT & Verification by Assertion Inference- Symbolic Software Model Checking,Horn Clauses
SMT & antsBoogie/Dafny PropertyFindbugsSAGE, PexSynthesizeAuxiliaryinvariantsSLAM, Yogi, DASH,Z3-Horn, Duality,HSF, Liquid
– Backed by Proof PlumbersNot all is hopelessLeonardo de Moura, Nikolaj Bjørner, Christoph Wintersteiger
A primer on SMT with Z3
MaterialSeptember 2011
Some Microsoft Tools based AnalysisAuditingUnderApproximationType SafetySLAyerSAGESynthesisBEK
SAT IN A NUTSHELL
SAT in a nutshell(Tie Shirt) ( Tie Shirt) ( Tie Shirt)
SMT IN A NUTSHELL
Satisfiability Modulo Theories (SMT)Is formula satisfiablemodulo theory T ?SMT solvers havespecialized algorithms for T
Satisfiability Modulo Theories (SMT)𝑥 2 𝑦 𝑓 𝑠𝑒𝑙𝑒𝑐𝑡 𝑠𝑡𝑜𝑟𝑒 𝑎, 𝑥, 3 , 𝑦 2Array ���𝑟𝑒 𝑎, 𝑖, 𝑣 , 𝑖) 𝑣𝑖 𝑗 𝑠𝑒𝑙𝑒𝑐𝑡(𝑠𝑡𝑜𝑟𝑒 𝑎, 𝑖, 𝑣 , 𝑗) 𝑠𝑒𝑙𝑒𝑐𝑡(𝑎, 𝑗) 𝑓(𝑦 𝑥 1)UninterpretedFunctions
SMT SOLVING IN A NUTSHELLJob Shop Scheduling
Job Shop SchedulingMachinesTasksJobsP NP?Laundry𝜁 𝑠 0 𝑠 1 𝑖𝑟2
Job Shop SchedulingConstraints:Precedence: between two tasks of the samejob3412Resource: Machines execute at most one jobat a time𝑠𝑡𝑎𝑟𝑡2,2 . . 𝑒𝑛𝑑2,2 𝑠𝑡𝑎𝑟𝑡4,2 . . 𝑒𝑛𝑑4,2
Job Shop 2,3 - start time ofjob 2 on mach 3𝑑2,3 - duration ofjob 2 on mach 3𝑡2,3 𝑑2,3 𝑡2,4Resource:Not convex𝑠𝑡𝑎𝑟𝑡2,2 . . 𝑒𝑛𝑑2,2 𝑠𝑡𝑎𝑟𝑡4,2 . . 𝑒𝑛𝑑4,2 𝑡2,2 𝑑2,2 𝑡4,2 𝑡4,2 d4,2 𝑡2,2
Job Shop Scheduling
Job Shop Schedulingcase splitEfficient solvers:- Floyd-Warshal algorithm- Ford-Fulkerson algorithmcase split𝑧 𝑧 5 – 2 – 3 – 2 2 0
THEORIES
TheoriesUninterpreted functions
TheoriesUninterpreted functionsArithmetic (linear)
TheoriesUninterpreted functionsArithmetic (linear)Bit-vectors
TheoriesUninterpreted functionsArithmetic (linear)Bit-vectorsAlgebraic data-types
TheoriesUninterpreted functionsArithmetic (linear)Bit-vectorsAlgebraic data-typesArrays
TheoriesUninterpreted functionsArithmetic (linear)Bit-vectorsAlgebraic data-typesArraysPolynomial Arithmetic
QUANTIFIERS
Quantifier EliminationPresburger Arithmetic,Algebraic Data-types,Quadratic polynomialsSMT integration to prune branches[B. IJCAR 2010]
MBQI: Model based QuantifierInstantiation[de Moura, Ge. CAV 2008][Bonachnia, Lynch, de Moura CADE 2009][de Moura, B. IJCAR 2010]
MODELS, PROOFS, CORES &SIMPLIFICATION
ModelsLogical FormulaSat/Model
ProofsLogical FormulaUnsat/Proof
SimplificationLogical FormulaSimplify
CoresLogical FormulaUnsat. Core
TACTICS, SOLVERS
TacticsComposition of tactics: (then t s) (par-then t s) applies t to the input goal and s to every subgoal produced by t in parallel. (or-else t s) (par-or t s) applies t and s in parallel until one of them succeed. (repeat t) (repeat t n) (try-for t ms) (using-params t params) Apply the given tactic using the given parameters.
Solvers Tactics take goals and reduce to sub-goals Solvers take tactics and serve as logical contexts. push add check model, core, proof pop
APISC pythonJavaOCaml.NETC
SummaryZ3 supports several theories– Using a default combination– Providing custom tactics for special combinationsZ3 is more than sat/unsat– Models, proofs, unsat cores,– simplification, quantifier elimination are tacticsPrototype with python/smt-lib2– Implement using smt-lib2/programmatic API
SMT SOLVING IN A NUTSHELL Job Shop Scheduling. Job Shop Scheduling Machines Jobs P NP? Laundry 1 2 . Prototype with python/smt-lib2 -Implement using smt-lib2/programmatic API. Title: PowerPoint Presentation Author: Nikolaj Bjorner Created Date: 5/21/2014 7:49:27 AM .
