var bibbase_data = {"data":"<img src=\"//bibbase.org/img/ajax-loader.gif\" id=\"spinner\"\n  style=\"display: none;\" alt=\"Loading..\" />\n\n<div id=\"bibbase\">\n\n  <script type=\"text/javascript\">\n    var bibbase = {\n      params: {\"bib\":\"http://science.mq.edu.au/~fcassez/bib/franck-bib.bib\",\"jsonp\":\"1\",\"filter\":\"mywebpage:soft-verif\",\"css\":\"true\",\"host\":\"bibbase.org\"},\n      data: [{\"bibtype\":\"inproceedings\",\"type\":\"B - International Conferences\",\"author\":[{\"firstnames\":[\"Franck\"],\"propositions\":[],\"lastnames\":[\"Cassez\"],\"suffixes\":[]},{\"firstnames\":[\"Anthony M.\"],\"propositions\":[],\"lastnames\":[\"Sloane\"],\"suffixes\":[]}],\"title\":\"ScalaSMT: Satisfiability Modulo Theory in Scala (Tool Paper)\",\"booktitle\":\"SCALA'17, October 23–27, 2017, Vancouver, BC, Canada. Proceedings.\",\"pages\":\"\",\"year\":\"2017\",\"xxxurl\":\"http://dx.doi.org/10.1007/978-3-662-46681-0_39\",\"xxxdoi\":\"10.1007/978-3-662-46681-0_39\",\"publisher\":\"Association for Computing Machinery\",\"xvolume\":\"9035\",\"xxxseries\":\"LNCS\",\"mywebpage\":\"soft-verif\",\"keywords\":\"scala, SMT solvers\",\"category\":\"soft-verif\",\"show\":\"\",\"note\":\"forthcoming\",\"urlpaper\":\"papers/scala-17.pdf\",\"abstract\":\"A Satisfiability Modulo Theory (SMT) solver is a program that implements algorithms to automatically determine whether a logical formula is satisfiable. The performance of SMT solvers has dramatically increased in the last decade and for instance, many of the state-of-the-art software analysis tools heavily rely on SMT solving to analyse source code. We present ScalaSMT, a Scala library that leverages the power of SMT solvers and makes SMT solving directly usable in Scala. ScalaSMT provides seamless access to numerous popular SMT solvers like Z3, CVC4, Yices, MathSat or SMTInterpol. Our library comes with a domain-specific language to write terms and logical formulas for a wide range of logical theories, thereby isolating users from the details of particular solvers.\",\"bibtex\":\"@inproceedings{scala-17,\\nauthor    = {Franck Cassez\\nand {Anthony M.} Sloane},\\n  title     = {ScalaSMT: Satisfiability Modulo Theory in Scala (Tool Paper)},\\n  booktitle = {SCALA'17, October 23--27, 2017, Vancouver, BC, Canada. Proceedings.},\\n  pages     = {},\\n  year      = {2017},\\n  xxxurl       = {http://dx.doi.org/10.1007/978-3-662-46681-0_39},\\n  xxxdoi       = {10.1007/978-3-662-46681-0_39},\\n  publisher = acm,\\n  xvolume = 9035,\\n  xxxseries    = lncs,\\n  mywebpage = {soft-verif},\\n  keywords = {scala, SMT solvers},\\n  category = {soft-verif},\\n  show = {},\\n  note={forthcoming},\\n  urlpaper = {papers/scala-17.pdf},\\n  abstract = {A Satisfiability Modulo Theory (SMT) solver is a program that implements algorithms to automatically determine whether \\n  a logical formula is satisfiable. \\n  The performance of SMT solvers has dramatically increased in the last decade and for instance, \\n  many of the state-of-the-art software analysis tools heavily rely on SMT solving to analyse source code. \\n  We present ScalaSMT, a Scala library that leverages the power of SMT solvers and makes SMT solving directly usable in Scala. \\n  ScalaSMT provides seamless access to numerous popular SMT solvers like Z3, CVC4, Yices, MathSat or SMTInterpol. \\n  Our library comes with a domain-specific language to write terms and logical formulas for a wide range of logical theories, \\n  thereby isolating users from the details of particular solvers.},\\n    Type = {B - International Conferences},\\n    show = {},\\n}\\n\\n\",\"author_short\":[\"Cassez, F.\",\"Sloane, A.\"],\"key\":\"scala-17\",\"id\":\"scala-17\",\"bibbaseid\":\"cassez-sloane-scalasmtsatisfiabilitymodulotheoryinscalatoolpaper-2017\",\"role\":\"author\",\"urls\":{\"Paper\":\"http://science.mq.edu.au/~fcassez/bib/papers/scala-17.pdf\"},\"keyword\":[\"scala\",\"SMT solvers\"],\"metadata\":{\"authorlinks\":{\"cassez, f\":\"http://science.mq.edu.au/~fcassez/software-verif.html\"}},\"downloads\":3,\"html\":\"\"},{\"bibtype\":\"misc\",\"type\":\"misc\",\"title\":\"Analysis of program code\",\"author\":[{\"propositions\":[],\"lastnames\":[\"Cassez\"],\"firstnames\":[\"F.\"],\"suffixes\":[]},{\"propositions\":[],\"lastnames\":[\"Müller\"],\"firstnames\":[\"C.\"],\"suffixes\":[]}],\"url\":\"https://www.google.com/patents/US9760469\",\"year\":\"2017\",\"mywebpage\":\"soft-verif\",\"keywords\":\"software verification\",\"category\":\"soft-verif\",\"month\":\"September~12\",\"note\":\"US Patent 9,760,469\",\"bibtex\":\"@misc{cassez2017analysis,\\n  title={Analysis of program code},\\n  author={Cassez, F. and M{\\\\\\\"u}ller, C.},\\n  url={https://www.google.com/patents/US9760469},\\n  year={2017},\\n  mywebpage = {soft-verif},\\n  keywords = {software verification},\\n  category = {soft-verif},\\n  month=sep # \\\"~12\\\",\\n  note={US Patent 9,760,469}\\n}\\n\\n\",\"author_short\":[\"Cassez, F.\",\"Müller, C.\"],\"key\":\"cassez2017analysis\",\"id\":\"cassez2017analysis\",\"bibbaseid\":\"cassez-mller-analysisofprogramcode-2017\",\"role\":\"author\",\"urls\":{\"Paper\":\"https://www.google.com/patents/US9760469\"},\"keyword\":[\"software verification\"],\"metadata\":{\"authorlinks\":{\"cassez, f\":\"http://science.mq.edu.au/~fcassez/software-verif.html\"}},\"html\":\"\"},{\"bibtype\":\"inproceedings\",\"type\":\"A - International Conferences\",\"author\":[{\"firstnames\":[\"Franck\"],\"propositions\":[],\"lastnames\":[\"Cassez\"],\"suffixes\":[]},{\"firstnames\":[\"Anthony M.\"],\"propositions\":[],\"lastnames\":[\"Sloane\"],\"suffixes\":[]},{\"firstnames\":[\"Matthew\"],\"propositions\":[],\"lastnames\":[\"Roberts\"],\"suffixes\":[]},{\"firstnames\":[\"Matthew\"],\"propositions\":[],\"lastnames\":[\"Pigram\"],\"suffixes\":[]},{\"firstnames\":[\"Pongsak\"],\"propositions\":[],\"lastnames\":[\"Suvanpong\"],\"suffixes\":[]},{\"firstnames\":[\"Pablo\",\"González\"],\"propositions\":[\"de\"],\"lastnames\":[\"Aledo\",\"Marugán\"],\"suffixes\":[]}],\"title\":\"Skink: Static Analysis of Programs in LLVM Intermediate Representation (Competition contribution)\",\"booktitle\":\"Tools and Algorithms for the Construction and Analysis of Systems - 23rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017. Proceedings\",\"pages\":\"380–384\",\"year\":\"2017\",\"url\":\"https://doi.org/10.1007/978-3-662-54580-5_27\",\"doi\":\"10.1007/978-3-662-54580-5_27\",\"publisher\":\"Springer\",\"xvolume\":\"10206\",\"series\":\"LNCS\",\"mywebpage\":\"soft-verif\",\"keywords\":\"refinement, software verification\",\"category\":\"soft-verif\",\"show\":\"\",\"xxnote\":\"forthcoming\",\"urlpaper\":\"papers/sv-comp-2017.pdf\",\"abstract\":\"Skink is a static analysis tool that analyses the LLVM intermediate representation (LLVM-IR) of a program source code. The analysis consists of checking whether there is a feasible execution that can reach a designated error block in the LLVM-IR. The result of a program analysis is ``correct'' if the error block is not reachable, ``incorrect'' if the error block is reachable, or ``inconclusive'' if the status of the program could not be determined. In this paper, we introduce Skink V2.0 to analyse single and multi-threaded C programs.\",\"bibtex\":\"@inproceedings{tacas-17,\\nauthor    = {Franck Cassez\\nand {Anthony M.} Sloane\\nand Matthew Roberts\\nand Matthew Pigram\\nand Pongsak Suvanpong\\nand Pablo Gonz{\\\\'{a}}lez de Aledo Marug{\\\\'{a}}n},\\n  title     = {Skink: Static Analysis of Programs in LLVM Intermediate Representation (Competition contribution)},\\n  booktitle = {Tools and Algorithms for the Construction and Analysis of Systems\\n               - 23rd International Conference, {TACAS} 2017, Held as Part of the\\n               European Joint Conferences on Theory and Practice of Software, {ETAPS}\\n               2017, Uppsala, Sweden, April 22-29, 2017. Proceedings},\\n  \\n pages     = {380--384},\\n  year      = {2017},\\n  url       = {https://doi.org/10.1007/978-3-662-54580-5_27},\\n  doi       = {10.1007/978-3-662-54580-5_27},\\n  publisher = springv,\\n  xvolume = 10206,\\n  series    = lncs,\\n  mywebpage = {soft-verif},\\n  keywords = {refinement, software verification},\\n  category = {soft-verif},\\n  show = {},\\n  xxnote={forthcoming},\\n  urlpaper = {papers/sv-comp-2017.pdf},\\n  abstract = {Skink is a static analysis tool that analyses the LLVM intermediate representation (LLVM-IR)\\nof a program source code.\\nThe analysis consists of checking whether there is a feasible execution that can reach a\\n designated error block in the LLVM-IR.\\nThe result of a program analysis is ``correct'' if the error block is not reachable,\\n``incorrect'' if the error block is reachable, or ``inconclusive'' if the status of the program could not be determined.\\nIn this paper, we introduce Skink V2.0 to analyse single and multi-threaded C programs.},\\n    Type = {A - International Conferences},\\n}\\n\\n\\n\\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\\n%%% 2016\\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\\n\",\"author_short\":[\"Cassez, F.\",\"Sloane, A.\",\"Roberts, M.\",\"Pigram, M.\",\"Suvanpong, P.\",\"de Aledo Marugán, P. G.\"],\"key\":\"tacas-17\",\"id\":\"tacas-17\",\"bibbaseid\":\"cassez-sloane-roberts-pigram-suvanpong-dealedomarugn-skinkstaticanalysisofprogramsinllvmintermediaterepresentationcompetitioncontribution-2017\",\"role\":\"author\",\"urls\":{\"Paper\":\"http://science.mq.edu.au/~fcassez/bib/papers/sv-comp-2017.pdf\"},\"keyword\":[\"refinement\",\"software verification\"],\"metadata\":{\"authorlinks\":{\"cassez, f\":\"http://science.mq.edu.au/~fcassez/software-verif.html\"}},\"downloads\":2,\"html\":\"\"},{\"bibtype\":\"inproceedings\",\"type\":\"B - International Conferences\",\"author\":[{\"firstnames\":[\"Franck\"],\"propositions\":[],\"lastnames\":[\"Cassez\"],\"suffixes\":[]},{\"firstnames\":[\"Frowin\"],\"propositions\":[],\"lastnames\":[\"Ziegler\"],\"suffixes\":[]}],\"editor\":[{\"firstnames\":[\"Martin\"],\"propositions\":[],\"lastnames\":[\"Davis\"],\"suffixes\":[]},{\"firstnames\":[\"Ansgar\"],\"propositions\":[],\"lastnames\":[\"Fehnker\"],\"suffixes\":[]},{\"firstnames\":[\"Annabelle\"],\"propositions\":[],\"lastnames\":[\"McIver\"],\"suffixes\":[]},{\"firstnames\":[\"Andrei\"],\"propositions\":[],\"lastnames\":[\"Voronkov\"],\"suffixes\":[]}],\"title\":\"Verification of Concurrent Programs Using Trace Abstraction Refinement\",\"booktitle\":\"Logic for Programming, Artificial Intelligence, and Reasoning - 20th International Conference, LPAR-20 2015, Suva, Fiji, November 24-28, 2015, Proceedings\",\"pages\":\"233–248\",\"year\":\"2015\",\"series\":\"Lecture Notes in Computer Science\",\"volume\":\"9450\",\"publisher\":\"Springer\",\"url\":\"http://dx.doi.org/10.1007/978-3-662-48899-7_17\",\"mywebpage\":\"soft-verif\",\"category\":\"soft-verif\",\"isbn\":\"978-3-662-48898-0\",\"doi\":\"10.1007/978-3-662-48899-7_17\",\"show\":\"\",\"note\":\"LPAR Best paper award\",\"urlpaper\":\"papers/lpar-2015.pdf\",\"urlslides\":\"papers/slides-lpar-2015.pdf\",\"abstract\":\"Verifying concurrent programs is notoriously hard due to the state explosion problem: (1) the data state space can be very large as the variables can range over very large sets, and (2) the control state space is the Cartesian product of the control state space of the concurrent com- ponents and thus grows exponentially in the number of components. On the one hand, the most successful approaches to address the control state explosion problem are based on assume-guarantee reasoning or model-checking coupled with partial order reduction. On the other hand, the most successful techniques to address the data space explosion problem for sequential programs verification are based on the abstraction/refine- ment paradigm which consists in refining an abstract over-approximation of a program via predicate refinement. In this paper, we show that we can combine partial order reduction techniques with trace abstraction refinement. We apply our approach to standard benchmarks and show that it matches current state-of-the-art analysis techniques.\",\"bibtex\":\"@inproceedings{cassez-lpar-2015,\\n  author    = {Franck Cassez and\\n               Frowin Ziegler},\\n                editor    = {Martin Davis and\\n               Ansgar Fehnker and\\n               Annabelle McIver and\\n               Andrei Voronkov},\\n  title     = {Verification of Concurrent Programs Using Trace Abstraction Refinement},\\n  booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning - 20th\\n               International Conference, {LPAR-20} 2015, Suva, Fiji, November 24-28,\\n               2015, Proceedings},\\n  pages     = {233--248},\\n  year      = {2015},\\n  series    = {Lecture Notes in Computer Science},\\n  volume    = {9450},\\n  publisher = {Springer},\\n  year      = {2015},\\n  url       = {http://dx.doi.org/10.1007/978-3-662-48899-7_17},\\n  mywebpage = {soft-verif},\\n  category = {soft-verif},\\n  isbn      = {978-3-662-48898-0},\\n  doi       = {10.1007/978-3-662-48899-7_17},\\n  show = {},\\n  note = {LPAR Best paper award},\\n  urlpaper = {papers/lpar-2015.pdf},\\n    urlslides = {papers/slides-lpar-2015.pdf},\\n  abstract = {Verifying concurrent programs is notoriously hard due to the state explosion problem: (1) the data state space can be very large as the variables can range over very large sets, and (2) the control state space is the Cartesian product of the control state space of the concurrent com- ponents and thus grows exponentially in the number of components. On the one hand, the most successful approaches to address the control state explosion problem are based on assume-guarantee reasoning or model-checking coupled with partial order reduction. On the other hand, the most successful techniques to address the data space explosion problem for sequential programs verification are based on the abstraction/refine- ment paradigm which consists in refining an abstract over-approximation of a program via predicate refinement. In this paper, we show that we can combine partial order reduction techniques with trace abstraction refinement. We apply our approach to standard benchmarks and show that it matches current state-of-the-art analysis techniques.},\\n  Type = {B - International Conferences},\\n}\\n\\n\",\"author_short\":[\"Cassez, F.\",\"Ziegler, F.\"],\"editor_short\":[\"Davis, M.\",\"Fehnker, A.\",\"McIver, A.\",\"Voronkov, A.\"],\"key\":\"cassez-lpar-2015\",\"id\":\"cassez-lpar-2015\",\"bibbaseid\":\"cassez-ziegler-verificationofconcurrentprogramsusingtraceabstractionrefinement-2015\",\"role\":\"author\",\"urls\":{\"Paper\":\"http://science.mq.edu.au/~fcassez/bib/papers/lpar-2015.pdf\",\"Slides\":\"http://science.mq.edu.au/~fcassez/bib/papers/slides-lpar-2015.pdf\"},\"metadata\":{\"authorlinks\":{\"cassez, f\":\"http://science.mq.edu.au/~fcassez/software-verif.html\"}},\"downloads\":1,\"html\":\"\"},{\"bibtype\":\"inproceedings\",\"type\":\"B - International Conferences\",\"author\":[{\"firstnames\":[\"Franck\"],\"propositions\":[],\"lastnames\":[\"Cassez\"],\"suffixes\":[]},{\"firstnames\":[\"Takashi\"],\"propositions\":[],\"lastnames\":[\"Matsuoka\"],\"suffixes\":[]},{\"firstnames\":[\"Edward\"],\"propositions\":[],\"lastnames\":[\"Pierzchalski\"],\"suffixes\":[]},{\"firstnames\":[\"Nathan\"],\"propositions\":[],\"lastnames\":[\"Smyth\"],\"suffixes\":[]}],\"title\":\"Perentie: Modular Trace Refinement and Selective Value Tracking - (Competition Contribution)\",\"booktitle\":\"Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings\",\"pages\":\"439–442\",\"year\":\"2015\",\"url\":\"http://dx.doi.org/10.1007/978-3-662-46681-0_39\",\"doi\":\"10.1007/978-3-662-46681-0_39\",\"publisher\":\"Springer\",\"volume\":\"9035\",\"series\":\"LNCS\",\"mywebpage\":\"soft-verif\",\"keywords\":\"refinement, software verification\",\"category\":\"soft-verif\",\"show\":\"\",\"urlpaper\":\"papers/sv-comp-2015.pdf\",\"abstract\":\"Perentie is a software analysis tool based on iterative refinement of trace abstraction: if the refinement process terminates, the program is either declared correct or a counterexample is provided and the program is incorrect.\",\"bibtex\":\"@inproceedings{tacas-15,\\nauthor    = {Franck Cassez and\\n               Takashi Matsuoka and\\n               Edward Pierzchalski and\\n               Nathan Smyth},\\n  title     = {Perentie: Modular Trace Refinement and Selective Value Tracking -\\n               (Competition Contribution)},\\n  booktitle = {Tools and Algorithms for the Construction and Analysis of Systems\\n               - 21st International Conference, {TACAS} 2015, Held as Part of the\\n               European Joint Conferences on Theory and Practice of Software, {ETAPS}\\n               2015, London, UK, April 11-18, 2015. Proceedings},\\n  pages     = {439--442},\\n  year      = {2015},\\n  url       = {http://dx.doi.org/10.1007/978-3-662-46681-0_39},\\n  doi       = {10.1007/978-3-662-46681-0_39},\\n  publisher = springv,\\n  volume = 9035,\\n  series    = lncs,\\n  mywebpage = {soft-verif},\\n  keywords = {refinement, software verification},\\n  category = {soft-verif},\\n  show = {},\\n  urlpaper = {papers/sv-comp-2015.pdf},\\n  abstract = {Perentie is a software analysis tool based on iterative refinement of trace abstraction:\\n  if the refinement process terminates, the program is either declared correct or a counterexample is\\n  provided and the program is incorrect.},\\n    Type = {B - International Conferences},\\n\\n}\\n\\n\\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\\n%%% 2014\\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\\n\\n\",\"author_short\":[\"Cassez, F.\",\"Matsuoka, T.\",\"Pierzchalski, E.\",\"Smyth, N.\"],\"key\":\"tacas-15\",\"id\":\"tacas-15\",\"bibbaseid\":\"cassez-matsuoka-pierzchalski-smyth-perentiemodulartracerefinementandselectivevaluetrackingcompetitioncontribution-2015\",\"role\":\"author\",\"urls\":{\"Paper\":\"http://science.mq.edu.au/~fcassez/bib/papers/sv-comp-2015.pdf\"},\"keyword\":[\"refinement\",\"software verification\"],\"metadata\":{\"authorlinks\":{\"cassez, f\":\"http://science.mq.edu.au/~fcassez/software-verif.html\"}},\"html\":\"\"},{\"bibtype\":\"inproceedings\",\"type\":\"B - International Conferences\",\"author\":[{\"firstnames\":[\"Franck\"],\"propositions\":[],\"lastnames\":[\"Cassez\"],\"suffixes\":[]},{\"firstnames\":[\"Christian\"],\"propositions\":[],\"lastnames\":[\"Müller\"],\"suffixes\":[]},{\"firstnames\":[\"Karla\"],\"propositions\":[],\"lastnames\":[\"Burnett\"],\"suffixes\":[]}],\"title\":\"Summary-Based Inter-Procedural Analysis via Modular Trace Refinement\",\"booktitle\":\"34th International Conference on Foundation of Software Technology and Theoretical Computer Science, FSTTCS 2014, December 15-17, 2014, New Delhi, India\",\"pages\":\"545–556\",\"year\":\"2014\",\"mywebpage\":\"soft-verif\",\"category\":\"Software verification\",\"keywords\":\"trace refinement, software verification, Hoare logic\",\"url_link\":\"http://dx.doi.org/10.4230/LIPIcs.FSTTCS.2014.545\",\"doi\":\"10.4230/LIPIcs.FSTTCS.2014.545\",\"abstract\":\"We propose a generalisation of trace refinement for the verification of inter-procedural programs. Our method is a top-down modular, summary-based approach, and analyses inter-procedural programs by building function summaries on-demand and improving the summaries each time a function is analysed. Our method is sound, and complete relative to the existence of a modular Hoare proof for a non-recursive program. We have implemented a prototype analyser that demonstrates the main features of our approach and yields promising results. \",\"bibtex\":\"@inproceedings{fsttcs-14,\\n  author    = {Franck Cassez and\\n               Christian Müller and\\n               Karla Burnett},\\n  title     = {Summary-Based Inter-Procedural Analysis via Modular Trace Refinement},\\n  booktitle = {34th International Conference on Foundation of Software Technology\\n               and Theoretical Computer Science, {FSTTCS} 2014, December 15-17, 2014,\\n               New Delhi, India},\\n  pages     = {545--556},\\n  year      = {2014},\\n  mywebpage = {soft-verif},\\n  category = {Software verification},\\n  keywords = {trace refinement, software verification, Hoare logic},\\n  url_link       = {http://dx.doi.org/10.4230/LIPIcs.FSTTCS.2014.545},\\n  doi       = {10.4230/LIPIcs.FSTTCS.2014.545},\\n  abstract = {We propose a generalisation of trace refinement for the verification of inter-procedural programs.\\n  Our method is a top-down modular, summary-based approach, and analyses inter-procedural programs by building function summaries on-demand\\n  and improving the summaries each time a function is analysed. Our method is sound, and complete relative to the existence of a\\n  modular Hoare proof for a non-recursive program. We have implemented a prototype analyser that demonstrates the\\n  main features of our approach and yields promising results.\\n  },\\n  Type = {B - International Conferences},\\n}\\n\\n\\n\",\"author_short\":[\"Cassez, F.\",\"Müller, C.\",\"Burnett, K.\"],\"key\":\"fsttcs-14\",\"id\":\"fsttcs-14\",\"bibbaseid\":\"cassez-mller-burnett-summarybasedinterproceduralanalysisviamodulartracerefinement-2014\",\"role\":\"author\",\"urls\":{\" link\":\"http://dx.doi.org/10.4230/LIPIcs.FSTTCS.2014.545\"},\"keyword\":[\"trace refinement\",\"software verification\",\"Hoare logic\"],\"metadata\":{\"authorlinks\":{\"cassez, f\":\"http://science.mq.edu.au/~fcassez/software-verif.html\"}},\"html\":\"\"},{\"bibtype\":\"inproceedings\",\"type\":\"B - International Conferences\",\"author\":[{\"firstnames\":[\"Sebastian\"],\"propositions\":[],\"lastnames\":[\"Biallas\"],\"suffixes\":[]},{\"firstnames\":[\"Mads\",\"Chr.\"],\"propositions\":[],\"lastnames\":[\"Olesen\"],\"suffixes\":[]},{\"firstnames\":[\"Franck\"],\"propositions\":[],\"lastnames\":[\"Cassez\"],\"suffixes\":[]},{\"firstnames\":[\"Ralf\"],\"propositions\":[],\"lastnames\":[\"Huuck\"],\"suffixes\":[]}],\"title\":\"PtrTracker: Pragmatic pointer analysis\",\"booktitle\":\"13th IEEE International Working Conference on Source Code Analysis and Manipulation, SCAM 2013, Eindhoven, Netherlands, September 22-23, 2013\",\"pages\":\"69–73\",\"year\":\"2013\",\"publisher\":\"IEEE Computer Society\",\"urlpaper\":\"papers/scam-2013.pdf\",\"url_link\":\"http://dx.doi.org/10.1109/SCAM.2013.6648186\",\"doi\":\"10.1109/SCAM.2013.6648186\",\"keywords\":\"Software verification, pointers, static analysis\",\"mywebpage\":\"soft-verif\",\"category\":\"Software verification\",\"abstract\":\"Static program analysis for bug detection in industrial C/C++ code has many challenges. One of them is to analyze pointer and pointer structures efficiently. While there has been much research into various aspects of pointer analysis either for compiler optimization or for verification tasks, both classical categories are not optimized for bug detection, where speed and precision are important, but soundness (no missed bugs) and completeness (no false positives) do not necessarily need to be guaranteed. \",\"bibtex\":\"@inproceedings{scam-2013,\\n  author    = {Sebastian Biallas and\\n               Mads Chr. Olesen and\\n               Franck Cassez and\\n               Ralf Huuck},\\n  title     = {PtrTracker: Pragmatic pointer analysis},\\n  booktitle = {13th {IEEE} International Working Conference on Source Code Analysis\\n               and Manipulation, {SCAM} 2013, Eindhoven, Netherlands, September 22-23,\\n               2013},\\n  pages     = {69--73},\\n  year      = {2013},\\n  publisher = {{IEEE} Computer Society},\\n  urlpaper = {papers/scam-2013.pdf},\\n  url_link       = {http://dx.doi.org/10.1109/SCAM.2013.6648186},\\n  doi       = {10.1109/SCAM.2013.6648186},\\n  keywords = {Software verification, pointers, static analysis},\\n  mywebpage = {soft-verif},\\n  category = {Software verification},\\n  abstract = {\\n  Static program analysis for bug detection in industrial C/C++ code has many challenges. One of them is to analyze pointer and pointer structures efficiently. While there has been much research into various aspects of pointer analysis either for compiler optimization or for verification tasks, both classical categories are not optimized for bug detection, where speed and precision are important, but soundness (no missed bugs) and completeness (no false positives) do not necessarily need to be guaranteed.\\n  },\\n    Type = {B - International Conferences},\\n}\\n\\n\",\"author_short\":[\"Biallas, S.\",\"Olesen, M. C.\",\"Cassez, F.\",\"Huuck, R.\"],\"key\":\"scam-2013\",\"id\":\"scam-2013\",\"bibbaseid\":\"biallas-olesen-cassez-huuck-ptrtrackerpragmaticpointeranalysis-2013\",\"role\":\"author\",\"urls\":{\"Paper\":\"http://science.mq.edu.au/~fcassez/bib/papers/scam-2013.pdf\",\" link\":\"http://dx.doi.org/10.1109/SCAM.2013.6648186\"},\"keyword\":[\"Software verification\",\"pointers\",\"static analysis\"],\"metadata\":{\"authorlinks\":{\"cassez, f\":\"http://science.mq.edu.au/~fcassez/software-verif.html\"}},\"html\":\"\"},{\"bibtype\":\"inproceedings\",\"type\":\"B - International Conferences\",\"author\":[{\"firstnames\":[\"Franck\"],\"propositions\":[],\"lastnames\":[\"Cassez\"],\"suffixes\":[]},{\"firstnames\":[\"René\",\"Rydhof\"],\"propositions\":[],\"lastnames\":[\"Hansen\"],\"suffixes\":[]},{\"firstnames\":[\"Mads\",\"Chr.\"],\"propositions\":[],\"lastnames\":[\"Olesen\"],\"suffixes\":[]}],\"title\":\"What is a Timing Anomaly?\",\"booktitle\":\"12th International Workshop on Worst-Case Execution Time Analysis, WCET 2012, July 10, 2012, Pisa, Italy\",\"year\":\"2012\",\"pages\":\"1-12\",\"urlpaper\":\"papers/wcet-2012.pdf\",\"url_link\":\"http://dx.doi.org/10.4230/OASIcs.WCET.2012.1\",\"abstract\":\"Timing anomalies make worst-case execution time analysis much harder, because the analysis will have to consider all local choices. It has been widely recognised that certain hardware features are timing anomalous, while others are not. However, defining formally what a timing anomaly is, has been difficult. We examine previous definitions of timing anomalies, and identify examples where they do not align with common observations. We then provide a definition for consistently slower hardware traces that can be used to define timing anomalies and aligns with common observations.\",\"category\":\"wcet\",\"mywebpage\":\"soft-verif,wcet\",\"keywords\":\"wcet\",\"publisher\":\"Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik\",\"series\":\"OASICS\",\"volume\":\"23\",\"bibtex\":\"@inproceedings{wcet-12,\\n  author    = {Franck Cassez and\\n               René Rydhof Hansen and\\n               Mads Chr. Olesen},\\n  title     = {What is a Timing Anomaly?},\\n  booktitle = {12th International Workshop on Worst-Case Execution Time\\n               Analysis, WCET 2012, July 10, 2012, Pisa, Italy},\\n  year      = {2012},\\n  pages     = {1-12},\\n  urlpaper = {papers/wcet-2012.pdf},\\n  url_link        = {http://dx.doi.org/10.4230/OASIcs.WCET.2012.1},\\n  abstract = {Timing anomalies make worst-case execution time analysis much harder, because the analysis will have to consider all local choices. It has been widely recognised that certain hardware features are timing anomalous, while others are not. However, defining formally what a timing anomaly is, has been difficult. We examine previous definitions of timing anomalies, and identify examples where they do not align with common observations. We then provide a definition for consistently slower hardware traces that can be used to define timing anomalies and aligns with common observations.},\\n  category= {wcet},\\n  mywebpage = {soft-verif,wcet},\\n  keywords = {wcet},\\n   publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik},\\n  series    = {OASICS},\\n  volume    = {23},\\n        Type = {B - International Conferences},\\n\\n}\\n\\n\\n\",\"author_short\":[\"Cassez, F.\",\"Hansen, R. R.\",\"Olesen, M. C.\"],\"key\":\"wcet-12\",\"id\":\"wcet-12\",\"bibbaseid\":\"cassez-hansen-olesen-whatisatiminganomaly-2012\",\"role\":\"author\",\"urls\":{\"Paper\":\"http://science.mq.edu.au/~fcassez/bib/papers/wcet-2012.pdf\",\" link\":\"http://dx.doi.org/10.4230/OASIcs.WCET.2012.1\"},\"keyword\":[\"wcet\"],\"metadata\":{\"authorlinks\":{\"cassez, f\":\"http://science.mq.edu.au/~fcassez/software-verif.html\"}},\"html\":\"\"},{\"bibtype\":\"article\",\"type\":\"B - International Conferences\",\"author\":[{\"firstnames\":[\"Mark\"],\"propositions\":[],\"lastnames\":[\"Bradley\"],\"suffixes\":[]},{\"firstnames\":[\"Franck\"],\"propositions\":[],\"lastnames\":[\"Cassez\"],\"suffixes\":[]},{\"firstnames\":[\"Ansgar\"],\"propositions\":[],\"lastnames\":[\"Fehnker\"],\"suffixes\":[]},{\"firstnames\":[\"Thomas\"],\"propositions\":[],\"lastnames\":[\"Given-Wilson\"],\"suffixes\":[]},{\"firstnames\":[\"Ralf\"],\"propositions\":[],\"lastnames\":[\"Huuck\"],\"suffixes\":[]}],\"title\":\"High Performance Static Analysis for Industry\",\"journal\":\"Electr. Notes Theor. Comput. Sci.\",\"volume\":\"289\",\"year\":\"2012\",\"pages\":\"3-14\",\"urlpaper\":\"papers/tapas-2012.pdf\",\"ee\":\"http://dx.doi.org/10.1016/j.entcs.2012.11.002\",\"bibsource\":\"DBLP, http://dblp.uni-trier.de\",\"mywebpage\":\"soft-verif\",\"keywords\":\"software verification\",\"abstract\":\"Static source code analysis for software bug detection has come a long way since its early beginnings as a compiler technology. However, with the introduction of more sophisticated algorithmic techniques, such as model checking and constraint solving, questions about performance are a major concern. In this work we present an empirical study of our industrial strength source code analysis tool Goanna that uses a model checking core for static analysis of C/C++ code. We present the core technology and abstraction mechanism with a focus on performance, as guided by experience from having analyzed millions of lines of code. In particular, we present results from our recent study within the NIST/DHS SAMATE program. The results show that, maybe surprisingly, formal verification techniques can be used successfully in practical industry applications scaling roughly linearly, even for millions of lines of code. \",\"bibtex\":\"@article{tapas-12,\\n  author    = {Mark Bradley and\\n               Franck Cassez and\\n               Ansgar Fehnker and\\n               Thomas Given-Wilson and\\n               Ralf Huuck},\\n  title     = {High Performance Static Analysis for Industry},\\n  journal   = {Electr. Notes Theor. Comput. Sci.},\\n  volume    = {289},\\n  year      = {2012},\\n  pages     = {3-14},\\n  urlpaper = {papers/tapas-2012.pdf},\\n  ee        = {http://dx.doi.org/10.1016/j.entcs.2012.11.002},\\n  bibsource = {DBLP, http://dblp.uni-trier.de},\\n  mywebpage = {soft-verif},\\n  keywords = {software verification},\\n  abstract = {\\n  Static source code analysis for software bug detection has come a long way since its early beginnings as a compiler technology. However, with the introduction of more sophisticated algorithmic techniques, such as model checking and constraint solving, questions about performance are a major concern. In this work we present an empirical study of our industrial strength source code analysis tool Goanna that uses a model checking core for static analysis of C/C++ code. We present the core technology and abstraction mechanism with a focus on performance, as guided by experience from having analyzed millions of lines of code. In particular, we present results from our recent study within the NIST/DHS SAMATE program. The results show that, maybe surprisingly, formal verification techniques can be used successfully in practical industry applications scaling roughly linearly, even for millions of lines of code.\\n  },\\n        Type = {B - International Conferences},\\n\\n}\\n\\n\",\"author_short\":[\"Bradley, M.\",\"Cassez, F.\",\"Fehnker, A.\",\"Given-Wilson, T.\",\"Huuck, R.\"],\"key\":\"tapas-12\",\"id\":\"tapas-12\",\"bibbaseid\":\"bradley-cassez-fehnker-givenwilson-huuck-highperformancestaticanalysisforindustry-2012\",\"role\":\"author\",\"urls\":{\"Paper\":\"http://science.mq.edu.au/~fcassez/bib/papers/tapas-2012.pdf\",\"Link\":\"http://dx.doi.org/10.1016/j.entcs.2012.11.002\"},\"keyword\":[\"software verification\"],\"metadata\":{\"authorlinks\":{\"cassez, f\":\"http://science.mq.edu.au/~fcassez/software-verif.html\"}},\"html\":\"\"}],\n      metadata: {\"owner\":\"cassez, f\",\"authorlinks\":{\"cassez, f\":\"http://science.mq.edu.au/~fcassez/software-verif.html\"}},\n      ownerID: \"aYsqprsgp7HA5GpQ3\"\n    };\n  </script>\n\n  <script type=\"text/javascript\">\n  var site$;\n  if (typeof $ != 'undefined') {\n    console.log('existing jquery: storing and then restoring');\n    site$ = $;\n    $ = null;\n  }\n  </script>\n\n  <script src=\"https://ajax.googleapis.com/ajax/libs/jquery/2.2.4/jquery.min.js\">\n  </script>\n  <script type=\"text/javascript\">\n  if (site$) {\n    console.log('existing jquery: avoiding conflict and restoring');\n    bb$ = $.noConflict(true);\n    $ = site$;\n  } else {\n    bb$ = $;\n  }\n  </script>\n\n  <script src=\"//bibbase.org/js/bibbase.min.js\"\n          type=\"text/javascript\">\n  </script>\n\n  <script type=\"text/javascript\"\n          src=\"https://cdnjs.cloudflare.com/ajax/libs/mathjax/2.7.1/MathJax.js?config=TeX-AMS-MML_HTMLorMML\">\n  </script>\n  <script type=\"text/x-mathjax-config\">\n    MathJax.Hub.Config({tex2jax: {inlineMath: [['$','$'], ['\\\\(','\\\\)']]},\n                        skipTags: [\"body\"],\n                        processClass: \"bibbase_paper\"});\n  </script>\n\n  <style>\n  @media print {\n    .dontprint {\n        display: none !important;\n    }\n\n  .bibbase_group {\n    background-color: #E0E0E0;\n    font-style: italic;\n    font-size: larger;\n    text-shadow: 0px 0px 3px #FFFFFF;\n    border-radius: 4px 4px 4px 4px;\n    -moz-border-radius: 4px 4px 4px 4px;\n    -webkit-border-radius: 4px;\n    padding: 5px 40px 5px;\n    margin-top: 10px;\n    margin-bottom: 5px;\n    cursor: pointer;\n  }\n\n  .bibbase_paper {\n    margin-bottom: 5px;\n  }\n\n  }\n  </style>\n\n  \n  <div style=\"float: right; margin-right: 10px; margin-top: 10px; text-align: right; font-size: 12px\">\n    generated by\n    <a href=\"//bibbase.org\"\n       onclick=\"trackOutboundLink('bibbase', 'logo clicked', window.location.href, '//bibbase.org'); return false;\">\n      <img src=\"//bibbase.org/img/logo.svg\"\n           style=\"vertical-align: middle; margin-left: 3px; height: 16px;\"/\n           alt=\"bibbase.org\"\n           title=\"BibBase – The easiest way to maintain your publications page.\"\n        ></a>\n    \n  </div>\n  \n\n  <div id=\"bibbase_header\" class=\"dontprint\" style=\"\">\n\n    <ul class=\"nav nav-pills\" style=\"margin: 0px;\">\n\n      <li class=\"dropdown\" id=\"groupby_dropdown\">\n      <a class=\"dropdown-toggle\"\n         data-toggle=\"dropdown\"\n         href=\"#\">\n          Group by\n          <b class=\"caret\"></b>\n      </a>\n      <ul class=\"dropdown-menu\">\n        <li class=\"groupby year\"><a onclick=\"groupby('year')\">\n            Year</a>\n        </li>\n        <li class=\"groupby author\"><a onclick=\"groupby('author_short')\">\n            Author</a>\n        </li>\n        <li class=\"groupby type\"><a onclick=\"groupby('type')\">\n            Type</a>\n        </li>\n        <li class=\"groupby keyword\"><a onclick=\"groupby('keyword')\">\n            Keyword</a>\n        </li>\n        <li class=\"groupby downloads\"><a onclick=\"groupby('downloads')\">\n            Downloads</a>\n        </li>\n      </ul>\n      </li>\n\n\n      <li class=\"dropdown\" id=\"menu_dropdown\">\n      <a class=\"dropdown-toggle\"\n         data-toggle=\"dropdown\"\n         href=\"#\" alt=\"controls\">\n          <i class=\"fa fa-reorder\" alt=\"controls\"></i>\n          <b class=\"caret\"></b>\n      </a>\n      <ul class=\"dropdown-menu\">\n        <li>\n          <a onclick=\"toggleAll()\">\n            <i class=\"fa fa-chevron-down fa-fw\"></i> Expand/Collapse All\n          </a>\n        </li>\n        <li>\n          <a download=\"franck-bib.bib\" href=\"data:text/bibtex;base64,QGlucHJvY2VlZGluZ3N7c2NhbGEtMTcsCmF1dGhvciAgICA9IHtGcmFuY2sgQ2Fzc2V6CmFuZCB7QW50aG9ueSBNLn0gU2xvYW5lfSwKICB0aXRsZSAgICAgPSB7U2NhbGFTTVQ6IFNhdGlzZmlhYmlsaXR5IE1vZHVsbyBUaGVvcnkgaW4gU2NhbGEgKFRvb2wgUGFwZXIpfSwKICBib29rdGl0bGUgPSB7U0NBTEEnMTcsIE9jdG9iZXIgMjMtLTI3LCAyMDE3LCBWYW5jb3V2ZXIsIEJDLCBDYW5hZGEuIFByb2NlZWRpbmdzLn0sCiAgcGFnZXMgICAgID0ge30sCiAgeWVhciAgICAgID0gezIwMTd9LAogIHh4eHVybCAgICAgICA9IHtodHRwOi8vZHguZG9pLm9yZy8xMC4xMDA3Lzk3OC0zLTY2Mi00NjY4MS0wXzM5fSwKICB4eHhkb2kgICAgICAgPSB7MTAuMTAwNy85NzgtMy02NjItNDY2ODEtMF8zOX0sCiAgcHVibGlzaGVyID0gYWNtLAogIHh2b2x1bWUgPSA5MDM1LAogIHh4eHNlcmllcyAgICA9IGxuY3MsCiAgbXl3ZWJwYWdlID0ge3NvZnQtdmVyaWZ9LAogIGtleXdvcmRzID0ge3NjYWxhLCBTTVQgc29sdmVyc30sCiAgY2F0ZWdvcnkgPSB7c29mdC12ZXJpZn0sCiAgc2hvdyA9IHt9LAogIG5vdGU9e2ZvcnRoY29taW5nfSwKICB1cmxwYXBlciA9IHtwYXBlcnMvc2NhbGEtMTcucGRmfSwKICBhYnN0cmFjdCA9IHtBIFNhdGlzZmlhYmlsaXR5IE1vZHVsbyBUaGVvcnkgKFNNVCkgc29sdmVyIGlzIGEgcHJvZ3JhbSB0aGF0IGltcGxlbWVudHMgYWxnb3JpdGhtcyB0byBhdXRvbWF0aWNhbGx5IGRldGVybWluZSB3aGV0aGVyIAogIGEgbG9naWNhbCBmb3JtdWxhIGlzIHNhdGlzZmlhYmxlLiAKICBUaGUgcGVyZm9ybWFuY2Ugb2YgU01UIHNvbHZlcnMgaGFzIGRyYW1hdGljYWxseSBpbmNyZWFzZWQgaW4gdGhlIGxhc3QgZGVjYWRlIGFuZCBmb3IgaW5zdGFuY2UsIAogIG1hbnkgb2YgdGhlIHN0YXRlLW9mLXRoZS1hcnQgc29mdHdhcmUgYW5hbHlzaXMgdG9vbHMgaGVhdmlseSByZWx5IG9uIFNNVCBzb2x2aW5nIHRvIGFuYWx5c2Ugc291cmNlIGNvZGUuIAogIFdlIHByZXNlbnQgU2NhbGFTTVQsIGEgU2NhbGEgbGlicmFyeSB0aGF0IGxldmVyYWdlcyB0aGUgcG93ZXIgb2YgU01UIHNvbHZlcnMgYW5kIG1ha2VzIFNNVCBzb2x2aW5nIGRpcmVjdGx5IHVzYWJsZSBpbiBTY2FsYS4gCiAgU2NhbGFTTVQgcHJvdmlkZXMgc2VhbWxlc3MgYWNjZXNzIHRvIG51bWVyb3VzIHBvcHVsYXIgU01UIHNvbHZlcnMgbGlrZSBaMywgQ1ZDNCwgWWljZXMsIE1hdGhTYXQgb3IgU01USW50ZXJwb2wuIAogIE91ciBsaWJyYXJ5IGNvbWVzIHdpdGggYSBkb21haW4tc3BlY2lmaWMgbGFuZ3VhZ2UgdG8gd3JpdGUgdGVybXMgYW5kIGxvZ2ljYWwgZm9ybXVsYXMgZm9yIGEgd2lkZSByYW5nZSBvZiBsb2dpY2FsIHRoZW9yaWVzLCAKICB0aGVyZWJ5IGlzb2xhdGluZyB1c2VycyBmcm9tIHRoZSBkZXRhaWxzIG9mIHBhcnRpY3VsYXIgc29sdmVycy59LAogICAgVHlwZSA9IHtCIC0gSW50ZXJuYXRpb25hbCBDb25mZXJlbmNlc30sCiAgICBzaG93ID0ge30sCn0KCgoKQG1pc2N7Y2Fzc2V6MjAxN2FuYWx5c2lzLAogIHRpdGxlPXtBbmFseXNpcyBvZiBwcm9ncmFtIGNvZGV9LAogIGF1dGhvcj17Q2Fzc2V6LCBGLiBhbmQgTXtcInV9bGxlciwgQy59LAogIHVybD17aHR0cHM6Ly93d3cuZ29vZ2xlLmNvbS9wYXRlbnRzL1VTOTc2MDQ2OX0sCiAgeWVhcj17MjAxN30sCiAgbXl3ZWJwYWdlID0ge3NvZnQtdmVyaWZ9LAogIGtleXdvcmRzID0ge3NvZnR3YXJlIHZlcmlmaWNhdGlvbn0sCiAgY2F0ZWdvcnkgPSB7c29mdC12ZXJpZn0sCiAgbW9udGg9c2VwICMgIn4xMiIsCiAgbm90ZT17VVMgUGF0ZW50IDksNzYwLDQ2OX0KfQoKCgpAaW5wcm9jZWVkaW5nc3t0YWNhcy0xNywKYXV0aG9yICAgID0ge0ZyYW5jayBDYXNzZXoKYW5kIHtBbnRob255IE0ufSBTbG9hbmUKYW5kIE1hdHRoZXcgUm9iZXJ0cwphbmQgTWF0dGhldyBQaWdyYW0KYW5kIFBvbmdzYWsgU3V2YW5wb25nCmFuZCBQYWJsbyBHb256e1wne2F9fWxleiBkZSBBbGVkbyBNYXJ1Z3tcJ3thfX1ufSwKICB0aXRsZSAgICAgPSB7U2tpbms6IFN0YXRpYyBBbmFseXNpcyBvZiBQcm9ncmFtcyBpbiBMTFZNIEludGVybWVkaWF0ZSBSZXByZXNlbnRhdGlvbiAoQ29tcGV0aXRpb24gY29udHJpYnV0aW9uKX0sCiAgYm9va3RpdGxlID0ge1Rvb2xzIGFuZCBBbGdvcml0aG1zIGZvciB0aGUgQ29uc3RydWN0aW9uIGFuZCBBbmFseXNpcyBvZiBTeXN0ZW1zCiAgICAgICAgICAgICAgIC0gMjNyZCBJbnRlcm5hdGlvbmFsIENvbmZlcmVuY2UsIHtUQUNBU30gMjAxNywgSGVsZCBhcyBQYXJ0IG9mIHRoZQogICAgICAgICAgICAgICBFdXJvcGVhbiBKb2ludCBDb25mZXJlbmNlcyBvbiBUaGVvcnkgYW5kIFByYWN0aWNlIG9mIFNvZnR3YXJlLCB7RVRBUFN9CiAgICAgICAgICAgICAgIDIwMTcsIFVwcHNhbGEsIFN3ZWRlbiwgQXByaWwgMjItMjksIDIwMTcuIFByb2NlZWRpbmdzfSwKICAKIHBhZ2VzICAgICA9IHszODAtLTM4NH0sCiAgeWVhciAgICAgID0gezIwMTd9LAogIHVybCAgICAgICA9IHtodHRwczovL2RvaS5vcmcvMTAuMTAwNy85NzgtMy02NjItNTQ1ODAtNV8yN30sCiAgZG9pICAgICAgID0gezEwLjEwMDcvOTc4LTMtNjYyLTU0NTgwLTVfMjd9LAogIHB1Ymxpc2hlciA9IHNwcmluZ3YsCiAgeHZvbHVtZSA9IDEwMjA2LAogIHNlcmllcyAgICA9IGxuY3MsCiAgbXl3ZWJwYWdlID0ge3NvZnQtdmVyaWZ9LAogIGtleXdvcmRzID0ge3JlZmluZW1lbnQsIHNvZnR3YXJlIHZlcmlmaWNhdGlvbn0sCiAgY2F0ZWdvcnkgPSB7c29mdC12ZXJpZn0sCiAgc2hvdyA9IHt9LAogIHh4bm90ZT17Zm9ydGhjb21pbmd9LAogIHVybHBhcGVyID0ge3BhcGVycy9zdi1jb21wLTIwMTcucGRmfSwKICBhYnN0cmFjdCA9IHtTa2luayBpcyBhIHN0YXRpYyBhbmFseXNpcyB0b29sIHRoYXQgYW5hbHlzZXMgdGhlIExMVk0gaW50ZXJtZWRpYXRlIHJlcHJlc2VudGF0aW9uIChMTFZNLUlSKQpvZiBhIHByb2dyYW0gc291cmNlIGNvZGUuClRoZSBhbmFseXNpcyBjb25zaXN0cyBvZiBjaGVja2luZyB3aGV0aGVyIHRoZXJlIGlzIGEgZmVhc2libGUgZXhlY3V0aW9uIHRoYXQgY2FuIHJlYWNoIGEKIGRlc2lnbmF0ZWQgZXJyb3IgYmxvY2sgaW4gdGhlIExMVk0tSVIuClRoZSByZXN1bHQgb2YgYSBwcm9ncmFtIGFuYWx5c2lzIGlzIGBgY29ycmVjdCcnIGlmIHRoZSBlcnJvciBibG9jayBpcyBub3QgcmVhY2hhYmxlLApgYGluY29ycmVjdCcnIGlmIHRoZSBlcnJvciBibG9jayBpcyByZWFjaGFibGUsIG9yIGBgaW5jb25jbHVzaXZlJycgaWYgdGhlIHN0YXR1cyBvZiB0aGUgcHJvZ3JhbSBjb3VsZCBub3QgYmUgZGV0ZXJtaW5lZC4KSW4gdGhpcyBwYXBlciwgd2UgaW50cm9kdWNlIFNraW5rIFYyLjAgdG8gYW5hbHlzZSBzaW5nbGUgYW5kIG11bHRpLXRocmVhZGVkIEMgcHJvZ3JhbXMufSwKICAgIFR5cGUgPSB7QSAtIEludGVybmF0aW9uYWwgQ29uZmVyZW5jZXN9LAp9CgoKCiUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlCiUlJSAyMDE2CiUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlCgoKQGlucHJvY2VlZGluZ3N7Y2Fzc2V6LWxwYXItMjAxNSwKICBhdXRob3IgICAgPSB7RnJhbmNrIENhc3NleiBhbmQKICAgICAgICAgICAgICAgRnJvd2luIFppZWdsZXJ9LAogICAgICAgICAgICAgICAgZWRpdG9yICAgID0ge01hcnRpbiBEYXZpcyBhbmQKICAgICAgICAgICAgICAgQW5zZ2FyIEZlaG5rZXIgYW5kCiAgICAgICAgICAgICAgIEFubmFiZWxsZSBNY0l2ZXIgYW5kCiAgICAgICAgICAgICAgIEFuZHJlaSBWb3Jvbmtvdn0sCiAgdGl0bGUgICAgID0ge1ZlcmlmaWNhdGlvbiBvZiBDb25jdXJyZW50IFByb2dyYW1zIFVzaW5nIFRyYWNlIEFic3RyYWN0aW9uIFJlZmluZW1lbnR9LAogIGJvb2t0aXRsZSA9IHtMb2dpYyBmb3IgUHJvZ3JhbW1pbmcsIEFydGlmaWNpYWwgSW50ZWxsaWdlbmNlLCBhbmQgUmVhc29uaW5nIC0gMjB0aAogICAgICAgICAgICAgICBJbnRlcm5hdGlvbmFsIENvbmZlcmVuY2UsIHtMUEFSLTIwfSAyMDE1LCBTdXZhLCBGaWppLCBOb3ZlbWJlciAyNC0yOCwKICAgICAgICAgICAgICAgMjAxNSwgUHJvY2VlZGluZ3N9LAogIHBhZ2VzICAgICA9IHsyMzMtLTI0OH0sCiAgeWVhciAgICAgID0gezIwMTV9LAogIHNlcmllcyAgICA9IHtMZWN0dXJlIE5vdGVzIGluIENvbXB1dGVyIFNjaWVuY2V9LAogIHZvbHVtZSAgICA9IHs5NDUwfSwKICBwdWJsaXNoZXIgPSB7U3ByaW5nZXJ9LAogIHllYXIgICAgICA9IHsyMDE1fSwKICB1cmwgICAgICAgPSB7aHR0cDovL2R4LmRvaS5vcmcvMTAuMTAwNy85NzgtMy02NjItNDg4OTktN18xN30sCiAgbXl3ZWJwYWdlID0ge3NvZnQtdmVyaWZ9LAogIGNhdGVnb3J5ID0ge3NvZnQtdmVyaWZ9LAogIGlzYm4gICAgICA9IHs5NzgtMy02NjItNDg4OTgtMH0sCiAgZG9pICAgICAgID0gezEwLjEwMDcvOTc4LTMtNjYyLTQ4ODk5LTdfMTd9LAogIHNob3cgPSB7fSwKICBub3RlID0ge0xQQVIgQmVzdCBwYXBlciBhd2FyZH0sCiAgdXJscGFwZXIgPSB7cGFwZXJzL2xwYXItMjAxNS5wZGZ9LAogICAgdXJsc2xpZGVzID0ge3BhcGVycy9zbGlkZXMtbHBhci0yMDE1LnBkZn0sCiAgYWJzdHJhY3QgPSB7VmVyaWZ5aW5nIGNvbmN1cnJlbnQgcHJvZ3JhbXMgaXMgbm90b3Jpb3VzbHkgaGFyZCBkdWUgdG8gdGhlIHN0YXRlIGV4cGxvc2lvbiBwcm9ibGVtOiAoMSkgdGhlIGRhdGEgc3RhdGUgc3BhY2UgY2FuIGJlIHZlcnkgbGFyZ2UgYXMgdGhlIHZhcmlhYmxlcyBjYW4gcmFuZ2Ugb3ZlciB2ZXJ5IGxhcmdlIHNldHMsIGFuZCAoMikgdGhlIGNvbnRyb2wgc3RhdGUgc3BhY2UgaXMgdGhlIENhcnRlc2lhbiBwcm9kdWN0IG9mIHRoZSBjb250cm9sIHN0YXRlIHNwYWNlIG9mIHRoZSBjb25jdXJyZW50IGNvbS0gcG9uZW50cyBhbmQgdGh1cyBncm93cyBleHBvbmVudGlhbGx5IGluIHRoZSBudW1iZXIgb2YgY29tcG9uZW50cy4gT24gdGhlIG9uZSBoYW5kLCB0aGUgbW9zdCBzdWNjZXNzZnVsIGFwcHJvYWNoZXMgdG8gYWRkcmVzcyB0aGUgY29udHJvbCBzdGF0ZSBleHBsb3Npb24gcHJvYmxlbSBhcmUgYmFzZWQgb24gYXNzdW1lLWd1YXJhbnRlZSByZWFzb25pbmcgb3IgbW9kZWwtY2hlY2tpbmcgY291cGxlZCB3aXRoIHBhcnRpYWwgb3JkZXIgcmVkdWN0aW9uLiBPbiB0aGUgb3RoZXIgaGFuZCwgdGhlIG1vc3Qgc3VjY2Vzc2Z1bCB0ZWNobmlxdWVzIHRvIGFkZHJlc3MgdGhlIGRhdGEgc3BhY2UgZXhwbG9zaW9uIHByb2JsZW0gZm9yIHNlcXVlbnRpYWwgcHJvZ3JhbXMgdmVyaWZpY2F0aW9uIGFyZSBiYXNlZCBvbiB0aGUgYWJzdHJhY3Rpb24vcmVmaW5lLSBtZW50IHBhcmFkaWdtIHdoaWNoIGNvbnNpc3RzIGluIHJlZmluaW5nIGFuIGFic3RyYWN0IG92ZXItYXBwcm94aW1hdGlvbiBvZiBhIHByb2dyYW0gdmlhIHByZWRpY2F0ZSByZWZpbmVtZW50LiBJbiB0aGlzIHBhcGVyLCB3ZSBzaG93IHRoYXQgd2UgY2FuIGNvbWJpbmUgcGFydGlhbCBvcmRlciByZWR1Y3Rpb24gdGVjaG5pcXVlcyB3aXRoIHRyYWNlIGFic3RyYWN0aW9uIHJlZmluZW1lbnQuIFdlIGFwcGx5IG91ciBhcHByb2FjaCB0byBzdGFuZGFyZCBiZW5jaG1hcmtzIGFuZCBzaG93IHRoYXQgaXQgbWF0Y2hlcyBjdXJyZW50IHN0YXRlLW9mLXRoZS1hcnQgYW5hbHlzaXMgdGVjaG5pcXVlcy59LAogIFR5cGUgPSB7QiAtIEludGVybmF0aW9uYWwgQ29uZmVyZW5jZXN9LAp9CgoKCkBpbnByb2NlZWRpbmdze3RhY2FzLTE1LAphdXRob3IgICAgPSB7RnJhbmNrIENhc3NleiBhbmQKICAgICAgICAgICAgICAgVGFrYXNoaSBNYXRzdW9rYSBhbmQKICAgICAgICAgICAgICAgRWR3YXJkIFBpZXJ6Y2hhbHNraSBhbmQKICAgICAgICAgICAgICAgTmF0aGFuIFNteXRofSwKICB0aXRsZSAgICAgPSB7UGVyZW50aWU6IE1vZHVsYXIgVHJhY2UgUmVmaW5lbWVudCBhbmQgU2VsZWN0aXZlIFZhbHVlIFRyYWNraW5nIC0KICAgICAgICAgICAgICAgKENvbXBldGl0aW9uIENvbnRyaWJ1dGlvbil9LAogIGJvb2t0aXRsZSA9IHtUb29scyBhbmQgQWxnb3JpdGhtcyBmb3IgdGhlIENvbnN0cnVjdGlvbiBhbmQgQW5hbHlzaXMgb2YgU3lzdGVtcwogICAgICAgICAgICAgICAtIDIxc3QgSW50ZXJuYXRpb25hbCBDb25mZXJlbmNlLCB7VEFDQVN9IDIwMTUsIEhlbGQgYXMgUGFydCBvZiB0aGUKICAgICAgICAgICAgICAgRXVyb3BlYW4gSm9pbnQgQ29uZmVyZW5jZXMgb24gVGhlb3J5IGFuZCBQcmFjdGljZSBvZiBTb2Z0d2FyZSwge0VUQVBTfQogICAgICAgICAgICAgICAyMDE1LCBMb25kb24sIFVLLCBBcHJpbCAxMS0xOCwgMjAxNS4gUHJvY2VlZGluZ3N9LAogIHBhZ2VzICAgICA9IHs0MzktLTQ0Mn0sCiAgeWVhciAgICAgID0gezIwMTV9LAogIHVybCAgICAgICA9IHtodHRwOi8vZHguZG9pLm9yZy8xMC4xMDA3Lzk3OC0zLTY2Mi00NjY4MS0wXzM5fSwKICBkb2kgICAgICAgPSB7MTAuMTAwNy85NzgtMy02NjItNDY2ODEtMF8zOX0sCiAgcHVibGlzaGVyID0gc3ByaW5ndiwKICB2b2x1bWUgPSA5MDM1LAogIHNlcmllcyAgICA9IGxuY3MsCiAgbXl3ZWJwYWdlID0ge3NvZnQtdmVyaWZ9LAogIGtleXdvcmRzID0ge3JlZmluZW1lbnQsIHNvZnR3YXJlIHZlcmlmaWNhdGlvbn0sCiAgY2F0ZWdvcnkgPSB7c29mdC12ZXJpZn0sCiAgc2hvdyA9IHt9LAogIHVybHBhcGVyID0ge3BhcGVycy9zdi1jb21wLTIwMTUucGRmfSwKICBhYnN0cmFjdCA9IHtQZXJlbnRpZSBpcyBhIHNvZnR3YXJlIGFuYWx5c2lzIHRvb2wgYmFzZWQgb24gaXRlcmF0aXZlIHJlZmluZW1lbnQgb2YgdHJhY2UgYWJzdHJhY3Rpb246CiAgaWYgdGhlIHJlZmluZW1lbnQgcHJvY2VzcyB0ZXJtaW5hdGVzLCB0aGUgcHJvZ3JhbSBpcyBlaXRoZXIgZGVjbGFyZWQgY29ycmVjdCBvciBhIGNvdW50ZXJleGFtcGxlIGlzCiAgcHJvdmlkZWQgYW5kIHRoZSBwcm9ncmFtIGlzIGluY29ycmVjdC59LAogICAgVHlwZSA9IHtCIC0gSW50ZXJuYXRpb25hbCBDb25mZXJlbmNlc30sCgp9CgoKJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUKJSUlIDIwMTQKJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUKCgoKQGlucHJvY2VlZGluZ3N7ZnN0dGNzLTE0LAogIGF1dGhvciAgICA9IHtGcmFuY2sgQ2Fzc2V6IGFuZAogICAgICAgICAgICAgICBDaHJpc3RpYW4gTcO8bGxlciBhbmQKICAgICAgICAgICAgICAgS2FybGEgQnVybmV0dH0sCiAgdGl0bGUgICAgID0ge1N1bW1hcnktQmFzZWQgSW50ZXItUHJvY2VkdXJhbCBBbmFseXNpcyB2aWEgTW9kdWxhciBUcmFjZSBSZWZpbmVtZW50fSwKICBib29rdGl0bGUgPSB7MzR0aCBJbnRlcm5hdGlvbmFsIENvbmZlcmVuY2Ugb24gRm91bmRhdGlvbiBvZiBTb2Z0d2FyZSBUZWNobm9sb2d5CiAgICAgICAgICAgICAgIGFuZCBUaGVvcmV0aWNhbCBDb21wdXRlciBTY2llbmNlLCB7RlNUVENTfSAyMDE0LCBEZWNlbWJlciAxNS0xNywgMjAxNCwKICAgICAgICAgICAgICAgTmV3IERlbGhpLCBJbmRpYX0sCiAgcGFnZXMgICAgID0gezU0NS0tNTU2fSwKICB5ZWFyICAgICAgPSB7MjAxNH0sCiAgbXl3ZWJwYWdlID0ge3NvZnQtdmVyaWZ9LAogIGNhdGVnb3J5ID0ge1NvZnR3YXJlIHZlcmlmaWNhdGlvbn0sCiAga2V5d29yZHMgPSB7dHJhY2UgcmVmaW5lbWVudCwgc29mdHdhcmUgdmVyaWZpY2F0aW9uLCBIb2FyZSBsb2dpY30sCiAgdXJsX2xpbmsgICAgICAgPSB7aHR0cDovL2R4LmRvaS5vcmcvMTAuNDIzMC9MSVBJY3MuRlNUVENTLjIwMTQuNTQ1fSwKICBkb2kgICAgICAgPSB7MTAuNDIzMC9MSVBJY3MuRlNUVENTLjIwMTQuNTQ1fSwKICBhYnN0cmFjdCA9IHtXZSBwcm9wb3NlIGEgZ2VuZXJhbGlzYXRpb24gb2YgdHJhY2UgcmVmaW5lbWVudCBmb3IgdGhlIHZlcmlmaWNhdGlvbiBvZiBpbnRlci1wcm9jZWR1cmFsIHByb2dyYW1zLgogIE91ciBtZXRob2QgaXMgYSB0b3AtZG93biBtb2R1bGFyLCBzdW1tYXJ5LWJhc2VkIGFwcHJvYWNoLCBhbmQgYW5hbHlzZXMgaW50ZXItcHJvY2VkdXJhbCBwcm9ncmFtcyBieSBidWlsZGluZyBmdW5jdGlvbiBzdW1tYXJpZXMgb24tZGVtYW5kCiAgYW5kIGltcHJvdmluZyB0aGUgc3VtbWFyaWVzIGVhY2ggdGltZSBhIGZ1bmN0aW9uIGlzIGFuYWx5c2VkLiBPdXIgbWV0aG9kIGlzIHNvdW5kLCBhbmQgY29tcGxldGUgcmVsYXRpdmUgdG8gdGhlIGV4aXN0ZW5jZSBvZiBhCiAgbW9kdWxhciBIb2FyZSBwcm9vZiBmb3IgYSBub24tcmVjdXJzaXZlIHByb2dyYW0uIFdlIGhhdmUgaW1wbGVtZW50ZWQgYSBwcm90b3R5cGUgYW5hbHlzZXIgdGhhdCBkZW1vbnN0cmF0ZXMgdGhlCiAgbWFpbiBmZWF0dXJlcyBvZiBvdXIgYXBwcm9hY2ggYW5kIHlpZWxkcyBwcm9taXNpbmcgcmVzdWx0cy4KICB9LAogIFR5cGUgPSB7QiAtIEludGVybmF0aW9uYWwgQ29uZmVyZW5jZXN9LAp9CgoKCgpAaW5wcm9jZWVkaW5nc3tzY2FtLTIwMTMsCiAgYXV0aG9yICAgID0ge1NlYmFzdGlhbiBCaWFsbGFzIGFuZAogICAgICAgICAgICAgICBNYWRzIENoci4gT2xlc2VuIGFuZAogICAgICAgICAgICAgICBGcmFuY2sgQ2Fzc2V6IGFuZAogICAgICAgICAgICAgICBSYWxmIEh1dWNrfSwKICB0aXRsZSAgICAgPSB7UHRyVHJhY2tlcjogUHJhZ21hdGljIHBvaW50ZXIgYW5hbHlzaXN9LAogIGJvb2t0aXRsZSA9IHsxM3RoIHtJRUVFfSBJbnRlcm5hdGlvbmFsIFdvcmtpbmcgQ29uZmVyZW5jZSBvbiBTb3VyY2UgQ29kZSBBbmFseXNpcwogICAgICAgICAgICAgICBhbmQgTWFuaXB1bGF0aW9uLCB7U0NBTX0gMjAxMywgRWluZGhvdmVuLCBOZXRoZXJsYW5kcywgU2VwdGVtYmVyIDIyLTIzLAogICAgICAgICAgICAgICAyMDEzfSwKICBwYWdlcyAgICAgPSB7NjktLTczfSwKICB5ZWFyICAgICAgPSB7MjAxM30sCiAgcHVibGlzaGVyID0ge3tJRUVFfSBDb21wdXRlciBTb2NpZXR5fSwKICB1cmxwYXBlciA9IHtwYXBlcnMvc2NhbS0yMDEzLnBkZn0sCiAgdXJsX2xpbmsgICAgICAgPSB7aHR0cDovL2R4LmRvaS5vcmcvMTAuMTEwOS9TQ0FNLjIwMTMuNjY0ODE4Nn0sCiAgZG9pICAgICAgID0gezEwLjExMDkvU0NBTS4yMDEzLjY2NDgxODZ9LAogIGtleXdvcmRzID0ge1NvZnR3YXJlIHZlcmlmaWNhdGlvbiwgcG9pbnRlcnMsIHN0YXRpYyBhbmFseXNpc30sCiAgbXl3ZWJwYWdlID0ge3NvZnQtdmVyaWZ9LAogIGNhdGVnb3J5ID0ge1NvZnR3YXJlIHZlcmlmaWNhdGlvbn0sCiAgYWJzdHJhY3QgPSB7CiAgU3RhdGljIHByb2dyYW0gYW5hbHlzaXMgZm9yIGJ1ZyBkZXRlY3Rpb24gaW4gaW5kdXN0cmlhbCBDL0MrKyBjb2RlIGhhcyBtYW55IGNoYWxsZW5nZXMuIE9uZSBvZiB0aGVtIGlzIHRvIGFuYWx5emUgcG9pbnRlciBhbmQgcG9pbnRlciBzdHJ1Y3R1cmVzIGVmZmljaWVudGx5LiBXaGlsZSB0aGVyZSBoYXMgYmVlbiBtdWNoIHJlc2VhcmNoIGludG8gdmFyaW91cyBhc3BlY3RzIG9mIHBvaW50ZXIgYW5hbHlzaXMgZWl0aGVyIGZvciBjb21waWxlciBvcHRpbWl6YXRpb24gb3IgZm9yIHZlcmlmaWNhdGlvbiB0YXNrcywgYm90aCBjbGFzc2ljYWwgY2F0ZWdvcmllcyBhcmUgbm90IG9wdGltaXplZCBmb3IgYnVnIGRldGVjdGlvbiwgd2hlcmUgc3BlZWQgYW5kIHByZWNpc2lvbiBhcmUgaW1wb3J0YW50LCBidXQgc291bmRuZXNzIChubyBtaXNzZWQgYnVncykgYW5kIGNvbXBsZXRlbmVzcyAobm8gZmFsc2UgcG9zaXRpdmVzKSBkbyBub3QgbmVjZXNzYXJpbHkgbmVlZCB0byBiZSBndWFyYW50ZWVkLgogIH0sCiAgICBUeXBlID0ge0IgLSBJbnRlcm5hdGlvbmFsIENvbmZlcmVuY2VzfSwKfQoKCgpAaW5wcm9jZWVkaW5nc3t3Y2V0LTEyLAogIGF1dGhvciAgICA9IHtGcmFuY2sgQ2Fzc2V6IGFuZAogICAgICAgICAgICAgICBSZW7DqSBSeWRob2YgSGFuc2VuIGFuZAogICAgICAgICAgICAgICBNYWRzIENoci4gT2xlc2VufSwKICB0aXRsZSAgICAgPSB7V2hhdCBpcyBhIFRpbWluZyBBbm9tYWx5P30sCiAgYm9va3RpdGxlID0gezEydGggSW50ZXJuYXRpb25hbCBXb3Jrc2hvcCBvbiBXb3JzdC1DYXNlIEV4ZWN1dGlvbiBUaW1lCiAgICAgICAgICAgICAgIEFuYWx5c2lzLCBXQ0VUIDIwMTIsIEp1bHkgMTAsIDIwMTIsIFBpc2EsIEl0YWx5fSwKICB5ZWFyICAgICAgPSB7MjAxMn0sCiAgcGFnZXMgICAgID0gezEtMTJ9LAogIHVybHBhcGVyID0ge3BhcGVycy93Y2V0LTIwMTIucGRmfSwKICB1cmxfbGluayAgICAgICAgPSB7aHR0cDovL2R4LmRvaS5vcmcvMTAuNDIzMC9PQVNJY3MuV0NFVC4yMDEyLjF9LAogIGFic3RyYWN0ID0ge1RpbWluZyBhbm9tYWxpZXMgbWFrZSB3b3JzdC1jYXNlIGV4ZWN1dGlvbiB0aW1lIGFuYWx5c2lzIG11Y2ggaGFyZGVyLCBiZWNhdXNlIHRoZSBhbmFseXNpcyB3aWxsIGhhdmUgdG8gY29uc2lkZXIgYWxsIGxvY2FsIGNob2ljZXMuIEl0IGhhcyBiZWVuIHdpZGVseSByZWNvZ25pc2VkIHRoYXQgY2VydGFpbiBoYXJkd2FyZSBmZWF0dXJlcyBhcmUgdGltaW5nIGFub21hbG91cywgd2hpbGUgb3RoZXJzIGFyZSBub3QuIEhvd2V2ZXIsIGRlZmluaW5nIGZvcm1hbGx5IHdoYXQgYSB0aW1pbmcgYW5vbWFseSBpcywgaGFzIGJlZW4gZGlmZmljdWx0LiBXZSBleGFtaW5lIHByZXZpb3VzIGRlZmluaXRpb25zIG9mIHRpbWluZyBhbm9tYWxpZXMsIGFuZCBpZGVudGlmeSBleGFtcGxlcyB3aGVyZSB0aGV5IGRvIG5vdCBhbGlnbiB3aXRoIGNvbW1vbiBvYnNlcnZhdGlvbnMuIFdlIHRoZW4gcHJvdmlkZSBhIGRlZmluaXRpb24gZm9yIGNvbnNpc3RlbnRseSBzbG93ZXIgaGFyZHdhcmUgdHJhY2VzIHRoYXQgY2FuIGJlIHVzZWQgdG8gZGVmaW5lIHRpbWluZyBhbm9tYWxpZXMgYW5kIGFsaWducyB3aXRoIGNvbW1vbiBvYnNlcnZhdGlvbnMufSwKICBjYXRlZ29yeT0ge3djZXR9LAogIG15d2VicGFnZSA9IHtzb2Z0LXZlcmlmLHdjZXR9LAogIGtleXdvcmRzID0ge3djZXR9LAogICBwdWJsaXNoZXIgPSB7U2NobG9zcyBEYWdzdHVobCAtIExlaWJuaXotWmVudHJ1bSBmdWVyIEluZm9ybWF0aWt9LAogIHNlcmllcyAgICA9IHtPQVNJQ1N9LAogIHZvbHVtZSAgICA9IHsyM30sCiAgICAgICAgVHlwZSA9IHtCIC0gSW50ZXJuYXRpb25hbCBDb25mZXJlbmNlc30sCgp9CgoKCgpAYXJ0aWNsZXt0YXBhcy0xMiwKICBhdXRob3IgICAgPSB7TWFyayBCcmFkbGV5IGFuZAogICAgICAgICAgICAgICBGcmFuY2sgQ2Fzc2V6IGFuZAogICAgICAgICAgICAgICBBbnNnYXIgRmVobmtlciBhbmQKICAgICAgICAgICAgICAgVGhvbWFzIEdpdmVuLVdpbHNvbiBhbmQKICAgICAgICAgICAgICAgUmFsZiBIdXVja30sCiAgdGl0bGUgICAgID0ge0hpZ2ggUGVyZm9ybWFuY2UgU3RhdGljIEFuYWx5c2lzIGZvciBJbmR1c3RyeX0sCiAgam91cm5hbCAgID0ge0VsZWN0ci4gTm90ZXMgVGhlb3IuIENvbXB1dC4gU2NpLn0sCiAgdm9sdW1lICAgID0gezI4OX0sCiAgeWVhciAgICAgID0gezIwMTJ9LAogIHBhZ2VzICAgICA9IHszLTE0fSwKICB1cmxwYXBlciA9IHtwYXBlcnMvdGFwYXMtMjAxMi5wZGZ9LAogIGVlICAgICAgICA9IHtodHRwOi8vZHguZG9pLm9yZy8xMC4xMDE2L2ouZW50Y3MuMjAxMi4xMS4wMDJ9LAogIGJpYnNvdXJjZSA9IHtEQkxQLCBodHRwOi8vZGJscC51bmktdHJpZXIuZGV9LAogIG15d2VicGFnZSA9IHtzb2Z0LXZlcmlmfSwKICBrZXl3b3JkcyA9IHtzb2Z0d2FyZSB2ZXJpZmljYXRpb259LAogIGFic3RyYWN0ID0gewogIFN0YXRpYyBzb3VyY2UgY29kZSBhbmFseXNpcyBmb3Igc29mdHdhcmUgYnVnIGRldGVjdGlvbiBoYXMgY29tZSBhIGxvbmcgd2F5IHNpbmNlIGl0cyBlYXJseSBiZWdpbm5pbmdzIGFzIGEgY29tcGlsZXIgdGVjaG5vbG9neS4gSG93ZXZlciwgd2l0aCB0aGUgaW50cm9kdWN0aW9uIG9mIG1vcmUgc29waGlzdGljYXRlZCBhbGdvcml0aG1pYyB0ZWNobmlxdWVzLCBzdWNoIGFzIG1vZGVsIGNoZWNraW5nIGFuZCBjb25zdHJhaW50IHNvbHZpbmcsIHF1ZXN0aW9ucyBhYm91dCBwZXJmb3JtYW5jZSBhcmUgYSBtYWpvciBjb25jZXJuLiBJbiB0aGlzIHdvcmsgd2UgcHJlc2VudCBhbiBlbXBpcmljYWwgc3R1ZHkgb2Ygb3VyIGluZHVzdHJpYWwgc3RyZW5ndGggc291cmNlIGNvZGUgYW5hbHlzaXMgdG9vbCBHb2FubmEgdGhhdCB1c2VzIGEgbW9kZWwgY2hlY2tpbmcgY29yZSBmb3Igc3RhdGljIGFuYWx5c2lzIG9mIEMvQysrIGNvZGUuIFdlIHByZXNlbnQgdGhlIGNvcmUgdGVjaG5vbG9neSBhbmQgYWJzdHJhY3Rpb24gbWVjaGFuaXNtIHdpdGggYSBmb2N1cyBvbiBwZXJmb3JtYW5jZSwgYXMgZ3VpZGVkIGJ5IGV4cGVyaWVuY2UgZnJvbSBoYXZpbmcgYW5hbHl6ZWQgbWlsbGlvbnMgb2YgbGluZXMgb2YgY29kZS4gSW4gcGFydGljdWxhciwgd2UgcHJlc2VudCByZXN1bHRzIGZyb20gb3VyIHJlY2VudCBzdHVkeSB3aXRoaW4gdGhlIE5JU1QvREhTIFNBTUFURSBwcm9ncmFtLiBUaGUgcmVzdWx0cyBzaG93IHRoYXQsIG1heWJlIHN1cnByaXNpbmdseSwgZm9ybWFsIHZlcmlmaWNhdGlvbiB0ZWNobmlxdWVzIGNhbiBiZSB1c2VkIHN1Y2Nlc3NmdWxseSBpbiBwcmFjdGljYWwgaW5kdXN0cnkgYXBwbGljYXRpb25zIHNjYWxpbmcgcm91Z2hseSBsaW5lYXJseSwgZXZlbiBmb3IgbWlsbGlvbnMgb2YgbGluZXMgb2YgY29kZS4KICB9LAogICAgICAgIFR5cGUgPSB7QiAtIEludGVybmF0aW9uYWwgQ29uZmVyZW5jZXN9LAoKfQoK\">\n            <i class=\"fa fa-download fa-fw\"></i> Download BibTeX\n          </a>\n        </li>\n        <li>\n          <a href=\"//bibbase.org/rss?bib=http://science.mq.edu.au/~fcassez/bib/franck-bib.bib\">\n            <i class=\"fa fa-rss fa-fw\"></i> RSS Feed\n          </a>\n          </li>\n      </ul>\n      </li>\n\n      \n\n\n      \n    </ul>\n\n\n    <div class=\"alert alert-success bibbase_msg\" id=\"bibbase_msg_embed\"\n         style=\"display: none;\">\n\n      Excellent! Next you can\n      <a href=\"/network/register?next=/network/newSiteFromTemplate%3Fbiburl=http://science.mq.edu.au/~fcassez/bib/franck-bib.bib\"\n      >create a new website with this list</a>, or\n      embed it in an existing web page by copying &amp; pasting\n      any of the following snippets.\n\n      <div style=\"text-align: left; margin-top: 1em;\">\n        <strong>JavaScript</strong>\n        <span class=\"comment recommended\">(easiest)</span>\n        <div class=\"well well-small\">\n          <code>\n            &lt;script src=\"https://bibbase.org/show?bib=http%3A%2F%2Fscience.mq.edu.au%2F%7Efcassez%2Fbib%2Ffranck-bib.bib&amp;jsonp=1&amp;filter=mywebpage:soft-verif&amp;css=true&amp;jsonp=1\"&gt;&lt;/script&gt;\n          </code>\n        </div>\n\n        <strong>PHP</strong>\n        <div class=\"well well-small\">\n          <code>\n            &lt;?php\n            $contents = file_get_contents(\"https://bibbase.org/show?bib=http%3A%2F%2Fscience.mq.edu.au%2F%7Efcassez%2Fbib%2Ffranck-bib.bib&amp;jsonp=1&amp;filter=mywebpage:soft-verif&amp;css=true\");\n            print_r($contents);\n            ?&gt;\n          </code>\n        </div>\n\n        <strong>iFrame</strong>\n        <span class=\"comment\">(not recommended)</span>\n        <div class=\"well well-small\">\n          <code>\n            &lt;iframe src=\"https://bibbase.org/show?bib=http%3A%2F%2Fscience.mq.edu.au%2F%7Efcassez%2Fbib%2Ffranck-bib.bib&amp;jsonp=1&amp;filter=mywebpage:soft-verif&amp;css=true\"&gt;&lt;/iframe&gt;\n          </code>\n        </div>\n\n        <p>\n          For more details see the <a href=\"//bibbase.org/help\">documention</a>.\n        </p>\n      </div>\n    </div>\n\n    <div class=\"alert alert-success bibbase_msg\" id=\"bibbase_msg_preview\"\n         style=\"display: none;\">\n\n      This is a preview! To use this list on your own web site\n      or create a new web site from it,\n      <a href=\"/network/register?next=/network/newAccountWithFile%3FfileId=\"\n      >create a free account</a>. The file will be added\n      and you will be able to edit it in the File Manager.\n      We will show you instructions once you've created your account.\n    </div>\n\n    <div class=\"alert alert-warning bibbase_msg\" id=\"bibbase_msg_mendeley1\"\n         style=\"display: none;\">\n\n      <p>To the site owner:</p>\n\n      <p><strong>Action required!</strong> Mendeley is changing its\n        API. In order to keep using Mendeley with BibBase past April\n        14th, you need to:\n        <ol>\n          <li>renew the authorization for BibBase on Mendeley, and</li>\n          <li>update the BibBase URL\n            in your page the same way you did when you initially set up\n            this page.\n          </li>\n        </ol>\n      </p>\n\n      <p>\n        <a href=\"http://bibbase.org/cgi-bin/mendeley2/get.py\">\n          <i class=\"fa fa-angle-double-right\"></i>\n          Fix it now</a>\n      </p>\n    </div>\n\n  </div>\n\n\n  <div id=\"bibbase_body\">\n    \n  \n  <div class=\"bibbase_group_whole\" id=\"group_2017\">\n    <div class=\"bibbase_group\"\n      onclick=\"toggleGroup('group_2017')\"\n      onkeypress=\"toggleGroup('group_2017')\"\n      tabindex=\"0\">\n      <i class=\"fa fa-angle-down bibbase_group_head_icon\"></i>&nbsp;\n      <span>2017</span>\n      <span class=\"bibbase_group_count\">\n        \n        (3)\n        \n      </span>\n    </div>\n    <div class=\"bibbase_group_body\">\n      \n  \n  <div class=\"bibbase_paper\" id=\"cassez-sloane-scalasmtsatisfiabilitymodulotheoryinscalatoolpaper-2017\">\n  <span class=\"bibbase_paper_titleauthoryear\">\n\n  \n  <span class=\"bibbase_paper_title\">\n  \n  \n  \n  <a href=\"http://science.mq.edu.au/~fcassez/bib/papers/scala-17.pdf\"\n     onclick=\"return trackOutboundLink('publications', 'click', 'cassez-sloane-scalasmtsatisfiabilitymodulotheoryinscalatoolpaper-2017', 'http://science.mq.edu.au/~fcassez/bib/papers/scala-17.pdf', event);\">\n    ScalaSMT: Satisfiability Modulo Theory in Scala (Tool Paper).\n  </a>\n  \n  \n  \n</span>\n\n  <span class=\"bibbase_paper_author\">\n  <a class=\"bibbase author link\" href=\"http://science.mq.edu.au/~fcassez/software-verif.html\">Cassez, F.</a>;  and Sloane, A.\n</span>\n\n  \n\n</span>\n\n  In <i>SCALA'17, October 23–27, 2017, Vancouver, BC, Canada. Proceedings.</i>,  2017. Association for Computing Machinery\n  <span class=\"note\">forthcoming</span>\n\n<span class=\"bibbase_note\"></span>\n\n<br class=\"bibbase_paper_content\"/>\n\n<span class=\"bibbase_paper_content dontprint\">\n\n  \n  <a href=\"http://science.mq.edu.au/~fcassez/bib/papers/scala-17.pdf\"\n     onclick=\"log_download('cassez-sloane-scalasmtsatisfiabilitymodulotheoryinscalatoolpaper-2017', 'http://science.mq.edu.au/~fcassez/bib/papers/scala-17.pdf', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/pdf.svg\"\n\t     alt=\"ScalaSMT: Satisfiability Modulo Theory in Scala (Tool Paper) [pdf]\"\n       title=\"Paper\"\n\t     class=\"bibbase_icon\"\n         ><span class=\"bibbase_icon_text\">Paper</span></a>\n  &nbsp;\n  \n\n  \n\n  \n  <a href=\"//bibbase.org/network/publication/cassez-sloane-scalasmtsatisfiabilitymodulotheoryinscalatoolpaper-2017\"\n     class=\"bibbase bibbase_page link\">link</a>\n  &nbsp;\n  \n\n  <a href=\"#\"\n     onclick=\"showBib(event); return false;\"\n     class=\"bibbase bibtex link\">bibtex\n    <i class=\"fa fa-caret-down\"></i></a>\n\n  \n  &nbsp;\n  <a class=\"bibbase_abstract_link bibbase link\"\n     href=\"#\"\n     onclick=\"showAbstract(event); return false;\">\n    abstract <i class=\"fa fa-caret-down\"></i></a>\n  \n\n  \n  &nbsp;\n  <span class=\"bibbase_stats_paper\" style=\"color: #777;\">\n    <span>3 downloads</span>\n  </span>\n  \n\n  <!-- <a class=\"bibbase read link hidden\" -->\n  <!--    href=\"javascript:toggleRead('cassez-sloane-scalasmtsatisfiabilitymodulotheoryinscalatoolpaper-2017')\" -->\n  <!--    title=\"Marking this paper as read adds it to your library on BibBase.\" -->\n  <!--    > -->\n  <!--   <i class=\"fa fa-check\"></i>&nbsp; -->\n  <!--   <span>mark as read</span> -->\n  <!-- </a> -->\n\n  &nbsp;\n  \n  \n  \n  \n  \n  \n\n</span>\n\n<div class=\"well well-small bibbase\" data-type=\"bibtex\"\n     style=\"display:none\">\n  <pre style=\"white-space: pre-wrap;\">@inproceedings{scala-17,\nauthor    = {Franck Cassez\nand {Anthony M.} Sloane},\n  title     = {ScalaSMT: Satisfiability Modulo Theory in Scala (Tool Paper)},\n  booktitle = {SCALA&#x27;17, October 23--27, 2017, Vancouver, BC, Canada. Proceedings.},\n  pages     = {},\n  year      = {2017},\n  xxxurl       = {http://dx.doi.org/10.1007/978-3-662-46681-0_39},\n  xxxdoi       = {10.1007/978-3-662-46681-0_39},\n  publisher = acm,\n  xvolume = 9035,\n  xxxseries    = lncs,\n  mywebpage = {soft-verif},\n  keywords = {scala, SMT solvers},\n  category = {soft-verif},\n  show = {},\n  note={forthcoming},\n  urlpaper = {papers/scala-17.pdf},\n  abstract = {A Satisfiability Modulo Theory (SMT) solver is a program that implements algorithms to automatically determine whether \n  a logical formula is satisfiable. \n  The performance of SMT solvers has dramatically increased in the last decade and for instance, \n  many of the state-of-the-art software analysis tools heavily rely on SMT solving to analyse source code. \n  We present ScalaSMT, a Scala library that leverages the power of SMT solvers and makes SMT solving directly usable in Scala. \n  ScalaSMT provides seamless access to numerous popular SMT solvers like Z3, CVC4, Yices, MathSat or SMTInterpol. \n  Our library comes with a domain-specific language to write terms and logical formulas for a wide range of logical theories, \n  thereby isolating users from the details of particular solvers.},\n    Type = {B - International Conferences},\n    show = {},\n}\n\n</pre>\n</div>\n\n\n<div class=\"well well-small bibbase\" data-type=\"abstract\"\n     style=\"display:none\">\n  A Satisfiability Modulo Theory (SMT) solver is a program that implements algorithms to automatically determine whether a logical formula is satisfiable. The performance of SMT solvers has dramatically increased in the last decade and for instance, many of the state-of-the-art software analysis tools heavily rely on SMT solving to analyse source code. We present ScalaSMT, a Scala library that leverages the power of SMT solvers and makes SMT solving directly usable in Scala. ScalaSMT provides seamless access to numerous popular SMT solvers like Z3, CVC4, Yices, MathSat or SMTInterpol. Our library comes with a domain-specific language to write terms and logical formulas for a wide range of logical theories, thereby isolating users from the details of particular solvers.\n</div>\n\n\n</div>\n\n\n  <div class=\"bibbase_paper\" id=\"cassez-mller-analysisofprogramcode-2017\">\n  <span class=\"bibbase_paper_titleauthoryear\">\n\n  \n  <span class=\"bibbase_paper_title\">\n  \n  \n  \n  <a href=\"https://www.google.com/patents/US9760469\"\n     onclick=\"return trackOutboundLink('publications', 'click', 'cassez-mller-analysisofprogramcode-2017', 'https://www.google.com/patents/US9760469', event);\">\n    Analysis of program code.\n  </a>\n  \n  \n  \n</span>\n\n  <span class=\"bibbase_paper_author\">\n  <a class=\"bibbase author link\" href=\"http://science.mq.edu.au/~fcassez/software-verif.html\">Cassez, F.</a>;  and Müller, C.\n</span>\n\n  \n\n</span>\n\n  September~12 2017.\n  <span class=\"note\">US Patent 9,760,469</span>\n\n<span class=\"bibbase_note\"></span>\n\n<br class=\"bibbase_paper_content\"/>\n\n<span class=\"bibbase_paper_content dontprint\">\n\n  \n  <a href=\"https://www.google.com/patents/US9760469\"\n     onclick=\"log_download('cassez-mller-analysisofprogramcode-2017', 'https://www.google.com/patents/US9760469', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/link.svg\"\n\t     alt=\"Analysis of program code [link]\"\n       title=\"Paper\"\n\t     class=\"bibbase_icon\"\n         ><span class=\"bibbase_icon_text\">Paper</span></a>\n  &nbsp;\n  \n\n  \n\n  \n  <a href=\"//bibbase.org/network/publication/cassez-mller-analysisofprogramcode-2017\"\n     class=\"bibbase bibbase_page link\">link</a>\n  &nbsp;\n  \n\n  <a href=\"#\"\n     onclick=\"showBib(event); return false;\"\n     class=\"bibbase bibtex link\">bibtex\n    <i class=\"fa fa-caret-down\"></i></a>\n\n  \n\n  \n\n  <!-- <a class=\"bibbase read link hidden\" -->\n  <!--    href=\"javascript:toggleRead('cassez-mller-analysisofprogramcode-2017')\" -->\n  <!--    title=\"Marking this paper as read adds it to your library on BibBase.\" -->\n  <!--    > -->\n  <!--   <i class=\"fa fa-check\"></i>&nbsp; -->\n  <!--   <span>mark as read</span> -->\n  <!-- </a> -->\n\n  &nbsp;\n  \n  \n  \n  \n\n</span>\n\n<div class=\"well well-small bibbase\" data-type=\"bibtex\"\n     style=\"display:none\">\n  <pre style=\"white-space: pre-wrap;\">@misc{cassez2017analysis,\n  title={Analysis of program code},\n  author={Cassez, F. and M{\\&quot;u}ller, C.},\n  url={https://www.google.com/patents/US9760469},\n  year={2017},\n  mywebpage = {soft-verif},\n  keywords = {software verification},\n  category = {soft-verif},\n  month=sep # &quot;~12&quot;,\n  note={US Patent 9,760,469}\n}\n\n</pre>\n</div>\n\n\n\n</div>\n\n\n  <div class=\"bibbase_paper\" id=\"cassez-sloane-roberts-pigram-suvanpong-dealedomarugn-skinkstaticanalysisofprogramsinllvmintermediaterepresentationcompetitioncontribution-2017\">\n  <span class=\"bibbase_paper_titleauthoryear\">\n\n  \n  <span class=\"bibbase_paper_title\">\n  \n  \n  \n  <a href=\"http://science.mq.edu.au/~fcassez/bib/papers/sv-comp-2017.pdf\"\n     onclick=\"return trackOutboundLink('publications', 'click', 'cassez-sloane-roberts-pigram-suvanpong-dealedomarugn-skinkstaticanalysisofprogramsinllvmintermediaterepresentationcompetitioncontribution-2017', 'http://science.mq.edu.au/~fcassez/bib/papers/sv-comp-2017.pdf', event);\">\n    Skink: Static Analysis of Programs in LLVM Intermediate Representation (Competition contribution).\n  </a>\n  \n  \n  \n</span>\n\n  <span class=\"bibbase_paper_author\">\n  <a class=\"bibbase author link\" href=\"http://science.mq.edu.au/~fcassez/software-verif.html\">Cassez, F.</a>; Sloane, A.; Roberts, M.; Pigram, M.; Suvanpong, P.;  and de Aledo Marugán, P. G.\n</span>\n\n  \n\n</span>\n\n  In <i>Tools and Algorithms for the Construction and Analysis of Systems - 23rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017. Proceedings</i>, of <i>LNCS</i>, pages 380–384,  2017. Springer\n  <span class=\"note\"></span>\n\n<span class=\"bibbase_note\"></span>\n\n<br class=\"bibbase_paper_content\"/>\n\n<span class=\"bibbase_paper_content dontprint\">\n\n  \n  <a href=\"http://science.mq.edu.au/~fcassez/bib/papers/sv-comp-2017.pdf\"\n     onclick=\"log_download('cassez-sloane-roberts-pigram-suvanpong-dealedomarugn-skinkstaticanalysisofprogramsinllvmintermediaterepresentationcompetitioncontribution-2017', 'http://science.mq.edu.au/~fcassez/bib/papers/sv-comp-2017.pdf', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/pdf.svg\"\n\t     alt=\"Skink: Static Analysis of Programs in LLVM Intermediate Representation (Competition contribution) [pdf]\"\n       title=\"Paper\"\n\t     class=\"bibbase_icon\"\n         ><span class=\"bibbase_icon_text\">Paper</span></a>\n  &nbsp;\n  \n\n  \n  <a href=\"http://doi.org/10.1007/978-3-662-54580-5_27\"\n     onclick=\"log_download('cassez-sloane-roberts-pigram-suvanpong-dealedomarugn-skinkstaticanalysisofprogramsinllvmintermediaterepresentationcompetitioncontribution-2017', 'http://doi.org/10.1007/978-3-662-54580-5_27', event.ctrlKey)\"\n     class=\"bibbase doi link\">\n    <span>doi</span></a>\n  &nbsp;\n  \n\n  \n  <a href=\"//bibbase.org/network/publication/cassez-sloane-roberts-pigram-suvanpong-dealedomarugn-skinkstaticanalysisofprogramsinllvmintermediaterepresentationcompetitioncontribution-2017\"\n     class=\"bibbase bibbase_page link\">link</a>\n  &nbsp;\n  \n\n  <a href=\"#\"\n     onclick=\"showBib(event); return false;\"\n     class=\"bibbase bibtex link\">bibtex\n    <i class=\"fa fa-caret-down\"></i></a>\n\n  \n  &nbsp;\n  <a class=\"bibbase_abstract_link bibbase link\"\n     href=\"#\"\n     onclick=\"showAbstract(event); return false;\">\n    abstract <i class=\"fa fa-caret-down\"></i></a>\n  \n\n  \n  &nbsp;\n  <span class=\"bibbase_stats_paper\" style=\"color: #777;\">\n    <span>2 downloads</span>\n  </span>\n  \n\n  <!-- <a class=\"bibbase read link hidden\" -->\n  <!--    href=\"javascript:toggleRead('cassez-sloane-roberts-pigram-suvanpong-dealedomarugn-skinkstaticanalysisofprogramsinllvmintermediaterepresentationcompetitioncontribution-2017')\" -->\n  <!--    title=\"Marking this paper as read adds it to your library on BibBase.\" -->\n  <!--    > -->\n  <!--   <i class=\"fa fa-check\"></i>&nbsp; -->\n  <!--   <span>mark as read</span> -->\n  <!-- </a> -->\n\n  &nbsp;\n  \n  \n  \n  \n  \n  \n\n</span>\n\n<div class=\"well well-small bibbase\" data-type=\"bibtex\"\n     style=\"display:none\">\n  <pre style=\"white-space: pre-wrap;\">@inproceedings{tacas-17,\nauthor    = {Franck Cassez\nand {Anthony M.} Sloane\nand Matthew Roberts\nand Matthew Pigram\nand Pongsak Suvanpong\nand Pablo Gonz{\\&#x27;{a}}lez de Aledo Marug{\\&#x27;{a}}n},\n  title     = {Skink: Static Analysis of Programs in LLVM Intermediate Representation (Competition contribution)},\n  booktitle = {Tools and Algorithms for the Construction and Analysis of Systems\n               - 23rd International Conference, {TACAS} 2017, Held as Part of the\n               European Joint Conferences on Theory and Practice of Software, {ETAPS}\n               2017, Uppsala, Sweden, April 22-29, 2017. Proceedings},\n  \n pages     = {380--384},\n  year      = {2017},\n  url       = {https://doi.org/10.1007/978-3-662-54580-5_27},\n  doi       = {10.1007/978-3-662-54580-5_27},\n  publisher = springv,\n  xvolume = 10206,\n  series    = lncs,\n  mywebpage = {soft-verif},\n  keywords = {refinement, software verification},\n  category = {soft-verif},\n  show = {},\n  xxnote={forthcoming},\n  urlpaper = {papers/sv-comp-2017.pdf},\n  abstract = {Skink is a static analysis tool that analyses the LLVM intermediate representation (LLVM-IR)\nof a program source code.\nThe analysis consists of checking whether there is a feasible execution that can reach a\n designated error block in the LLVM-IR.\nThe result of a program analysis is &#x60;&#x60;correct&#x27;&#x27; if the error block is not reachable,\n&#x60;&#x60;incorrect&#x27;&#x27; if the error block is reachable, or &#x60;&#x60;inconclusive&#x27;&#x27; if the status of the program could not be determined.\nIn this paper, we introduce Skink V2.0 to analyse single and multi-threaded C programs.},\n    Type = {A - International Conferences},\n}\n\n\n\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n%%% 2016\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n</pre>\n</div>\n\n\n<div class=\"well well-small bibbase\" data-type=\"abstract\"\n     style=\"display:none\">\n  Skink is a static analysis tool that analyses the LLVM intermediate representation (LLVM-IR) of a program source code. The analysis consists of checking whether there is a feasible execution that can reach a designated error block in the LLVM-IR. The result of a program analysis is ``correct'' if the error block is not reachable, ``incorrect'' if the error block is reachable, or ``inconclusive'' if the status of the program could not be determined. In this paper, we introduce Skink V2.0 to analyse single and multi-threaded C programs.\n</div>\n\n\n</div>\n\n\n\n\n\n    </div>\n  </div>\n\n  <div class=\"bibbase_group_whole\" id=\"group_2015\">\n    <div class=\"bibbase_group\"\n      onclick=\"toggleGroup('group_2015')\"\n      onkeypress=\"toggleGroup('group_2015')\"\n      tabindex=\"0\">\n      <i class=\"fa fa-angle-down bibbase_group_head_icon\"></i>&nbsp;\n      <span>2015</span>\n      <span class=\"bibbase_group_count\">\n        \n        (2)\n        \n      </span>\n    </div>\n    <div class=\"bibbase_group_body\">\n      \n  \n  <div class=\"bibbase_paper\" id=\"cassez-ziegler-verificationofconcurrentprogramsusingtraceabstractionrefinement-2015\">\n  <span class=\"bibbase_paper_titleauthoryear\">\n\n  \n  <span class=\"bibbase_paper_title\">\n  \n  \n  \n  <a href=\"http://science.mq.edu.au/~fcassez/bib/papers/lpar-2015.pdf\"\n     onclick=\"return trackOutboundLink('publications', 'click', 'cassez-ziegler-verificationofconcurrentprogramsusingtraceabstractionrefinement-2015', 'http://science.mq.edu.au/~fcassez/bib/papers/lpar-2015.pdf', event);\">\n    Verification of Concurrent Programs Using Trace Abstraction Refinement.\n  </a>\n  \n  \n  \n</span>\n\n  <span class=\"bibbase_paper_author\">\n  <a class=\"bibbase author link\" href=\"http://science.mq.edu.au/~fcassez/software-verif.html\">Cassez, F.</a>;  and Ziegler, F.\n</span>\n\n  \n\n</span>\n\n  In Davis, M.; Fehnker, A.; McIver, A.;  and Voronkov, A., editor(s), <i>Logic for Programming, Artificial Intelligence, and Reasoning - 20th International Conference, LPAR-20 2015, Suva, Fiji, November 24-28, 2015, Proceedings</i>, volume 9450, of <i>Lecture Notes in Computer Science</i>, pages 233–248,  2015. Springer\n  <span class=\"note\">LPAR Best paper award</span>\n\n<span class=\"bibbase_note\"></span>\n\n<br class=\"bibbase_paper_content\"/>\n\n<span class=\"bibbase_paper_content dontprint\">\n\n  \n  <a href=\"http://science.mq.edu.au/~fcassez/bib/papers/lpar-2015.pdf\"\n     onclick=\"log_download('cassez-ziegler-verificationofconcurrentprogramsusingtraceabstractionrefinement-2015', 'http://science.mq.edu.au/~fcassez/bib/papers/lpar-2015.pdf', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/pdf.svg\"\n\t     alt=\"Verification of Concurrent Programs Using Trace Abstraction Refinement [pdf]\"\n       title=\"Paper\"\n\t     class=\"bibbase_icon\"\n         ><span class=\"bibbase_icon_text\">Paper</span></a>\n  &nbsp;\n  \n  <a href=\"http://science.mq.edu.au/~fcassez/bib/papers/slides-lpar-2015.pdf\"\n     onclick=\"log_download('cassez-ziegler-verificationofconcurrentprogramsusingtraceabstractionrefinement-2015', 'http://science.mq.edu.au/~fcassez/bib/papers/slides-lpar-2015.pdf', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/pdf.svg\"\n\t     alt=\"Verification of Concurrent Programs Using Trace Abstraction Refinement [pdf]\"\n       title=\"Slides\"\n\t     class=\"bibbase_icon\"\n         ><span class=\"bibbase_icon_text\">Slides</span></a>\n  &nbsp;\n  \n\n  \n  <a href=\"http://doi.org/10.1007/978-3-662-48899-7_17\"\n     onclick=\"log_download('cassez-ziegler-verificationofconcurrentprogramsusingtraceabstractionrefinement-2015', 'http://doi.org/10.1007/978-3-662-48899-7_17', event.ctrlKey)\"\n     class=\"bibbase doi link\">\n    <span>doi</span></a>\n  &nbsp;\n  \n\n  \n  <a href=\"//bibbase.org/network/publication/cassez-ziegler-verificationofconcurrentprogramsusingtraceabstractionrefinement-2015\"\n     class=\"bibbase bibbase_page link\">link</a>\n  &nbsp;\n  \n\n  <a href=\"#\"\n     onclick=\"showBib(event); return false;\"\n     class=\"bibbase bibtex link\">bibtex\n    <i class=\"fa fa-caret-down\"></i></a>\n\n  \n  &nbsp;\n  <a class=\"bibbase_abstract_link bibbase link\"\n     href=\"#\"\n     onclick=\"showAbstract(event); return false;\">\n    abstract <i class=\"fa fa-caret-down\"></i></a>\n  \n\n  \n  &nbsp;\n  <span class=\"bibbase_stats_paper\" style=\"color: #777;\">\n    <span>1 download</span>\n  </span>\n  \n\n  <!-- <a class=\"bibbase read link hidden\" -->\n  <!--    href=\"javascript:toggleRead('cassez-ziegler-verificationofconcurrentprogramsusingtraceabstractionrefinement-2015')\" -->\n  <!--    title=\"Marking this paper as read adds it to your library on BibBase.\" -->\n  <!--    > -->\n  <!--   <i class=\"fa fa-check\"></i>&nbsp; -->\n  <!--   <span>mark as read</span> -->\n  <!-- </a> -->\n\n  &nbsp;\n  \n  \n\n</span>\n\n<div class=\"well well-small bibbase\" data-type=\"bibtex\"\n     style=\"display:none\">\n  <pre style=\"white-space: pre-wrap;\">@inproceedings{cassez-lpar-2015,\n  author    = {Franck Cassez and\n               Frowin Ziegler},\n                editor    = {Martin Davis and\n               Ansgar Fehnker and\n               Annabelle McIver and\n               Andrei Voronkov},\n  title     = {Verification of Concurrent Programs Using Trace Abstraction Refinement},\n  booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning - 20th\n               International Conference, {LPAR-20} 2015, Suva, Fiji, November 24-28,\n               2015, Proceedings},\n  pages     = {233--248},\n  year      = {2015},\n  series    = {Lecture Notes in Computer Science},\n  volume    = {9450},\n  publisher = {Springer},\n  year      = {2015},\n  url       = {http://dx.doi.org/10.1007/978-3-662-48899-7_17},\n  mywebpage = {soft-verif},\n  category = {soft-verif},\n  isbn      = {978-3-662-48898-0},\n  doi       = {10.1007/978-3-662-48899-7_17},\n  show = {},\n  note = {LPAR Best paper award},\n  urlpaper = {papers/lpar-2015.pdf},\n    urlslides = {papers/slides-lpar-2015.pdf},\n  abstract = {Verifying concurrent programs is notoriously hard due to the state explosion problem: (1) the data state space can be very large as the variables can range over very large sets, and (2) the control state space is the Cartesian product of the control state space of the concurrent com- ponents and thus grows exponentially in the number of components. On the one hand, the most successful approaches to address the control state explosion problem are based on assume-guarantee reasoning or model-checking coupled with partial order reduction. On the other hand, the most successful techniques to address the data space explosion problem for sequential programs verification are based on the abstraction/refine- ment paradigm which consists in refining an abstract over-approximation of a program via predicate refinement. In this paper, we show that we can combine partial order reduction techniques with trace abstraction refinement. We apply our approach to standard benchmarks and show that it matches current state-of-the-art analysis techniques.},\n  Type = {B - International Conferences},\n}\n\n</pre>\n</div>\n\n\n<div class=\"well well-small bibbase\" data-type=\"abstract\"\n     style=\"display:none\">\n  Verifying concurrent programs is notoriously hard due to the state explosion problem: (1) the data state space can be very large as the variables can range over very large sets, and (2) the control state space is the Cartesian product of the control state space of the concurrent com- ponents and thus grows exponentially in the number of components. On the one hand, the most successful approaches to address the control state explosion problem are based on assume-guarantee reasoning or model-checking coupled with partial order reduction. On the other hand, the most successful techniques to address the data space explosion problem for sequential programs verification are based on the abstraction/refine- ment paradigm which consists in refining an abstract over-approximation of a program via predicate refinement. In this paper, we show that we can combine partial order reduction techniques with trace abstraction refinement. We apply our approach to standard benchmarks and show that it matches current state-of-the-art analysis techniques.\n</div>\n\n\n</div>\n\n\n  <div class=\"bibbase_paper\" id=\"cassez-matsuoka-pierzchalski-smyth-perentiemodulartracerefinementandselectivevaluetrackingcompetitioncontribution-2015\">\n  <span class=\"bibbase_paper_titleauthoryear\">\n\n  \n  <span class=\"bibbase_paper_title\">\n  \n  \n  \n  <a href=\"http://science.mq.edu.au/~fcassez/bib/papers/sv-comp-2015.pdf\"\n     onclick=\"return trackOutboundLink('publications', 'click', 'cassez-matsuoka-pierzchalski-smyth-perentiemodulartracerefinementandselectivevaluetrackingcompetitioncontribution-2015', 'http://science.mq.edu.au/~fcassez/bib/papers/sv-comp-2015.pdf', event);\">\n    Perentie: Modular Trace Refinement and Selective Value Tracking - (Competition Contribution).\n  </a>\n  \n  \n  \n</span>\n\n  <span class=\"bibbase_paper_author\">\n  <a class=\"bibbase author link\" href=\"http://science.mq.edu.au/~fcassez/software-verif.html\">Cassez, F.</a>; Matsuoka, T.; Pierzchalski, E.;  and Smyth, N.\n</span>\n\n  \n\n</span>\n\n  In <i>Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings</i>, volume 9035, of <i>LNCS</i>, pages 439–442,  2015. Springer\n  <span class=\"note\"></span>\n\n<span class=\"bibbase_note\"></span>\n\n<br class=\"bibbase_paper_content\"/>\n\n<span class=\"bibbase_paper_content dontprint\">\n\n  \n  <a href=\"http://science.mq.edu.au/~fcassez/bib/papers/sv-comp-2015.pdf\"\n     onclick=\"log_download('cassez-matsuoka-pierzchalski-smyth-perentiemodulartracerefinementandselectivevaluetrackingcompetitioncontribution-2015', 'http://science.mq.edu.au/~fcassez/bib/papers/sv-comp-2015.pdf', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/pdf.svg\"\n\t     alt=\"Perentie: Modular Trace Refinement and Selective Value Tracking - (Competition Contribution) [pdf]\"\n       title=\"Paper\"\n\t     class=\"bibbase_icon\"\n         ><span class=\"bibbase_icon_text\">Paper</span></a>\n  &nbsp;\n  \n\n  \n  <a href=\"http://doi.org/10.1007/978-3-662-46681-0_39\"\n     onclick=\"log_download('cassez-matsuoka-pierzchalski-smyth-perentiemodulartracerefinementandselectivevaluetrackingcompetitioncontribution-2015', 'http://doi.org/10.1007/978-3-662-46681-0_39', event.ctrlKey)\"\n     class=\"bibbase doi link\">\n    <span>doi</span></a>\n  &nbsp;\n  \n\n  \n  <a href=\"//bibbase.org/network/publication/cassez-matsuoka-pierzchalski-smyth-perentiemodulartracerefinementandselectivevaluetrackingcompetitioncontribution-2015\"\n     class=\"bibbase bibbase_page link\">link</a>\n  &nbsp;\n  \n\n  <a href=\"#\"\n     onclick=\"showBib(event); return false;\"\n     class=\"bibbase bibtex link\">bibtex\n    <i class=\"fa fa-caret-down\"></i></a>\n\n  \n  &nbsp;\n  <a class=\"bibbase_abstract_link bibbase link\"\n     href=\"#\"\n     onclick=\"showAbstract(event); return false;\">\n    abstract <i class=\"fa fa-caret-down\"></i></a>\n  \n\n  \n\n  <!-- <a class=\"bibbase read link hidden\" -->\n  <!--    href=\"javascript:toggleRead('cassez-matsuoka-pierzchalski-smyth-perentiemodulartracerefinementandselectivevaluetrackingcompetitioncontribution-2015')\" -->\n  <!--    title=\"Marking this paper as read adds it to your library on BibBase.\" -->\n  <!--    > -->\n  <!--   <i class=\"fa fa-check\"></i>&nbsp; -->\n  <!--   <span>mark as read</span> -->\n  <!-- </a> -->\n\n  &nbsp;\n  \n  \n  \n  \n  \n  \n\n</span>\n\n<div class=\"well well-small bibbase\" data-type=\"bibtex\"\n     style=\"display:none\">\n  <pre style=\"white-space: pre-wrap;\">@inproceedings{tacas-15,\nauthor    = {Franck Cassez and\n               Takashi Matsuoka and\n               Edward Pierzchalski and\n               Nathan Smyth},\n  title     = {Perentie: Modular Trace Refinement and Selective Value Tracking -\n               (Competition Contribution)},\n  booktitle = {Tools and Algorithms for the Construction and Analysis of Systems\n               - 21st International Conference, {TACAS} 2015, Held as Part of the\n               European Joint Conferences on Theory and Practice of Software, {ETAPS}\n               2015, London, UK, April 11-18, 2015. Proceedings},\n  pages     = {439--442},\n  year      = {2015},\n  url       = {http://dx.doi.org/10.1007/978-3-662-46681-0_39},\n  doi       = {10.1007/978-3-662-46681-0_39},\n  publisher = springv,\n  volume = 9035,\n  series    = lncs,\n  mywebpage = {soft-verif},\n  keywords = {refinement, software verification},\n  category = {soft-verif},\n  show = {},\n  urlpaper = {papers/sv-comp-2015.pdf},\n  abstract = {Perentie is a software analysis tool based on iterative refinement of trace abstraction:\n  if the refinement process terminates, the program is either declared correct or a counterexample is\n  provided and the program is incorrect.},\n    Type = {B - International Conferences},\n\n}\n\n\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n%%% 2014\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n\n</pre>\n</div>\n\n\n<div class=\"well well-small bibbase\" data-type=\"abstract\"\n     style=\"display:none\">\n  Perentie is a software analysis tool based on iterative refinement of trace abstraction: if the refinement process terminates, the program is either declared correct or a counterexample is provided and the program is incorrect.\n</div>\n\n\n</div>\n\n\n\n\n\n    </div>\n  </div>\n\n  <div class=\"bibbase_group_whole\" id=\"group_2014\">\n    <div class=\"bibbase_group\"\n      onclick=\"toggleGroup('group_2014')\"\n      onkeypress=\"toggleGroup('group_2014')\"\n      tabindex=\"0\">\n      <i class=\"fa fa-angle-down bibbase_group_head_icon\"></i>&nbsp;\n      <span>2014</span>\n      <span class=\"bibbase_group_count\">\n        \n        (1)\n        \n      </span>\n    </div>\n    <div class=\"bibbase_group_body\">\n      \n  \n  <div class=\"bibbase_paper\" id=\"cassez-mller-burnett-summarybasedinterproceduralanalysisviamodulartracerefinement-2014\">\n  <span class=\"bibbase_paper_titleauthoryear\">\n\n  \n  <span class=\"bibbase_paper_title\">\n  \n  \n  \n  <a href=\"http://dx.doi.org/10.4230/LIPIcs.FSTTCS.2014.545\"\n     onclick=\"return trackOutboundLink('publications', 'click', 'cassez-mller-burnett-summarybasedinterproceduralanalysisviamodulartracerefinement-2014', 'http://dx.doi.org/10.4230/LIPIcs.FSTTCS.2014.545', event);\">\n    Summary-Based Inter-Procedural Analysis via Modular Trace Refinement.\n  </a>\n  \n  \n  \n</span>\n\n  <span class=\"bibbase_paper_author\">\n  <a class=\"bibbase author link\" href=\"http://science.mq.edu.au/~fcassez/software-verif.html\">Cassez, F.</a>; Müller, C.;  and Burnett, K.\n</span>\n\n  \n\n</span>\n\n  In <i>34th International Conference on Foundation of Software Technology and Theoretical Computer Science, FSTTCS 2014, December 15-17, 2014, New Delhi, India</i>, pages 545–556,  2014. \n  <span class=\"note\"></span>\n\n<span class=\"bibbase_note\"></span>\n\n<br class=\"bibbase_paper_content\"/>\n\n<span class=\"bibbase_paper_content dontprint\">\n\n  \n  <a href=\"http://dx.doi.org/10.4230/LIPIcs.FSTTCS.2014.545\"\n     onclick=\"log_download('cassez-mller-burnett-summarybasedinterproceduralanalysisviamodulartracerefinement-2014', 'http://dx.doi.org/10.4230/LIPIcs.FSTTCS.2014.545', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/link.svg\"\n\t     alt=\"Summary-Based Inter-Procedural Analysis via Modular Trace Refinement [link]\"\n       title=\" link\"\n\t     class=\"bibbase_icon\"\n         ><span class=\"bibbase_icon_text\"> link</span></a>\n  &nbsp;\n  \n\n  \n  <a href=\"http://doi.org/10.4230/LIPIcs.FSTTCS.2014.545\"\n     onclick=\"log_download('cassez-mller-burnett-summarybasedinterproceduralanalysisviamodulartracerefinement-2014', 'http://doi.org/10.4230/LIPIcs.FSTTCS.2014.545', event.ctrlKey)\"\n     class=\"bibbase doi link\">\n    <span>doi</span></a>\n  &nbsp;\n  \n\n  \n  <a href=\"//bibbase.org/network/publication/cassez-mller-burnett-summarybasedinterproceduralanalysisviamodulartracerefinement-2014\"\n     class=\"bibbase bibbase_page link\">link</a>\n  &nbsp;\n  \n\n  <a href=\"#\"\n     onclick=\"showBib(event); return false;\"\n     class=\"bibbase bibtex link\">bibtex\n    <i class=\"fa fa-caret-down\"></i></a>\n\n  \n  &nbsp;\n  <a class=\"bibbase_abstract_link bibbase link\"\n     href=\"#\"\n     onclick=\"showAbstract(event); return false;\">\n    abstract <i class=\"fa fa-caret-down\"></i></a>\n  \n\n  \n\n  <!-- <a class=\"bibbase read link hidden\" -->\n  <!--    href=\"javascript:toggleRead('cassez-mller-burnett-summarybasedinterproceduralanalysisviamodulartracerefinement-2014')\" -->\n  <!--    title=\"Marking this paper as read adds it to your library on BibBase.\" -->\n  <!--    > -->\n  <!--   <i class=\"fa fa-check\"></i>&nbsp; -->\n  <!--   <span>mark as read</span> -->\n  <!-- </a> -->\n\n  &nbsp;\n  \n  \n  \n  \n  \n  \n  \n  \n\n</span>\n\n<div class=\"well well-small bibbase\" data-type=\"bibtex\"\n     style=\"display:none\">\n  <pre style=\"white-space: pre-wrap;\">@inproceedings{fsttcs-14,\n  author    = {Franck Cassez and\n               Christian Müller and\n               Karla Burnett},\n  title     = {Summary-Based Inter-Procedural Analysis via Modular Trace Refinement},\n  booktitle = {34th International Conference on Foundation of Software Technology\n               and Theoretical Computer Science, {FSTTCS} 2014, December 15-17, 2014,\n               New Delhi, India},\n  pages     = {545--556},\n  year      = {2014},\n  mywebpage = {soft-verif},\n  category = {Software verification},\n  keywords = {trace refinement, software verification, Hoare logic},\n  url_link       = {http://dx.doi.org/10.4230/LIPIcs.FSTTCS.2014.545},\n  doi       = {10.4230/LIPIcs.FSTTCS.2014.545},\n  abstract = {We propose a generalisation of trace refinement for the verification of inter-procedural programs.\n  Our method is a top-down modular, summary-based approach, and analyses inter-procedural programs by building function summaries on-demand\n  and improving the summaries each time a function is analysed. Our method is sound, and complete relative to the existence of a\n  modular Hoare proof for a non-recursive program. We have implemented a prototype analyser that demonstrates the\n  main features of our approach and yields promising results.\n  },\n  Type = {B - International Conferences},\n}\n\n\n</pre>\n</div>\n\n\n<div class=\"well well-small bibbase\" data-type=\"abstract\"\n     style=\"display:none\">\n  We propose a generalisation of trace refinement for the verification of inter-procedural programs. Our method is a top-down modular, summary-based approach, and analyses inter-procedural programs by building function summaries on-demand and improving the summaries each time a function is analysed. Our method is sound, and complete relative to the existence of a modular Hoare proof for a non-recursive program. We have implemented a prototype analyser that demonstrates the main features of our approach and yields promising results. \n</div>\n\n\n</div>\n\n\n\n\n\n    </div>\n  </div>\n\n  <div class=\"bibbase_group_whole\" id=\"group_2013\">\n    <div class=\"bibbase_group\"\n      onclick=\"toggleGroup('group_2013')\"\n      onkeypress=\"toggleGroup('group_2013')\"\n      tabindex=\"0\">\n      <i class=\"fa fa-angle-down bibbase_group_head_icon\"></i>&nbsp;\n      <span>2013</span>\n      <span class=\"bibbase_group_count\">\n        \n        (1)\n        \n      </span>\n    </div>\n    <div class=\"bibbase_group_body\">\n      \n  \n  <div class=\"bibbase_paper\" id=\"biallas-olesen-cassez-huuck-ptrtrackerpragmaticpointeranalysis-2013\">\n  <span class=\"bibbase_paper_titleauthoryear\">\n\n  \n  <span class=\"bibbase_paper_title\">\n  \n  \n  \n  <a href=\"http://science.mq.edu.au/~fcassez/bib/papers/scam-2013.pdf\"\n     onclick=\"return trackOutboundLink('publications', 'click', 'biallas-olesen-cassez-huuck-ptrtrackerpragmaticpointeranalysis-2013', 'http://science.mq.edu.au/~fcassez/bib/papers/scam-2013.pdf', event);\">\n    PtrTracker: Pragmatic pointer analysis.\n  </a>\n  \n  \n  \n</span>\n\n  <span class=\"bibbase_paper_author\">\n  Biallas, S.; Olesen, M. C.; <a class=\"bibbase author link\" href=\"http://science.mq.edu.au/~fcassez/software-verif.html\">Cassez, F.</a>;  and Huuck, R.\n</span>\n\n  \n\n</span>\n\n  In <i>13th IEEE International Working Conference on Source Code Analysis and Manipulation, SCAM 2013, Eindhoven, Netherlands, September 22-23, 2013</i>, pages 69–73,  2013. IEEE Computer Society\n  <span class=\"note\"></span>\n\n<span class=\"bibbase_note\"></span>\n\n<br class=\"bibbase_paper_content\"/>\n\n<span class=\"bibbase_paper_content dontprint\">\n\n  \n  <a href=\"http://science.mq.edu.au/~fcassez/bib/papers/scam-2013.pdf\"\n     onclick=\"log_download('biallas-olesen-cassez-huuck-ptrtrackerpragmaticpointeranalysis-2013', 'http://science.mq.edu.au/~fcassez/bib/papers/scam-2013.pdf', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/pdf.svg\"\n\t     alt=\"PtrTracker: Pragmatic pointer analysis [pdf]\"\n       title=\"Paper\"\n\t     class=\"bibbase_icon\"\n         ><span class=\"bibbase_icon_text\">Paper</span></a>\n  &nbsp;\n  \n  <a href=\"http://dx.doi.org/10.1109/SCAM.2013.6648186\"\n     onclick=\"log_download('biallas-olesen-cassez-huuck-ptrtrackerpragmaticpointeranalysis-2013', 'http://dx.doi.org/10.1109/SCAM.2013.6648186', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/link.svg\"\n\t     alt=\"PtrTracker: Pragmatic pointer analysis [link]\"\n       title=\" link\"\n\t     class=\"bibbase_icon\"\n         ><span class=\"bibbase_icon_text\"> link</span></a>\n  &nbsp;\n  \n\n  \n  <a href=\"http://doi.org/10.1109/SCAM.2013.6648186\"\n     onclick=\"log_download('biallas-olesen-cassez-huuck-ptrtrackerpragmaticpointeranalysis-2013', 'http://doi.org/10.1109/SCAM.2013.6648186', event.ctrlKey)\"\n     class=\"bibbase doi link\">\n    <span>doi</span></a>\n  &nbsp;\n  \n\n  \n  <a href=\"//bibbase.org/network/publication/biallas-olesen-cassez-huuck-ptrtrackerpragmaticpointeranalysis-2013\"\n     class=\"bibbase bibbase_page link\">link</a>\n  &nbsp;\n  \n\n  <a href=\"#\"\n     onclick=\"showBib(event); return false;\"\n     class=\"bibbase bibtex link\">bibtex\n    <i class=\"fa fa-caret-down\"></i></a>\n\n  \n  &nbsp;\n  <a class=\"bibbase_abstract_link bibbase link\"\n     href=\"#\"\n     onclick=\"showAbstract(event); return false;\">\n    abstract <i class=\"fa fa-caret-down\"></i></a>\n  \n\n  \n\n  <!-- <a class=\"bibbase read link hidden\" -->\n  <!--    href=\"javascript:toggleRead('biallas-olesen-cassez-huuck-ptrtrackerpragmaticpointeranalysis-2013')\" -->\n  <!--    title=\"Marking this paper as read adds it to your library on BibBase.\" -->\n  <!--    > -->\n  <!--   <i class=\"fa fa-check\"></i>&nbsp; -->\n  <!--   <span>mark as read</span> -->\n  <!-- </a> -->\n\n  &nbsp;\n  \n  \n  \n  \n  \n  \n  \n  \n\n</span>\n\n<div class=\"well well-small bibbase\" data-type=\"bibtex\"\n     style=\"display:none\">\n  <pre style=\"white-space: pre-wrap;\">@inproceedings{scam-2013,\n  author    = {Sebastian Biallas and\n               Mads Chr. Olesen and\n               Franck Cassez and\n               Ralf Huuck},\n  title     = {PtrTracker: Pragmatic pointer analysis},\n  booktitle = {13th {IEEE} International Working Conference on Source Code Analysis\n               and Manipulation, {SCAM} 2013, Eindhoven, Netherlands, September 22-23,\n               2013},\n  pages     = {69--73},\n  year      = {2013},\n  publisher = {{IEEE} Computer Society},\n  urlpaper = {papers/scam-2013.pdf},\n  url_link       = {http://dx.doi.org/10.1109/SCAM.2013.6648186},\n  doi       = {10.1109/SCAM.2013.6648186},\n  keywords = {Software verification, pointers, static analysis},\n  mywebpage = {soft-verif},\n  category = {Software verification},\n  abstract = {\n  Static program analysis for bug detection in industrial C/C++ code has many challenges. One of them is to analyze pointer and pointer structures efficiently. While there has been much research into various aspects of pointer analysis either for compiler optimization or for verification tasks, both classical categories are not optimized for bug detection, where speed and precision are important, but soundness (no missed bugs) and completeness (no false positives) do not necessarily need to be guaranteed.\n  },\n    Type = {B - International Conferences},\n}\n\n</pre>\n</div>\n\n\n<div class=\"well well-small bibbase\" data-type=\"abstract\"\n     style=\"display:none\">\n  Static program analysis for bug detection in industrial C/C++ code has many challenges. One of them is to analyze pointer and pointer structures efficiently. While there has been much research into various aspects of pointer analysis either for compiler optimization or for verification tasks, both classical categories are not optimized for bug detection, where speed and precision are important, but soundness (no missed bugs) and completeness (no false positives) do not necessarily need to be guaranteed. \n</div>\n\n\n</div>\n\n\n\n\n\n    </div>\n  </div>\n\n  <div class=\"bibbase_group_whole\" id=\"group_2012\">\n    <div class=\"bibbase_group\"\n      onclick=\"toggleGroup('group_2012')\"\n      onkeypress=\"toggleGroup('group_2012')\"\n      tabindex=\"0\">\n      <i class=\"fa fa-angle-down bibbase_group_head_icon\"></i>&nbsp;\n      <span>2012</span>\n      <span class=\"bibbase_group_count\">\n        \n        (2)\n        \n      </span>\n    </div>\n    <div class=\"bibbase_group_body\">\n      \n  \n  <div class=\"bibbase_paper\" id=\"cassez-hansen-olesen-whatisatiminganomaly-2012\">\n  <span class=\"bibbase_paper_titleauthoryear\">\n\n  \n  <span class=\"bibbase_paper_title\">\n  \n  \n  \n  <a href=\"http://science.mq.edu.au/~fcassez/bib/papers/wcet-2012.pdf\"\n     onclick=\"return trackOutboundLink('publications', 'click', 'cassez-hansen-olesen-whatisatiminganomaly-2012', 'http://science.mq.edu.au/~fcassez/bib/papers/wcet-2012.pdf', event);\">\n    What is a Timing Anomaly?.\n  </a>\n  \n  \n  \n</span>\n\n  <span class=\"bibbase_paper_author\">\n  <a class=\"bibbase author link\" href=\"http://science.mq.edu.au/~fcassez/software-verif.html\">Cassez, F.</a>; Hansen, R. R.;  and Olesen, M. C.\n</span>\n\n  \n\n</span>\n\n  In <i>12th International Workshop on Worst-Case Execution Time Analysis, WCET 2012, July 10, 2012, Pisa, Italy</i>, volume 23, of <i>OASICS</i>, pages 1-12,  2012. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik\n  <span class=\"note\"></span>\n\n<span class=\"bibbase_note\"></span>\n\n<br class=\"bibbase_paper_content\"/>\n\n<span class=\"bibbase_paper_content dontprint\">\n\n  \n  <a href=\"http://science.mq.edu.au/~fcassez/bib/papers/wcet-2012.pdf\"\n     onclick=\"log_download('cassez-hansen-olesen-whatisatiminganomaly-2012', 'http://science.mq.edu.au/~fcassez/bib/papers/wcet-2012.pdf', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/pdf.svg\"\n\t     alt=\"What is a Timing Anomaly? [pdf]\"\n       title=\"Paper\"\n\t     class=\"bibbase_icon\"\n         ><span class=\"bibbase_icon_text\">Paper</span></a>\n  &nbsp;\n  \n  <a href=\"http://dx.doi.org/10.4230/OASIcs.WCET.2012.1\"\n     onclick=\"log_download('cassez-hansen-olesen-whatisatiminganomaly-2012', 'http://dx.doi.org/10.4230/OASIcs.WCET.2012.1', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/link.svg\"\n\t     alt=\"What is a Timing Anomaly? [link]\"\n       title=\" link\"\n\t     class=\"bibbase_icon\"\n         ><span class=\"bibbase_icon_text\"> link</span></a>\n  &nbsp;\n  \n\n  \n\n  \n  <a href=\"//bibbase.org/network/publication/cassez-hansen-olesen-whatisatiminganomaly-2012\"\n     class=\"bibbase bibbase_page link\">link</a>\n  &nbsp;\n  \n\n  <a href=\"#\"\n     onclick=\"showBib(event); return false;\"\n     class=\"bibbase bibtex link\">bibtex\n    <i class=\"fa fa-caret-down\"></i></a>\n\n  \n  &nbsp;\n  <a class=\"bibbase_abstract_link bibbase link\"\n     href=\"#\"\n     onclick=\"showAbstract(event); return false;\">\n    abstract <i class=\"fa fa-caret-down\"></i></a>\n  \n\n  \n\n  <!-- <a class=\"bibbase read link hidden\" -->\n  <!--    href=\"javascript:toggleRead('cassez-hansen-olesen-whatisatiminganomaly-2012')\" -->\n  <!--    title=\"Marking this paper as read adds it to your library on BibBase.\" -->\n  <!--    > -->\n  <!--   <i class=\"fa fa-check\"></i>&nbsp; -->\n  <!--   <span>mark as read</span> -->\n  <!-- </a> -->\n\n  &nbsp;\n  \n  \n  \n  \n\n</span>\n\n<div class=\"well well-small bibbase\" data-type=\"bibtex\"\n     style=\"display:none\">\n  <pre style=\"white-space: pre-wrap;\">@inproceedings{wcet-12,\n  author    = {Franck Cassez and\n               René Rydhof Hansen and\n               Mads Chr. Olesen},\n  title     = {What is a Timing Anomaly?},\n  booktitle = {12th International Workshop on Worst-Case Execution Time\n               Analysis, WCET 2012, July 10, 2012, Pisa, Italy},\n  year      = {2012},\n  pages     = {1-12},\n  urlpaper = {papers/wcet-2012.pdf},\n  url_link        = {http://dx.doi.org/10.4230/OASIcs.WCET.2012.1},\n  abstract = {Timing anomalies make worst-case execution time analysis much harder, because the analysis will have to consider all local choices. It has been widely recognised that certain hardware features are timing anomalous, while others are not. However, defining formally what a timing anomaly is, has been difficult. We examine previous definitions of timing anomalies, and identify examples where they do not align with common observations. We then provide a definition for consistently slower hardware traces that can be used to define timing anomalies and aligns with common observations.},\n  category= {wcet},\n  mywebpage = {soft-verif,wcet},\n  keywords = {wcet},\n   publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik},\n  series    = {OASICS},\n  volume    = {23},\n        Type = {B - International Conferences},\n\n}\n\n\n</pre>\n</div>\n\n\n<div class=\"well well-small bibbase\" data-type=\"abstract\"\n     style=\"display:none\">\n  Timing anomalies make worst-case execution time analysis much harder, because the analysis will have to consider all local choices. It has been widely recognised that certain hardware features are timing anomalous, while others are not. However, defining formally what a timing anomaly is, has been difficult. We examine previous definitions of timing anomalies, and identify examples where they do not align with common observations. We then provide a definition for consistently slower hardware traces that can be used to define timing anomalies and aligns with common observations.\n</div>\n\n\n</div>\n\n\n  <div class=\"bibbase_paper\" id=\"bradley-cassez-fehnker-givenwilson-huuck-highperformancestaticanalysisforindustry-2012\">\n  <span class=\"bibbase_paper_titleauthoryear\">\n\n  \n  <span class=\"bibbase_paper_title\">\n  \n  \n  \n  <a href=\"http://science.mq.edu.au/~fcassez/bib/papers/tapas-2012.pdf\"\n     onclick=\"return trackOutboundLink('publications', 'click', 'bradley-cassez-fehnker-givenwilson-huuck-highperformancestaticanalysisforindustry-2012', 'http://science.mq.edu.au/~fcassez/bib/papers/tapas-2012.pdf', event);\">\n    High Performance Static Analysis for Industry.\n  </a>\n  \n  \n  \n</span>\n\n  <span class=\"bibbase_paper_author\">\n  Bradley, M.; <a class=\"bibbase author link\" href=\"http://science.mq.edu.au/~fcassez/software-verif.html\">Cassez, F.</a>; Fehnker, A.; Given-Wilson, T.;  and Huuck, R.\n</span>\n\n  \n\n</span>\n\n  <i>Electr. Notes Theor. Comput. Sci.</i>, 289: 3-14.  2012.\n  <span class=\"note\"></span>\n\n<span class=\"bibbase_note\"></span>\n\n<br class=\"bibbase_paper_content\"/>\n\n<span class=\"bibbase_paper_content dontprint\">\n\n  \n  <a href=\"http://science.mq.edu.au/~fcassez/bib/papers/tapas-2012.pdf\"\n     onclick=\"log_download('bradley-cassez-fehnker-givenwilson-huuck-highperformancestaticanalysisforindustry-2012', 'http://science.mq.edu.au/~fcassez/bib/papers/tapas-2012.pdf', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/pdf.svg\"\n\t     alt=\"High Performance Static Analysis for Industry [pdf]\"\n       title=\"Paper\"\n\t     class=\"bibbase_icon\"\n         ><span class=\"bibbase_icon_text\">Paper</span></a>\n  &nbsp;\n  \n  <a href=\"http://dx.doi.org/10.1016/j.entcs.2012.11.002\"\n     onclick=\"log_download('bradley-cassez-fehnker-givenwilson-huuck-highperformancestaticanalysisforindustry-2012', 'http://dx.doi.org/10.1016/j.entcs.2012.11.002', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/link.svg\"\n\t     alt=\"High Performance Static Analysis for Industry [link]\"\n       title=\"Link\"\n\t     class=\"bibbase_icon\"\n         ><span class=\"bibbase_icon_text\">Link</span></a>\n  &nbsp;\n  \n\n  \n\n  \n  <a href=\"//bibbase.org/network/publication/bradley-cassez-fehnker-givenwilson-huuck-highperformancestaticanalysisforindustry-2012\"\n     class=\"bibbase bibbase_page link\">link</a>\n  &nbsp;\n  \n\n  <a href=\"#\"\n     onclick=\"showBib(event); return false;\"\n     class=\"bibbase bibtex link\">bibtex\n    <i class=\"fa fa-caret-down\"></i></a>\n\n  \n  &nbsp;\n  <a class=\"bibbase_abstract_link bibbase link\"\n     href=\"#\"\n     onclick=\"showAbstract(event); return false;\">\n    abstract <i class=\"fa fa-caret-down\"></i></a>\n  \n\n  \n\n  <!-- <a class=\"bibbase read link hidden\" -->\n  <!--    href=\"javascript:toggleRead('bradley-cassez-fehnker-givenwilson-huuck-highperformancestaticanalysisforindustry-2012')\" -->\n  <!--    title=\"Marking this paper as read adds it to your library on BibBase.\" -->\n  <!--    > -->\n  <!--   <i class=\"fa fa-check\"></i>&nbsp; -->\n  <!--   <span>mark as read</span> -->\n  <!-- </a> -->\n\n  &nbsp;\n  \n  \n  \n  \n\n</span>\n\n<div class=\"well well-small bibbase\" data-type=\"bibtex\"\n     style=\"display:none\">\n  <pre style=\"white-space: pre-wrap;\">@article{tapas-12,\n  author    = {Mark Bradley and\n               Franck Cassez and\n               Ansgar Fehnker and\n               Thomas Given-Wilson and\n               Ralf Huuck},\n  title     = {High Performance Static Analysis for Industry},\n  journal   = {Electr. Notes Theor. Comput. Sci.},\n  volume    = {289},\n  year      = {2012},\n  pages     = {3-14},\n  urlpaper = {papers/tapas-2012.pdf},\n  ee        = {http://dx.doi.org/10.1016/j.entcs.2012.11.002},\n  bibsource = {DBLP, http://dblp.uni-trier.de},\n  mywebpage = {soft-verif},\n  keywords = {software verification},\n  abstract = {\n  Static source code analysis for software bug detection has come a long way since its early beginnings as a compiler technology. However, with the introduction of more sophisticated algorithmic techniques, such as model checking and constraint solving, questions about performance are a major concern. In this work we present an empirical study of our industrial strength source code analysis tool Goanna that uses a model checking core for static analysis of C/C++ code. We present the core technology and abstraction mechanism with a focus on performance, as guided by experience from having analyzed millions of lines of code. In particular, we present results from our recent study within the NIST/DHS SAMATE program. The results show that, maybe surprisingly, formal verification techniques can be used successfully in practical industry applications scaling roughly linearly, even for millions of lines of code.\n  },\n        Type = {B - International Conferences},\n\n}\n\n</pre>\n</div>\n\n\n<div class=\"well well-small bibbase\" data-type=\"abstract\"\n     style=\"display:none\">\n  Static source code analysis for software bug detection has come a long way since its early beginnings as a compiler technology. However, with the introduction of more sophisticated algorithmic techniques, such as model checking and constraint solving, questions about performance are a major concern. In this work we present an empirical study of our industrial strength source code analysis tool Goanna that uses a model checking core for static analysis of C/C++ code. We present the core technology and abstraction mechanism with a focus on performance, as guided by experience from having analyzed millions of lines of code. In particular, we present results from our recent study within the NIST/DHS SAMATE program. The results show that, maybe surprisingly, formal verification techniques can be used successfully in practical industry applications scaling roughly linearly, even for millions of lines of code. \n</div>\n\n\n</div>\n\n\n\n\n\n    </div>\n  </div>\n\n\n\n\n  </div>\n\n\n  <!-- Modal -->\n\n  <!-- <iframe id=\"bibbase_network_frame\" -->\n  <!--         src=\"//bibbase.org/network/control\" -->\n  <!--         style=\"display: none;\"> -->\n  <!-- </iframe> -->\n\n</div>\n"}; document.write(bibbase_data.data);