---
_id: '4390'
abstract:
- lang: eng
text: Concurrent data structures with fine-grained synchronization are notoriously
difficult to implement correctly. The difficulty of reasoning about these implementations
does not stem from the number of variables or the program size, but rather from
the large number of possible interleavings. These implementations are therefore
prime candidates for model checking. We introduce an algorithm for verifying linearizability
of singly-linked heap-based concurrent data structures. We consider a model consisting
of an unbounded heap where each vertex stores an element from an unbounded data
domain, with a restricted set of operations for testing and updating pointers
and data elements. Our main result is that linearizability is decidable for programs
that invoke a fixed number of methods, possibly in parallel. This decidable fragment
covers many of the common implementation techniques — fine-grained locking, lazy
synchronization, and lock-free synchronization. We also show how the technique
can be used to verify optimistic implementations with the help of programmer annotations.
We developed a verification tool CoLT and evaluated it on a representative sample
of Java implementations of the concurrent set data structure. The tool verified
linearizability of a number of implementations, found a known error in a lock-free
implementation and proved that the corrected version is linearizable.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Pavol
full_name: Cerny, Pavol
id: 4DCBEFFE-F248-11E8-B48F-1D18A9856A87
last_name: Cerny
- first_name: Arjun
full_name: Radhakrishna, Arjun
id: 3B51CAC4-F248-11E8-B48F-1D18A9856A87
last_name: Radhakrishna
- first_name: Damien
full_name: Zufferey, Damien
id: 4397AC76-F248-11E8-B48F-1D18A9856A87
last_name: Zufferey
orcid: 0000-0002-3197-8736
- first_name: Swarat
full_name: Chaudhuri, Swarat
last_name: Chaudhuri
- first_name: Rajeev
full_name: Alur, Rajeev
last_name: Alur
citation:
ama: 'Cerny P, Radhakrishna A, Zufferey D, Chaudhuri S, Alur R. Model checking of
linearizability of concurrent list implementations. In: Vol 6174. Springer; 2010:465-479.
doi:10.1007/978-3-642-14295-6_41'
apa: 'Cerny, P., Radhakrishna, A., Zufferey, D., Chaudhuri, S., & Alur, R. (2010).
Model checking of linearizability of concurrent list implementations (Vol. 6174,
pp. 465–479). Presented at the CAV: Computer Aided Verification, Edinburgh, UK:
Springer. https://doi.org/10.1007/978-3-642-14295-6_41'
chicago: Cerny, Pavol, Arjun Radhakrishna, Damien Zufferey, Swarat Chaudhuri, and
Rajeev Alur. “Model Checking of Linearizability of Concurrent List Implementations,”
6174:465–79. Springer, 2010. https://doi.org/10.1007/978-3-642-14295-6_41.
ieee: 'P. Cerny, A. Radhakrishna, D. Zufferey, S. Chaudhuri, and R. Alur, “Model
checking of linearizability of concurrent list implementations,” presented at
the CAV: Computer Aided Verification, Edinburgh, UK, 2010, vol. 6174, pp. 465–479.'
ista: 'Cerny P, Radhakrishna A, Zufferey D, Chaudhuri S, Alur R. 2010. Model checking
of linearizability of concurrent list implementations. CAV: Computer Aided Verification,
LNCS, vol. 6174, 465–479.'
mla: Cerny, Pavol, et al. Model Checking of Linearizability of Concurrent List
Implementations. Vol. 6174, Springer, 2010, pp. 465–79, doi:10.1007/978-3-642-14295-6_41.
short: P. Cerny, A. Radhakrishna, D. Zufferey, S. Chaudhuri, R. Alur, in:, Springer,
2010, pp. 465–479.
conference:
end_date: 2010-07-17
location: Edinburgh, UK
name: 'CAV: Computer Aided Verification'
start_date: 2010-07-15
date_created: 2018-12-11T12:08:36Z
date_published: 2010-07-01T00:00:00Z
date_updated: 2023-02-23T12:24:12Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-642-14295-6_41
file:
- access_level: open_access
checksum: 2eb211ce40b3c4988bce3a3592980704
content_type: application/pdf
creator: dernst
date_created: 2020-05-19T16:31:56Z
date_updated: 2020-07-14T12:46:28Z
file_id: '7873'
file_name: 2010_CAV_Cerny.pdf
file_size: 3633276
relation: main_file
file_date_updated: 2020-07-14T12:46:28Z
has_accepted_license: '1'
intvolume: ' 6174'
language:
- iso: eng
month: '07'
oa: 1
oa_version: Submitted Version
page: 465 - 479
publication_status: published
publisher: Springer
publist_id: '1066'
pubrep_id: '27'
quality_controlled: '1'
related_material:
record:
- id: '5391'
relation: earlier_version
status: public
status: public
title: Model checking of linearizability of concurrent list implementations
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 6174
year: '2010'
...
---
_id: '4392'
abstract:
- lang: eng
text: 'While a boolean notion of correctness is given by a preorder on systems and
properties, a quantitative notion of correctness is defined by a distance function
on systems and properties, where the distance between a system and a property
provides a measure of “fit” or “desirability.” In this article, we explore several
ways how the simulation preorder can be generalized to a distance function. This
is done by equipping the classical simulation game between a system and a property
with quantitative objectives. In particular, for systems that satisfy a property,
a quantitative simulation game can measure the “robustness” of the satisfaction,
that is, how much the system can deviate from its nominal behavior while still
satisfying the property. For systems that violate a property, a quantitative simulation
game can measure the “seriousness” of the violation, that is, how much the property
has to be modified so that it is satisfied by the system. These distances can
be computed in polynomial time, since the computation reduces to the value problem
in limit average games with constant weights. Finally, we demonstrate how the
robustness distance can be used to measure how many transmission errors are tolerated
by error correcting codes. '
alternative_title:
- LNCS
author:
- first_name: Pavol
full_name: Cerny, Pavol
id: 4DCBEFFE-F248-11E8-B48F-1D18A9856A87
last_name: Cerny
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Arjun
full_name: Radhakrishna, Arjun
id: 3B51CAC4-F248-11E8-B48F-1D18A9856A87
last_name: Radhakrishna
citation:
ama: 'Cerny P, Henzinger TA, Radhakrishna A. Quantitative Simulation Games. In:
Manna Z, Peled D, eds. Time For Verification: Essays in Memory of Amir Pnueli.
Vol 6200. Essays in Memory of Amir Pnueli. Springer; 2010:42-60. doi:10.1007/978-3-642-13754-9_3'
apa: 'Cerny, P., Henzinger, T. A., & Radhakrishna, A. (2010). Quantitative Simulation
Games. In Z. Manna & D. Peled (Eds.), Time For Verification: Essays in
Memory of Amir Pnueli (Vol. 6200, pp. 42–60). Springer. https://doi.org/10.1007/978-3-642-13754-9_3'
chicago: 'Cerny, Pavol, Thomas A Henzinger, and Arjun Radhakrishna. “Quantitative
Simulation Games.” In Time For Verification: Essays in Memory of Amir Pnueli,
edited by Zohar Manna and Doron Peled, 6200:42–60. Essays in Memory of Amir Pnueli.
Springer, 2010. https://doi.org/10.1007/978-3-642-13754-9_3.'
ieee: 'P. Cerny, T. A. Henzinger, and A. Radhakrishna, “Quantitative Simulation
Games,” in Time For Verification: Essays in Memory of Amir Pnueli, vol.
6200, Z. Manna and D. Peled, Eds. Springer, 2010, pp. 42–60.'
ista: 'Cerny P, Henzinger TA, Radhakrishna A. 2010.Quantitative Simulation Games.
In: Time For Verification: Essays in Memory of Amir Pnueli. LNCS, vol. 6200, 42–60.'
mla: 'Cerny, Pavol, et al. “Quantitative Simulation Games.” Time For Verification:
Essays in Memory of Amir Pnueli, edited by Zohar Manna and Doron Peled, vol.
6200, Springer, 2010, pp. 42–60, doi:10.1007/978-3-642-13754-9_3.'
short: 'P. Cerny, T.A. Henzinger, A. Radhakrishna, in:, Z. Manna, D. Peled (Eds.),
Time For Verification: Essays in Memory of Amir Pnueli, Springer, 2010, pp. 42–60.'
date_created: 2018-12-11T12:08:37Z
date_published: 2010-07-29T00:00:00Z
date_updated: 2021-01-12T07:56:38Z
day: '29'
department:
- _id: ToHe
doi: 10.1007/978-3-642-13754-9_3
ec_funded: 1
editor:
- first_name: Zohar
full_name: Manna, Zohar
last_name: Manna
- first_name: Doron
full_name: Peled, Doron
last_name: Peled
intvolume: ' 6200'
language:
- iso: eng
month: '07'
oa_version: None
page: 42 - 60
project:
- _id: 25EFB36C-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '215543'
name: COMponent-Based Embedded Systems design Techniques
- _id: 25F1337C-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '214373'
name: Design for Embedded Systems
publication: 'Time For Verification: Essays in Memory of Amir Pnueli'
publication_status: published
publisher: Springer
publist_id: '1064'
quality_controlled: '1'
scopus_import: 1
series_title: Essays in Memory of Amir Pnueli
status: public
title: Quantitative Simulation Games
type: book_chapter
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
volume: 6200
year: '2010'
...
---
_id: '4393'
abstract:
- lang: eng
text: Boolean notions of correctness are formalized by preorders on systems. Quantitative
measures of correctness can be formalized by real-valued distance functions between
systems, where the distance between implementation and specification provides
a measure of “fit” or “desirability.” We extend the simulation preorder to the
quantitative setting, by making each player of a simulation game pay a certain
price for her choices. We use the resulting games with quantitative objectives
to define three different simulation distances. The correctness distance measures
how much the specification must be changed in order to be satisfied by the implementation.
The coverage distance measures how much the implementation restricts the degrees
of freedom offered by the specification. The robustness distance measures how
much a system can deviate from the implementation description without violating
the specification. We consider these distances for safety as well as liveness
specifications. The distances can be computed in polynomial time for safety specifications,
and for liveness specifications given by weak fairness constraints. We show that
the distance functions satisfy the triangle inequality, that the distance between
two systems does not increase under parallel composition with a third system,
and that the distance between two systems can be bounded from above and below
by distances between abstractions of the two systems. These properties suggest
that our simulation distances provide an appropriate basis for a quantitative
theory of discrete systems. We also demonstrate how the robustness distance can
be used to measure how many transmission errors are tolerated by error correcting
codes.
acknowledgement: This work was partially supported by the European Union project COMBEST
and the European Network of Excellence ArtistDesign.
alternative_title:
- LNCS
author:
- first_name: Pavol
full_name: Cerny, Pavol
id: 4DCBEFFE-F248-11E8-B48F-1D18A9856A87
last_name: Cerny
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Arjun
full_name: Radhakrishna, Arjun
id: 3B51CAC4-F248-11E8-B48F-1D18A9856A87
last_name: Radhakrishna
citation:
ama: 'Cerny P, Henzinger TA, Radhakrishna A. Simulation distances. In: Vol 6269.
Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2010:235-268. doi:10.1007/978-3-642-15375-4_18'
apa: 'Cerny, P., Henzinger, T. A., & Radhakrishna, A. (2010). Simulation distances
(Vol. 6269, pp. 235–268). Presented at the CONCUR: Concurrency Theory, Paris,
France: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.1007/978-3-642-15375-4_18'
chicago: Cerny, Pavol, Thomas A Henzinger, and Arjun Radhakrishna. “Simulation Distances,”
6269:235–68. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2010. https://doi.org/10.1007/978-3-642-15375-4_18.
ieee: 'P. Cerny, T. A. Henzinger, and A. Radhakrishna, “Simulation distances,” presented
at the CONCUR: Concurrency Theory, Paris, France, 2010, vol. 6269, pp. 235–268.'
ista: 'Cerny P, Henzinger TA, Radhakrishna A. 2010. Simulation distances. CONCUR:
Concurrency Theory, LNCS, vol. 6269, 235–268.'
mla: Cerny, Pavol, et al. Simulation Distances. Vol. 6269, Schloss Dagstuhl
- Leibniz-Zentrum für Informatik, 2010, pp. 235–68, doi:10.1007/978-3-642-15375-4_18.
short: P. Cerny, T.A. Henzinger, A. Radhakrishna, in:, Schloss Dagstuhl - Leibniz-Zentrum
für Informatik, 2010, pp. 235–268.
conference:
end_date: 2010-09-03
location: Paris, France
name: 'CONCUR: Concurrency Theory'
start_date: 2010-08-31
date_created: 2018-12-11T12:08:37Z
date_published: 2010-11-01T00:00:00Z
date_updated: 2023-02-23T12:24:04Z
day: '01'
ddc:
- '005'
department:
- _id: ToHe
doi: 10.1007/978-3-642-15375-4_18
ec_funded: 1
file:
- access_level: open_access
checksum: ea567903676ba8afe0507ee11313dce5
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:15:12Z
date_updated: 2020-07-14T12:46:28Z
file_id: '5130'
file_name: IST-2012-42-v1+1_Simulation_distances.pdf
file_size: 198913
relation: main_file
file_date_updated: 2020-07-14T12:46:28Z
has_accepted_license: '1'
intvolume: ' 6269'
language:
- iso: eng
month: '11'
oa: 1
oa_version: Submitted Version
page: 235 - 268
project:
- _id: 25EFB36C-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '215543'
name: COMponent-Based Embedded Systems design Techniques
- _id: 25F1337C-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '214373'
name: Design for Embedded Systems
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '1065'
pubrep_id: '42'
quality_controlled: '1'
related_material:
record:
- id: '3249'
relation: later_version
status: public
- id: '5389'
relation: earlier_version
status: public
scopus_import: 1
status: public
title: Simulation distances
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 6269
year: '2010'
...
---
_id: '4395'
abstract:
- lang: eng
text: The problem of locally transforming or translating programs without altering
their semantics is central to the construction of correct compilers. For concurrent
shared-memory programs this task is challenging because (1) concurrent threads
can observe transformations that would be undetectable in a sequential program,
and (2) contemporary multiprocessors commonly use relaxed memory models that complicate
the reasoning. In this paper, we present a novel proof methodology for verifying
that a local program transformation is sound with respect to a specific hardware
memory model, in the sense that it is not observable in any context. The methodology
is based on a structural induction and relies on a novel compositional denotational
semantics for relaxed memory models that formalizes (1) the behaviors of program
fragments as a set of traces, and (2) the effect of memory model relaxations as
local trace rewrite operations. To apply this methodology in practice, we implemented
a semi- automated tool called Traver and used it to verify/falsify several compiler
transformations for a number of different hardware memory models.
alternative_title:
- LNCS
author:
- first_name: Sebastian
full_name: Burckhardt, Sebastian
last_name: Burckhardt
- first_name: Madanlal
full_name: Musuvathi, Madanlal
last_name: Musuvathi
- first_name: Vasu
full_name: Singh, Vasu
id: 4DAE2708-F248-11E8-B48F-1D18A9856A87
last_name: Singh
citation:
ama: 'Burckhardt S, Musuvathi M, Singh V. Verifying local transformations on relaxed
memory models. In: Gupta R, ed. Vol 6011. Springer; 2010:104-123. doi:10.1007/978-3-642-11970-5_7'
apa: 'Burckhardt, S., Musuvathi, M., & Singh, V. (2010). Verifying local transformations
on relaxed memory models. In R. Gupta (Ed.) (Vol. 6011, pp. 104–123). Presented
at the CC: Compiler Construction, Pahos, Cyprus: Springer. https://doi.org/10.1007/978-3-642-11970-5_7'
chicago: Burckhardt, Sebastian, Madanlal Musuvathi, and Vasu Singh. “Verifying Local
Transformations on Relaxed Memory Models.” edited by Rajiv Gupta, 6011:104–23.
Springer, 2010. https://doi.org/10.1007/978-3-642-11970-5_7.
ieee: 'S. Burckhardt, M. Musuvathi, and V. Singh, “Verifying local transformations
on relaxed memory models,” presented at the CC: Compiler Construction, Pahos,
Cyprus, 2010, vol. 6011, pp. 104–123.'
ista: 'Burckhardt S, Musuvathi M, Singh V. 2010. Verifying local transformations
on relaxed memory models. CC: Compiler Construction, LNCS, vol. 6011, 104–123.'
mla: Burckhardt, Sebastian, et al. Verifying Local Transformations on Relaxed
Memory Models. Edited by Rajiv Gupta, vol. 6011, Springer, 2010, pp. 104–23,
doi:10.1007/978-3-642-11970-5_7.
short: S. Burckhardt, M. Musuvathi, V. Singh, in:, R. Gupta (Ed.), Springer, 2010,
pp. 104–123.
conference:
end_date: 2010-03-28
location: Pahos, Cyprus
name: 'CC: Compiler Construction'
start_date: 2010-03-20
date_created: 2018-12-11T12:08:38Z
date_published: 2010-04-21T00:00:00Z
date_updated: 2021-01-12T07:56:39Z
day: '21'
doi: 10.1007/978-3-642-11970-5_7
editor:
- first_name: Rajiv
full_name: Gupta, Rajiv
last_name: Gupta
extern: '1'
intvolume: ' 6011'
language:
- iso: eng
month: '04'
oa_version: None
page: 104 - 123
publication_status: published
publisher: Springer
publist_id: '1063'
quality_controlled: '1'
status: public
title: Verifying local transformations on relaxed memory models
type: conference
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
volume: 6011
year: '2010'
...
---
_id: '4396'
abstract:
- lang: eng
text: 'Shape analysis is a promising technique to prove program properties about
recursive data structures. The challenge is to automatically determine the data-structure
type, and to supply the shape analysis with the necessary information about the
data structure. We present a stepwise approach to the selection of instrumentation
predicates for a TVLA-based shape analysis, which takes us a step closer towards
the fully automatic verification of data structures. The approach uses two techniques
to guide the refinement of shape abstractions: (1) during program exploration,
an explicit heap analysis collects sample instances of the heap structures, which
are used to identify the data structures that are manipulated by the program;
and (2) during abstraction refinement along an infeasible error path, we consider
different possible heap abstractions and choose the coarsest one that eliminates
the infeasible path. We have implemented this combined approach for automatic
shape refinement as an extension of the software model checker BLAST. Example
programs from a data-structure library that manipulate doubly-linked lists and
trees were successfully verified by our tool.'
alternative_title:
- LNCS
author:
- first_name: Dirk
full_name: Beyer, Dirk
last_name: Beyer
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Grégory
full_name: Théoduloz, Grégory
last_name: Théoduloz
- first_name: Damien
full_name: Zufferey, Damien
id: 4397AC76-F248-11E8-B48F-1D18A9856A87
last_name: Zufferey
orcid: 0000-0002-3197-8736
citation:
ama: 'Beyer D, Henzinger TA, Théoduloz G, Zufferey D. Shape refinement through explicit
heap analysis. In: Rosenblum D, Taenzer G, eds. Vol 6013. Springer; 2010:263-277.
doi:10.1007/978-3-642-12029-9_19'
apa: 'Beyer, D., Henzinger, T. A., Théoduloz, G., & Zufferey, D. (2010). Shape
refinement through explicit heap analysis. In D. Rosenblum & G. Taenzer (Eds.)
(Vol. 6013, pp. 263–277). Presented at the FASE: Fundamental Approaches To Software
Engineering, Paphos, Cyprus: Springer. https://doi.org/10.1007/978-3-642-12029-9_19'
chicago: Beyer, Dirk, Thomas A Henzinger, Grégory Théoduloz, and Damien Zufferey.
“Shape Refinement through Explicit Heap Analysis.” edited by David Rosenblum and
Gabriele Taenzer, 6013:263–77. Springer, 2010. https://doi.org/10.1007/978-3-642-12029-9_19.
ieee: 'D. Beyer, T. A. Henzinger, G. Théoduloz, and D. Zufferey, “Shape refinement
through explicit heap analysis,” presented at the FASE: Fundamental Approaches
To Software Engineering, Paphos, Cyprus, 2010, vol. 6013, pp. 263–277.'
ista: 'Beyer D, Henzinger TA, Théoduloz G, Zufferey D. 2010. Shape refinement through
explicit heap analysis. FASE: Fundamental Approaches To Software Engineering,
LNCS, vol. 6013, 263–277.'
mla: Beyer, Dirk, et al. Shape Refinement through Explicit Heap Analysis.
Edited by David Rosenblum and Gabriele Taenzer, vol. 6013, Springer, 2010, pp.
263–77, doi:10.1007/978-3-642-12029-9_19.
short: D. Beyer, T.A. Henzinger, G. Théoduloz, D. Zufferey, in:, D. Rosenblum, G.
Taenzer (Eds.), Springer, 2010, pp. 263–277.
conference:
end_date: 2010-03-28
location: Paphos, Cyprus
name: 'FASE: Fundamental Approaches To Software Engineering'
start_date: 2010-03-20
date_created: 2018-12-11T12:08:38Z
date_published: 2010-04-21T00:00:00Z
date_updated: 2021-01-12T07:56:40Z
day: '21'
ddc:
- '004'
department:
- _id: ToHe
doi: 10.1007/978-3-642-12029-9_19
editor:
- first_name: David
full_name: Rosenblum, David
last_name: Rosenblum
- first_name: Gabriele
full_name: Taenzer, Gabriele
last_name: Taenzer
file:
- access_level: open_access
checksum: 7d26e59a9681487d7283eba337292b2c
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:18:13Z
date_updated: 2020-07-14T12:46:29Z
file_id: '5332'
file_name: IST-2012-41-v1+1_Shape_refinement_through_explicit_heap_analysis.pdf
file_size: 312147
relation: main_file
file_date_updated: 2020-07-14T12:46:29Z
has_accepted_license: '1'
intvolume: ' 6013'
language:
- iso: eng
month: '04'
oa: 1
oa_version: Submitted Version
page: 263 - 277
project:
- _id: 2587B514-B435-11E9-9278-68D0E5697425
name: Microsoft Research Faculty Fellowship
publication_status: published
publisher: Springer
publist_id: '1061'
pubrep_id: '41'
quality_controlled: '1'
scopus_import: 1
status: public
title: Shape refinement through explicit heap analysis
type: conference
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
volume: 6013
year: '2010'
...
---
_id: '474'
abstract:
- lang: eng
text: 'Classical models of gene flow fail in three ways: they cannot explain large-scale
patterns; they predict much more genetic diversity than is observed; and they
assume that loosely linked genetic loci evolve independently. We propose a new
model that deals with these problems. Extinction events kill some fraction of
individuals in a region. These are replaced by offspring from a small number of
parents, drawn from the preexisting population. This model of evolution forwards
in time corresponds to a backwards model, in which ancestral lineages jump to
a new location if they are hit by an event, and may coalesce with other lineages
that are hit by the same event. We derive an expression for the identity in allelic
state, and show that, over scales much larger than the largest event, this converges
to the classical value derived by Wright and Malécot. However, rare events that
cover large areas cause low genetic diversity, large-scale patterns, and correlations
in ancestry between unlinked loci.'
acknowledgement: This work has made use of the resources provided by the Edinburgh
Compute and Data Facility (ECDF). The ECDF is partially supported by the eDIKT initiative.
NHB is supported in part by EPSRC Grant EP/E066070/1; JK is supported by EPSRC Grant
EP/E066070/1; and AME is supported in part by EPSRC Grant EP/E065945/1.
author:
- first_name: Nicholas H
full_name: Barton, Nicholas H
id: 4880FE40-F248-11E8-B48F-1D18A9856A87
last_name: Barton
orcid: 0000-0002-8548-5240
- first_name: Jerome
full_name: Kelleher, Jerome
last_name: Kelleher
- first_name: Alison
full_name: Etheridge, Alison
last_name: Etheridge
citation:
ama: 'Barton NH, Kelleher J, Etheridge A. A new model for extinction and recolonization
in two dimensions: Quantifying phylogeography. Evolution. 2010;64(9):2701-2715.
doi:10.1111/j.1558-5646.2010.01019.x'
apa: 'Barton, N. H., Kelleher, J., & Etheridge, A. (2010). A new model for extinction
and recolonization in two dimensions: Quantifying phylogeography. Evolution.
Wiley-Blackwell. https://doi.org/10.1111/j.1558-5646.2010.01019.x'
chicago: 'Barton, Nicholas H, Jerome Kelleher, and Alison Etheridge. “A New Model
for Extinction and Recolonization in Two Dimensions: Quantifying Phylogeography.”
Evolution. Wiley-Blackwell, 2010. https://doi.org/10.1111/j.1558-5646.2010.01019.x.'
ieee: 'N. H. Barton, J. Kelleher, and A. Etheridge, “A new model for extinction
and recolonization in two dimensions: Quantifying phylogeography,” Evolution,
vol. 64, no. 9. Wiley-Blackwell, pp. 2701–2715, 2010.'
ista: 'Barton NH, Kelleher J, Etheridge A. 2010. A new model for extinction and
recolonization in two dimensions: Quantifying phylogeography. Evolution. 64(9),
2701–2715.'
mla: 'Barton, Nicholas H., et al. “A New Model for Extinction and Recolonization
in Two Dimensions: Quantifying Phylogeography.” Evolution, vol. 64, no.
9, Wiley-Blackwell, 2010, pp. 2701–15, doi:10.1111/j.1558-5646.2010.01019.x.'
short: N.H. Barton, J. Kelleher, A. Etheridge, Evolution 64 (2010) 2701–2715.
date_created: 2018-12-11T11:46:40Z
date_published: 2010-09-01T00:00:00Z
date_updated: 2021-01-12T08:00:52Z
day: '01'
department:
- _id: NiBa
doi: 10.1111/j.1558-5646.2010.01019.x
intvolume: ' 64'
issue: '9'
language:
- iso: eng
month: '09'
oa_version: None
page: 2701 - 2715
publication: Evolution
publication_status: published
publisher: Wiley-Blackwell
publist_id: '2780'
quality_controlled: '1'
scopus_import: 1
status: public
title: 'A new model for extinction and recolonization in two dimensions: Quantifying
phylogeography'
type: journal_article
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 64
year: '2010'
...
---
_id: '488'
abstract:
- lang: eng
text: 'Streaming string transducers [1] define (partial) functions from input strings
to output strings. A streaming string transducer makes a single pass through the
input string and uses a finite set of variables that range over strings from the
output alphabet. At every step, the transducer processes an input symbol, and
updates all the variables in parallel using assignments whose right-hand-sides
are concatenations of output symbols and variables with the restriction that a
variable can be used at most once in a right-hand-side expression. It has been
shown that streaming string transducers operating on strings over infinite data
domains are of interest in algorithmic verification of list-processing programs,
as they lead to PSPACE decision procedures for checking pre/post conditions and
for checking semantic equivalence, for a well-defined class of heap-manipulating
programs. In order to understand the theoretical expressiveness of streaming transducers,
we focus on streaming transducers processing strings over finite alphabets, given
the existence of a robust and well-studied class of "regular" transductions
for this case. Such regular transductions can be defined either by two-way deterministic
finite-state transducers, or using a logical MSO-based characterization. Our main
result is that the expressiveness of streaming string transducers coincides exactly
with this class of regular transductions. '
alternative_title:
- LIPIcs
author:
- first_name: Rajeev
full_name: Alur, Rajeev
last_name: Alur
- first_name: Pavol
full_name: Cerny, Pavol
id: 4DCBEFFE-F248-11E8-B48F-1D18A9856A87
last_name: Cerny
citation:
ama: 'Alur R, Cerny P. Expressiveness of streaming string transducers. In: Vol 8.
Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2010:1-12. doi:10.4230/LIPIcs.FSTTCS.2010.1'
apa: 'Alur, R., & Cerny, P. (2010). Expressiveness of streaming string transducers
(Vol. 8, pp. 1–12). Presented at the FSTTCS: Foundations of Software Technology
and Theoretical Computer Science, Chennai, India: Schloss Dagstuhl - Leibniz-Zentrum
für Informatik. https://doi.org/10.4230/LIPIcs.FSTTCS.2010.1'
chicago: Alur, Rajeev, and Pavol Cerny. “Expressiveness of Streaming String Transducers,”
8:1–12. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2010. https://doi.org/10.4230/LIPIcs.FSTTCS.2010.1.
ieee: 'R. Alur and P. Cerny, “Expressiveness of streaming string transducers,” presented
at the FSTTCS: Foundations of Software Technology and Theoretical Computer Science,
Chennai, India, 2010, vol. 8, pp. 1–12.'
ista: 'Alur R, Cerny P. 2010. Expressiveness of streaming string transducers. FSTTCS:
Foundations of Software Technology and Theoretical Computer Science, LIPIcs, vol.
8, 1–12.'
mla: Alur, Rajeev, and Pavol Cerny. Expressiveness of Streaming String Transducers.
Vol. 8, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2010, pp. 1–12, doi:10.4230/LIPIcs.FSTTCS.2010.1.
short: R. Alur, P. Cerny, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
2010, pp. 1–12.
conference:
end_date: 2010-12-18
location: Chennai, India
name: 'FSTTCS: Foundations of Software Technology and Theoretical Computer Science'
start_date: 2010-12-15
date_created: 2018-12-11T11:46:45Z
date_published: 2010-01-01T00:00:00Z
date_updated: 2021-01-12T08:01:00Z
day: '01'
ddc:
- '005'
department:
- _id: ToHe
doi: 10.4230/LIPIcs.FSTTCS.2010.1
file:
- access_level: open_access
checksum: 5845be5aa19791830f7407d8853f2df0
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:08:29Z
date_updated: 2020-07-14T12:46:35Z
file_id: '4690'
file_name: IST-2018-948-v1+1_2011_Cerny_Expressiveness_of.pdf
file_size: 492344
relation: main_file
file_date_updated: 2020-07-14T12:46:35Z
has_accepted_license: '1'
intvolume: ' 8'
language:
- iso: eng
month: '01'
oa: 1
oa_version: Published Version
page: 1 - 12
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '7331'
pubrep_id: '948'
quality_controlled: '1'
scopus_import: 1
status: public
title: Expressiveness of streaming string transducers
tmp:
image: /images/cc_by_nc_nd.png
legal_code_url: https://creativecommons.org/licenses/by-nc-nd/4.0/legalcode
name: Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International
(CC BY-NC-ND 4.0)
short: CC BY-NC-ND (4.0)
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 8
year: '2010'
...
---
_id: '489'
abstract:
- lang: eng
text: 'Graph games of infinite length are a natural model for open reactive processes:
one player represents the controller, trying to ensure a given specification,
and the other represents a hostile environment. The evolution of the system depends
on the decisions of both players, supplemented by chance. In this work, we focus
on the notion of randomised strategy. More specifically, we show that three natural
definitions may lead to very different results: in the most general cases, an
almost-surely winning situation may become almost-surely losing if the player
is only allowed to use a weaker notion of strategy. In more reasonable settings,
translations exist, but they require infinite memory, even in simple cases. Finally,
some traditional problems becomes undecidable for the strongest type of strategies.'
alternative_title:
- EPTCS
author:
- first_name: Julien
full_name: Cristau, Julien
last_name: Cristau
- first_name: Claire
full_name: David, Claire
last_name: David
- first_name: Florian
full_name: Horn, Florian
id: 37327ACE-F248-11E8-B48F-1D18A9856A87
last_name: Horn
citation:
ama: 'Cristau J, David C, Horn F. How do we remember the past in randomised strategies?
. In: Proceedings of GandALF 2010. Vol 25. Open Publishing Association;
2010:30-39. doi:10.4204/EPTCS.25.7'
apa: 'Cristau, J., David, C., & Horn, F. (2010). How do we remember the past
in randomised strategies? . In Proceedings of GandALF 2010 (Vol. 25, pp.
30–39). Minori, Amalfi Coast, Italy: Open Publishing Association. https://doi.org/10.4204/EPTCS.25.7'
chicago: Cristau, Julien, Claire David, and Florian Horn. “How Do We Remember the
Past in Randomised Strategies? .” In Proceedings of GandALF 2010, 25:30–39.
Open Publishing Association, 2010. https://doi.org/10.4204/EPTCS.25.7.
ieee: J. Cristau, C. David, and F. Horn, “How do we remember the past in randomised
strategies? ,” in Proceedings of GandALF 2010, Minori, Amalfi Coast, Italy,
2010, vol. 25, pp. 30–39.
ista: 'Cristau J, David C, Horn F. 2010. How do we remember the past in randomised
strategies? . Proceedings of GandALF 2010. GandALF: Games, Automata, Logic, and
Formal Verification, EPTCS, vol. 25, 30–39.'
mla: Cristau, Julien, et al. “How Do We Remember the Past in Randomised Strategies?
.” Proceedings of GandALF 2010, vol. 25, Open Publishing Association, 2010,
pp. 30–39, doi:10.4204/EPTCS.25.7.
short: J. Cristau, C. David, F. Horn, in:, Proceedings of GandALF 2010, Open Publishing
Association, 2010, pp. 30–39.
conference:
end_date: 2010-06-18
location: Minori, Amalfi Coast, Italy
name: 'GandALF: Games, Automata, Logic, and Formal Verification'
start_date: 2010-06-17
date_created: 2018-12-11T11:46:45Z
date_published: 2010-06-09T00:00:00Z
date_updated: 2021-01-12T08:01:01Z
day: '09'
department:
- _id: KrCh
doi: 10.4204/EPTCS.25.7
intvolume: ' 25'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1006.1404v1
month: '06'
oa: 1
oa_version: Published Version
page: 30 - 39
publication: Proceedings of GandALF 2010
publication_status: published
publisher: Open Publishing Association
publist_id: '7332'
quality_controlled: '1'
scopus_import: 1
status: public
title: 'How do we remember the past in randomised strategies? '
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 25
year: '2010'
...
---
_id: '533'
abstract:
- lang: eng
text: Any programming error that can be revealed before compiling a program saves
precious time for the programmer. While integrated development environments already
do a good job by detecting, e.g., data-flow abnormalities, current static analysis
tools suffer from false positives ("noise") or require strong user interaction.
We propose to avoid this deficiency by defining a new class of errors. A program
fragment is doomed if its execution will inevitably fail, regardless of which
state it is started in. We use a formal verification method to identify such errors
fully automatically and, most significantly, without producing noise. We report
on experiments with a prototype tool.
author:
- first_name: Jochen
full_name: Hoenicke, Jochen
last_name: Hoenicke
- first_name: Kari
full_name: Leino, Kari
last_name: Leino
- first_name: Andreas
full_name: Podelski, Andreas
last_name: Podelski
- first_name: Martin
full_name: Schäf, Martin
last_name: Schäf
- first_name: Thomas
full_name: Wies, Thomas
id: 447BFB88-F248-11E8-B48F-1D18A9856A87
last_name: Wies
citation:
ama: Hoenicke J, Leino K, Podelski A, Schäf M, Wies T. Doomed program points. Formal
Methods in System Design. 2010;37(2-3):171-199. doi:10.1007/s10703-010-0102-0
apa: Hoenicke, J., Leino, K., Podelski, A., Schäf, M., & Wies, T. (2010). Doomed
program points. Formal Methods in System Design. Springer. https://doi.org/10.1007/s10703-010-0102-0
chicago: Hoenicke, Jochen, Kari Leino, Andreas Podelski, Martin Schäf, and Thomas
Wies. “Doomed Program Points.” Formal Methods in System Design. Springer,
2010. https://doi.org/10.1007/s10703-010-0102-0.
ieee: J. Hoenicke, K. Leino, A. Podelski, M. Schäf, and T. Wies, “Doomed program
points,” Formal Methods in System Design, vol. 37, no. 2–3. Springer, pp.
171–199, 2010.
ista: Hoenicke J, Leino K, Podelski A, Schäf M, Wies T. 2010. Doomed program points.
Formal Methods in System Design. 37(2–3), 171–199.
mla: Hoenicke, Jochen, et al. “Doomed Program Points.” Formal Methods in System
Design, vol. 37, no. 2–3, Springer, 2010, pp. 171–99, doi:10.1007/s10703-010-0102-0.
short: J. Hoenicke, K. Leino, A. Podelski, M. Schäf, T. Wies, Formal Methods in
System Design 37 (2010) 171–199.
date_created: 2018-12-11T11:47:01Z
date_published: 2010-12-01T00:00:00Z
date_updated: 2021-01-12T08:01:28Z
day: '01'
department:
- _id: ToHe
doi: 10.1007/s10703-010-0102-0
intvolume: ' 37'
issue: 2-3
language:
- iso: eng
month: '12'
oa_version: None
page: 171 - 199
publication: Formal Methods in System Design
publication_status: published
publisher: Springer
publist_id: '7284'
quality_controlled: '1'
scopus_import: 1
status: public
title: Doomed program points
type: journal_article
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 37
year: '2010'
...