@article{DBLP:tr/trier/MI96-11, author = {Christian Fecht and Helmut Seidl}, title = {An Even Faster Solver for General Systems of Equations}, journal = {Universit{\"a}t Trier, Mathematik/Informatik, Forschungsbericht}, volume = {96-11}, year = {1996}, bibsource = {DBLP, http://dblp.uni-trier.de} } @inproceedings{CousotCousot77-1, author = {Cousot, P{.} and Cousot, R{.}}, title = {Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints}, pages = {238--252}, booktitle = {Conference Record of the Fourth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages}, address = {Los Angeles, California}, publisher = {ACM Press, New York, NY}, year = 1977, } @article{mine:hosc06, author = {Min\'e, A{.}}, title = {The Octagon Abstract Domain}, journal = {Higher-Order and Symbolic Computation}, editor = {O. Danvy}, publisher = {Springer}, year = {2006}, volume = {19}, number = {1}, pages = {31--100}, note = {\url{http://www.di.ens.fr/~mine/publi/article-mine-HOSC06.pdf}} } @inproceedings{mine:padoII, author = {Min\'e, A{.}}, title = {A New Numerical Abstract Domain Based on Difference-Bound Matrices}, booktitle = {Proc. of the 2d Symp. on Programs as Data Objects (PADO II)}, series = {Lecture Notes in Computer Science}, year = {2001}, month = {May}, pages = {155--172}, volume = {2053}, publisher = {Springer}, location = {Aarhus, Danemark}, note = {\url{http://www.di.ens.fr/~mine/publi/article-mine-padoII.pdf}} } @inproceedings{DBLP:conf/vmcai/SankaranarayananSM05, author = {Sriram Sankaranarayanan and Henny B. Sipma and Zohar Manna}, title = {Scalable Analysis of Linear Systems Using Mathematical Programming}, booktitle = {VMCAI}, year = {2005}, pages = {25-41}, ee = {http://dx.doi.org/10.1007/978-3-540-30579-8_2}, bibsource = {DBLP, http://dblp.uni-trier.de} } @inproceedings{Dor:2001:CCS:647170.718291, author = {Dor, Nurit and Rodeh, Michael and Sagiv, Shmuel}, title = {Cleanness Checking of String Manipulations in C Programs via Integer Analysis}, booktitle = {Proceedings of the 8th International Symposium on Static Analysis}, series = {SAS '01}, year = {2001}, isbn = {3-540-42314-1}, pages = {194--212}, numpages = {19}, url = {http://dl.acm.org/citation.cfm?id=647170.718291}, acmid = {718291}, publisher = {Springer-Verlag}, address = {London, UK, UK}, } @INPROCEEDINGS{Yovine98modelchecking, author = {Sergio Yovine}, title = {Model checking timed automata}, booktitle = {In European Educational Forum: School on Embedded Systems}, year = {1998}, pages = {114--152}, publisher = {Springer-Verlag} } @inproceedings{EasyChair:117, author = {Thomas Martin Gawlitza and Helmut Seidl}, title = {Abstract Interpretation over Zones without Widening}, booktitle = {WING 2010}, editor = {Andrei Voronkov and Laura Kovacs and Nikolaj Bjorner}, series = {EPiC Series}, volume = {1}, pages = {12-43}, year = {2012}, publisher = {EasyChair}, bibsource = {EasyChair, http://www.easychair.org}, issn = {2040-557X}, } @inproceedings{Gawlitza:2007:PFC:1762174.1762203, author = {Gawlitza, Thomas and Seidl, Helmut}, title = {Precise fixpoint computation through strategy iteration}, booktitle = {Proceedings of the 16th European conference on Programming}, series = {ESOP'07}, year = {2007}, isbn = {978-3-540-71314-2}, location = {Braga, Portugal}, pages = {300--315}, numpages = {16}, url = {http://dl.acm.org/citation.cfm?id=1762174.1762203}, acmid = {1762203}, publisher = {Springer-Verlag}, address = {Berlin, Heidelberg}, } @article{tarski, author = {Tarski, Alfred}, title = {A lattice-theoretical fixpoint theorem and its applications.}, year = {1955} } @incollection {springerlink, author = {Christensen, Aske and Mø, Anders and Schwartzbach, Michael}, affiliation = {BRICS Denmark}, title = {Precise Analysis of String Expressions}, booktitle = {Static Analysis}, series = {Lecture Notes in Computer Science}, editor = {Cousot, Radhia}, publisher = {Springer Berlin / Heidelberg}, isbn = {978-3-540-40325-8}, keyword = {Computer Science}, pages = {1076-1076}, volume = {2694}, year = {2003} } % http://www.mrtc.mdh.se/projects/wcet/benchmarks.html @InProceedings{Gustafsson:WCET2010:Benchmarks, author = {Jan Gustafsson and Adam Betts and Andreas Ermedahl and Bj{\"{o}}rn Lisper}, title = {The {M{\"a}lardalen} {WCET} Benchmarks -- Past, Present and Future}, booktitle = WCET2010, OPTcrossref = {}, OPTkey = {}, pages = {137--147}, year = {2010}, editor = {Bj{\"o}rn Lisper}, OPTvolume = {}, OPTnumber = {}, OPTseries = {}, address = {Brussels, Belgium}, month = jul, OPTorganization = {}, publisher = {OCG}, OPTnote = {}, OPTannote = {} } @misc{fixpoint-slides, author = {Helmut Seidl}, title = {Lecture Slides in Program Optimisation}, url = {http://www2.in.tum.de/~seidl/Courses/WS2011/Optimierung/all2011.pdf}, urldate = {2012-11-04}, year = {2011} } @article{Rice, author = {H. Rice}, title = {Classes of Recursively Enumerable Sets and their Decision problems}, year = {1953}, journal = {Transactions of the American Mathematical Society}, volume = {83} } @TECHREPORT{SCOTT70B, AUTHOR = {Scott, Dana S.}, TITLE = {Outline of a Mathematical Theory of Computation}, TYPE = {Technical Monograph}, NUMBER = {PRG--2}, INSTITUTION = {Oxford University Computing Laboratory}, DEPARTMENT = {Programming Research Group}, ADDRESS = {Oxford, England}, MONTH = {November}, YEAR = {1970} } @book{debugging-book, author = {Zeller, Andreas}, title = {Why Programs Fail: A Guide to Systematic Debugging}, year = {2005}, isbn = {1558608664}, publisher = {Morgan Kaufmann Publishers Inc.}, address = {San Francisco, CA, USA}, page = {21}, } @ARTICLE{Hailpern01softwaredebugging, author = {Brent Hailpern and Padmanabhan Santhanam}, title = {Software Debugging, Testing, and Verification}, journal = {IBM SYSTEMS JOURNAL}, year = {2001}, volume = {41}, pages = {4--12} } @article{Halting, added-at = {2011-12-06T14:58:09.000+0100}, author = {Turing, Alan M.}, biburl = {http://www.bibsonomy.org/bibtex/297ba9ab572e2017ce1dd25da3af837af/msteele}, interhash = {8ac1f5e961ff74849ab6f0c7348b9c9c}, intrahash = {97ba9ab572e2017ce1dd25da3af837af}, journal = {Proceedings of the London Mathematical Society}, keywords = {calculus}, pages = {230--265}, series = 2, timestamp = {2011-12-06T14:58:09.000+0100}, title = {On Computable Numbers, with an application to the Entscheidungsproblem}, volume = 42, year = 1936 } @article{Knaster-Tarski, author = {Tarski, Alfred}, journal = {Pacific Journal of Mathematics}, number = {2}, pages = {285-309}, title = {A Lattice-Theoretical Fixpoint Theorem and its Applications}, volume = {5}, year = {1955}, } @TECHREPORT{TD-fixpoint, author = {Baudouin Le Charlier and Pascal Van Hentenryck}, title = {A Universal Top-Down Fixpoint Algorithm}, institution = {}, year = {1992} } @INPROCEEDINGS{Jorgensen94findingfixpoints, author = {Niels Jørgensen}, title = {Finding Fixpoints in Finite Function Spaces Using Neededness Analysis and Chaotic Iteration}, booktitle = {In SAS'94}, year = {1994}, pages = {329--345}, publisher = {Springer, LNCS} } @inproceedings{Kildall:1973:UAG:512927.512945, author = {Kildall, Gary A.}, title = {A unified approach to global program optimization}, booktitle = {Proceedings of the 1st annual ACM SIGACT-SIGPLAN symposium on Principles of programming languages}, series = {POPL '73}, year = {1973}, location = {Boston, Massachusetts}, pages = {194--206}, numpages = {13}, url = {http://doi.acm.org/10.1145/512927.512945}, doi = {10.1145/512927.512945}, acmid = {512945}, publisher = {ACM}, address = {New York, NY, USA}, } @incollection{FP-efficient, year={1994}, isbn={978-3-540-58485-8}, booktitle={Static Analysis}, volume={864}, series={Lecture Notes in Computer Science}, editor={Charlier, Baudouin}, doi={10.1007/3-540-58485-4_49}, title={Efficient fixpoint computation}, url={http://dx.doi.org/10.1007/3-540-58485-4_49}, publisher={Springer Berlin Heidelberg}, author={Vergauwen, B. and Wauman, J. and Lewi, J.}, pages={314-328} } @misc{MCFClass, author={Centro di Ricerca e Formazione per l'Ottimizzazione su Reti}, title={The MCFClass Project}, year={2011}, url={http://www.di.unipi.it/optimize/Software/MCF.html} } @article {antlr, author = {Parr, T. J. and Quong, R. W.}, title = {ANTLR: A predicated-LL(k) parser generator}, journal = {Software: Practice and Experience}, volume = {25}, number = {7}, publisher = {John Wiley & Sons, Ltd.}, issn = {1097-024X}, url = {http://dx.doi.org/10.1002/spe.4380250705}, doi = {10.1002/spe.4380250705}, pages = {789--810}, keywords = {parsing, compiler, parser generator, predicates, LL(k) parser}, year = {1995}, } @MastersThesis{LLVM-paper, author = {Chris Lattner}, title = "{LLVM: An Infrastructure for Multi-Stage Optimization}", school = "{Computer Science Dept., University of Illinois at Urbana-Champaign}", year = {2002}, address = {Urbana, IL}, month = {Dec}, note = {{\em See {\tt http://llvm.cs.uiuc.edu}.}} } @misc{LLVM, title={The LLVM Compiler Infrastructure}, url={http://llvm.org/}, author={Chris Lattner} } @misc{Clang, title={clang: a C language family frontend for LLVM}, url={http://clang.llvm.org/} } @INPROCEEDINGS{yovine-zones, author = {Sergio Yovine}, title = {Model checking timed automata}, booktitle = {In European Educational Forum: School on Embedded Systems}, year = {1998}, pages = {114--152}, publisher = {Springer-Verlag} }