@inproceedings{vuicse2014,
	Abstract = {Program invariants are important for defect detection, program verification, and program repair. However, existing techniques have limited support for important classes of invariants such as disjunctions, which express the semantics of conditional statements. We propose a method for generating disjunctive invariants over numerical domains, which are inexpressible using classical convex polyhedra. Using dynamic analysis and reformulating the problem in non-standard ``max-plus'' and ``min-plus'' algebras, our method constructs hulls over program trace points. Critically, we introduce and infer a weak class of such invariants that balances expressive power against the computational cost of generating nonconvex shapes in high dimensions. 

Existing dynamic inference techniques often generate spurious invariants that fit some program traces but do not generalize. With the insight that generating dynamic invariants is easy, we propose to verify these invariants statically using k-inductive SMT theorem proving which allows us to validate invariants that are not classically inductive. 

Results on difficult kernels involving nonlinear arithmetic and abstract arrays suggest that this hybrid approach efficiently generates and proves correct program invariants.},
	Author = {Nguyen, ThanhVu and Kapur, Deepak and Weimer, Westley and Forrest, Stephanie},
	Booktitle = {International Conference on Software Engineering (ICSE)},
	Keywords = {program analysis; static and dynamic analyses; invariant generation; disjunctive invariants; theorem proving; max-plus polyhedra},
	Publisher = {IEEE},
	Pages = {608-619},
	Title = {{Using Dynamic Analysis to Generate Disjunctive Invariants}},
	Url_code = {https://bitbucket.org/nguyenthanhvuh/dig/},
        Url_paper = {Pub/mpp.pdf},
        Url_slides = {Pub/icse14_pres.pdf},
	Year = {2014}}

{"_id":{"_str":"5345701f67062a5e680001e0"},"__v":1,"authorIDs":["545748b32abc8e9f3700025d"],"author_short":["Nguyen, T.","Kapur, D.","Weimer, W.","Forrest, S."],"bibbaseid":"nguyen-kapur-weimer-forrest-usingdynamicanalysistogeneratedisjunctiveinvariants-2014","bibdata":{"bibtype":"inproceedings","type":"inproceedings","abstract":"Program invariants are important for defect detection, program verification, and program repair. However, existing techniques have limited support for important classes of invariants such as disjunctions, which express the semantics of conditional statements. We propose a method for generating disjunctive invariants over numerical domains, which are inexpressible using classical convex polyhedra. Using dynamic analysis and reformulating the problem in non-standard ``max-plus'' and ``min-plus'' algebras, our method constructs hulls over program trace points. Critically, we introduce and infer a weak class of such invariants that balances expressive power against the computational cost of generating nonconvex shapes in high dimensions. Existing dynamic inference techniques often generate spurious invariants that fit some program traces but do not generalize. With the insight that generating dynamic invariants is easy, we propose to verify these invariants statically using k-inductive SMT theorem proving which allows us to validate invariants that are not classically inductive. Results on difficult kernels involving nonlinear arithmetic and abstract arrays suggest that this hybrid approach efficiently generates and proves correct program invariants.","author":[{"propositions":[],"lastnames":["Nguyen"],"firstnames":["ThanhVu"],"suffixes":[]},{"propositions":[],"lastnames":["Kapur"],"firstnames":["Deepak"],"suffixes":[]},{"propositions":[],"lastnames":["Weimer"],"firstnames":["Westley"],"suffixes":[]},{"propositions":[],"lastnames":["Forrest"],"firstnames":["Stephanie"],"suffixes":[]}],"booktitle":"International Conference on Software Engineering (ICSE)","keywords":"program analysis; static and dynamic analyses; invariant generation; disjunctive invariants; theorem proving; max-plus polyhedra","publisher":"IEEE","pages":"608-619","title":"Using Dynamic Analysis to Generate Disjunctive Invariants","url_code":"https://bitbucket.org/nguyenthanhvuh/dig/","url_paper":"Pub/mpp.pdf","url_slides":"Pub/icse14_pres.pdf","year":"2014","bibtex":"@inproceedings{vuicse2014,\n\tAbstract = {Program invariants are important for defect detection, program verification, and program repair. However, existing techniques have limited support for important classes of invariants such as disjunctions, which express the semantics of conditional statements. We propose a method for generating disjunctive invariants over numerical domains, which are inexpressible using classical convex polyhedra. Using dynamic analysis and reformulating the problem in non-standard ``max-plus'' and ``min-plus'' algebras, our method constructs hulls over program trace points. Critically, we introduce and infer a weak class of such invariants that balances expressive power against the computational cost of generating nonconvex shapes in high dimensions. \n\nExisting dynamic inference techniques often generate spurious invariants that fit some program traces but do not generalize. With the insight that generating dynamic invariants is easy, we propose to verify these invariants statically using k-inductive SMT theorem proving which allows us to validate invariants that are not classically inductive. \n\nResults on difficult kernels involving nonlinear arithmetic and abstract arrays suggest that this hybrid approach efficiently generates and proves correct program invariants.},\n\tAuthor = {Nguyen, ThanhVu and Kapur, Deepak and Weimer, Westley and Forrest, Stephanie},\n\tBooktitle = {International Conference on Software Engineering (ICSE)},\n\tKeywords = {program analysis; static and dynamic analyses; invariant generation; disjunctive invariants; theorem proving; max-plus polyhedra},\n\tPublisher = {IEEE},\n\tPages = {608-619},\n\tTitle = {{Using Dynamic Analysis to Generate Disjunctive Invariants}},\n\tUrl_code = {https://bitbucket.org/nguyenthanhvuh/dig/},\n Url_paper = {Pub/mpp.pdf},\n Url_slides = {Pub/icse14_pres.pdf},\n\tYear = {2014}}","author_short":["Nguyen, T.","Kapur, D.","Weimer, W.","Forrest, S."],"key":"vuicse2014","id":"vuicse2014","bibbaseid":"nguyen-kapur-weimer-forrest-usingdynamicanalysistogeneratedisjunctiveinvariants-2014","role":"author","urls":{" code":"https://bitbucket.org/nguyenthanhvuh/dig/"," paper":"http://cse.unl.edu/~tnguyen/Pub/mpp.pdf"," slides":"http://cse.unl.edu/~tnguyen/Pub/icse14_pres.pdf"},"keyword":["program analysis; static and dynamic analyses; invariant generation; disjunctive invariants; theorem proving; max-plus polyhedra"],"downloads":24},"bibtype":"inproceedings","biburl":"http://cse.unl.edu/~tnguyen/vu_bibs1.bib","downloads":24,"keywords":["program analysis; static and dynamic analyses; invariant generation; disjunctive invariants; theorem proving; max-plus polyhedra"],"search_terms":["using","dynamic","analysis","generate","disjunctive","invariants","nguyen","kapur","weimer","forrest"],"title":"Using Dynamic Analysis to Generate Disjunctive Invariants","year":2014,"dataSources":["AAQcbSuJRTAKBGbG3"]}