From fac4bf19d8fbcb5f588eb80b07e5862a126bf943 Mon Sep 17 00:00:00 2001 From: Oana Fabiana Andreescu Date: Thu, 17 Aug 2017 13:42:12 +0200 Subject: [PATCH] initial commit - Thomas' files --- .gitignore | 9 + biblio.bib | 3219 +++++++++++++++++++++++++++++++++++++++++ dependency-macros.tex | 244 ++++ main.tex | 2260 +++++++++++++++++++++++++++++ 4 files changed, 5732 insertions(+) create mode 100644 .gitignore create mode 100755 biblio.bib create mode 100644 dependency-macros.tex create mode 100644 main.tex diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..aa2df3d --- /dev/null +++ b/.gitignore @@ -0,0 +1,9 @@ +*~ +*.aux +*.bbl +*.blg +*.log +*.pdf +*.out +*.toc +*.lof diff --git a/biblio.bib b/biblio.bib new file mode 100755 index 0000000..e7bb1f7 --- /dev/null +++ b/biblio.bib @@ -0,0 +1,3219 @@ +@misc{jdt, + title = {{Eclipse Java} {Development} {Tools} {(JDT)}}, + howpublished = {\url{http://www.eclipse.org/jdt/}}, + note = {Accessed: 2016-09-11} +} + +@book{liang99, + author = {Liang, Sheng}, + title = {{Java Native Interface}: Programmer's Guide and Reference}, + year = 1999, + isbn = 0201325772, + edition = {1st}, + publisher = {Addison-Wesley Longman Publishing Co., Inc.}, + address = {Boston, MA, USA}, +} + +@misc{jni, + title = {{Java} {Native} {Interface} {Documentation} {(JNI)}}, + url = {https://docs.oracle.com/javase/7/docs/technotes/guides/jni/spec/intro.html#wp725}, + urldate = {2016-09-11}, +} + +@MISC{strachey67, + AUTHOR = {Strachey, Christopher}, + TITLE = {Fundamental Concepts in Programming Languages}, + HOWPUBLISHED = {Lecture Notes, International Summer School in Computer + Programming, Copenhagen}, + MONTH = AUG, + YEAR = {1967}, + NOTE = {Reprinted in {\em Higher-Order and Symbolic Computation}, + 13(1/2), pp. 1--49, 2000} +} + +@inproceedings{cytron89, + author = {Ron Cytron and + Jeanne Ferrante and + Barry K. Rosen and + Mark N. Wegman and + F. Kenneth Zadeck}, + title = {An Efficient Method of Computing Static Single Assignment Form}, + booktitle = {Conference Record of the Sixteenth Annual {ACM} Symposium on Principles + of Programming Languages, Austin, Texas, USA, January 11-13, 1989}, + pages = {25--35}, + year = {1989}, + url = {http://doi.acm.org/10.1145/75277.75280}, + doi = {10.1145/75277.75280}, + timestamp = {Thu, 27 Sep 2012 09:35:37 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/popl/CytronFRWZ89}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@book{nielsonbook, + author = {Flemming Nielson and + Hanne Riis Nielson and + Chris Hankin}, + title = {Principles of Program Analysis}, + publisher = {Springer}, + year = {1999}, + isbn = {978-3-540-65410-0}, + timestamp = {Fri, 12 Jun 2015 15:27:08 +0200} +} + +@misc{xtext, + title = {{Xtext} Documentation}, + howpublished = {\url{https://eclipse.org/Xtext/}}, + note = {Accessed: 2016-09-11} +} + +@article{plotkin04, + author = {Gordon D. Plotkin}, + title = {A Structural Approach to Operational Semantics}, + journal = {J. Log. Algebr. Program.}, + volume = {60-61}, + pages = {17--139}, + year = {2004}, + timestamp = {Mon, 21 Feb 2005 12:50:35 +0100} +} + + +@INPROCEEDINGS{mccarthy69, + author = {John McCarthy and Patrick J. Hayes}, + title = {Some Philosophical Problems from the Standpoint of Artificial Intelligence}, + booktitle = {Machine Intelligence}, + year = 1969, + publisher = {Edinburgh University Press}, +} + + +@incollection{meyer15, + author = {Bertrand Meyer}, + title = {Framing the Frame Problem}, + booktitle = {Dependable Software Systems Engineering}, + pages = {193--203}, + year = {2015}, + url = {http://dx.doi.org/10.3233/978-1-61499-495-4-193}, + doi = {10.3233/978-1-61499-495-4-193}, + timestamp = {Fri, 12 Feb 2016 07:36:54 +0100}, + biburl = {http://dblp.uni-trier.de/rec/bib/series/natosec/Meyer15}, + bibsource = {dblp computer science bibliography, http://dblp.org}, +} + +@inproceedings{banerjee14, + author = {Anindya Banerjee and + David A. Naumann}, + title = {A Logical Analysis of Framing for Specifications with Pure Method + Calls}, + booktitle = {Verified Software: Theories, Tools and Experiments - 6th International + Conference, {VSTTE} 2014, Vienna, Austria, July 17-18, 2014, Revised + Selected Papers}, + pages = {3--20}, + year = {2014}, + doi = {10.1007/978-3-319-12154-3_1}, + timestamp = {Wed, 15 Oct 2014 16:30:37 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/vstte/BanerjeeN14}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + + +@inproceedings{andr15, + author = {Oana F. Andreescu and + Thomas Jensen and + St{\'{e}}phane Lescuyer}, + title = {Dependency Analysis of Functional Specifications with Algebraic Data + Structures}, + booktitle = {Formal Methods and Software Engineering - 17th International Conference + on Formal Engineering Methods, {ICFEM} 2015, Proceedings}, + pages = {116--133}, + year = 2015, + url = {http://dx.doi.org/10.1007/978-3-319-25423-4_8}, + doi = {10.1007/978-3-319-25423-4_8}, + timestamp = {Tue, 01 Dec 2015 20:54:41 +0100}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/icfem/AndreescuJL15}, + bibsource = {dblp computer science bibliography, http://dblp.org}, +} + +@inproceedings{kildall73, + author = {Gary A. Kildall}, + title = {A Unified Approach to Global Program Optimization}, + booktitle = {Conference Record of the {ACM} Symposium on Principles of Programming + Languages, 1973}, + pages = {194--206}, + year = 1973, + url = {http://doi.acm.org/10.1145/512927.512945}, + doi = {10.1145/512927.512945}, + timestamp = {Mon, 21 May 2012 16:19:50 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/popl/Kildall73}, + bibsource = {dblp computer science bibliography, http://dblp.org}, +} + +@inproceedings{taghdiri06, + author = {Mana Taghdiri and + Robert Seater and + Daniel Jackson}, + title = {Lightweight Extraction of Syntactic Specifications}, + booktitle = {Proceedings of the 14th {ACM} {SIGSOFT} International Symposium on + Foundations of Software Engineering, {FSE} 2006}, + pages = {276--286}, + year = {2006}, + url = {http://doi.acm.org/10.1145/1181775.1181809}, + doi = {10.1145/1181775.1181809}, + timestamp = {Sat, 14 May 2011 10:24:07 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/sigsoft/TaghdiriSJ06}, +} + +@inproceedings{rakamaric08, + author = {Zvonimir Rakamaric and + Alan J. Hu}, + title = {Automatic Inference of Frame Axioms Using Static Analysis}, + booktitle = {23rd {IEEE/ACM} International Conference on Automated Software Engineering + {(ASE} 2008)}, + pages = {89--98}, + year = {2008}, + url = {http://dx.doi.org/10.1109/ASE.2008.19}, + doi = {10.1109/ASE.2008.19}, + timestamp = {Fri, 14 Aug 2015 14:46:09 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/kbse/RakamaricH08}, + bibsource = {dblp computer science bibliography, http://dblp.org}, +} + +@inproceedings{lattner07, + author = {Chris Lattner and + Andrew Lenharth and + Vikram S. Adve}, + title = {Making Context-Sensitive Points-To Analysis with Heap Cloning Practical + for the Real World}, + booktitle = {Proceedings of the {ACM} {SIGPLAN} 2007 Conference on Programming + Language Design and Implementation, 2007}, + pages = {278--289}, + year = {2007}, + url = {http://doi.acm.org/10.1145/1250734.1250766}, + doi = {10.1145/1250734.1250766}, + timestamp = {Wed, 13 Jun 2007 10:00:03 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/pldi/LattnerLA07}, + bibsource = {dblp computer science bibliography, http://dblp.org}, +} + + +@inproceedings{chang05, + author = {Bor{-}Yuh Evan Chang and + K. Rustan M. Leino}, + title = {Abstract Interpretation with Alien Expressions and Heap Structures}, + booktitle = {Verification, Model Checking, and Abstract Interpretation, 6th International + Conference, {VMCAI} 2005, Proceedings}, + pages = {147--163}, + year = 2005, + url = {http://dx.doi.org/10.1007/978-3-540-30579-8_11}, + doi = {10.1007/978-3-540-30579-8_11}, + timestamp = {Mon, 08 Aug 2011 15:22:35 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/vmcai/ChangL05}, + bibsource = {dblp computer science bibliography, http://dblp.org}, +} + +@article{montenegro13, + author = {Manuel Montenegro and + Ricardo Pe{\~{n}}a and + Clara Segura}, + title = {Shape Analysis in a Functional Language by Using Regular Languages}, + journal = {Sci. Comput. Program.}, + volume = {111}, + pages = {51--78}, + year = {2015}, + url = {http://dx.doi.org/10.1016/j.scico.2014.12.006}, + doi = {10.1016/j.scico.2014.12.006}, + timestamp = {Wed, 13 Jan 2016 12:54:06 +0100}, + biburl = {http://dblp.uni-trier.de/rec/bib/journals/scp/MontenegroPS15}, + bibsource = {dblp computer science bibliography, http://dblp.org}, +} + +@inproceedings{calcagno09, + author = {Cristiano Calcagno and + Dino Distefano and + Peter W. O'Hearn and + Hongseok Yang}, + title = {Compositional Shape Analysis by Means of Bi-Abduction}, + booktitle = {Proceedings of the 36th {ACM} {SIGPLAN-SIGACT} Symposium on Principles + of Programming Languages, {POPL} 2009}, + pages = {289--300}, + year = {2009}, + url = {http://doi.acm.org/10.1145/1480881.1480917}, + doi = {10.1145/1480881.1480917}, + timestamp = {Tue, 22 May 2012 15:24:56 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/popl/CalcagnoDOY09}, + bibsource = {dblp computer science bibliography, http://dblp.org}, +} + + +@inproceedings{distefano06, + author = {Distefano, Dino and O'Hearn, Peter W. and Yang, Hongseok}, + title = {A Local Shape Analysis Based on Separation Logic}, + booktitle = {Proceedings of the 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems}, + series = {TACAS'06}, + year = {2006}, + isbn = {3-540-33056-9, 978-3-540-33056-1}, + location = {Vienna, Austria}, + pages = {287--302}, + numpages = {16}, + publisher = {Springer-Verlag}, + address = {Berlin, Heidelberg}, +} + +@inproceedings{sagiv99, + author = {Shmuel Sagiv and + Thomas W. Reps and + Reinhard Wilhelm}, + title = {Parametric Shape Analysis via 3-Valued Logic}, + booktitle = {{POPL} '99, Proceedings of the 26th {ACM} {SIGPLAN-SIGACT} Symposium + on Principles of Programming Languages, 1999}, + pages = {105--118}, + year = {1999}, + url = {http://doi.acm.org/10.1145/292540.292552}, + doi = {10.1145/292540.292552}, + timestamp = {Mon, 21 May 2012 16:19:51 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/popl/SagivRW99}, + bibsource = {dblp computer science bibliography, http://dblp.org}, +} + +@inproceedings{jones79, + author = {Neil D. Jones and + Steven S. Muchnick}, + title = {Flow Analysis and Optimization of Lisp-Like Structures}, + booktitle = {Conference Record of the Sixth Annual {ACM} Symposium on Principles + of Programming Languages, 1979}, + pages = {244--256}, + year = {1979}, + url = {http://doi.acm.org/10.1145/567752.567776}, + doi = {10.1145/567752.567776}, + timestamp = {Mon, 21 May 2012 16:19:51 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/popl/JonesM79}, + bibsource = {dblp computer science bibliography, http://dblp.org}, +} + +@inproceedings{choi93, + author = {Choi, Jong-Deok and Burke, Michael and Carini, Paul}, + title = {Efficient Flow-Sensitive Interprocedural Computation of Pointer-Induced Aliases and Side Effects}, + booktitle = {Proceedings of the 20th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages}, + series = {POPL '93}, + year = {1993}, + isbn = {0-89791-560-7}, + location = {Charleston, South Carolina, USA}, + pages = {232--245}, + numpages = {14}, + publisher = {ACM}, + address = {New York, NY, USA}, +} + +@inproceedings{salcianu05, + author = {Alexandru Salcianu and + Martin C. Rinard}, + title = {Purity and Side Effect Analysis for Java Programs}, + booktitle = {Verification, Model Checking, and Abstract Interpretation, 6th International + Conference, {VMCAI} 2005, Proceedings}, + pages = {199--215}, + year = {2005}, + url = {http://dx.doi.org/10.1007/978-3-540-30579-8_14}, + doi = {10.1007/978-3-540-30579-8_14}, + timestamp = {Mon, 08 Aug 2011 15:22:35 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/vmcai/SalcianuR05}, + bibsource = {dblp computer science bibliography, http://dblp.org}, +} + +@inproceedings{tkachuk03, + author = {Tkachuk, Oksana and Dwyer, Matthew B.}, + title = {Adapting Side Effects Analysis for Modular Program Model Checking}, + booktitle = {Proceedings of the 9th European Software Engineering Conference Held Jointly with 11th ACM SIGSOFT International Symposium on Foundations of Software Engineering}, + series = {ESEC/FSE-11}, + year = {2003}, + isbn = {1-58113-743-5}, + location = {Helsinki, Finland}, + pages = {188--197}, + numpages = {10}, + publisher = {ACM}, + address = {New York, NY, USA}, + keywords = {assume-guarantee, model checking, modular flow analysis}, +} + +@article{milanova05, + author = {Ana Milanova and + Atanas Rountev and + Barbara G. Ryder}, + title = {Parameterized Object Sensitivity for Points-To Analysis for Java}, + journal = {{ACM} Trans. Softw. Eng. Methodol.}, + volume = {14}, + number = {1}, + pages = {1--41}, + year = {2005}, + url = {http://doi.acm.org/10.1145/1044834.1044835}, + doi = {10.1145/1044834.1044835}, + timestamp = {Thu, 09 Feb 2006 13:58:18 +0100}, + biburl = {http://dblp.uni-trier.de/rec/bib/journals/tosem/MilanovaRR05}, + bibsource = {dblp computer science bibliography, http://dblp.org}, +} + +@article{kogtenkov15, + author = {Kogtenkov, Alexander and Meyer, Bertrand and Velder, Sergey}, + title = {Alias Calculus, Change Calculus and Frame Inference}, + journal = {Sci. Comput. Program.}, + issue_date = {January 2015}, + volume = {97}, + number = {P1}, + month = jan, + year = {2015}, + issn = {0167-6423}, + pages = {163--172}, + numpages = {10}, + publisher = {Elsevier North-Holland, Inc.}, + address = {Amsterdam, The Netherlands, The Netherlands}, +} + +@article{lescuyer15, +author = {St{\'e}phane Lescuyer}, +title = {Proven\protect{C}ore: Towards a Verified Isolation Micro-Kernel}, +series = {International Workshop on MILS: Architecture and Assurance for Secure Systems}, +year = {2015}, +url = {http://mils-workshop-2015.euromils.eu/}, +} + +@inproceedings{borgida93, + author = {Alexander Borgida and + John Mylopoulos and + Raymond Reiter}, + title = {"... {And} Nothing Else Changes": The Frame Problem in Procedure Specifications}, + booktitle = {Proceedings of the 15th International Conference on Software Engineering, + Baltimore, Maryland, USA, May 17-21, 1993.}, + pages = {303--314}, + year = {1993}, + url = {http://portal.acm.org/citation.cfm?id=257572.257636}, + timestamp = {Mon, 14 May 2012 18:17:27 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/icse/BorgidaMR93}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@article{borgida95, + author = {Alexander Borgida and + John Mylopoulos and + Raymond Reiter}, + title = {On the Frame Problem in Procedure Specifications}, + journal = {{IEEE} Trans. Software Eng.}, + volume = {21}, + number = {10}, + pages = {785--798}, + year = {1995}, + url = {http://dx.doi.org/10.1109/32.469460}, + doi = {10.1109/32.469460}, + timestamp = {Thu, 10 Dec 2015 11:33:09 +0100}, + biburl = {http://dblp.uni-trier.de/rec/bib/journals/tse/BorgidaMR95}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + + +@article{leavens07, + author = {Gary T. Leavens and + K. Rustan M. Leino and + Peter M{\"{u}}ller}, + title = {Specification and Verification Challenges for Sequential Object-Oriented + Programs}, + journal = {Formal Asp. Comput.}, + volume = {19}, + number = {2}, + pages = {159--189}, + year = {2007}, + url = {http://dx.doi.org/10.1007/s00165-007-0026-7}, + doi = {10.1007/s00165-007-0026-7}, + timestamp = {Wed, 01 Oct 2014 13:31:09 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/journals/fac/LeavensLM07}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@book{meyer97, + author = {Bertrand Meyer}, + title = {Object-Oriented Software Construction, 2nd Edition}, + publisher = {Prentice-Hall}, + year = {1997}, + isbn = {0-13-629155-4}, + timestamp = {Tue, 16 Apr 2002 15:51:02 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/books/ph/Meyer97}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@book{guttag93, + author = {John V. Guttag and + James J. Horning and + Stephen J. Garland and + Kevin D. Jones and + A. Modet and + Jeannette M. Wing}, + title = {Larch: Languages and Tools for Formal Specification}, + series = {Texts and Monographs in Computer Science}, + publisher = {Springer}, + year = {1993}, + url = {http://dx.doi.org/10.1007/978-1-4612-2704-5}, + doi = {10.1007/978-1-4612-2704-5}, + isbn = {978-1-4612-7636-4}, + timestamp = {Mon, 12 Jan 2015 17:10:20 +0100}, + biburl = {http://dblp.uni-trier.de/rec/bib/series/mcs/GuttagHGJMW93}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{clarke02, + author = {David G. Clarke and + Sophia Drossopoulou}, + title = {Ownership, Encapsulation and the Disjointness of Type and Effect}, + booktitle = {Proceedings of the 2002 {ACM} {SIGPLAN} Conference on Object-Oriented + Programming Systems, Languages and Applications, {OOPSLA} 2002, Seattle, + Washington, USA, November 4-8, 2002.}, + pages = {292--310}, + year = {2002}, + url = {http://doi.acm.org/10.1145/582419.582447}, + doi = {10.1145/582419.582447}, + timestamp = {Tue, 11 Jun 2013 10:00:57 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/oopsla/ClarkeD02}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{greenhouse99, + author = {Aaron Greenhouse and + John Boyland}, + title = {An Object-Oriented Effects System}, + booktitle = {ECOOP'99 - Object-Oriented Programming, 13th European Conference, + Lisbon, Portugal, June 14-18, 1999, Proceedings}, + pages = {205--229}, + year = {1999}, + url = {http://dx.doi.org/10.1007/3-540-48743-3_10}, + doi = {10.1007/3-540-48743-3_10}, + timestamp = {Fri, 17 Jun 2011 14:10:37 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/ecoop/GreenhouseB99}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@book{feijs92, + author = {Feijs, L. M. G. Loe M. G. and Jonkers, H. B. M.}, + title = {Formal Specification and Design}, + series = {Cambridge tracts in theoretical computer science}, + publisher = {Cambridge University Press}, + address = {Cambridge, New York}, + url = {http://opac.inria.fr/record=b1083844}, + isbn = {0-521-43457-2}, + year = {1992} +} + +@article{liu03, + author = {Yanhong A. Liu and + Scott D. Stoller}, + title = {Eliminating Dead Code on Recursive Data}, + journal = {Sci. Comput. Program.}, + volume = {47}, + number = {2-3}, + pages = {221--242}, + year = {2003}, + url = {http://dx.doi.org/10.1016/S0167-6423(02)00134-X}, + doi = {10.1016/S0167-6423(02)00134-X}, + timestamp = {Thu, 27 Nov 2003 13:16:17 +0100}, + biburl = {http://dblp.uni-trier.de/rec/bib/journals/scp/LiuS03}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{park92, + author = {Young Gil Park and + Benjamin Goldberg}, + title = {Escape Analysis on Lists}, + booktitle = {Proceedings of the {ACM} SIGPLAN'92 Conference on Programming Language + Design and Implementation (PLDI), San Francisco, California, USA, + June 17-19, 1992}, + pages = {116--127}, + year = {1992}, + url = {http://doi.acm.org/10.1145/143095.143125}, + doi = {10.1145/143095.143125}, + timestamp = {Mon, 21 May 2012 16:19:53 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/pldi/ParkG92}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@article{kennedy78, + author = {Ken Kennedy}, + title = {Use-Definition Chains with Applications}, + journal = {Comput. Lang.}, + volume = {3}, + number = {3}, + pages = {163--179}, + year = {1978}, + url = {http://dx.doi.org/10.1016/0096-0551(78)90009-7}, + doi = {10.1016/0096-0551(78)90009-7}, + timestamp = {Tue, 05 Jul 2011 17:30:57 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/journals/cl/Kennedy78}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{castillo08, + author = {Rosa Castillo and + Francisco Corbera and + Angeles G. Navarro and + Rafael Asenjo and + Emilio L. Zapata}, + title = {Complete Def-Use Analysis in Recursive Programs with Dynamic Data + Structures}, + booktitle = {Euro-Par 2008 Workshops - Parallel Processing, {VHPC} 2008, {UNICORE} + 2008, {HPPC} 2008, {SGS} 2008, {PROPER} 2008, {ROIA} 2008, and {DPA} + 2008, Las Palmas de Gran Canaria, Spain, August 25-26, 2008, Revised + Selected Papers}, + pages = {273--282}, + year = {2008}, + url = {http://dx.doi.org/10.1007/978-3-642-00955-6_32}, + doi = {10.1007/978-3-642-00955-6_32}, + timestamp = {Thu, 16 Apr 2009 07:40:35 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/europar/CastilloCNAZ08}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{polikarpova13, + author = {Nadia Polikarpova and + Carlo A. Furia and + Yu Pei and + Yi Wei and + Bertrand Meyer}, + title = {What Good are Strong Specifications?}, + booktitle = {35th International Conference on Software Engineering, {ICSE} '13, + San Francisco, CA, USA, May 18-26, 2013}, + pages = {262--271}, + year = {2013}, + url = {http://dx.doi.org/10.1109/ICSE.2013.6606572}, + doi = {10.1109/ICSE.2013.6606572}, + timestamp = {Tue, 03 May 2016 16:26:31 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/icse/PolikarpovaF0WM13}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{reps96, + author = {Thomas W. Reps and + Todd Turnidge}, + title = {Program Specialization via Program Slicing}, + booktitle = {Partial Evaluation, International Seminar, Dagstuhl Castle, Germany, + February 12-16, 1996, Selected Papers}, + pages = {409--429}, + year = {1996}, + url = {http://dx.doi.org/10.1007/3-540-61580-6_20}, + doi = {10.1007/3-540-61580-6_20}, + timestamp = {Fri, 24 Jun 2011 20:39:39 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/dagstuhl/RepsT96}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@article{weiser84, + author = {Mark Weiser}, + title = {Program Slicing}, + journal = {{IEEE} Trans. Software Eng.}, + volume = {10}, + number = {4}, + pages = {352--357}, + year = {1984}, + url = {http://dx.doi.org/10.1109/TSE.1984.5010248}, + doi = {10.1109/TSE.1984.5010248}, + timestamp = {Thu, 10 Dec 2015 11:33:08 +0100}, + biburl = {http://dblp.uni-trier.de/rec/bib/journals/tse/Weiser84}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{jones89, + author = {Simon B. Jones and + Daniel Le M{\'{e}}tayer}, + title = {Computer-Time Garbage Collection by Sharing Analysis}, + booktitle = {Proceedings of the fourth international conference on Functional programming + languages and computer architecture, {FPCA} 1989, London, UK, September + 11-13, 1989}, + pages = {54--74}, + year = {1989}, + url = {http://doi.acm.org/10.1145/99370.99375}, + doi = {10.1145/99370.99375}, + timestamp = {Thu, 12 Nov 2015 12:04:24 +0100}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/fpca/JonesM89}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{wand98, + author = {Mitchell Wand and + William D. Clinger}, + title = {Set Constraints for Destructive Array Update Optimization}, + booktitle = {Proceedings of the 1998 International Conference on Computer Languages, + {ICCL} 1998, Chicago, IL, USA, May 14-16, 1998}, + pages = {184--195}, + year = {1998}, + url = {http://dx.doi.org/10.1109/ICCL.1998.674169}, + doi = {10.1109/ICCL.1998.674169}, + timestamp = {Fri, 27 May 2016 12:59:37 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/iccl/WandC98}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@article{tip95, + author = {Frank Tip}, + title = {A Survey of Program Slicing Techniques}, + journal = {J. Prog. Lang.}, + volume = {3}, + number = {3}, + year = {1995}, + url = {http://compscinet.dcs.kcl.ac.uk/JP/jp030301.abs.html}, + timestamp = {Fri, 09 Jan 2004 08:53:31 +0100}, + biburl = {http://dblp.uni-trier.de/rec/bib/journals/jpl/Tip95}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{wand99, + author = {Mitchell Wand and + Igor Siveroni}, + title = {Constraint Systems for Useless Variable Elimination}, + booktitle = {{POPL} '99, Proceedings of the 26th {ACM} {SIGPLAN-SIGACT} Symposium + on Principles of Programming Languages, San Antonio, TX, USA, January + 20-22, 1999}, + pages = {291--302}, + year = {1999}, + url = {http://doi.acm.org/10.1145/292540.292567}, + doi = {10.1145/292540.292567}, + timestamp = {Mon, 21 May 2012 16:19:51 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/popl/WandS99}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{knoop94, + author = {Jens Knoop and + Oliver R{\"{u}}thing and + Bernhard Steffen}, + title = {Partial Dead Code Elimination}, + booktitle = {Proceedings of the {ACM} SIGPLAN'94 Conference on Programming Language + Design and Implementation (PLDI), Orlando, Florida, USA, June 20-24, + 1994}, + pages = {147--158}, + year = {1994}, + url = {http://doi.acm.org/10.1145/178243.178256}, + doi = {10.1145/178243.178256}, + timestamp = {Mon, 21 May 2012 16:19:53 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/pldi/KnoopRS94}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{hind01, + author = {Michael Hind}, + title = {Pointer Analysis: Haven't We Solved This Problem Yet?}, + booktitle = {Proceedings of the 2001 {ACM} {SIGPLAN-SIGSOFT} Workshop on Program + Analysis For Software Tools and Engineering, PASTE'01, Snowbird, Utah, + USA, June 18-19, 2001}, + pages = {54--61}, + year = {2001}, + url = {http://doi.acm.org/10.1145/379605.379665}, + doi = {10.1145/379605.379665}, + timestamp = {Tue, 22 May 2012 15:24:55 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/paste/Hind01}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@article{gross90, + author = {Thomas R. Gross and + Peter Steenkiste}, + title = {Structured Dataflow Analysis for Arrays and its Use in an Optimizing + Compiler}, + journal = {Softw., Pract. Exper.}, + volume = {20}, + number = {2}, + pages = {133--155}, + year = {1990}, + url = {http://dx.doi.org/10.1002/spe.4380200203}, + doi = {10.1002/spe.4380200203}, + timestamp = {Sat, 14 Apr 2012 16:35:13 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/journals/spe/GrossS90}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{leroy12, + author = {Valentin Robert and + Xavier Leroy}, + title = {A Formally-Verified Alias Analysis}, + booktitle = {Certified Programs and Proofs - Second International Conference, {CPP} + 2012, Kyoto, Japan, December 13-15, 2012. Proceedings}, + pages = {11--26}, + year = {2012}, + url = {http://dx.doi.org/10.1007/978-3-642-35308-6_5}, + doi = {10.1007/978-3-642-35308-6_5}, + timestamp = {Thu, 08 Nov 2012 16:22:09 +0100}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/cpp/RobertL12}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{leino08, + author = {K. Rustan M. Leino and + Peter M{\"{u}}ller}, + title = {Verification of Equivalent-Results Methods}, + booktitle = {Programming Languages and Systems, 17th European Symposium on Programming, + {ESOP} 2008, Held as Part of the Joint European Conferences on Theory + and Practice of Software, {ETAPS} 2008, Budapest, Hungary, March 29-April + 6, 2008. Proceedings}, + pages = {307--321}, + year = {2008}, + url = {http://dx.doi.org/10.1007/978-3-540-78739-6_24}, + doi = {10.1007/978-3-540-78739-6_24}, + timestamp = {Thu, 28 May 2015 17:23:23 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/esop/LeinoM08}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{cuoq12, + author = {Pascal Cuoq and + Florent Kirchner and + Nikolai Kosmatov and + Virgile Prevosto and + Julien Signoles and + Boris Yakobowski}, + title = {Frama-{C} - {A} Software Analysis Perspective}, + booktitle = {Software Engineering and Formal Methods - 10th International Conference, + {SEFM} 2012, Thessaloniki, Greece, October 1-5, 2012. Proceedings}, + pages = {233--247}, + year = 2012, + url = {http://dx.doi.org/10.1007/978-3-642-33826-7_16}, + doi = {10.1007/978-3-642-33826-7_16}, + timestamp = {Wed, 26 Sep 2012 16:11:11 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/sefm/CuoqKKPSY12}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@article{calcagno11, + author = {Cristiano Calcagno and + Dino Distefano and + Peter W. O'Hearn and + Hongseok Yang}, + title = {Compositional Shape Analysis by Means of Bi-Abduction}, + journal = {J. {ACM}}, + volume = {58}, + number = {6}, + pages = {26}, + year = {2011}, + doi = {10.1145/2049697.2049700}, + timestamp = {Mon, 16 Jan 2012 13:04:41 +0100}, + biburl = {http://dblp.uni-trier.de/rec/bib/journals/jacm/CalcagnoDOY11}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@misc{framaman, +author = {Cuoq, Pascal and Prevosto, Virgile and Yakobowski, Boris}, +title = {Frama-{C} Value Analysis User Manual}, +url = {http://frama-c.com/download/frama-c-value-analysis.pdf} +} + +@MISC{leavens06, + author = {Gary T. Leavens and Erik Poll and Curtis Clifton and Yoonsik Cheon and Clyde Ruby and David Cok and Joseph Kiniry}, + title = {{JML} Reference Manual}, + year = {2006} +} + +@inproceedings{leavens05, + author = {Gary T. Leavens and + Curtis Clifton}, + title = {Lessons from the {JML} Project}, + booktitle = {Verified Software: Theories, Tools, Experiments, First {IFIP} {TC} + 2/WG 2.3 Conference, {VSTTE} 2005, Zurich, Switzerland, October 10-13, + 2005, Revised Selected Papers and Discussions}, + pages = {134--143}, + year = {2005}, + url = {http://dx.doi.org/10.1007/978-3-540-69149-5_15}, + doi = {10.1007/978-3-540-69149-5_15}, + timestamp = {Thu, 22 Jan 2009 15:27:54 +0100}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/vstte/LeavensC05}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{ohearn05, + author = {Peter W. O'Hearn}, + title = {Scalable Specification and Reasoning: Challenges for Program Logic}, + booktitle = {Verified Software: Theories, Tools, Experiments, First {IFIP} {TC} + 2/WG 2.3 Conference, {VSTTE} 2005, Zurich, Switzerland, October 10-13, + 2005, Revised Selected Papers and Discussions}, + pages = {116--133}, + year = {2005}, + url = {http://dx.doi.org/10.1007/978-3-540-69149-5_14}, + doi = {10.1007/978-3-540-69149-5_14}, + timestamp = {Thu, 22 Jan 2009 15:27:54 +0100}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/vstte/OHearn05}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{reynolds05, + author = {John C. Reynolds}, + title = {An Overview of Separation Logic}, + booktitle = {Verified Software: Theories, Tools, Experiments, First {IFIP} {TC} + 2/WG 2.3 Conference, {VSTTE} 2005, Zurich, Switzerland, October 10-13, + 2005, Revised Selected Papers and Discussions}, + pages = {460--469}, + year = {2005}, + url = {http://dx.doi.org/10.1007/978-3-540-69149-5_49}, + doi = {10.1007/978-3-540-69149-5_49}, + timestamp = {Thu, 22 Jan 2009 15:27:54 +0100}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/vstte/Reynolds05}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{reynolds02, + author = {John C. Reynolds}, + title = {Separation Logic: {A} Logic for Shared Mutable Data Structures}, + booktitle = {17th {IEEE} Symposium on Logic in Computer Science {(LICS} 2002), + 22-25 July 2002, Copenhagen, Denmark, Proceedings}, + pages = {55--74}, + year = {2002}, + url = {http://dx.doi.org/10.1109/LICS.2002.1029817}, + doi = {10.1109/LICS.2002.1029817}, + timestamp = {Sat, 22 Nov 2014 13:44:45 +0100}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/lics/Reynolds02}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{hur11, + author = {Chung{-}Kil Hur and + Derek Dreyer and + Viktor Vafeiadis}, + title = {Separation Logic in the Presence of Garbage Collection}, + booktitle = {Proceedings of the 26th Annual {IEEE} Symposium on Logic in Computer + Science, {LICS} 2011, June 21-24, 2011, Toronto, Ontario, Canada}, + pages = {247--256}, + year = {2011}, + url = {http://dx.doi.org/10.1109/LICS.2011.46}, + doi = {10.1109/LICS.2011.46}, + timestamp = {Sat, 22 Nov 2014 13:44:46 +0100}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/lics/HurDV11}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{bobot12, + author = {Fran{\c{c}}ois Bobot and + Jean{-}Christophe Filli{\^{a}}tre}, + title = {Separation Predicates: {A} Taste of Separation Logic in First-Order + Logic}, + booktitle = {Formal Methods and Software Engineering - 14th International Conference + on Formal Engineering Methods, {ICFEM} 2012, Kyoto, Japan, November + 12-16, 2012. Proceedings}, + pages = {167--181}, + year = {2012}, + url = {http://dx.doi.org/10.1007/978-3-642-34281-3_14}, + doi = {10.1007/978-3-642-34281-3_14}, + timestamp = {Sat, 09 Mar 2013 16:54:49 +0100}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/icfem/BobotF12}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@incollection{ohearn12, + author = {Peter W. O'Hearn}, + title = {A Primer on Separation Logic (and Automatic Program Verification and + Analysis)}, + booktitle = {Software Safety and Security - Tools for Analysis and Verification}, + pages = {286--318}, + year = {2012}, + url = {http://dx.doi.org/10.3233/978-1-61499-028-4-286}, + doi = {10.3233/978-1-61499-028-4-286}, + timestamp = {Tue, 30 Sep 2014 10:20:05 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/series/natosec/OHearn12}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{hughes87, + AUTHOR = {J. Hughes}, + TITLE = {{Backwards Analysis of Functional Programs}}, + BOOKTITLE = {{IFIP Workshop on Partial Evaluation and Mivxed Computation}}, + EDITOR = {Bj{\o}rner and Ershov}, + YEAR = {1987} +} + +@inproceedings{leinomullerwal08, + author = {K. Rustan M. Leino and + Peter M{\"{u}}ller and + Angela Wallenburg}, + title = {Flexible Immutability with Frozen Objects}, + booktitle = {Verified Software: Theories, Tools, Experiments, Second International + Conference, {VSTTE} 2008, Toronto, Canada, October 6-9, 2008. Proceedings}, + pages = {192--208}, + year = {2008}, + url = {http://dx.doi.org/10.1007/978-3-540-87873-5_17}, + doi = {10.1007/978-3-540-87873-5_17}, + timestamp = {Wed, 01 Oct 2014 13:31:09 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/vstte/LeinoMW08}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@article{hatcliff12, + author = {John Hatcliff and + Gary T. Leavens and + K. Rustan M. Leino and + Peter M{\"{u}}ller and + Matthew J. Parkinson}, + title = {Behavioral Interface Specification Languages}, + journal = {{ACM} Comput. Surv.}, + volume = 44, + number = 3, + pages = 16, + year = 2012, + url = {http://doi.acm.org/10.1145/2187671.2187678}, + doi = {10.1145/2187671.2187678}, + timestamp = {Wed, 01 Oct 2014 13:31:09 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/journals/csur/HatcliffLLMP12}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{nordio10, + author = {Martin Nordio and + Cristiano Calcagno and + Bertrand Meyer and + Peter M{\"{u}}ller and + Julian Tschannen}, + title = {Reasoning about Function Objects}, + booktitle = {Objects, Models, Components, Patterns, 48th International Conference, + {TOOLS} 2010, M{\'{a}}laga, Spain, June 28 - July 2, 2010. Proceedings}, + pages = {79--96}, + year = {2010}, + url = {http://dx.doi.org/10.1007/978-3-642-13953-6_5}, + doi = {10.1007/978-3-642-13953-6_5}, + timestamp = {Wed, 01 Oct 2014 13:31:09 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/tools/NordioCMMT10}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@article{volpano96, + author = {Dennis M. Volpano and + Cynthia E. Irvine and + Geoffrey Smith}, + title = {A Sound Type System for Secure Flow Analysis}, + journal = {Journal of Computer Security}, + volume = {4}, + number = {2/3}, + pages = {167--188}, + year = {1996}, + url = {http://dx.doi.org/10.3233/JCS-1996-42-304}, + doi = {10.3233/JCS-1996-42-304}, + timestamp = {Tue, 16 Apr 2013 15:50:01 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/journals/jcs/VolpanoIS96}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@article{sabelfeld03, + author = {Andrei Sabelfeld and + Andrew C. Myers}, + title = {Language-Based Information-Flow Security}, + journal = {{IEEE} Journal on Selected Areas in Communications}, + volume = {21}, + number = {1}, + pages = {5--19}, + year = {2003}, + url = {http://dx.doi.org/10.1109/JSAC.2002.806121}, + doi = {10.1109/JSAC.2002.806121}, + timestamp = {Wed, 15 Feb 2012 15:45:42 +0100}, + biburl = {http://dblp.uni-trier.de/rec/bib/journals/jsac/SabelfeldM03}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{wadler87, + author = {Philip Wadler and + R. J. M. Hughes}, + title = {Projections for Strictness Analysis}, + booktitle = {Functional Programming Languages and Computer Architecture, Portland, + Oregon, USA, September 14-16, 1987, Proceedings}, + pages = {385--407}, + year = {1987}, + url = {http://dx.doi.org/10.1007/3-540-18317-5_21}, + doi = {10.1007/3-540-18317-5_21}, + timestamp = {Thu, 12 Nov 2015 12:04:24 +0100}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/fpca/WadlerH87}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{liu98, + author = {Yanhong A. Liu}, + title = {Dependence Analysis for Recursive Data}, + booktitle = {Proceedings of the 1998 International Conference on Computer Languages, + {ICCL} 1998, Chicago, IL, USA, May 14-16, 1998}, + pages = {206--215}, + year = {1998}, + url = {http://dx.doi.org/10.1109/ICCL.1998.674171}, + doi = {10.1109/ICCL.1998.674171}, + timestamp = {Fri, 27 May 2016 12:59:37 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/iccl/Liu98}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{clarke98, + author = {David G. Clarke and + John Potter and + James Noble}, + title = {Ownership Types for Flexible Alias Protection}, + booktitle = {Proceedings of the 1998 {ACM} {SIGPLAN} Conference on Object-Oriented + Programming Systems, Languages {\&} Applications {(OOPSLA} '98), + Vancouver, British Columbia, Canada, October 18-22, 1998.}, + pages = {48--64}, + year = {1998}, + url = {http://doi.acm.org/10.1145/286936.286947}, + doi = {10.1145/286936.286947}, + timestamp = {Tue, 11 Jun 2013 10:03:19 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/oopsla/ClarkePN98}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{ohearn04, + author = {Peter W. O'Hearn and + Hongseok Yang and + John C. Reynolds}, + title = {Separation and Information Hiding}, + booktitle = {Proceedings of the 31st {ACM} {SIGPLAN-SIGACT} Symposium on Principles + of Programming Languages, {POPL} 2004, Venice, Italy, January 14-16, + 2004}, + pages = {268--280}, + year = {2004}, + url = {http://doi.acm.org/10.1145/964001.964024}, + doi = {10.1145/964001.964024}, + timestamp = {Tue, 22 May 2012 15:24:56 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/popl/OHearnYR04}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{barnett04, +author = {Mike Barnett, Rustan Leino, Wolfram Schulte}, +title = {The {Spec\#} Programming System: An Overview}, +booktitle = {CASSIS 2004, Construction and Analysis of Safe, Secure and Interoperable Smart devices}, +year = {2005}, +month = {January}, +publisher = {Springer}, +url = {https://www.microsoft.com/en-us/research/publication/the-spec-programming-system-an-overview/}, +address = {}, +pages = {49-69}, +journal = {}, +volume = {3362}, +chapter = {}, +isbn = {}, +} + +@inproceedings{zhao08, + author = {Yang Zhao and + John Boyland}, + title = {A Fundamental Permission Interpretation for Ownership Types}, + booktitle = {Second {IEEE/IFIP} International Symposium on Theoretical Aspects + of Software Engineering, {TASE} 2008, June 17-19, 2008, Nanjing, China}, + pages = {65--72}, + year = {2008}, + url = {http://dx.doi.org/10.1109/TASE.2008.45}, + doi = {10.1109/TASE.2008.45}, + timestamp = {Mon, 01 Dec 2014 19:24:57 +0100}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/tase/ZhaoB08}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{cousot94, + author = {Cousot, P{.} and Cousot, R{.}}, + title = {Higher-Order Abstract Interpretation (and Application to + Comportment Analysis Generalizing Strictness, Termination, + Projection and {PER} Analysis of Functional Languages), invited + paper}, + pages = {95--112}, + booktitle = {Proceedings of the 1994 International Conference on Computer + Languages}, + address = {Toulouse, France}, + month = {16--19 May}, + year = 1994, + publisher = {IEEE Computer Society Press, Los Alamitos, California}, +} + +@inproceedings{leuschel96, + author = {Michael Leuschel and + Morten Heine S{\o}rensen}, + title = {Redundant Argument Filtering of Logic Programs}, + booktitle = {Logic Programming Synthesis and Transformation, 6th International + Workshop, LOPSTR'96, Stockholm, Sweden, August 28-30, 1996, Proceedings}, + pages = {83--103}, + year = {1996}, + url = {http://dx.doi.org/10.1007/3-540-62718-9_6}, + doi = {10.1007/3-540-62718-9_6}, + timestamp = {Wed, 15 Jun 2011 15:40:01 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/lopstr/LeuschelS96a}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@article{alpuente07, + author = {Mar{\'{\i}}a Alpuente and + Santiago Escobar and + Salvador Lucas}, + title = {Removing Redundant Arguments Automatically}, + journal = {{TPLP}}, + volume = {7}, + number = {1-2}, + pages = {3--35}, + year = {2007}, + url = {http://dx.doi.org/10.1017/S1471068406002869}, + timestamp = {Thu, 12 Jun 2008 10:20:02 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/journals/tplp/AlpuenteEL07}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@article{midtgaard12, + author = {Jan Midtgaard}, + title = {Control-Flow Analysis of Functional Programs}, + journal = {{ACM} Comput. Surv.}, + volume = {44}, + number = {3}, + pages = {10}, + year = {2012}, + url = {http://doi.acm.org/10.1145/2187671.2187672}, + doi = {10.1145/2187671.2187672}, + timestamp = {Fri, 06 Jul 2012 09:13:48 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/journals/csur/Midtgaard12}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{nielson99, + author = {Flemming Nielson and + Hanne Riis Nielson}, + title = {Interprocedural Control Flow Analysis}, + booktitle = {Programming Languages and Systems, 8th European Symposium on Programming, + ESOP'99, Held as Part of the European Joint Conferences on the Theory + and Practice of Software, ETAPS'99, Amsterdam, The Netherlands, 22-28 + March, 1999, Proceedings}, + pages = {20--39}, + year = {1999}, + url = {http://dx.doi.org/10.1007/3-540-49099-X_3}, + doi = {10.1007/3-540-49099-X_3}, + timestamp = {Sun, 20 Sep 2009 17:27:13 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/esop/NielsonN99}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@article{khedker11, + author = {Uday P. Khedker and + Alan Mycroft and + Prashant Singh Rawat}, + title = {Lazy Pointer Analysis}, + journal = {CoRR}, + volume = {abs/1112.5000}, + year = {2011}, + url = {http://arxiv.org/abs/1112.5000}, + timestamp = {Wed, 10 Oct 2012 21:28:45 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/journals/corr/abs-1112-5000}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@book{sharir78, + author = {Sharir, M and Pnueli, A}, + title = {Two Approaches to Interprocedural Data Flow Analysis}, + publisher = {New York Univ. Comput. Sci. Dept."}, + address = {New York, NY}, + year = {1978}, + url = {https://cds.cern.ch/record/120118"} +} + +@inproceedings{jensen10, + author = {Simon Holm Jensen and + Anders M{\o}ller and + Peter Thiemann}, + title = {Interprocedural Analysis with Lazy Propagation}, + booktitle = {Static Analysis - 17th International Symposium, {SAS} 2010, Perpignan, + France, September 14-16, 2010. Proceedings}, + pages = {320--339}, + year = {2010}, + url = {http://dx.doi.org/10.1007/978-3-642-15769-1_20}, + doi = {10.1007/978-3-642-15769-1_20}, + timestamp = {Tue, 21 Sep 2010 14:57:19 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/sas/JensenMT10}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{reps95, + author = {Thomas W. Reps and + Susan Horwitz and + Shmuel Sagiv}, + title = {Precise Interprocedural Dataflow Analysis via Graph Reachability}, + booktitle = {Conference Record of POPL'95: 22nd {ACM} {SIGPLAN-SIGACT} Symposium + on Principles of Programming Languages, San Francisco, California, + USA, January 23-25, 1995}, + pages = {49--61}, + year = {1995}, + url = {http://doi.acm.org/10.1145/199448.199462}, + doi = {10.1145/199448.199462}, + timestamp = {Mon, 10 Dec 2012 15:26:39 +0100}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/popl/RepsHS95}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{horwitz95, + author = {Susan Horwitz and + Thomas W. Reps and + Shmuel Sagiv}, + title = {Demand Interprocedural Dataflow Analysis}, + booktitle = {{SIGSOFT} '95, Proceedings of the Third {ACM} {SIGSOFT} Symposium + on Foundations of Software Engineering, Washington, DC, USA, October + 10-13, 1995}, + pages = {104--115}, + year = {1995}, + url = {http://doi.acm.org/10.1145/222124.222146}, + doi = {10.1145/222124.222146}, + timestamp = {Mon, 10 Jun 2013 17:49:05 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/sigsoft/HorwitzRS95}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@book{jones87, + author = {Simon L. Peyton Jones}, + title = {The Implementation of Functional Programming Languages}, + publisher = {Prentice-Hall}, + year = {1987}, + timestamp = {Thu, 03 Jan 2002 11:51:40 +0100}, + biburl = {http://dblp.uni-trier.de/rec/bib/books/ph/Jones87}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{lhotak06, + author = {Ondrej Lhot{\'{a}}k and + Laurie J. Hendren}, + title = {Context-Sensitive Points-to Analysis: Is It Worth It?}, + booktitle = {Compiler Construction, 15th International Conference, {CC} 2006, Held + as Part of the Joint European Conferences on Theory and Practice of + Software, {ETAPS} 2006, Vienna, Austria, March 30-31, 2006, Proceedings}, + pages = {47--64}, + year = {2006}, + url = {http://dx.doi.org/10.1007/11688839_5}, + doi = {10.1007/11688839_5}, + timestamp = {Thu, 28 May 2015 17:23:25 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/cc/LhotakH06}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{ruf95, + author = {Ruf, Erik}, + title = {Context-Insensitive Alias Analysis Reconsidered}, + booktitle = {Proceedings of the ACM SIGPLAN 1995 Conference on Programming Language Design and Implementation}, + series = {PLDI '95}, + year = {1995}, + isbn = {0-89791-697-2}, + location = {La Jolla, California, USA}, + pages = {13--22}, + numpages = {10}, + url = {http://doi.acm.org/10.1145/207110.207112}, + doi = {10.1145/207110.207112}, + acmid = {207112}, + publisher = {ACM}, + address = {New York, NY, USA}, +} + +@inproceedings{shapiro97, + author = {Marc Shapiro and + Susan Horwitz}, + title = {The Effects of the Precision of Pointer Analysis}, + booktitle = {Static Analysis, 4th International Symposium, {SAS} '97, Paris, France, + September 8-10, 1997, Proceedings}, + pages = {16--34}, + year = {1997}, + url = {http://dx.doi.org/10.1007/BFb0032731}, + doi = {10.1007/BFb0032731}, + timestamp = {Sat, 27 Apr 2013 16:26:53 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/sas/ShapiroH97}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{heintze01, + author = {Heintze, Nevin and Tardieu, Olivier}, + title = {Demand-Driven Pointer Analysis}, + booktitle = {Proceedings of the ACM SIGPLAN 2001 Conference on Programming Language Design and Implementation}, + series = {PLDI '01}, + year = {2001}, + isbn = {1-58113-414-2}, + location = {Snowbird, Utah, USA}, + pages = {24--34}, + numpages = {11}, + url = {http://doi.acm.org/10.1145/378795.378802}, + doi = {10.1145/378795.378802}, + acmid = {378802}, + publisher = {ACM}, + address = {New York, NY, USA}, +} + +@inproceedings{zheng08, + author = {Zheng, Xin and Rugina, Radu}, + title = {Demand-Driven Alias Analysis for {C}}, + booktitle = {Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages}, + series = {POPL '08}, + year = {2008}, + isbn = {978-1-59593-689-9}, + location = {San Francisco, California, USA}, + pages = {197--208}, + numpages = {12}, + url = {http://doi.acm.org/10.1145/1328438.1328464}, + doi = {10.1145/1328438.1328464}, + acmid = {1328464}, + publisher = {ACM}, + address = {New York, NY, USA}, + keywords = {CFL reachability, alias analysis, demand-driven analysis, memory disambiguation, pointer analysis}, +} + +@inproceedings{sridharan05, + author = {Sridharan, Manu and Gopan, Denis and Shan, Lexin and Bod\'{\i}k, Rastislav}, + title = {Demand-Driven Points-to Analysis for {Java}}, + booktitle = {Proceedings of the 20th Annual ACM SIGPLAN Conference on Object-oriented Programming, Systems, Languages, and Applications}, + series = {OOPSLA '05}, + year = {2005}, + isbn = {1-59593-031-0}, + location = {San Diego, CA, USA}, + pages = {59--76}, + numpages = {18}, + url = {http://doi.acm.org/10.1145/1094811.1094817}, + doi = {10.1145/1094811.1094817}, + acmid = {1094817}, + publisher = {ACM}, + address = {New York, NY, USA}, + keywords = {context-free language reachability, demand-driven analysis, points-to analysis, refinement}, +} + +@inproceedings{gharat16, + author = {Pritam M. Gharat and + Uday P. Khedker and + Alan Mycroft}, + title = {Flow- and Context-Sensitive Points-To Analysis Using Generalized Points-To + Graphs}, + booktitle = {Static Analysis - 23rd International Symposium, {SAS} 2016, Edinburgh, + UK, September 8-10, 2016, Proceedings}, + pages = {212--236}, + year = {2016}, + url = {http://dx.doi.org/10.1007/978-3-662-53413-7_11}, + doi = {10.1007/978-3-662-53413-7_11}, + timestamp = {Thu, 01 Sep 2016 11:24:02 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/sas/GharatKM16}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@article{hammer09, + author = {Christian Hammer and + Gregor Snelting}, + title = {Flow-Sensitive, Context-Sensitive, and Object-Sensitive Information + Flow Control based on Program Dependence Graphs}, + journal = {Int. J. Inf. Sec.}, + volume = {8}, + number = {6}, + pages = {399--422}, + year = {2009}, + url = {http://dx.doi.org/10.1007/s10207-009-0086-1}, + doi = {10.1007/s10207-009-0086-1}, + timestamp = {Fri, 02 Jan 2015 13:41:11 +0100}, + biburl = {http://dblp.uni-trier.de/rec/bib/journals/ijisec/HammerS09}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{asati14, + author = {Rahul Asati and + Amitabha Sanyal and + Amey Karkare and + Alan Mycroft}, + title = {Liveness-Based Garbage Collection}, + booktitle = {Compiler Construction - 23rd International Conference, {CC} 2014, + Held as Part of the European Joint Conferences on Theory and Practice + of Software, {ETAPS} 2014, Grenoble, France, April 5-13, 2014. Proceedings}, + pages = {85--106}, + year = {2014}, + url = {http://dx.doi.org/10.1007/978-3-642-54807-9_5}, + doi = {10.1007/978-3-642-54807-9_5}, + timestamp = {Mon, 27 Jul 2015 18:21:38 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/cc/AsatiSKM14}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + + +@inproceedings{padhye13, + author = {Rohan Padhye and + Uday P. Khedker}, + title = {Interprocedural Data Flow Analysis in Soot Using Value Contexts}, + booktitle = {Proceedings of the 2nd {ACM} {SIGPLAN} International Workshop on State + Of the Art in Java Program analysis, {SOAP} 2013, Seattle, WA, USA, + June 20, 2013}, + pages = {31--36}, + year = 2013, + url = {http://doi.acm.org/10.1145/2487568.2487569}, + doi = {10.1145/2487568.2487569}, + timestamp = {Mon, 19 Dec 2016 07:38:57 +0100}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/pldi/PadhyeK13}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{andr16, + author = {Oana Fabiana Andreescu and + Thomas Jensen and + St{\'{e}}phane Lescuyer}, + title = {Correlating Structured Inputs and Outputs in Functional Specifications}, + booktitle = {Software Engineering and Formal Methods - 14th International Conference, + {SEFM} 2016, Held as Part of {STAF} 2016, Vienna, Austria, July 4-8, + 2016, Proceedings}, + pages = {85--103}, + year = {2016}, + url = {http://dx.doi.org/10.1007/978-3-319-41591-8_7}, + doi = {10.1007/978-3-319-41591-8_7}, + timestamp = {Thu, 23 Jun 2016 13:50:58 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/sefm/AndreescuJL16}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@book{liskov86, + author = {Liskov, Barbara and Guttag, John}, + title = {Abstraction and Specification in Program Development}, + year = {1986}, + isbn = {0-262-12112-3}, + publisher = {MIT Press}, + address = {Cambridge, MA, USA}, +} + +@article{guttag85, + author = {John V. Guttag and + James J. Horning and + Jeannette M. Wing}, + title = {The Larch Family of Specification Languages}, + journal = {{IEEE} Software}, + volume = {2}, + number = {5}, + pages = {24--36}, + year = {1985}, + url = {http://dx.doi.org/10.1109/MS.1985.231756}, + doi = {10.1109/MS.1985.231756}, + timestamp = {Tue, 12 Jan 2016 12:01:50 +0100}, + biburl = {http://dblp.uni-trier.de/rec/bib/journals/software/GuttagHW85}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@incollection{hoare71, + author = {C. A. R. Hoare}, + title = {Procedures and Parameters: An Axiomatic Approach}, + booktitle = {Symposium on Semantics of Algorithmic Languages}, + pages = {102--116}, + year = {1971}, + url = {http://dx.doi.org/10.1007/BFb0059696}, + doi = {10.1007/BFb0059696}, + timestamp = {Wed, 15 Jun 2011 20:53:44 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/series/lnm/Hoare71}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@book{reynolds81, + author = {John C. Reynolds}, + title = {The Craft of Programming}, + series = {Prentice Hall International series in computer science}, + publisher = {Prentice Hall}, + year = {1981}, + isbn = {978-0-13-188862-3}, + timestamp = {Wed, 23 Mar 2011 08:32:52 +0100}, + biburl = {http://dblp.uni-trier.de/rec/bib/books/daglib/0078442}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{ohearn01, + author = {Peter W. O'Hearn and + John C. Reynolds and + Hongseok Yang}, + title = {Local Reasoning about Programs that Alter Data Structures}, + booktitle = {Computer Science Logic, 15th International Workshop, {CSL} 2001. 10th + Annual Conference of the EACSL, Paris, France, September 10-13, 2001, + Proceedings}, + pages = {1--19}, + year = {2001}, + url = {http://dx.doi.org/10.1007/3-540-44802-0_1}, + doi = {10.1007/3-540-44802-0_1}, + timestamp = {Tue, 28 Jun 2011 15:11:08 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/csl/OHearnRY01}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{banerjee08, + author = {Anindya Banerjee and + David A. Naumann and + Stan Rosenberg}, + title = {Regional Logic for Local Reasoning about Global Invariants}, + booktitle = {{ECOOP} 2008 - Object-Oriented Programming, 22nd European Conference, + Paphos, Cyprus, July 7-11, 2008, Proceedings}, + pages = {387--411}, + year = {2008}, + url = {http://dx.doi.org/10.1007/978-3-540-70592-5_17}, + doi = {10.1007/978-3-540-70592-5_17}, + timestamp = {Mon, 14 Jul 2008 10:36:13 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/ecoop/BanerjeeNR08}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@incollection{abrial80, + author = {Jean{-}Raymond Abrial and + Stephen A. Schuman and + Bertrand Meyer}, + title = {Specification Language}, + booktitle = {On the Construction of Programs}, + pages = {343--410}, + year = {1980}, + timestamp = {Fri, 20 Dec 2002 15:09:29 +0100}, + biburl = {http://dblp.uni-trier.de/rec/bib/books/cu/mckeag80/AbrialSM80}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{leinodafny10, + author = {K. Rustan M. Leino}, + title = {Dafny: An Automatic Program Verifier for Functional Correctness}, + booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning - 16th + International Conference, LPAR-16, Dakar, Senegal, April 25-May 1, + 2010, Revised Selected Papers}, + pages = {348--370}, + year = 2010, + url = {http://dx.doi.org/10.1007/978-3-642-17511-4_20}, + doi = {10.1007/978-3-642-17511-4_20}, + timestamp = {Thu, 23 Dec 2010 12:42:49 +0100}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/lpar/Leino10}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@INPROCEEDINGS{morgenstern95, + author = {Leora Morgenstern}, + title = {The Problem with Solutions to the Frame Problem}, + booktitle = {The Robot’s Dilemma Revisited: The Frame Problem in Artificial Intelligence. Ablex}, + year = {1995}, + pages = {99--133}, + publisher = {Ablex Publishing Co} +} + +@article{leinonelson02, + author = {K. Rustan M. Leino and + Greg Nelson}, + title = {Data Abstraction and Information Hiding}, + journal = {{ACM} Trans. Program. Lang. Syst.}, + volume = {24}, + number = {5}, + pages = {491--553}, + year = {2002}, + url = {http://doi.acm.org/10.1145/570886.570888}, + doi = {10.1145/570886.570888}, + timestamp = {Wed, 26 Nov 2003 14:26:45 +0100}, + biburl = {http://dblp.uni-trier.de/rec/bib/journals/toplas/LeinoN02}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{oopslaleino98, + author = {K. Rustan M. Leino}, + title = {Data Groups: Specifying the Modification of Extended State}, + booktitle = {Proceedings of the 1998 {ACM} {SIGPLAN} Conference on Object-Oriented + Programming Systems, Languages {\&} Applications {(OOPSLA} '98), + Vancouver, British Columbia, Canada, October 18-22, 1998.}, + pages = {144--153}, + year = {1998}, + url = {http://doi.acm.org/10.1145/286936.286953}, + doi = {10.1145/286936.286953}, + timestamp = {Tue, 11 Jun 2013 10:03:19 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/oopsla/Leino98}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{pldileino02, + author = {K. Rustan M. Leino and + Arnd Poetzsch{-}Heffter and + Yunhong Zhou}, + title = {Using Data Groups to Specify and Check Side Effects}, + booktitle = {Proceedings of the 2002 {ACM} {SIGPLAN} Conference on Programming + Language Design and Implementation (PLDI), Berlin, Germany, June 17-19, + 2002}, + pages = {246--257}, + year = {2002}, + url = {http://doi.acm.org/10.1145/512529.512559}, + doi = {10.1145/512529.512559}, + timestamp = {Mon, 21 May 2012 16:19:53 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/pldi/LeinoPZ02}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@book{mullerphd02, + author = {Peter M{\"{u}}ller}, + title = {Modular Specification and Verification of Object-Oriented Programs}, + series = {Lecture Notes in Computer Science}, + volume = {2262}, + publisher = {Springer}, + year = {2002}, + url = {http://dx.doi.org/10.1007/3-540-45651-1}, + doi = {10.1007/3-540-45651-1}, + isbn = {3-540-43167-5}, + timestamp = {Wed, 01 Oct 2014 13:31:08 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/books/sp/Muller02}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@article{mullerjournal03, + author = {Peter M{\"{u}}ller and + Arnd Poetzsch{-}Heffter and + Gary T. Leavens}, + title = {Modular Specification of Frame Properties in {JML}}, + journal = {Concurrency and Computation: Practice and Experience}, + volume = {15}, + number = {2}, + pages = {117--154}, + year = {2003}, + url = {http://dx.doi.org/10.1002/cpe.713}, + doi = {10.1002/cpe.713}, + timestamp = {Wed, 01 Oct 2014 13:31:08 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/journals/concurrency/MullerPL03}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{ecoopleino04, + author = {K. Rustan M. Leino and + Peter M{\"{u}}ller}, + title = {Object Invariants in Dynamic Contexts}, + booktitle = {{ECOOP} 2004 - Object-Oriented Programming, 18th European Conference, + Oslo, Norway, June 14-18, 2004, Proceedings}, + pages = {491--516}, + year = {2004}, + url = {http://dx.doi.org/10.1007/978-3-540-24851-4_22}, + doi = {10.1007/978-3-540-24851-4_22}, + timestamp = {Wed, 01 Oct 2014 13:31:09 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/ecoop/LeinoM04}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{esopleino06, + author = {K. Rustan M. Leino and + Peter M{\"{u}}ller}, + title = {A Verification Methodology for Model Fields}, + booktitle = {Programming Languages and Systems, 15th European Symposium on Programming, + {ESOP} 2006, Held as Part of the Joint European Conferences on Theory + and Practice of Software, {ETAPS} 2006, Vienna, Austria, March 27-28, + 2006, Proceedings}, + pages = {115--130}, + year = {2006}, + url = {http://dx.doi.org/10.1007/11693024_9}, + doi = {10.1007/11693024_9}, + timestamp = {Thu, 28 May 2015 17:23:23 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/esop/LeinoM06}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{barnettnaumann04, + author = {Michael Barnett and + David A. Naumann}, + title = {Friends Need a Bit More: Maintaining Invariants Over Shared State}, + booktitle = {Mathematics of Program Construction, 7th International Conference, + {MPC} 2004, Stirling, Scotland, UK, July 12-14, 2004, Proceedings}, + pages = {54--84}, + year = {2004}, + url = {http://dx.doi.org/10.1007/978-3-540-27764-4_5}, + doi = {10.1007/978-3-540-27764-4_5}, + timestamp = {Fri, 22 May 2015 07:12:28 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/mpc/BarnettN04}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{kassios06, + author = {Ioannis T. Kassios}, + title = {Dynamic Frames: Support for Framing, Dependencies and Sharing Without + Restrictions}, + booktitle = {{FM} 2006: Formal Methods, 14th International Symposium on Formal + Methods, Hamilton, Canada, August 21-27, 2006, Proceedings}, + pages = {268--283}, + year = {2006}, + url = {http://dx.doi.org/10.1007/11813040_19}, + doi = {10.1007/11813040_19}, + timestamp = {Tue, 22 Aug 2006 14:47:47 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/fm/Kassios06}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@article{kassios11, + author = {Ioannis T. Kassios}, + title = {The Dynamic Frames Theory}, + journal = {Formal Asp. Comput.}, + volume = {23}, + number = {3}, + pages = {267--288}, + year = {2011}, + url = {http://dx.doi.org/10.1007/s00165-010-0152-5}, + doi = {10.1007/s00165-010-0152-5}, + timestamp = {Wed, 11 May 2011 15:37:14 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/journals/fac/Kassios11}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@article{smans12, + author = {Jan Smans and + Bart Jacobs and + Frank Piessens}, + title = {Implicit Dynamic Frames}, + journal = {{ACM} Trans. Program. Lang. Syst.}, + volume = {34}, + number = {1}, + pages = {2:1--2:58}, + year = {2012}, + url = {http://doi.acm.org/10.1145/2160910.2160911}, + doi = {10.1145/2160910.2160911}, + timestamp = {Fri, 06 Jan 2017 11:44:59 +0100}, + biburl = {http://dblp.uni-trier.de/rec/bib/journals/toplas/SmansJP12}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{parkinson05, + author = {Matthew J. Parkinson and + Gavin M. Bierman}, + title = {Separation Logic and Abstraction}, + booktitle = {Proceedings of the 32nd {ACM} {SIGPLAN-SIGACT} Symposium on Principles + of Programming Languages, {POPL} 2005, Long Beach, California, USA, + January 12-14, 2005}, + pages = {247--258}, + year = {2005}, + url = {http://doi.acm.org/10.1145/1040305.1040326}, + doi = {10.1145/1040305.1040326}, + timestamp = {Tue, 22 May 2012 15:24:56 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/popl/ParkinsonB05}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@article{meyerjournal10, + author = {Bertrand Meyer}, + title = {Towards a Theory and Calculus of Aliasing}, + journal = {Journal of Object Technology}, + volume = {9}, + number = {2}, + pages = {37--74}, + year = {2010}, + url = {http://dx.doi.org/10.5381/jot.2010.9.2.c5}, + doi = {10.5381/jot.2010.9.2.c5}, + timestamp = {Fri, 19 Nov 2010 11:59:39 +0100}, + biburl = {http://dblp.uni-trier.de/rec/bib/journals/jot/Meyer10}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@article{meyerjournal11, + author = {Bertrand Meyer}, + title = {Steps Towards a Theory and Calculus of Aliasing}, + journal = {Int. J. Software and Informatics}, + volume = {5}, + number = {1-2}, + pages = {77--115}, + year = {2011}, + url = {http://www.ijsi.org/ch/reader/view_abstract.aspx?file_no=i77}, + timestamp = {Wed, 30 Jan 2013 14:41:57 +0100}, + biburl = {http://dblp.uni-trier.de/rec/bib/journals/ijsi/Meyer11}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@article{meyerdbc92, + author = {Bertrand Meyer}, + title = {Applying "Design by Contract"}, + journal = {{IEEE} Computer}, + volume = {25}, + number = {10}, + pages = {40--51}, + year = {1992}, + url = {http://dx.doi.org/10.1109/2.161279}, + doi = {10.1109/2.161279}, + timestamp = {Wed, 16 Dec 2015 10:09:37 +0100}, + biburl = {http://dblp.uni-trier.de/rec/bib/journals/computer/Meyer92}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@book{meyereiffel91, + author = {Bertrand Meyer}, + title = {Eiffel: The Language}, + publisher = {Prentice-Hall}, + year = {1991}, + isbn = {0-13-247925-7}, + timestamp = {Tue, 16 Apr 2002 15:53:25 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/books/ph/Meyer91}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@article{barnettschulte04, + author = {Michael Barnett and + Robert DeLine and + Manuel F{\"{a}}hndrich and + K. Rustan M. Leino and + Wolfram Schulte}, + title = {Verification of Object-Oriented Programs with Invariants}, + journal = {Journal of Object Technology}, + volume = {3}, + number = {6}, + pages = {27--56}, + year = {2004}, + url = {http://dx.doi.org/10.5381/jot.2004.3.6.a2}, + doi = {10.5381/jot.2004.3.6.a2}, + timestamp = {Fri, 22 May 2015 07:12:28 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/journals/jot/BarnettDFLS04}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@INPROCEEDINGS{floyd67, + AUTHOR = {Floyd, Robert W.}, + TITLE = {Assigning Meanings to Programs}, + BOOKTITLE = {Mathematical Aspects of Computer Science}, + PLACE = {New York City}, + DATES = {April 5--7, 1966}, + EDITOR = {J. T. Schwartz}, + SERIES = {Proceedings of Symposia in Applied Mathematics}, + VOLUME = {19}, + PUBLISHER = {American Mathematical Society}, + ADDRESS = {Providence, Rhode Island}, + YEAR = {1967}, + PAGES = {19--32}, +} + +@article{hoare69, + author = {C. A. R. Hoare}, + title = {An Axiomatic Basis for Computer Programming}, + journal = {Commun. {ACM}}, + volume = {12}, + number = {10}, + pages = {576--580}, + year = {1969}, + url = {http://doi.acm.org/10.1145/363235.363259}, + doi = {10.1145/363235.363259}, + timestamp = {Thu, 20 Nov 2003 13:06:13 +0100}, + biburl = {http://dblp.uni-trier.de/rec/bib/journals/cacm/Hoare69}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@article{naur66, +author="Naur, Peter", +title="Proof of Algorithms by General Snapshots", +journal="BIT Numerical Mathematics", +year="1966", +volume="6", +number="4", +pages="310--316", +issn="1572-9125", +doi="10.1007/BF01966091", +url="http://dx.doi.org/10.1007/BF01966091" +} + +@book{piercebook, + author = {Benjamin C. Pierce}, + title = {Types and Programming Languages}, + publisher = {{MIT} Press}, + year = {2002}, + isbn = {978-0-262-16209-8}, + timestamp = {Thu, 03 Feb 2011 10:51:35 +0100}, + biburl = {http://dblp.uni-trier.de/rec/bib/books/daglib/0005958}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@article{cardelli85, + author = {Luca Cardelli and + Peter Wegner}, + title = {On Understanding Types, Data Abstraction, and Polymorphism}, + journal = {{ACM} Comput. Surv.}, + volume = {17}, + number = {4}, + pages = {471--522}, + year = {1985}, + url = {http://doi.acm.org/10.1145/6041.6042}, + doi = {10.1145/6041.6042}, + timestamp = {Mon, 05 Dec 2011 18:03:13 +0100}, + biburl = {http://dblp.uni-trier.de/rec/bib/journals/csur/CardelliW85}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{esc98, + author = {K. Rustan M. Leino and + Greg Nelson}, + title = {An Extended Static Checker for Modular-3}, + booktitle = {Compiler Construction, 7th International Conference, CC'98, Held as + Part of the European Joint Conferences on the Theory and Practice + of Software, ETAPS'98, Lisbon, Portugal, March 28 - April 4, 1998, + Proceedings}, + pages = {302--305}, + year = {1998}, + url = {http://dx.doi.org/10.1007/BFb0026441}, + doi = {10.1007/BFb0026441}, + timestamp = {Thu, 15 Oct 2009 09:07:53 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/cc/LeinoN98}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{esc01, + author = {K. Rustan M. Leino}, + title = {Extended Static Checking: {A} Ten-Year Perspective}, + booktitle = {Informatics - 10 Years Back. 10 Years Ahead.}, + pages = {157--175}, + year = {2001}, + url = {http://dx.doi.org/10.1007/3-540-44577-3_11}, + doi = {10.1007/3-540-44577-3_11}, + timestamp = {Thu, 23 Jun 2016 15:53:29 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/dagstuhl/Leino01}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{esc02, + author = {Cormac Flanagan and + K. Rustan M. Leino and + Mark Lillibridge and + Greg Nelson and + James B. Saxe and + Raymie Stata}, + title = {Extended Static Checking for Java}, + booktitle = {Proceedings of the 2002 {ACM} {SIGPLAN} Conference on Programming + Language Design and Implementation (PLDI), Berlin, Germany, June 17-19, + 2002}, + pages = {234--245}, + year = {2002}, + url = {http://doi.acm.org/10.1145/512529.512558}, + doi = {10.1145/512529.512558}, + timestamp = {Mon, 21 May 2012 16:19:53 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/pldi/FlanaganLLNSS02}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{ocallahan97, + author = {Robert O'Callahan and + Daniel Jackson}, + title = {Lackwit: {A} Program Understanding Tool Based on Type Inference}, + booktitle = {Pulling Together, Proceedings of the 19th International Conference + on Software Engineering, Boston, Massachusetts, USA, May 17-23, 1997.}, + pages = {338--348}, + year = {1997}, + url = {http://doi.acm.org/10.1145/253228.253351}, + doi = {10.1145/253228.253351}, + timestamp = {Mon, 14 May 2012 18:17:22 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/icse/OCallahanJ97}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@article{leroy00, + author = {Xavier Leroy and + Fran{\c{c}}ois Pessaux}, + title = {Type-Based Analysis of Uncaught Exceptions}, + journal = {{ACM} Trans. Program. Lang. Syst.}, + volume = {22}, + number = {2}, + pages = {340--377}, + year = {2000}, + url = {http://doi.acm.org/10.1145/349214.349230}, + doi = {10.1145/349214.349230}, + timestamp = {Wed, 26 Nov 2003 14:26:45 +0100}, + biburl = {http://dblp.uni-trier.de/rec/bib/journals/toplas/LeroyP00}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@book{lof84, + address = {Naples}, + author = {Martin-L\"{o}f, Per}, + citeulike-article-id = {1177380}, + keywords = {type-theory}, + posted-at = {2007-03-20 13:21:29}, + priority = {2}, + publisher = {Bibliopolis}, + title = {{Intuitionistic Type Theory}}, + year = {1984} +} + +@book{nordstrom90, + title={Programming in Martin-L{\"o}f’s Type Theory}, + author={Nordstr{\"o}m, Bengt and Petersson, Kent and Smith, Jan M}, + volume={200}, + year={1990}, + publisher={Oxford University Press Oxford} +} + +@book{bertot04, + author = {Yves Bertot and + Pierre Cast{\'{e}}ran}, + title = {Interactive Theorem Proving and Program Development - Coq'Art: The + Calculus of Inductive Constructions}, + series = {Texts in Theoretical Computer Science. An {EATCS} Series}, + publisher = {Springer}, + year = {2004}, + url = {http://dx.doi.org/10.1007/978-3-662-07964-5}, + doi = {10.1007/978-3-662-07964-5}, + isbn = {978-3-642-05880-6}, + timestamp = {Wed, 09 Sep 2015 16:46:05 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/series/txtcs/BertotC04}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@book{baier08, + author = {Christel Baier and + Joost{-}Pieter Katoen}, + title = {Principles of Model Checking}, + publisher = {{MIT} Press}, + year = {2008}, + isbn = {978-0-262-02649-9}, + timestamp = {Tue, 15 Feb 2011 11:22:37 +0100}, + biburl = {http://dblp.uni-trier.de/rec/bib/books/daglib/0020348}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@article{rupak09, + author = {Ranjit Jhala and + Rupak Majumdar}, + title = {Software Model Checking}, + journal = {{ACM} Comput. Surv.}, + volume = {41}, + number = {4}, + pages = {21:1--21:54}, + year = {2009}, + url = {http://doi.acm.org/10.1145/1592434.1592438}, + doi = {10.1145/1592434.1592438}, + timestamp = {Mon, 09 Jan 2017 15:02:22 +0100}, + biburl = {http://dblp.uni-trier.de/rec/bib/journals/csur/JhalaM09}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@article{nelsonoppen80, + author = {Greg Nelson and + Derek C. Oppen}, + title = {Fast Decision Procedures Based on Congruence Closure}, + journal = {J. {ACM}}, + volume = {27}, + number = {2}, + pages = {356--364}, + year = {1980}, + url = {http://doi.acm.org/10.1145/322186.322198}, + doi = {10.1145/322186.322198}, + timestamp = {Thu, 26 Jan 2012 17:31:32 +0100}, + biburl = {http://dblp.uni-trier.de/rec/bib/journals/jacm/NelsonO80}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@article{shostak84, + author = {Robert E. Shostak}, + title = {Deciding Combinations of Theories}, + journal = {J. {ACM}}, + volume = {31}, + number = {1}, + pages = {1--12}, + year = {1984}, + url = {http://doi.acm.org/10.1145/2422.322411}, + doi = {10.1145/2422.322411}, + timestamp = {Thu, 20 Nov 2003 12:28:22 +0100}, + biburl = {http://dblp.uni-trier.de/rec/bib/journals/jacm/Shostak84}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{clarke81, + author = {Edmund M. Clarke and + E. Allen Emerson}, + title = {Design and Synthesis of Synchronization Skeletons Using Branching-Time + Temporal Logic}, + booktitle = {Logics of Programs, Workshop, Yorktown Heights, New York, May 1981}, + pages = {52--71}, + year = {1981}, + url = {http://dx.doi.org/10.1007/BFb0025774}, + doi = {10.1007/BFb0025774}, + timestamp = {Fri, 10 Jun 2011 14:41:11 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/lop/ClarkeE81}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@ARTICLE{vardi94, + author = {Moshe Y. Vardi and Pierre Wolper}, + title = {Reasoning about Infinite Computations}, + journal = {Information and Computation}, + year = {1994}, + volume = {115}, + pages = {1--37} +} + +@inproceedings{cousot77, + author = {Patrick Cousot and + Radhia Cousot}, + title = {Abstract Interpretation: {A} Unified Lattice Model for Static Analysis + of Programs by Construction or Approximation of Fixpoints}, + booktitle = {Conference Record of the Fourth {ACM} Symposium on Principles of Programming + Languages, Los Angeles, California, USA, January 1977}, + pages = {238--252}, + year = {1977}, + url = {http://doi.acm.org/10.1145/512950.512973}, + doi = {10.1145/512950.512973}, + timestamp = {Mon, 21 May 2012 16:19:51 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/popl/CousotC77}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@book{gallier87, + author = {Jean H. Gallier}, + title = {Logic for Computer Science: Foundations of Automatic Theorem Proving}, + publisher = {Wiley}, + year = 1987, + isbn = {978-0-471-61546-0}, + timestamp = {Tue, 12 Apr 2011 15:08:30 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/books/daglib/0068003}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inbook{leinenbach09, +author="Leinenbach, Dirk +and Santen, Thomas", +editor="Cavalcanti, Ana +and Dams, Dennis R.", +title="Verifying the Microsoft Hyper-V Hypervisor with VCC", +bookTitle="FM 2009: Formal Methods: Second World Congress, Eindhoven, The Netherlands, November 2-6, 2009. Proceedings", +year="2009", +publisher="Springer Berlin Heidelberg", +address="Berlin, Heidelberg", +pages="806--809", +isbn="978-3-642-05089-3", +doi="10.1007/978-3-642-05089-3_51", +url="http://dx.doi.org/10.1007/978-3-642-05089-3_51" +} + +@article{leroycomp09, + author = {Xavier Leroy}, + title = {A Formally Verified Compiler Back-end}, + journal = {J. Autom. Reasoning}, + volume = {43}, + number = {4}, + pages = {363--446}, + year = {2009}, + url = {http://dx.doi.org/10.1007/s10817-009-9155-4}, + doi = {10.1007/s10817-009-9155-4}, + timestamp = {Tue, 15 Dec 2009 14:21:05 +0100}, + biburl = {http://dblp.uni-trier.de/rec/bib/journals/jar/Leroy09}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{sel4, + author = {Klein, Gerwin and Elphinstone, Kevin and Heiser, Gernot and Andronick, June and Cock, David and Derrin, Philip and Elkaduwe, Dhammika and Engelhardt, Kai and Kolanski, Rafal and Norrish, Michael and Sewell, Thomas and Tuch, Harvey and Winwood, Simon}, + title = {seL4: Formal Verification of an OS Kernel}, + booktitle = {Proceedings of the ACM SIGOPS 22Nd Symposium on Operating Systems Principles}, + series = {SOSP '09}, + year = {2009}, + isbn = {978-1-60558-752-3}, + location = {Big Sky, Montana, USA}, + pages = {207--220}, + numpages = {14}, + url = {http://doi.acm.org/10.1145/1629575.1629596}, + doi = {10.1145/1629575.1629596}, + acmid = {1629596}, + publisher = {ACM}, + address = {New York, NY, USA}, + keywords = {isabelle/hol, l4, microkernel, sel4}, +} + +@inproceedings{astree05, + author = {Patrick Cousot and + Radhia Cousot and + J{\'{e}}r{\^{o}}me Feret and + Laurent Mauborgne and + Antoine Min{\'{e}} and + David Monniaux and + Xavier Rival}, + title = {The ASTRE{\'{E}} Analyzer}, + booktitle = {Programming Languages and Systems, 14th European Symposium on Programming,ESOP + 2005, Held as Part of the Joint European Conferences on Theory and + Practice of Software, {ETAPS} 2005, Edinburgh, UK, April 4-8, 2005, + Proceedings}, + pages = {21--30}, + year = {2005}, + url = {http://dx.doi.org/10.1007/978-3-540-31987-0_3}, + doi = {10.1007/978-3-540-31987-0_3}, + timestamp = {Thu, 28 May 2015 17:23:23 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/esop/CousotCFMMMR05}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{astree03, + author = {Bruno Blanchet and + Patrick Cousot and + Radhia Cousot and + J{\'{e}}r{\^{o}}me Feret and + Laurent Mauborgne and + Antoine Min{\'{e}} and + David Monniaux and + Xavier Rival}, + title = {A Static Analyzer for Large Safety-Critical Software}, + booktitle = {Proceedings of the {ACM} {SIGPLAN} 2003 Conference on Programming + Language Design and Implementation 2003, San Diego, California, USA, + June 9-11, 2003}, + pages = {196--207}, + year = {2003}, + url = {http://doi.acm.org/10.1145/781131.781153}, + doi = {10.1145/781131.781153}, + timestamp = {Mon, 21 May 2012 16:19:51 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/pldi/BlanchetCCFMMMR03}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@incollection{cousot10, + author = {Patrick Cousot and + Radhia Cousot}, + title = {A Gentle Introduction to Formal Verification of Computer Systems by + Abstract Interpretation}, + booktitle = {Logics and Languages for Reliability and Security}, + pages = {1--29}, + year = {2010}, + url = {http://dx.doi.org/10.3233/978-1-60750-100-8-1}, + doi = {10.3233/978-1-60750-100-8-1}, + timestamp = {Wed, 14 Mar 2012 15:17:08 +0100}, + biburl = {http://dblp.uni-trier.de/rec/bib/series/natosec/CousotC10}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} +@inproceedings{cousotsurvey01, + author = {Patrick Cousot}, + title = {Abstract Interpretation Based Formal Methods and Future Challenges}, + booktitle = {Informatics - 10 Years Back. 10 Years Ahead.}, + pages = {138--156}, + year = {2001}, + url = {http://dx.doi.org/10.1007/3-540-44577-3_10}, + doi = {10.1007/3-540-44577-3_10}, + timestamp = {Thu, 23 Jun 2016 15:53:29 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/dagstuhl/Cousot01}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@book{dijkstra76, + author = {Edsger W. Dijkstra}, + title = {A Discipline of Programming}, + publisher = {Prentice-Hall}, + year = {1976}, + timestamp = {Thu, 03 Jan 2002 11:51:39 +0100}, + biburl = {http://dblp.uni-trier.de/rec/bib/books/ph/Dijkstra76}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@book{guttaghorning93, + author = {John V. Guttag and + James J. Horning and + Stephen J. Garland and + Kevin D. Jones and + A. Modet and + Jeannette M. Wing}, + title = {Larch: Languages and Tools for Formal Specification}, + series = {Texts and Monographs in Computer Science}, + publisher = {Springer}, + year = {1993}, + url = {http://dx.doi.org/10.1007/978-1-4612-2704-5}, + doi = {10.1007/978-1-4612-2704-5}, + isbn = {978-1-4612-7636-4}, + timestamp = {Mon, 12 Jan 2015 17:10:20 +0100}, + biburl = {http://dblp.uni-trier.de/rec/bib/series/mcs/GuttagHGJMW93}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@article{leavensjournal06, + author = {Gary T. Leavens and + Albert L. Baker and + Clyde Ruby}, + title = {Preliminary Design of {JML:} A Behavioral Interface Specification + Language for Java}, + journal = {{ACM} {SIGSOFT} Software Engineering Notes}, + volume = {31}, + number = {3}, + pages = {1--38}, + year = {2006}, + url = {http://doi.acm.org/10.1145/1127878.1127884}, + doi = {10.1145/1127878.1127884}, + timestamp = {Wed, 07 May 2008 08:44:52 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/journals/sigsoft/LeavensBR06}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@book{jonesvdm90, + author = {Jones, Cliff B.}, + title = {Systematic Software Development Using VDM (2Nd Ed.)}, + year = {1990}, + isbn = {0-13-880733-7}, + publisher = {Prentice-Hall, Inc.}, + address = {Upper Saddle River, NJ, USA}, +} + +@book{barnesada1997, + title={High Integrity Ada: The SPARK Approach}, + author={Barnes, J. and Praxis Critical Systems Limited}, + isbn={9780201175172}, + lccn={gb97050416}, + series={Programming Languages}, + url={https://books.google.fr/books?id=YoBGAAAAYAAJ}, + year={1997}, + publisher={Addison-Wesley} +} + +@article{cok05, + author = {David R. Cok}, + title = {Reasoning with Specifications Containing Method Calls and Model Fields}, + journal = {Journal of Object Technology}, + volume = {4}, + number = {8}, + pages = {77--103}, + year = {2005}, + url = {http://dx.doi.org/10.5381/jot.2005.4.8.a4}, + doi = {10.5381/jot.2005.4.8.a4}, + timestamp = {Fri, 19 Nov 2010 11:51:02 +0100}, + biburl = {http://dblp.uni-trier.de/rec/bib/journals/jot/Cok05}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@article{darvas06, + author = {{\'{A}}d{\'{a}}m Darvas and + Peter M{\"{u}}ller}, + title = {Reasoning About Method Calls in Interface Specifications}, + journal = {Journal of Object Technology}, + volume = {5}, + number = {5}, + pages = {59--85}, + year = {2006}, + url = {http://dx.doi.org/10.5381/jot.2006.5.5.a3}, + doi = {10.5381/jot.2006.5.5.a3}, + timestamp = {Wed, 01 Oct 2014 13:31:09 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/journals/jot/DarvasM06}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@INPROCEEDINGS{jacobs06, + author = {Bart Jacobs and Frank Piessens}, + title = {Verification of Programs with Inspector Methods}, + booktitle = {In FTfJP 2006}, + year = {2006} +} + +@inproceedings{praun03, + author = {Christoph von Praun and + Thomas R. Gross}, + title = {Static Conflict Analysis for Multi-Threaded Object-Oriented Programs}, + booktitle = {Proceedings of the {ACM} {SIGPLAN} 2003 Conference on Programming + Language Design and Implementation 2003, San Diego, California, USA, + June 9-11, 2003}, + pages = {115--128}, + year = {2003}, + url = {http://doi.acm.org/10.1145/781131.781145}, + doi = {10.1145/781131.781145}, + timestamp = {Mon, 21 May 2012 16:19:51 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/pldi/PraunG03}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{icseleavens07, + author = {Gary T. Leavens and + Peter M{\"{u}}ller}, + title = {Information Hiding and Visibility in Interface Specifications}, + booktitle = {29th International Conference on Software Engineering {(ICSE} 2007), + Minneapolis, MN, USA, May 20-26, 2007}, + pages = {385--395}, + year = {2007}, + url = {http://dx.doi.org/10.1109/ICSE.2007.44}, + doi = {10.1109/ICSE.2007.44}, + timestamp = {Tue, 08 Sep 2015 16:21:53 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/icse/LeavensM07}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{smansvericool08, + author = {Jan Smans and + Bart Jacobs and + Frank Piessens}, + title = {VeriCool: An Automatic Verifier for a Concurrent Object-Oriented Language}, + booktitle = {Formal Methods for Open Object-Based Distributed Systems, 10th {IFIP} + {WG} 6.1 International Conference, {FMOODS} 2008, Oslo, Norway, June + 4-6, 2008, Proceedings}, + pages = {220--239}, + year = {2008}, + url = {http://dx.doi.org/10.1007/978-3-540-68863-1_14}, + doi = {10.1007/978-3-540-68863-1_14}, + timestamp = {Wed, 29 Oct 2008 19:13:57 +0100}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/fmoods/SmansJP08}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{pldiZee08, + author = {Karen Zee and + Viktor Kuncak and + Martin C. Rinard}, + title = {Full Functional Verification of Linked Data Structures}, + booktitle = {Proceedings of the {ACM} {SIGPLAN} 2008 Conference on Programming + Language Design and Implementation, Tucson, AZ, USA, June 7-13, 2008}, + pages = {349--361}, + year = {2008}, + url = {http://doi.acm.org/10.1145/1375581.1375624}, + doi = {10.1145/1375581.1375624}, + timestamp = {Mon, 16 Jun 2008 08:31:44 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/pldi/ZeeKR08}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{leinotacas10, + author = {K. Rustan M. Leino and + Philipp R{\"{u}}mmer}, + title = {A Polymorphic Intermediate Verification Language: Design and Logical + Encoding}, + booktitle = {Tools and Algorithms for the Construction and Analysis of Systems, + 16th International Conference, {TACAS} 2010, Held as Part of the Joint + European Conferences on Theory and Practice of Software, {ETAPS} 2010, + Paphos, Cyprus, March 20-28, 2010. Proceedings}, + pages = {312--327}, + year = {2010}, + url = {http://dx.doi.org/10.1007/978-3-642-12002-2_26}, + doi = {10.1007/978-3-642-12002-2_26}, + timestamp = {Mon, 15 Mar 2010 17:34:39 +0100}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/tacas/LeinoR10}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{vccCohen09, + author = {Ernie Cohen and + Markus Dahlweid and + Mark A. Hillebrand and + Dirk Leinenbach and + Michal Moskal and + Thomas Santen and + Wolfram Schulte and + Stephan Tobies}, + title = {{VCC:} {A} Practical System for Verifying Concurrent {C}}, + booktitle = {Theorem Proving in Higher Order Logics, 22nd International Conference, + TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings}, + pages = {23--42}, + year = {2009}, + url = {http://dx.doi.org/10.1007/978-3-642-03359-9_2}, + doi = {10.1007/978-3-642-03359-9_2}, + timestamp = {Thu, 03 Sep 2009 22:14:13 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/tphol/CohenDHLMSST09}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@INPROCEEDINGS{reynolds00, + author = {John C. Reynolds}, + title = {Intuitionistic Reasoning about Shared Mutable Data Structure}, + booktitle = {Millennial Perspectives in Computer Science}, + year = {2000}, + pages = {303--321}, + publisher = {Palgrave} +} + +@inproceedings{parkinson06, + author = {Matthew J. Parkinson and + Richard Bornat and + Cristiano Calcagno}, + title = {Variables as Resource in Hoare Logics}, + booktitle = {21th {IEEE} Symposium on Logic in Computer Science {(LICS} 2006), + 12-15 August 2006, Seattle, WA, USA, Proceedings}, + pages = {137--146}, + year = {2006}, + url = {http://dx.doi.org/10.1109/LICS.2006.52}, + doi = {10.1109/LICS.2006.52}, + timestamp = {Fri, 21 Nov 2014 14:08:56 +0100}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/lics/ParkinsonBC06}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{berdine05, + author = {Josh Berdine and + Cristiano Calcagno and + Peter W. O'Hearn}, + title = {Smallfoot: Modular Automatic Assertion Checking with Separation Logic}, + booktitle = {Formal Methods for Components and Objects, 4th International Symposium, + {FMCO} 2005, Amsterdam, The Netherlands, November 1-4, 2005, Revised + Lectures}, + pages = {115--137}, + year = {2005}, + url = {http://dx.doi.org/10.1007/11804192_6}, + doi = {10.1007/11804192_6}, + timestamp = {Fri, 15 Dec 2006 15:37:51 +0100}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/fmco/BerdineCO05}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{distefano08, + author = {Dino Distefano and + Matthew J. Parkinson}, + title = {jStar: Towards Practical Verification for {Java}}, + booktitle = {Proceedings of the 23rd Annual {ACM} {SIGPLAN} Conference on Object-Oriented + Programming, Systems, Languages, and Applications, {OOPSLA} 2008, + October 19-23, 2008, Nashville, TN, {USA}}, + pages = {213--226}, + year = {2008}, + url = {http://doi.acm.org/10.1145/1449764.1449782}, + doi = {10.1145/1449764.1449782}, + timestamp = {Mon, 27 Oct 2008 11:12:10 +0100}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/oopsla/DistefanoP08}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{jacobs10, + author = {Bart Jacobs and + Jan Smans and + Frank Piessens}, + title = {A Quick Tour of the VeriFast Program Verifier}, + booktitle = {Programming Languages and Systems - 8th Asian Symposium, {APLAS} 2010, + Shanghai, China, November 28 - December 1, 2010. Proceedings}, + pages = {304--311}, + year = {2010}, + url = {http://dx.doi.org/10.1007/978-3-642-17164-2_21}, + doi = {10.1007/978-3-642-17164-2_21}, + timestamp = {Mon, 02 Dec 2013 10:51:48 +0100}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/aplas/JacobsSP10}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{jacobs11, + author = {Bart Jacobs and + Jan Smans and + Pieter Philippaerts and + Fr{\'{e}}d{\'{e}}ric Vogels and + Willem Penninckx and + Frank Piessens}, + title = {VeriFast: {A} Powerful, Sound, Predictable, Fast Verifier for {C} + and Java}, + booktitle = {{NASA} Formal Methods - Third International Symposium, {NFM} 2011, + Pasadena, CA, USA, April 18-20, 2011. Proceedings}, + pages = {41--55}, + year = {2011}, + url = {http://dx.doi.org/10.1007/978-3-642-20398-5_4}, + doi = {10.1007/978-3-642-20398-5_4}, + timestamp = {Mon, 02 Dec 2013 10:51:44 +0100}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/nfm/JacobsSPVPP11}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{leinosmans09, + author = {K. Rustan M. Leino and + Peter M{\"{u}}ller and + Jan Smans}, + title = {Verification of Concurrent Programs with Chalice}, + booktitle = {Foundations of Security Analysis and Design V, {FOSAD} 2007/2008/2009 + Tutorial Lectures}, + pages = {195--222}, + year = {2009}, + url = {http://dx.doi.org/10.1007/978-3-642-03829-7_7}, + doi = {10.1007/978-3-642-03829-7_7}, + timestamp = {Wed, 01 Oct 2014 13:31:09 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/fosad/LeinoMS09}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{drossopoulou08, + author = {Sophia Drossopoulou and + Adrian Francalanza and + Peter M{\"{u}}ller and + Alexander J. Summers}, + title = {A Unified Framework for Verification Techniques for Object Invariants}, + booktitle = {{ECOOP} 2008 - Object-Oriented Programming, 22nd European Conference, + Paphos, Cyprus, July 7-11, 2008, Proceedings}, + pages = {412--437}, + year = {2008}, + url = {http://dx.doi.org/10.1007/978-3-540-70592-5_18}, + doi = {10.1007/978-3-540-70592-5_18}, + timestamp = {Wed, 01 Oct 2014 13:31:09 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/ecoop/DrossopoulouFMS08}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@article{mullerheffter06, + author = {Peter M{\"{u}}ller and + Arnd Poetzsch{-}Heffter and + Gary T. Leavens}, + title = {Modular Invariants for Layered Object Structures}, + journal = {Sci. Comput. Program.}, + volume = {62}, + number = {3}, + pages = {253--286}, + year = {2006}, + url = {http://dx.doi.org/10.1016/j.scico.2006.03.001}, + doi = {10.1016/j.scico.2006.03.001}, + timestamp = {Wed, 01 Oct 2014 13:31:08 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/journals/scp/MullerPL06}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{lu07, + author = {Yi Lu and + John Potter and + Jingling Xue}, + title = {Validity Invariants and Effects}, + booktitle = {{ECOOP} 2007 - Object-Oriented Programming, 21st European Conference, + Berlin, Germany, July 30 - August 3, 2007, Proceedings}, + pages = {202--226}, + year = {2007}, + url = {http://dx.doi.org/10.1007/978-3-540-73589-2_11}, + doi = {10.1007/978-3-540-73589-2_11}, + timestamp = {Fri, 16 Jul 2010 10:49:57 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/ecoop/LuPX07}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@article{dietl05, + author = {Werner Dietl and + Peter M{\"{u}}ller}, + title = {Universes: Lightweight Ownership for {JML}}, + journal = {Journal of Object Technology}, + volume = {4}, + number = {8}, + pages = {5--32}, + year = {2005}, + url = {http://dx.doi.org/10.5381/jot.2005.4.8.a1}, + doi = {10.5381/jot.2005.4.8.a1}, + timestamp = {Wed, 01 Oct 2014 13:31:08 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/journals/jot/DietlM05}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{leinomulleresop09, + author = {K. Rustan M. Leino and + Peter M{\"{u}}ller}, + title = {A Basis for Verifying Multi-threaded Programs}, + booktitle = {Programming Languages and Systems, 18th European Symposium on Programming, + {ESOP} 2009, Held as Part of the Joint European Conferences on Theory + and Practice of Software, {ETAPS} 2009, York, UK, March 22-29, 2009. + Proceedings}, + pages = {378--393}, + year = {2009}, + url = {http://dx.doi.org/10.1007/978-3-642-00590-9_27}, + doi = {10.1007/978-3-642-00590-9_27}, + timestamp = {Wed, 01 Oct 2014 13:31:09 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/esop/LeinoM09}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{berdine11, + author = {Josh Berdine and + Byron Cook and + Samin Ishtiaq}, + title = {SLAyer: Memory Safety for Systems-Level Code}, + booktitle = {Computer Aided Verification - 23rd International Conference, {CAV} + 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings}, + pages = {178--183}, + year = {2011}, + url = {http://dx.doi.org/10.1007/978-3-642-22110-1_15}, + doi = {10.1007/978-3-642-22110-1_15}, + timestamp = {Mon, 11 Jul 2011 13:24:02 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/cav/BerdineCI11}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@article{berdine12, + author = {Josh Berdine and + Cristiano Calcagno and + Peter W. O'Hearn}, + title = {Verification Condition Generation and Variable Conditions in Smallfoot}, + journal = {CoRR}, + volume = {abs/1204.4804}, + year = {2012}, + url = {http://arxiv.org/abs/1204.4804}, + timestamp = {Wed, 10 Oct 2012 21:28:51 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/journals/corr/abs-1204-4804}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{naudziuniene11, + author = {Daiva Naudziuniene and + Matko Botincan and + Dino Distefano and + Mike Dodds and + Radu Grigore and + Matthew J. Parkinson}, + title = {jStar-Eclipse: An {IDE} for Automated Verification of Java Programs}, + booktitle = {SIGSOFT/FSE'11 19th {ACM} {SIGSOFT} Symposium on the Foundations of + Software Engineering {(FSE-19)} and ESEC'11: 13th European Software + Engineering Conference (ESEC-13), Szeged, Hungary, September 5-9, + 2011}, + pages = {428--431}, + year = {2011}, + url = {http://doi.acm.org/10.1145/2025113.2025182}, + doi = {10.1145/2025113.2025182}, + timestamp = {Mon, 11 Jul 2016 18:16:25 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/sigsoft/NaudziunieneBDDGP11}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{calcagnodis08, + author = {Cristiano Calcagno and + Dino Distefano and + Peter W. O'Hearn and + Hongseok Yang}, + title = {Space Invading Systems Code}, + booktitle = {Logic-Based Program Synthesis and Transformation, 18th International + Symposium, {LOPSTR} 2008, Valencia, Spain, July 17-18, 2008, Revised + Selected Papers}, + pages = {1--3}, + year = {2008}, + url = {http://dx.doi.org/10.1007/978-3-642-00515-2_1}, + doi = {10.1007/978-3-642-00515-2_1}, + timestamp = {Tue, 17 Mar 2009 22:48:28 +0100}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/lopstr/CalcagnoDOY08}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{calcagnonfm11, + author = {Cristiano Calcagno and + Dino Distefano}, + title = {Infer: An Automatic Program Verifier for Memory Safety of {C} Programs}, + booktitle = {{NASA} Formal Methods - Third International Symposium, {NFM} 2011, + Pasadena, CA, USA, April 18-20, 2011. Proceedings}, + pages = {459--465}, + year = {2011}, + url = {http://dx.doi.org/10.1007/978-3-642-20398-5_33}, + doi = {10.1007/978-3-642-20398-5_33}, + timestamp = {Mon, 09 May 2011 12:29:08 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/nfm/CalcagnoD11}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{infer11, + author = {Cristiano Calcagno and + Dino Distefano}, + title = {Infer: An Automatic Program Verifier for Memory Safety of {C} Programs}, + booktitle = {{NASA} Formal Methods - Third International Symposium, {NFM} 2011, + Pasadena, CA, USA, April 18-20, 2011. Proceedings}, + pages = {459--465}, + year = {2011}, + url = {http://dx.doi.org/10.1007/978-3-642-20398-5_33}, + doi = {10.1007/978-3-642-20398-5_33}, + timestamp = {Mon, 09 May 2011 12:29:08 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/nfm/CalcagnoD11}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{barnettspec05, + author = {Michael Barnett and + Robert DeLine and + Manuel F{\"{a}}hndrich and + Bart Jacobs and + K. Rustan M. Leino and + Wolfram Schulte and + Herman Venter}, + title = {The Spec{\#} Programming System: Challenges and Directions}, + booktitle = {Verified Software: Theories, Tools, Experiments, First {IFIP} {TC} + 2/WG 2.3 Conference, {VSTTE} 2005, Zurich, Switzerland, October 10-13, + 2005, Revised Selected Papers and Discussions}, + pages = {144--152}, + year = {2005}, + url = {http://dx.doi.org/10.1007/978-3-540-69149-5_16}, + doi = {10.1007/978-3-540-69149-5_16}, + timestamp = {Fri, 22 May 2015 07:12:28 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/vstte/BarnettDFJLSV05}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{barnettboogie05, + author = {Michael Barnett and + Bor{-}Yuh Evan Chang and + Robert DeLine and + Bart Jacobs and + K. Rustan M. Leino}, + title = {Boogie: {A} Modular Reusable Verifier for Object-Oriented Programs}, + booktitle = {Formal Methods for Components and Objects, 4th International Symposium, + {FMCO} 2005, Amsterdam, The Netherlands, November 1-4, 2005, Revised + Lectures}, + pages = {364--387}, + year = {2005}, + url = {http://dx.doi.org/10.1007/11804192_17}, + doi = {10.1007/11804192_17}, + timestamp = {Fri, 22 May 2015 07:12:28 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/fmco/BarnettCDJL05}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{mouraz308, + author = {Leonardo Mendon{\c{c}}a de Moura and + Nikolaj Bj{\o}rner}, + title = {{Z3:} An Efficient {SMT} Solver}, + booktitle = {Tools and Algorithms for the Construction and Analysis of Systems, + 14th International Conference, {TACAS} 2008, Held as Part of the Joint + European Conferences on Theory and Practice of Software, {ETAPS} 2008, + Budapest, Hungary, March 29-April 6, 2008. Proceedings}, + pages = {337--340}, + year = {2008}, + url = {http://dx.doi.org/10.1007/978-3-540-78800-3_24}, + doi = {10.1007/978-3-540-78800-3_24}, + timestamp = {Thu, 28 May 2015 17:23:18 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/tacas/MouraB08}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@article{barnett11, + author = {Mike Barnett and + Manuel F{\"{a}}hndrich and + K. Rustan M. Leino and + Peter M{\"{u}}ller and + Wolfram Schulte and + Herman Venter}, + title = {Specification and Verification: The Spec{\#} Experience}, + journal = {Commun. {ACM}}, + volume = {54}, + number = {6}, + pages = {81--91}, + year = {2011}, + url = {http://doi.acm.org/10.1145/1953122.1953145}, + doi = {10.1145/1953122.1953145}, + timestamp = {Wed, 01 Oct 2014 13:31:09 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/journals/cacm/BarnettFLMSV11}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@misc{boogie2, +author = {K. Rustan M. Leino}, +title = {This is Boogie 2, Boogie Reference Manual}, +url = {http://research.microsoft.com/en-us/um/people/leino/papers/krml178.pdf} +} + +@article{wing87, + author = {Jeannette M. Wing}, + title = {Writing Larch Interface Language Specifications}, + journal = {{ACM} Trans. Program. Lang. Syst.}, + volume = {9}, + number = {1}, + pages = {1--24}, + year = {1987}, + url = {http://doi.acm.org/10.1145/9758.10500}, + doi = {10.1145/9758.10500}, + timestamp = {Mon, 03 Apr 2006 11:19:31 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/journals/toplas/Wing87}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@article{burdy05, + author = {Lilian Burdy and + Yoonsik Cheon and + David R. Cok and + Michael D. Ernst and + Joseph R. Kiniry and + Gary T. Leavens and + K. Rustan M. Leino and + Erik Poll}, + title = {An Overview of {JML} Tools and Applications}, + journal = {{STTT}}, + volume = {7}, + number = {3}, + pages = {212--232}, + year = {2005}, + url = {http://dx.doi.org/10.1007/s10009-004-0167-4}, + doi = {10.1007/s10009-004-0167-4}, + timestamp = {Mon, 08 Aug 2005 13:49:44 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/journals/sttt/BurdyCCEKLLP05}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{chalin05, + author = {Patrice Chalin and + Joseph R. Kiniry and + Gary T. Leavens and + Erik Poll}, + title = {Beyond Assertions: Advanced Specification and Verification with {JML} + and ESC/Java2}, + booktitle = {Formal Methods for Components and Objects, 4th International Symposium, + {FMCO} 2005, Amsterdam, The Netherlands, November 1-4, 2005, Revised + Lectures}, + pages = {342--363}, + year = {2005}, + url = {http://dx.doi.org/10.1007/11804192_16}, + doi = {10.1007/11804192_16}, + timestamp = {Fri, 15 Dec 2006 15:37:51 +0100}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/fmco/ChalinKLP05}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@misc{krakatoa16, +author = {Claude Marché}, +title = {The Krakatoa Verification Tool for Java Programs, Krakatoa Tutorial and Reference Manual}, +year = {2016}, +url = {http://krakatoa.lri.fr/krakatoa.pdf} +} + +@article{marche04, + author = {Claude March{\'{e}} and + Christine Paulin{-}Mohring and + Xavier Urbain}, + title = {The {KRAKATOA} Tool for Certification of {JAVA/JAVACARD} Programs Annotated + in {JML}}, + journal = {J. Log. Algebr. Program.}, + volume = {58}, + number = {1-2}, + pages = {89--106}, + year = {2004}, + url = {http://dx.doi.org/10.1016/j.jlap.2003.07.006}, + doi = {10.1016/j.jlap.2003.07.006}, + timestamp = {Mon, 21 Feb 2005 12:26:33 +0100}, + biburl = {http://dblp.uni-trier.de/rec/bib/journals/jlp/MarchePU04}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{filliatre07, + author = {Jean{-}Christophe Filli{\^{a}}tre and + Claude March{\'{e}}}, + title = {The Why/Krakatoa/Caduceus Platform for Deductive Program Verification}, + booktitle = {Computer Aided Verification, 19th International Conference, {CAV} + 2007, Berlin, Germany, July 3-7, 2007, Proceedings}, + pages = {173--177}, + year = {2007}, + url = {http://dx.doi.org/10.1007/978-3-540-73368-3_21}, + doi = {10.1007/978-3-540-73368-3_21}, + timestamp = {Mon, 03 Sep 2007 13:24:22 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/cav/FilliatreM07}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{filliatre13, + author = {Jean{-}Christophe Filli{\^{a}}tre and + Andrei Paskevich}, + title = {Why3 - Where Programs Meet Provers}, + booktitle = {Programming Languages and Systems - 22nd European Symposium on Programming, + {ESOP} 2013, Held as Part of the European Joint Conferences on Theory + and Practice of Software, {ETAPS} 2013, Rome, Italy, March 16-24, + 2013. Proceedings}, + pages = {125--128}, + year = {2013}, + url = {http://dx.doi.org/10.1007/978-3-642-37036-6_8}, + doi = {10.1007/978-3-642-37036-6_8}, + timestamp = {Mon, 18 Feb 2013 15:03:29 +0100}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/esop/FilliatreP13}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@article{bobot15, + author = {Fran{\c{c}}ois Bobot and + Jean{-}Christophe Filli{\^{a}}tre and + Claude March{\'{e}} and + Andrei Paskevich}, + title = {Let's verify this with Why3}, + journal = {{STTT}}, + volume = {17}, + number = {6}, + pages = {709--727}, + year = {2015}, + url = {http://dx.doi.org/10.1007/s10009-014-0314-5}, + doi = {10.1007/s10009-014-0314-5}, + timestamp = {Tue, 13 Oct 2015 11:22:21 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/journals/sttt/BobotFMP15}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@incollection{dafnyguide12, + author = {Jason Koenig and + K. Rustan M. Leino}, + title = {Getting Started with Dafny: {A} Guide}, + booktitle = {Software Safety and Security - Tools for Analysis and Verification}, + pages = {152--181}, + year = {2012}, + url = {http://dx.doi.org/10.3233/978-1-61499-028-4-152}, + doi = {10.3233/978-1-61499-028-4-152}, + timestamp = {Tue, 30 Sep 2014 10:20:05 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/series/natosec/KoenigL12}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{specguide08, + author = {K. Rustan M. Leino and + Peter M{\"{u}}ller}, + title = {Using the Spec{\#} Language, Methodology, and Tools to Write Bug-Free + Programs}, + booktitle = {Advanced Lectures on Software Engineering, {LASER} Summer School 2007/2008}, + pages = {91--139}, + year = {2008}, + url = {http://dx.doi.org/10.1007/978-3-642-13010-6_4}, + doi = {10.1007/978-3-642-13010-6_4}, + timestamp = {Wed, 01 Oct 2014 13:31:09 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/laser/LeinoM08}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@article{banerjee13, + author = {Anindya Banerjee and + David A. Naumann and + Stan Rosenberg}, + title = {Local Reasoning for Global Invariants, Part {I:} Region Logic}, + journal = {J. {ACM}}, + volume = {60}, + number = {3}, + pages = {18:1--18:56}, + year = {2013}, + url = {http://doi.acm.org/10.1145/2485982}, + doi = {10.1145/2485982}, + timestamp = {Fri, 06 Jan 2017 11:28:53 +0100}, + biburl = {http://dblp.uni-trier.de/rec/bib/journals/jacm/BanerjeeNR13}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@Inbook{banerjeeregions2008, +author="Banerjee, Anindya +and Barnett, Mike +and Naumann, David A.", +editor="Shankar, Natarajan +and Woodcock, Jim", +title="Boogie Meets Regions: A Verification Experience Report ", +bookTitle="Verified Software: Theories, Tools, Experiments: Second International Conference, VSTTE 2008, Toronto, Canada, October 6-9, 2008. Proceedings", +year="2008", +publisher="Springer Berlin Heidelberg", +address="Berlin, Heidelberg", +pages="177--191", +isbn="978-3-540-87873-5", +doi="10.1007/978-3-540-87873-5_16", +url="http://dx.doi.org/10.1007/978-3-540-87873-5_16" +} + +@article{sozeau09, + author = {Matthieu Sozeau}, + title = {A New Look at Generalized Rewriting in Type Theory}, + journal = {J. Formalized Reasoning}, + volume = {2}, + number = {1}, + pages = {41--62}, + year = {2009}, + url = {http://dx.doi.org/10.6092/issn.1972-5787/1574}, + doi = {10.6092/issn.1972-5787/1574}, + timestamp = {Mon, 13 Jan 2014 12:51:50 +0100}, + biburl = {http://dblp.uni-trier.de/rec/bib/journals/jfrea/Sozeau09}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{marcheP05, + author = {Claude March{\'{e}} and + Christine Paulin{-}Mohring}, + title = {Reasoning About Java Programs with Aliasing and Frame Conditions}, + booktitle = {Theorem Proving in Higher Order Logics, 18th International Conference, + TPHOLs 2005, Oxford, UK, August 22-25, 2005, Proceedings}, + pages = {179--194}, + year = {2005}, + url = {http://dx.doi.org/10.1007/11541868_12}, + doi = {10.1007/11541868_12}, + timestamp = {Thu, 15 Sep 2005 14:56:48 +0200}, + biburl = {http://dblp2.uni-trier.de/rec/bib/conf/tphol/MarcheP05}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{catano03, + author = {N{\'{e}}stor Cata{\~{n}}o and + Marieke Huisman}, + title = {{CHASE:} {A} Static Checker for JML's Assignable Clause}, + booktitle = {Verification, Model Checking, and Abstract Interpretation, 4th International + Conference, {VMCAI} 2003, New York, NY, USA, January 9-11, 2002, Proceedings}, + pages = {26--40}, + year = {2003}, + url = {http://dx.doi.org/10.1007/3-540-36384-X_6}, + doi = {10.1007/3-540-36384-X_6}, + timestamp = {Mon, 04 Jul 2011 09:38:53 +0200}, + biburl = {http://dblp2.uni-trier.de/rec/bib/conf/vmcai/CatanoH03}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{berg01, + author = {Joachim van den Berg and + Bart Jacobs}, + title = {The {LOOP} Compiler for Java and {JML}}, + booktitle = {Tools and Algorithms for the Construction and Analysis of Systems, + 7th International Conference, {TACAS} 2001 Held as Part of the Joint + European Conferences on Theory and Practice of Software, {ETAPS} 2001 + Genova, Italy, April 2-6, 2001, Proceedings}, + pages = {299--312}, + year = {2001}, + url = {http://dx.doi.org/10.1007/3-540-45319-9_21}, + doi = {10.1007/3-540-45319-9_21}, + timestamp = {Thu, 09 Jul 2015 16:49:47 +0200}, + biburl = {http://dblp2.uni-trier.de/rec/bib/conf/tacas/BergJ01}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{lehner10, + author = {Hermann Lehner and + Peter M{\"{u}}ller}, + title = {Efficient Runtime Assertion Checking of Assignable Clauses with Datagroups}, + booktitle = {Fundamental Approaches to Software Engineering, 13th International + Conference, {FASE} 2010, Held as Part of the Joint European Conferences + on Theory and Practice of Software, {ETAPS} 2010, Paphos, Cyprus, + March 20-28, 2010. Proceedings}, + pages = {338--352}, + year = {2010}, + url = {http://dx.doi.org/10.1007/978-3-642-12029-9_24}, + doi = {10.1007/978-3-642-12029-9_24}, + timestamp = {Wed, 01 Oct 2014 13:31:09 +0200}, + biburl = {http://dblp2.uni-trier.de/rec/bib/conf/fase/LehnerM10}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@book{sozeaucoq2016, + title={The Coq Proof Assistant Reference Manual: Version 8.6}, + author={Matthieu Sozeau and the COQ development team}, + year={1997}, + month = dec, + publisher={Inria}, +} + +@inproceedings{remypopl97, + author = {Didier R{\'{e}}my and + Jerome Vouillon}, + title = {Objective {ML:} {A} Simple Object-Oriented Extension of {ML}}, + booktitle = {Conference Record of POPL'97: The 24th {ACM} {SIGPLAN-SIGACT} Symposium + on Principles of Programming Languages, Papers Presented at the Symposium, + Paris, France, 15-17 January 1997}, + pages = {40--53}, + year = {1997}, + url = {http://doi.acm.org/10.1145/263699.263707}, + doi = {10.1145/263699.263707}, + timestamp = {Mon, 10 Dec 2012 15:26:39 +0100}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/popl/RemyV97}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@article{bertrane15, + author = {Julien Bertrane and + Patrick Cousot and + Radhia Cousot and + J{\'{e}}r{\^{o}}me Feret and + Laurent Mauborgne and + Antoine Min{\'{e}} and + Xavier Rival}, + title = {Static Analysis and Verification of Aerospace Software by Abstract + Interpretation}, + journal = {Foundations and Trends in Programming Languages}, + volume = {2}, + number = {2-3}, + pages = {71--190}, + year = {2015}, + url = {http://dx.doi.org/10.1561/2500000002}, + doi = {10.1561/2500000002}, + timestamp = {Fri, 18 Mar 2016 13:52:58 +0100}, + biburl = {http://dblp.uni-trier.de/rec/bib/journals/ftpl/BertraneCCFMMR15}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{delmas07, + author = {David Delmas and + Jean Souyris}, + title = {Astr{\'{e}}e: From Research to Industry}, + booktitle = {Static Analysis, 14th International Symposium, {SAS} 2007, Kongens + Lyngby, Denmark, August 22-24, 2007, Proceedings}, + pages = {437--451}, + year = {2007}, + crossref = {DBLP:conf/sas/2007}, + url = {http://dx.doi.org/10.1007/978-3-540-74061-2_27}, + doi = {10.1007/978-3-540-74061-2_27}, + timestamp = {Thu, 23 Aug 2007 13:57:38 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/sas/DelmasS07}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{cousottase07, + author = {Patrick Cousot and + Radhia Cousot and + J{\'{e}}r{\^{o}}me Feret and + Antoine Min{\'{e}} and + Laurent Mauborgne and + David Monniaux and + Xavier Rival}, + title = {Varieties of Static Analyzers: {A} Comparison with {ASTREE}}, + booktitle = {First Joint {IEEE/IFIP} Symposium on Theoretical Aspects of Software + Engineering, {TASE} 2007, June 5-8, 2007, Shanghai, China}, + pages = {3--20}, + year = {2007}, + crossref = {DBLP:conf/tase/2007}, + url = {http://dx.doi.org/10.1109/TASE.2007.55}, + doi = {10.1109/TASE.2007.55}, + timestamp = {Mon, 01 Dec 2014 19:24:57 +0100}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/tase/CousotCFMMMR07}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{bouissou09, + author={Bouissou, O{.} and Conquet, {\'E}{.} and Cousot, P{.} and Cousot, R{.} and Feret, J{.} and Ghorbal, K{.} and Goubault, {\'E}{.} and Lesens, D{.} and Mauborgne, L{.} and Min{\'e}, A{.} and Putot, S{.} and Rival, X{.} and Turin, M{.}}, + title={Space Software Validation using Abstract Interpretation}, + booktitle={Proc{.}~of the International Space System Engineering Conference on Data Systems in Aerospace (DASIA 2009)}, + year={2009}, + pages={7}, + volume={SP-669}, + month={May}, + location={Istambul, Turkey}, + publisher={ESA}, + note={\url{http://www-apr.lip6.fr/~mine/publi/article-bouissou-al-dasia09.pdf}}, + doi={1921532.1921553}, +} + +@article{ouadjaout16, + author = {Abdelraouf Ouadjaout and + Antoine Min{\'{e}} and + Noureddine Lasla and + Nadjib Badache}, + title = {Static Analysis by Abstract Interpretation of Functional Properties + of Device Drivers in TinyOS}, + journal = {Journal of Systems and Software}, + volume = {120}, + pages = {114--132}, + year = {2016}, + url = {http://dx.doi.org/10.1016/j.jss.2016.07.030}, + doi = {10.1016/j.jss.2016.07.030}, + timestamp = {Tue, 11 Oct 2016 15:01:57 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/journals/jss/OuadjaoutMLB16}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} \ No newline at end of file diff --git a/dependency-macros.tex b/dependency-macros.tex new file mode 100644 index 0000000..be7e94e --- /dev/null +++ b/dependency-macros.tex @@ -0,0 +1,244 @@ +%%% Macros %%% + +%% % Values + +%% %Variant Values +%% \newcommand{\plainvval}[4] +%% {\ensuremath{#1_{#2}[#3_{#4}] }} + +%% \newcommand{\plainvvalindex}[1] +%% {\ensuremath{C_{#1}[v_{#1}]}} + +%% \def\commonvval{\plainvval{C}{i}{v}{i}} + + +%% Dependency macros + +%% \addto\captionsenglish{ +%% \renewcommand{\tablename}{Figure} +%% } +\newcolumntype{L}[1]{>{\raggedright}m{#1}} +%misc macros +\newcommand{\comment}[1]{\ifdraft{\small\textbf{#1}}{}} + +\def\inputs{\ensuremath{\mathcal{I}}} +\def\writ{\mathscr{V}^{+}} + +\newcommand\mmyrbox[2][fill=red!20]{% + \tikz[baseline]\node[% + inner ysep=0pt, + inner xsep=2pt, + anchor=text, + rectangle, + rounded corners=1mm, + #1] {\strut#2};% +} + +\newcommand\mmygbox[2][fill=lightgray!30]{% + \tikz[baseline]\node[% + inner ysep=0pt, + inner xsep=2pt, + anchor=text, + rectangle, + rounded corners=1mm, + #1] {\strut#2};% +} + +\def\everything{\ensuremath \top} +\def\nothing{\ensuremath \oslash} +\def\impossible{\ensuremath \bot} + +%dependency domain macros +\def\udep{\mathcal{D}} +\def\dom{\mathit{\delta}} +\newcommand{\structdom}[2]{\{#1; \ldots; #2\}} +\newcommand{\vardom}[2]{[#1; \ldots; #2]} +\newcommand{\adom}[1]{\langle #1 \rangle} +\newcommand{\aexcdom}[3]{\langle #1 \triangleright #2: \; #3 \rangle} +\newcommand{\adomusual}{\langle \dom_{\mathit{def}} \triangleright i \;: \; \dom_{\mathit{exc}} \rangle} +\newcommand{\addef}{\langle \dom_{\mathit{def}} \triangleright i \;: \; \dom_{\mathit{exc}} \rangle} + +\newcommand{\dstruct}[1]{f_{#1} \mapsto \dom_{#1}} +\newcommand{\dostruct}[1]{f_{#1} \mapsto \dom'_{#1}} +\newcommand{\djstruct}[1]{f_{#1} \mapsto \dom_{#1} \vee \dom'_{#1}} +\newcommand{\djnothingstruct}[1]{f_{#1} \mapsto \oslash \vee \dom_{#1}} +\newcommand{\dmstruct}[1]{f_{#1} \mapsto \dom_{#1} \oplus \dom'_{#1}} + + +\newcommand{\dvar}[1]{C_{#1} \mapsto \dom_{#1}} +\newcommand{\dovar}[1]{C_{#1} \mapsto \dom'_{#1}} +\newcommand{\djvar}[1]{C_{#1} \mapsto \dom_{#1} \vee \dom'_{#1}} +\newcommand{\djnothingvar}[1]{C_{#1} \mapsto \oslash \vee \dom_{#1}} +\newcommand{\dmvar}[1]{C_{#1} \mapsto \dom_{#1} \oplus \dom'_{#1}} + +\newcommand{\deferred}[1]{\textrm{\textbf{\textsf{Deferred}}}(#1)} + + +\newcommand{\subst}{\blacktriangleleft(\sigma, \phi)} + +\def\ddef {\ensuremath{\mathit{\dom_{def}}}} +\def\dexc {\ensuremath{\mathit{\dom_{exc}}}} +\def\dodef{\ensuremath{\mathit{\dom'_{def}}}} +\def\doexc{\ensuremath{\mathit{\dom'_{exc}}}} + +\def\dleq{\sqsubseteq} + +%intra macros +\def\intra{\Delta} + +%inter macro +\def\inter{\mathscr{D}} +%% \def\defstruct{ \{.f_1\pi_1, \; \ldots, \; .f_n\pi_n\} } +%% \def\defstructo{ \{.f_1\pi'_1, \; \ldots, \; .f_n\pi'_n\} } +%% \def\defvar{[@C_1\pi_1, \; \ldots, \;@C_n\pi_n]} +%% \def\defvaro{[@C_1\pi'_1, \; \ldots, \;@C_n\pi'_n]} +%% \def\defcell{\langle i \rangle \pi_{\mathit{exc}}} +%% \def\defcello{\langle i \rangle \pi'_{\mathit{exc}}} +%% \def\defout{\langle * \setminus i \rangle \pi_{\mathit{out}}} +%% \def\defouto{\langle * \setminus i \rangle \pi'_{\mathit{out}}} +%% \def\defarr{\langle * \rangle \pi_{\mathit{def}}} +%% \def\defarro{\langle * \rangle \pi'_{\mathit{def}}} +%% \def\pexc{\pi_{\mathit{exc}}} +%% \def\pdef{\pi_{\mathit{def}}} +%% \def\piout{\pi_{\mathit{out}}} +%% \def\pleq{\underset{\circ}{\dleq}} +%% \def\pjoin{\underset{\circ}{\vee}} +%% \def\pf{\underset{\circ}{.f}} +%% \def\pc{\underset{\circ}{@C}} +%% \def\pind{\underset{\circ}{\langle i \rangle}} +%% \def\pout{\underset{\circ}{\langle * \setminus i \rangle}} +%% \def\parr{\underset{\circ}{\langle * \rangle}} +%% \def\wtpath{\underset{\circ}{\vdash}} +%% \def\wfpath{\underset{\circ}{\vDash}} +%% \def\app{\mathit{::}\pi_a } +%% \def\appf{\mathit{::}.f } +%% \def\appc{\mathit{::}@C } +%% \def\appa{\mathit{::}\langle * \rangle} +%% \def\appo{\mathit{::}\langle * \setminus i \rangle} +%% \def\appi{\mathit{::}\langle i \rangle} + +%equations macros +\newcommand{\transfer}[3]{\llbracket#2\rrbracket_{#3}(#1)} +\newcommand{\killo}[2]{(\intra_{#1} \setminus #2)} +\def\binlabels{ + \begin{tabular}{@{}l@{}} +$\lambda_{true}$ \\\\ +$\lambda_{false}$ \\ +\end{tabular} } +\def\ltrue{\lambda_{true}} + +%join comment macros +\def\veps{\varepsilon} +\def\vepsi{\varepsilon_i} +\def\eei{(\varepsilon \vee \varepsilon_i)} +\def\ddj{(\delta \vee \delta_j)} + +%projection macros +\newcommand{\projcell}[1][i]{\langle#1\rangle} +\newcommand{\projext}[1][i]{\langle * \setminus#1\rangle} +\def\projarr{\langle * \rangle} + +%paths macros +%% \def\arrpath{\langle * \rangle} +%% \def\cellpath{\langle i \rangle} +%% \def\outpath{\langle * \setminus i \rangle} + +%wf +\def\inps{\mathcal{I}} +\def\outs{\mathcal{O}} + +% tabular column +\newcolumntype{L}[1]{>{\raggedright\let\newline\\\arraybackslash\hspace{0pt}}m{#1}} + + +% tikz figures for example +% Preparation for Variant, Structure and Array diagrams with arrows and red and green + +\def\tmul{*1mm} +\def\dtriangle#1#2#3#4#5{% + \tikz[remember picture, baseline={(dottriangle-x#1.base)}]{% + \node[inner sep=0pt] (dottriangle-x#1) {\phantom{$x$}};% + \node[dot,#2] (dottriangle-dot#1) at ($(dottriangle-x#1.base)!.5!(dottriangle-x#1.north)$) {};% + %% The anchors and size of the isosceles triangle are not well positionned. + % \node[draw, shape=isosceles triangle, shape border rotate=90, anchor=north,#2,isosceles triangle stretches,inner sep=0pt,minimum width=#3\tmul,minimum height=#4\tmul] (t) at (dot.center) {}; + \draw[#2] (dottriangle-dot#1.center) -- ++(.5*#3\tmul,-#4\tmul) coordinate (dottriangle-te#1) -- ++(-#3\tmul,0) coordinate (dottriangle-tw#1) -- cycle; + \coordinate (dottriangle-tc#1) at (barycentric cs:dottriangle-dot#1=1,dottriangle-te#1=1,dottriangle-tw#1=1); + \begin{pgfonlayer}{background} + \node[fit=(dottriangle-dot#1) (dottriangle-te#1) (dottriangle-tw#1),#5] (dottriangle-bg#1) {}; + \end{pgfonlayer} + }% +} + +\def\defaultinnersep{1.3mm} +\tikzset{ + resetinnersep/.style={inner sep=\defaultinnersep,}, +} + +\def\dottriangle#1#2#3#4#5#6{% + \node[resetinnersep,inner sep=0pt,anchor=base west,opacity=0] (predottriangle-x-#2) at #1 {\phantom{$x$}};% + \node[resetinnersep,dot,anchor=south,#3,xshift=.5*#4\tmul,opacity=0] (predottriangle-dot-#2) at (predottriangle-x-#2.base west) {};% + %% The anchors and size of the isosceles triangle are not well positionned. + % \node[draw, shape=isosceles triangle, shape border rotate=90, anchor=north,#3,isosceles triangle stretches,inner sep=0pt,minimum width=#4\tmul,minimum height=#5\tmul] (t) at (dot.center) {}; + \draw[resetinnersep,#3,opacity=0] (predottriangle-dot-#2.center) -- ++(.5*#4\tmul,-#5\tmul) coordinate (predottriangle-te-#2) -- ++(-#4\tmul,0) coordinate (predottriangle-tw-#2) -- cycle; +%%%%%%%%%%%% + % \begin{pgfonlayer}{background} + \node[resetinnersep,fit=(predottriangle-dot-#2) (predottriangle-te-#2) (predottriangle-tw-#2)] (dottriangle-isep-#2) {}; + \node[inner sep=.7mm,fit=(predottriangle-dot-#2) (predottriangle-te-#2) (predottriangle-tw-#2),#6] (dottriangle-bg-#2) {}; + % \end{pgfonlayer} +%%%%%%%%%%%% same as above, but put above the background. + \node[resetinnersep,inner sep=0pt,anchor=base west] (dottriangle-x-#2) at #1 {\phantom{$x$}};% + \node[resetinnersep,dot,anchor=south,#3,xshift=.5*#4\tmul] (dottriangle-dot-#2) at (dottriangle-x-#2.base west) {};% + %% The anchors and size of the isosceles triangle are not well positionned. + % \node[draw, shape=isosceles triangle, shape border rotate=90, anchor=north,#3,isosceles triangle stretches,inner sep=0pt,minimum width=#4\tmul,minimum height=#5\tmul] (t) at (dot.center) {}; + \draw[resetinnersep,#3] (dottriangle-dot-#2.center) -- ++(.5*#4\tmul,-#5\tmul) coordinate (dottriangle-te-#2) -- ++(-#4\tmul,0) coordinate (dottriangle-tw-#2) -- cycle; +%%%%%%%%%%%% + \coordinate (dottriangle-tc-#2) at (barycentric cs:dottriangle-dot-#2=1,dottriangle-te-#2=1,dottriangle-tw-#2=1); + \node[inner sep=0pt,fit=(predottriangle-dot-#2) (predottriangle-te-#2) (predottriangle-tw-#2)] (dottriangle-boundingbox-#2) {}; +} + +%Some colors +\definecolor{coolgrey}{rgb}{0.55, 0.57, 0.67} +\definecolor{fgred}{rgb}{0.66, 0.13, 0.24} +\definecolor{yonder}{rgb}{0.64, 0.68, 0.82} +\definecolor{tangerine}{rgb}{1.0, 0.6, 0.4} +\definecolor{salmon}{rgb}{1.0, 0.63, 0.48} +\definecolor{caribbeangreen}{rgb}{0.0, 0.8, 0.6} +\definecolor{cream}{rgb}{1.0, 0.99, 0.82} +\definecolor{deepchampagne}{rgb}{0.98, 0.84, 0.65} +\definecolor{burntsienna}{rgb}{0.91, 0.45, 0.32} + + +% This is the definition of join_k +\def\bigijoin{% + \alignedmathop{% + \bigvee% + }{% + \mathchoice% + {\bigvee\mkern-8mu\smash{\raisebox{-0.9ex}{$\resetstyle\mathlarger{\mathlarger{{}_{\intra}}}$}}}% + {\bigvee\mkern-7mu\smash{\raisebox{-0.6ex}{$\resetstyle\mathlarger{\mathlarger{{}_{\intra}}}$}}}% + {\bigvee\mkern-2.25mu\smash{\raisebox{-0.3ex}{$\resetstyle\mathlarger{\mathlarger{{}_{\intra}}}$}}}% + {\bigvee\mkern-2.5mu\smash{\raisebox{-0.35ex}{$\resetstyle\mathlarger{{}_{\intra}}$}}}% + }% +} +\def\largeijoin{% + \alignedmathop{% + \bigvee% + }{% + \mathchoice% + {\bigvee\mkern-8mu\smash{\raisebox{-0.6ex}{$\resetstyle\mathlarger{{}_{\intra}}$}}}% + {\bigvee\mkern-5mu\smash{\raisebox{-0.6ex}{$\resetstyle\mathlarger{\mathlarger{{}_{\intra}}}$}}}% + {\bigvee\mkern-2.25mu\smash{\raisebox{-0.3ex}{$\resetstyle\mathlarger{\mathlarger{{}_{\intra}}}$}}}% + {\bigvee\mkern-2.5mu\smash{\raisebox{-0.35ex}{$\resetstyle\mathlarger{{}_{\intra}}$}}}% + }% +} +\def\ijoin{% + \alignedmathop{% + \vee% + }{% + \mathchoice% + {\vee\mkern-4mu\smash{\raisebox{-0.3ex}{$\resetstyle\mathlarger{{}_{\intra}}$}}}% + {\vee\mkern-3mu\smash{\raisebox{-0.1ex}{$\resetstyle\mathlarger{{}_{\intra}}$}}}% + {\vee\mkern-2.25mu\smash{\raisebox{-0.3ex}{$\resetstyle\mathlarger{{}_{\intra}}$}}}% + {\vee\mkern-2.5mu\smash{\raisebox{-0.35ex}{$\resetstyle\mathlarger{{}_{\intra}}$}}}% + }% +} diff --git a/main.tex b/main.tex new file mode 100644 index 0000000..9132705 --- /dev/null +++ b/main.tex @@ -0,0 +1,2260 @@ +\documentclass[11pt]{article} + +\usepackage{a4wide} + + +\usepackage[T1]{fontenc} +\usepackage[scaled=.7]{beramono} +\usepackage{lmodern} +\usepackage[utf8]{inputenc} +%\usepackage[english]{babel} +\usepackage{amsmath} +\usepackage{amssymb} +\usepackage{amsfonts} +\usepackage{amsthm} +\usepackage{dsfont} +\usepackage{mathrsfs} +\usepackage{ifdraft} +\usepackage{array,multicol} +\usepackage{booktabs} +\usepackage{longtable} +\usepackage{cancel} +\usepackage{float} +\usepackage{stmaryrd} +\usepackage{colortbl} +\usepackage{caption} +\usepackage{mathpartir} +\usepackage{mathtools} +\usepackage[final]{listings} +\usepackage{url} +%\usepackage{bibunits}% Incompatible with biblatex, see biblatex's documentation for workarounds. +\usepackage{marvosym} % Note that this exports \Cross, incompatible with package bbding. +% % Circumvented by code around the \usepackage{bdding} below. +\usepackage{forest} +\usepackage{tikz,datetime} +\usetikzlibrary{decorations.pathreplacing,trees,calc,fit,positioning,chains,arrows,arrows.meta,automata,shapes,graphs,shapes.geometric,shapes.symbols, +decorations.markings,patterns,matrix,decorations.pathmorphing,mindmap,math} +%,triangle-fit,decorations.growingwave,oni-squiggly} +\usepackage{pgf} +\usepackage{pgfplots} +\usepackage{graphicx} +\usepackage{subfigure} +\usepackage{alltt} +\usepackage{mathrsfs} +\usepackage{wrapfig} +\usepackage{xcolor} +\usepackage{dsfont} +\usepackage{amsbsy} +\usepackage{savesym} +% Circumvent incompatibility between marvosym and bdding, which both define \Cross. +% See https://groups.google.com/forum/#!topic/comp.text.tex/LSETDAIaJug +\savesymbol{Cross}% Save original \Cross as \origCross. +\usepackage{bbding} +\restoresymbol{bb}{Cross}% Restore original \Cross from marvosym + rename bbding's \Cross to \bbCross. +\usepackage{relsize} +\usepackage{wasysym} +%\usepackage{growingwave} +\pgfdeclarelayer{background} +\pgfdeclarelayer{foreground} +\pgfsetlayers{background,main,foreground} +\usepackage{epigraph} +%\usepackage{oni-trees} +%\usepackage{oni-tree-defaults} +%\usepackage[backend=bibtex,style=authoryear,natbib=true,maxbibnames=99]{biblatex} +%% User the bibtex backend with the authoryear citation style (which +%% resembles APA) +\usepackage{tikz,datetime} +\usetikzlibrary{decorations.pathreplacing,trees,calc,fit,positioning,chains,arrows,arrows.meta,automata,shapes,graphs,shapes.geometric,shapes.symbols, +decorations.markings,patterns,matrix,decorations.pathmorphing,mindmap,math} +%,triangle-fit,decorations.growingwave,oni-squiggly} +\usepackage{pgf} +\usepackage{pgfplots} +\usepackage{graphicx} +\usepackage{subfigure} + +%%%%%%%%%% +%% from main.tex + + + + +\newtheorem{definition}{Definition} + +\newcommand{\snumber}[1]{\textrm{{\scriptsize(#1)}}} + +%%%%% +%%%%% From Chapter on SSMART +\newcommand{\disp}[1]{\lstinline&} + +%% True label +\def\lbtrue{\textsf{true}} +%% False Label +\def\lbfalse{\textsf{false}} + + +%Set of structure field identifiers +\def\fset{\ensuremath{\mathcal{F}}} +%Set of variant constructors identifiers +\def\cset{\ensuremath{\mathcal{C}}} +%Set of variable identifiers +\def\vset{\ensuremath{\mathcal{V}}} +%Set of writeable variable identifiers +\def\wrvset{\ensuremath{\mathcal{V}^{+}}} +%Set of read-only variable identifiers +\def\rovset{\ensuremath{\mathcal{V}^{-}}} +%Universe of type identifiers +\def\utyp{\ensuremath{\mathbb{T}}} +%Set of base type identifiers +\def\basetyp{\ensuremath{T_0}} +%Universe of semantic values +\def\uval{\ensuremath{\mathbb{D}}} +%Typing environment +\def\tenv{\ensuremath{\Gamma}} +%Valuation +\def\env{\ensuremath{E}} + +%% Types +\def\primtyp{\tau} + +%Structure Type +\newcommand{\plainstype}[6] +{\ensuremath{\boldsymbol{struct}\{#1_{#2}: #3, \ldots, #4_{#5}: #6 \}}} + +\newcommand{\plainmiddlestype}[9] +{\ensuremath{\boldsymbol{struct}\{#1_{#2}: #3, \ldots, #4_{#5}: #6 , \ldots,#7_{#8}: #9\}}} + +\def\commonstype{\plainstype{f}{1}{\tau}{f}{n}{\tau}} +\def\commonstypeindex{\plainstype{f}{1}{\tau_1}{f}{n}{\tau_n}} +\def\commonmiddlestype{\plainmiddlestype{f}{1}{\tau_1}{f}{i}{\tau_i}{f}{n}{\tau_n}} + +%Variant Type +\newcommand{\plainvtype}[6] +{\ensuremath{\boldsymbol{variant}[#1_{#2}: #3 \ver \ldots \ver #4_{#5}: #6]}} + +\newcommand{\plainmiddlevtype}[9] +{\ensuremath{\boldsymbol{variant}[#1_{#2}: #3 \ver \ldots \ver #4_{#5}: #6 \ver \ldots \ver #7_{#8}: #9]}} + +\def\commonvtype{\plainvtype{C}{1}{\tau}{C}{n}{\tau}} +\def\commonvtypeindex{\plainvtype{C}{1}{\tau_1}{C}{n}{\tau_n}} +\def\commonmiddlevtype{\plainmiddlevtype{C}{1}{\tau_1}{C}{i}{\tau_i}{C}{n}{\tau_n}} + +%Array Type +\newcommand{\plainatype}[2] +{\ensuremath{\boldsymbol{arr}^{#1} \langle #2 \rangle}} + +\def\commonatype{\plainatype{\tau}{\tau}} +\def\commonatypeindex{\plainatype{\tau_i}{\tau}} + +% Values + +%Structure Values +\newcommand{\plainsval}[6] +{\ensuremath{\{#1_{#2} = #3, \ldots, #4_{#5} = #6\}}} + +\newcommand{\plainmiddlesval}[9] +{\ensuremath{\{#1_{#2} = #3, \ldots, #4_{#5} = #6, \ldots, #7_{#8} = #9\}}} + +\def\commonsval{\plainsval{f}{1}{v_1}{f}{n}{v_n}} +\def\commonmiddlesval{\plainmiddlesval{f}{1}{v_1}{f}{i}{v_i}{f}{n}{v_n}} + +%% %Variant Values +%% \newcommand{\plainvval}[4] +%% {\ensuremath{#1_{#2}[#3_{#4}] }} + +%% \newcommand{\plainvvalindex}[1] +%% {\ensuremath{C_{#1}[v_{#1}]}} + +%% \def\commonvval{\plainvval{C}{i}{v}{i}} + +%Array Values +\def\asup{\mathcal{P}} + +%% Built-in Statements +\def\unop{\ensuremath{\boldsymbol{nop}}} +\newcommand{\plainasgn}[2]{\ensuremath{#1 := #2}} +\def\commonasgn{\plainasgn{o}{e}} +\newcommand{\plaineqtest}[2]{\ensuremath{#1 = #2}} +\def\commoneqtest{\plaineqtest{e_1}{e_2}} +\newcommand{\recordnew}{r := \{e_1, \ldots, e_n \}} +\newcommand{\recordall}{\{o_1, \ldots, o_n \} := r} +\newcommand{\recordset}{r' := \{r\; \boldsymbol{with}\; f_i = e \} } +\newcommand{\recordget}{o := r.f_i} +\newcommand{\recordeq}{r' = \langle f_1, \ldots, f_k \rangle r''} +\newcommand{\varcons}{v := C_p[e]} +\newcommand{\varswitch} +{\boldsymbol{switch}(v) \;\boldsymbol{as} \;[o_1 \arrowvert \ldots \arrowvert o_n ]} +\newcommand{\varpossible}{v \in \{ C_1,\ldots ,C_k \}} +\newcommand{\arrayget}{o := a[i]} +\newcommand{\arrayset}{a' := [a \; \boldsymbol{with} \; i = e]} + +\newcommand{\predcall} +{p(e_1, \ldots, e_n) \; [\lambda_1: \bar{o}_1 \; \arrowvert \ldots \arrowvert \; \lambda_m: \bar{o}_m]} +\newcommand{\pcall} +{ +{p(e_1, \ldots, e_n)\newline +[\lambda_1: \bar{o}_1 \; \arrowvert \ldots \arrowvert \; \lambda_m: \bar{o}_m]} +} + +%% Exit Labels + +%% True label +\def\lbtrue{\textsf{true}} +%% False Label +\def\lbfalse{\textsf{false}} + +%labels-outputs maps macros +\newcommand{\unary}[1]{\left[\begin{array}{ccc} + \lbtrue &\mapsto \\ + \end{array} + \right]} + +\newcommand{\lbinary}[2]{ + \left[\begin{array}{c} + \lbtrue \mapsto #1\\ + \lbfalse \mapsto #2 + \end{array}\right] +} + +\newcommand{\multi}[4]{\left[\begin{array}{ccc} + \lambda_{#1} &\mapsto & \bar{o}_{1}\\ + \vdots &\ddots &\vdots \\ + \lambda_{#2} &\mapsto & \bar{o}_{#4} + \end{array} + \right]} + +\newcommand{\multiv}[3]{\left[\begin{array}{ccc} + \lambda_{#1} &\mapsto &o_{1}\\ + \vdots &\ddots &\vdots \\ + \lambda_{#2} &\mapsto &o_{#3} + \end{array} + \right]} + + + + +%%%%% +%%%%% From Chapter on SMIL +\def\asmil{\textsf{$\alpha$Smil}} + +\def\commonvval{\plainvval{C}{i}{v}} + +%Generic option type +\def\optiont{\boldsymbol{\small{variant}} +[\textrm{\disp{Some}} : \boldsymbol{\small{struct}}\{\textrm{\disp{t}} : \textrm{\disp{T}}\} \; +\arrowvert\; +\; \textrm{\disp{None}} : \boldsymbol{\small{struct}}\{\}]} + +%%%%% Chapter 5 +\def\ileq{\dleq_{\intra}} +%\def\ijoin{\vee_{\intra}} +\def\ireduce{\oplus_{\intra}} +\def\uintra{\mathscr{D}} + + +%% misc macros +\newcommand{\ver}{\arrowvert \;} + +%macros tables (chapters 5 and 7) +%!%!%! Does this impact tables in other chapters? +%!%!%! If so, we can put it in a \begingroup \endgroup, so that it affects only the desired tables +\newcommand{\ra}[1]{\renewcommand{\arraystretch}{#1}} +\colorlet{tableheadcolor}{gray!25} % Table header colour = 25% gray +\newcommand{\headcol}{\rowcolor{tableheadcolor}} % +\colorlet{tablerowcolor}{gray!10} % Table row separator colour = 10% gray +\newcommand{\rowcol}{\rowcolor{tablerowcolor}} % +\colorlet{tablerowcolor}{gray!10} % Table row separator colour = 10% gray %!%!%! was not in chapter 5. + +% math operators with subscript-ish +%Macro big meet +\makeatletter +\newlength{\widthofMeet} +\newlength{\widthofR} + +\newsavebox{\boxname} +\newsavebox{\boxnameb} +\newsavebox{\boxnamec} + +\def\negphantomdiff#1#2#3{% + \def\resetstyle{#1} + \savebox{\boxname}{$#1#2$}% + \savebox{\boxnameb}{$#1#3$}% + \hspace{-\wd\boxnameb}\hspace{\wd\boxname}% negative width of just the R (= - whole + wedge) +} +\def\withwidthoffirst#1#2#3{% + \def\resetstyle{#1} + \savebox{\boxname}{$#1#2$}% + \savebox{\boxnameb}{$#1#3$}% + \hspace{\wd\boxnameb}\hspace{-\wd\boxname}%width of just the R (= whole - wedge) + \usebox{\boxnameb}% +} +\def\alignedmathop#1#2{% + \@ifstar{% + \centeredmathop{#1}{#2}% + }{% + \mathchoice% + {\negphantomdiff{\displaystyle}{#1}{#2}}% <--- HERE displaystyle + {\negphantomdiff{\textstyle}{#1}{#2}}% <--- HERE textstyle + {\negphantomdiff{\scriptstyle}{#1}{#2}}% <--- HERE scriptstyle + {\negphantomdiff{\scriptscriptstyle}{#1}{#2}}% <--- HERE scriptscriptstyle + \centeredmathop{#1}{#2}% + }% +} +\def\centeredmathop#1#2{% + \mathop{% + \mathchoice% + {\withwidthoffirst{\displaystyle}{#1}{#2}}% <--- HERE displaystyle + {\withwidthoffirst{\textstyle}{#1}{#2}}% <--- HERE textstyle + {\withwidthoffirst{\scriptstyle}{#1}{#2}}% <--- HERE scriptstyle + {\withwidthoffirst{\scriptscriptstyle}{#1}{#2}}% <--- HERE scriptscriptstyle + }% +} +\makeatother + +% Needed to appear cleanly in the list of symbols +\def\intrachapfive{\Delta} +\def\ijoinchapfive{% + \alignedmathop{% + \vee% + }{% + \mathchoice% + {\vee\mkern-4mu\smash{\raisebox{-0.3ex}{$\resetstyle\mathlarger{{}_{\intrachapfive}}$}}}% + {\vee\mkern-3mu\smash{\raisebox{-0.1ex}{$\resetstyle\mathlarger{{}_{\intrachapfive}}$}}}% + {\vee\mkern-2.25mu\smash{\raisebox{-0.3ex}{$\resetstyle\mathlarger{{}_{\intrachapfive}}$}}}% + {\vee\mkern-2.5mu\smash{\raisebox{-0.35ex}{$\resetstyle\mathlarger{{}_{\intrachapfive}}$}}}% + }% +} + + + + + +\title{Static analysis for proof obligation elimination in functional + specifications} + +\author{Oana Andreescu \and Thomas Jensen \and St\'ephane Lescuyer} + +\date{\today} + +\begin{document} + +\begin{abstract} + +\end{abstract} + + +\section{Introduction} + +\subsection{The frame problem} + +The frame problem~\cite{mccarthy69} was identified and described at +least as early as 1969 by McCarthy and Hayes, in the context of +Artificial Intelligence (AI). The initial description of the +frame problem is the following: + +\begin{quotation} +``In proving that one person could get into conversation with another, we were + obliged to add the hypothesis that if a person has a telephone he still has it + after looking up a number in the telephone book. If we had a number of actions + to be performed in sequence we would have quite a number of conditions to + write down that certain actions do not change the values of certain + fluents. In fact, with $n$ actions and $m$ fluents we might have to write down + $mn$ such conditions.'' +\end{quotation} + +Unsurprisingly, +%given its identification in the context of logicist AI, +the frame problem manifests itself in the realm of formal software +specification and deductive verification as well~\cite{borgida93}. +Deductive verification methods consist in producing formal correctness +proofs, by first generating a set of formal mathematical proof +obligations from the program and its specification, and by +subsequently discharging these. Proof +obligations can sometimes be discharged automatically by using static +analysis and decision procedures, but often they require the use of +an interactive prover. Reducing the number of proof obligations in a +verification hence becomes an essential task. + +A large part of a proof consists in proving that a global invariant is +preserved, despite the state changes that a program makes +as it executes. A number of proof obligations deal with those parts of the +state that actually have been changed. Another set of proof +obligations arise from dealing with the part of the state that does +not change. These may be particularly tedious to handle because it +should be ``evident'' that the invariant holds for this part of the +state. As a consequence, several specification formalisms offer the +possibility of specifying what is changed and what does not +change. These properties are called \emph{frame properties}. + +Frame properties help reducing the number of proof +obligations. However, specifying frame properties might not seem dramatic +on small examples, but in real-world examples this quickly +escalates, leading to the necessity of specifying a plethora of +conditions.Writing such conditions is necessary but also notoriously +repetitive and tedious. As Kogtenkov et al.~\cite{kogtenkov15} +so eloquently puts it: + +\begin{quotation} +``It is hard enough to convince programmers to state what their program does; forcing +them in addition to specify all that it does not do may be a tough sell.'' +\end{quotation} + +The tedious, undeserved, manual effort entailed by the specification and +verification of frame properties is a manifestation of the frame problem. Though +certain conventions and approaches, such as the \emph{implicit frames} approach, +for specifying frame properties can alleviate the manual effort imposed, some +manifestation of the frame problem will be visible to some extent in the context +of any specification language and verification method. + +The article proposes a solution to the frame problem based on +fully-automatic, static program analyses for inferring the +preservation of program invariants. More specifically, we target the +automatic identification of properties that depend only on an input +subset that is disjoint from an operation's \emph{frame}, i.e. the +state subset it modifies. + +\subsection{Methodology} + +To this end, we propose a solution based on static analysis which does not +require any additional frame annotations. By detecting the subset +on which a property depends and by uncovering the part that is not modified by +an operation, as shown in Figure~\ref{ch1:fig:strategy}, we can automatically +discharge proof obligations related to unmodified parts. We employ two different +static analyses for this goal. + +\begin{figure}[!h] +%Second Line +\begin{minipage}[c]{0.1\textwidth} +\[ +\begin{array}[b]{crcl} + +\textrm{{Dependency}} & +Obs +\left( +\mathord{% +\resizebox{\textwidth}{!}{ +\begin{tikzpicture}[ baseline= (current bounding box.center), scale=0.7, auto] + \filldraw[fill=lightgray!60,pattern = north west lines, pattern color=red, rounded corners] (4.5,-8.5) rectangle (8.5,-5.5); + \filldraw[fill=lightgray!60] (4.5, -6.5) rectangle (8.5, -6.8); + \filldraw[fill=lightgray!60,pattern=vertical lines, pattern color=black] (4.5, -6.5) rectangle (8.5, -6.8); +\end{tikzpicture}% +} +} +\right) + & = & +Obs +\left( +\mathord{% +\resizebox{\textwidth}{!}{ +\begin{tikzpicture}[baseline=(current bounding box.center), scale=0.7, auto] + \filldraw[fill=red!75!black, rounded corners] (12,-12) rectangle (16,-9) ;% draw/fill the box + \filldraw[pattern = north east lines, pattern color=white, rounded corners] (12,-12) rectangle (16,-9) ;% draw the stripes + \filldraw[fill=lightgray!40] (12, -10) rectangle (16, -10.3); + \filldraw[pattern=vertical lines, pattern color=black] (12, -10) rectangle (16, -10.3); +\end{tikzpicture}% +} +} +\right) \\[1.5em] + +\textrm{{Correlation}} & +\textrm{\huge{$f$}} +\left ( +\mathord{% +\resizebox{\textwidth}{!}{ +\begin{tikzpicture}[baseline=(current bounding box.center), scale=0.7, auto] + \filldraw[fill=lightgray!60, rounded corners] (1,-10) rectangle (5,-7) + node[scale=1.5,rectangle, minimum size = 2] at (3,-7.5) {\Large$?$} + node[scale=1.5,rectangle, minimum size = 2] at (3, -9) {\Large$?$}; + \filldraw[fill=lightgray!60] (1, -8) rectangle (5, -8.3); + \filldraw[fill=lightgray!60,pattern=vertical lines, pattern color=black] (1, -8) rectangle (5, -8.3); +\end{tikzpicture}% +} +} +\right) +& = & +\mathord{% +\resizebox{\textwidth}{!}{ +\begin{tikzpicture}[baseline=(current bounding box.center), scale=0.7, auto] + \filldraw[fill=darkgray!60, rounded corners] (12,-10) rectangle (16,-7) + node[scale=1.5,rectangle, minimum size = 2] at (14,-7.5) {\Large$?$} + node[scale=1.5,rectangle, minimum size = 2] at (14, -9) {\Large$?$};;% draw the box + \filldraw[fill=lightgray!40] (12, -8) rectangle (16, -8.3); + \filldraw[fill=lightgray!40,pattern=vertical lines, pattern color=black] (12, -8) rectangle (16, -8.3); +\end{tikzpicture}% +} +} \\[1.5em] + +\textrm{{Invariant}} & +Obs +\left ( +\mathord{% +\resizebox{\textwidth}{!}{ +\begin{tikzpicture}[baseline=(current bounding box.center), scale=0.7, auto] + \filldraw[fill=lightgray!40,pattern = north west lines, pattern color=red, rounded corners] (1,-12) rectangle (5,-9); + \filldraw[fill=lightgray!40] (1, -10) rectangle (5, -10.3); + \filldraw[fill=lightgray!40,pattern=vertical lines, pattern color=black] (1, -10) rectangle (5, -10.3); +\end{tikzpicture}% +} +} +\right) + & \Rightarrow & Obs +\left ( +\textrm{\huge{$f$}} +\left( +\mathord{% +\resizebox{\textwidth}{!}{ +\begin{tikzpicture}[baseline=(current bounding box.center), scale=0.7, auto] + \filldraw[fill=lightgray!40,pattern = north west lines, pattern color=red, rounded corners] (12,-12) rectangle (16,-9) ;% draw the box + \filldraw[fill=lightgray!40] (12, -10) rectangle (16, -10.3); + \filldraw[fill=lightgray!40,pattern=vertical lines, pattern color=black] (12, -10) rectangle (16, -10.3); +\end{tikzpicture}% +} +} +\right) +\right) +\end{array} +\] +\end{minipage} +\caption{Frame Problem and Solution Strategy} +\label{ch1:fig:strategy} +\end{figure} + +The first analysis of our two-step strategy is a \emph{dependency + analysis}, which detects the input subset $\delta$ on which the +outcome of an operation or of a logical property $\mathscr{L}$ +relies. This subset is represented by the grey rectangle with vertical +lines in Figure~\ref{ch1:fig:frameproblem}. The second is a +\emph{correlation analysis}, meant to detect the subset $\xi$ modified +by an operation $\mathscr{O}$, illustrated by the orange +rectangles with inclined lines in +Figure~\ref{fig:frameproblem}. By employing these two static +analyses, thus detecting $\delta$ and $\xi$ automatically, and by +subsequently reasoning based on their combined results, we can infer +the preservation of the property $\mathscr{L}$ for the post-state of +$\mathscr{O}$. + +\subsection{Application context: Formal verification of systems software} + +\subsection{Organisation of the article} + +\section{The SMART functional specification language} + +\section{Dependency analysis} + +\input{dependency-macros} + +The dependency analysis delimits the input subset on which the output +depends, in the context of an operation with a compound input. We +define \emph{dependency} as the observed part of a structured domain +and strive to obtain type-sensitive results, distinguishing between +the subelements of arrays and algebraic data types and capturing the +dependency specific to each. The targeted results are meant to mirror +-- in terms of dependency -- the layered structure of compound data +types. Furthermore, the \emph{dependency analysis} must work with +\emph{conservative approximations} and it must guarantee that what is +marked as not needed is definitely not needed, i.e. it is irrelevant +for the obtained output. + +In the classification of Hind~\cite{hind01}, our dependency analysis is a +\emph{flow-sensitive}, \emph{field-sensitive}, \emph{interprocedural} analysis +that handles associative arrays, structures and variant data types. Specific +dependency results are computed for each of the possible execution +scenarios, i.e. for each exit label. Thus, our analysis also shows a form of +\emph{path-sensitivity}~\cite{hind01}. However, we favour the term +\emph{label-sensitivity} to describe this characteristic, as it seems more +appropriate applied to our case and the language we are working with. + +Our dependency analysis targets complex transition systems in general, and +operating systems and microkernels in particular. +%% Generally, our dependency analysis targets complex transition systems, such as +%% microkernels and operating systems, for example. +These are +characterized by states defined by complex compound data structures and by +transitions, i.e. state changes, that map an input state to an output state. +Automatically proving the preservation of invariants concerning only +subelements of the state, i.e. fields, array cells, etc., that have not been +altered by a transition in the system would considerably diminish the number of +proof obligations. The first step towards achieving this goal consists in +automatically detecting dependency summaries and the minimum relevant input +information for producing certain outputs. + +As mentioned, our analysis targets fine-grained dependency summaries for arrays, +structures and variants, expressed at the level of their subelements. For +variants, besides capturing the specific dependency on each constructor +and its arguments, we argue that additional, relevant information can be +computed, regarding the subset of possible constructors at a given program +point. This is not dependency information \emph{per se} but it enriches the +footprint of a predicate with useful information. Together with the dependency +information, this additional information about constructors is meant to answer +the same question, namely, what fragments of the input influence the output, +from a different, albeit related point of view. Therefore, we are +simultaneously performing a \emph{possible-constructors} analysis. This has an +impact on the defined abstract dependency type, making it more complex, as we will see in +the following section. The \emph{possible-constructors} analysis could be +performed separately, as a stand-alone analysis. By performing the two analyses +simultaneously, we lose some of the precision that would be attained if the two +were performed separately, but we reduce overhead and present relevant +information in a unified manner. + +Designing the analysis as a tool to be used in the context of +interactive program verification, on both code and specifications, has +led to specific traits. One of them concerns the treatment of +arrays. In contrast to dependence and liveness analyses used for code +optimizations~\cite{gross90}, which require precision for every +array cell, we compute dependency information referring to all cells +of the array or to all but one cell, for which an exceptional +dependency is computed. In practice, a considerable number of +relevant properties and operations involving arrays fall into this +spectrum. + + + +%% Frequently operations manipulating arrays are concerned only with +%% one element; others, such as sorting algorithms are concerned and potentially +%% modify every element. Properties on arrays most often refer to all cells of an +%% array or to one cell, imposing conditions of the \emph{forall} or \emph{exists} +%% type. Properties on arrays often address somehow a \emph{uniform} quality +%% applying to all elements of the array or to ... + +\subsection{Targeted Dependency Information}\label{sec:intro:example} + +We briefly present two examples of {\asmil} predicates \disp{thread} +and \disp{start_address}, +manipulating structures, variants and arrays and describe the dependency +information that we are targeting. +Both predicates manipulate inputs of type +\disp{process}, and handle values of type \disp{thread} and +\disp{memory_region}. + +\begin{figure}[hbtp]\centering +\begin{tabular}{ll} +\toprule +\begin{lstlisting} +type memory_region = { + // Start address + start : int; + // Region length + length : int +} +\end{lstlisting} +&\begin{lstlisting} +type thread = { + // Identifier + id : int; + // Current state + crt_state : state; + // Stack + stack : memory_region +} +\end{lstlisting} \\ +\bottomrule +\end{tabular} +\caption{Example Data Types -- Thread and Memory Region} +\label{ex:atype} +\end{figure} + +\begin{figure}[hbtp]\centering +\begin{tabular}{ll} +\toprule +\begin{lstlisting} +type option = + | None + | Some (A a) +\end{lstlisting} +&\begin{lstlisting} +type process = { + // Array of associated threads + threads : array>; + // Internal id + pid : int; + // Currently running thread + crt_thread : int; + // Address space + adr_space : address_space +} +\end{lstlisting} +\\ +\bottomrule +\end{tabular} +\caption{Input Type -- Process} +\label{ex:itype} +\end{figure} + +The first predicate, \disp{thread}, having the control flow graph shown in +Figure~\ref{pred:cfg:thread} and whose implementation is shown in +Figure~\ref{ex:thread:code}, receives a process \disp{p} and an index \disp{i} +as inputs. It reads the \disp{i}-th element in the \disp{threads} array of the +input process \disp{p}. If this element is active, then the predicate exits with +the label \disp{true} and outputs the corresponding thread \disp{ti}. Otherwise, +it exits with the label \disp{None} and no output is generated. + +\begin{figure}[!h] +\begin{lstlisting} +predicate thread(process p, int i) + -> [true: thread ti|None|oob] +{{array> th, option tio}} { + th := p.threads : [true -> 1]; + tio := th[i] : [true -> 2, false -> 5]; + switch (tio) as [ |ti] : [None -> 4, Some -> 3]; + [true]; + [None]; + [oob] +} +\end{lstlisting} +\caption{Predicate \disp{thread} -- Implementation} +\label{ex:thread:code} +\end{figure} + +\begin{figure}[!h]\centering +\resizebox{0.7\textwidth}{!}{% +\begin{tabular}{@{}c@{}} +\toprule +{ \centering + \hspace{1.6cm} + \begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node distance=1.2cm, semithick, + statt/.style={fill=lightgray!50,draw=none,text=black,ellipse,inner sep=0pt,minimum width=.7cm,minimum height=.7cm}] +% + \node[statt] (N1) {{th := p.threads}}; + \node[statt] (N2) [below=1cm of N1] { {tio := th[i]}}; + \node[statt] (N3) [below left=of N2] { {$\boldsymbol{switch}$(tio) $\boldsymbol{as}$ + [ $\ver$ti}]}; + \node[statt] (N4) [below right=of N2]{\textsf{oob}}; + \node[statt] (N5) [below left=of N3]{\lbtrue}; + \node[statt] (N6) [below right=of N3]{\textsf{None}}; + \path (N1) edge node[xshift=-0.95cm] {{\lbtrue}} (N2); + \path (N2) edge node[xshift=-0.8cm,yshift = 0.4cm] {\large{\lbtrue}} (N3); + \path (N2) edge node {{\lbfalse}} (N4); + \path (N3) edge node[left, anchor=south east] { {\textsf{Some}}} (N5); + \path (N3) edge node[right, anchor=south west] { {\textsf{None}}} (N6); +\end{tikzpicture} + } +\\ +\bottomrule +\end{tabular} +} +\caption{$G_{\mathit{thread}}$ -- Control Flow Graph of Predicate \disp{thread}} +\label{pred:cfg:thread} +\end{figure} + + +\begin{figure}[hbtp] +\resizebox{0.95\textwidth}{!}{ +\begin{tabular}{lll} +\toprule +\begin{tikzpicture} +\tikzset{ + position label/.style={ + below = 3pt, + text height = 1.5ex, + text depth = 1ex + }, + brace/.style={ + decoration={brace}, + decorate + } +} + +\node at (3,9) {\Huge Exit label \lbtrue:}; + +\draw[dotted] (0,0) grid[xstep=8, ystep = 2] (8,8); +\fill[lightgray, opacity=0.2] (0,0) rectangle (8,8); +\node at (4,1) {\Huge adr\_space}; +\node at (4,3) {\Huge crt\_thread}; +\node at (4,5) {\Huge pid}; +\node at (4,-1) {\Huge process p}; +\draw[help lines] (0,6) grid[xstep=0.5, ystep = 2] (8,8); +\node at (1,7.5) (nr) {} ; + +\fill[caribbeangreen](2.5,6) rectangle (3,8); +\draw[pattern=north west lines, pattern color=black] (2.5,6) rectangle (3,8); +\node at (4,7) {\Huge threads}; +\end{tikzpicture} +% +&\begin{tikzpicture} +\tikzset{ + position label/.style={ + below = 3pt, + text height = 1.5ex, + text depth = 1ex + }, + brace/.style={ + decoration={brace}, + decorate + } +} +% +\node at (3,9) {\Huge Exit label \textsf{None}:}; + +\draw[dotted] (0,0) grid[xstep=8, ystep = 2] (8,8); +\fill[lightgray, opacity=0.2] (0,0) rectangle (8,8); +\node at (4,1) {\Huge adr\_space}; +\node at (4,3) {\Huge crt\_thread}; +\node at (4,5) {\Huge pid}; +\node at (4,-1) {\Huge process p}; +\draw[help lines] (0,6) grid[xstep=0.5, ystep = 2] (8,8); +\node at (1,7.5) (nr) {} ; + +\fill[red, opacity=0.3](2.5,6) rectangle (3,8); +\draw[pattern=north west lines, pattern color=black] (2.5,6) rectangle (3,8); +\node at (4,7) {\Huge threads}; +\end{tikzpicture} +% +&\begin{tikzpicture}[node distance=0.5cm, legend-square/.style={draw=black!50!white, draw opacity=1, minimum width=1cm, minimum height=1cm, inner sep=0pt, anchor=north west}] +\node[anchor=base west] at (29,1.8) {\Large option:}; +\node[fill=caribbeangreen,legend-square] (legend-green) at (29,1) {}; +\node[right=of legend-green] {\Large Some(thread t)}; +\node[fill=red,opacity=0.3,legend-square] (legend-red) at (29,-1) {}; +\node[right=of legend-red] {\Large None}; + +\node[pattern=north west lines, pattern color=black, preaction={fill=lightgray, opacity=0.2},legend-square] (legend-gray-lines) at (29,6) {}; +\node[anchor=base west, right=of legend-gray-lines] {\Large Read/Needed}; + +\node[fill=lightgray, opacity=0.2, minimum width=1cm, minimum height=1cm,legend-square] (legend-gray) at (29,4) {}; +\node[anchor=base west,right=of legend-gray] {\Large Irrelevant/Not Needed}; + +\path[draw=none,fill=none](29,-3.5) rectangle (31,0); +\end{tikzpicture}\\ +\bottomrule +% +\end{tabular} +} +\caption{Targeted Dependency Results for Predicate \disp{thread}} +\label{ex:res:thread} +\end{figure} + +Our dependency analysis should be able to distinguish between the different +exit labels of the predicate. For the label \disp{true} for instance, it +should detect that only the field \disp{threads} is read by the predicate, +while all others are irrelevant to the result. Furthermore, it should detect +that for the \disp{threads} array of the input \disp{p} only the \disp{i}-th +element is inspected. Additionally, since we are considering the label +\disp{true}, the \disp{i}-th element is necessarily an \emph{active} thread, +indicated by the constructor \disp{Some}. The other constructor, \disp{None}, is +\emph{impossible} for this execution scenario. On the contrary, for the exit +label \disp{None}, the constructor \disp{Some} is impossible. For the exit label +\disp{oob}, nothing but the index \disp{i} and the ``support'' or ``length'' of the +associated \disp{threads} array is read. The targeted dependency results for the +predicate \disp{thread} are depicted in Figure~\ref{ex:res:thread}. +%% The second predicate, \disp{start_address}, whose control flow graph is shown in +%% Figure~\ref{ch4:pred:cfg:start}, receives a process \disp{p} and an index \disp{j} +%% as inputs and finds the start address of the stack corresponding to an active thread. + +\begin{figure}[hbtp]\centering +\resizebox{0.7\textwidth}{!}{% +\begin{tabular}{@{}c@{}} +\toprule +{ \centering + \hspace{1.6cm} + \begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node distance=1.2cm, semithick, + statt/.style={fill=lightgray!50,draw=none,text=black,ellipse,inner sep=0pt,minimum width=.7cm,minimum height=.7cm}] +% + \node[statt] (N1) {\large {thread(p, j)[true: tj | None | oob]}}; + \node[statt] (N2) [below left=of N1] {\large {sj := tj.stack}}; + \node[statt] (N3) [below right=of N1] {\textsf{None}}; + \node[statt] (N4) [below=1cm of N2]{\large {adr := sj.start}}; + \node[statt] (N5) [below=1cm of N4]{\lbtrue}; + \node[statt] (N6) [below=of N1]{\textsf{error}}; + \path (N1) edge node[xshift=-0.05cm, yshift=0.15cm] {\large {\lbtrue}} (N2); + \path (N1) edge node {\large {\textsf{None}}} (N3); + \path (N2) edge node {\large {\lbtrue}} (N4); + \path (N4) edge node{\large {\lbtrue}} (N5); + \path (N1) edge node {\large {\textsf{oob}}} (N6); +\end{tikzpicture} + } +\\ +\bottomrule +\end{tabular} +} +\caption{$G_{\mathit{start\_address}}$ -- Control Flow Graph of Predicate \disp{start_address}} +\label{ch4:pred:cfg:start} +\end{figure} + +The second predicate, \disp{start_address}, whose control flow graph is shown in +Figure~\ref{ch4:pred:cfg:start}, receives a process \disp{p} and an index \disp{j} +as inputs and finds the start address of the stack corresponding to an active thread. +It makes a call to the predicate \disp{thread}, thus reading the +\disp{j}-th element of the \disp{threads} array of its input process. If this is +an active element, it further accesses the field \disp{stack}, from which it +only reads the start address \disp{start}. Otherwise, if the element is inactive, +the predicate forwards the exit label \disp{None} of the called predicate \disp{thread} +and generates no output. When given an invalid index \disp{i}, the predicate exits +with label \disp{oob}. +The predicate's implementation is shown in Figure~\ref{ex:start:code}. + +\begin{figure}[hbtp] +\begin{lstlisting} +predicate start_address(process p, int j) + -> [true: int adr|None] +{{thread tj, memory_region sj}} { + thread(p, j)[true: tj | None | oob] : [true -> 1, + None -> 4, oob -> 5]; + sj := tj.stack : [true -> 2]; + adr := sj.start : [true -> 3]; + [true]; + [None]; + [error] +} +\end{lstlisting} +\caption{Predicate \disp{start_address} -- Implementation} +\label{ex:start:code} +\end{figure} + +The dependency information for this predicate should capture the fact that on the +\disp{true} execution scenario, only the field \disp{start} of the input's +\disp{j}-th associated thread is read. Furthermore, the only possible constructor +on this execution path is the \disp{Some} constructor. On the contrary, for the +\disp{None} execution scenario the only possible constructor is the \disp{None} +constructor. The targeted dependency results for the \disp{start_address} +predicate are depicted in Figure~\ref{ex:res:start}. We remark that for the \disp{oob} +execution scenario, only the ``support'' or ``length'' of the \disp{threads} array is +read. + +\begin{figure}[hbtp] +\resizebox{0.95\textwidth}{!}{ +\begin{tabular}{lll} +\toprule +\begin{tikzpicture} +\tikzset{ + position label/.style={ + below = 3pt, + text height = 1.5ex, + text depth = 1ex + }, + brace/.style={ + decoration={brace}, + decorate + } +} + +\node at (3,9) {\Huge Exit label \lbtrue:}; + +\draw[dotted] (0,0) grid[xstep=8, ystep = 2] (8,8); +\fill[lightgray, opacity=0.2] (0,0) rectangle (8,8); +\node at (4,1) {\Huge adr\_space}; +\node at (4,3) {\Huge crt\_thread}; +\node at (4,5) {\Huge pid}; +\node at (4,-1) {\Huge process p}; +\draw[help lines] (0,6) grid[xstep=0.5, ystep = 2] (8,8); +\node at (1,7.5) (nr) {} ; + +\fill[caribbeangreen](2.5,6) rectangle (3,8); +\node (tj) at (2.8,7.8) {}; +\node at (4,7) {\Huge threads}; + +\draw[dotted] (9,11) rectangle (12,12); +\fill[lightgray, opacity=0.2] (9,11) rectangle (12,12); +\node at (10.5,11.5) {\huge id}; + +\draw[dotted] (9,10) rectangle (12,11); +\fill[lightgray, opacity=0.2] (9,10) rectangle (12,11); +\node at (10.5,10.5) {\Large crt\_state}; + +\draw[dotted] (9,9) rectangle (12,10); +\fill[lightgray, opacity=0.2] (9,9) rectangle (12,10); +\node (s) at (10.5,9.5) {\Large stack}; +\node (s2) at (9, 9.5) {}; +\node at (10.5,8.5) {\huge thread tj}; + + +\draw[dotted] (14,9) rectangle (16,10); +\fill[lightgray, opacity=0.2] (14,9) rectangle (16,10); +\draw[pattern=north west lines, pattern color=black, opacity=0.5] (14,9) rectangle (16,10); +\node (a) at (15,9.5) {\Huge start}; +\node at (16,8.5) {\huge stack stj}; + +\draw[dotted] (16,9) rectangle (18,10); +\fill[lightgray, opacity=0.2] (16,9) rectangle (18,10); +\node at (17,9.5) {\huge length}; + +\draw[->, very thick] (s) edge (a); +\draw[->, very thick, out=90] (tj) edge (s2); + +\end{tikzpicture} +% +&\begin{tikzpicture} +\tikzset{ + position label/.style={ + below = 3pt, + text height = 1.5ex, + text depth = 1ex + }, + brace/.style={ + decoration={brace}, + decorate + } +} +% +\node at (3,9) {\Huge Exit label \textsf{None}:}; + +\draw[dotted] (0,0) grid[xstep=8, ystep = 2] (8,8); +\fill[lightgray, opacity=0.2] (0,0) rectangle (8,8); +\node at (4,1) {\Huge adr\_space}; +\node at (4,3) {\Huge crt\_thread}; +\node at (4,5) {\Huge pid}; +\node at (4,7) {\Huge threads}; +\node at (4,-1) {\Huge process p}; +\draw[help lines] (0,6) grid[xstep=0.5, ystep = 2] (8,8); +\node at (1,7.5) (nr) {} ; + +\fill[red, opacity=0.3](2.5,6) rectangle (3,8); +\draw[pattern=north west lines, pattern color=black] (2.5,6) rectangle (3,8); +%\draw[dotted, red] (2.5,6) rectangle (3,8); +\end{tikzpicture} +% +&\begin{tikzpicture}[node distance=0.5cm, legend-square/.style={draw=black!50!white, draw opacity=1, minimum width=1cm, minimum height=1cm, inner sep=0pt, anchor=north west}] +\node[anchor=base west] at (29,1.8) {\Large option:}; +\node[fill=caribbeangreen,legend-square] (legend-green) at (29,1) {}; +\node[right=of legend-green] {\Large Some(thread t)}; +\node[fill=red,opacity=0.3,legend-square] (legend-red) at (29,-1) {}; +\node[right=of legend-red] {\Large None}; + +\node[pattern=north west lines, pattern color=black, preaction={fill=lightgray, opacity=0.2},legend-square] (legend-gray-lines) at (29,6) {}; +\node[anchor=base west, right=of legend-gray-lines] {\Large Read/Needed}; + +\node[fill=lightgray, opacity=0.2, minimum width=1cm, minimum height=1cm,legend-square] (legend-gray) at (29,4) {}; +\node[anchor=base west,right=of legend-gray] {\Large Irrelevant/Not Needed}; + +\path[draw=none,fill=none](29,-3.5) rectangle (31,0); +\end{tikzpicture}\\ +\bottomrule +% +\end{tabular} +} +\caption{Targeted Dependency Results for Predicate \disp{start_address}} +\label{ex:res:start} +\end{figure} + +\subsection{The dependency abstract domain} +\label{sec:depdom} + +The first step towards inferring expressive, type-sensitive results that capture +the dependency specific to each subelement of an algebraic data type or an +associative array, is the definition of an \emph{abstract dependency domain} +%\defsymbol{$\udep$}{Abstract dependency domain}% +$\udep$, that mimics the structure of such data types. The dependency domain $\delta \in +\udep$, shown below, is defined inductively from the three atomic cases --- +$\everything$, $\nothing$ and $\impossible$ --- and mirrors the structure of the +concrete types. +% +\begin{definition}\label{ch5depdom}{Dependency Domain $\delta \in +\udep$.} +\[ +\begin{array}{lllr} +\dom := &\ver \everything &\textrm{\emph{Everything} -- atomic case} &\snumber{i}\\ + &\ver \nothing &\textrm{\emph{Nothing} -- atomic case} &\snumber{ii}\\ + &\ver \impossible &\textrm{\emph{Impossible} -- atomic case} &\snumber{iii}\\ + &\ver \structdom{\dstruct{1}}{\dstruct{n}} &f_1, \ldots, f_n \textrm{ fields} &\snumber{iv}\\ + &\ver \vardom{\dvar{1}}{\dvar{m}} & C_1, \ldots, C_m \textrm{ constructors} &\snumber{v}\\ + &\ver \adom{\dom} & &\snumber{vi} \\ + &\ver \addef & i \; \textrm{array index} & \snumber{vii}\\ +\end{array} +\] +\end{definition} +% +\noindent As reflected by the above definition, the dependency for atomic types +is expressed in terms of the domain's atomic cases: \everything{} (least +precise), denoting that \emph{everything} is needed and \nothing, denoting that +\emph{nothing} is needed. The third atomic case \impossible, denoting +\emph{impossible}, is introduced for the \emph{possible constructors} analysis +performed simultaneously, and is further explained below. + +The dependency of a structure {\snumber{iv}} describes the dependency on each of +its fields. %% For example, the dependency assigned to a structure having three +%% fields, $f$, $g$ and $h$, in the context of a predicate operating on it and +%% reading only the $h$ field, while ignoring the other two fields, could be of the +%% following form: $\{f \mapsto \oslash, g \mapsto \oslash, h \mapsto \top \}$. +For instance, revisiting our \disp{thread} example from +Section~\ref{sec:intro:example}, we could express an over-approximation of the +dependency information depicted for the process \disp{p} in +Figure~\ref{ex:res:thread} using the following dependency: +% +\[ +\{\mathit{threads} \mapsto \top; \; \mathit{pid} \mapsto \oslash; \; +\mathit{crt\_thread} \mapsto \oslash; \; \mathit{adr\_space} \mapsto \oslash \}.\] +% +This captures the fact that all fields except the \disp{threads} field are +irrelevant, i.e. they are not read and \emph{nothing} in their contents is +needed. The dependency for the \disp{threads} field is an over-approximation +and expresses the fact that it is entirely necessary, i.e. \emph{everything} in +its value is needed for the result. + +For arrays we distinguish between two cases, namely arrays with a general +dependency applying to all of the cells {given by \snumber{vi}} and arrays with a +general dependency applying to \emph{all but one} exceptional cell, for which a specific +dependency is known {given by \snumber{vii}}. %% For example, the dependency assigned to an +%% array having elements of the structured type with three fields used above, +%% considered in the context of a predicate reading only the field $h$ of the $i$-th +%% array element and ignoring everything else, could be of the following form: +%% $\aexcdom{\oslash}{i}{\{f \mapsto \oslash, g \mapsto \oslash, h \mapsto \top \}}$. +For instance, for the \disp{threads} field of the previous example, the +following dependency: +% +\[ +\aexcdom{\oslash}{i}{\top} +\] +% +would be a less coarse approximation, capturing the fact that only the \disp{i}-th +element of the associated \disp{threads} array is needed, while all others are +irrelevant. + +For variants {\snumber{v}}, the dependency is expressed in terms of the +dependencies of their constructors, expressed in turn in terms of their +arguments' dependencies. Thus, a constructor having a dependency mapped to +\nothing{} is one for which nothing but the \emph{tag} has been read, i.e. its +arguments, if any, are irrelevant for the execution. %% For instance, the dependency assigned to a +%% variant having two constructors $A$ and $B$, in the context of a predicate that +%% only reads the tag for the $A$ constructor and depends completely on the $B$ +%% constructor, could be of the following form: +%% $[A \mapsto \oslash; B \mapsto \top]$. +For instance, for the \disp{i}-th element of the \disp{threads} array of our +previous example, the following dependency: +% +\[ +[\mathit{Some} \mapsto \top; \mathit{None} \mapsto \oslash] +\] +% +would be a more precise approximation, when considering the exit label +\disp{true}. It is still an over-approximation as it expresses that both +constructors are possible. The argument of the \disp{Some} constructor is +entirely read, while for \disp{None} only the tag is read. +%% This expresses the fact that the only possible constructor is +%% \disp{Some} and that its argument is entirely read. + +For variants, we want to take a step further and to also include the information +that certain constructors cannot occur for certain execution paths. \emph{Impossible}, the third +atomic case --- \impossible{} --- is introduced for this purpose. As mentioned +previously in Section~\ref{sec:intro}, in order to obtain this additional +information, we perform a ``possible-constructors'' analysis simultaneously, +which computes for each execution scenario, the subset of possible constructors +for a given value, at a given program point. All constructors that cannot occur +on a given execution path are marked as being \impossible. In contrast, +constructors for which \emph{only} the tag is read are marked as $\oslash$. The +difference between $\impossible$ and $\nothing$ can be illustrated by +considering a polymorphic option type \emph{option}, having two constructors, +$None$ and $\mathit{Some(A \, val)}$, respectively, and a Boolean predicate that +pattern matches on an input of this type and returns \emph{false} in the case of +$None$ and \emph{true} in the case of $Some$, unconditioned by the value $val$ of +its argument. For the \emph{true} execution scenario, the dependency on the +$Some$ constructor would be $\oslash$. The tag is read and it is decisive for the +outcome, but the value of its argument $val$ is completely irrelevant. The +dependency on the $None$ constructor however would be $\impossible$: the +predicate can exit with label \emph{true} if and only if the input matches +against the $Some$ constructor. By distinguishing between these two cases we +can not only distinguish the input's subelements that have a direct impact on an +operation's output, but additionally, we can also obtain a more detailed +footprint that highlights the influence exerted by the input's ``shape'' on the +operation's outcome. + +For instance, for the \disp{i}-th element of the \disp{threads} array of our +previous example, a dependency mapping the constructor \disp{None} to $\bot$ +would be a more precise approximation, when considering the label \disp{true}. +Taking into account all the discussed values, we can express the dependency +depicted in Figure~\ref{ex:res:thread} for the label \disp{true} as follows: + +\[ +\left \{ +\begin{array}{lll} +\mathit{threads} &\mapsto & \aexcdom{\oslash}{i}{[\mathit{Some} \mapsto \top; \mathit{None} \mapsto \bot]}\\ +\mathit{pid} &\mapsto &\oslash \\ +\mathit{crt\_thread} &\mapsto &\oslash \\ +\mathit{adr\_space} &\mapsto &\oslash\\ +\end{array} +\right\}. +\] + +We remark that $\top$, $\oslash$ and $\bot$ can apply to any type. For +instance, $\top$ can be seen as a placeholder for data that is needed in its +entirety. Structure, array or variant dependencies whose subelements are all +entirely needed and thus, uniformly mapped to $\top$, are transformed to $\top$. +The $\bot$ dependency is a placeholder for data that cannot occur on a certain +execution scenario. A whole variant value is impossible if all its constructors +are mapped to $\bot$. A whole structure or array is impossible if any of its +subelements is impossible. + +The {\impossible} atomic value is the lower bound of our domain and hence, the +most precise value. The final abstract dependency is a closure of all these combined +recursively. To give an intuition of the shape of our dependency lattice, we +illustrate below in Figure~\ref{hasse} the Hasse diagram of the order relation +between pairs of atomic dependency values. Intuitively, if the two analyses would +be performed separately, the upper ``diamond'' shape would correspond to the +dependency analysis, and the lower one to the possible-constructors analysis. The +$\oslash$ element would be the lower bound for the dependency domain and the upper +bound for the possible-constructors domain. By performing them simultaneously, +$\bot$ becomes the domain's lower bound. + +\begin{center} +\begin{tikzpicture} + \node (top) at (0,0) {$(\top,\top)$}; + \node [below left of=top] (left) {$(\top, \oslash)$}; + \node [below right of=top] (right) {$(\oslash, \top)$}; + \node [below right of=left,yshift=-0.25cm] (middle) {$(\oslash, \oslash)$}; + + \node [below left of=middle, yshift=-0.25cm] (lowerleft) {$(\bot, \oslash)$}; + \node [below right of=middle,yshift=-0.25cm] (lowerright) {$(\oslash, \bot)$}; + + \node [below right of=lowerleft] (bot) {$(\bot, \bot)$}; + + \node [above right of=lowerleft, xshift=-1.5cm, yshift=-4.25] (inbetleft) {$(\top, \bot)$}; + \node [above left of=lowerright, xshift=1.5cm, yshift=-4.25] (inbetright) {$(\bot, \top)$}; + + \draw [thick, shorten <=-3pt, shorten >=-5pt, out=-120, in=90] (top) to (left); + \draw [thick, shorten <=-3pt, shorten >=-5pt, out=-60, in=90] (top) to (right); + + \draw [thick, shorten <=-5pt, shorten >=-3pt, out=120, in=-90] (middle) to (left); + \draw [thick, shorten <=-5pt, shorten >=-3pt, out=60, in=-90] (middle) to (right); + + \draw [thick, shorten <=-3pt, shorten >=-5pt, out=-120, in=90] (middle) to (lowerleft); + \draw [thick, shorten <=-3pt, shorten >=-5pt, out=-60, in=90] (middle) to (lowerright); + + \draw [thick, shorten <=-5pt, shorten >=-3pt, out=120, in=-90] (bot) to (lowerleft); + \draw [thick, shorten <=-5pt, shorten >=-3pt, out=60, in=-90] (bot) to (lowerright); + + \draw [gray, thick, shorten <=-5pt, shorten >=-3pt, out=160, in=-90] (bot) to (inbetleft); + \draw [gray, thick, shorten <=-5pt, shorten >=-3pt, out=20, in=-90] (bot) to (inbetright); + + \draw [gray, thick, shorten <=-5pt, shorten >=-3pt, out=100, in=-150] (inbetleft) to (left); + \draw [gray, thick, shorten <=-5pt, shorten >=-3pt, out=80, in=-30] (inbetright) to (right); +\end{tikzpicture} +\captionof{figure}{Order Relation on Pairs of Atomic Dependencies} +\label{hasse} +\end{center} + +\subsection{Dependency flow equations} +The intraprocedural dependency analysis keeps dependency information at each point +of the control flow graph, for each input, output and local +variables. + +\begin{definition}{Intraprocedural Dependency Domain $\intra \in \uintra$.}\label{ch5:intradom:definition} +The \emph{intraprocedural} dependency domain $\uintra$ is defined as +% +\[\intra \ni \uintra = \mathcal{V} \rightarrow \udep\] +% +An element of this domain is a mapping from variables to dependencies. +\end{definition} + + +Our dependency analysis is a \emph{backward} data-flow analysis. For each exit +label, it traverses the control flow graph starting with its corresponding exit +node and it marks all other exit points as \emph{Unreachable}, since exit labels +are mutually exclusive. The intraprocedural domain for the currently analysed +label is initialized with its associated output variables mapped to \everything. +Thereby, the analysis starts by making a conservative approximation and by +considering that all the input has been observed and the output depends on it +entirely. Typically, dependence analyses are \emph{forward} analyses. However, +given our goal to express \emph{label-specific} dependencies as input-output +relations and taking into consideration the characteristics of the {\asmil} +language, choosing to design our analysis as a backward data-flow analysis +seemed a pertinent choice. In {\asmil}, outputs are associated to a particular +exit label and they are generated if and only if the predicate exits with that +particular label. By traversing the control flow graph backwards, we can use +this information and consider, starting with the initialisation phase, only the outputs +that are relevant for the analysed exit label. + +After the initialisation, the analysis then traverses the control flow graph and +gradually refines the dependencies until a fixed point is reached. +Table~\ref{representation} summarizes the representation and general equation of +the statements. For each statement, the presented data-flow equation operates on +the intraprocedural domains of the statement's \emph{successor} nodes. The +intraprocedural domain at the \emph{entry point} of the node is obtained by +\emph{joining} the contributions of each \emph{outgoing} edge as shown in +Figure~\ref{intra:contrib:entry}. + + +\definecolor{indianred}{rgb}{0.90, 0.80, 0.71} %melon +\tikzstyle{vertex} = [ellipse, fill=lightgray!50, minimum size =30pt, inner sep = 0pt] +\tikzstyle{edge} = [draw, semithick, -> ] +\begin{figure}[hbt]\centering +\begin{tabular}{@{}c@{}} +\toprule +\begin{tikzpicture} +[scale=0.4, auto] +\node[vertex] (n1) at (10.5,14) {\phantom{switch }\Large{\textsf{statement}}\phantom{switch}}; +\draw[edge] (10.5,16.3) -- (10.5,15.2); +\node [above](l1) at (6.5, 16.15) {$\Delta_{in} = \;$}; +%% \node [above](l9) at (14.95, 16.1) {$ \;[(\Delta_{\lambda_1}\!\setminus \textrm{\textsf{gen}})\oplus \transfer{.}{s}{\lambda_1}]\vee \ldots \vee [(\Delta_{\lambda_n}\!\setminus \textrm{\textsf{gen}})\oplus \transfer{.}{s} +%% {\lambda_n}] \;$}; +\node [above](l9) at (14.95, 16.1) {$ \; \transfer{\Delta_{\lambda_1}}{s}{\lambda_1} \ijoin \ldots \ijoin +\transfer{\Delta_{\lambda_n}}{s}{\lambda_n}\;$}; +\node (contrib) at (23.2, 15.2) {\small $\transfer{\Delta_i}{s}{\lambda_i} : (\Delta_i \setminus +\textrm{\textsf{gen}}_{s, \lambda_i}) \ireduce \delta_{s,\lambda_i}$} ; +\node (line2) at (24.2, 14) {\small $\delta_{s,\lambda_i}$ contribution of $s$ on $\lambda_i$}; + +\draw[edge] (8.5, 12.75) -- (7.5, 9.5); +\node [below](l2) at (6.5, 11.9) {\small $\delta_{s,\lambda_1}$}; +\node [above](l3) at (6.6, 9.4) {$\Delta_{\lambda_{1}}$}; +\draw[edge] (12.5, 12.75) -- (13.5, 9.5); +\node [below](l6) at (10.5, 12.5) {$\ldots$}; +\node [below](l4) at (14.5, 11.9) {\small $\delta_{s,\lambda_n}$}; +\node [above](l5) at (14.5, 9.4) {$\Delta_{\lambda_{n}}$}; +\node [below](l7) at (4.1, 12.9) {\footnotesize ($\Delta_{\lambda_1}\!\setminus \textrm{\textsf{gen}}_{s,\lambda_1}$) $\ireduce \delta_{s,\lambda_1} $}; +\node [below](l8) at (17, 12.9) {\footnotesize ($\Delta_{\lambda_n}\!\setminus \textrm{\textsf{gen}}_{s,\lambda_n}$) $\ireduce \delta_{s,\lambda_n}$}; +\end{tikzpicture} \\ +\bottomrule +\end{tabular} +\caption{Computation of the Intraprocedural Domain at a Node's Entry Point} +\label{intra:contrib:entry} +\end{figure} + +Table~\ref{generic} presents the transfer functions for statements which are not +type-specific. For equality tests \snumber{1} both of the inputs $e_1$, $e_2$ are +completely read, whether the test returns \lbtrue{} or \lbfalse. The transfer +functions therefore, reduce the domain of the corresponding successor node with +a domain consisting of $e_1$ and $e_2$ both mapped to $\everything$. +% +In the case of assignment \snumber{2}, the dependency of the written output +variable $o$ is forgotten from the successor's intraprocedural domain, thus +being mapped to \nothing{} and forwarded to the input variable $e$. +% +The transfer function for the $\unop$ operation \snumber{3} is simply the +identity. + +\begin{longtable}{@{}c@{}} +\caption{Generic Statements -- Data-Flow Equations} +\ra{1.4} +\label{generic} +\endlastfoot +\resizebox{0.99\linewidth}{!}{ +$ +\begin{array}{@{}lll@{}} +\toprule +\textsf{Statement} & & \transfer {\intra}{s}{\lambda_i} +\\ +\midrule +% +%Equality test +\textrm{\textsf{Equality test}} & (1) +% +&\begin{tabular}{@{}lcccl@{}} + $ \transfer{\intra}{e_1 = e_2}{\textrm{\lbtrue}} = \displaystyle \intra \; \ireduce\; dep $ +&&&& where +% +\\ +$\transfer{\intra}{e_1 = e_2}{\textrm{\lbfalse}} = \displaystyle \intra \; \ireduce\; dep + $ +&&&& +$ dep = \left \{ +\begin{array} {lcl} + e_1 & \mapsto \top \\ + e_2 & \mapsto \top + \end{array} + + \right \} $ +\\ +\end{tabular} +% +\\ \\ +% +%Assignment + \textrm{\textsf{Assignment}} & (2) +% +& \transfer{\intra}{o:=e}{\lbtrue} = \displaystyle \killo{}{o} \; \ireduce \; + \{ e \mapsto \intra(o) \}\\\\ +%Nop +\textrm{\textsf{No Operation}} & (3) &\transfer{\intra}{\unop}{\lbtrue} = \intra \\\\ +\bottomrule +\end{array} +$ +} +\end{longtable} +% + +The data-flow equations given in Table~\ref{structures} correspond to +structure-related statements. For the equations \snumber{4}, \snumber{5}, +\snumber{6} and \snumber{7} we assume that the variable $r$ is of type +$\commonstype$ for some fields $f_i,\; 1 \leq i \leq n$. The equation \snumber{4} +refers to the creation of a structure: each input $e_i$ is read as much as the +corresponding field $f_i$ of the structure is read. +% +The destructuring of a structure is handled in \snumber{5}: each field $f_i$ is +needed as much as the corresponding variable $o_i$ is. +% +When accessing the $i$-th field of a structure $r$ \snumber{6}, only the field +$f_i$ is read, and only as much as the access' result $o$ itself. +% +The equation \snumber{7} treats field updates: the variable $e_i$ is read as much +as the field $f_i$ is. The structure $r$ is read as much as all the fields other +than $f_i$ are read in $r'$. +% +Finally, the equations given in \snumber{8} handle partial structure equality +tests, and the transfer functions are the same for the labels \lbtrue{} or +\lbfalse: for both compared structures $r'$ and $r''$, all the fields in the given +set $f_1, \ldots, f_k$ are completely read, and only those. + +\begin{longtable}{@{}c@{}} +\caption{Structure-Related Statements -- Data-Flow Equations} +\ra{1.3} +\label{structures} +\endlastfoot +\resizebox{0.99\linewidth}{!}{ +$ +\begin{array}{@{}lcl@{}} +\toprule + \textsf{Statement} & & \transfer {\intra}{s}{\lambda_i} \\ +\midrule +%Create Structure +\textrm{\textsf{Create}} & \textrm{(4)} +& \transfer{\intra}{\recordnew}{\textrm{\textsf{\lbtrue}}} = +\displaystyle \killo {}{r} \; \ireduce \; \displaystyle \bigoplus_{1\leq i \leq n}\{e_i \mapsto \intra(r).f_i \}\\\\ +% Destruct structure +\textrm{\textsf{Destructure}} & \textrm{(5)} +& \transfer{\intra}{\recordall}{\textrm{\textsf{\lbtrue}}} = +\displaystyle \killo {}{ \{o_i \ver o_i \in \bar{o} \}} \; \ireduce \; +\displaystyle \{r \mapsto \{f_1 \mapsto\intra(o_1); \ldots; f_n \mapsto \intra(o_n)\}\}\\\\ +% Field Access +\textrm{\textsf{Access field}} & \textrm{(6)} +& \transfer{\intra}{\recordget}{\textrm{\textsf{\lbtrue}}} = +\displaystyle \killo {}{o} \; \ireduce \; \{r \mapsto \{f_1 \mapsto \oslash; \ldots; + f_i \mapsto \intra(o); \ldots; f_n \mapsto \oslash \} \}\\\\ +% Field Update +\textrm{\textsf{Update field}} & \textrm{(7)} +& \transfer{\intra}{\recordset}{\textrm{\textsf{\lbtrue}}} = + \displaystyle \killo{}{r'} + \; \ireduce \; + \left \{ + \begin{array}{lll} + e_i & \mapsto & \intra(r').f_i \\ + r & \mapsto & \left \{ \displaystyle + f_1 \mapsto \delta_1; \ldots ; f_n \mapsto \delta_n + \right \} + \end{array} + \right \} \\\\ +&& \textrm{where } \delta_j = \left \{ + \begin{array}{ll} + \intra(r').f_j & \textrm{if $j \neq i $} \\ + \oslash & \textrm{otherwise}\\ + \end{array} \right . \\\\ +% Structure Equality +\textrm{\textsf{Equality}} & \textrm{(8)} +& +\begin{tabular}{@{}lccl@{}} +$\transfer{\intra}{\recordeq}{\lbtrue} = \displaystyle + \intra \; \ireduce \; d$ +&&& +%\textrm{where} +$ \textrm{where } d = \left \{ + \begin{array} {lll} + r' & \mapsto & \displaystyle \left \{ f_1 \mapsto \delta_1; \ldots ; f_n \mapsto \delta_n + \right \} \\ + r'' & \mapsto & \displaystyle \left \{ f_1 \mapsto \delta_1; \ldots; f_n \mapsto \delta_n + \right \} + \end{array} + \right \} +\; + $ \\\\ +$\transfer{\intra}{\recordeq}{\lbfalse} = \displaystyle + \intra \; \ireduce \; d $ +&&& $\textrm{and } \delta_i = \left \{ + \begin{array} {ll} + \top & \textrm{if } f_i \in \{f_1, \ldots, f_k\}\\ + \oslash & \textrm{otherwise} + \end{array} + \right. +\; + $ +\end{tabular}\\ \\ +\bottomrule +\end{array} +$ +} +\end{longtable} + + +%%% More tables for arrays and variants at line 1985 in Chapter5.tex + + +\subsection{Intraprocedural Dependency Analysis Illustrated}\label{sec:intra:example} + +To better illustrate our analysis at an intraprocedural level, we exemplify +the mechanism behind it, step by step, on the predicate \disp{thread}, discussed +in Section~\ref{sec:intro:example}. We consider the \disp{true} execution +scenario, apply our dependency analysis and compare the actual obtained results +with the targeted ones depicted in Figure~\ref{ex:res:thread}. + +\definecolor{indianred}{rgb}{0.90, 0.80, 0.71} %melon +\definecolor{burg}{rgb}{0.8, 0.36, 0.36} +\tikzstyle{vertex} = [ellipse, fill=lightgray!50, minimum size =30pt, inner sep = 0pt] +\tikzstyle{lvertex} = [circle, fill=lightgray!50, minimum size=30pt, inner sep=0pt] +\tikzstyle{ivertex} = [circle, draw=red, minimum size=30pt, inner sep = 0pt] +\tikzstyle{edge} = [draw, semithick, -> ] +\tikzstyle{edgeRed} = [draw=red!50!black, dashed, thick, -> ] +\begin{figure}[h]\centering +\begin{tabular}{@{}c@{}} +\toprule +%% \begin{tikzpicture} +%% [scale=0.6, auto] +%% \node[vertex] (n1) at (10,14) {\emph{threads := p.threads}}; +%% \node[vertex] (n2) at (10,11) {\emph{tio := threads[i]}}; +%% \node[vertex] (n3) at (10,8) {\emph{switch(tio) as [ti$\arrowvert\;$]}}; + +%% \node (n4) [draw=red!50!black, circle,fill=lightgray!50, minimum size=30pt, inner sep =0pt] at(8,5.5) {\emph{true}}; +%% \draw[draw=red!50!black] (8,5.5) circle(20pt); + +%% \node (n5) [draw=red!50!black, circle,fill=lightgray!50, minimum size=30pt, inner sep =0pt] at(12,5.5) {\emph{None}}; +%% \draw[draw=red!50!black] (12,5.5) circle(20pt); + +%% \foreach \from/\to in {n1/n2,n2/n3,n3/n4,n3/n5}{ +%% \draw[edge] (\from) -- (\to); +%% } + +%% \draw (n2.-30) edge[semithick,->,bend left,in=120] (n5.30); + +%% \node(n8) [draw=indianred!50, fill = indianred!50, scale=0.7] at (17.5, 4) { +%% \textrm{thread(p, i) $\to$ [true: ti $\ver$ None]}}; + +%% \node(n9)[draw=burg, scale = 0.8] at (15.75,5.5) { +%% \begin{tabular}{c} +%% $ \mathit{Unreachable} $\\ +%% \end{tabular} +%% }; + +%% \node(d1) [draw=caribbeangreen, scale = 0.9] at (3,5.5) { +%% \begin{tabular}{c} +%% ti $\mapsto$ $\top$\\ +%% \end{tabular} +%% }; + +%% \end{tikzpicture} + \begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node distance=1.2cm, semithick, + statt/.style={scale=0.7,fill=lightgray!50,draw=none,text=black,ellipse,inner sep=0pt,minimum width=.7cm,minimum height=.7cm}] +% + \node[statt] (N1) {\large {th := p.threads}}; + \node[statt] (N2) [below=1cm of N1] {\large {tio := th[i]}}; + \node[statt] (N3) [below left=of N2] {\large {$\boldsymbol{switch}$(tio) $\boldsymbol{as}$ + [ $\ver$ti}]}; + \node[statt] (N4) [below right=of N2]{\textsf{oob}}; + \node[statt] (N5) [below left=of N3]{\lbtrue}; + \node[statt] (N6) [below right=of N3]{\textsf{None}}; + \path (N1) edge node[xshift=-0.95cm] {\large {\lbtrue}} (N2); + \path (N2) edge node[xshift=-0.8cm,yshift = 0.4cm] {\large{\lbtrue}} (N3); + \path (N2) edge node {\large {\lbfalse}} (N4); + \path (N3) edge node[left, anchor=south east] {\large {\textsf{Some}}} (N5); + \path (N3) edge node[right, anchor=south west] {\large {\textsf{None}}} (N6); + +\node(n8)[draw=burg,dotted, scale = 0.7, right=of N4, xshift=-1.6cm] { +\begin{tabular}{c} + $ \mathit{Unreachable} $\\ +\end{tabular} +}; + +\node(n9)[draw=burg,dotted, scale = 0.7, right=of N6] { +\begin{tabular}{c} + $ \mathit{Unreachable} $\\ +\end{tabular} +}; + +\node(d1) [draw=caribbeangreen, scale = 0.9, left=of N5] { +\begin{tabular}{c} +ti $\mapsto$ $\top$\\ +\end{tabular} +}; +\end{tikzpicture}\\ +\bottomrule +\end{tabular} +\caption{Analysing Predicate \disp{thread} -- Initialisation} +\label{intra:ss:init} +\end{figure} + +Since a predicate can only exit with one label at a time and we are considering +the \disp{true} label, we can map the nodes \disp{None} and \disp{oob} to +\emph{Unreachable}, as shown in Figure~\ref{intra:ss:init}. This is an advantage +of backwards analyses. For \disp{true}, we +make a pessimistic assumption and map the output \disp{ti} to {\everything}, +considering that control on the output is external and hence, out of our reach, +and that \disp{ti} will be entirely needed by a potential caller. Going further +up the control flow graph, we analyse the \emph{variant switch}. + +In order to compute the dependency for the node corresponding to the variant +switch, we apply the data-flow equation, given by \snumber{10} in +Table~\ref{variants}. Since we are analysing the \disp{true} case, we know that +all other constructors (only the constructor \disp{None} in this case) are +locally impossible. Thus, we map it to $\bot$. We continue by forgetting the +dependency information we knew about the output \disp{ti}. Since its value is +needed only in as much as the result of the switch on the corresponding edge is +needed, we forward it to the part corresponding to the \disp{Some} constructor. +This is summarized below: + +\begin{figure}[!h]\centering +\begin{tabular}{c} +%\begin{table}{@{}c@{}} +\toprule + \begin{tikzpicture}[ + dot/.style={circle,inner sep=0pt,minimum size=1mm,fill=black}, + ] + + \matrix[inner sep=0pt,ampersand replacement=\&] (mtop) { + \dottriangle{(0,0)}{1}{}{5}{4}{};\& + \node[resetinnersep, anchor=base,yshift=-.2cm] (dots2) {$\vphantom{x}\dots\vphantom{x}$};\& + \coordinate (myorigin); + \dottriangle{(0,0)}{ia}{}{5}{4}{}; + \coordinate[xshift=.15cm] (coord-ib) at (dottriangle-isep-ia.east |- myorigin); + \node[anchor=west,inner sep=0pt] (ioplus) at (dottriangle-boundingbox-ia.east) {$\vphantom{x}\mathbin{\oplus}\vphantom{x}\;$}; + \dottriangle{(ioplus.east |- myorigin)}{ib}{green!50!black}{5}{4}{fill=green!50!black!30!white}; + { + \node[anchor=west,inner sep=0pt,opacity=0] (ioplus) at (dottriangle-boundingbox-ia.east) {$\vphantom{x}\mathbin{\oplus}\vphantom{x}\;$}; + \dottriangle{(ioplus.east |- myorigin)}{ib}{green!50!black,opacity=0}{5}{4}{fill=green!50!black!30!white,opacity=0}; + } + \& + \node[resetinnersep, anchor=base,yshift=-.2cm] (dotsn1) {$\vphantom{x}\dots\vphantom{x}$};\& + \dottriangle{(0,0)}{n}{}{5}{4}{}; \\ + }; + + % Draw bottoms on top: + \node[fit=(dottriangle-bg-1),fill=red!20!white,inner sep=0pt,opacity=.9] {}; + \node[green!50!black] at (dottriangle-bg-1.center) {$\bot$}; + \node[fit=(dottriangle-bg-n),fill=red!20!white,inner sep=0pt,opacity=.9] {}; + \node[green!50!black] at (dottriangle-bg-n.center) {$\bot$}; + + \draw (dottriangle-isep-1.east |- mtop.north) -- (dottriangle-isep-1.east |- mtop.south); + \draw (dots2.east |- mtop.north) -- (dots2.east |- mtop.south); + \draw (dottriangle-isep-ib.east |- mtop.north) -- (dottriangle-isep-ib.east |- mtop.south); + \draw (dotsn1.east |- mtop.north) -- (dotsn1.east |- mtop.south); + + \node[resetinnersep,anchor=south,yshift=.3cm] at (dottriangle-dot-1 |- mtop.north) (num1) {\footnotesize$C_1$}; + \path ($(dottriangle-dot-ia)!.5!(dottriangle-dot-ib)$) |- node[resetinnersep,anchor=south,yshift=.3cm] (numi) {\footnotesize$C_{Some}$} (mtop.north); + \node[resetinnersep,anchor=south,yshift=.3cm] at (dottriangle-dot-n |- mtop.north) (numn) {\footnotesize$C_n$}; + + \node[inner sep=0pt,fit=(num1) (numi) (numn)] (mnum) {}; + \node[inner sep=0pt,fit=(mtop) (mnum)] (mall) {}; + + \path[fill=black!7] (mnum.south west -| mall.west) -- (mnum.south east -| mall.east) -- (mtop.north east -| mall.east) -- (mtop.north west -| mall.west) -- cycle; + \path (mnum.south west -| mall.west) edge[draw] (mnum.south east -| mall.east) -- (mtop.north east -| mall.east) edge[draw] (mtop.north west -| mall.west) -- cycle; + \draw (mall.north west) -- (mall.north east) -- (mall.south east) -- (mall.south west) -- cycle; + + \node[anchor=base east,xshift=\defaultinnersep] (a) at (dottriangle-x-1.base -| mall.west) {$\mathit{tio} =\vphantom{x}$}; + + \node[below left,yshift=-3mm] (o) at (mall.south west) {$\mathit{ti} =$}; + + \dottriangle{(o.base east)}{o}{red}{5}{4}{fill=red!30!white}; + % cross out: + \node[draw=red,cross out,inner sep=0pt,minimum width=.75cm,minimum height=.55cm,thick,opacity=.5] at (dottriangle-bg-o) {}; + { + \dottriangle{(o.base east)}{o}{}{5}{4}{}; + } + + \draw (dottriangle-tc-o) edge[->,>=stealth,bend right,thick,green!30!black] (dottriangle-tc-ib); + ; + \end{tikzpicture}\\ + %\end{figure} + + \definecolor{indianred}{rgb}{0.8, 0.36, 0.36} + +$ +\colorbox{lightgray!50}{ +\begin{tabular}{@{}l@{}} +$\transfer{\intra}{\varswitch}{\lambda_i} = +\displaystyle (\intra \setminus o_i) \oplus \{ v \mapsto dep_i\}$ +\\ +where \\ +$dep_i = [\colorbox{indianred}{$C_1 \mapsto \bot;$} \ldots; \colorbox{green!50!black!30!white}{$C_i \mapsto \intra(o_i);$} \ldots; \colorbox{indianred}{$C_n \mapsto \bot$}]$ +\end{tabular}} +%\bottomrule +$ \\ +\bottomrule +\end{tabular} +\caption{Applying the Variant Switch Equation} +\end{figure} + +\definecolor{indianred}{rgb}{0.8, 0.36, 0.36} + +\begin{figure}[h]\centering +\begin{tabular}{c} +\toprule +\resizebox{0.99\textwidth}{!}{% +%% \begin{tikzpicture} +%% [scale=0.6, auto] +%% \node[vertex] (n1) at (10,14) {\emph{threads := p.threads}}; +%% \node[vertex] (n2) at (10,11) {\emph{tio := threads[i]}}; +%% \node[vertex] (n3) at (10,8) {\emph{switch(tio) as [ti$\arrowvert\;$]}}; + +%% \node (n4) [draw=red!50!black, circle,fill=lightgray!50, minimum size=30pt, inner sep =0pt] at(8,5.5) {\emph{true}}; +%% \draw[draw=red!50!black] (8,5.5) circle(20pt); + +%% \node (n5) [draw=red!50!black, circle,fill=lightgray!50, minimum size=30pt, inner sep =0pt] at(12,5.5) {\emph{None}}; +%% \draw[draw=red!50!black] (12,5.5) circle(20pt); + +%% \foreach \from/\to in {n1/n2,n2/n3,n3/n4,n3/n5}{ +%% \draw[edge] (\from) -- (\to); +%% } + +%% \draw (n2.-30) edge[semithick,->,bend left,in=120] (n5.30); + +%% \node(n8) [draw=indianred!50, fill = indianred!50, scale=0.7] at (17.5, 4) { +%% \textrm{thread(p, i) $\to$ [true: ti $\ver$ None]}}; + +%% \node(n9)[draw=burg, scale = 0.8] at (15.75,5.5) { +%% \begin{tabular}{c} +%% $ \mathit{Unreachable} $\\ +%% \end{tabular} +%% }; + +%% \node(d2) [draw=caribbeangreen, scale=0.8] at (2.5,8) { +%% \begin{tabular}{ccc} +%% tio & $\mapsto$ & [Some $\mapsto \top$; None $\mapsto \bot$] \\ +%% \end{tabular} +%% }; + +%% \node(d1) [draw=caribbeangreen, scale = 0.9] at (3,5.5) { +%% \begin{tabular}{c} +%% ti $\mapsto$ $\top$\\ +%% \end{tabular} +%% }; + +%% \end{tikzpicture} + \begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node distance=1.2cm, semithick, + statt/.style={scale=0.7,fill=lightgray!50,draw=none,text=black,ellipse,inner sep=0pt,minimum width=.7cm,minimum height=.7cm}] +% + \node[statt] (N1) {\large {th := p.threads}}; + \node[statt] (N2) [below=1cm of N1] {\large {tio := th[i]}}; + \node[statt] (N3) [below left=of N2] {\large {$\boldsymbol{switch}$(tio) $\boldsymbol{as}$ + [ $\ver$ti}]}; + \node[statt] (N4) [below right=of N2]{\textsf{oob}}; + \node[statt] (N5) [below left=of N3]{\lbtrue}; + \node[statt] (N6) [below right=of N3]{\textsf{None}}; + \path (N1) edge node[xshift=-0.95cm] {\large {\lbtrue}} (N2); + \path (N2) edge node[xshift=-0.8cm,yshift = 0.4cm] {\large{\lbtrue}} (N3); + \path (N2) edge node {\large {\lbfalse}} (N4); + \path (N3) edge node[left, anchor=south east] {\large {\textsf{Some}}} (N5); + \path (N3) edge node[right, anchor=south west] {\large {\textsf{None}}} (N6); + +\node(n8)[draw=burg,dotted, scale = 0.7, right=of N4, xshift=-1.6cm] { +\begin{tabular}{c} + $ \mathit{Unreachable} $\\ +\end{tabular} +}; + +\node(n9)[draw=burg,dotted, scale = 0.7, right=of N6] { +\begin{tabular}{c} + $ \mathit{Unreachable} $\\ +\end{tabular} +}; + +\node(d2) [draw=caribbeangreen, scale=0.8, left=of N3] { +\begin{tabular}{ccc} +tio & $\mapsto$ & [Some $\mapsto \top$; None $\mapsto \bot$] \\ +\end{tabular} +}; + +\node(d1) [draw=caribbeangreen, scale = 0.9, left=of N5] { +\begin{tabular}{c} +ti $\mapsto$ $\top$\\ +\end{tabular} +}; +\end{tikzpicture} +}\\ +\bottomrule +\end{tabular} +\caption{Analysing Predicate \disp{thread} -- Variant Switch} +\label{intra:ss:switch} +\end{figure} + +Taking all this into account, for the node corresponding to the variant switch, +we obtain the dependency shown in Figure~\ref{intra:ss:switch}. For the output +\disp{ti}, we depend entirely on the \disp{Some} constructor of the node's +input variant \disp{tio}, while the constructor \disp{None} is impossible. + +Making a step further up the graph, we access the cell \disp{i} of the array +\disp{th} and apply the equation \snumber{12} given in Table~\ref{arrays}. +We begin by forgetting the dependency for the output \disp{tio}, +since this is written. Since we only access the element \disp{i}, we map all +other cells to \emph{Nothing}, i.e. $\oslash$. To the dependency corresponding +to the \disp{i}-th cell, we forward the dependency we knew about \disp{tio}, +since we depend on it to the extent to which the result of the access is needed. + +\begin{figure}[!h]\centering +\begin{tabular}{c} +\toprule + \begin{tikzpicture}[ + dot/.style={circle,inner sep=0pt,minimum size=1mm,fill=black}, + ] + + \matrix[inner sep=0pt,ampersand replacement=\&] (mtop) { + \dottriangle{(0,0)}{1}{}{5}{4}{}; + \node[anchor=west,inner sep=1.3mm,xshift=-1.3mm] (1oplus) at (dottriangle-boundingbox-1.east) + {$\vphantom{x}\mathbin{\oplus}\textcolor{green!50!black}{\oslash}$}; + { + \node[anchor=west,inner sep=1.3mm,xshift=-1.3mm,opacity=0] (1oplus) at (dottriangle-boundingbox-1.east) +{$\vphantom{x}\mathbin{\oplus}\textcolor{green!50!black}{\oslash}$}; + } \& + \node[resetinnersep, anchor=base,yshift=-.2cm] (dots2) {$\vphantom{x}\dots\vphantom{x}$};\& + \coordinate (myorigin); + \dottriangle{(0,0)}{ia}{}{5}{4}{}; + %\alt<3->{ + \node[anchor=west,inner sep=0pt] (ioplus) at (dottriangle-boundingbox-ia.east) + {$\vphantom{x}\mathbin{\oplus}\vphantom{x}\;$}; + \dottriangle{(ioplus.east |- myorigin)}{ib}{green!50!black}{5}{4}{fill=green!50!black!30!white}; + { + \node[anchor=west,inner sep=0pt,opacity=0] (ioplus) at (dottriangle-boundingbox-ia.east) +{$\vphantom{x}\mathbin{\oplus}\vphantom{x}\;$}; + \dottriangle{(ioplus.east |- myorigin)}{ib}{green!50!black,opacity=0}{5}{4}{fill=green!50!black!30!white,opacity=0}; + }\& + \node[resetinnersep, anchor=base,yshift=-.2cm] (dotsn1) {$\vphantom{x}\dots\vphantom{x}$};\& + % \dottriangle{(0,0)}{n1}{}{5}{4}{}; \& + \dottriangle{(0,0)}{n}{}{5}{4}{}; + + \node[anchor=west,inner sep=1.3mm,xshift=-1.3mm] (noplus) at (dottriangle-boundingbox-n.east) + {$\vphantom{x}\mathbin{\oplus}\textcolor{green!50!black}{\oslash}$}; + { + \node[anchor=west,inner sep=1.3mm,xshift=-1.3mm,opacity=0] (noplus) at (dottriangle-boundingbox-n.east) +{$\vphantom{x}\mathbin{\oplus}\textcolor{green!50!black}{\oslash}$}; + } \\ + }; + + \draw (1oplus.east |- mtop.north) -- (1oplus.east |- mtop.south); + \draw (dots2.east |- mtop.north) -- (dots2.east |- mtop.south); + \draw (dottriangle-isep-ib.east |- mtop.north) -- (dottriangle-isep-ib.east |- mtop.south); + \draw (dotsn1.east |- mtop.north) -- (dotsn1.east |- mtop.south); + + \node[resetinnersep,anchor=south] at (dottriangle-dot-1 |- mtop.north) (num1) {\footnotesize$1$}; + \path ($(dottriangle-dot-ia)!.5!(dottriangle-dot-ib)$) |- node[resetinnersep,anchor=south] (numi) {\footnotesize$i$} (mtop.north); + \node[resetinnersep,anchor=south] at (dottriangle-dot-n |- mtop.north) (numn) {\footnotesize$n$}; + + \node[inner sep=0pt,fit=(num1) (numi) (numn)] (mnum) {}; + \node[inner sep=0pt,fit=(mtop) (mnum),draw] (mall) {}; + + \draw (mtop.north west) -- (mtop.north east); + + \node[anchor=base east,xshift=\defaultinnersep] (a) at (dottriangle-x-1.base -| mall.west) {$\mathit{th} =\vphantom{x}$}; + + \node[below left,yshift=-3mm] (o) at (mall.south west) {$\mathit{tio} =$}; + + \dottriangle{(o.base east)}{o}{red}{5}{4}{fill=red!30!white}; + % cross out: + \node[draw=red,cross out,inner sep=0pt,minimum width=.75cm,minimum height=.55cm,thick,opacity=.5] at (dottriangle-bg-o) {}; + { + \dottriangle{(o.base east)}{o}{}{5}{4}{}; + } + +% { + \node[draw=red,cross out,inner sep=0pt,minimum width=.75cm,minimum height=.55cm,thick,opacity=0] at (dottriangle-bg-ia) {}; + + \draw (dottriangle-tc-o) edge[->,>=stealth,bend right,thick,green!30!black] (dottriangle-tc-ib); + ; + \end{tikzpicture}\\ + + +\resizebox{0.95\textwidth}{!}{ +\colorbox{lightgray!50}{ +$\transfer{\intra}{\arrayget}{\lbtrue} = \displaystyle + \left \lgroup + \begin {array}{ll} + \colorbox{indianred}{$\killo{}{o} $}\; \oplus \; + \left \{ + \begin{array}{lll} + i & \mapsto & \top \\%{green!50!black!30!white} + a & \mapsto & \colorbox{green!50!black!30!white}{$\langle \oslash \; \triangleright \; i: \intra(o) \rangle$} + \end{array} \right \} + & \begin{array}{l} + \textrm{when $ i \in \inputs \;$} \\ + \end{array} + \\ \\ + \colorbox{indianred}{$\killo{}{o}$} \; \oplus \; + \left \{ + \begin{array} {lll} + i & \mapsto & \top \\ + a & \mapsto &\colorbox{green!50!black!30!white}{$ \langle \intra(o) \vee \oslash \rangle$} + \end{array} + \right \} + & \begin{array}{l} + \textrm {when $ i \notin \inputs \;$} \\ + \end{array} + \\ + \end{array} \right. + $ +}}\\ +\bottomrule +\end{tabular} +\caption{Applying the Array Access Equation} +\label{fig:eq:array} +\end{figure} + +We thus obtain a dependency stating that we depend only on the \disp{i}-th +cell of the array \disp{th}, for which only the constructor \disp{Some} is +possible and entirely needed. The cell's index \disp{i} is entirely needed as +well. The applied equation is shown in Figure~\ref{fig:eq:array} (since \disp{i} +is an input, we use the first case of the equation) and the +obtained results are shown in Figure~\ref{intra:ss:array}. + +\begin{figure}[h]\centering +\begin{tabular}{@{}c@{}} +\toprule +\resizebox{0.99\textwidth}{!}{% +%% \begin{tikzpicture} +%% [scale=0.6, auto] +%% \node[vertex] (n1) at (10,14) {\emph{threads := p.threads}}; +%% \node[vertex] (n2) at (10,11) {\emph{tio := threads[i]}}; +%% \node[vertex] (n3) at (10,8) {\emph{switch(tio) as [ti$\arrowvert\;$]}}; + +%% \node (n4) [draw=red!50!black, circle,fill=lightgray!50, minimum size=30pt, inner sep =0pt] at(8,5.5) {\emph{true}}; +%% \draw[draw=red!50!black] (8,5.5) circle(20pt); + +%% \node (n5) [draw=red!50!black, circle,fill=lightgray!50, minimum size=30pt, inner sep =0pt] at(12,5.5) {\emph{None}}; +%% \draw[draw=red!50!black] (12,5.5) circle(20pt); + +%% \foreach \from/\to in {n1/n2,n2/n3,n3/n4,n3/n5}{ +%% \draw[edge] (\from) -- (\to); +%% } + +%% \draw (n2.-30) edge[semithick,->,bend left,in=120] (n5.30); + +%% \node(n8) [draw=indianred!50, fill = indianred!50, scale=0.7] at (17.5, 4) { +%% \textrm{thread(p, i) $\to$ [true: ti $\ver$ None]}}; + +%% \node(n9)[draw=burg, scale = 0.8] at (15.75,5.5) { +%% \begin{tabular}{c} +%% $ \mathit{Unreachable} $\\ +%% \end{tabular} +%% }; + +%% \node(d3) [draw=caribbeangreen, scale=0.8] at (1.4,10.8) { +%% \begin{tabular}{cll} +%% threads & $\mapsto $ +%% & $\langle \oslash\;\; \triangleright\;$ i: [Some $\mapsto \top$; None $\mapsto \bot$] $\rangle$ \\ + +%% i & $\mapsto$ &$\top$\\ +%% \end{tabular} +%% }; + +%% \node(d2) [draw=caribbeangreen, scale=0.8] at (2.5,8) { +%% \begin{tabular}{ccc} +%% tio & $\mapsto$ & [Some $\mapsto \top$; None $\mapsto \bot$] \\ +%% \end{tabular} +%% }; + +%% \node(d1) [draw=caribbeangreen, scale = 0.9] at (3,5.5) { +%% \begin{tabular}{c} +%% ti $\mapsto$ $\top$\\ +%% \end{tabular} +%% }; + +%% \end{tikzpicture} + \begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node distance=1.2cm, semithick, + statt/.style={scale=0.7,fill=lightgray!50,draw=none,text=black,ellipse,inner sep=0pt,minimum width=.7cm,minimum height=.7cm}] +% + \node[statt] (N1) {\large {th := p.threads}}; + \node[statt] (N2) [below=1cm of N1] {\large {tio := th[i]}}; + \node[statt] (N3) [below left=of N2] {\large {$\boldsymbol{switch}$(tio) $\boldsymbol{as}$ + [ $\ver$ti}]}; + \node[statt] (N4) [below right=of N2]{\textsf{oob}}; + \node[statt] (N5) [below left=of N3]{\lbtrue}; + \node[statt] (N6) [below right=of N3]{\textsf{None}}; + \path (N1) edge node[xshift=-0.95cm] {\large {\lbtrue}} (N2); + \path (N2) edge node[xshift=-0.8cm,yshift = 0.4cm] {\large{\lbtrue}} (N3); + \path (N2) edge node {\large {\lbfalse}} (N4); + \path (N3) edge node[left, anchor=south east] {\large {\textsf{Some}}} (N5); + \path (N3) edge node[right, anchor=south west] {\large {\textsf{None}}} (N6); + +\node(n8)[draw=burg,dotted, scale = 0.7, right=of N4, xshift=-1.6cm] { +\begin{tabular}{c} + $ \mathit{Unreachable} $\\ +\end{tabular} +}; + +\node(n9)[draw=burg,dotted, scale = 0.7, right=of N6] { +\begin{tabular}{c} + $ \mathit{Unreachable} $\\ +\end{tabular} +}; + +\node(d3) [draw=caribbeangreen, scale=0.8, left=of N2] { +\begin{tabular}{cll} +th & $\mapsto $ +& $\langle \oslash\;\; \triangleright\;$ i: [Some $\mapsto \top$; None $\mapsto \bot$] $\rangle$ \\ +i & $\mapsto$ &$\top$\\ +\end{tabular} +}; + +\node(d2) [draw=caribbeangreen, scale=0.8, left=of N3] { +\begin{tabular}{ccc} +tio & $\mapsto$ & [Some $\mapsto \top$; None $\mapsto \bot$] \\ +\end{tabular} +}; + +\node(d1) [draw=caribbeangreen, scale = 0.9, left=of N5] { +\begin{tabular}{c} +ti $\mapsto$ $\top$\\ +\end{tabular} +}; +\end{tikzpicture} +}\\ +\bottomrule +\end{tabular} +\caption{Analysing Predicate \disp{thread} -- Array Access} +\label{intra:ss:array} +\end{figure} + +As a last step, we access the field \disp{threads} of the input process \disp{p} +and apply the equation \snumber{6} given in Table~\ref{structures} and illustrated in +Figure~\ref{intra:ss:faccess}. +As before, we forget the information for \disp{th}, the access result. We +map all other fields to $\oslash$ and we forward the dependency of the variable +\disp{th} to the dependency part of the field \disp{threads}. + +\begin{figure}[!h] +\begin{tabular}{c} +\toprule + % \centering + \begin{tikzpicture}[ + dot/.style={circle,inner sep=0pt,minimum size=1mm,fill=black}, +% every node/.style={draw=black!50!white} + ] + + \matrix[inner sep=0pt,ampersand replacement=\&] (mtop) { + \node[resetinnersep,] (f1) {$f_1=$}; \dottriangle{(f1.base east)}{1}{}{3}{4}{}; + %\alt<3->{ + \node[anchor=west,inner sep=1.3mm,xshift=-1.3mm] (1oplus) at (dottriangle-boundingbox-1.east) + {$\vphantom{x}\mathbin{\oplus}\textcolor{green!50!black}{\oslash}$}; + { + \node[anchor=west,inner sep=1.3mm,xshift=-1.3mm,opacity=0] (1oplus) at (dottriangle-boundingbox-1.east) + {$\vphantom{x}\mathbin{\oplus}\textcolor{green!50!black}{\oslash}$}; + } \& + \& + \node[resetinnersep,] (f2) {$f_2=$}; \dottriangle{(f2.base east)}{2}{}{5}{4}{}; + %\alt<3->{ + \node[anchor=west,inner sep=1.3mm,xshift=-1.3mm] (2oplus) at (dottriangle-boundingbox-2.east) + {$\vphantom{x}\mathbin{\oplus}\textcolor{green!50!black}{\oslash}$}; + { + \node[anchor=west,inner sep=1.3mm,xshift=-1.3mm,opacity=0] (2oplus) at (dottriangle-boundingbox-2.east) + {$\vphantom{x}\mathbin{\oplus}\textcolor{green!50!black}{\oslash}$}; + } \\ + }; + + \matrix[inner sep=0pt,below=0cm of mtop, ampersand replacement=\&] (mmid) { + \node[resetinnersep,] (fi) {$f_{threads}=\vphantom{x}$}; + % \alt<2->{ + % \dottriangle{([xshift=-\defaultinnersep]fi.base east)}{ia}{}{5}{3}{fill=red!30!white}; + % }{ + \dottriangle{([xshift=-\defaultinnersep]fi.base east)}{ia}{}{3}{5}{}; + % } + \node[anchor=base west,inner sep=0pt] (ioplus) at (dottriangle-boundingbox-ia.east |- fi.base) {$\vphantom{x}\mathbin{\oplus}\vphantom{x}\;$}; + \dottriangle{(ioplus.base east)}{ib}{green!50!black}{3}{5}{fill=green!50!black!30!white}; + { + \node[anchor=base west,inner sep=0pt,opacity=0] (ioplus) at (dottriangle-boundingbox-ia.east |- fi.base) {$\vphantom{x}\mathbin{\oplus}\vphantom{x}\;$}; + \dottriangle{(ioplus.base east)}{ib}{green!50!black,opacity=0}{3}{5}{fill=green!50!black!30!white,opacity=0}; + }\\ + }; + + \matrix[inner sep=0pt,below=0cm of mmid,ampersand replacement=\&] (mbot) { + \node[resetinnersep,] (fn1) {$f_{n-1}=$}; \dottriangle{(fn1.base east)}{n1}{}{4}{3}{}; + \node[anchor=west,inner sep=1.3mm,xshift=-1.3mm] (n1oplus) at (dottriangle-boundingbox-n1.east) + {$\vphantom{x}\mathbin{\oplus}\textcolor{green!50!black}{\oslash}$}; + { + \node[anchor=west,inner sep=1.3mm,xshift=-1.3mm,opacity=0] (n1oplus) at (dottriangle-boundingbox-n1.east) + {$\vphantom{x}\mathbin{\oplus}\textcolor{green!50!black}{\oslash}$}; + } \& + \node[resetinnersep,] (fn) {$f_{n}=$}; \dottriangle{(fn.base east)}{n}{}{4}{5}{}; + %\alt<3->{ + \node[anchor=west,inner sep=1.3mm,xshift=-1.3mm] (noplus) at (dottriangle-boundingbox-n.east) + {$\vphantom{x}\mathbin{\oplus}\textcolor{green!50!black}{\oslash}$}; + { + \node[anchor=west,inner sep=1.3mm,xshift=-1.3mm,opacity=0] (noplus) at (dottriangle-boundingbox-n.east) + {$\vphantom{x}\mathbin{\oplus}\textcolor{green!50!black}{\oslash}$}; + } \\ + }; + + \node[inner sep=0pt,fit=(mtop) (mmid) (mbot),draw] (mall) {}; + \draw (mtop.south -| mall.west) -- (mtop.south -| mall.east); + \draw (mmid.south -| mall.west) -- (mmid.south -| mall.east); + % \draw (f2.west |- mtop.north) -- (f2.west |- mtop.south); + \draw (1oplus.east |- mtop.north) -- (1oplus.east |- mtop.south); + % \draw (fn.west |- mbot.north) -- (fn.west |- mbot.south); + \draw (n1oplus.east |- mbot.north) -- (n1oplus.east |- mbot.south); + + \node[anchor=base east,xshift=\defaultinnersep] (s) at (f1.base -| mall.west) {$p =\vphantom{x}$}; + + \node[below left,yshift=-3mm] (o) at (mall.south west) {$th =$}; + + + \dottriangle{(o.base east)}{o}{red}{3}{5}{fill=red!30!white}; + % cross out: + \node[draw=red,cross out,inner sep=0pt,minimum size=.55cm,thick,opacity=.5] at (dottriangle-bg-o) {}; + { + \dottriangle{(o.base east)}{o}{}{3}{5}{}; + } + + \draw (dottriangle-tc-o) edge[->,>=stealth,bend right,thick,green!30!black] (dottriangle-tc-ib); + + \end{tikzpicture}\\ + +\colorbox{lightgray!50}{ +$\transfer{\intra}{\recordget}{\textrm{\textsf{\lbtrue}}} = +\displaystyle +\colorbox{indianred} {$\killo {}{o}$} +\; \oplus \; \{s \mapsto \{f_1 \mapsto \oslash; \ldots; +\colorbox{green!50!black!30!white} {$f_i \mapsto \intra(o);$} +\ldots; f_n \mapsto \oslash \} \} +$ +}\\ +\bottomrule +\end{tabular} +\caption{Applying the Field Access Equation} +\label{intra:ss:faccess} +\end{figure} + +We thus obtain the dependency result shown in Figure~\ref{intra:ss:struct}. +This states that for the label \disp{true}, the output \disp{ti} depends only on +the \disp{i}-th cell of the field \disp{threads} of the input process \disp{p}, +for which it depends entirely on the \disp{Some} constructor. Before returning +the predicate's final results, the analysis filters out any dependency +information referring to local variables and verifies that the invariant imposed +on dependency information related to arrays holds. Since the results refer only +to the inputs \disp{p} and \disp{i} and the index of the exceptional computed +dependency is an input, the invariant holds and the final result can be retrieved. +The final dependency results obtained for the \disp{thread} predicate on the exit +label \disp{true} are identical to the ones that we were targeting and that were +depicted in Figure~\ref{ex:res:thread}. For readability considerations, for +structures such as the input process \disp{p}, we omit dependencies on fields +mapped to $\oslash$. We maintain this convention throughout the rest of this +chapter, and thus any field of a structure that is omitted from a dependency +summary should be interpreted as being mapped to $\oslash$, i.e. \emph{nothing}. + +%de sters +%pana aici + +\begin{figure}[htbp]\centering +\begin{tabular}{c} +\toprule +\resizebox{0.99\textwidth}{!}{% +%% \begin{tikzpicture} +%% [scale=0.6, auto] +%% \node[vertex] (n1) at (10,14) {\emph{threads := p.threads}}; +%% \node[vertex] (n2) at (10,11) {\emph{tio := threads[i]}}; +%% \node[vertex] (n3) at (10,8) {\emph{switch(tio) as [ti$\arrowvert\;$]}}; + +%% \node (n4) [draw=red!50!black, circle,fill=lightgray!50, minimum size=30pt, inner sep =0pt] at(8,5.5) {\emph{true}}; +%% \draw[draw=red!50!black] (8,5.5) circle(20pt); + +%% \node (n5) [draw=red!50!black, circle,fill=lightgray!50, minimum size=30pt, inner sep =0pt] at(12,5.5) {\emph{None}}; +%% \draw[draw=red!50!black] (12,5.5) circle(20pt); + +%% \foreach \from/\to in {n1/n2,n2/n3,n3/n4,n3/n5}{ +%% \draw[edge] (\from) -- (\to); +%% } + +%% \draw (n2.-30) edge[semithick,->,bend left,in=120] (n5.30); + +%% \node(n8) [draw=indianred!50, fill = indianred!50, scale=0.7] at (17.5, 4) { +%% \textrm{thread(p, i) $\to$ [true: ti $\ver$ None]}}; + +%% \node(n9)[draw=burg, scale = 0.8] at (15.75,5.5) { +%% \begin{tabular}{c} +%% $ \mathit{Unreachable} $\\ +%% \end{tabular} +%% }; + +%% \node(d4) [draw=caribbeangreen, scale=0.7] at (0.6, 14) { +%% \begin{tabular}{lll} +%% p & $\mapsto $ +%% & \{ threads $\mapsto$ $\langle \oslash\;\; \triangleright\; $ i: +%% [Some $\mapsto \top$; \textrm{None $\mapsto \bot$}]$\rangle\}$ \\ +%% i & $\mapsto$ & $\top$ \\ +%% \end{tabular} +%% }; + +%% \node(d3) [draw=caribbeangreen, scale=0.8] at (1.4,10.8) { +%% \begin{tabular}{cll} +%% threads & $\mapsto $ +%% & $\langle \oslash\;\; \triangleright\;$ i: [Some $\mapsto \top$; None $\mapsto \bot$] $\rangle$ \\ + +%% i & $\mapsto$ &$\top$\\ +%% \end{tabular} +%% }; + +%% \node(d2) [draw=caribbeangreen, scale=0.8] at (2.5,8) { +%% \begin{tabular}{ccc} +%% tio & $\mapsto$ & [Some $\mapsto \top$; None $\mapsto \bot$] \\ +%% \end{tabular} +%% }; + +%% \node(d1) [draw=caribbeangreen, scale = 0.9] at (3,5.5) { +%% \begin{tabular}{c} +%% ti $\mapsto$ $\top$\\ +%% \end{tabular} +%% }; + +%% \end{tikzpicture} + + \begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node distance=1.2cm, semithick, + statt/.style={scale=0.7,fill=lightgray!50,draw=none,text=black,ellipse,inner sep=0pt,minimum width=.7cm,minimum height=.7cm}] +% + \node[statt] (N1) {\large {th := p.threads}}; + \node[statt] (N2) [below=1cm of N1] {\large {tio := th[i]}}; + \node[statt] (N3) [below left=of N2] {\large {$\boldsymbol{switch}$(tio) $\boldsymbol{as}$ + [ $\ver$ti}]}; + \node[statt] (N4) [below right=of N2]{\textsf{oob}}; + \node[statt] (N5) [below left=of N3]{\lbtrue}; + \node[statt] (N6) [below right=of N3]{\textsf{None}}; + \path (N1) edge node[xshift=-0.95cm] {\large {\lbtrue}} (N2); + \path (N2) edge node[xshift=-0.8cm,yshift = 0.4cm] {\large{\lbtrue}} (N3); + \path (N2) edge node {\large {\lbfalse}} (N4); + \path (N3) edge node[left, anchor=south east] {\large {\textsf{Some}}} (N5); + \path (N3) edge node[right, anchor=south west] {\large {\textsf{None}}} (N6); + +\node(n8)[draw=burg,dotted, scale = 0.7, right=of N4, xshift=-1.6cm] { +\begin{tabular}{c} + $ \mathit{Unreachable} $\\ +\end{tabular} +}; + +\node(n9)[draw=burg,dotted, scale = 0.7, right=of N6] { +\begin{tabular}{c} + $ \mathit{Unreachable} $\\ +\end{tabular} +}; + +\node(d4) [draw=caribbeangreen, scale=0.7, left=of N1] { +\begin{tabular}{lll} +p & $\mapsto $ +& \{ threads $\mapsto$ $\langle \oslash\;\; \triangleright\; $ i: +[Some $\mapsto \top$; \textrm{None $\mapsto \bot$}]$\rangle\}$ \\ +i & $\mapsto$ & $\top$ \\ +\end{tabular} +}; + +\node(d3) [draw=caribbeangreen, scale=0.8, left=of N2] { +\begin{tabular}{cll} +th & $\mapsto $ +& $\langle \oslash\;\; \triangleright\;$ i: [Some $\mapsto \top$; None $\mapsto \bot$] $\rangle$ \\ + +i & $\mapsto$ &$\top$\\ +\end{tabular} +}; + +\node(d2) [draw=caribbeangreen, scale=0.8, left=of N3] { +\begin{tabular}{ccc} +tio & $\mapsto$ & [Some $\mapsto \top$; None $\mapsto \bot$] \\ +\end{tabular} +}; + +\node(d1) [draw=caribbeangreen, scale = 0.9, left=of N5] { +\begin{tabular}{c} +ti $\mapsto$ $\top$\\ +\end{tabular} +}; +\end{tikzpicture} +}\\ +\bottomrule +\end{tabular} +\caption{Analysing Predicate \disp{thread} -- Field Access} +\label{intra:ss:struct} +\end{figure} + + +\subsection{An inter-procedural extension} + +\section{Correlation analysis} + +\subsection{Introductory example} + +\subsection{Correlations as partial equivalence relations} + +\subsection{Correlation analysis} + +\section{Experimental evaluation} + +\section{Related work} + +\section{Conclusions} + +\bibliographystyle{alpha} +\bibliography{biblio} + +\end{document}