Commit 3f505fcd authored by Mihaela SIGHIREANU's avatar Mihaela SIGHIREANU
Browse files

update bibliography to compact given names and remove pages

parent b3b02490
......@@ -81,14 +81,14 @@ Zhilin Wu\inst{2} \orcidID{0000-0003-0899-628X}
\newpage
%------------------------------------------------------------------------------
\bibliographystyle{plain}
\bibliographystyle{siam}
\bibliography{../bibs/biblio}
\newpage
\appendix
%\section{Appendixes}
\input{app-sat-hls.tex}
\input{app-ent-hls.tex}
%\input{app-ent-hls.tex}
%% temporary
%\newpage
......
......@@ -5,7 +5,7 @@
booktitle = {{VMCAI}},
series = {LNCS},
volume = {12597},
pages = {578--602},
OPTpages = {578--602},
publisher = {Springer},
year = {2021},
OPTurl = {https://doi.org/10.1007/978-3-030-67067-2\_26},
......@@ -26,7 +26,7 @@
booktitle = {{LPAR}},
series = {EPiC Series in Computing},
volume = {73},
pages = {191--211},
OPTpages = {191--211},
publisher = {EasyChair},
year = {2020},
doi = {10.29007/f5wh},
......@@ -45,7 +45,7 @@
booktitle = {{LPAR}},
series = {EPiC Series in Computing},
volume = {73},
pages = {390--408},
OPTpages = {390--408},
publisher = {EasyChair},
year = {2020},
doi = {10.29007/vkmj},
......@@ -73,7 +73,7 @@
booktitle = {{NFM}},
series = {LNCS},
volume = {9058},
pages = {3--11},
OPTpages = {3--11},
publisher = {Springer},
year = {2015},
OPTurl = {https://doi.org/10.1007/978-3-319-17524-9\_1},
......@@ -93,7 +93,7 @@
on Formal Engineering Methods, {ICFEM} 2006, Macao, China, November
1-3, 2006, Proceedings},
booktitle = {{ICFEM}},
pages = {400--419},
OPTpages = {400--419},
year = {2006},
series = {LNCS},
volume = {4260},
......@@ -113,7 +113,7 @@
Language Design and Implementation, {PLDI} 2011, San Jose, CA, USA,
June 4-8, 2011},
booktitle = {{PLDI}},
pages = {234--245},
OPTpages = {234--245},
year = {2011},
publisher = {{ACM}},
OPTnote = {Presents a Coq library based on Separation Logic that
......@@ -134,7 +134,7 @@ OPTurl = {https://doi.org/10.1145/3381898.3397211},
doi = {10.1145/3381898.3397211},
abstract = {We verify the functional correctness of an array-of-bins (segregated free-lists) single-thread malloc/free system with respect to a correctness specification written in separation logic. The memory allocator is written in standard C code compatible with the standard API; the specification is in the Verifiable C program logic, and the proof is done in the Verified Software Toolchain within the Coq proof assistant. Our "resource-aware" specification can guarantee when malloc will successfully return a block, unlike the standard Posix specification that allows malloc to return NULL whenever it wants to. We also prove subsumption (refinement): the resource-aware specification implies a resource-oblivious spec.},
booktitle = {Proceedings of the 2020 ACM SIGPLAN International Symposium on Memory Management},
pages = {48–59},
OPTpages = {48–59},
numpages = {12},
keywords = {formal verification, separation logic, memory management},
location = {London, UK},
......@@ -170,7 +170,7 @@ series = {ISMM 2020}
series = {LNCS},
volume = {3328},
year = {2005},
pages = {97--109},
OPTpages = {97--109},
doi = {10.1007/978-3-540-30538-5_9},
ee = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=3328{\&}spage=97},
bibsource = {DBLP, http://dblp.uni-trier.de}
......@@ -181,7 +181,7 @@ series = {ISMM 2020}
Mihaela Sighireanu},
title = {A Verified Implementation of the Bounded List Container},
booktitle = {{TACAS}},
pages = {172--189},
OPTpages = {172--189},
year = {2018},
series = {LNCS},
volume = {10805},
......@@ -200,7 +200,7 @@ series = {ISMM 2020}
title = {The Tree Width of Separation Logic with Recursive Definitions},
booktitle = {CADE},
year = {2013},
pages = {21--38},
OPTpages = {21--38},
series = {Lecture Notes in Computer Science},
volume = {7898},
publisher = {Springer},
......@@ -238,7 +238,7 @@ series = {ISMM 2020}
Zhilin Wu},
title = {{SL-COMP:} Competition of Solvers for Separation Logic},
booktitle = {{TACAS}},
pages = {116--132},
OPTpages = {116--132},
year = {2019},
series = {LNCS},
volume = {11429},
......@@ -256,7 +256,7 @@ series = {ISMM 2020}
Andrey Rybalchenko},
title = {Separation Logic Modulo Theories},
booktitle = {{APLAS}},
pages = {90--106},
OPTpages = {90--106},
series = {LNCS},
year = {2013},
volume = {8301},
......@@ -274,7 +274,7 @@ series = {ISMM 2020}
title = {Tractable Reasoning in a Fragment of Separation Logic},
booktitle = {CONCUR},
year = {2011},
pages = {235--249},
OPTpages = {235--249},
series = {LNCS},
volume = {6901},
publisher = {Springer},
......@@ -298,7 +298,7 @@ series = {ISMM 2020}
doi = {10.1145/3211968},
journal = {Commun. ACM},
month = jan,
pages = {86-95},
OPTpages = {86-95},
OPTnumpages = {10}
}
......@@ -311,7 +311,7 @@ series = {ISMM 2020}
series = {LNCS},
volume = {6461},
publisher = {Springer},
pages = {304--311},
OPTpages = {304--311},
year = {2010},
OPTurl = {http://dx.doi.org/10.1007/978-3-642-17164-2\_21},
doi = {10.1007/978-3-642-17164-2\_21},
......@@ -328,7 +328,7 @@ series = {ISMM 2020}
journal = {Commun. {ACM}},
volume = {62},
number = {8},
pages = {62--70},
OPTpages = {62--70},
year = {2019},
url = {https://doi.org/10.1145/3338112},
doi = {10.1145/3338112},
......@@ -342,7 +342,7 @@ series = {ISMM 2020}
title = {Separation Logic: A Logic for Shared Mutable Data Structures},
booktitle = {LICS},
year = {2002},
pages = {55--74},
OPTpages = {55--74},
numpages = {20},
acmid = {664578},
publisher = {IEEE Computer Society},
......@@ -354,7 +354,7 @@ series = {ISMM 2020}
Makoto Tatsuta},
title = {Decidability for Entailments of Symbolic Heaps with Arrays},
journal = {CoRR},
volume = {abs/1802.05935},
volume = {arXiv:1802.05935v3},
year = {2018},
url = {http://arxiv.org/abs/1802.05935},
archivePrefix = {arXiv},
......@@ -385,7 +385,7 @@ series = {ISMM 2020}
isbn = {978-3-319-63045-8 978-3-319-63046-5},
url = {http://link.springer.com/10.1007/978-3-319-63046-5_29},
eventtitle = {{CADE}},
pages = {472--490},
OPTpages = {472--490},
booktitle = {{CADE} 26},
publisher = {Springer},
author = {Brotherston, James and Gorogiannis, Nikos and Kanovich, Max},
......@@ -405,7 +405,7 @@ series = {ISMM 2020}
title = {A decision procedure for satisfiability in separation logic with inductive
predicates},
booktitle = {{CSL-LICS}},
pages = {25:1--25:10},
OPTpages = {25:1--25:10},
publisher = {{ACM}},
year = {2014},
OPTurl = {https://doi.org/10.1145/2603088.2603091},
......@@ -431,7 +431,7 @@ series = {ISMM 2020}
year = {2006},
doi = {10.1007/11823230_13},
keywords = {Separation Logic, Shape Analysis, Memory Allocators},
pages = {182--203}
OPTpages = {182--203}
}
@inproceedings{DacaHK16,
......@@ -441,7 +441,7 @@ series = {ISMM 2020}
isbn = {978-3-319-41539-0 978-3-319-41540-6},
url = {http://link.springer.com/10.1007/978-3-319-41540-6_13},
eventtitle = {{CAV}},
pages = {230--248},
OPTpages = {230--248},
booktitle = {Computer Aided Verification},
publisher = {Springer International Publishing},
author = {Daca, Przemysaw and Henzinger, Thomas A. and Kupriyanov, Andrey},
......@@ -457,7 +457,7 @@ series = {ISMM 2020}
isbn = {978-3-319-40228-4 978-3-319-40229-1},
url = {http://link.springer.com/10.1007/978-3-319-40229-1_36},
eventtitle = {{IJCAR}},
pages = {532--549},
OPTpages = {532--549},
booktitle = {{IJCAR}},
series = {LNAI},
publisher = {Springer},
......@@ -482,7 +482,7 @@ series = {ISMM 2020}
author = {Fang, Bin and Sighireanu, Mihaela},
year = {2017},
keywords = {Static Analysis for Low-Level Code, Separation Logic, Memory Allocators},
pages = {151--167}
OPTpages = {151--167}
}
@phdthesis{linthesis,
......@@ -501,7 +501,7 @@ series = {ISMM 2020}
Science Logic {(CSL)} and the Twenty-Ninth Annual {ACM/IEEE} Symposium
on Logic in Computer Science (LICS), {CSL-LICS} '14, Vienna, Austria,
July 14 - 18, 2014},
pages = {47:1--47:10},
OPTpages = {47:1--47:10},
publisher = {{ACM}},
year = {2014},
}
......@@ -525,7 +525,7 @@ series = {ISMM 2020}
booktitle = {ATVA},
series = {LNCS},
volume = {9364},
pages = {80--96},
OPTpages = {80--96},
publisher = {Springer},
year = {2015},
}
......@@ -546,7 +546,7 @@ series = {ISMM 2020}
booktitle = {{APLAS}},
series = {LNCS},
volume = {10695},
pages = {169--189},
OPTpages = {169--189},
publisher = {Springer},
year = {2017},
}
......@@ -558,7 +558,7 @@ series = {ISMM 2020}
booktitle = {{NFM}},
series = {LNCS},
volume = {6617},
pages = {459--465},
OPTpages = {459--465},
publisher = {Springer},
year = {2011},
}
......@@ -579,7 +579,7 @@ series = {ISMM 2020}
series = {LNCS},
volume = {9058},
publisher = {Springer},
pages = {3--11},
OPTpages = {3--11},
year = {2015},
}
......@@ -599,7 +599,7 @@ year = {1995},
publisher = {Springer},
OPTaddress = {Berlin, Heidelberg},
booktitle = {{IWMM}},
pages = {1--116},
OPTpages = {1--116},
numpages = {116},
OPTseries = {IWMM'95}
}
......@@ -615,7 +615,7 @@ OPTseries = {IWMM'95}
booktitle = {{TACAS}},
series = {LNCS},
volume = {11428},
pages = {319--336},
OPTpages = {319--336},
publisher = {Springer},
year = {2019},
}
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment