Skip to content
Snippets Groups Projects
Commit 32725b7d authored by Pedro da Rocha Pinto's avatar Pedro da Rocha Pinto
Browse files

Update publications.bib

parent d23ebaa0
No related branches found
No related tags found
No related merge requests found
...@@ -1582,7 +1582,7 @@ exhibit the desired behaviour.}, ...@@ -1582,7 +1582,7 @@ exhibit the desired behaviour.},
issn = {2352-2208}, issn = {2352-2208},
abstract = {The specification of a concurrent program module, and the verification of implementations and clients with respect to such a specification, are difficult problems. A specification should be general enough that any reasonable implementation satisfies it, yet precise enough that it can be used by any reasonable client. We survey a range of techniques for specifying concurrent modules, using the example of a counter module to illustrate the benefits and limitations of each. In particular, we highlight four key concepts underpinning these techniques: auxiliary state, interference abstraction, resource ownership and atomicity. We demonstrate how these concepts can be combined to achieve two powerful approaches for specifying concurrent modules and verifying implementations and clients, which remove the limitations highlighted by the counter example.}, abstract = {The specification of a concurrent program module, and the verification of implementations and clients with respect to such a specification, are difficult problems. A specification should be general enough that any reasonable implementation satisfies it, yet precise enough that it can be used by any reasonable client. We survey a range of techniques for specifying concurrent modules, using the example of a counter module to illustrate the benefits and limitations of each. In particular, we highlight four key concepts underpinning these techniques: auxiliary state, interference abstraction, resource ownership and atomicity. We demonstrate how these concepts can be combined to achieve two powerful approaches for specifying concurrent modules and verifying implementations and clients, which remove the limitations highlighted by the counter example.},
project = { concurrency }, project = { concurrency },
doi = {https://doi.org/10.1016/j.jlamp.2018.03.003}, doi = {10.1016/j.jlamp.2018.03.003},
keywords = {Concurrency, Specification, Program verification}, keywords = {Concurrency, Specification, Program verification},
url = {http://www.sciencedirect.com/science/article/pii/S2352220817300871}, url = {http://www.sciencedirect.com/science/article/pii/S2352220817300871},
} }
...@@ -1607,7 +1607,7 @@ of the module, and modules built over a file system, where the interference cann ...@@ -1607,7 +1607,7 @@ of the module, and modules built over a file system, where the interference cann
as the file system is a public namespace. We introduce specifications conditional on context as the file system is a public namespace. We introduce specifications conditional on context
invariants used to restrict the interference, and apply our reasoning to the example of lock files.}, invariants used to restrict the interference, and apply our reasoning to the example of lock files.},
project = { concurrency, tada }, project = { concurrency, tada },
doi = {https://doi.org/10.4230/LIPIcs.ECOOP.2018.4}, doi = {10.4230/LIPIcs.ECOOP.2018.4},
} }
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment