 Timestamp:
 Mar 14, 2017, 11:14:29 AM (2 years ago)
 Location:
 Papers/jarcerco2017
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

Papers/jarcerco2017/cerco.bib
r3650 r3651 102 102 address = {New York, NY, USA}, 103 103 keywords = {CompCert, Compositional compiler verification, separate compilation}, 104 } 105 106 @Inbook{Atkey2010, 107 author="Atkey, Robert", 108 editor="Gordon, Andrew D.", 109 title="Amortised Resource Analysis with Separation Logic", 110 bookTitle="Programming Languages and Systems: 19th European Symposium on Programming, ESOP 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 2028, 2010. Proceedings", 111 year="2010", 112 publisher="Springer Berlin Heidelberg", 113 address="Berlin, Heidelberg", 114 pages="85103", 115 isbn="9783642119576", 116 doi="10.1007/9783642119576_6", 117 url="http://dx.doi.org/10.1007/9783642119576_6" 118 } 119 120 121 @Inbook{Aspinall2010, 122 author="Aspinall, David 123 and Atkey, Robert 124 and MacKenzie, Kenneth 125 and Sannella, Donald", 126 editor="Wirsing, Martin 127 and Hofmann, Martin 128 and Rauschmayer, Axel", 129 title="Symbolic and Analytic Techniques for Resource Analysis of Java Bytecode", 130 bookTitle="Trustworthly Global Computing: 5th International Symposium, TGC 2010, Munich, Germany, February 2426, 2010, Revised Selected Papers", 131 year="2010", 132 publisher="Springer Berlin Heidelberg", 133 address="Berlin, Heidelberg", 134 pages="122", 135 isbn="9783642156403", 136 doi="10.1007/9783642156403_1", 137 url="http://dx.doi.org/10.1007/9783642156403_1" 138 } 139 140 141 @article{Salvucci201627, 142 title = "Memory Consumption Analysis for a Functional and Imperative Language ", 143 journal = "Electronic Notes in Theoretical Computer Science ", 144 volume = "330", 145 number = "", 146 pages = "27  46", 147 year = "2016", 148 note = "\{RAC\} 2016  Resource Aware Computing ", 149 issn = "15710661", 150 doi = "http://dx.doi.org/10.1016/j.entcs.2016.12.013", 151 url = "http://www.sciencedirect.com/science/article/pii/S1571066116301207", 152 author = "Jérémie Salvucci and Emmanuel Chailloux", 153 keywords = "ML", 154 keywords = "regions", 155 keywords = "static analysis", 156 keywords = "memory analysis ", 157 abstract = "Abstract The omnipresence of resourceconstrained embedded systems makes them critical components. Programmers have to provide strong guarantees about their runtime behavior to make them reliable. Among these, giving an upper bound of live memory at runtime is mandatory to prevent heap overflows from happening. The paper proposes a semiautomatic technique to infer the space complexity of MLlike programs with explicit region management. It aims at combining existing formalisms to obtain the space complexity of imperative and purely functional programs in a consistent framework. " 158 } 159 160 161 @Inbook{Hoffmann2015, 162 author="Hoffmann, Jan 163 and Shao, Zhong", 164 editor="Vitek, Jan", 165 title="Automatic Static Cost Analysis for Parallel Programs", 166 bookTitle="Programming Languages and Systems: 24th European Symposium on Programming, ESOP 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 1118, 2015, Proceedings", 167 year="2015", 168 publisher="Springer Berlin Heidelberg", 169 address="Berlin, Heidelberg", 170 pages="132157", 171 isbn="9783662466698", 172 doi="10.1007/9783662466698_6", 173 url="http://dx.doi.org/10.1007/9783662466698_6" 174 } 175 176 177 @inproceedings{HAH12, 178 author = {Jan Hoffmann and Klaus Aehlig and 179 Martin Hofmann}, 180 title = {{Resource Aware ML}}, 181 booktitle = {{24rd International Conference on Computer Aided 182 Verification (CAV'12)}}, 183 publisher = {Springer}, 184 series = {Lecture Notes in Computer Science}, 185 volume = {7358}, 186 pages = {781786}, 187 year = {2012} 104 188 } 105 189 … … 377 461 address = {New York, NY, USA}, 378 462 keywords = {compiler verification, interactive proof assistants}, 379 } 463 } 464 465 @Article{Albert2011, 466 author="Albert, Elvira 467 and Arenas, Puri 468 and Genaim, Samir 469 and Puebla, Germ{\'a}n", 470 title="ClosedForm Upper Bounds in Static Cost Analysis", 471 journal="Journal of Automated Reasoning", 472 year="2011", 473 volume="46", 474 number="2", 475 pages="161203", 476 abstract="The classical approach to automatic cost analysis consists of two phases. Given a program and some measure of cost, the analysis first produces cost relations (CRs), i.e., recursive equations which capture the cost of the program in terms of the size of its input data. Second, CRs are converted into closedform, i.e., without recurrences. Whereas the first phase has received considerable attention, with a number of cost analyses available for a variety of programming languages, the second phase has been comparatively less studied. This article presents, to our knowledge, the first practical framework for the generation of closedform upper bounds for CRs which (1) is fully automatic, (2) can handle the distinctive features of CRs, originating from cost analysis of realistic programming languages, (3) is not restricted to simple complexity classes, and (4) produces reasonably accurate solutions. A key idea in our approach is to view CRs as programs, which allows applying semanticbased static analyses and transformations to bound them, namely our method is based on the inference of ranking functions and loop invariants and on the use of partial evaluation.", 477 issn="15730670", 478 doi="10.1007/s1081701091741", 479 url="http://dx.doi.org/10.1007/s1081701091741" 480 } 481 482 483 @article{ALBERT200767, 484 title = "Experiments in Cost Analysis of Java Bytecode", 485 journal = "Electronic Notes in Theoretical Computer Science", 486 volume = "190", 487 number = "1", 488 pages = "67  83", 489 year = "2007", 490 note = "", 491 issn = "15710661", 492 doi = "http://dx.doi.org/10.1016/j.entcs.2007.02.061", 493 url = "http://www.sciencedirect.com/science/article/pii/S1571066107005294", 494 author = "E. Albert and P. Arenas and S. Genaim and G. Puebla and D. Zanardini", 495 keywords = "Cost analysis", 496 keywords = "Java bytecode", 497 keywords = "cost relations", 498 keywords = "recurrence equations", 499 keywords = "complexity" 500 } 380 501 381 502 @article{Wang:2014:CVM:2714064.2660201, … … 598 719 doi = {10.1007/9783642005909_14} 599 720 } 721 722 @Inbook{Chalin2006, 723 author="Chalin, Patrice 724 and Kiniry, Joseph R. 725 and Leavens, Gary T. 726 and Poll, Erik", 727 editor="de Boer, Frank S. 728 and Bonsangue, Marcello M. 729 and Graf, Susanne 730 and de Roever, WillemPaul", 731 title="Beyond Assertions: Advanced Specification and Verification with JML and ESC/Java2", 732 bookTitle="Formal Methods for Components and Objects: 4th International Symposium, FMCO 2005, Amsterdam, The Netherlands, November 14, 2005, Revised Lectures", 733 year="2006", 734 publisher="Springer Berlin Heidelberg", 735 address="Berlin, Heidelberg", 736 pages="342363", 737 isbn="9783540367505", 738 doi="10.1007/11804192_16", 739 url="http://dx.doi.org/10.1007/11804192_16" 740 } 741 742 743 @book{KeYBook2016, 744 title = {Deductive Software Verification  The KeY Book  From Theory to Practice}, 745 editor = {Wolfgang Ahrendt and Bernhard Beckert and Richard Bubel and Reiner H{\"{a}}hnle and Peter H. Schmitt and Mattias Ulbrich}, 746 url = {http://dx.doi.org/10.1007/9783319498126}, 747 doi = {10.1007/9783319498126}, 748 isbn = {9783319498119}, 749 year = {2016}, 750 date = {20161216}, 751 volume = {10001}, 752 publisher = {Springer}, 753 series = {Lecture Notes in Computer Science}, 754 keywords = {}, 755 pubstate = {published}, 756 tppubtype = {book} 757 } 758 759 760 761 @Inbook{Montenegro2010a, 762 author="Montenegro, Manuel 763 and Pe{\~{n}}a, Ricardo 764 and Segura, Clara", 765 editor="van Eekelen, Marko 766 and Shkaravska, Olha", 767 title="A Space Consumption Analysis by Abstract Interpretation", 768 bookTitle="Foundational and Practical Aspects of Resource Analysis: First International Workshop, FOPARA 2009, Eindhoven, The Netherlands, November 6, 2009, Revised Selected Papers", 769 year="2010", 770 publisher="Springer Berlin Heidelberg", 771 address="Berlin, Heidelberg", 772 pages="3450", 773 isbn="9783642153310", 774 doi="10.1007/9783642153310_3", 775 url="http://dx.doi.org/10.1007/9783642153310_3" 776 } 777 778 779 @Inbook{Montenegro2010, 780 author="Montenegro, Manuel 781 and Pe{\~{n}}a, Ricardo 782 and Segura, Clara", 783 editor="Escobar, Santiago", 784 title="A Simple Region Inference Algorithm for a FirstOrder Functional Language", 785 bookTitle="Functional and Constraint Logic Programming: 18th International Workshop, WFLP 2009, Brasilia, Brazil, June 28, 2009, Revised Selected Papers", 786 year="2010", 787 publisher="Springer Berlin Heidelberg", 788 address="Berlin, Heidelberg", 789 pages="145161", 790 isbn="9783642119996", 791 doi="10.1007/9783642119996_10", 792 url="http://dx.doi.org/10.1007/9783642119996_10" 793 } 794 795 796 @Inbook{deDios2011, 797 author="de Dios, Javier 798 and Pe{\~{n}}a, Ricardo", 799 editor="Butler, Michael 800 and Schulte, Wolfram", 801 title="Certification of Safe Polynomial Memory Bounds", 802 bookTitle="FM 2011: Formal Methods: 17th International Symposium on Formal Methods, Limerick, Ireland, June 2024, 2011. Proceedings", 803 year="2011", 804 publisher="Springer Berlin Heidelberg", 805 address="Berlin, Heidelberg", 806 pages="184199", 807 isbn="9783642214370", 808 doi="10.1007/9783642214370_16", 809 url="http://dx.doi.org/10.1007/9783642214370_16" 810 } 811 812 813 @Inbook{Albert2012, 814 author="Albert, Elvira 815 and Bubel, Richard 816 and Genaim, Samir 817 and H{\"a}hnle, Reiner 818 and Rom{\'a}nD{\'i}ez, Guillermo", 819 editor="de Lara, Juan 820 and Zisman, Andrea", 821 title="Verified Resource Guarantees for Heap Manipulating Programs", 822 bookTitle="Fundamental Approaches to Software Engineering: 15th International Conference, FASE 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24  April 1, 2012. Proceedings", 823 year="2012", 824 publisher="Springer Berlin Heidelberg", 825 address="Berlin, Heidelberg", 826 pages="130145", 827 isbn="9783642288722", 828 doi="10.1007/9783642288722_10", 829 url="http://dx.doi.org/10.1007/9783642288722_10" 830 } 831 832 833 @Inbook{Nipkow2015, 834 author="Nipkow, Tobias", 835 editor="Urban, Christian 836 and Zhang, Xingyuan", 837 title="Amortized Complexity Verified", 838 bookTitle="Interactive Theorem Proving: 6th International Conference, ITP 2015, Nanjing, China, August 2427, 2015, Proceedings", 839 year="2015", 840 publisher="Springer International Publishing", 841 address="Cham", 842 pages="310324", 843 isbn="9783319221021", 844 doi="10.1007/9783319221021_21", 845 url="http://dx.doi.org/10.1007/9783319221021_21" 846 } 847 848 849 @article{Hoffmann:2012:MAR:2362389.2362393, 850 author = {Hoffmann, Jan and Aehlig, Klaus and Hofmann, Martin}, 851 title = {Multivariate Amortized Resource Analysis}, 852 journal = {ACM Trans. Program. Lang. Syst.}, 853 issue_date = {October 2012}, 854 volume = {34}, 855 number = {3}, 856 month = nov, 857 year = {2012}, 858 issn = {01640925}, 859 pages = {14:114:62}, 860 articleno = {14}, 861 numpages = {62}, 862 url = {http://doi.acm.org/10.1145/2362389.2362393}, 863 doi = {10.1145/2362389.2362393}, 864 acmid = {2362393}, 865 publisher = {ACM}, 866 address = {New York, NY, USA}, 867 keywords = {Amortized analysis, functional programming, quantitative analysis, resource consumption, static analysis}, 868 } 869 870 871 872 @Inbook{Chargueraud2015, 873 author="Chargu{\'e}raud, Arthur 874 and Pottier, Fran{\c{c}}ois", 875 editor="Urban, Christian 876 and Zhang, Xingyuan", 877 title="MachineChecked Verification of the Correctness and Amortized Complexity of an Efficient UnionFind Implementation", 878 bookTitle="Interactive Theorem Proving: 6th International Conference, ITP 2015, Nanjing, China, August 2427, 2015, Proceedings", 879 year="2015", 880 publisher="Springer International Publishing", 881 address="Cham", 882 pages="137153", 883 isbn="9783319221021", 884 doi="10.1007/9783319221021_9", 885 url="http://dx.doi.org/10.1007/9783319221021_9" 886 } 887 888 889 @Inbook{Teller2002, 890 author="Teller, David 891 and Zimmer, Pascal 892 and Hirschkoff, Daniel", 893 editor="Brim, Lubo{\v{s}} 894 and K{\v{r}}et{\'i}nsk{\'y}, Mojm{\'i}r 895 and Ku{\v{c}}era, Anton{\'i}n 896 and Jan{\v{c}}ar, Petr", 897 title="Using Ambients to Control Resources* ", 898 bookTitle="CONCUR 2002  Concurrency Theory: 13th International Conference Brno, Czech Republic, August 2023, 2002 Proceedings", 899 year="2002", 900 publisher="Springer Berlin Heidelberg", 901 address="Berlin, Heidelberg", 902 pages="288303", 903 isbn="9783540456940", 904 doi="10.1007/3540456945_20", 905 url="http://dx.doi.org/10.1007/3540456945_20" 906 } 907 908 909 @article{DBLP:journals/jfp/0002S15, 910 author = {Jan Hoffmann and 911 Zhong Shao}, 912 title = {Typebased amortized resource analysis with integers and arrays}, 913 journal = {J. Funct. Program.}, 914 volume = {25}, 915 year = {2015}, 916 url = {http://dx.doi.org/10.1017/S0956796815000192}, 917 doi = {10.1017/S0956796815000192}, 918 timestamp = {Tue, 26 Jan 2016 16:08:20 +0100}, 919 biburl = {http://dblp.unitrier.de/rec/bib/journals/jfp/0002S15}, 920 bibsource = {dblp computer science bibliography, http://dblp.org} 921 } 922 923 @Inbook{Barbanera2003, 924 author="Barbanera, Franco 925 and Bugliesi, Michele 926 and DezaniCiancaglini, Mariangiola 927 and Sassone, Vladimiro", 928 editor="Saraswat, Vijay A.", 929 title="A Calculus of Bounded Capacities", 930 bookTitle="Advances in Computing Science  ASIAN 2003. Progamming Languages and Distributed Computation Programming Languages and Distributed Computation: 8th Asian Computing Science Conference, Mumbai, India, December 1012, 2003. Proceedings", 931 year="2003", 932 publisher="Springer Berlin Heidelberg", 933 address="Berlin, Heidelberg", 934 pages="205223", 935 isbn="9783540409656", 936 doi="10.1007/9783540409656_14", 937 url="http://dx.doi.org/10.1007/9783540409656_14" 938 } 939 940 @article{Danielsson:2008:LST:1328897.1328457, 941 author = {Danielsson, Nils Anders}, 942 title = {Lightweight Semiformal Time Complexity Analysis for Purely Functional Data Structures}, 943 journal = {SIGPLAN Not.}, 944 issue_date = {January 2008}, 945 volume = {43}, 946 number = {1}, 947 month = jan, 948 year = {2008}, 949 issn = {03621340}, 950 pages = {133144}, 951 numpages = {12}, 952 url = {http://doi.acm.org/10.1145/1328897.1328457}, 953 doi = {10.1145/1328897.1328457}, 954 acmid = {1328457}, 955 publisher = {ACM}, 956 address = {New York, NY, USA}, 957 keywords = {amortised time complexity, dependent types, lazy evaluation, purely functional data structures}, 958 } 959 960 961 @inproceedings{Crary:2000:RBC:325694.325716, 962 author = {Crary, Karl and Weirich, Stephnie}, 963 title = {Resource Bound Certification}, 964 booktitle = {Proceedings of the 27th ACM SIGPLANSIGACT Symposium on Principles of Programming Languages}, 965 series = {POPL '00}, 966 year = {2000}, 967 isbn = {1581131259}, 968 location = {Boston, MA, USA}, 969 pages = {184198}, 970 numpages = {15}, 971 url = {http://doi.acm.org/10.1145/325694.325716}, 972 doi = {10.1145/325694.325716}, 973 acmid = {325716}, 974 publisher = {ACM}, 975 address = {New York, NY, USA}, 976 } 977 978 @Inbook{McCarthy2016, 979 author="McCarthy, Jay 980 and Fetscher, Burke 981 and New, Max 982 and Feltey, Daniel 983 and Findler, Robert Bruce", 984 editor="Kiselyov, Oleg 985 and King, Andy", 986 title="A Coq Library for Internal Verification of RunningTimes", 987 bookTitle="Functional and Logic Programming: 13th International Symposium, FLOPS 2016, Kochi, Japan, March 46, 2016, Proceedings", 988 year="2016", 989 publisher="Springer International Publishing", 990 address="Cham", 991 pages="144162", 992 isbn="9783319296043", 993 doi="10.1007/9783319296043_10", 994 url="http://dx.doi.org/10.1007/9783319296043_10" 995 } 996 997 @inproceedings { channgoverifying2017, 998 title = {Verifying and Synthesizing ConstantResource Implementations with Types}, 999 author = {Van Chan Ngo and Mario DehesaAzuara and Matthew Fredrikson and Jan Hoffmann}, 1000 booktitle = {Proceedings of the {IEEE} Symposium on Security and Privacy}, 1001 year = {2017}, 1002 note = {to appear} 1003 } 1004 1005 @Inbook{Brady2006, 1006 author="Brady, Edwin 1007 and Hammond, Kevin", 1008 editor="Butterfield, Andrew 1009 and Grelck, Clemens 1010 and Huch, Frank", 1011 title="A Dependently Typed Framework for Static Analysis of Program Execution Costs", 1012 bookTitle="Implementation and Application of Functional Languages: 17th International Workshop, IFL 2005, Dublin, Ireland, September 1921, 2005, Revised Selected Papers", 1013 year="2006", 1014 publisher="Springer Berlin Heidelberg", 1015 address="Berlin, Heidelberg", 1016 pages="7490", 1017 isbn="9783540691754", 1018 doi="10.1007/11964681_5", 1019 url="http://dx.doi.org/10.1007/11964681_5" 1020 } 1021 1022 1023 @inproceedings{Danner:2013:SCA:2428116.2428123, 1024 author = {Danner, Norman and Paykin, Jennifer and Royer, James S.}, 1025 title = {A Static Cost Analysis for a Higherorder Language}, 1026 booktitle = {Proceedings of the 7th Workshop on Programming Languages Meets Program Verification}, 1027 series = {PLPV '13}, 1028 year = {2013}, 1029 isbn = {9781450318600}, 1030 location = {Rome, Italy}, 1031 pages = {2534}, 1032 numpages = {10}, 1033 url = {http://doi.acm.org/10.1145/2428116.2428123}, 1034 doi = {10.1145/2428116.2428123}, 1035 acmid = {2428123}, 1036 publisher = {ACM}, 1037 address = {New York, NY, USA}, 1038 keywords = {automated theorem proving, certified bounds, higherorder complexity}, 1039 } 1040 1041 1042 @inproceedings{Reynolds:2002:SLL:645683.664578, 1043 author = {Reynolds, John C.}, 1044 title = {Separation Logic: A Logic for Shared Mutable Data Structures}, 1045 booktitle = {Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science}, 1046 series = {LICS '02}, 1047 year = {2002}, 1048 isbn = {0769514839}, 1049 pages = {5574}, 1050 numpages = {20}, 1051 url = {http://dl.acm.org/citation.cfm?id=645683.664578}, 1052 acmid = {664578}, 1053 publisher = {IEEE Computer Society}, 1054 address = {Washington, DC, USA}, 1055 } 600 1056 601 1057 @article{ASPINALL2007411, 
Papers/jarcerco2017/conclusions.tex
r3650 r3651 70 70 Abstract Interpretation may also be used to derive upper bounds for stack usage (e.g.~\cite{Regehr:2005:ESO:1113830.1113833}), and Abstract Interpretation tools for predicting stack space usage, for example the StackAnalyzer tool~\cite{stackanalyzer}, are also commercially available. 71 71 72 \paragraph{ Type and program logicbased analyses}72 \paragraph{Highlevel approaches} 73 73 74 Resource Aware ML (RAML) is a firstorder statically typed functional programming language~\cite{Hoffmann11,HAH12Toplas,HoffHof10}. 75 The RAML type system is able to derive polynomial resource bounds from firstorder functional programs, using a variant of the `potential method'. 76 This approach was first pioneered by Hoffman and Jost for amortized, linear bounds on resource consumption~\cite{DBLP:conf/esop/HofmannJ06}, who focussed on predicting heapspace usage. 77 Campbell also used a variant of this approach to predict stack space usage~\cite{bacthesis08,bacgiveback08,bacesop09}. 78 79 Implicit Computational Complexity represents another related approach to bounding resource usage via types~\cite{DalLago2012}. 80 Here, a fragment of Linear Logic, or some other substructural logic, is taken as the typelanguage of a programming language, with a provable guarantee that typeable terms normalise to a value in some bounded (e.g. polynomial in the size of the term) number of reduction steps. 81 Note that complained to the concrete complexity measures dealt with in this work, bounding reduction steps is rather coarsegrained: one reduction step in the calculus may decompose into some nonconstant number of primitive machine operations, when executed on physical hardware. 82 Indeed, the focus of Implicit Computational Complexity is not to capture \emph{concrete} resource usage of programs, but to provide a typetheoretic interpretation of complexity classes. 83 84 Several program logics for reasoning about a program's resource consumption have been investigated in the literature. 85 86 Aspinall et al. developed a program logic for a subset of the Java Virtual Machine's instruction set, capable of establishing resource bounds on JVM programs~\cite{ASPINALL2007411}. 87 The soundness of the logic was formally verified in Isabelle/HOL. 88 Along similar lines, Carbonneaux et al. developed a `quantitative Hoare logic' for reasoning about stack space usage of CompCert C programs~\cite{DBLP:conf/pldi/Carbonneaux0RS14}. 89 The soundness of the logic was also formally verified, using the Coq proof assistant. 90 This work will be further discussed below. 91 92 \subsubsection{Highlevel approaches} 93 94 \paragraph{Compilerbased costmodel lifting} 95 Perhaps the most similar piece of work to our own is the recent work by Carbonneaux \emph{et al}~\cite{DBLP:conf/pldi/Carbonneaux0RS14}, who extended the CompCert verified C compiler in order to lift a concrete cost model for stack space usage back to the C sourcelevel. 74 Perhaps the most closely related piece of work to our own is the recent work by Carbonneaux \emph{et al}~\cite{DBLP:conf/pldi/Carbonneaux0RS14}, who extended the CompCert verified C compiler in order to lift a concrete cost model for stack space usage back to the C sourcelevel. 96 75 Like CerCo, this work was verified within a theorem proverin this case Coq, rather than Matita. 97 76 Though Carbonneaux \emph{et al} were working entirely independently of the project described herein\footnote{Personal communication with Carbonneaux and Hoffmann}, the two pieces of work share some remarkable similarities, with both projects developing an analogue of the `structured trace' data structure described earlier in this paper in order to facilitate the verification of the lifting. … … 101 80 Carbonneaux \emph{at al} lift their model from the assembly generated by the CompCert compiler; we must go further, to the level of machine code, in order to lift our timing cost model, necessitating the development of a verified assembler. 102 81 Nevertheless, despite these differences, the two projects are clearly closely related. 82 83 Another closely related piece of work to our own is COSTA~\cite{Albert2012}, a heap resource bound static analysis system for the Java programming language, building on previous work investigating cost models for Java bytecode programs~\cite{ALBERT200767}. 84 COSTA is able to produce parametric heap resource bounds for a given Java program, which are made manifest as Java Modelling Language (JML)~\cite{Chalin2006} assertions, inserted into the Java source file. 85 Coupled with the KeY symbolic reasoning/automated reasoning system~\cite{KeYBook2016}, these assertions may be automatically verified, obtaining trustworthy upper bounds on a Java program's dynamic heap space usage at runtime. 86 87 Other work has explored the use of Computer Algebra Software, such as the Mathematica system, for deriving closedform upperbounds of a program's resource usage~\cite{Albert2011}. 88 89 Previous works have researched various static analyses of time and spaceusage of programs written in a simple functional programming language with regions, called Safe~\cite{Montenegro2010,Montenegro2010a}. 90 One such analysis was verified in Isabelle/HOL~\cite{deDios2011}. 91 92 The use of types to bound, or program logics to reason about, a program's resource usage have also been extensively investigated in previous work. 93 94 Resource Aware ML (RAML) is a firstorder statically typed functional programming language~\cite{Hoffmann11,HAH12Toplas,HoffHof10,HAH12,DBLP:journals/jfp/0002S15}. 95 The RAML type system is able to derive polynomial resource bounds from firstorder functional programs, using a variant of the `potential method'. 96 This approach was first pioneered by Hoffman and Jost for amortized, linear bounds on resource consumption~\cite{DBLP:conf/esop/HofmannJ06}, who focussed on predicting heapspace usage. 97 Campbell also used a variant of this approach to predict stack space usage~\cite{bacthesis08,bacgiveback08,bacesop09}, whilst Atkey extended the approach to imperative languages~\cite{Atkey2010}, using ideas from Separation Logic~\cite{Reynolds:2002:SLL:645683.664578}. 98 Recent work has extended this approach to include more features of the core programming language~\cite{Hoffmann2015}, improving the resource analysis~\cite{Hoffmann:2012:MAR:2362389.2362393}, and to apply extensions of the technique to case studies, demonstrating that cryptographic code is free from sidechannel attacks~\cite{channgoverifying2017}. 99 100 In related work, Salvucci and Chailloux~\cite{Salvucci201627} used a static type and effect system to bound runtime heap usage of an impure functional programming language, similar to ML. 101 Domainspecific type systems and calculi of mobile processes, for bounding agents in a distributed setting, have also been investigated~\cite{Barbanera2003,Teller2002}. 102 Brady and Hammond also investigated a dependent type system extended with features for bounding a program's dynamic resource usage~\cite{Brady2006}. 103 Similar ideas had previously been investigated by Crary and Weirich~\cite{Crary:2000:RBC:325694.325716}. 104 Libraries within dependentlytyped languages, such as Coq~\cite{McCarthy2016} and Agda~\cite{Danielsson:2008:LST:1328897.1328457}, have also been written for reasoning about the complexity of algorithms written in the language. 105 Oneoff machinechecked verifications of the algorithmic complexity of various data structure implementations, and operations over them, have also been investigated (e.g.~\cite{Chargueraud2015,Nipkow2015}). 106 107 Implicit Computational Complexity represents another related approach to bounding resource usage via types~\cite{DalLago2012}. 108 Here, a fragment of Linear Logic, or some other substructural logic, is taken as the language of types of some calculus, with a provable guarantee that typeable terms of the calculus normalise to a value in some bounded (e.g. polynomial in the size of the term) number of reduction steps. 109 Note that compared to the concrete complexity measures dealt with in this work, bounding reduction steps is rather coarsegrained: one reduction step in the calculus may decompose into some nonconstant number of primitive machine operations, when executed on physical hardware. 110 Indeed, the focus of Implicit Computational Complexity is not to capture \emph{concrete} resource usage of programs, but to provide a typetheoretic interpretation of complexity classes. 111 A formalisation of a cost semantics for System T using ideas from Implicit Computational Complexity was formalised in Coq~\cite{Danner:2013:SCA:2428116.2428123}. 112 113 Several program logics for reasoning about a program's resource consumption have been investigated in the literature. 114 115 Aspinall et al. developed a program logic for a subset of the Java Virtual Machine's instruction set, capable of establishing resource bounds on JVM programs~\cite{ASPINALL2007411}, similar in spirit to the `quantitative Hoare logic' mentioned above. 116 The soundness of the logic was formally verified in Isabelle/HOL. 117 Another program logic for reasoning about Java resource usage, based on ideas taken from Separation Logic, was also developed by Aspinall et al.~\cite{Aspinall2010}. 103 118 104 119 \paragraph{Verified compilation}
Note: See TracChangeset
for help on using the changeset viewer.