---
_id: '3249'
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 ERC Advanced Grant QUAREM,
the FWF NFN Grant S11402-N23 (RiSE), the European Union project COMBEST and the
European Network of Excellence Artist Design.
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. Theoretical
Computer Science. 2012;413(1):21-35. doi:10.1016/j.tcs.2011.08.002
apa: Cerny, P., Henzinger, T. A., & Radhakrishna, A. (2012). Simulation distances.
Theoretical Computer Science. Elsevier. https://doi.org/10.1016/j.tcs.2011.08.002
chicago: Cerny, Pavol, Thomas A Henzinger, and Arjun Radhakrishna. “Simulation Distances.”
Theoretical Computer Science. Elsevier, 2012. https://doi.org/10.1016/j.tcs.2011.08.002.
ieee: P. Cerny, T. A. Henzinger, and A. Radhakrishna, “Simulation distances,” Theoretical
Computer Science, vol. 413, no. 1. Elsevier, pp. 21–35, 2012.
ista: Cerny P, Henzinger TA, Radhakrishna A. 2012. Simulation distances. Theoretical
Computer Science. 413(1), 21–35.
mla: Cerny, Pavol, et al. “Simulation Distances.” Theoretical Computer Science,
vol. 413, no. 1, Elsevier, 2012, pp. 21–35, doi:10.1016/j.tcs.2011.08.002.
short: P. Cerny, T.A. Henzinger, A. Radhakrishna, Theoretical Computer Science 413
(2012) 21–35.
date_created: 2018-12-11T12:02:15Z
date_published: 2012-01-06T00:00:00Z
date_updated: 2023-02-23T12:24:04Z
day: '06'
department:
- _id: ToHe
doi: 10.1016/j.tcs.2011.08.002
ec_funded: 1
intvolume: ' 413'
issue: '1'
language:
- iso: eng
month: '01'
oa_version: None
page: 21 - 35
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
- _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: Theoretical Computer Science
publication_status: published
publisher: Elsevier
publist_id: '3408'
pubrep_id: '42'
quality_controlled: '1'
related_material:
record:
- id: '4393'
relation: earlier_version
status: public
- id: '5389'
relation: earlier_version
status: public
scopus_import: 1
status: public
title: Simulation distances
type: journal_article
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 413
year: '2012'
...
---
_id: '3251'
abstract:
- lang: eng
text: Many infinite state systems can be seen as well-structured transition systems
(WSTS), i.e., systems equipped with a well-quasi-ordering on states that is also
a simulation relation. WSTS are an attractive target for formal analysis because
there exist generic algorithms that decide interesting verification problems for
this class. Among the most popular algorithms are acceleration-based forward analyses
for computing the covering set. Termination of these algorithms can only be guaranteed
for flattable WSTS. Yet, many WSTS of practical interest are not flattable and
the question whether any given WSTS is flattable is itself undecidable. We therefore
propose an analysis that computes the covering set and captures the essence of
acceleration-based algorithms, but sacrifices precision for guaranteed termination.
Our analysis is an abstract interpretation whose abstract domain builds on the
ideal completion of the well-quasi-ordered state space, and a widening operator
that mimics acceleration and controls the loss of precision of the analysis. We
present instances of our framework for various classes of WSTS. Our experience
with a prototype implementation indicates that, despite the inherent precision
loss, our analysis often computes the precise covering set of the analyzed system.
acknowledgement: This research was supported in part by the European Research Council
(ERC) Advanced Investigator Grant QUAREM and by the Austrian Science Fund (FWF)
project S11402-N23.
alternative_title:
- LNCS
author:
- first_name: Damien
full_name: Zufferey, Damien
id: 4397AC76-F248-11E8-B48F-1D18A9856A87
last_name: Zufferey
orcid: 0000-0002-3197-8736
- first_name: Thomas
full_name: Wies, Thomas
id: 447BFB88-F248-11E8-B48F-1D18A9856A87
last_name: Wies
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
citation:
ama: 'Zufferey D, Wies T, Henzinger TA. Ideal abstractions for well structured transition
systems. In: Vol 7148. Springer; 2012:445-460. doi:10.1007/978-3-642-27940-9_29'
apa: 'Zufferey, D., Wies, T., & Henzinger, T. A. (2012). Ideal abstractions
for well structured transition systems (Vol. 7148, pp. 445–460). Presented at
the VMCAI: Verification, Model Checking and Abstract Interpretation, Philadelphia,
PA, USA: Springer. https://doi.org/10.1007/978-3-642-27940-9_29'
chicago: Zufferey, Damien, Thomas Wies, and Thomas A Henzinger. “Ideal Abstractions
for Well Structured Transition Systems,” 7148:445–60. Springer, 2012. https://doi.org/10.1007/978-3-642-27940-9_29.
ieee: 'D. Zufferey, T. Wies, and T. A. Henzinger, “Ideal abstractions for well structured
transition systems,” presented at the VMCAI: Verification, Model Checking and
Abstract Interpretation, Philadelphia, PA, USA, 2012, vol. 7148, pp. 445–460.'
ista: 'Zufferey D, Wies T, Henzinger TA. 2012. Ideal abstractions for well structured
transition systems. VMCAI: Verification, Model Checking and Abstract Interpretation,
LNCS, vol. 7148, 445–460.'
mla: Zufferey, Damien, et al. Ideal Abstractions for Well Structured Transition
Systems. Vol. 7148, Springer, 2012, pp. 445–60, doi:10.1007/978-3-642-27940-9_29.
short: D. Zufferey, T. Wies, T.A. Henzinger, in:, Springer, 2012, pp. 445–460.
conference:
end_date: 2012-01-24
location: Philadelphia, PA, USA
name: 'VMCAI: Verification, Model Checking and Abstract Interpretation'
start_date: 2012-01-22
date_created: 2018-12-11T12:02:16Z
date_published: 2012-01-01T00:00:00Z
date_updated: 2023-09-07T11:36:36Z
day: '01'
ddc:
- '000'
- '005'
department:
- _id: ToHe
doi: 10.1007/978-3-642-27940-9_29
ec_funded: 1
file:
- access_level: open_access
checksum: f2f0d55efa32309ad1fe65a5fcaad90c
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:09:35Z
date_updated: 2020-07-14T12:46:05Z
file_id: '4759'
file_name: IST-2012-100-v1+1_Ideal_abstractions_for_well-structured_transition_systems.pdf
file_size: 217104
relation: main_file
file_date_updated: 2020-07-14T12:46:05Z
has_accepted_license: '1'
intvolume: ' 7148'
language:
- iso: eng
month: '01'
oa: 1
oa_version: Submitted Version
page: 445 - 460
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: '3406'
pubrep_id: '100'
quality_controlled: '1'
related_material:
record:
- id: '1405'
relation: dissertation_contains
status: public
status: public
title: Ideal abstractions for well structured transition systems
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 7148
year: '2012'
...
---
_id: '3253'
abstract:
- lang: eng
text: We describe a framework for reasoning about programs with lists carrying integer
numerical data. We use abstract domains to describe and manipulate complex constraints
on configurations of these programs mixing constraints on the shape of the heap,
sizes of the lists, on the multisets of data stored in these lists, and on the
data at their different positions. Moreover, we provide powerful techniques for
automatic validation of Hoare-triples and invariant checking, as well as for automatic
synthesis of invariants and procedure summaries using modular inter-procedural
analysis. The approach has been implemented in a tool called Celia and experimented
successfully on a large benchmark of programs.
acknowledgement: This work was partly supported by the French National Research Agency
(ANR) project Veridyc (ANR-09-SEGI-016).
alternative_title:
- LNCS
author:
- first_name: Ahmed
full_name: Bouajjani, Ahmed
last_name: Bouajjani
- first_name: Cezara
full_name: Dragoi, Cezara
id: 2B2B5ED0-F248-11E8-B48F-1D18A9856A87
last_name: Dragoi
- first_name: Constantin
full_name: Enea, Constantin
last_name: Enea
- first_name: Mihaela
full_name: Sighireanu, Mihaela
last_name: Sighireanu
citation:
ama: 'Bouajjani A, Dragoi C, Enea C, Sighireanu M. Abstract domains for automated
reasoning about list manipulating programs with infinite data. In: Vol 7148. Springer;
2012:1-22. doi:10.1007/978-3-642-27940-9_1'
apa: 'Bouajjani, A., Dragoi, C., Enea, C., & Sighireanu, M. (2012). Abstract
domains for automated reasoning about list manipulating programs with infinite
data (Vol. 7148, pp. 1–22). Presented at the VMCAI: Verification, Model Checking
and Abstract Interpretation, Philadelphia, PA, USA: Springer. https://doi.org/10.1007/978-3-642-27940-9_1'
chicago: Bouajjani, Ahmed, Cezara Dragoi, Constantin Enea, and Mihaela Sighireanu.
“Abstract Domains for Automated Reasoning about List Manipulating Programs with
Infinite Data,” 7148:1–22. Springer, 2012. https://doi.org/10.1007/978-3-642-27940-9_1.
ieee: 'A. Bouajjani, C. Dragoi, C. Enea, and M. Sighireanu, “Abstract domains for
automated reasoning about list manipulating programs with infinite data,” presented
at the VMCAI: Verification, Model Checking and Abstract Interpretation, Philadelphia,
PA, USA, 2012, vol. 7148, pp. 1–22.'
ista: 'Bouajjani A, Dragoi C, Enea C, Sighireanu M. 2012. Abstract domains for automated
reasoning about list manipulating programs with infinite data. VMCAI: Verification,
Model Checking and Abstract Interpretation, LNCS, vol. 7148, 1–22.'
mla: Bouajjani, Ahmed, et al. Abstract Domains for Automated Reasoning about
List Manipulating Programs with Infinite Data. Vol. 7148, Springer, 2012,
pp. 1–22, doi:10.1007/978-3-642-27940-9_1.
short: A. Bouajjani, C. Dragoi, C. Enea, M. Sighireanu, in:, Springer, 2012, pp.
1–22.
conference:
end_date: 2012-01-24
location: Philadelphia, PA, USA
name: 'VMCAI: Verification, Model Checking and Abstract Interpretation'
start_date: 2012-01-22
date_created: 2018-12-11T12:02:17Z
date_published: 2012-02-26T00:00:00Z
date_updated: 2021-01-12T07:42:09Z
day: '26'
department:
- _id: ToHe
doi: 10.1007/978-3-642-27940-9_1
intvolume: ' 7148'
language:
- iso: eng
month: '02'
oa_version: None
page: 1 - 22
publication_status: published
publisher: Springer
publist_id: '3404'
quality_controlled: '1'
status: public
title: Abstract domains for automated reasoning about list manipulating programs with
infinite data
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 7148
year: '2012'
...
---
_id: '10903'
abstract:
- lang: eng
text: We propose a logic-based framework for automated reasoning about sequential
programs manipulating singly-linked lists and arrays with unbounded data. We introduce
the logic SLAD, which allows combining shape constraints, written in a fragment
of Separation Logic, with data and size constraints. We address the problem of
checking the entailment between SLAD formulas, which is crucial in performing
pre-post condition reasoning. Although this problem is undecidable in general
for SLAD, we propose a sound and powerful procedure that is able to solve this
problem for a large class of formulas, beyond the capabilities of existing techniques
and tools. We prove that this procedure is complete, i.e., it is actually a decision
procedure for this problem, for an important fragment of SLAD including known
decidable logics. We implemented this procedure and shown its preciseness and
its efficiency on a significant benchmark of formulas.
acknowledgement: This work has been partially supported by the French ANR project
Veridyc
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Ahmed
full_name: Bouajjani, Ahmed
last_name: Bouajjani
- first_name: Cezara
full_name: Dragoi, Cezara
id: 2B2B5ED0-F248-11E8-B48F-1D18A9856A87
last_name: Dragoi
- first_name: Constantin
full_name: Enea, Constantin
last_name: Enea
- first_name: Mihaela
full_name: Sighireanu, Mihaela
last_name: Sighireanu
citation:
ama: 'Bouajjani A, Dragoi C, Enea C, Sighireanu M. Accurate invariant checking for
programs manipulating lists and arrays with infinite data. In: Automated Technology
for Verification and Analysis. Vol 7561. LNCS. Berlin, Heidelberg: Springer;
2012:167-182. doi:10.1007/978-3-642-33386-6_14'
apa: 'Bouajjani, A., Dragoi, C., Enea, C., & Sighireanu, M. (2012). Accurate
invariant checking for programs manipulating lists and arrays with infinite data.
In Automated Technology for Verification and Analysis (Vol. 7561, pp. 167–182).
Berlin, Heidelberg: Springer. https://doi.org/10.1007/978-3-642-33386-6_14'
chicago: 'Bouajjani, Ahmed, Cezara Dragoi, Constantin Enea, and Mihaela Sighireanu.
“Accurate Invariant Checking for Programs Manipulating Lists and Arrays with Infinite
Data.” In Automated Technology for Verification and Analysis, 7561:167–82.
LNCS. Berlin, Heidelberg: Springer, 2012. https://doi.org/10.1007/978-3-642-33386-6_14.'
ieee: A. Bouajjani, C. Dragoi, C. Enea, and M. Sighireanu, “Accurate invariant checking
for programs manipulating lists and arrays with infinite data,” in Automated
Technology for Verification and Analysis, Thiruvananthapuram, India, 2012,
vol. 7561, pp. 167–182.
ista: 'Bouajjani A, Dragoi C, Enea C, Sighireanu M. 2012. Accurate invariant checking
for programs manipulating lists and arrays with infinite data. Automated Technology
for Verification and Analysis. ATVA: Automated Technology for Verification and
AnalysisLNCS, LNCS, vol. 7561, 167–182.'
mla: Bouajjani, Ahmed, et al. “Accurate Invariant Checking for Programs Manipulating
Lists and Arrays with Infinite Data.” Automated Technology for Verification
and Analysis, vol. 7561, Springer, 2012, pp. 167–82, doi:10.1007/978-3-642-33386-6_14.
short: A. Bouajjani, C. Dragoi, C. Enea, M. Sighireanu, in:, Automated Technology
for Verification and Analysis, Springer, Berlin, Heidelberg, 2012, pp. 167–182.
conference:
end_date: 2012-10-06
location: Thiruvananthapuram, India
name: 'ATVA: Automated Technology for Verification and Analysis'
start_date: 2012-10-03
date_created: 2022-03-21T07:58:39Z
date_published: 2012-10-15T00:00:00Z
date_updated: 2023-09-05T14:07:24Z
day: '15'
department:
- _id: ToHe
doi: 10.1007/978-3-642-33386-6_14
intvolume: ' 7561'
language:
- iso: eng
month: '10'
oa_version: None
page: 167-182
place: Berlin, Heidelberg
publication: Automated Technology for Verification and Analysis
publication_identifier:
eisbn:
- '9783642333866'
eissn:
- 1611-3349
isbn:
- '9783642333859'
issn:
- 0302-9743
publication_status: published
publisher: Springer
quality_controlled: '1'
scopus_import: '1'
series_title: LNCS
status: public
title: Accurate invariant checking for programs manipulating lists and arrays with
infinite data
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 7561
year: '2012'
...
---
_id: '10906'
abstract:
- lang: eng
text: HSF(C) is a tool that automates verification of safety and liveness properties
for C programs. This paper describes the verification approach taken by HSF(C)
and provides instructions on how to install and use the tool.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Sergey
full_name: Grebenshchikov, Sergey
last_name: Grebenshchikov
- first_name: Ashutosh
full_name: Gupta, Ashutosh
id: 335E5684-F248-11E8-B48F-1D18A9856A87
last_name: Gupta
- first_name: Nuno P.
full_name: Lopes, Nuno P.
last_name: Lopes
- first_name: Corneliu
full_name: Popeea, Corneliu
last_name: Popeea
- first_name: Andrey
full_name: Rybalchenko, Andrey
last_name: Rybalchenko
citation:
ama: 'Grebenshchikov S, Gupta A, Lopes NP, Popeea C, Rybalchenko A. HSF(C): A software
verifier based on Horn clauses. In: Flanagan C, König B, eds. Tools and Algorithms
for the Construction and Analysis of Systems. Vol 7214. LNCS. Berlin, Heidelberg:
Springer; 2012:549-551. doi:10.1007/978-3-642-28756-5_46'
apa: 'Grebenshchikov, S., Gupta, A., Lopes, N. P., Popeea, C., & Rybalchenko,
A. (2012). HSF(C): A software verifier based on Horn clauses. In C. Flanagan &
B. König (Eds.), Tools and Algorithms for the Construction and Analysis of
Systems (Vol. 7214, pp. 549–551). Berlin, Heidelberg: Springer. https://doi.org/10.1007/978-3-642-28756-5_46'
chicago: 'Grebenshchikov, Sergey, Ashutosh Gupta, Nuno P. Lopes, Corneliu Popeea,
and Andrey Rybalchenko. “HSF(C): A Software Verifier Based on Horn Clauses.” In
Tools and Algorithms for the Construction and Analysis of Systems, edited
by Cormac Flanagan and Barbara König, 7214:549–51. LNCS. Berlin, Heidelberg: Springer,
2012. https://doi.org/10.1007/978-3-642-28756-5_46.'
ieee: 'S. Grebenshchikov, A. Gupta, N. P. Lopes, C. Popeea, and A. Rybalchenko,
“HSF(C): A software verifier based on Horn clauses,” in Tools and Algorithms
for the Construction and Analysis of Systems, Tallinn, Estonia, 2012, vol.
7214, pp. 549–551.'
ista: 'Grebenshchikov S, Gupta A, Lopes NP, Popeea C, Rybalchenko A. 2012. HSF(C):
A software verifier based on Horn clauses. Tools and Algorithms for the Construction
and Analysis of Systems. TACAS: Tools and Algorithms for the Construction and
Analysis of SystemsLNCS, LNCS, vol. 7214, 549–551.'
mla: 'Grebenshchikov, Sergey, et al. “HSF(C): A Software Verifier Based on Horn
Clauses.” Tools and Algorithms for the Construction and Analysis of Systems,
edited by Cormac Flanagan and Barbara König, vol. 7214, Springer, 2012, pp. 549–51,
doi:10.1007/978-3-642-28756-5_46.'
short: S. Grebenshchikov, A. Gupta, N.P. Lopes, C. Popeea, A. Rybalchenko, in:,
C. Flanagan, B. König (Eds.), Tools and Algorithms for the Construction and Analysis
of Systems, Springer, Berlin, Heidelberg, 2012, pp. 549–551.
conference:
end_date: 2012-04-01
location: Tallinn, Estonia
name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
start_date: 2012-03-24
date_created: 2022-03-21T08:03:30Z
date_published: 2012-04-01T00:00:00Z
date_updated: 2023-09-05T14:09:54Z
day: '01'
department:
- _id: ToHe
doi: 10.1007/978-3-642-28756-5_46
editor:
- first_name: Cormac
full_name: Flanagan, Cormac
last_name: Flanagan
- first_name: Barbara
full_name: König, Barbara
last_name: König
intvolume: ' 7214'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.1007/978-3-642-28756-5_46
month: '04'
oa: 1
oa_version: Published Version
page: 549-551
place: Berlin, Heidelberg
publication: Tools and Algorithms for the Construction and Analysis of Systems
publication_identifier:
eisbn:
- '9783642287565'
eissn:
- 1611-3349
isbn:
- '9783642287558'
issn:
- 0302-9743
publication_status: published
publisher: Springer
quality_controlled: '1'
scopus_import: '1'
series_title: LNCS
status: public
title: 'HSF(C): A software verifier based on Horn clauses'
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 7214
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: '494'
abstract:
- lang: eng
text: We solve the longstanding open problems of the blow-up involved in the translations,
when possible, of a nondeterministic Büchi word automaton (NBW) to a nondeterministic
co-Büchi word automaton (NCW) and to a deterministic co-Büchi word automaton (DCW).
For the NBW to NCW translation, the currently known upper bound is 2o(nlog n)
and the lower bound is 1.5n. We improve the upper bound to n2n and describe a
matching lower bound of 2ω(n). For the NBW to DCW translation, the currently known
upper bound is 2o(nlog n). We improve it to 2 o(n), which is asymptotically tight.
Both of our upper-bound constructions are based on a simple subset construction,
do not involve intermediate automata with richer acceptance conditions, and can
be implemented symbolically. We continue and solve the open problems of translating
nondeterministic Streett, Rabin, Muller, and parity word automata to NCW and to
DCW. Going via an intermediate NBW is not optimal and we describe direct, simple,
and asymptotically tight constructions, involving a 2o(n) blow-up. The constructions
are variants of the subset construction, providing a unified approach for translating
all common classes of automata to NCW and DCW. Beyond the theoretical importance
of the results, we point to numerous applications of the new constructions. In
particular, they imply a simple subset-construction based translation, when possible,
of LTL to deterministic Büchi word automata.
article_number: '29'
author:
- first_name: Udi
full_name: Boker, Udi
id: 31E297B6-F248-11E8-B48F-1D18A9856A87
last_name: Boker
- first_name: Orna
full_name: Kupferman, Orna
last_name: Kupferman
citation:
ama: Boker U, Kupferman O. Translating to Co-Büchi made tight, unified, and useful.
ACM Transactions on Computational Logic (TOCL). 2012;13(4). doi:10.1145/2362355.2362357
apa: Boker, U., & Kupferman, O. (2012). Translating to Co-Büchi made tight,
unified, and useful. ACM Transactions on Computational Logic (TOCL). ACM.
https://doi.org/10.1145/2362355.2362357
chicago: Boker, Udi, and Orna Kupferman. “Translating to Co-Büchi Made Tight, Unified,
and Useful.” ACM Transactions on Computational Logic (TOCL). ACM, 2012.
https://doi.org/10.1145/2362355.2362357.
ieee: U. Boker and O. Kupferman, “Translating to Co-Büchi made tight, unified, and
useful,” ACM Transactions on Computational Logic (TOCL), vol. 13, no. 4.
ACM, 2012.
ista: Boker U, Kupferman O. 2012. Translating to Co-Büchi made tight, unified, and
useful. ACM Transactions on Computational Logic (TOCL). 13(4), 29.
mla: Boker, Udi, and Orna Kupferman. “Translating to Co-Büchi Made Tight, Unified,
and Useful.” ACM Transactions on Computational Logic (TOCL), vol. 13, no.
4, 29, ACM, 2012, doi:10.1145/2362355.2362357.
short: U. Boker, O. Kupferman, ACM Transactions on Computational Logic (TOCL) 13
(2012).
date_created: 2018-12-11T11:46:47Z
date_published: 2012-10-01T00:00:00Z
date_updated: 2021-01-12T08:01:03Z
day: '01'
department:
- _id: ToHe
doi: 10.1145/2362355.2362357
intvolume: ' 13'
issue: '4'
language:
- iso: eng
month: '10'
oa_version: None
publication: ACM Transactions on Computational Logic (TOCL)
publication_status: published
publisher: ACM
publist_id: '7326'
quality_controlled: '1'
scopus_import: 1
status: public
title: Translating to Co-Büchi made tight, unified, and useful
type: journal_article
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 13
year: '2012'
...
---
_id: '5745'
article_processing_charge: No
author:
- first_name: Ashutosh
full_name: Gupta, Ashutosh
last_name: Gupta
citation:
ama: 'Gupta A. Improved Single Pass Algorithms for Resolution Proof Reduction. In:
Automated Technology for Verification and Analysis. Vol 7561. LNCS. Berlin,
Heidelberg: Springer Berlin Heidelberg; 2012:107-121. doi:10.1007/978-3-642-33386-6_10'
apa: 'Gupta, A. (2012). Improved Single Pass Algorithms for Resolution Proof Reduction.
In Automated Technology for Verification and Analysis (Vol. 7561, pp. 107–121).
Berlin, Heidelberg: Springer Berlin Heidelberg. https://doi.org/10.1007/978-3-642-33386-6_10'
chicago: 'Gupta, Ashutosh. “Improved Single Pass Algorithms for Resolution Proof
Reduction.” In Automated Technology for Verification and Analysis, 7561:107–21.
LNCS. Berlin, Heidelberg: Springer Berlin Heidelberg, 2012. https://doi.org/10.1007/978-3-642-33386-6_10.'
ieee: 'A. Gupta, “Improved Single Pass Algorithms for Resolution Proof Reduction,”
in Automated Technology for Verification and Analysis, vol. 7561, Berlin,
Heidelberg: Springer Berlin Heidelberg, 2012, pp. 107–121.'
ista: 'Gupta A. 2012.Improved Single Pass Algorithms for Resolution Proof Reduction.
In: Automated Technology for Verification and Analysis. vol. 7561, 107–121.'
mla: Gupta, Ashutosh. “Improved Single Pass Algorithms for Resolution Proof Reduction.”
Automated Technology for Verification and Analysis, vol. 7561, Springer
Berlin Heidelberg, 2012, pp. 107–21, doi:10.1007/978-3-642-33386-6_10.
short: A. Gupta, in:, Automated Technology for Verification and Analysis, Springer
Berlin Heidelberg, Berlin, Heidelberg, 2012, pp. 107–121.
conference:
end_date: 2012-10-06
location: Thiruvananthapuram, Kerala, India
name: ATVA 2012
start_date: 2012-10-03
date_created: 2018-12-18T13:01:46Z
date_published: 2012-01-01T00:00:00Z
date_updated: 2023-09-05T14:15:29Z
ddc:
- '005'
department:
- _id: ToHe
doi: 10.1007/978-3-642-33386-6_10
ec_funded: 1
file:
- access_level: open_access
checksum: 68415837a315de3cc4d120f6019d752c
content_type: application/pdf
creator: dernst
date_created: 2018-12-18T13:07:35Z
date_updated: 2020-07-14T12:47:10Z
file_id: '5746'
file_name: 2012_ATVA_Gupta.pdf
file_size: 465502
relation: main_file
file_date_updated: 2020-07-14T12:47:10Z
has_accepted_license: '1'
intvolume: ' 7561'
language:
- iso: eng
oa: 1
oa_version: None
page: 107-121
place: Berlin, Heidelberg
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
publication: Automated Technology for Verification and Analysis
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783642333859'
- '9783642333866'
issn:
- 0302-9743
publication_status: published
publisher: Springer Berlin Heidelberg
pubrep_id: '180'
quality_controlled: '1'
series_title: LNCS
status: public
title: Improved Single Pass Algorithms for Resolution Proof Reduction
type: book_chapter
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 7561
year: '2012'
...
---
_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: '3836'
abstract:
- lang: eng
text: Hierarchical Timing Language (HTL) is a coordination language for distributed,
hard real-time applications. HTL is a hierarchical extension of Giotto and, like
its predecessor, based on the logical execution time (LET) paradigm of real-time
programming. Giotto is compiled into code for a virtual machine, called the EmbeddedMachine
(or E machine). If HTL is targeted to the E machine, then the hierarchicalprogram
structure needs to be flattened; the flattening makes separatecompilation difficult,
and may result in E machinecode of exponential size. In this paper, we propose
a generalization of the E machine, which supports a hierarchicalprogram structure
at runtime through real-time trigger mechanisms that are arranged in a tree. We
present the generalized E machine, and a modular compiler for HTL that generates
code of linear size. The compiler may generate code for any part of a given HTL
program separately in any order.
author:
- first_name: Arkadeb
full_name: Ghosal, Arkadeb
last_name: Ghosal
- first_name: Daniel
full_name: Iercan, Daniel
last_name: Iercan
- first_name: Christoph
full_name: Kirsch, Christoph
last_name: Kirsch
- 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: Alberto
full_name: Sangiovanni Vincentelli, Alberto
last_name: Sangiovanni Vincentelli
citation:
ama: Ghosal A, Iercan D, Kirsch C, Henzinger TA, Sangiovanni Vincentelli A. Separate
compilation of hierarchical real-time programs into linear-bounded embedded machine
code. Science of Computer Programming. 2012;77(2):96-112. doi:10.1016/j.scico.2010.06.004
apa: Ghosal, A., Iercan, D., Kirsch, C., Henzinger, T. A., & Sangiovanni Vincentelli,
A. (2012). Separate compilation of hierarchical real-time programs into linear-bounded
embedded machine code. Science of Computer Programming. Elsevier. https://doi.org/10.1016/j.scico.2010.06.004
chicago: Ghosal, Arkadeb, Daniel Iercan, Christoph Kirsch, Thomas A Henzinger, and
Alberto Sangiovanni Vincentelli. “Separate Compilation of Hierarchical Real-Time
Programs into Linear-Bounded Embedded Machine Code.” Science of Computer Programming.
Elsevier, 2012. https://doi.org/10.1016/j.scico.2010.06.004.
ieee: A. Ghosal, D. Iercan, C. Kirsch, T. A. Henzinger, and A. Sangiovanni Vincentelli,
“Separate compilation of hierarchical real-time programs into linear-bounded embedded
machine code,” Science of Computer Programming, vol. 77, no. 2. Elsevier,
pp. 96–112, 2012.
ista: Ghosal A, Iercan D, Kirsch C, Henzinger TA, Sangiovanni Vincentelli A. 2012.
Separate compilation of hierarchical real-time programs into linear-bounded embedded
machine code. Science of Computer Programming. 77(2), 96–112.
mla: Ghosal, Arkadeb, et al. “Separate Compilation of Hierarchical Real-Time Programs
into Linear-Bounded Embedded Machine Code.” Science of Computer Programming,
vol. 77, no. 2, Elsevier, 2012, pp. 96–112, doi:10.1016/j.scico.2010.06.004.
short: A. Ghosal, D. Iercan, C. Kirsch, T.A. Henzinger, A. Sangiovanni Vincentelli,
Science of Computer Programming 77 (2012) 96–112.
date_created: 2018-12-11T12:05:26Z
date_published: 2012-02-01T00:00:00Z
date_updated: 2021-01-12T07:52:32Z
day: '01'
department:
- _id: ToHe
doi: 10.1016/j.scico.2010.06.004
intvolume: ' 77'
issue: '2'
language:
- iso: eng
month: '02'
oa_version: None
page: 96 - 112
publication: Science of Computer Programming
publication_status: published
publisher: Elsevier
publist_id: '2370'
quality_controlled: '1'
scopus_import: 1
status: public
title: Separate compilation of hierarchical real-time programs into linear-bounded
embedded machine code
type: journal_article
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 77
year: '2012'
...
---
_id: '3846'
abstract:
- lang: eng
text: We summarize classical and recent results about two-player games played on
graphs with ω-regular objectives. These games have applications in the verification
and synthesis of reactive systems. Important distinctions are whether a graph
game is turn-based or concurrent; deterministic or stochastic; zero-sum or not.
We cluster known results and open problems according to these classifications.
acknowledgement: This research was supported in part by the ONR grant N00014-02-1-0671,
by the AFOSR MURI grant F49620-00-1-0327, and by the NSF grants CCR-9988172, CCR-0085949,
and CCR-0225610.
article_processing_charge: No
article_type: original
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
citation:
ama: Chatterjee K, Henzinger TA. A survey of stochastic ω regular games. Journal
of Computer and System Sciences. 2012;78(2):394-413. doi:10.1016/j.jcss.2011.05.002
apa: Chatterjee, K., & Henzinger, T. A. (2012). A survey of stochastic ω regular
games. Journal of Computer and System Sciences. Elsevier. https://doi.org/10.1016/j.jcss.2011.05.002
chicago: Chatterjee, Krishnendu, and Thomas A Henzinger. “A Survey of Stochastic
ω Regular Games.” Journal of Computer and System Sciences. Elsevier, 2012.
https://doi.org/10.1016/j.jcss.2011.05.002.
ieee: K. Chatterjee and T. A. Henzinger, “A survey of stochastic ω regular games,”
Journal of Computer and System Sciences, vol. 78, no. 2. Elsevier, pp.
394–413, 2012.
ista: Chatterjee K, Henzinger TA. 2012. A survey of stochastic ω regular games.
Journal of Computer and System Sciences. 78(2), 394–413.
mla: Chatterjee, Krishnendu, and Thomas A. Henzinger. “A Survey of Stochastic ω
Regular Games.” Journal of Computer and System Sciences, vol. 78, no. 2,
Elsevier, 2012, pp. 394–413, doi:10.1016/j.jcss.2011.05.002.
short: K. Chatterjee, T.A. Henzinger, Journal of Computer and System Sciences 78
(2012) 394–413.
date_created: 2018-12-11T12:05:29Z
date_published: 2012-03-02T00:00:00Z
date_updated: 2022-05-24T08:00:54Z
day: '02'
ddc:
- '000'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1016/j.jcss.2011.05.002
file:
- access_level: open_access
checksum: 241b939deb4517cdd4426d49c67e3fa2
content_type: application/pdf
creator: kschuh
date_created: 2019-01-29T10:54:28Z
date_updated: 2020-07-14T12:46:17Z
file_id: '5897'
file_name: a_survey_of_stochastic_omega-regular_games.pdf
file_size: 336450
relation: main_file
file_date_updated: 2020-07-14T12:46:17Z
has_accepted_license: '1'
intvolume: ' 78'
issue: '2'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.1016/j.jcss.2011.05.002
month: '03'
oa: 1
oa_version: Submitted Version
page: 394 - 413
publication: Journal of Computer and System Sciences
publication_status: published
publisher: Elsevier
publist_id: '2341'
quality_controlled: '1'
scopus_import: '1'
status: public
title: A survey of stochastic ω regular games
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 78
year: '2012'
...
---
_id: '3264'
abstract:
- lang: eng
text: Verification of programs with procedures, multi-threaded programs, and higher-order
functional programs can be effectively au- tomated using abstraction and refinement
schemes that rely on spurious counterexamples for abstraction discovery. The analysis
of counterexam- ples can be automated by a series of interpolation queries, or,
alterna- tively, as a constraint solving query expressed by a set of recursion
free Horn clauses. (A set of interpolation queries can be formulated as a single
constraint over Horn clauses with linear dependency structure between the unknown
relations.) In this paper we present an algorithm for solving recursion free Horn
clauses over a combined theory of linear real/rational arithmetic and uninterpreted
functions. Our algorithm performs resolu- tion to deal with the clausal structure
and relies on partial solutions to deal with (non-local) instances of functionality
axioms.
alternative_title:
- LNCS
author:
- first_name: Ashutosh
full_name: Gupta, Ashutosh
id: 335E5684-F248-11E8-B48F-1D18A9856A87
last_name: Gupta
- first_name: Corneliu
full_name: Popeea, Corneliu
last_name: Popeea
- first_name: Andrey
full_name: Rybalchenko, Andrey
last_name: Rybalchenko
citation:
ama: 'Gupta A, Popeea C, Rybalchenko A. Solving recursion-free Horn clauses over
LI+UIF. In: Yang H, ed. Vol 7078. Springer; 2011:188-203. doi:10.1007/978-3-642-25318-8_16'
apa: 'Gupta, A., Popeea, C., & Rybalchenko, A. (2011). Solving recursion-free
Horn clauses over LI+UIF. In H. Yang (Ed.) (Vol. 7078, pp. 188–203). Presented
at the APLAS: Asian Symposium on Programming Languages and Systems, Kenting, Taiwan:
Springer. https://doi.org/10.1007/978-3-642-25318-8_16'
chicago: Gupta, Ashutosh, Corneliu Popeea, and Andrey Rybalchenko. “Solving Recursion-Free
Horn Clauses over LI+UIF.” edited by Hongseok Yang, 7078:188–203. Springer, 2011.
https://doi.org/10.1007/978-3-642-25318-8_16.
ieee: 'A. Gupta, C. Popeea, and A. Rybalchenko, “Solving recursion-free Horn clauses
over LI+UIF,” presented at the APLAS: Asian Symposium on Programming Languages
and Systems, Kenting, Taiwan, 2011, vol. 7078, pp. 188–203.'
ista: 'Gupta A, Popeea C, Rybalchenko A. 2011. Solving recursion-free Horn clauses
over LI+UIF. APLAS: Asian Symposium on Programming Languages and Systems, LNCS,
vol. 7078, 188–203.'
mla: Gupta, Ashutosh, et al. Solving Recursion-Free Horn Clauses over LI+UIF.
Edited by Hongseok Yang, vol. 7078, Springer, 2011, pp. 188–203, doi:10.1007/978-3-642-25318-8_16.
short: A. Gupta, C. Popeea, A. Rybalchenko, in:, H. Yang (Ed.), Springer, 2011,
pp. 188–203.
conference:
end_date: 2011-12-07
location: Kenting, Taiwan
name: 'APLAS: Asian Symposium on Programming Languages and Systems'
start_date: 2011-12-05
date_created: 2018-12-11T12:02:20Z
date_published: 2011-12-05T00:00:00Z
date_updated: 2021-01-12T07:42:15Z
day: '05'
department:
- _id: ToHe
doi: 10.1007/978-3-642-25318-8_16
ec_funded: 1
editor:
- first_name: Hongseok
full_name: Yang, Hongseok
last_name: Yang
intvolume: ' 7078'
language:
- iso: eng
month: '12'
oa_version: None
page: 188 - 203
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
publication_status: published
publisher: Springer
publist_id: '3383'
quality_controlled: '1'
status: public
title: Solving recursion-free Horn clauses over LI+UIF
type: conference
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
volume: 7078
year: '2011'
...
---
_id: '3299'
abstract:
- lang: eng
text: 'We introduce propagation models, a formalism designed to support general
and efficient data structures for the transient analysis of biochemical reaction
networks. We give two use cases for propagation abstract data types: the uniformization
method and numerical integration. We also sketch an implementation of a propagation
abstract data type, which uses abstraction to approximate states.'
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
last_name: Mateescu
citation:
ama: 'Henzinger TA, Mateescu M. Propagation models for computing biochemical reaction
networks. In: Springer; 2011:1-3. doi:10.1145/2037509.2037510'
apa: 'Henzinger, T. A., & Mateescu, M. (2011). Propagation models for computing
biochemical reaction networks (pp. 1–3). Presented at the CMSB: Computational
Methods in Systems Biology, Paris, France: Springer. https://doi.org/10.1145/2037509.2037510'
chicago: Henzinger, Thomas A, and Maria Mateescu. “Propagation Models for Computing
Biochemical Reaction Networks,” 1–3. Springer, 2011. https://doi.org/10.1145/2037509.2037510.
ieee: 'T. A. Henzinger and M. Mateescu, “Propagation models for computing biochemical
reaction networks,” presented at the CMSB: Computational Methods in Systems Biology,
Paris, France, 2011, pp. 1–3.'
ista: 'Henzinger TA, Mateescu M. 2011. Propagation models for computing biochemical
reaction networks. CMSB: Computational Methods in Systems Biology, 1–3.'
mla: Henzinger, Thomas A., and Maria Mateescu. Propagation Models for Computing
Biochemical Reaction Networks. Springer, 2011, pp. 1–3, doi:10.1145/2037509.2037510.
short: T.A. Henzinger, M. Mateescu, in:, Springer, 2011, pp. 1–3.
conference:
end_date: 2011-09-23
location: Paris, France
name: 'CMSB: Computational Methods in Systems Biology'
start_date: 2011-09-21
date_created: 2018-12-11T12:02:32Z
date_published: 2011-09-21T00:00:00Z
date_updated: 2021-01-12T07:42:29Z
day: '21'
ddc:
- '000'
- '004'
department:
- _id: ToHe
doi: 10.1145/2037509.2037510
file:
- access_level: open_access
checksum: 7f5c65509db1a9fb049abedd9663ed06
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:07:50Z
date_updated: 2020-07-14T12:46:06Z
file_id: '4649'
file_name: IST-2012-92-v1+1_Propagation_models_for_computing_biochemical_reaction_networks.pdf
file_size: 255780
relation: main_file
file_date_updated: 2020-07-14T12:46:06Z
has_accepted_license: '1'
language:
- iso: eng
month: '09'
oa: 1
oa_version: Submitted Version
page: 1 - 3
publication_status: published
publisher: Springer
publist_id: '3341'
pubrep_id: '92'
quality_controlled: '1'
scopus_import: 1
status: public
title: Propagation models for computing biochemical reaction networks
type: conference
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
year: '2011'
...
---
_id: '3301'
abstract:
- lang: eng
text: The chemical master equation is a differential equation describing the time
evolution of the probability distribution over the possible “states” of a biochemical
system. The solution of this equation is of interest within the systems biology
field ever since the importance of the molec- ular noise has been acknowledged.
Unfortunately, most of the systems do not have analytical solutions, and numerical
solutions suffer from the course of dimensionality and therefore need to be approximated.
Here, we introduce the concept of tail approximation, which retrieves an approximation
of the probabilities in the tail of a distribution from the total probability
of the tail and its conditional expectation. This approximation method can then
be used to numerically compute the solution of the chemical master equation on
a subset of the state space, thus fighting the explosion of the state space, for
which this problem is renowned.
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
last_name: Mateescu
citation:
ama: 'Henzinger TA, Mateescu M. Tail approximation for the chemical master equation.
In: Tampere International Center for Signal Processing; 2011.'
apa: 'Henzinger, T. A., & Mateescu, M. (2011). Tail approximation for the chemical
master equation. Presented at the WCSB: Workshop on Computational Systems Biology
(TICSP), Tampere International Center for Signal Processing.'
chicago: Henzinger, Thomas A, and Maria Mateescu. “Tail Approximation for the Chemical
Master Equation.” Tampere International Center for Signal Processing, 2011.
ieee: 'T. A. Henzinger and M. Mateescu, “Tail approximation for the chemical master
equation,” presented at the WCSB: Workshop on Computational Systems Biology (TICSP),
2011.'
ista: 'Henzinger TA, Mateescu M. 2011. Tail approximation for the chemical master
equation. WCSB: Workshop on Computational Systems Biology (TICSP).'
mla: Henzinger, Thomas A., and Maria Mateescu. Tail Approximation for the Chemical
Master Equation. Tampere International Center for Signal Processing, 2011.
short: T.A. Henzinger, M. Mateescu, in:, Tampere International Center for Signal
Processing, 2011.
conference:
name: 'WCSB: Workshop on Computational Systems Biology (TICSP)'
date_created: 2018-12-11T12:02:33Z
date_published: 2011-01-01T00:00:00Z
date_updated: 2021-01-12T07:42:30Z
day: '01'
ddc:
- '005'
- '570'
department:
- _id: ToHe
file:
- access_level: open_access
checksum: aa4d7a832a5419e6c0090650ebff2b9a
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:18:12Z
date_updated: 2020-07-14T12:46:06Z
file_id: '5331'
file_name: IST-2012-91-v1+1_Tail_approximation_for_the_chemical_master_equation.pdf
file_size: 240820
relation: main_file
file_date_updated: 2020-07-14T12:46:06Z
has_accepted_license: '1'
language:
- iso: eng
month: '01'
oa: 1
oa_version: Submitted Version
publication_status: published
publisher: Tampere International Center for Signal Processing
publist_id: '3339'
pubrep_id: '91'
quality_controlled: '1'
status: public
title: Tail approximation for the chemical master equation
type: conference
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
year: '2011'
...
---
_id: '3302'
abstract:
- lang: eng
text: Cloud computing aims to give users virtually unlimited pay-per-use computing
resources without the burden of managing the underlying infrastructure. We present
a new job execution environment Flextic that exploits scal- able static scheduling
techniques to provide the user with a flexible pricing model, such as a tradeoff
between dif- ferent degrees of execution speed and execution price, and at the
same time, reduce scheduling overhead for the cloud provider. We have evaluated
a prototype of Flextic on Amazon EC2 and compared it against Hadoop. For various
data parallel jobs from machine learning, im- age processing, and gene sequencing
that we considered, Flextic has low scheduling overhead and reduces job du- ration
by up to 15% compared to Hadoop, a dynamic cloud scheduler.
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: Anmol
full_name: Singh, Anmol
id: 72A86902-E99F-11E9-9F62-915534D1B916
last_name: Singh
- first_name: Vasu
full_name: Singh, Vasu
id: 4DAE2708-F248-11E8-B48F-1D18A9856A87
last_name: Singh
- 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: 'Henzinger TA, Singh A, Singh V, Wies T, Zufferey D. Static scheduling in clouds.
In: USENIX; 2011:1-6.'
apa: 'Henzinger, T. A., Singh, A., Singh, V., Wies, T., & Zufferey, D. (2011).
Static scheduling in clouds (pp. 1–6). Presented at the HotCloud: Workshop on
Hot Topics in Cloud Computing, USENIX.'
chicago: Henzinger, Thomas A, Anmol Singh, Vasu Singh, Thomas Wies, and Damien Zufferey.
“Static Scheduling in Clouds,” 1–6. USENIX, 2011.
ieee: 'T. A. Henzinger, A. Singh, V. Singh, T. Wies, and D. Zufferey, “Static scheduling
in clouds,” presented at the HotCloud: Workshop on Hot Topics in Cloud Computing,
2011, pp. 1–6.'
ista: 'Henzinger TA, Singh A, Singh V, Wies T, Zufferey D. 2011. Static scheduling
in clouds. HotCloud: Workshop on Hot Topics in Cloud Computing, 1–6.'
mla: Henzinger, Thomas A., et al. Static Scheduling in Clouds. USENIX, 2011,
pp. 1–6.
short: T.A. Henzinger, A. Singh, V. Singh, T. Wies, D. Zufferey, in:, USENIX, 2011,
pp. 1–6.
conference:
end_date: 2011-06-15
name: 'HotCloud: Workshop on Hot Topics in Cloud Computing'
start_date: 2011-06-14
date_created: 2018-12-11T12:02:33Z
date_published: 2011-06-14T00:00:00Z
date_updated: 2021-01-12T07:42:31Z
day: '14'
ddc:
- '000'
- '005'
department:
- _id: ToHe
file:
- access_level: open_access
checksum: 21a461ac004bb535c83320fe79b30375
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:18:14Z
date_updated: 2020-07-14T12:46:06Z
file_id: '5333'
file_name: IST-2012-90-v1+1_Static_scheduling_in_clouds.pdf
file_size: 232770
relation: main_file
file_date_updated: 2020-07-14T12:46:06Z
has_accepted_license: '1'
language:
- iso: eng
month: '06'
oa: 1
oa_version: Submitted Version
page: 1 - 6
publication_status: published
publisher: USENIX
publist_id: '3338'
pubrep_id: '90'
quality_controlled: '1'
status: public
title: Static scheduling in clouds
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2011'
...
---
_id: '3315'
abstract:
- lang: eng
text: We consider two-player games played in real time on game structures with clocks
where the objectives of players are described using parity conditions. The games
are concurrent in that at each turn, both players independently propose a time
delay and an action, and the action with the shorter delay is chosen. To prevent
a player from winning by blocking time, we restrict each player to play strategies
that ensure that the player cannot be responsible for causing a zeno run. First,
we present an efficient reduction of these games to turn-based (i.e., not concurrent)
finite-state (i.e., untimed) parity games. Our reduction improves the best known
complexity for solving timed parity games. Moreover, the rich class of algorithms
for classical parity games can now be applied to timed parity games. The states
of the resulting game are based on clock regions of the original game, and the
state space of the finite game is linear in the size of the region graph. Second,
we consider two restricted classes of strategies for the player that represents
the controller in a real-time synthesis problem, namely, limit-robust and bounded-robust
winning strategies. Using a limit-robust winning strategy, the controller cannot
choose an exact real-valued time delay but must allow for some nonzero jitter
in each of its actions. If there is a given lower bound on the jitter, then the
strategy is bounded-robust winning. We show that exact strategies are more powerful
than limit-robust strategies, which are more powerful than bounded-robust winning
strategies for any bound. For both kinds of robust strategies, we present efficient
reductions to standard timed automaton games. These reductions provide algorithms
for the synthesis of robust real-time controllers.
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- 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: Vinayak
full_name: Prabhu, Vinayak
last_name: Prabhu
citation:
ama: 'Chatterjee K, Henzinger TA, Prabhu V. Timed parity games: Complexity and robustness.
Logical Methods in Computer Science. 2011;7(4). doi:10.2168/LMCS-7(4:8)2011'
apa: 'Chatterjee, K., Henzinger, T. A., & Prabhu, V. (2011). Timed parity games:
Complexity and robustness. Logical Methods in Computer Science. International
Federation of Computational Logic. https://doi.org/10.2168/LMCS-7(4:8)2011'
chicago: 'Chatterjee, Krishnendu, Thomas A Henzinger, and Vinayak Prabhu. “Timed
Parity Games: Complexity and Robustness.” Logical Methods in Computer Science.
International Federation of Computational Logic, 2011. https://doi.org/10.2168/LMCS-7(4:8)2011.'
ieee: 'K. Chatterjee, T. A. Henzinger, and V. Prabhu, “Timed parity games: Complexity
and robustness,” Logical Methods in Computer Science, vol. 7, no. 4. International
Federation of Computational Logic, 2011.'
ista: 'Chatterjee K, Henzinger TA, Prabhu V. 2011. Timed parity games: Complexity
and robustness. Logical Methods in Computer Science. 7(4).'
mla: 'Chatterjee, Krishnendu, et al. “Timed Parity Games: Complexity and Robustness.”
Logical Methods in Computer Science, vol. 7, no. 4, International Federation
of Computational Logic, 2011, doi:10.2168/LMCS-7(4:8)2011.'
short: K. Chatterjee, T.A. Henzinger, V. Prabhu, Logical Methods in Computer Science
7 (2011).
date_created: 2018-12-11T12:02:37Z
date_published: 2011-12-14T00:00:00Z
date_updated: 2023-02-23T11:46:35Z
day: '14'
ddc:
- '000'
- '005'
department:
- _id: KrCh
- _id: ToHe
doi: 10.2168/LMCS-7(4:8)2011
ec_funded: 1
file:
- access_level: open_access
checksum: 3480e1594bbef25ff7462fa93a8a814e
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:16:42Z
date_updated: 2020-07-14T12:46:07Z
file_id: '5231'
file_name: IST-2016-86-v2+1_1011.0688_3_.pdf
file_size: 588863
relation: main_file
file_date_updated: 2020-07-14T12:46:07Z
has_accepted_license: '1'
intvolume: ' 7'
issue: '4'
language:
- iso: eng
license: https://creativecommons.org/licenses/by-nd/4.0/
month: '12'
oa: 1
oa_version: Published Version
project:
- _id: 25EFB36C-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '215543'
name: COMponent-Based Embedded Systems design Techniques
publication: Logical Methods in Computer Science
publication_status: published
publisher: International Federation of Computational Logic
publist_id: '3324'
pubrep_id: '506'
quality_controlled: '1'
related_material:
record:
- id: '3876'
relation: earlier_version
status: public
scopus_import: 1
status: public
title: 'Timed parity games: Complexity and robustness'
tmp:
image: /image/cc_by_nd.png
legal_code_url: https://creativecommons.org/licenses/by-nd/4.0/legalcode
name: Creative Commons Attribution-NoDerivatives 4.0 International (CC BY-ND 4.0)
short: CC BY-ND (4.0)
type: journal_article
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 7
year: '2011'
...
---
_id: '3316'
abstract:
- lang: eng
text: In addition to being correct, a system should be robust, that is, it should
behave reasonably even after receiving unexpected inputs. In this paper, we summarize
two formal notions of robustness that we have introduced previously for reactive
systems. One of the notions is based on assigning costs for failures on a user-provided
notion of incorrect transitions in a specification. Here, we define a system to
be robust if a finite number of incorrect inputs does not lead to an infinite
number of incorrect outputs. We also give a more refined notion of robustness
that aims to minimize the ratio of output failures to input failures. The second
notion is aimed at liveness. In contrast to the previous notion, it has no concept
of recovery from an error. Instead, it compares the ratio of the number of liveness
constraints that the system violates to the number of liveness constraints that
the environment violates.
article_processing_charge: No
author:
- first_name: Roderick
full_name: Bloem, Roderick
last_name: Bloem
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Karin
full_name: Greimel, Karin
last_name: Greimel
- 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: Barbara
full_name: Jobstmann, Barbara
last_name: Jobstmann
citation:
ama: 'Bloem R, Chatterjee K, Greimel K, Henzinger TA, Jobstmann B. Specification-centered
robustness. In: 6th IEEE International Symposium on Industrial and Embedded
Systems. IEEE; 2011:176-185. doi:10.1109/SIES.2011.5953660'
apa: 'Bloem, R., Chatterjee, K., Greimel, K., Henzinger, T. A., & Jobstmann,
B. (2011). Specification-centered robustness. In 6th IEEE International Symposium
on Industrial and Embedded Systems (pp. 176–185). Vasteras, Sweden: IEEE.
https://doi.org/10.1109/SIES.2011.5953660'
chicago: Bloem, Roderick, Krishnendu Chatterjee, Karin Greimel, Thomas A Henzinger,
and Barbara Jobstmann. “Specification-Centered Robustness.” In 6th IEEE International
Symposium on Industrial and Embedded Systems, 176–85. IEEE, 2011. https://doi.org/10.1109/SIES.2011.5953660.
ieee: R. Bloem, K. Chatterjee, K. Greimel, T. A. Henzinger, and B. Jobstmann, “Specification-centered
robustness,” in 6th IEEE International Symposium on Industrial and Embedded
Systems, Vasteras, Sweden, 2011, pp. 176–185.
ista: 'Bloem R, Chatterjee K, Greimel K, Henzinger TA, Jobstmann B. 2011. Specification-centered
robustness. 6th IEEE International Symposium on Industrial and Embedded Systems. SIES:
International Symposium on Industrial Embedded Systems, 176–185.'
mla: Bloem, Roderick, et al. “Specification-Centered Robustness.” 6th IEEE International
Symposium on Industrial and Embedded Systems, IEEE, 2011, pp. 176–85, doi:10.1109/SIES.2011.5953660.
short: R. Bloem, K. Chatterjee, K. Greimel, T.A. Henzinger, B. Jobstmann, in:, 6th
IEEE International Symposium on Industrial and Embedded Systems, IEEE, 2011, pp.
176–185.
conference:
end_date: 2011-06-17
location: Vasteras, Sweden
name: ' SIES: International Symposium on Industrial Embedded Systems'
start_date: 2011-06-15
date_created: 2018-12-11T12:02:38Z
date_published: 2011-07-14T00:00:00Z
date_updated: 2021-01-12T07:42:36Z
day: '14'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1109/SIES.2011.5953660
ec_funded: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://openlib.tugraz.at/download.php?id=5cb57c8a49344&location=browse
month: '07'
oa: 1
oa_version: Published Version
page: 176 - 185
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _id: 25F2ACDE-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11402-N23
name: Rigorous Systems Engineering
- _id: 25F1337C-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '214373'
name: Design for Embedded Systems
- _id: 2587B514-B435-11E9-9278-68D0E5697425
name: Microsoft Research Faculty Fellowship
publication: 6th IEEE International Symposium on Industrial and Embedded Systems
publication_status: published
publisher: IEEE
publist_id: '3323'
quality_controlled: '1'
scopus_import: 1
status: public
title: Specification-centered robustness
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2011'
...
---
_id: '3323'
abstract:
- lang: eng
text: We present a new decidable logic called TREX for expressing constraints about
imperative tree data structures. In particular, TREX supports a transitive closure
operator that can express reachability constraints, which often appear in data
structure invariants. We show that our logic is closed under weakest precondition
computation, which enables its use for automated software verification. We further
show that satisfiability of formulas in TREX is decidable in NP. The low complexity
makes it an attractive alternative to more expensive logics such as monadic second-order
logic (MSOL) over trees, which have been traditionally used for reasoning about
tree data structures.
alternative_title:
- 'LNAI '
author:
- first_name: Thomas
full_name: Wies, Thomas
id: 447BFB88-F248-11E8-B48F-1D18A9856A87
last_name: Wies
- first_name: Marco
full_name: Muñiz, Marco
last_name: Muñiz
- first_name: Viktor
full_name: Kuncak, Viktor
last_name: Kuncak
citation:
ama: 'Wies T, Muñiz M, Kuncak V. An efficient decision procedure for imperative
tree data structures. In: Vol 6803. Springer; 2011:476-491. doi:10.1007/978-3-642-22438-6_36'
apa: 'Wies, T., Muñiz, M., & Kuncak, V. (2011). An efficient decision procedure
for imperative tree data structures (Vol. 6803, pp. 476–491). Presented at the
CADE 23: Automated Deduction , Wrocław, Poland: Springer. https://doi.org/10.1007/978-3-642-22438-6_36'
chicago: Wies, Thomas, Marco Muñiz, and Viktor Kuncak. “An Efficient Decision Procedure
for Imperative Tree Data Structures,” 6803:476–91. Springer, 2011. https://doi.org/10.1007/978-3-642-22438-6_36.
ieee: 'T. Wies, M. Muñiz, and V. Kuncak, “An efficient decision procedure for imperative
tree data structures,” presented at the CADE 23: Automated Deduction , Wrocław,
Poland, 2011, vol. 6803, pp. 476–491.'
ista: 'Wies T, Muñiz M, Kuncak V. 2011. An efficient decision procedure for imperative
tree data structures. CADE 23: Automated Deduction , LNAI , vol. 6803, 476–491.'
mla: Wies, Thomas, et al. An Efficient Decision Procedure for Imperative Tree
Data Structures. Vol. 6803, Springer, 2011, pp. 476–91, doi:10.1007/978-3-642-22438-6_36.
short: T. Wies, M. Muñiz, V. Kuncak, in:, Springer, 2011, pp. 476–491.
conference:
end_date: 2011-08-05
location: Wrocław, Poland
name: 'CADE 23: Automated Deduction '
start_date: 2011-07-31
date_created: 2018-12-11T12:02:40Z
date_published: 2011-07-19T00:00:00Z
date_updated: 2023-02-23T12:23:48Z
day: '19'
department:
- _id: ToHe
doi: 10.1007/978-3-642-22438-6_36
intvolume: ' 6803'
language:
- iso: eng
month: '07'
oa_version: None
page: 476 - 491
publication_status: published
publisher: Springer
publist_id: '3312'
quality_controlled: '1'
related_material:
record:
- id: '5383'
relation: earlier_version
status: public
scopus_import: 1
status: public
title: An efficient decision procedure for imperative tree data structures
type: conference
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
volume: 6803
year: '2011'
...
---
_id: '3324'
abstract:
- lang: eng
text: 'Automated termination provers often use the following schema to prove that
a program terminates: construct a relational abstraction of the program''s transition
relation and then show that the relational abstraction is well-founded. The focus
of current tools has been on developing sophisticated techniques for constructing
the abstractions while relying on known decidable logics (such as linear arithmetic)
to express them. We believe we can significantly increase the class of programs
that are amenable to automated termination proofs by identifying more expressive
decidable logics for reasoning about well-founded relations. We therefore present
a new decision procedure for reasoning about multiset orderings, which are among
the most powerful orderings used to prove termination. We show that, using our
decision procedure, one can automatically prove termination of natural abstractions
of programs.'
alternative_title:
- LNCS
author:
- first_name: Ruzica
full_name: Piskac, Ruzica
last_name: Piskac
- first_name: Thomas
full_name: Wies, Thomas
id: 447BFB88-F248-11E8-B48F-1D18A9856A87
last_name: Wies
citation:
ama: 'Piskac R, Wies T. Decision procedures for automating termination proofs. In:
Jhala R, Schmidt D, eds. Vol 6538. Springer; 2011:371-386. doi:10.1007/978-3-642-18275-4_26'
apa: 'Piskac, R., & Wies, T. (2011). Decision procedures for automating termination
proofs. In R. Jhala & D. Schmidt (Eds.) (Vol. 6538, pp. 371–386). Presented
at the VMCAI: Verification Model Checking and Abstract Interpretation, Texas,
USA: Springer. https://doi.org/10.1007/978-3-642-18275-4_26'
chicago: Piskac, Ruzica, and Thomas Wies. “Decision Procedures for Automating Termination
Proofs.” edited by Ranjit Jhala and David Schmidt, 6538:371–86. Springer, 2011.
https://doi.org/10.1007/978-3-642-18275-4_26.
ieee: 'R. Piskac and T. Wies, “Decision procedures for automating termination proofs,”
presented at the VMCAI: Verification Model Checking and Abstract Interpretation,
Texas, USA, 2011, vol. 6538, pp. 371–386.'
ista: 'Piskac R, Wies T. 2011. Decision procedures for automating termination proofs.
VMCAI: Verification Model Checking and Abstract Interpretation, LNCS, vol. 6538,
371–386.'
mla: Piskac, Ruzica, and Thomas Wies. Decision Procedures for Automating Termination
Proofs. Edited by Ranjit Jhala and David Schmidt, vol. 6538, Springer, 2011,
pp. 371–86, doi:10.1007/978-3-642-18275-4_26.
short: R. Piskac, T. Wies, in:, R. Jhala, D. Schmidt (Eds.), Springer, 2011, pp.
371–386.
conference:
end_date: 2011-01-25
location: Texas, USA
name: 'VMCAI: Verification Model Checking and Abstract Interpretation'
start_date: 2011-01-23
date_created: 2018-12-11T12:02:40Z
date_published: 2011-01-01T00:00:00Z
date_updated: 2021-01-12T07:42:39Z
day: '01'
department:
- _id: ToHe
doi: 10.1007/978-3-642-18275-4_26
editor:
- first_name: Ranjit
full_name: Jhala, Ranjit
last_name: Jhala
- first_name: David
full_name: Schmidt, David
last_name: Schmidt
intvolume: ' 6538'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://infoscience.epfl.ch/record/170697/
month: '01'
oa: 1
oa_version: Submitted Version
page: 371 - 386
publication_status: published
publisher: Springer
publist_id: '3311'
quality_controlled: '1'
scopus_import: 1
status: public
title: Decision procedures for automating termination proofs
type: conference
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
volume: 6538
year: '2011'
...
---
_id: '3325'
abstract:
- lang: eng
text: We introduce streaming data string transducers that map input data strings
to output data strings in a single left-to-right pass in linear time. Data strings
are (unbounded) sequences of data values, tagged with symbols from a finite set,
over a potentially infinite data do- main that supports only the operations of
equality and ordering. The transducer uses a finite set of states, a finite set
of variables ranging over the data domain, and a finite set of variables ranging
over data strings. At every step, it can make decisions based on the next in-
put symbol, updating its state, remembering the input data value in its data variables,
and updating data-string variables by concatenat- ing data-string variables and
new symbols formed from data vari- ables, while avoiding duplication. We establish
that the problems of checking functional equivalence of two streaming transducers,
and of checking whether a streaming transducer satisfies pre/post verification
conditions specified by streaming acceptors over in- put/output data-strings,
are in PSPACE. We identify a class of imperative and a class of functional pro-
grams, manipulating lists of data items, which can be effectively translated to
streaming data-string transducers. The imperative pro- grams dynamically modify
a singly-linked heap by changing next- pointers of heap-nodes and by adding new
nodes. The main re- striction specifies how the next-pointers can be used for
traversal. We also identify an expressively equivalent fragment of functional
programs that traverse a list using syntactically restricted recursive calls.
Our results lead to algorithms for assertion checking and for checking functional
equivalence of two programs, written possibly in different programming styles,
for commonly used routines such as insert, delete, and reverse.
article_processing_charge: No
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. Streaming transducers for algorithmic verification of single
pass list processing programs. In: Vol 46. ACM; 2011:599-610. doi:10.1145/1926385.1926454'
apa: 'Alur, R., & Cerny, P. (2011). Streaming transducers for algorithmic verification
of single pass list processing programs (Vol. 46, pp. 599–610). Presented at the
POPL: Principles of Programming Languages, Texas, USA: ACM. https://doi.org/10.1145/1926385.1926454'
chicago: Alur, Rajeev, and Pavol Cerny. “Streaming Transducers for Algorithmic Verification
of Single Pass List Processing Programs,” 46:599–610. ACM, 2011. https://doi.org/10.1145/1926385.1926454.
ieee: 'R. Alur and P. Cerny, “Streaming transducers for algorithmic verification
of single pass list processing programs,” presented at the POPL: Principles of
Programming Languages, Texas, USA, 2011, vol. 46, no. 1, pp. 599–610.'
ista: 'Alur R, Cerny P. 2011. Streaming transducers for algorithmic verification
of single pass list processing programs. POPL: Principles of Programming Languages
vol. 46, 599–610.'
mla: Alur, Rajeev, and Pavol Cerny. Streaming Transducers for Algorithmic Verification
of Single Pass List Processing Programs. Vol. 46, no. 1, ACM, 2011, pp. 599–610,
doi:10.1145/1926385.1926454.
short: R. Alur, P. Cerny, in:, ACM, 2011, pp. 599–610.
conference:
end_date: 2011-01-28
location: Texas, USA
name: 'POPL: Principles of Programming Languages'
start_date: 2011-01-26
date_created: 2018-12-11T12:02:41Z
date_published: 2011-01-26T00:00:00Z
date_updated: 2022-03-21T08:12:51Z
day: '26'
department:
- _id: ToHe
doi: 10.1145/1926385.1926454
intvolume: ' 46'
issue: '1'
language:
- iso: eng
month: '01'
oa_version: None
page: 599 - 610
publication_status: published
publisher: ACM
publist_id: '3310'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Streaming transducers for algorithmic verification of single pass list processing
programs
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 46
year: '2011'
...