On Abstraction Refinement for Program Analyses in Datalog

On Abstraction Refinement for Program Analyses in Datalog

Maximum Satisfiability in Software Analysis: Applications & Techniques Mayur Naik, University of Pennsylvania Joint work with: Xujie Si and Xin Zhang Georgia Tech Aditya Nori Microsoft Research Radu Grigore University of Kent Hongseok Yang University of Oxford Constraint-Based Software Analysis Program Constraints Constra int Resoluti on Solution Long history Constrai nt Generati on Type constraints, set constraints, SAT/SMT constraints Many benefits

2 Separates analysis specification from implementation Allows to leverage sophisticated off-the-shelf solvers Yields natural program specifications CAV 2017 02/29/2020 Challenges in Software Analysis But constraint-based approach is not well-suited for Balancing trade-offs Handling uncertainty e.g. precision vs. scalability e.g. incorrect specifications Modeling missing information 3 e.g. incomplete programs CAV 2017 02/29/2020 An Emerging Approach Constraint Satisfaction Optimization

Balancing trade-offs e.g. precision vs. scalability Handling uncertainty Constraint Objectives e.g. incorrect specifications Modeling missing information 4 e.g. incomplete programs CAV 2017 02/29/2020 The Maximum Satisfiability Problem MaxSAT: 1 2 3 5 (C1) (C2) (C3) (C4) (C5) CAV 2017 02/29/2020

The Maximum Satisfiability Problem MaxSAT: 4: 1 2:2 7:3 (C1) (C2) (C3) (C4) (C5) = Subject to Subject to Maximize C1 C2 4C3+2C4+7C5 Solution: a = true, b = true, c = true, d = false (Objective = 11) 6 CAV 2017 02/29/2020 The Maximum Satisfiability Problem + Expressive for our problems Hard Soundness Conditions + Soft 7

Objectives Balancing Handling Modeling tradeoffs uncertaintymissing data (e.g., precision (e.g., (e.g., partial vs. scalability) incorrect programs) specs) CAV 2017 02/29/2020 The Maximum Satisfiability Problem + Efficient (and improving) solvers + Expressive for our problems Largest instance solved in MaxSAT competition: # Clauses 13.3M 10.0M 4.1M Year 8 CAV 2017 02/29/2020 The Maximum Satisfiability Problem + Efficient (and improving) solvers + Expressive for our problems

x. path(x, x) x, y, z. path(x, y) /\ edge(y, z) path(x, z) x, y. path(x, y) Cannot concisely specify our problems (lacks quantifiers) 9 Loses high-level structure that solvers could exploit CAV 2017 02/29/2020 The Maximum Satisfiability Problem + Efficient (and improving) How to overcome limitations ofsolvers MaxSAT + Expressive for our problems while retaining its benefits? x. path(x, x) x, y, z. path(x, y) /\ edge(y, z) path(x, z) x, y. path(x, y) A solution: Markov Logic Network (MLN) Cannot [Richardson & Domingos, Loses

2006] high-level concisely specify structure that our problems solvers could (lacks exploit quantifiers) 10 CAV 2017 02/29/2020 Markov Logic Network: Syntax (constraints) (hard constraints) (soft constraints) , s ::= w:h (ground fact) (input, output) (fact) (argument) Example: 11 x. path(x, x) x, y, z. path(x, y) /\ edge(y, z) path(x, z) x, y. path(x, y) CAV 2017 02/29/2020

Datalog-like Notation Input relations: edge(x, y) Output relations: Hard constraints: path(x, x). path(x, z) : path(x, y), edge(y, z). Soft constraints: path(x, y). weight path(x, y) Example: 12 x. path(x, x) x, y, z. path(x, y) /\ edge(y, z) path(x, z) x, y. path(x, y) CAV 2017 02/29/2020 Markov Logic Network: Grounding (valuation) = = = (), , ()) = () = 13 c CAV 2017

02/29/2020 Markov Logic Network: Semantics Conceptually, two steps: Step 1: Ground the MLN instance Step 2: Solve the MaxSAT instance Using off-the-shelf MaxSAT solver Challenge: both steps intractable for our problems Substitute quantifiers by all possible valuations to constants, to yield a MaxSAT instance MaxSAT instances can comprise upto 10^30 clauses! Solution: Iterative lazy refinement 14 CAV 2017 02/29/2020 Markov Logic Network: Example Input relations: edge(x, y) Output relations: path(x, y)

Hard constraints: 1 4 7 2 5 Input: edge(1, 7), edge(4, 7), 8 3 6 path(x, x). Hard path(x, z) :- path(x, y), edge(y, z).Grounding clauses: Soft constraints: edge(4, 7) path(x, y). Output: Solving Soft clauses: 15 CAV 2017

02/29/2020 Landscape of Problems Focus of this Talk INFERENCE Maximum A Posteriori (MAP) Inference LEARNING Weight Learning Structure Learning 16 Marginal Inference x. path(x, x) x, y, z. path(x, y) /\ edge(y, z) path(x, z) x, y. path(x, y) CAV 2017 02/29/2020 Talk Outline Background Part I: Applications in Software Analysis Part II: Techniques for MaxSAT Solving Conclusion

17 CAV 2017 02/29/2020 Applications in Software Analysis Abstraction Selection in Automated Verification [PLDI 2014] Input relations: edge(a, b) Output relations: path(a, b) Constraints: 1path(a, a). 2path(a, c) :- path(a, b), edge(b, c). Alarm Classification in Static Bug Detection [FSE 2015] Alarm Resolution in Interactive Verification [OOPSLA 2017] 18 CAV 2017 02/29/2020 Overview of Applications Abstraction Selection [PLDI 2014] Alarm Classification [FSE 2015] Alarm Resolution [OOSPLA 2017]

19 CAV 2017 02/29/2020 An Example: Pointer Analysis 20 f(){ v1 = new ... v2 = id1(v1) v3 = id2(v2) assert(v3 != v1) q1 } g(){ v4 = new ... v5 = id1(v4) v6 = id2(v5) assert(v6 != v1) q2 } id1(v){ return v } id2(v){ return v } CAV 2017 02/29/2020 Pointer Analysis via Graph Reachability 1 4 7 2 5 f(){ v1 = new ... v2 = id1(v1) v3 = id2(v2)

assert(v3!=v1) q1 } g(){ v4 = new ... v5 = id1(v4) v6 = id2(v5) assert(v6!=v1) q2 } id1(v){ return v } id2(v){ return v } 8 3 6 assert(v6!=v1) holds if there is no path from 1 to 6. assert(v3!=v1) holds if there is no path from 1 to 3. Analysis Writer (Alice) 21 CAV 2017 02/29/2020 Analysis Specification in Datalog Input relations: Output relations: edge(a, b) path(a, b) Constraints: path(a, a).

path(a, c) :- path(a, b), edge(b, c). If Analysis Writer (Alice) 22 there is a path from a to b, and there is an edge from b to c, then there is a path from a to c. CAV 2017 02/29/2020 Analysis Evaluation in Datalog 1 4 7 2 5 f(){ v1 = new ... v2 = id1(v1) v3 = id2(v2) assert(v3!=v1) q1 } g(){ v4 = new ... v5 = id1(v4) v6 = id2(v5) assert(v6!=v1) q2 } id1(v){ return v }

id2(v){ return v } 8 3 6 Analysis User (Bob) 23 edge(1 path(1, ,7) 1) edge(7 path(1, edge(7 ,2) 7) ,5) path(1 edge(5,8) edge(2,8) path(1, 2) ,5) edge(8 path(1 edge(8 false ,3) ,6) ,8) alar path(1, path(1, m! 3) 6) CAV 2017 02/29/2020 A More Precise Abstraction 1 7f 4 7g

7 2 8f 5 8 3 24 g(){ v4 = new ... v5 = id1(v4) v6 = id2(v5) assert(v6!=v1) q2 } id1(v){ return v } id2(v){ return v } 8g 6 Analysis User (Bob) f(){ v1 = new ... v2 = id1(v1) v3 = id2(v2) assert(v3!=v1) q1 } edge(1 path(1, ,7) 1) edge(7 path(1, edge(7 ,2) 7) ,5) path(1 edge(5,8) edge(2,8) path(1,

2) ,5) edge(8 path(1 edge(8 false ,3) ,6) ,8) alar path(1, path(1, m! 3) 6) CAV 2017 02/29/2020 A More Precise Abstraction 1 7f 4 7g 7 2 8f 5 8 3 25 g(){ v4 = new ... v5 = id1(v4) v6 = id2(v5) assert(v6!=v1) q2 } id1(v){ return v } id2(v){ return v }

8g 6 Analysis User (Bob) f(){ v1 = new ... v2 = id1(v1) v3 = id2(v2) assert(v3!=v1) q1 } edge(1, path(1, 7f) 1) edge(7f path(1, edge(7 7f) ,2) g,5) path(1 edge(5,8g edge(2,8f path(1, 2) ,5) ) ) edge(8f path(1, edge(8g false 8f) ,3) ,6) alar path(1, path(1, m! 3) 6) CAV 2017 02/29/2020 Abstraction Refinement a1 1

a0 7f b0 4 7g 7 a 1 c 1 2 a0 b0 c0 d0 8f 5 8 c1 3 c0 Input relations: Output relations: b), abs(n) path(a, b) edge(a, b) path(a, b)

Constraints: path(a, a). Constraints: abs(a 0)abs(a 1), edge(b, a). path(a, c) :- path(a, b), abs(b 0)abs(b 1), edge(b, path(a, c) :- path(a, b), c) . abs(c c, n), abs(n) . 0)abs(c1), 16 possible abs(d 0)abs(d1). b1 b1 d1 8g d0 6 d1 abstractions in total Query Tuple Original Query q1: path(1, assert(v3!=v1) 3)

q2: path(1, assert(v6!=v1) 6) 26 CAV 2017 02/29/2020 Desired Result a1 1 a0 7f b0 4 b1 7g 7 a 1 c 1 2 a0 b0 c0 d0 8f 5 b1

d1 8 c1 3 c0 8g d0 6 d1 Query Answer q1: path(1, 3) Impossibility q2: path(1, 6) a1b0c1d0 27 Input relations: Output relations: edge(a, b), abs(n) path(a, b) Constraints: abs(a0)abs(a1), path(a, a). abs(b 0)abs(b 1), edge(b, path(a, c) :- path(a,

b), abs(c c, n), abs(n) . 0)abs(c1), abs(d0)abs(d1). CAV 2017 02/29/2020 Iteration 1 a1 1 a0 7f b0 4 7g 7 a 1 c 1 2 a0 b0 c0 d0 8f 5 8

c1 3 c0 b1 b1 d1 8g d0 6 d1 Input relations: Output relations: edge(a, b), abs(n) path(a, b) Constraints: abs(a0)abs(a1), path(a, a). abs(b 0)abs(b 1), edge(b, path(a, c) :- path(a, b), abs(c c, n), abs(n) . 0)abs(c1), abs(dedge(1,7,a ). 0)abs(d a1 bs(a ) path(1,1) ) 0 0

Query q1 : path(1, 3) q2 : path(1, 6) 28 Eliminated Abstractions abs(a0) edge(7,2,a0) path(1,7) edge(7,5,b0) abs(c0) edge(2,8,c0) path(1,2) abs(c0) edge(8,3,c0) path(1,3) CAV 2017 abs(b0) path(1,5) edge(5,8,d0) abs(d0) path(1,8) edge(8,6,d0) abs(d0) path(1,6) 02/29/2020 Iteration 1 - Derivation Graph path(1,1) edge(1,7,a0) abs(a0) abs(a0edge(7,2,a ) ) edge(7,5,b0)abs(b0) 0path(1,7) abs(c0edge(2,8,c ) )

0path(1,2) path(1,5) edge(5,8,d0)abs(d0) abs(c0)edge(8,3,c0) path(1,8) edge(8,6,d0)abs(d0) path(1,3) 29 CAV 2017 path(1,6) 02/29/2020 Iteration 1 - Derivation Graph path(1,1) edge(1,7,a0) abs(a0) abs(a0edge(7,2,a ) ) edge(7,5,b0)abs(b0) 0path(1,7) abs(c0edge(2,8,c ) ) 0path(1,2) path(1,5) edge(5,8,d0)abs(d0) abs(c0)edge(8,3,c0) path(1,8) edge(8,6,d0)abs(d0) path(1,3) path(1,6) a0c0 30 CAV 2017 02/29/2020 Iteration 1 - Derivation Graph path(1,1) edge(1,7,a0) abs(a0) abs(a0edge(7,2,a

) ) edge(7,5,b0)abs(b0) 0path(1,7) abs(c0edge(2,8,c ) ) 0path(1,2) path(1,5) edge(5,8,d0)abs(d0) abs(c0)edge(8,3,c0) path(1,8) edge(8,6,d0)abs(d0) path(1,3) path(1,6) a0c0 31 CAV 2017 02/29/2020 Iteration 1 - Derivation Graph path(1,1) edge(1,7,a0) abs(a0) abs(a0edge(7,2,a ) ) edge(7,5,b0)abs(b0) 0path(1,7) abs(c0edge(2,8,c ) ) 0path(1,2) path(1,5) edge(5,8,d0)abs(d0) abs(c0)edge(8,3,c0) path(1,8) edge(8,6,d0)abs(d0) path(1,3) path(1,6) a0b0d0 32

CAV 2017 02/29/2020 Iteration 1 - Derivation Graph a1 1 a0 b0 7f 4 b1 2 a0 b0 c0 d0 8f 3 c0 Query 5 d1 abs(c0) edge(2,8,c0) path(1,2) abs(b0) path(1,5) edge(5,8,d0) abs(d0)

8g d0 6 abs(c0) d1 edge(8,3,c0) path(1,3) path(1,8) edge(8,6,d0) abs(d0) path(1,6) abs(a0)abs(a1), abs(b0)abs(b1), abs(c0)abs(c1), abs(d0)abs(d1). Eliminated Abstractions q1 : path(1, 3) a0*c0* (4/16) q2 : path(1, 6) a0*c0d0, a0b0*d0 (3/16) 33 abs(a0) abs(a0) edge(7,2,a0) path(1,7) edge(7,5,b0)

b1 8 c1 edge(1,7,a0) 7g 7 a 1 c 1 path(1,1) CAV 2017 02/29/2020 Encoding in MaxSAT path(1,1) edge(1,7,a0) abs(a0) abs(a0) edge(7,2,a0) path(1,7) edge(7,5,b0) abs(c0) edge(2,8,c0) path(1,2) abs(c0) edge(8,3,c0) path(1,3) abs(b0) path(1,5) edge(5,8,d0) abs(d0) path(1,8) edge(8,6,d0) abs(d0)

path(1,6) abs(a0)abs(a1), abs(b0)abs(b1), abs(c0)abs(c1), abs(d0)abs(d1). 34 CAV 2017 02/29/2020 Encoding in MaxSAT path(1,1) edge(1,7,a0) abs(a0) abs(a0) edge(7,2,a0) path(1,7) edge(7,5,b0) abs(c0) edge(2,8,c0) path(1,2) abs(c0) edge(8,3,c0) path(1,3) abs(b0) path(1,5) edge(5,8,d0) abs(d0) path(1,8) edge(8,6,d0) abs(d0) path(1,6) abs(a0)abs(a1), abs(b0)abs(b1), abs(c0)abs(c1), abs(d0)abs(d1).

35 CAV 2017 02/29/2020 Encoding in MaxSAT path(1,1) Avoid all the counterexam abs(a ) edge(1,7,a ) ples 0 0 abs(b0) abs(a0) edge(7,2,a0) path(1,7) edge(7,5,b0) abs(c0) edge(2,8,c0) path(1,2) abs(c0) Hard constraints: path(1,5) edge(5,8,d0) abs(d0) edge(8,6,d ) abs(d ) path(1,8) Minimize the path(1,3) abstraction path(1,6) cost edge(8,3,c0) 0 0 Soft constraints: abs(a0)abs(a1),

abs(b0)abs(b1), abs(c0)abs(c1), abs(d0)abs(d1). 36 CAV 2017 02/29/2020 Encoding in MaxSAT Solution: Hard constraints: a1c0d0 Query q1: path(1, 3) q2: path(1, 6) 37 Soft constraints: Eliminated Abstractions a0*c0* (4/16) a0*c0d0, a0b0*d0 (3/16) CAV 2017 02/29/2020 Iteration 2 and Beyond Iteratio n1 Derivation Constraint s Datalo

g solver MaxSA T solver a1c0d0 Query q1: path(1, 3) 38 q2: path(1, 6) Answer Eliminated Abstractions a0*c0* (4/16) a0*c0d0, a0b0*d0 (3/16) CAV 2017 a 02/29/2020 Iteration 2 and Beyond Iteratio n2 Derivation Constraint s Datalo g solver MaxSA

T solver a1c0d0 Query q1: path(1, 3) 39 q2: path(1, 6) Answer Eliminated Abstractions a0*c0* (4/16) a0*c0d0, a0b0*d0 (3/16) CAV 2017 a 02/29/2020 Iteration 2 and Beyond Iteratio n2 Derivation Constraint s Datalo g solver MaxSA T solver a1c0d0 Query

q1: path(1, 3) 40 q2: path(1, 6) Answer Eliminated Abstractions a0*c0* (4/16) a0*c0d0, a0b0*d0 (3/16) CAV 2017 a 02/29/2020 Iteration 2 and Beyond Iteratio n2 Derivation Constraint s Datalo g solver MaxSA T solver a1c1d0 Query q1: path(1, 3) 41 q2:

path(1, 6) Answer Eliminated Abstractions a0*c0*, a1*c0* (8/16) a0*c0d0, a0b0*d0, a1*c0d0 a (5/16) CAV 2017 02/29/2020 Iteration 2 and Beyond Iteratio n3 Derivation Constraint s Datalo g solver q2 is proven. Query q1: path(1, 3) 42 q2: path(1, 6) MaxSA T solver a1c1d0 Answer a1c1d0

Eliminated Abstractions a0*c0*, a1*c0* (8/16) a0*c0d0, a0b0*d0, a1*c0d0 a (5/16) CAV 2017 02/29/2020 Iteration 2 and Beyond Iteratio n3 Derivation Constraint s Datalo g solver q2 is proven. Query q1: path(1, 3) 43 q2: path(1, 6) MaxSA T solver a1c1d0 Answer a1c1d0 Eliminated Abstractions

a0*c0*, a1*c0* (8/16) a0*c0d0, a0b0*d0, a1*c0d0 a (5/16) CAV 2017 02/29/2020 Iteration 2 and Beyond Iteratio n3 Derivation Constraint s Datalo g solver q2 is proven. Query q1: path(1, 3) 44 q2: path(1, 6) MaxSA T solver a1c1d0 Answer q1 is impossible to prove. Eliminated Abstractions

Impossibil a0*c0*, a1*c0*, a0*c1*, a1*c1* ity (16/16) a1c1d0 a0*c0d0, a0b0*d0, a1*c0d0 a (5/16) CAV 2017 02/29/2020 Mixing Counterexamples Iteration 1 Eliminate d Abstracti ons: 45 Iteration 3 a0c0 a1c1 CAV 2017 02/29/2020 Mixing Counterexamples Iteration 1 Eliminate d Abstracti ons: 46 a0c0 Mixed! a0c1 CAV 2017

Iteration 3 a1c1 02/29/2020 Experimental Setup Implemented using off-the-shelf solvers Datalog: bddbddb MaxSAT: MiFuMaX Applied to two analyses that are challenging to scale k-object-sensitive pointer analysis flow-insensitive, weak updates, cloning-based 76 rules, 50 input relations, 42 type-state analysis output relations flow-sensitive, strong updates, summary-based 52 rules, 33 input relations, 14 output relations

Evaluated on 8 Java programs (250-450 KLOC each) 47 CAV 2017 02/29/2020 Pointer Analysis Results 4-objectsensitivity < 50% queries abstractio n size resolved total toba-s curre nt baseli fina ne l max < 3% of max iteratio ns 7 7 0 170 18K 10 javasrc-p

46 46 0 470 18K 13 weblech 5 5 2 140 31K 10 hedc 47 47 6 730 29K 18 antlr 143 143

5 970 29K 15 luindex 138 138 67 1K 40K 26 lusearch 322 322 29 1K 39K 17 51 51 25 450 58K

15 schroederm48 CAV 2017 02/29/2020 Performance of Datalog Solver Baselin e k = 4, 3h28m k = 3, 590s lusearch k = 2, k =214s 1, 153s 49 CAV 2017 02/29/2020 Performance of MaxSAT Solver lusearch 50 CAV 2017 02/29/2020 Statistics of MaxSAT Formulae pointer analysis 51

variabl es clauses toba-s 0.7M 1.5M javasrc-p 0.5M 0.9M weblech 1.6M 3.3M hedc 1.2M 2.7M antlr 3.6M 6.9M luindex 2.4M 5.6M lusearch 2.1M 5.0M

schroederm 6.7M 23.7M CAV 2017 02/29/2020 Overview of Applications Abstraction Selection [PLDI 2014] Alarm Classification [FSE 2015] Alarm Resolution [OOSPLA 2017] 52 CAV 2017 02/29/2020 How Do We Go From This Detected Races R1: Race on eld org.apache.ftpserver.RequestHandler.m_request org.apache.ftpserver.RequestHandler: 9 org.apache.ftpserver.RequestHandler: 18 R2: Race on eld org.apache.ftpserver.RequestHandler.m_request org.apache.ftpserver.RequestHandler: 17 org.apache.ftpserver.RequestHandler: 18 R3: Race on eld org.apache.ftpserver.RequestHandler.m_writer org.apache.ftpserver.RequestHandler: 19

org.apache.ftpserver.RequestHandler: 20 R4: Race on eld org.apache.ftpserver.RequestHandler.m_reader org.apache.ftpserver.RequestHandler: 21 org.apache.ftpserver.RequestHandler: 22 R5: Race on eld org.apache.ftpserver.RequestHandler.m_controlSocket org.apache.ftpserver.RequestHandler: 23 org.apache.ftpserver.RequestHandler: 24 Eliminated Races E1: Race on eld org.apache.ftpserver.RequestHandler. m_isConnectionClosed org.apache.ftpserver.RequestHandler: 13 53 org.apache.ftpserver.RequestHandler: 15 CAV 2017 02/29/2020 To This? Detected Races R1: Race on eld org.apache.ftpserver.RequestHandler.m_request org.apache.ftpserver.RequestHandler: 9 org.apache.ftpserver.RequestHandler: 18 R2: Race on eld org.apache.ftpserver.RequestHandler.m_request org.apache.ftpserver.RequestHandler: 17 org.apache.ftpserver.RequestHandler: 18 R3: Race on eld org.apache.ftpserver.RequestHandler.m_writer org.apache.ftpserver.RequestHandler: 19 org.apache.ftpserver.RequestHandler: 20 R4: Race on eld org.apache.ftpserver.RequestHandler.m_reader org.apache.ftpserver.RequestHandler: 21 org.apache.ftpserver.RequestHandler: 22

R5: Race on eld org.apache.ftpserver.RequestHandler.m_controlSocket org.apache.ftpserver.RequestHandler: 23 org.apache.ftpserver.RequestHandler: 24 Eliminated Races E1: Race on eld org.apache.ftpserver.RequestHandler. m_isConnectionClosed org.apache.ftpserver.RequestHandler: 13 54 org.apache.ftpserver.RequestHandler: 15 CAV 2017 02/29/2020 To This? Detected Races R1: Race on eld org.apache.ftpserver.RequestHandler.m_request org.apache.ftpserver.RequestHandler: 9 org.apache.ftpserver.RequestHandler: 18 Eliminated Races E1: Race on eld org.apache.ftpserver.RequestHandler. m_isConnectionClosed org.apache.ftpserver.RequestHandler: 13 org.apache.ftpserver.RequestHandler: 15 E2: Race on eld org.apache.ftpserver.RequestHandler.m_request org.apache.ftpserver.RequestHandler: 17 org.apache.ftpserver.RequestHandler: 18 E3: Race on eld org.apache.ftpserver.RequestHandler.m_writer org.apache.ftpserver.RequestHandler: 19 org.apache.ftpserver.RequestHandler: 20 E4: Race on eld org.apache.ftpserver.RequestHandler.m_reader org.apache.ftpserver.RequestHandler: 21 org.apache.ftpserver.RequestHandler: 22 E5: Race on eld org.apache.ftpserver.RequestHandler.m_controlSocket

org.apache.ftpserver.RequestHandler: 23 55 org.apache.ftpserver.RequestHandler: 24 CAV 2017 02/29/2020 An Example: Static Datarace Analysis Input relations: next(p1, p2), mayAlias(p1, p2), guarded(p1, p2) Output relations: parallel(p1, p2), race(p1, p2) Constraints: parallel(p3, p2) :- parallel(p1, p2), next(p3, p1). (2) parallel(p1, p2) :- parallel(p2, p1). race(p1, p2) :- parallel(p1, p2), mayAlias(p1, p2), guarded(p1, p2). 56 CAV 2017 02/29/2020 An Example: Static Datarace Analysis program point p1 is immediate successor of p2. Input relations: p1 & p2 may access the same memory location. & p2 are next(p1, p2), mayAlias(p1, p2), guarded(p1,p1 p2) guarded by the p1 & p2 may If p1 & p2 may happen

same lock. in happen in Output relations: parallel, parallel. parallel(p1, p2), race(p1, p2) and p3 is successor of p1, then p1 & p2 may p3 & p2 may happen in Constraints: have a datarace. parallel. parallel(p3, p2) :- parallel(p1, p2), next(p3, If p2 & p1 mayp1). happen in parallel, (2) parallel(p1, p2) :- parallel(p2, p1). then p1 & p2 may happen in parallel. race(p1, p2) :- parallel(p1, p2), mayAlias(p1, p2), guarded(p1, Ifp2). p1 & p2 may happen in parallel, and they may access the same memory location, and they are not guarded by the same lock, then p1 & p2 may have a datarace. 57 CAV 2017 02/29/2020 An Example: Static Datarace Analysis Input relations: next(p1, p2), mayAlias(p1, p2), guarded(p1, p2) Output relations: a = 1; parallel(p1, p2), race(p1, if (a p2) > 2) { // p1 ... // p3

} Soft Rule Constraints: parallel(p3, p2) :- parallel(p1, p2), next(p3, weightp1). 5 (2) parallel(p1, p2) :- parallel(p2, p1). race(p1, p2) :- parallel(p1, p2), mayAlias(p1, p2), guarded(p1, p2). Hard Rule weight 25 race(x2, x1). 58 CAV 2017 02/29/2020 An Example: Static Datarace Analysis 1 public class RequestHandler { 2 3 4 5 6 7 Request request; FtpWriter writer; BufferedReader reader; Socket controlSocket; boolean isConnectionClosed; 8 public Request getRequest() { 9 return request; 10 } 11 public void close() { 12 synchronized (this) { 13 if (isClosed)

14 15 16 return; isClosed = true; } 17 request.clear(); 18 request = null; 19 writer.close(); 20 writer = null; 21 reader.close(); 22 reader = null; 23 controlSocket.close(); 24 controlSocket = null; 25 } Source code snippet from Apache FTP Server 59 CAV 2017 02/29/2020 An Example: Static Datarace Analysis 11 public void close() { 12 synchronized (this) { 13 if (isClosed) 1 public class RequestHandler { 2 3 4 5 6 7 Request request; FtpWriter writer; BufferedReader reader; Socket controlSocket; boolean isConnectionClosed; 14

15 16 R1 8 public Request getRequest() { 9 return request; 10 } return; isClosed = true; } 17 request.clear(); 18 request = null; 19 writer.close(); 20 writer = null; 21 reader.close(); 22 reader = null; 23 controlSocket.close(); 24 controlSocket = null; 25 } Source code snippet from Apache FTP Server 60 CAV 2017 02/29/2020 An Example: Static Datarace Analysis 1 public class RequestHandler { 2 3 4 5 6 7 Request request; FtpWriter writer; BufferedReader reader; Socket controlSocket; boolean isConnectionClosed;

8 public Request getRequest() { 9 return request; 10 } 11 public void close() { 12 synchronized (this) { 13 if (isClosed) 14 15 16 return; isClosed = true; } 17 request.clear(); 18 request = null; 19 writer.close(); 20 writer = null; 21 reader.close(); 22 reader = null; 23 controlSocket.close(); 24 controlSocket = null; 25 } R2 R3 R4 R5 Source code snippet from Apache FTP Server 61 CAV 2017 02/29/2020 How Does Generalization Work? 17 18 request = null; // x2 19

writer.close(); // y1 20 writer = null; // y2 guarded(x2 mayAias(x2, , x1) x1) race(x2, x1) race(x2, x1) weight 25 parallel(p3, p2) :- parallel(p1, p2), next (p3, p1). weight 5 race(p1, p2) :- parallel(p1, p2), mayAlias(p1, p2), guarded(p1, p2). parallel(x2 ,x1) parallel(x1 ,x2) next(y1, x2) next(y1, x2) parallel(p1, p2) :- parallel(p2, p1). 62 parallel(x1 ,x1) next(x2, x1) request.clear();// x1

CAV 2017 parallel(x2 ,x2) parallel(y1 ,x2) parallel(x2 ,y1) parallel(y1 ,y1) mayAias(y2, y1) next(x2, x1) next(y2, y1) parallel(y2 ,y1) race(y2, y1) guarded(y2 , y1) 02/29/2020 How Does Generalization Work? 17 18 request = null; // x2 19 writer.close(); // y1 20 writer = null; // y2

guarded(x2 mayAias(x2, , x1) x1) race(x2, x1) race(x2, x1) weight 25 parallel(p3, p2) :- parallel(p1, p2), next (p3, p1). weight 5 race(p1, p2) :- parallel(p1, p2), mayAlias(p1, p2), guarded(p1, p2). parallel(x2 ,x1) parallel(x1 ,x2) next(y1, x2) next(y1, x2) parallel(p1, p2) :- parallel(p2, p1). 63 parallel(x1 ,x1) next(x2, x1) request.clear();// x1 CAV 2017 parallel(x2 ,x2)

parallel(y1 ,x2) parallel(x2 ,y1) parallel(y1 ,y1) mayAias(y2, y1) next(x2, x1) next(y2, y1) parallel(y2 ,y1) race(y2, y1) guarded(y2 , y1) 02/29/2020 How Does Generalization Work? 17 18 request = null; // x2 19 writer.close(); // y1 20 writer = null; // y2 guarded(x2 mayAias(x2, , x1) x1) race(x2, x1)

race(x2, x1) weight 25 parallel(p3, p2) :- parallel(p1, p2), next (p3, p1). weight 5 race(p1, p2) :- parallel(p1, p2), mayAlias(p1, p2), guarded(p1, p2). parallel(x2 ,x1) parallel(x1 ,x2) next(y1, x2) next(y1, x2) parallel(p1, p2) :- parallel(p2, p1). 64 parallel(x1 ,x1) next(x2, x1) request.clear();// x1 CAV 2017 parallel(x2 ,x2) parallel(y1 ,x2) parallel(x2 ,y1) parallel(y1

,y1) mayAias(y2, y1) next(x2, x1) next(y2, y1) parallel(y2 ,y1) race(y2, y1) guarded(y2 , y1) 02/29/2020 How Does Generalization Work? 17 18 request = null; // x2 19 writer.close(); // y1 20 writer = null; // y2 guarded(x2 mayAias(x2, , x1) x1) race(x2, x1) race(x2, x1) weight 25 parallel(p3, p2) :- parallel(p1, p2), next (p3, p1). weight

5 race(p1, p2) :- parallel(p1, p2), mayAlias(p1, p2), guarded(p1, p2). parallel(x2 ,x1) parallel(x1 ,x2) next(y1, x2) next(y1, x2) parallel(p1, p2) :- parallel(p2, p1). 65 parallel(x1 ,x1) next(x2, x1) request.clear();// x1 CAV 2017 parallel(x2 ,x2) parallel(y1 ,x2) parallel(x2 ,y1) parallel(y1 ,y1) mayAias(y2, y1) next(x2, x1)

next(y2, y1) parallel(y2 ,y1) race(y2, y1) guarded(y2 , y1) 02/29/2020 Accuracy of Alarm Classification 100% 338 700 feedback on 5% 324 reports 119 111 1824 153 79 183 0 10 2597 80% 60% 40% 20% 0% avrora ftp hedc false reports eliminated 66

CAV 2017 luindex lusearch weblech true reports retained 02/29/2020 Accuracy of Alarm Classification 100% 338 700 feedback on 5% 324 reports 119 111 1824 153 79 183 0 10 2597 80% With 60% only up to 5% feedback, 70% of the false positives are eliminated and 96% of true positives retained. 40% 20% 0% avrora ftp hedc false reports eliminated 67 CAV 2017

luindex lusearch weblech true reports retained 02/29/2020 Impact of Varying Amount of Feedback 338 false and 700 true reports 100% 80% 60% 40% 20% 0% 5% 10% false reports eliminated 68 CAV 2017 15% 20% true reports retained 02/29/2020 Overview of Applications Abstraction Selection [PLDI 2014] Alarm Classification [FSE 2015] Alarm Resolution [OOSPLA 2017]

69 CAV 2017 02/29/2020 Example Revisited: Static Datarace Analysis 1 public class RequestHandler { 2 3 4 5 6 7 Request request; Can this statement be FtpWriter writer; executed different BufferedReaderby reader; Socket controlSocket; threads in parallel? boolean isConnectionClosed; 8 public Request getRequest() { 9 return request; 10 } 11 public void close() { 12 synchronized (this) { 13 if (isClosed) 14 15 16 return; isClosed = true; }

17 request.clear(); 18 request = null; 19 writer.close(); 20 writer = null; 21 reader.close(); 22 reader = null; 23 controlSocket.close(); 24 controlSocket = null; 25 } Source code snippet from Apache FTP Server 70 CAV 2017 02/29/2020 Illustration: Space of Questions 17 18 request = null; // x2 19 writer.close(); // y1 20 writer = null; // y2 guarded(x2 mayAias(x2, , x1) x1) race(x2, x1) parallel(p3, p2) :- parallel(p1, p2), next (p3, p1). parallel(p1, p2) :- parallel(p2, p1). race(p1, p2) :- parallel(p1, p2), mayAlias(p1, p2), guarded(p1, p2).

71 parallel(x1 ,x1) next(x2, x1) request.clear();// x1 parallel(x2 ,x1) parallel(x1 ,x2) next(y1, x2) next(y1, x2) CAV 2017 parallel(x2 ,x2) parallel(y1 ,x2) parallel(x2 ,y1) parallel(y1 ,y1) mayAias(y2, y1) next(x2, x1) next(y2, y1) parallel(y2 ,y1)

race(y2, y1) guarded(y2 , y1) 02/29/2020 Illustration: Space of Questions 17 18 request = null; // x2 19 writer.close(); // y1 20 writer = null; // y2 guarded(x2 mayAias(x2, , x1) x1) race(x2, x1) parallel(p3, p2) :- parallel(p1, p2), next (p3, p1). parallel(p1, p2) :- parallel(p2, p1). race(p1, p2) :- parallel(p1, p2), mayAlias(p1, p2), guarded(p1, p2). 72 parallel(x1 ,x1) next(x2, x1)

request.clear();// x1 parallel(x2 ,x1) parallel(x1 ,x2) next(y1, x2) next(y1, x2) CAV 2017 parallel(x2 ,x2) parallel(y1 ,x2) parallel(x2 ,y1) parallel(y1 ,y1) mayAias(y2, y1) next(x2, x1) next(y2, y1) parallel(y2 ,y1) race(y2, y1) guarded(y2 , y1) 02/29/2020 Illustration: Space of Questions

17 18 request = null; // x2 19 writer.close(); // y1 20 writer = null; // y2 guarded(x2 mayAias(x2, , x1) x1) race(x2, x1) parallel(p3, p2) :- parallel(p1, p2), next (p3, p1). parallel(p1, p2) :- parallel(p2, p1). race(p1, p2) :- parallel(p1, p2), mayAlias(p1, p2), guarded(p1, p2). 73 parallel(x1 ,x1) next(x2, x1) request.clear();// x1 parallel(x2 ,x1) parallel(x1 ,x2) next(y1, x2)

next(y1, x2) CAV 2017 parallel(x2 ,x2) parallel(y1 ,x2) parallel(x2 ,y1) parallel(y1 ,y1) mayAias(y2, y1) next(x2, x1) next(y2, y1) parallel(y2 ,y1) race(y2, y1) guarded(y2 , y1) 02/29/2020 Two Key Objectives Generalization Number of Questions << Number of Alarms Resolved

Prioritization 74 Prioritize Questions Likely to Resolve the Most Alarms CAV 2017 02/29/2020 Illustration: Payoff Comparison 17 18 request = null; // x2 19 writer.close(); // y1 20 writer = null; // y2 guarded(x2 mayAlias(x2 , x1) ,x1) Rx Alarms Resolved { parallel(x1, x1) } { Rx, Ry } { parallel(y1, y1) }

{ Ry } 75 race(x2, x1) parallel(x2 ,x1) next(y1, x2) CAV 2017 parallel(x2 ,x2) parallel(y1 ,x2) parallel(x2 ,y1) parallel(y1 ,y1) mayAlias(y2 ,y1) next(x2, x1) parallel(x1 ,x2) next(y1, x2) Questions Asked { mayAlias(y2, y1) } parallel(x1 ,x1)

next(x2, x1) request.clear();// x1 next(y2, y1) parallel(y2 ,y1) race(y2, y1) guarded(y2 , y1) Ry 02/29/2020 Highlights of Overall Approach Iterative: leverages labels of past questions in choosing future questions Maximizes the expected payoff in each iteration Non-linear optimization objective Payoff = # Alarms Resolved / # Questions Asked Binary search on payoff by solving sequence of MaxSAT instances Data-driven: leverages heuristics to guess likely labels 76

Static, Dynamic, Aggregated CAV 2017 02/29/2020 Empirical Results: Generalization total false and true reports 22 18 10000% 6 5 64 0 100 0 214 50 594 317 ftp hedc 8000% 6000% 4000% 2000% 0% raytracer sor elevator jspider questions asked 77 alarms resolved CAV 2017

02/29/2020 Empirical Results: Generalization total false and true reports 22 18 10000% 6 5 64 0 100 0 214 50 594 317 8000% 6000% With only up to 5% questions, 74% of the false alarms are resolved with average payoff of 12X per question. 4000% 2000% 0% raytracer sor elevator jspider questions asked 78 ftp hedc alarms resolved CAV 2017

02/29/2020 Empirical Results: Prioritization 75 raytracer 100 sor 45 30 15 750 jspider 80 40 79 125 ftp 450 300 0 1 2 3 4 # questions 5 hedc 100

150 5 10 15 20 25 # questions 40 0 5 # alarms 120 0 1 2 3 4 # questions 600 # alarms # alarms 160 60 20 0 200 elevator 80 # alarms # alarms 60

75 50 25 4 8 12 16 20 # questions CAV 2017 0 5 10 15 20 25 # questions 02/29/2020 Empirical Results: Prioritization 75 raytracer 100 sor elevator 80 # alarms # alarms 60 45 30 15 60 40 20 0 1 2

3 4 # questions 0 5 1 2 3 4 # questions Earlier iterations yield higher payoffs and match the performance of the ideal setting. 750 200 600 120 80 40 80 450 300 150 5 10 15 20 25 # questions 0 hedc 100 # alarms # alarms # alarms 160

0 125 ftp jspider 5 75 50 25 4 8 12 16 20 # questions CAV 2017 0 5 10 15 20 25 # questions 02/29/2020 Summary: Applications in Software Analysis Automated Verification [PLDI14] Static Bug Detection [FSE15] Interactive Verification [OOPSLA17] 81 Hard Constraints analysis rules

abstraction1 abstractionn analysis rules analysis rules CAV 2017 Soft Constraints resulti weight query resolution wi award abstraction j abstraction weight wcost j analysis rulei weight confidence wiof writer resultj weight confidence wj of user causei cost weight of inspection w i resultj weight reward ofwresolution j 02/29/2020 Other Applications Statistical Relational Learning wrote(p, wrote(p, t)

t) ::- advisedBy(s, advisedBy(s, p), p), wrote(s, wrote(s, t). t). weight weight 3 3 p == q :advisedBy(s, p), advisedBy(s, q). weight p == q :- advisedBy(s, p), advisedBy(s, q). weight 5 5 professor(p) weight professor(p) ::- advisedBy(_, advisedBy(_, p). p). Given constraints weight 20 20 and wrote("Tom", "paper1"). wrote("Tom", "paper1"). facts, wrote("Tom", wrote("Tom", "paper2"). "paper2"). wrote("Jerry", find most likely wrote("Jerry", "paper1"). "paper1"). wrote("Chuck", wrote("Chuck", "paper2"). "paper2"). answer to: professor("Jerry"). professor("Jerry"). advisedBy("Tom", advisedBy("Tom", ?) ?)

Mathematical Programming totalShelf totalShelf [] [] += += stock[p] stock[p] * * space space [p] [p] totalProfit[] totalProfit[] += += stock[p] stock[p] * * profit[p] profit[p] product(p) >= product(p) -> -> stock[p] stock[p] >= minStock[p] minStock[p] product(p) <= product(p) -> -> stock[p] stock[p] <= maxStock[p] maxStock[p] true -> true -> totalShelf[] totalShelf[] <= <= maxShelf[] maxShelf[] lang:solve:variable(`stock) lang:solve:variable(`stock) lang:solve:max(`totalProfit) lang:solve:max(`totalProfit) 82 CAV 2017

02/29/2020 Talk Outline Background Part I: Applications in Software Analysis Part II: Techniques for MaxSAT Solving Conclusion 83 CAV 2017 02/29/2020 The Inference Problem Input relations: edge(x, y) Markov Logic Network Output relations: path(x, y) Hard constraints: path(x, x). path(x, z) :- path(x, y), edge(y, z). Solver Soft constraints: path(x, y). weight Scalability Soundness Optimality 1.5 Existing Solvers Tuffy [VLDB11] Alchemy [ML06]

CPI [UAI08] RockIt [AAAI13] Z3 [TACAS08] 84 CAV 2017 02/29/2020 Overview of Techniques General Framework [SAT 2015] Bottom-Up Solving [AAAI 2016] Top-Down Solving [POPL 2016] 85 CAV 2017 02/29/2020 Framework Architecture MLN instance work set candidate solution MaxSA T Solver Yes Checke r No

sound & optimal solution expanded work set 86 CAV 2017 02/29/2020 Framework Instances MLN instance work set candidate solution MaxSA T Solver Yes Checke r No Datalog SQL MaxSAT ILP SMT sound & optimal solution expanded work set 87 CAV 2017

02/29/2020 Framework Instance: Abstraction Refinement MLN instance work set candidate solution MaxSA T Solver Yes Checke r No Datalog SQL MaxSAT ILP SMT sound & optimal solution expanded work set On Abstraction Refinement for Program Analyses in Datalog [PLDI 2014] 88 CAV 2017 02/29/2020 Framework Instance: Bottom-Up Solving MLN instance work set candidate solution

MaxSA T Solver Yes Checke r No Datalog SQL MaxSAT ILP SMT sound & optimal solution expanded work set Scaling Relational Inference Using Proofs and Refutations [AAAI 2016] 89 CAV 2017 02/29/2020 Framework Instance: Top-Down Solving MLN instance work set candidate solution MaxSA T Solver Yes Checke

r No Datalog SQL MaxSAT ILP SMT sound & optimal solution expanded work set Query-Guided Maximum Satisfiability [POPL 2016] 90 CAV 2017 02/29/2020 Overview of Techniques General Framework [SAT 2015] Bottom-Up Solving [AAAI 2016] Top-Down Solving [POPL 2016] 91 CAV 2017 02/29/2020 Bottom-Up Solving Follows cutting-plane method [Riedl09] with three

new insights for better scalability on our applications: 1. Exploits high-level structure of MLN to efficiently find new ground constraints violated current solution. 2. Accelerates convergence by eagerly grounding Horn constraints using Datalog solver. 3. Terminates earlier by checking objective value (rather than set of violated soft constraints) for saturation. 92 CAV 2017 02/29/2020 Example Input relations: edge(x, y) Output relations: path(x, y) Hard constraints: path(x, x). path(x, z) :- path(x, y), edge(y, z). Soft constraints: path(x, y). weight 1.5 edge(c1,c2) path(c1,c2) 93 CAV 2017 02/29/2020 Example: Iteration 1 - Solve Input relations: edge(x, y) Output relations: path(x, y) Hard constraints: path(x, x). path(x, z) :- path(x, y), edge(y, z). Soft constraints:

path(x, y). weight 1.5 94 Hard clauses: Soft clauses: CAV 2017 02/29/2020 Example: Iteration 1 - Check Input relations: edge(x, y) Output relations: path(x, y) Hard constraints: path(x, x). path(x, z) :- path(x, y), edge(y, z). Soft constraints: path(x, y). weight 1.5 95 Hard clauses: Soft clauses: CAV 2017 02/29/2020 Example: Iteration 2 - Solve Input relations: edge(x, y) Output relations: path(x, y) Hard constraints: path(x, x). path(x, z) :- path(x, y), edge(y, z). Soft constraints: path(x, y). weight 1.5

96 Hard clauses: Soft clauses: CAV 2017 02/29/2020 Example: Iteration 2 - Check Input relations: edge(x, y) Output relations: path(x, y) Hard constraints: path(x, x). path(x, z) :- path(x, y), edge(y, z). Soft constraints: path(x, y). weight 1.5 97 Hard clauses: Soft clauses: CAV 2017 02/29/2020 Example: Iteration 3 - Solve Input relations: edge(x, y) Output relations: path(x, y) Hard constraints: path(x, x). path(x, z) :- path(x, y), edge(y, z). Soft constraints: path(x, y). weight 1.5

98 Hard clauses: ... Soft clauses: ) ... ) CAV 2017 02/29/2020 Example: Iteration 3 - Check Input relations: edge(x, y) Output relations: path(x, y) Hard constraints: path(x, x). path(x, z) :- path(x, y), edge(y, z). Soft constraints: path(x, y). weight 1.5 99 Hard clauses: ... Soft clauses: ) ... ) CAV 2017 02/29/2020 Example: Iteration 4 - Solve Input relations:

edge(x, y) Output relations: path(x, y) Hard constraints: path(x, x). path(x, z) :- path(x, y), edge(y, z). Soft constraints: path(x, y). weight 1.5 Hard clauses: ... ... Soft clauses: ) ... ) ) ... ) 100 CAV 2017 02/29/2020 Example: Iteration 4 - Check Input relations: edge(x, y) Output relations: path(x, y) Hard constraints: path(x, x). path(x, z) :- path(x, y), edge(y, z). Soft constraints: path(x, y). weight 1.5 Hard clauses: ...

... Soft clauses: ) ... ) ) ... ) 101 CAV 2017 02/29/2020 Example: Iteration 5 - Solve Input relations: edge(x, y) Output relations: path(x, y) Hard constraints: path(x, x). path(x, z) :- path(x, y), edge(y, z). Soft constraints: path(x, y). weight 1.5 Hard clauses: ... ... Soft clauses: ) ... ) ) ... )) ... ) 102

CAV 2017 02/29/2020 Example: Iteration 5 - Check 1) All hard constraints are Input relations: satisfied y) violated soft 2)edge(x, No new Output relations: constraints path(x, y) => sound to terminate Hard constraints: path(x, x). path(x, z) :- path(x, y), edge(y, z). Soft constraints: path(x, y). weight 1.5 Hard clauses: ... ... Soft clauses: ) ... ) ) ... )) ... ) 103 CAV 2017 02/29/2020

Horn-Guided Optimization Input relations: edge(x, y) Output relations: path(x, y) Hard constraints: path(x, x). Horn path(x, z) :-Rules! path(x, y), edge(y, z). Soft constraints: path(x, y). weight 1.5 104 Preprocess hard Horn rules CAV 2017 02/29/2020 Horn-Guided Optimization 1) All hard constraints are Input relations: satisfied y) violated soft 2)edge(x, No new Output relations: constraints path(x, y) => sound to terminate Hard constraints: Hard clauses: Soft clauses: path(x, x). path(x, z) :- path(x, y), edge(y, z). Soft constraints: path(x, y). weight

1.5 105 ) ... ) ) ... ) ) ... ) CAV 2017 02/29/2020 Performance Evaluation total # ground clauses avrora 1.8 x 1026 ftp 3.7 x 1023 hedc 1.9 x 1024 luinde 1.6 x x 1025 lusearc 1.7 x h 1025 weblec 4.4 x h 1024 106 #

iterations Lazy Guid ed 492 12 463 5 354 total time (hours : mins) Guide Lazy d # ground clauses Lazy Guide d 0.8M 1.6M 1.2M 1.4M 6:31 0:25 7:53 0:08

6 1:55 0:06 0.8M 0.9M 481 7 4:07 0:12 0.6M 1.1M 429 6 2:38 0:14 0.6M 1.0M 416 6 1:59 0:07 0.6M 0.9M

CAV 2017 02/29/2020 Overview of Techniques General Framework [SAT 2015] Bottom-Up Solving [AAAI 2016] Top-Down Solving [POPL 2016] 107 CAV 2017 02/29/2020 Queries in Different Domains Program Reasoning: Information Retrieval: Does variable head alias with variable tail on line 50 in Complex.java? 108 CAV 2017 Is Dijkstra most likely an author of Structured Programming? 02/29/2020 Queries in MaxSAT 4

2 7 (C1) (C2) (C3) (C4) (C5) QUERIES = {a, d} 109 CAV 2017 02/29/2020 Query-Guided Maximum Satisfiability (Q-MaxSAT) 4 2 7 (C1) (C2) (C3) (C4) (C5) Q-MaxSAT: Given a MaxSAT formula and a set of queries , a solution to the Q-MaxSAT instance is a partial solution such that QUERIES = {a, d} 110 CAV 2017 02/29/2020 Query-Guided Maximum Satisfiability (Q-MaxSAT)

4 2 7 (C1) (C2) (C3) (C4) (C5) Q-MaxSAT: Given a MaxSAT formula and a set of queries , a solution to the Q-MaxSAT instance is a partial solution such that QUERIES = {a, d} Solution: a = true, d = false 111 CAV 2017 02/29/2020 Query-Guided Maximum Satisfiability (Q-MaxSAT) 4 2 7 (C1) (C2) (C3) (C4) (C5) Q-MaxSAT: Given a MaxSAT formula and a set of queries , a solution to the Q-MaxSAT instance is a partial solution such that QUERIES = {a, d} MaxSAT Solution: a = true, b = true, c =

true, d = false 112 CAV 2017 02/29/2020 Our key idea: Use a small set of clauses to succinctly summarize effect of unexplored clauses 113 CAV 2017 02/29/2020 Example Queries = {v6}, formula = v4 weight 100 v8 weight 100 v7 weight 100 v3 v1 weight 5 v5 v2 weight 5 v5 v3 weight 5 v6 v5 weight 5 v6 v7 weight 5 v4 v6 weight 5

v8 v6 weight 5 ... 114 CAV 2017 02/29/2020 Example Queries = {v6}, formula = v4 weight 100 v8 weight 100 v7 weight 100 v3 v1 weight 5 v5 v2 weight 5 v5 v3 weight 5 v6 v5 weight 5 v6 v7 weight 5 v4 v6 weight 5 v8 v6 weight 5 ... 115 CAV 2017

02/29/2020 Example Queries = {v6}, formula = v4 weight 100 v8 weight 100 v7 weight 100 v3 v1 weight 5 v5 v2 weight 5 v5 v3 weight 5 v6 v5 weight 5 v6 v7 weight 5 v4 v6 weight 5 v8 v6 weight 5 ... 116 CAV 2017 02/29/2020 Example Queries = {v6}, formula = v4 weight 100

v8 weight 100 v7 weight 100 v3 v1 weight 5 v5 v2 weight 5 v5 v3 weight 5 v6 v5 weight 5 v6 v7 weight 5 v4 v6 weight 5 v8 v6 weight 5 ... 117 CAV 2017 02/29/2020 Example Queries = {v6}, formula = v4 weight 100 v8 weight 100 v7 weight 100 v3 v1 weight 5 v5 v2

weight 5 v5 v3 weight 5 v6 v5 weight 5 v6 v7 weight 5 v4 v6 weight 5 v8 v6 weight 5 ... 118 CAV 2017 02/29/2020 Example Queries = {v6}, formula = v4 weight 100 v8 weight 100 v7 weight 100 v3 v1 weight 5 v5 v2 weight 5 v5 v3 weight 5 v6 v5 weight 5

v6 v7 weight 5 v4 v6 weight 5 v8 v6 weight 5 ... 119 CAV 2017 02/29/2020 Example Queries = {v6}, formula = v4 weight 100 v8 weight 100 v7 weight 100 v3 v1 weight 5 v5 v2 weight 5 v5 v3 weight 5 v6 v5 weight 5 v6 v7 weight 5 v4 v6 weight 5 v8 v6 weight 5

... 120 CAV 2017 02/29/2020 Example: Iteration 1 Queries = {v6}, formula = v4 weight 100 v8 weight 100 v7 weight 100 v3 v1 weight 5 workSe v5 v2 weight 5 t v5 v3 weight 5 v6 v5 weight 5 v6 v7 weight 5 v4 v6 weight 5 v8 v6 weight 5 ... 121 CAV 2017

02/29/2020 Example: Iteration 1 (blue = true, red = false) Queries = {v6}, formula = v4 weight 100 v8 weight 100 v7 weight 100 v3 v1 weight 5 workSe v5 v2 weight 5 t v5 v3 weight 5 v6 v5 weight 5 v6 v7 weight 5 v4 v6 weight 5 v8 v6 weight 5 ... 122 CAV 2017 02/29/2020 Example: Iteration 1 (blue = true, red = false) = {v6}, ? Queries formula =

workSe t 123 CAV 2017 v4 v8 v7 v3 v5 v5 v6 v6 v4 v8 ... v1 v2 v3 v5 v7 v6 v6 weight 100 weight 100 weight 100 weight 5 weight 5 weight 5 weight 5

weight 5 weight 5 weight 5 02/29/2020 Example: Iteration 1 (blue = true, red = false) = {v6}, ? Queries formula = workSe t frontie rs 124 CAV 2017 v4 v8 v7 v3 v5 v5 v6 v6 v4 v8 ... v1 v2 v3

v5 v7 v6 v6 weight 100 weight 100 weight 100 weight 5 weight 5 weight 5 weight 5 weight 5 weight 5 weight 5 02/29/2020 Example: Iteration 1 (blue = true, red = false) = {v6}, ? Queries formula = workSe t frontie rs 125 CAV 2017 v4 v8 v7 v3 v5 v5 v6

v6 v4 v8 ... v1 v2 v3 v5 v7 v6 v6 weight 100 weight 100 weight 100 weight 5 weight 5 weight 5 weight 5 weight 5 weight 5 weight 5 02/29/2020 Example: Iteration 1 (blue = true, red = false) = {v6}, ? Queries formula =

workSe t frontie rs summarySet = {(100, v4), (100, v8)} 126 CAV 2017 v4 v8 v7 v3 v5 v5 v6 v6 v4 v8 ... v1 v2 v3 v5 v7 v6 v6 weight 100 weight 100 weight 100 weight 5

weight 5 weight 5 weight 5 weight 5 weight 5 weight 5 02/29/2020 Example: Iteration 1 (blue = true, red = false) Queries = {v6}, formula = v4 weight 100 v8 weight 100 v7 weight 100 v3 v1 weight 5 workSe v5 v2 weight 5 t v5 v3 weight 5 frontie v6 v5 weight 5 rs v6 v7 weight 5 v4 v6 weight 5 summarySet =

v8 v6 weight 5 {(100, v4), (100, ... v8)} 20 220 127 max(workSet summarySet) max(workSet) = 0 CAV 2017 ? 02/29/2020 Example: Iteration 1 (blue = true, red = false) Queries = {v6}, formula = v4 weight 100 v8 weight 100 v7 weight 100 v3 v1 weight 5 workSe v5 v2 weight 5 t v5 v3 weight 5 frontie v6 v5 weight 5 rs v6 v7 weight 5 v4 v6 weight 5

summarySet = v8 v6 weight 5 {(100, v4), (100, ... v8)} 20 220 128 max(workSet summarySet) max(workSet) = 0 CAV 2017 02/29/2020 Example: Iteration 1 (blue = true, red = false) Queries = {v6}, formula = v4 weight 100 v8 weight 100 v7 weight 100 v3 v1 weight 5 workSe v5 v2 weight 5 t v5 v3 weight 5 frontie v6 v5 weight 5 rs v6 v7 weight 5 v4 v6

weight 5 summarySet = v8 v6 weight 5 {(100, v4), (100, v4 ...= true, v5 = true, v6 v8)} 20 = true, v8 = = true, v7 true 220 max(workSet summarySet) - max(workSet) = 0 129 CAV 2017 02/29/2020 Example: Iteration 2 (blue = true, red = false) Queries = {v6}, formula = v4 weight 100 v8 weight 100 v7 weight 100 v3 v1 weight 5 workSe v5 v2 weight 5 t v5 v3 weight 5 v6 v5 weight 5

v6 v7 weight 5 v4 v6 weight 5 v8 v6 weight 5 ... 130 CAV 2017 02/29/2020 Example: Iteration 2 (blue = true, red = false) = {v6}, ? Queries formula = workSe t 131 CAV 2017 v4 v8 v7 v3 v5 v5 v6 v6 v4 v8 ...

v1 v2 v3 v5 v7 v6 v6 weight 100 weight 100 weight 100 weight 5 weight 5 weight 5 weight 5 weight 5 weight 5 weight 5 02/29/2020 Example: Iteration 2 (blue = true, red = false) = {v6}, ? Queries formula = workSe t frontie rs summarySet = {(100, v7), (5, v5v2), (5, v5v3)}

132 CAV 2017 v4 v8 v7 v3 v5 v5 v6 v6 v4 v8 ... v1 v2 v3 v5 v7 v6 v6 weight 100 weight 100 weight 100 weight 5 weight 5 weight 5 weight 5 weight 5

weight 5 weight 5 02/29/2020 Example: Iteration 2 (blue = true, red = false) Queries = {v6}, formula = v4 weight 100 v8 weight 100 v7 weight 100 v3 v1 weight 5 workSe v5 v2 weight 5 t v5 v3 weight 5 v6 v5 weight 5 v6 v7 weight 5 summarySet = {(100, v4 v6 weight 5 v7), v8 v6 weight 5 (5, v5v2), (5, ... v5v3)} max(workSet summarySet) max(workSet) = 0 133

CAV 2017 ? 02/29/2020 Example: Iteration 2 (blue = true, red = false) Queries = {v6}, formula = v4 weight 100 v8 weight 100 v7 weight 100 v3 v1 weight 5 workSe v5 v2 weight 5 t v5 v3 weight 5 v6 v5 weight 5 v6 v7 weight 5 v4 v6 weight 5 {(100, v8 v6 weight 5 ... summarySet = v7), (5, v5), (5, v5)} max(workSet summarySet) max(workSet) = 0 134

CAV 2017 ? 02/29/2020 Example: Iteration 2 (blue = true, red = false) Queries = {v6}, formula = v4 weight 100 v8 weight 100 v7 weight 100 v3 v1 weight 5 workSe v5 v2 weight 5 t v5 v3 weight 5 v6 v5 weight 5 v6 v7 weight 5 v4 v6 weight 5 summarySet = {(100, v8 v6 weight 5 v7), ... (5, v5), (5, v5)} 220 320 135 max(workSet summarySet) max(workSet) = 0

CAV 2017 02/29/2020 Example: Iteration 2 (blue = true, red = false) Queries = {v6}, formula = v4 weight 100 v8 weight 100 v7 weight 100 v3 v1 weight 5 workSe v5 v2 weight 5 t v5 v3 weight 5 v6 v5 weight 5 v6 v7 weight 5 v4 v6 weight 5 summarySet = {(100, v8 v6 weight 5 v7), ... (5, v5), (5, v5)} 220 v5 = false, v6 v4 = true, = true, v7 = true, v8 = 320 max(workSet summarySet) -true

max(workSet) = 0 136 CAV 2017 02/29/2020 Example: Iteration 3 (blue = true, red = false) Queries = {v6}, formula = v4 weight 100 v8 weight 100 v7 weight 100 v3 v1 weight 5 workSe v5 v2 weight 5 t v5 v3 weight 5 v6 v5 weight 5 v6 v7 weight 5 v4 v6 weight 5 v8 v6 weight 5 ... 137 CAV 2017

02/29/2020 Example: Iteration 3 (blue = true, red = false) = {v6}, ? Queries formula = workSe t 138 CAV 2017 v4 v8 v7 v3 v5 v5 v6 v6 v4 v8 ... v1 v2 v3 v5 v7 v6 v6 weight 100 weight 100 weight 100

weight 5 weight 5 weight 5 weight 5 weight 5 weight 5 weight 5 02/29/2020 Example: Iteration 3 (blue = true, red = false) = {v6}, ? Queries formula = frontie r workSe t summarySet = {(5, v3v1)} 139 CAV 2017 v4 v8 v7 v3 v5 v5 v6 v6 v4 v8 ...

v1 v2 v3 v5 v7 v6 v6 weight 100 weight 100 weight 100 weight 5 weight 5 weight 5 weight 5 weight 5 weight 5 weight 5 02/29/2020 Example: Iteration 3 (blue = true, red = false) frontie r summarySet = v3v1)} 330 140

Queries = {v6}, formula = v4 weight 100 v8 weight 100 v7 weight 100 v3 v1 weight 5 workSe v5 v2 weight 5 t v5 v3 weight 5 v6 v5 weight 5 v6 v7 weight 5 v4 v6 weight 5 v8 v6 weight 5 {(5, ... 325 max(workSet summarySet) max(workSet) = 0 CAV 2017 02/29/2020 Example: Iteration 3 (blue = true, red = false) frontie r summarySet = v3v1)}

325 141 Queries = {v6}, formula = v4 weight 100 v8 weight 100 v7 weight 100 v3 v1 weight 5 workSe v5 v2 weight 5 t v5 v3 weight 5 v6 v5 weight 5 v6 v7 weight 5 v4 v6 weight 5 v8 v6 weight 5 {(5, ... 325 max(workSet summarySet) max(workSet) = 0 CAV 2017 02/29/2020 Example Queries = {v6},

formula = v4 weight 100 v8 weight 100 v7 weight 100 workSe v3 v1 weight 5 t v5 v2 weight 5 = v5 v3 weight 5 formula v6 v5 weight 5 v6 v7 weight 5 v4 v6 weight 5 v8 v6 weight 5 ... 142 CAV 2017 02/29/2020 Benchmark Characteristics # queries # variables # clauses ftp 55 2.3M

3M hedc 36 3.8M 4.8M weblech 25 5.8M 8.4M lusearch 248 7.8M 10.9M luindex 109 8.5M 11.9M avrora 151 11.7M 16.3M 6 47K

0.9M ER 25 3K 4.8M AR 10 0.3M 7.9M IE K = thousands, M = millions 143 CAV 2017 02/29/2020 Performance Results running time (seconds) curren baseli t ne peak memory (MB) curre nt # clauses (M=million) baseli curren ne t

baseli ne 1,262 0.03M 3.0M ftp 16 11 16 hedc 23 21 181 1,918 0.4M 4.8M weblec h 4 timeou t 363 timeou t 0.9M 8.4M

lusearc h 115 timeou t 659 timeou t 1.5M 10.9M luindex 169 timeou t 944 timeou t 2.2M 11.9M avrora 178 timeou t 1,09 5 timeou t

2.6M 16.3M IE 2 2,760 13 335 27K 0.9M 144 ER 13 2 CAV 2017 6 44 9K 02/29/2020 4.8M Incremental Solving [CP 2016] = Two levels of incrementality

MaxSAT level Application solves a sequence of MaxSAT instances Re-use unsat cores (for core-guided solver) SAT level = Each MaxSAT solves a sequence of SAT instances Leverage standard incremental SAT solving Key insight: sporadic restarts 145 Heuristically detect and avoid reusing bad unsat cores based on split-limit (max. # times a soft clause is split) CAV 2017 02/29/2020 Performance Results in c re m e n tal ( s p l it l im it = 5 ) incremental (split limit=5) incremental in c re m e n tal(split ( s p l itliml imit=it2)= 2 ) 2500 in c re m e n ta l ( s p l it l im it = n o n in c

re m e n ta l non-incremental incremental in c re m e n ta (split l ( s p l limit= it l im it15)= n o n - in c re m e n ta l incremental in c re m e n ta(split l ( s p llimit= it l im 10) it = 1 0 ) incremental (no restart) in c re m e n ta l 10( s p l it l im it 1 0 ) 4 1800 sec. timeout 103 non-incremental 1500 1000 102 101 500 0 30 1800 sec. timeout CPU time(s) 2000 100

35 40 45 50 55 60 65 #sequential MaxSAT problems solved 70 101 1 10 100 101 102 103 incremental (split limit=5) 104 4 sequential MaxSAT problems (669 individual MaxSAT instances) 146 CAV 2017 02/29/2020 Future Directions Humans In the Loop Combining Logic With Probability Program Program Reasonin Reasonin g g Algorithm Algorithm Optimization Solvers SMT SAT 147

Datalo g ( | DataDriven MaxSAT MaxSMT Markov Logic Network Probabilistic Soft CAV 2017 Logic 02/29/2020 Conclusions New methodology to incorporate objectives into constraint-based software analyses General framework to solve weighted constraints that is sound, optimal and scalable Showed practical effectiveness for three dominant applications of software analyses 148 CAV 2017 02/29/2020

Recently Viewed Presentations

  • ESSR Gold Cup International Soccer Tournament Rome Italy June ...

    ESSR Gold Cup International Soccer Tournament Rome Italy June ...

    Totally Sincere, Steve Crossman Jacksonville FC Grandparent ... Tottenham Hotspurs v Sheffield Utd . Pre-match Lunch at Tottenham Hotspurs Stadium before the Premier League Match . Dinner in London . DAY 4 Sunday November 10th. Special Excursion to .
  • The Welsh National Anthem - zs-staravesno.cz

    The Welsh National Anthem - zs-staravesno.cz

    The Welsh National Anthem By Niamh Rind The Welsh National Anthem!!! Mae hen wlad fy nhadau yn annwyl i mi Gwlad beirdd a chantorion enwogion o fri Ei gwrol ryfelwr, gwlad garwyr tra mad Tros ryddid collasant eu gwaed.
  • HTML for JavaScript Web Applications CS3550 Dr. Brian

    HTML for JavaScript Web Applications CS3550 Dr. Brian

    div elements. Block elements. Often used to organize a web page. Can contain other block elements: paragraphs, headings, lists, and nested divs. Can be used to easily apply formatting to multiple elements
  • The Heckscher-Ohlin-Samuelson Theorem

    The Heckscher-Ohlin-Samuelson Theorem

    The H-O Theorem Given identical production functions but different factor endowments between countries, a country will tend to export the commodity which is relatively intensive in her relatively abundant factor In general, countries tend to have comparative advantage in the...
  • Unit 6 - Home - Monroe County Schools

    Unit 6 - Home - Monroe County Schools

    Unit 6. Level G. Group A1 complicity 2 inane3 agnostic4 indictment5 equity 6 abject7 diatribe 8 intermittent9 derelict 10 effigy 11 indubitableGroup B12 travesty13 surveillance 14 meretricious15 neophyte16 sylvan17 moot 18 perspicacity19 testy20 plenary21 motif22 prestigious
  • Vocabulary Lesson 9 Salvador Dali (1904-1989) Surrealist artist

    Vocabulary Lesson 9 Salvador Dali (1904-1989) Surrealist artist

    Salvador Dali (1904-1989) Surrealist artist PowerPoint by Mrs. Hinton For English 10 Montevallo High School PERCEPTION What is your perception of the work of surrealist artist Salvador Dali? Do you understand, for instance, his depictions of the human body? MUTABLE...
  • preview.thenewsmarket.com

    preview.thenewsmarket.com

    Overview. Never Made is an interactive future maker lab + cobbler where soles and uppers of adidas Originals footwear are swapped in real time. Celebrating the past whilst looking to the future, adidas Originals brings innovation to life, empowering our...
  • TimeClock Plus Full Time Faculty Biggest Changes:  All

    TimeClock Plus Full Time Faculty Biggest Changes: All

    Use the Computer for requesting leave. Use the Computer for reviewing and verifying timecards. Faculty please review your absences when requesting leave for accurate payroll processing. Become familiar with the software so that it can be utilized to the best...