@inproceedings{leino_basis_2009,
	title = {A basis for verifying multi-threaded programs},
	volume = {5502},
	isbn = {978-3-642-00589-3},
	url = {http://link.springer.com/10.1007/978-3-642-00590-9_27},
	doi = {10/bgmg5p},
	abstract = {Advanced multi-threaded programs apply concurrency concepts in sophisticated ways. For instance, they use fine-grained locking to increase parallelism and change locking orders dynamically when data structures are being reorganized. This paper presents a sound and modular verification methodology that can handle advanced concurrency patterns in multi-threaded, object-based programs. The methodology is based on implicit dynamic frames and uses fractional permissions to support fine-grained locking. It supports concepts such as multi-object monitor invariants, thread-local and shared objects, thread pre- and postconditions, and deadlock prevention with a dynamically changeable locking order. The paper prescribes the generation of verification conditions in first-order logic, well-suited for scrutiny by off-the-shelf SMT solvers. A verifier for the methodology has been implemented for an experimental language, and has been used to verify several challenging examples including hand-over-hand locking for linked lists and a lock re-ordering algorithm.},
	urldate = {2017-02-05},
	booktitle = {Lecture {Notes} in {Computer} {Science} (including subseries {Lecture} {Notes} in {Artificial} {Intelligence} and {Lecture} {Notes} in {Bioinformatics})},
	publisher = {Springer-Verlag},
	author = {Leino, K. Rustan M. and Müller, Peter},
	year = {2009},
	note = {ISSN: 03029743},
	pages = {378--393}
}

{"_id":"EnWy2ghgSWHxABPf2","bibbaseid":"leino-mller-abasisforverifyingmultithreadedprograms-2009","authorIDs":[],"author_short":["Leino, K. R. M.","Müller, P."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","title":"A basis for verifying multi-threaded programs","volume":"5502","isbn":"978-3-642-00589-3","url":"http://link.springer.com/10.1007/978-3-642-00590-9_27","doi":"10/bgmg5p","abstract":"Advanced multi-threaded programs apply concurrency concepts in sophisticated ways. For instance, they use fine-grained locking to increase parallelism and change locking orders dynamically when data structures are being reorganized. This paper presents a sound and modular verification methodology that can handle advanced concurrency patterns in multi-threaded, object-based programs. The methodology is based on implicit dynamic frames and uses fractional permissions to support fine-grained locking. It supports concepts such as multi-object monitor invariants, thread-local and shared objects, thread pre- and postconditions, and deadlock prevention with a dynamically changeable locking order. The paper prescribes the generation of verification conditions in first-order logic, well-suited for scrutiny by off-the-shelf SMT solvers. A verifier for the methodology has been implemented for an experimental language, and has been used to verify several challenging examples including hand-over-hand locking for linked lists and a lock re-ordering algorithm.","urldate":"2017-02-05","booktitle":"Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)","publisher":"Springer-Verlag","author":[{"propositions":[],"lastnames":["Leino"],"firstnames":["K.","Rustan","M."],"suffixes":[]},{"propositions":[],"lastnames":["Müller"],"firstnames":["Peter"],"suffixes":[]}],"year":"2009","note":"ISSN: 03029743","pages":"378–393","bibtex":"@inproceedings{leino_basis_2009,\n\ttitle = {A basis for verifying multi-threaded programs},\n\tvolume = {5502},\n\tisbn = {978-3-642-00589-3},\n\turl = {http://link.springer.com/10.1007/978-3-642-00590-9_27},\n\tdoi = {10/bgmg5p},\n\tabstract = {Advanced multi-threaded programs apply concurrency concepts in sophisticated ways. For instance, they use fine-grained locking to increase parallelism and change locking orders dynamically when data structures are being reorganized. This paper presents a sound and modular verification methodology that can handle advanced concurrency patterns in multi-threaded, object-based programs. The methodology is based on implicit dynamic frames and uses fractional permissions to support fine-grained locking. It supports concepts such as multi-object monitor invariants, thread-local and shared objects, thread pre- and postconditions, and deadlock prevention with a dynamically changeable locking order. The paper prescribes the generation of verification conditions in first-order logic, well-suited for scrutiny by off-the-shelf SMT solvers. A verifier for the methodology has been implemented for an experimental language, and has been used to verify several challenging examples including hand-over-hand locking for linked lists and a lock re-ordering algorithm.},\n\turldate = {2017-02-05},\n\tbooktitle = {Lecture {Notes} in {Computer} {Science} (including subseries {Lecture} {Notes} in {Artificial} {Intelligence} and {Lecture} {Notes} in {Bioinformatics})},\n\tpublisher = {Springer-Verlag},\n\tauthor = {Leino, K. Rustan M. and Müller, Peter},\n\tyear = {2009},\n\tnote = {ISSN: 03029743},\n\tpages = {378--393}\n}\n\n","author_short":["Leino, K. R. M.","Müller, P."],"key":"leino_basis_2009","id":"leino_basis_2009","bibbaseid":"leino-mller-abasisforverifyingmultithreadedprograms-2009","role":"author","urls":{"Paper":"http://link.springer.com/10.1007/978-3-642-00590-9_27"},"downloads":0},"bibtype":"inproceedings","biburl":"https://bibbase.org/zotero/k4rtik","creationDate":"2019-07-02T12:17:56.559Z","downloads":0,"keywords":[],"search_terms":["basis","verifying","multi","threaded","programs","leino","müller"],"title":"A basis for verifying multi-threaded programs","year":2009,"dataSources":["Z5Dp3qAJiMzxtvKMq"]}