@inproceedings{dig2fse17,
	Author = {Nguyen, ThanhVu and Antopoulos, Timos and Ruef, Andrew and Hicks, Michael},
	Booktitle = {Foundations of Software Engineering (FSE)},
	Publisher = {ACM},
	Pages = {605-615},
	Bibbase_Note = {},
	Title = {{A Counterexample-guided Approach to Finding Numerical Invariants}},
        Url_paper = {Pub/dig2.pdf},
	Url_slides = {Pub/dig2_pres.pdf},		
	Url_code = {https://bitbucket.org/nguyenthanhvuh/dig2/},
	Year = {2017},
	Abstract = {
Numerical invariants, e.g., relationships among numerical variables in a program, represent a useful class of properties to analyze programs.
General polynomial invariants represent more complex numerical relations, but they are often required in many scientific and engineering applications.
We present NumInv, a tool that implements a counterexample-guided invariant generation (CEGIR) technique to automatically discover numerical invariants, which are  polynomial equality and inequality relations among numerical variables.
This CEGIR technique infers candidate invariants from program traces and then checks them against the program source code using the KLEE test-input generation tool.
If the invariants are incorrect KLEE returns counterexample traces, which help the dynamic inference obtain better results.
Existing CEGIR approaches often require sound invariants, however NumInv sacrifices soundness and produces results that KLEE cannot refute within certain time bounds.
This design and the use of KLEE as a verifier allow NumInv to discover useful and important numerical invariants for many challenging programs.

Preliminary results show that NumInv generates required invariants for understanding and verifying correctness of programs involving complex  arithmetic.
We also show that NumInv discovers polynomial invariants that capture precise complexity bounds of programs used to benchmark existing static complexity analysis techniques.
Finally, we show that NumInv performs competitively comparing to state of the art numerical invariant analysis tools.	
	}
	}

{"_id":"smC6Ph2MLMPNBCP4i","bibbaseid":"nguyen-antopoulos-ruef-hicks-acounterexampleguidedapproachtofindingnumericalinvariants-2017","downloads":0,"creationDate":"2017-07-19T18:00:22.774Z","title":"A Counterexample-guided Approach to Finding Numerical Invariants","author_short":["Nguyen, T.","Antopoulos, T.","Ruef, A.","Hicks, M."],"year":2017,"bibtype":"inproceedings","biburl":"http://cse.unl.edu/~tnguyen/vu_bibs1.bib","bibdata":{"bibtype":"inproceedings","type":"inproceedings","author":[{"propositions":[],"lastnames":["Nguyen"],"firstnames":["ThanhVu"],"suffixes":[]},{"propositions":[],"lastnames":["Antopoulos"],"firstnames":["Timos"],"suffixes":[]},{"propositions":[],"lastnames":["Ruef"],"firstnames":["Andrew"],"suffixes":[]},{"propositions":[],"lastnames":["Hicks"],"firstnames":["Michael"],"suffixes":[]}],"booktitle":"Foundations of Software Engineering (FSE)","publisher":"ACM","pages":"605-615","bibbase_note":"","title":"A Counterexample-guided Approach to Finding Numerical Invariants","url_paper":"Pub/dig2.pdf","url_slides":"Pub/dig2_pres.pdf","url_code":"https://bitbucket.org/nguyenthanhvuh/dig2/","year":"2017","abstract":"Numerical invariants, e.g., relationships among numerical variables in a program, represent a useful class of properties to analyze programs. General polynomial invariants represent more complex numerical relations, but they are often required in many scientific and engineering applications. We present NumInv, a tool that implements a counterexample-guided invariant generation (CEGIR) technique to automatically discover numerical invariants, which are polynomial equality and inequality relations among numerical variables. This CEGIR technique infers candidate invariants from program traces and then checks them against the program source code using the KLEE test-input generation tool. If the invariants are incorrect KLEE returns counterexample traces, which help the dynamic inference obtain better results. Existing CEGIR approaches often require sound invariants, however NumInv sacrifices soundness and produces results that KLEE cannot refute within certain time bounds. This design and the use of KLEE as a verifier allow NumInv to discover useful and important numerical invariants for many challenging programs. Preliminary results show that NumInv generates required invariants for understanding and verifying correctness of programs involving complex arithmetic. We also show that NumInv discovers polynomial invariants that capture precise complexity bounds of programs used to benchmark existing static complexity analysis techniques. Finally, we show that NumInv performs competitively comparing to state of the art numerical invariant analysis tools. ","bibtex":"@inproceedings{dig2fse17,\n\tAuthor = {Nguyen, ThanhVu and Antopoulos, Timos and Ruef, Andrew and Hicks, Michael},\n\tBooktitle = {Foundations of Software Engineering (FSE)},\n\tPublisher = {ACM},\n\tPages = {605-615},\n\tBibbase_Note = {},\n\tTitle = {{A Counterexample-guided Approach to Finding Numerical Invariants}},\n Url_paper = {Pub/dig2.pdf},\n\tUrl_slides = {Pub/dig2_pres.pdf},\t\t\n\tUrl_code = {https://bitbucket.org/nguyenthanhvuh/dig2/},\n\tYear = {2017},\n\tAbstract = {\nNumerical invariants, e.g., relationships among numerical variables in a program, represent a useful class of properties to analyze programs.\nGeneral polynomial invariants represent more complex numerical relations, but they are often required in many scientific and engineering applications.\nWe present NumInv, a tool that implements a counterexample-guided invariant generation (CEGIR) technique to automatically discover numerical invariants, which are polynomial equality and inequality relations among numerical variables.\nThis CEGIR technique infers candidate invariants from program traces and then checks them against the program source code using the KLEE test-input generation tool.\nIf the invariants are incorrect KLEE returns counterexample traces, which help the dynamic inference obtain better results.\nExisting CEGIR approaches often require sound invariants, however NumInv sacrifices soundness and produces results that KLEE cannot refute within certain time bounds.\nThis design and the use of KLEE as a verifier allow NumInv to discover useful and important numerical invariants for many challenging programs.\n\nPreliminary results show that NumInv generates required invariants for understanding and verifying correctness of programs involving complex arithmetic.\nWe also show that NumInv discovers polynomial invariants that capture precise complexity bounds of programs used to benchmark existing static complexity analysis techniques.\nFinally, we show that NumInv performs competitively comparing to state of the art numerical invariant analysis tools.\t\n\t}\n\t}\n\n\n","author_short":["Nguyen, T.","Antopoulos, T.","Ruef, A.","Hicks, M."],"key":"dig2fse17","id":"dig2fse17","bibbaseid":"nguyen-antopoulos-ruef-hicks-acounterexampleguidedapproachtofindingnumericalinvariants-2017","role":"author","urls":{" paper":"http://cse.unl.edu/~tnguyen/Pub/dig2.pdf"," slides":"http://cse.unl.edu/~tnguyen/Pub/dig2_pres.pdf"," code":"https://bitbucket.org/nguyenthanhvuh/dig2/"},"downloads":0},"search_terms":["counterexample","guided","approach","finding","numerical","invariants","nguyen","antopoulos","ruef","hicks"],"keywords":[],"authorIDs":["545748b32abc8e9f3700025d"],"dataSources":["AAQcbSuJRTAKBGbG3"]}