---
_id: '2847'
abstract:
- lang: eng
text: Depth-Bounded Systems form an expressive class of well-structured transition
systems. They can model a wide range of concurrent infinite-state systems including
those with dynamic thread creation, dynamically changing communication topology,
and complex shared heap structures. We present the first method to automatically
prove fair termination of depth-bounded systems. Our method uses a numerical abstraction
of the system, which we obtain by systematically augmenting an over-approximation
of the system’s reachable states with a finite set of counters. This numerical
abstraction can be analyzed with existing termination provers. What makes our
approach unique is the way in which it exploits the well-structuredness of the
analyzed system. We have implemented our work in a prototype tool and used it
to automatically prove liveness properties of complex concurrent systems, including
nonblocking algorithms such as Treiber’s stack and several distributed processes.
Many of these examples are beyond the scope of termination analyses that are based
on traditional counter abstractions.
alternative_title:
- LNCS
author:
- first_name: Kshitij
full_name: Bansal, Kshitij
last_name: Bansal
- first_name: Eric
full_name: Koskinen, Eric
last_name: Koskinen
- first_name: Thomas
full_name: Wies, Thomas
id: 447BFB88-F248-11E8-B48F-1D18A9856A87
last_name: Wies
- first_name: Damien
full_name: Zufferey, Damien
id: 4397AC76-F248-11E8-B48F-1D18A9856A87
last_name: Zufferey
orcid: 0000-0002-3197-8736
citation:
ama: Bansal K, Koskinen E, Wies T, Zufferey D. Structural Counter Abstraction. Piterman
N, Smolka S, eds. 2013;7795:62-77. doi:10.1007/978-3-642-36742-7_5
apa: 'Bansal, K., Koskinen, E., Wies, T., & Zufferey, D. (2013). Structural
Counter Abstraction. (N. Piterman & S. Smolka, Eds.). Presented at the TACAS:
Tools and Algorithms for the Construction and Analysis of Systems, Rome, Italy:
Springer. https://doi.org/10.1007/978-3-642-36742-7_5'
chicago: Bansal, Kshitij, Eric Koskinen, Thomas Wies, and Damien Zufferey. “Structural
Counter Abstraction.” Edited by Nir Piterman and Scott Smolka. Lecture Notes in
Computer Science. Springer, 2013. https://doi.org/10.1007/978-3-642-36742-7_5.
ieee: K. Bansal, E. Koskinen, T. Wies, and D. Zufferey, “Structural Counter Abstraction,”
vol. 7795. Springer, pp. 62–77, 2013.
ista: Bansal K, Koskinen E, Wies T, Zufferey D. 2013. Structural Counter Abstraction
(eds. N. Piterman & S. Smolka). 7795, 62–77.
mla: Bansal, Kshitij, et al. Structural Counter Abstraction. Edited by Nir
Piterman and Scott Smolka, vol. 7795, Springer, 2013, pp. 62–77, doi:10.1007/978-3-642-36742-7_5.
short: K. Bansal, E. Koskinen, T. Wies, D. Zufferey, 7795 (2013) 62–77.
conference:
end_date: 2013-03-24
location: Rome, Italy
name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
start_date: 2013-03-16
date_created: 2018-12-11T11:59:54Z
date_published: 2013-03-01T00:00:00Z
date_updated: 2023-09-07T11:36:36Z
day: '01'
department:
- _id: ToHe
doi: 10.1007/978-3-642-36742-7_5
ec_funded: 1
editor:
- first_name: Nir
full_name: Piterman, Nir
last_name: Piterman
- first_name: Scott
full_name: Smolka, Scott
last_name: Smolka
intvolume: ' 7795'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arise.or.at/pubpdf/Structural_Counter_Abstraction.pdf
month: '03'
oa: 1
oa_version: Submitted Version
page: 62 - 77
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
publication_status: published
publisher: Springer
publist_id: '3947'
quality_controlled: '1'
related_material:
record:
- id: '1405'
relation: dissertation_contains
status: public
scopus_import: 1
series_title: Lecture Notes in Computer Science
status: public
title: Structural Counter Abstraction
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 7795
year: '2013'
...
---
_id: '2445'
abstract:
- lang: eng
text: We develop program synthesis techniques that can help programmers fix concurrency-related
bugs. We make two new contributions to synthesis for concurrency, the first improving
the efficiency of the synthesized code, and the second improving the efficiency
of the synthesis procedure itself. The first contribution is to have the synthesis
procedure explore a variety of (sequential) semantics-preserving program transformations.
Classically, only one such transformation has been considered, namely, the insertion
of synchronization primitives (such as locks). Based on common manual bug-fixing
techniques used by Linux device-driver developers, we explore additional, more
efficient transformations, such as the reordering of independent instructions.
The second contribution is to speed up the counterexample-guided removal of concurrency
bugs within the synthesis procedure by considering partial-order traces (instead
of linear traces) as counterexamples. A partial-order error trace represents a
set of linear (interleaved) traces of a concurrent program all of which lead to
the same error. By eliminating a partial-order error trace, we eliminate in a
single iteration of the synthesis procedure all linearizations of the partial-order
trace. We evaluated our techniques on several simplified examples of real concurrency
bugs that occurred in Linux device drivers.
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
- first_name: Leonid
full_name: Ryzhyk, Leonid
last_name: Ryzhyk
- first_name: Thorsten
full_name: Tarrach, Thorsten
id: 3D6E8F2C-F248-11E8-B48F-1D18A9856A87
last_name: Tarrach
orcid: 0000-0003-4409-8487
citation:
ama: 'Cerny P, Henzinger TA, Radhakrishna A, Ryzhyk L, Tarrach T. Efficient synthesis
for concurrency by semantics-preserving transformations. In: Vol 8044. Springer;
2013:951-967. doi:10.1007/978-3-642-39799-8_68'
apa: 'Cerny, P., Henzinger, T. A., Radhakrishna, A., Ryzhyk, L., & Tarrach,
T. (2013). Efficient synthesis for concurrency by semantics-preserving transformations
(Vol. 8044, pp. 951–967). Presented at the CAV: Computer Aided Verification, St.
Petersburg, Russia: Springer. https://doi.org/10.1007/978-3-642-39799-8_68'
chicago: Cerny, Pavol, Thomas A Henzinger, Arjun Radhakrishna, Leonid Ryzhyk, and
Thorsten Tarrach. “Efficient Synthesis for Concurrency by Semantics-Preserving
Transformations,” 8044:951–67. Springer, 2013. https://doi.org/10.1007/978-3-642-39799-8_68.
ieee: 'P. Cerny, T. A. Henzinger, A. Radhakrishna, L. Ryzhyk, and T. Tarrach, “Efficient
synthesis for concurrency by semantics-preserving transformations,” presented
at the CAV: Computer Aided Verification, St. Petersburg, Russia, 2013, vol. 8044,
pp. 951–967.'
ista: 'Cerny P, Henzinger TA, Radhakrishna A, Ryzhyk L, Tarrach T. 2013. Efficient
synthesis for concurrency by semantics-preserving transformations. CAV: Computer
Aided Verification, LNCS, vol. 8044, 951–967.'
mla: Cerny, Pavol, et al. Efficient Synthesis for Concurrency by Semantics-Preserving
Transformations. Vol. 8044, Springer, 2013, pp. 951–67, doi:10.1007/978-3-642-39799-8_68.
short: P. Cerny, T.A. Henzinger, A. Radhakrishna, L. Ryzhyk, T. Tarrach, in:, Springer,
2013, pp. 951–967.
conference:
end_date: 2013-07-19
location: St. Petersburg, Russia
name: 'CAV: Computer Aided Verification'
start_date: 2013-07-13
date_created: 2018-12-11T11:57:42Z
date_published: 2013-07-01T00:00:00Z
date_updated: 2023-09-07T11:57:01Z
day: '01'
ddc:
- '000'
- '004'
department:
- _id: ToHe
doi: 10.1007/978-3-642-39799-8_68
ec_funded: 1
file:
- access_level: open_access
checksum: 70c70ca5487faba82262c63e1b678a27
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:15:37Z
date_updated: 2020-07-14T12:45:40Z
file_id: '5158'
file_name: IST-2014-199-v1+1_cav2013-final.pdf
file_size: 365548
relation: main_file
file_date_updated: 2020-07-14T12:45:40Z
has_accepted_license: '1'
intvolume: ' 8044'
language:
- iso: eng
month: '07'
oa: 1
oa_version: Submitted Version
page: 951 - 967
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
publication_status: published
publisher: Springer
publist_id: '4458'
pubrep_id: '199'
quality_controlled: '1'
related_material:
record:
- id: '1130'
relation: dissertation_contains
status: public
scopus_import: 1
status: public
title: Efficient synthesis for concurrency by semantics-preserving transformations
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 8044
year: '2013'
...
---
_id: '1384'
abstract:
- lang: eng
text: 'Software model checking, as an undecidable problem, has three possible outcomes:
(1) the program satisfies the specification, (2) the program does not satisfy
the specification, and (3) the model checker fails. The third outcome usually
manifests itself in a space-out, time-out, or one component of the verification
tool giving up; in all of these failing cases, significant computation is performed
by the verification tool before the failure, but no result is reported. We propose
to reformulate the model-checking problem as follows, in order to have the verification
tool report a summary of the performed work even in case of failure: given a program
and a specification, the model checker returns a condition Ψ - usually a state
predicate - such that the program satisfies the specification under the condition
Ψ - that is, as long as the program does not leave the states in which Ψ is satisfied.
In our experiments, we investigated as one major application of conditional model
checking the sequential combination of model checkers with information passing.
We give the condition that one model checker produces, as input to a second conditional
model checker, such that the verification problem for the second is restricted
to the part of the state space that is not covered by the condition, i.e., the
second model checker works on the problems that the first model checker could
not solve. Our experiments demonstrate that repeated application of conditional
model checkers, passing information from one model checker to the next, can significantly
improve the verification results and performance, i.e., we can now verify programs
that we could not verify before.'
acknowledgement: This research was supported by the Canadian NSERC grant RGPIN 341819-07, the ERC Advanced Grant
QUAREM, and the Austrian Science Fund NFN RiSE.
article_number: '57'
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: Mehmet
full_name: Keremoglu, Mehmet
last_name: Keremoglu
- first_name: Philipp
full_name: Wendler, Philipp
last_name: Wendler
citation:
ama: 'Beyer D, Henzinger TA, Keremoglu M, Wendler P. Conditional model checking:
A technique to pass information between verifiers. In: Proceedings of the ACM
SIGSOFT 20th International Symposium on the Foundations of Software Engineering.
ACM; 2012. doi:10.1145/2393596.2393664'
apa: 'Beyer, D., Henzinger, T. A., Keremoglu, M., & Wendler, P. (2012). Conditional
model checking: A technique to pass information between verifiers. In Proceedings
of the ACM SIGSOFT 20th International Symposium on the Foundations of Software
Engineering. Cary, NC, USA: ACM. https://doi.org/10.1145/2393596.2393664'
chicago: 'Beyer, Dirk, Thomas A Henzinger, Mehmet Keremoglu, and Philipp Wendler.
“Conditional Model Checking: A Technique to Pass Information between Verifiers.”
In Proceedings of the ACM SIGSOFT 20th International Symposium on the Foundations
of Software Engineering. ACM, 2012. https://doi.org/10.1145/2393596.2393664.'
ieee: 'D. Beyer, T. A. Henzinger, M. Keremoglu, and P. Wendler, “Conditional model
checking: A technique to pass information between verifiers,” in Proceedings
of the ACM SIGSOFT 20th International Symposium on the Foundations of Software
Engineering, Cary, NC, USA, 2012.'
ista: 'Beyer D, Henzinger TA, Keremoglu M, Wendler P. 2012. Conditional model checking:
A technique to pass information between verifiers. Proceedings of the ACM SIGSOFT
20th International Symposium on the Foundations of Software Engineering. FSE:
Foundations of Software Engineering, 57.'
mla: 'Beyer, Dirk, et al. “Conditional Model Checking: A Technique to Pass Information
between Verifiers.” Proceedings of the ACM SIGSOFT 20th International Symposium
on the Foundations of Software Engineering, 57, ACM, 2012, doi:10.1145/2393596.2393664.'
short: D. Beyer, T.A. Henzinger, M. Keremoglu, P. Wendler, in:, Proceedings of the
ACM SIGSOFT 20th International Symposium on the Foundations of Software Engineering,
ACM, 2012.
conference:
end_date: 2012-11-16
location: Cary, NC, USA
name: 'FSE: Foundations of Software Engineering'
start_date: 2012-11-11
date_created: 2018-12-11T11:51:42Z
date_published: 2012-11-01T00:00:00Z
date_updated: 2021-01-12T06:50:18Z
day: '01'
department:
- _id: ToHe
doi: 10.1145/2393596.2393664
ec_funded: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1109.6926
month: '11'
oa: 1
oa_version: Preprint
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
publication: Proceedings of the ACM SIGSOFT 20th International Symposium on the Foundations
of Software Engineering
publication_status: published
publisher: ACM
publist_id: '5826'
quality_controlled: '1'
scopus_import: 1
status: public
title: 'Conditional model checking: A technique to pass information between verifiers'
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
year: '2012'
...
---
_id: '2302'
abstract:
- lang: eng
text: 'We introduce propagation models (PMs), a formalism able to express several
kinds of equations that describe the behavior of biochemical reaction networks.
Furthermore, we introduce the propagation abstract data type (PADT), which separates
concerns regarding different numerical algorithms for the transient analysis of
biochemical reaction networks from concerns regarding their implementation, thus
allowing for portable and efficient solutions. The state of a propagation abstract
data type is given by a vector that assigns mass values to a set of nodes, and
its (next) operator propagates mass values through this set of nodes. We propose
an approximate implementation of the (next) operator, based on threshold abstraction,
which propagates only "significant" mass values and thus achieves a
compromise between efficiency and accuracy. Finally, we give three use cases for
propagation models: the chemical master equation (CME), the reaction rate equation
(RRE), and a hybrid method that combines these two equations. These three applications
use propagation models in order to propagate probabilities and/or expected values
and variances of the model''s variables.'
author:
- 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: Maria
full_name: Mateescu, Maria
id: 3B43276C-F248-11E8-B48F-1D18A9856A87
last_name: Mateescu
citation:
ama: Henzinger TA, Mateescu M. The propagation approach for computing biochemical
reaction networks. IEEE ACM Transactions on Computational Biology and Bioinformatics.
2012;10(2):310-322. doi:10.1109/TCBB.2012.91
apa: Henzinger, T. A., & Mateescu, M. (2012). The propagation approach for computing
biochemical reaction networks. IEEE ACM Transactions on Computational Biology
and Bioinformatics. IEEE. https://doi.org/10.1109/TCBB.2012.91
chicago: Henzinger, Thomas A, and Maria Mateescu. “The Propagation Approach for
Computing Biochemical Reaction Networks.” IEEE ACM Transactions on Computational
Biology and Bioinformatics. IEEE, 2012. https://doi.org/10.1109/TCBB.2012.91.
ieee: T. A. Henzinger and M. Mateescu, “The propagation approach for computing biochemical
reaction networks,” IEEE ACM Transactions on Computational Biology and Bioinformatics,
vol. 10, no. 2. IEEE, pp. 310–322, 2012.
ista: Henzinger TA, Mateescu M. 2012. The propagation approach for computing biochemical
reaction networks. IEEE ACM Transactions on Computational Biology and Bioinformatics.
10(2), 310–322.
mla: Henzinger, Thomas A., and Maria Mateescu. “The Propagation Approach for Computing
Biochemical Reaction Networks.” IEEE ACM Transactions on Computational Biology
and Bioinformatics, vol. 10, no. 2, IEEE, 2012, pp. 310–22, doi:10.1109/TCBB.2012.91.
short: T.A. Henzinger, M. Mateescu, IEEE ACM Transactions on Computational Biology
and Bioinformatics 10 (2012) 310–322.
date_created: 2018-12-11T11:56:52Z
date_published: 2012-07-03T00:00:00Z
date_updated: 2021-01-12T06:56:38Z
day: '03'
department:
- _id: ToHe
- _id: CaGu
doi: 10.1109/TCBB.2012.91
ec_funded: 1
external_id:
pmid:
- '22778152'
intvolume: ' 10'
issue: '2'
language:
- iso: eng
month: '07'
oa_version: None
page: 310 - 322
pmid: 1
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
publication: IEEE ACM Transactions on Computational Biology and Bioinformatics
publication_status: published
publisher: IEEE
publist_id: '4625'
quality_controlled: '1'
scopus_import: 1
status: public
title: The propagation approach for computing biochemical reaction networks
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 10
year: '2012'
...
---
_id: '2848'
abstract:
- lang: eng
text: We study evolutionary game theory in a setting where individuals learn from
each other. We extend the traditional approach by assuming that a population contains
individuals with different learning abilities. In particular, we explore the situation
where individuals have different search spaces, when attempting to learn the strategies
of others. The search space of an individual specifies the set of strategies learnable
by that individual. The search space is genetically given and does not change
under social evolutionary dynamics. We introduce a general framework and study
a specific example in the context of direct reciprocity. For this example, we
obtain the counter intuitive result that cooperation can only evolve for intermediate
benefit-to-cost ratios, while small and large benefit-to-cost ratios favor defection.
Our paper is a step toward making a connection between computational learning
theory and evolutionary game dynamics.
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Damien
full_name: Zufferey, Damien
id: 4397AC76-F248-11E8-B48F-1D18A9856A87
last_name: Zufferey
orcid: 0000-0002-3197-8736
- first_name: Martin
full_name: Nowak, Martin
last_name: Nowak
citation:
ama: Chatterjee K, Zufferey D, Nowak M. Evolutionary game dynamics in populations
with different learners. Journal of Theoretical Biology. 2012;301:161-173.
doi:10.1016/j.jtbi.2012.02.021
apa: Chatterjee, K., Zufferey, D., & Nowak, M. (2012). Evolutionary game dynamics
in populations with different learners. Journal of Theoretical Biology.
Elsevier. https://doi.org/10.1016/j.jtbi.2012.02.021
chicago: Chatterjee, Krishnendu, Damien Zufferey, and Martin Nowak. “Evolutionary
Game Dynamics in Populations with Different Learners.” Journal of Theoretical
Biology. Elsevier, 2012. https://doi.org/10.1016/j.jtbi.2012.02.021.
ieee: K. Chatterjee, D. Zufferey, and M. Nowak, “Evolutionary game dynamics in populations
with different learners,” Journal of Theoretical Biology, vol. 301. Elsevier,
pp. 161–173, 2012.
ista: Chatterjee K, Zufferey D, Nowak M. 2012. Evolutionary game dynamics in populations
with different learners. Journal of Theoretical Biology. 301, 161–173.
mla: Chatterjee, Krishnendu, et al. “Evolutionary Game Dynamics in Populations with
Different Learners.” Journal of Theoretical Biology, vol. 301, Elsevier,
2012, pp. 161–73, doi:10.1016/j.jtbi.2012.02.021.
short: K. Chatterjee, D. Zufferey, M. Nowak, Journal of Theoretical Biology 301
(2012) 161–173.
date_created: 2018-12-11T11:59:55Z
date_published: 2012-05-21T00:00:00Z
date_updated: 2021-01-12T07:00:12Z
day: '21'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1016/j.jtbi.2012.02.021
ec_funded: 1
external_id:
pmid:
- '22394652'
intvolume: ' 301'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://www.ncbi.nlm.nih.gov/pmc/articles/PMC3322297/
month: '05'
oa: 1
oa_version: Submitted Version
page: 161 - 173
pmid: 1
project:
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 2584A770-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: P 23499-N23
name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 2587B514-B435-11E9-9278-68D0E5697425
name: Microsoft Research Faculty Fellowship
publication: Journal of Theoretical Biology
publication_status: published
publisher: Elsevier
publist_id: '3946'
quality_controlled: '1'
scopus_import: 1
status: public
title: Evolutionary game dynamics in populations with different learners
type: journal_article
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 301
year: '2012'
...