{"_id":"GScmaNZyrMSQN8eaT","bibbaseid":"cassez-sloane-roberts-pigram-suvanpong-dealedomarugn-skinkstaticanalysisofprogramsinllvmintermediaterepresentationcompetitioncontribution-2017","author_short":["Cassez, F.","Sloane, A.","Roberts, M.","Pigram, M.","Suvanpong, P.","de Aledo Marugán, P. G."],"bibdata":{"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":{}},"downloads":2},"bibtype":"inproceedings","biburl":"http://science.mq.edu.au/~fcassez/bib/franck-bib.bib","dataSources":["8742EsvjQfyP2fYBW","qbqYFWskmoonRB43F"],"keywords":["refinement","software verification"],"search_terms":["skink","static","analysis","programs","llvm","intermediate","representation","competition","contribution","cassez","sloane","roberts","pigram","suvanpong","de aledo marugán"],"title":"Skink: Static Analysis of Programs in LLVM Intermediate Representation (Competition contribution)","year":2017,"downloads":2}