---
_id: '942'
abstract:
- lang: eng
text: 'A notable class of techniques for automatic program repair is known as semantics-based.
Such techniques, e.g., Angelix, infer semantic specifications via symbolic execution,
and then use program synthesis to construct new code that satisfies those inferred
specifications. However, the obtained specifications are naturally incomplete,
leaving the synthesis engine with a difficult task of synthesizing a general solution
from a sparse space of many possible solutions that are consistent with the provided
specifications but that do not necessarily generalize. We present S3, a new repair
synthesis engine that leverages programming-by-examples methodology to synthesize
high-quality bug repairs. The novelty in S3 that allows it to tackle the sparse
search space to create more general repairs is three-fold: (1) A systematic way
to customize and constrain the syntactic search space via a domain-specific language,
(2) An efficient enumeration-based search strategy over the constrained search
space, and (3) A number of ranking features based on measures of the syntactic
and semantic distances between candidate solutions and the original buggy program.
We compare S3’s repair effectiveness with state-of-the-art synthesis engines Angelix,
Enumerative, and CVC4. S3 can successfully and correctly fix at least three times
more bugs than the best baseline on datasets of 52 bugs in small programs, and
100 bugs in real-world large programs. '
article_processing_charge: No
author:
- first_name: Xuan
full_name: Le, Xuan
last_name: Le
- first_name: Duc Hiep
full_name: Chu, Duc Hiep
id: 3598E630-F248-11E8-B48F-1D18A9856A87
last_name: Chu
- first_name: David
full_name: Lo, David
last_name: Lo
- first_name: Claire
full_name: Le Goues, Claire
last_name: Le Goues
- first_name: Willem
full_name: Visser, Willem
last_name: Visser
citation:
ama: 'Le X, Chu DH, Lo D, Le Goues C, Visser W. S3: Syntax- and semantic-guided
repair synthesis via programming by examples. In: Vol F130154. ACM; 2017:593-604.
doi:10.1145/3106237.3106309'
apa: 'Le, X., Chu, D. H., Lo, D., Le Goues, C., & Visser, W. (2017). S3: Syntax-
and semantic-guided repair synthesis via programming by examples (Vol. F130154,
pp. 593–604). Presented at the FSE: Foundations of Software Engineering, Paderborn,
Germany: ACM. https://doi.org/10.1145/3106237.3106309'
chicago: 'Le, Xuan, Duc Hiep Chu, David Lo, Claire Le Goues, and Willem Visser.
“S3: Syntax- and Semantic-Guided Repair Synthesis via Programming by Examples,”
F130154:593–604. ACM, 2017. https://doi.org/10.1145/3106237.3106309.'
ieee: 'X. Le, D. H. Chu, D. Lo, C. Le Goues, and W. Visser, “S3: Syntax- and semantic-guided
repair synthesis via programming by examples,” presented at the FSE: Foundations
of Software Engineering, Paderborn, Germany, 2017, vol. F130154, pp. 593–604.'
ista: 'Le X, Chu DH, Lo D, Le Goues C, Visser W. 2017. S3: Syntax- and semantic-guided
repair synthesis via programming by examples. FSE: Foundations of Software Engineering
vol. F130154, 593–604.'
mla: 'Le, Xuan, et al. S3: Syntax- and Semantic-Guided Repair Synthesis via Programming
by Examples. Vol. F130154, ACM, 2017, pp. 593–604, doi:10.1145/3106237.3106309.'
short: X. Le, D.H. Chu, D. Lo, C. Le Goues, W. Visser, in:, ACM, 2017, pp. 593–604.
conference:
end_date: 2017-09-08
location: Paderborn, Germany
name: 'FSE: Foundations of Software Engineering'
start_date: 2017-09-04
date_created: 2018-12-11T11:49:19Z
date_published: 2017-09-01T00:00:00Z
date_updated: 2023-09-26T15:38:36Z
day: '01'
department:
- _id: ToHe
doi: 10.1145/3106237.3106309
external_id:
isi:
- '000414279300055'
isi: 1
language:
- iso: eng
month: '09'
oa_version: None
page: 593 - 604
project:
- _id: 25F5A88A-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11402-N23
name: Moderne Concurrency Paradigms
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
publication_identifier:
isbn:
- 978-145035105-8
publication_status: published
publisher: ACM
publist_id: '6477'
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'S3: Syntax- and semantic-guided repair synthesis via programming by examples'
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: F130154
year: '2017'
...
---
_id: '950'
abstract:
- lang: eng
text: "Two-player games on graphs are widely studied in formal methods as they model
the interaction between a system and its environment. The game is played by moving
a token throughout a graph to produce an infinite path. There are several common
modes to determine how the players move the token through the graph; e.g., in
turn-based games the players alternate turns in moving the token. We study the
bidding mode of moving the token, which, to the best of our knowledge, has never
been studied in infinite-duration games. Both players have separate budgets, which
sum up to $1$. In each turn, a bidding takes place. Both players submit bids simultaneously,
and a bid is legal if it does not exceed the available budget. The winner of the
bidding pays his bid to the other player and moves the token. For reachability
objectives, repeated bidding games have been studied and are called Richman games.
There, a central question is the existence and computation of threshold budgets;
namely, a value t\\in [0,1] such that if\\PO's budget exceeds $t$, he can win
the game, and if\\PT's budget exceeds 1-t, he can win the game. We focus on parity
games and mean-payoff games. We show the existence of threshold budgets in these
games, and reduce the problem of finding them to Richman games. We also determine
the strategy-complexity of an optimal strategy. Our most interesting result shows
that memoryless strategies suffice for mean-payoff bidding games. \r\n"
alternative_title:
- LIPIcs
article_number: '17'
arxiv: 1
author:
- first_name: Guy
full_name: Avni, Guy
id: 463C8BC2-F248-11E8-B48F-1D18A9856A87
last_name: Avni
orcid: 0000-0001-5588-8287
- 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: Ventsislav K
full_name: Chonev, Ventsislav K
id: 36CBE2E6-F248-11E8-B48F-1D18A9856A87
last_name: Chonev
citation:
ama: 'Avni G, Henzinger TA, Chonev VK. Infinite-duration bidding games. In: Vol
85. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2017. doi:10.4230/LIPIcs.CONCUR.2017.21'
apa: 'Avni, G., Henzinger, T. A., & Chonev, V. K. (2017). Infinite-duration
bidding games (Vol. 85). Presented at the CONCUR: Concurrency Theory, Berlin,
Germany: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2017.21'
chicago: Avni, Guy, Thomas A Henzinger, and Ventsislav K Chonev. “Infinite-Duration
Bidding Games,” Vol. 85. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017.
https://doi.org/10.4230/LIPIcs.CONCUR.2017.21.
ieee: 'G. Avni, T. A. Henzinger, and V. K. Chonev, “Infinite-duration bidding games,”
presented at the CONCUR: Concurrency Theory, Berlin, Germany, 2017, vol. 85.'
ista: 'Avni G, Henzinger TA, Chonev VK. 2017. Infinite-duration bidding games. CONCUR:
Concurrency Theory, LIPIcs, vol. 85, 17.'
mla: Avni, Guy, et al. Infinite-Duration Bidding Games. Vol. 85, 17, Schloss
Dagstuhl - Leibniz-Zentrum für Informatik, 2017, doi:10.4230/LIPIcs.CONCUR.2017.21.
short: G. Avni, T.A. Henzinger, V.K. Chonev, in:, Schloss Dagstuhl - Leibniz-Zentrum
für Informatik, 2017.
conference:
end_date: 2017-09-07
location: Berlin, Germany
name: 'CONCUR: Concurrency Theory'
start_date: 2017-09-05
date_created: 2018-12-11T11:49:22Z
date_published: 2017-09-01T00:00:00Z
date_updated: 2023-08-29T07:02:13Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
- _id: KrCh
doi: 10.4230/LIPIcs.CONCUR.2017.21
external_id:
arxiv:
- '1705.01433'
file:
- access_level: open_access
checksum: 6d5cccf755207b91ccbef95d8275b013
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:18:00Z
date_updated: 2020-07-14T12:48:16Z
file_id: '5318'
file_name: IST-2017-844-v1+1_concur-cr.pdf
file_size: 335170
relation: main_file
file_date_updated: 2020-07-14T12:48:16Z
has_accepted_license: '1'
intvolume: ' 85'
language:
- iso: eng
month: '09'
oa: 1
oa_version: Published Version
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
publication_identifier:
issn:
- 1868-8969
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '6466'
pubrep_id: '844'
quality_controlled: '1'
related_material:
record:
- id: '6752'
relation: later_version
status: public
scopus_import: 1
status: public
title: Infinite-duration bidding games
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 85
year: '2017'
...
---
_id: '962'
abstract:
- lang: eng
text: 'We present a new algorithm for model counting of a class of string constraints.
In addition to the classic operation of concatenation, our class includes some
recursively defined operations such as Kleene closure, and replacement of substrings.
Additionally, our class also includes length constraints on the string expressions,
which means, by requiring reasoning about numbers, that we face a multi-sorted
logic. In the end, our string constraints are motivated by their use in programming
for web applications. Our algorithm comprises two novel features: the ability
to use a technique of (1) partial derivatives for constraints that are already
in a solved form, i.e. a form where its (string) satisfiability is clearly displayed,
and (2) non-progression, where cyclic reasoning in the reduction process may be
terminated (thus allowing for the algorithm to look elsewhere). Finally, we experimentally
compare our model counter with two recent works on model counting of similar constraints,
SMC [18] and ABC [5], to demonstrate its superior performance.'
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Minh
full_name: Trinh, Minh
last_name: Trinh
- first_name: Duc Hiep
full_name: Chu, Duc Hiep
id: 3598E630-F248-11E8-B48F-1D18A9856A87
last_name: Chu
- first_name: Joxan
full_name: Jaffar, Joxan
last_name: Jaffar
citation:
ama: 'Trinh M, Chu DH, Jaffar J. Model counting for recursively-defined strings.
In: Majumdar R, Kunčak V, eds. Vol 10427. Springer; 2017:399-418. doi:10.1007/978-3-319-63390-9_21'
apa: 'Trinh, M., Chu, D. H., & Jaffar, J. (2017). Model counting for recursively-defined
strings. In R. Majumdar & V. Kunčak (Eds.) (Vol. 10427, pp. 399–418). Presented
at the CAV: Computer Aided Verification, Heidelberg, Germany: Springer. https://doi.org/10.1007/978-3-319-63390-9_21'
chicago: Trinh, Minh, Duc Hiep Chu, and Joxan Jaffar. “Model Counting for Recursively-Defined
Strings.” edited by Rupak Majumdar and Viktor Kunčak, 10427:399–418. Springer,
2017. https://doi.org/10.1007/978-3-319-63390-9_21.
ieee: 'M. Trinh, D. H. Chu, and J. Jaffar, “Model counting for recursively-defined
strings,” presented at the CAV: Computer Aided Verification, Heidelberg, Germany,
2017, vol. 10427, pp. 399–418.'
ista: 'Trinh M, Chu DH, Jaffar J. 2017. Model counting for recursively-defined strings.
CAV: Computer Aided Verification, LNCS, vol. 10427, 399–418.'
mla: Trinh, Minh, et al. Model Counting for Recursively-Defined Strings.
Edited by Rupak Majumdar and Viktor Kunčak, vol. 10427, Springer, 2017, pp. 399–418,
doi:10.1007/978-3-319-63390-9_21.
short: M. Trinh, D.H. Chu, J. Jaffar, in:, R. Majumdar, V. Kunčak (Eds.), Springer,
2017, pp. 399–418.
conference:
end_date: 2017-07-28
location: Heidelberg, Germany
name: 'CAV: Computer Aided Verification'
start_date: 2017-07-24
date_created: 2018-12-11T11:49:26Z
date_published: 2017-01-01T00:00:00Z
date_updated: 2023-09-22T09:58:02Z
day: '01'
department:
- _id: ToHe
doi: 10.1007/978-3-319-63390-9_21
editor:
- first_name: Rupak
full_name: Majumdar, Rupak
last_name: Majumdar
- first_name: Viktor
full_name: Kunčak, Viktor
last_name: Kunčak
external_id:
isi:
- '000431900900021'
intvolume: ' 10427'
isi: 1
language:
- iso: eng
month: '01'
oa_version: None
page: 399 - 418
project:
- _id: 25F5A88A-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11402-N23
name: Moderne Concurrency Paradigms
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
publication_identifier:
issn:
- '03029743'
publication_status: published
publisher: Springer
publist_id: '6443'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Model counting for recursively-defined strings
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 10427
year: '2017'
...
---
_id: '963'
abstract:
- lang: eng
text: 'Network games are widely used as a model for selfish resource-allocation
problems. In the classical model, each player selects a path connecting her source
and target vertex. The cost of traversing an edge depends on the number of players
that traverse it. Thus, it abstracts the fact that different users may use a resource
at different times and for different durations, which plays an important role
in defining the costs of the users in reality. For example, when transmitting
packets in a communication network, routing traffic in a road network, or processing
a task in a production system, the traversal of the network involves an inherent
delay, and so sharing and congestion of resources crucially depends on time. We
study timed network games , which add a time component to network games. Each
vertex v in the network is associated with a cost function, mapping the load on
v to the price that a player pays for staying in v for one time unit with this
load. In addition, each edge has a guard, describing time intervals in which the
edge can be traversed, forcing the players to spend time on vertices. Unlike earlier
work that add a time component to network games, the time in our model is continuous
and cannot be discretized. In particular, players have uncountably many strategies,
and a game may have uncountably many pure Nash equilibria. We study properties
of timed network games with cost-sharing or congestion cost functions: their stability,
equilibrium inefficiency, and complexity. In particular, we show that the answer
to the question whether we can restrict attention to boundary strategies, namely
ones in which edges are traversed only at the boundaries of guards, is mixed. '
alternative_title:
- LIPIcs
article_number: '37'
author:
- first_name: Guy
full_name: Avni, Guy
id: 463C8BC2-F248-11E8-B48F-1D18A9856A87
last_name: Avni
orcid: 0000-0001-5588-8287
- first_name: Shibashis
full_name: Guha, Shibashis
last_name: Guha
- first_name: Orna
full_name: Kupferman, Orna
last_name: Kupferman
citation:
ama: 'Avni G, Guha S, Kupferman O. Timed network games with clocks. In: Vol 83.
Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2017. doi:10.4230/LIPIcs.MFCS.2017.37'
apa: 'Avni, G., Guha, S., & Kupferman, O. (2017). Timed network games with clocks
(Vol. 83). Presented at the MFCS: Mathematical Foundations of Computer Science
(SG), Aalborg, Denmark: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.MFCS.2017.37'
chicago: Avni, Guy, Shibashis Guha, and Orna Kupferman. “Timed Network Games with
Clocks,” Vol. 83. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. https://doi.org/10.4230/LIPIcs.MFCS.2017.37.
ieee: 'G. Avni, S. Guha, and O. Kupferman, “Timed network games with clocks,” presented
at the MFCS: Mathematical Foundations of Computer Science (SG), Aalborg, Denmark,
2017, vol. 83.'
ista: 'Avni G, Guha S, Kupferman O. 2017. Timed network games with clocks. MFCS:
Mathematical Foundations of Computer Science (SG), LIPIcs, vol. 83, 37.'
mla: Avni, Guy, et al. Timed Network Games with Clocks. Vol. 83, 37, Schloss
Dagstuhl - Leibniz-Zentrum für Informatik, 2017, doi:10.4230/LIPIcs.MFCS.2017.37.
short: G. Avni, S. Guha, O. Kupferman, in:, Schloss Dagstuhl - Leibniz-Zentrum für
Informatik, 2017.
conference:
end_date: 2017-08-25
location: Aalborg, Denmark
name: 'MFCS: Mathematical Foundations of Computer Science (SG)'
start_date: 2017-08-21
date_created: 2018-12-11T11:49:26Z
date_published: 2017-06-01T00:00:00Z
date_updated: 2023-02-23T12:35:50Z
day: '01'
ddc:
- '004'
department:
- _id: ToHe
doi: 10.4230/LIPIcs.MFCS.2017.37
file:
- access_level: open_access
checksum: f55eaf7f3c36ea07801112acfedd17d5
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:14:10Z
date_updated: 2020-07-14T12:48:18Z
file_id: '5059'
file_name: IST-2017-829-v1+1_mfcs-cr.pdf
file_size: 369730
relation: main_file
file_date_updated: 2020-07-14T12:48:18Z
has_accepted_license: '1'
intvolume: ' 83'
language:
- iso: eng
month: '06'
oa: 1
oa_version: Published Version
project:
- _id: 25F5A88A-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11402-N23
name: Moderne Concurrency Paradigms
publication_identifier:
issn:
- '18688969'
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '6438'
pubrep_id: '829'
quality_controlled: '1'
related_material:
record:
- id: '6005'
relation: later_version
status: public
scopus_import: 1
status: public
title: Timed network games with clocks
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 83
year: '2017'
...
---
_id: '1116'
abstract:
- lang: eng
text: "Time-triggered switched networks are a deterministic communication infrastructure
used by real-time distributed embedded systems. Due to the criticality of the
applications running over them, developers need to ensure that end-to-end communication
is dependable and predictable. Traditional approaches assume static networks that
are not flexible to changes caused by reconfigurations or, more importantly, faults,
which are dealt with in the application using redundancy. We adopt the concept
of handling faults in the switches from non-real-time networks while maintaining
the required predictability. \r\n\r\nWe study a class of forwarding schemes that
can handle various types of failures. We consider probabilistic failures. We study
a class of forwarding schemes that can handle various types of failures. We consider
probabilistic failures. For a given network with a forwarding scheme and a constant
ℓ, we compute the {\\em score} of the scheme, namely the probability (induced
by faults) that at least ℓ messages arrive on time. We reduce the scoring problem
to a reachability problem on a Markov chain with a "product-like" structure.
Its special structure allows us to reason about it symbolically, and reduce the
scoring problem to #SAT. Our solution is generic and can be adapted to different
networks and other contexts. Also, we show the computational complexity of the
scoring problem is #P-complete, and we study methods to estimate the score. We
evaluate the effectiveness of our techniques with an implementation. "
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Guy
full_name: Avni, Guy
id: 463C8BC2-F248-11E8-B48F-1D18A9856A87
last_name: Avni
orcid: 0000-0001-5588-8287
- first_name: Shubham
full_name: Goel, Shubham
last_name: Goel
- 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: Guillermo
full_name: Rodríguez Navas, Guillermo
last_name: Rodríguez Navas
citation:
ama: 'Avni G, Goel S, Henzinger TA, Rodríguez Navas G. Computing scores of forwarding
schemes in switched networks with probabilistic faults. In: Vol 10206. Springer;
2017:169-187. doi:10.1007/978-3-662-54580-5_10'
apa: 'Avni, G., Goel, S., Henzinger, T. A., & Rodríguez Navas, G. (2017). Computing
scores of forwarding schemes in switched networks with probabilistic faults (Vol.
10206, pp. 169–187). Presented at the TACAS: Tools and Algorithms for the Construction
and Analysis of Systems, Uppsala, Sweden: Springer. https://doi.org/10.1007/978-3-662-54580-5_10'
chicago: Avni, Guy, Shubham Goel, Thomas A Henzinger, and Guillermo Rodríguez Navas.
“Computing Scores of Forwarding Schemes in Switched Networks with Probabilistic
Faults,” 10206:169–87. Springer, 2017. https://doi.org/10.1007/978-3-662-54580-5_10.
ieee: 'G. Avni, S. Goel, T. A. Henzinger, and G. Rodríguez Navas, “Computing scores
of forwarding schemes in switched networks with probabilistic faults,” presented
at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems,
Uppsala, Sweden, 2017, vol. 10206, pp. 169–187.'
ista: 'Avni G, Goel S, Henzinger TA, Rodríguez Navas G. 2017. Computing scores of
forwarding schemes in switched networks with probabilistic faults. TACAS: Tools
and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 10206,
169–187.'
mla: Avni, Guy, et al. Computing Scores of Forwarding Schemes in Switched Networks
with Probabilistic Faults. Vol. 10206, Springer, 2017, pp. 169–87, doi:10.1007/978-3-662-54580-5_10.
short: G. Avni, S. Goel, T.A. Henzinger, G. Rodríguez Navas, in:, Springer, 2017,
pp. 169–187.
conference:
end_date: 2017-04-29
location: Uppsala, Sweden
name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
start_date: 2017-04-22
date_created: 2018-12-11T11:50:14Z
date_published: 2017-03-31T00:00:00Z
date_updated: 2023-09-20T11:32:43Z
day: '31'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-662-54580-5_10
external_id:
isi:
- '000440733400010'
file:
- access_level: open_access
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:08:37Z
date_updated: 2018-12-12T10:08:37Z
file_id: '4698'
file_name: IST-2017-758-v1+1_tacas-cr.pdf
file_size: 321800
relation: main_file
file_date_updated: 2018-12-12T10:08:37Z
has_accepted_license: '1'
intvolume: ' 10206'
isi: 1
language:
- iso: eng
month: '03'
oa: 1
oa_version: Submitted Version
page: 169 - 187
project:
- _id: 25F5A88A-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11402-N23
name: Moderne Concurrency Paradigms
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
publication_identifier:
issn:
- '03029743'
publication_status: published
publisher: Springer
publist_id: '6246'
pubrep_id: '758'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Computing scores of forwarding schemes in switched networks with probabilistic
faults
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 10206
year: '2017'
...
---
_id: '1155'
abstract:
- lang: eng
text: This dissertation concerns the automatic verification of probabilistic systems
and programs with arrays by statistical and logical methods. Although statistical
and logical methods are different in nature, we show that they can be successfully
combined for system analysis. In the first part of the dissertation we present
a new statistical algorithm for the verification of probabilistic systems with
respect to unbounded properties, including linear temporal logic. Our algorithm
often performs faster than the previous approaches, and at the same time requires
less information about the system. In addition, our method can be generalized
to unbounded quantitative properties such as mean-payoff bounds. In the second
part, we introduce two techniques for comparing probabilistic systems. Probabilistic
systems are typically compared using the notion of equivalence, which requires
the systems to have the equal probability of all behaviors. However, this notion
is often too strict, since probabilities are typically only empirically estimated,
and any imprecision may break the relation between processes. On the one hand,
we propose to replace the Boolean notion of equivalence by a quantitative distance
of similarity. For this purpose, we introduce a statistical framework for estimating
distances between Markov chains based on their simulation runs, and we investigate
which distances can be approximated in our framework. On the other hand, we propose
to compare systems with respect to a new qualitative logic, which expresses that
behaviors occur with probability one or a positive probability. This qualitative
analysis is robust with respect to modeling errors and applicable to many domains.
In the last part, we present a new quantifier-free logic for integer arrays, which
allows us to express counting. Counting properties are prevalent in array-manipulating
programs, however they cannot be expressed in the quantified fragments of the
theory of arrays. We present a decision procedure for our logic, and provide several
complexity results.
acknowledgement: ' First of all, I want to thank my advisor, prof. Thomas A. Henzinger,
for his guidance during my PhD program. I am grateful for the freedom I was given
to pursue my research interests, and his continuous support. Working with prof.
Henzinger was a truly inspiring experience and taught me what it means to be a scientist.
I want to express my gratitude to my collaborators: Nikola Beneš, Krishnendu Chatterjee,
Martin Chmelík, Ashutosh Gupta, Willibald Krenn, Jan Kˇretínský, Dejan Nickovic,
Andrey Kupriyanov, and Tatjana Petrov. I have learned a great deal from my collaborators,
and without their help this thesis would not be possible. In addition, I want to
thank the members of my thesis committee: Dirk Beyer, Dejan Nickovic, and Georg
Weissenbacher for their advice and reviewing this dissertation. I would especially
like to acknowledge the late Helmut Veith, who was a member of my committee. I will
remember Helmut for his kindness, enthusiasm, and wit, as well as for being an inspiring
scientist. Finally, I would like to thank my colleagues for making my stay at IST
such a pleasant experience: Guy Avni, Sergiy Bogomolov, Ventsislav Chonev, Rasmus
Ibsen-Jensen, Mirco Giacobbe, Bernhard Kragl, Hui Kong, Petr Novotný, Jan Otop,
Andreas Pavlogiannis, Tantjana Petrov, Arjun Radhakrishna, Jakob Ruess, Thorsten
Tarrach, as well as other members of groups Henzinger and Chatterjee. '
alternative_title:
- ISTA Thesis
article_processing_charge: No
author:
- first_name: Przemyslaw
full_name: Daca, Przemyslaw
id: 49351290-F248-11E8-B48F-1D18A9856A87
last_name: Daca
citation:
ama: Daca P. Statistical and logical methods for property checking. 2017. doi:10.15479/AT:ISTA:TH_730
apa: Daca, P. (2017). Statistical and logical methods for property checking.
Institute of Science and Technology Austria. https://doi.org/10.15479/AT:ISTA:TH_730
chicago: Daca, Przemyslaw. “Statistical and Logical Methods for Property Checking.”
Institute of Science and Technology Austria, 2017. https://doi.org/10.15479/AT:ISTA:TH_730.
ieee: P. Daca, “Statistical and logical methods for property checking,” Institute
of Science and Technology Austria, 2017.
ista: Daca P. 2017. Statistical and logical methods for property checking. Institute
of Science and Technology Austria.
mla: Daca, Przemyslaw. Statistical and Logical Methods for Property Checking.
Institute of Science and Technology Austria, 2017, doi:10.15479/AT:ISTA:TH_730.
short: P. Daca, Statistical and Logical Methods for Property Checking, Institute
of Science and Technology Austria, 2017.
date_created: 2018-12-11T11:50:27Z
date_published: 2017-01-02T00:00:00Z
date_updated: 2023-09-07T11:58:34Z
day: '02'
ddc:
- '004'
- '005'
degree_awarded: PhD
department:
- _id: ToHe
doi: 10.15479/AT:ISTA:TH_730
ec_funded: 1
file:
- access_level: open_access
checksum: 1406a681cb737508234fde34766be2c2
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:11:26Z
date_updated: 2020-07-14T12:44:34Z
file_id: '4880'
file_name: IST-2017-730-v1+1_Statistical_and_Logical_Methods_for_Property_Checking.pdf
file_size: 1028586
relation: main_file
file_date_updated: 2020-07-14T12:44:34Z
has_accepted_license: '1'
language:
- iso: eng
month: '01'
oa: 1
oa_version: Published Version
page: '163'
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
publication_identifier:
issn:
- 2663-337X
publication_status: published
publisher: Institute of Science and Technology Austria
publist_id: '6203'
pubrep_id: '730'
related_material:
record:
- id: '1093'
relation: part_of_dissertation
status: public
- id: '1230'
relation: part_of_dissertation
status: public
- id: '1234'
relation: part_of_dissertation
status: public
- id: '1391'
relation: part_of_dissertation
status: public
- id: '1501'
relation: part_of_dissertation
status: public
- id: '1502'
relation: part_of_dissertation
status: public
- id: '2063'
relation: part_of_dissertation
status: public
- id: '2167'
relation: part_of_dissertation
status: public
status: public
supervisor:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
title: Statistical and logical methods for property checking
type: dissertation
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
year: '2017'
...
---
_id: '1196'
abstract:
- lang: eng
text: 'We define the . model-measuring problem: given a model . M and specification
. ϕ, what is the maximal distance . ρ such that all models . M'' within distance
. ρ from . M satisfy (or violate) . ϕ. The model-measuring problem presupposes
a distance function on models. We concentrate on . automatic distance functions,
which are defined by weighted automata. The model-measuring problem subsumes several
generalizations of the classical model-checking problem, in particular, quantitative
model-checking problems that measure the degree of satisfaction of a specification;
robustness problems that measure how much a model can be perturbed without violating
the specification; and parameter synthesis for hybrid systems. We show that for
automatic distance functions, and (a) . ω-regular linear-time, (b) . ω-regular
branching-time, and (c) hybrid specifications, the model-measuring problem can
be solved.We use automata-theoretic model-checking methods for model measuring,
replacing the emptiness question for word, tree, and hybrid automata by the .
optimal-value question for the weighted versions of these automata. For automata
over words and trees, we consider weighted automata that accumulate weights by
maximizing, summing, discounting, and limit averaging. For hybrid automata, we
consider monotonic (parametric) hybrid automata, a hybrid counterpart of (discrete)
weighted automata.We give several examples of using the model-measuring problem
to compute various notions of robustness and quantitative satisfaction for temporal
specifications. Further, we propose the modeling framework for model measuring
to ease the specification and reduce the likelihood of errors in modeling.Finally,
we present a variant of the model-measuring problem, called the . model-repair
problem. The model-repair problem applies to models that do not satisfy the specification;
it can be used to derive restrictions, under which the model satisfies the specification,
i.e., to repair the model.'
acknowledgement: "This research was supported in part by the European Research Council
(ERC) under grant 267989 (QUAREM), by the Austrian Science Fund1 (FWF) under grants
S11402-N23 (RiSE) and Z211-N23 (Wittgenstein Award), and by the National Science
Centre (NCN), Poland under grant 2014/15/D/ST6/04543.\r\nA Technical Report of this
article is available via: https://repository.ist.ac.at/171/"
article_processing_charge: No
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: Jan
full_name: Otop, Jan
id: 2FC5DA74-F248-11E8-B48F-1D18A9856A87
last_name: Otop
citation:
ama: 'Henzinger TA, Otop J. Model measuring for discrete and hybrid systems. Nonlinear
Analysis: Hybrid Systems. 2017;23:166-190. doi:10.1016/j.nahs.2016.09.001'
apa: 'Henzinger, T. A., & Otop, J. (2017). Model measuring for discrete and
hybrid systems. Nonlinear Analysis: Hybrid Systems. Elsevier. https://doi.org/10.1016/j.nahs.2016.09.001'
chicago: 'Henzinger, Thomas A, and Jan Otop. “Model Measuring for Discrete and Hybrid
Systems.” Nonlinear Analysis: Hybrid Systems. Elsevier, 2017. https://doi.org/10.1016/j.nahs.2016.09.001.'
ieee: 'T. A. Henzinger and J. Otop, “Model measuring for discrete and hybrid systems,”
Nonlinear Analysis: Hybrid Systems, vol. 23. Elsevier, pp. 166–190, 2017.'
ista: 'Henzinger TA, Otop J. 2017. Model measuring for discrete and hybrid systems.
Nonlinear Analysis: Hybrid Systems. 23, 166–190.'
mla: 'Henzinger, Thomas A., and Jan Otop. “Model Measuring for Discrete and Hybrid
Systems.” Nonlinear Analysis: Hybrid Systems, vol. 23, Elsevier, 2017,
pp. 166–90, doi:10.1016/j.nahs.2016.09.001.'
short: 'T.A. Henzinger, J. Otop, Nonlinear Analysis: Hybrid Systems 23 (2017) 166–190.'
date_created: 2018-12-11T11:50:39Z
date_published: 2017-02-01T00:00:00Z
date_updated: 2023-09-20T11:18:50Z
day: '01'
department:
- _id: ToHe
doi: 10.1016/j.nahs.2016.09.001
ec_funded: 1
external_id:
isi:
- '000390637000011'
intvolume: ' 23'
isi: 1
language:
- iso: eng
month: '02'
oa_version: None
page: 166 - 190
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: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
publication: 'Nonlinear Analysis: Hybrid Systems'
publication_status: published
publisher: Elsevier
publist_id: '6154'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Model measuring for discrete and hybrid systems
type: journal_article
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 23
year: '2017'
...
---
_id: '465'
abstract:
- lang: eng
text: 'The edit distance between two words w 1 , w 2 is the minimal number of word
operations (letter insertions, deletions, and substitutions) necessary to transform
w 1 to w 2 . The edit distance generalizes to languages L 1 , L 2 , where the
edit distance from L 1 to L 2 is the minimal number k such that for every word
from L 1 there exists a word in L 2 with edit distance at most k . We study the
edit distance computation problem between pushdown automata and their subclasses.
The problem of computing edit distance to a pushdown automaton is undecidable,
and in practice, the interesting question is to compute the edit distance from
a pushdown automaton (the implementation, a standard model for programs with recursion)
to a regular language (the specification). In this work, we present a complete
picture of decidability and complexity for the following problems: (1) deciding
whether, for a given threshold k , the edit distance from a pushdown automaton
to a finite automaton is at most k , and (2) deciding whether the edit distance
from a pushdown automaton to a finite automaton is finite. '
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: Rasmus
full_name: Ibsen-Jensen, Rasmus
id: 3B699956-F248-11E8-B48F-1D18A9856A87
last_name: Ibsen-Jensen
orcid: 0000-0003-4783-0389
- first_name: Jan
full_name: Otop, Jan
last_name: Otop
citation:
ama: Chatterjee K, Henzinger TA, Ibsen-Jensen R, Otop J. Edit distance for pushdown
automata. Logical Methods in Computer Science. 2017;13(3). doi:10.23638/LMCS-13(3:23)2017
apa: Chatterjee, K., Henzinger, T. A., Ibsen-Jensen, R., & Otop, J. (2017).
Edit distance for pushdown automata. Logical Methods in Computer Science.
International Federation of Computational Logic. https://doi.org/10.23638/LMCS-13(3:23)2017
chicago: Chatterjee, Krishnendu, Thomas A Henzinger, Rasmus Ibsen-Jensen, and Jan
Otop. “Edit Distance for Pushdown Automata.” Logical Methods in Computer Science.
International Federation of Computational Logic, 2017. https://doi.org/10.23638/LMCS-13(3:23)2017.
ieee: K. Chatterjee, T. A. Henzinger, R. Ibsen-Jensen, and J. Otop, “Edit distance
for pushdown automata,” Logical Methods in Computer Science, vol. 13, no.
3. International Federation of Computational Logic, 2017.
ista: Chatterjee K, Henzinger TA, Ibsen-Jensen R, Otop J. 2017. Edit distance for
pushdown automata. Logical Methods in Computer Science. 13(3).
mla: Chatterjee, Krishnendu, et al. “Edit Distance for Pushdown Automata.” Logical
Methods in Computer Science, vol. 13, no. 3, International Federation of Computational
Logic, 2017, doi:10.23638/LMCS-13(3:23)2017.
short: K. Chatterjee, T.A. Henzinger, R. Ibsen-Jensen, J. Otop, Logical Methods
in Computer Science 13 (2017).
date_created: 2018-12-11T11:46:37Z
date_published: 2017-09-13T00:00:00Z
date_updated: 2023-02-23T12:26:25Z
day: '13'
ddc:
- '004'
department:
- _id: KrCh
- _id: ToHe
doi: 10.23638/LMCS-13(3:23)2017
ec_funded: 1
file:
- access_level: open_access
checksum: 08041379ba408d40664f449eb5907a8f
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:14:37Z
date_updated: 2020-07-14T12:46:33Z
file_id: '5090'
file_name: IST-2015-321-v1+1_main.pdf
file_size: 279071
relation: main_file
- access_level: open_access
checksum: 08041379ba408d40664f449eb5907a8f
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:14:38Z
date_updated: 2020-07-14T12:46:33Z
file_id: '5091'
file_name: IST-2018-955-v1+1_2017_Chatterjee_Edit_distance.pdf
file_size: 279071
relation: main_file
file_date_updated: 2020-07-14T12:46:33Z
has_accepted_license: '1'
intvolume: ' 13'
issue: '3'
language:
- iso: eng
license: https://creativecommons.org/licenses/by-nd/4.0/
month: '09'
oa: 1
oa_version: Published Version
project:
- _id: 25F5A88A-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11402-N23
name: Moderne Concurrency Paradigms
- _id: 2584A770-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: P 23499-N23
name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11407
name: Game Theory
publication: Logical Methods in Computer Science
publication_identifier:
issn:
- '18605974'
publication_status: published
publisher: International Federation of Computational Logic
publist_id: '7356'
pubrep_id: '955'
quality_controlled: '1'
related_material:
record:
- id: '1610'
relation: earlier_version
status: public
- id: '5438'
relation: earlier_version
status: public
scopus_import: 1
status: public
title: Edit distance for pushdown automata
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: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 13
year: '2017'
...
---
_id: '467'
abstract:
- lang: eng
text: Recently there has been a significant effort to handle quantitative properties
in formal verification and synthesis. While weighted automata over finite and
infinite words provide a natural and flexible framework to express quantitative
properties, perhaps surprisingly, some basic system properties such as average
response time cannot be expressed using weighted automata or in any other known
decidable formalism. In this work, we introduce nested weighted automata as a
natural extension of weighted automata, which makes it possible to express important
quantitative properties such as average response time. In nested weighted automata,
a master automaton spins off and collects results from weighted slave automata,
each of which computes a quantity along a finite portion of an infinite word.
Nested weighted automata can be viewed as the quantitative analogue of monitor
automata, which are used in runtime verification. We establish an almost-complete
decidability picture for the basic decision problems about nested weighted automata
and illustrate their applicability in several domains. In particular, nested weighted
automata can be used to decide average response time properties.
article_number: '31'
arxiv: 1
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: Jan
full_name: Otop, Jan
id: 2FC5DA74-F248-11E8-B48F-1D18A9856A87
last_name: Otop
citation:
ama: Chatterjee K, Henzinger TA, Otop J. Nested weighted automata. ACM Transactions
on Computational Logic (TOCL). 2017;18(4). doi:10.1145/3152769
apa: Chatterjee, K., Henzinger, T. A., & Otop, J. (2017). Nested weighted automata.
ACM Transactions on Computational Logic (TOCL). ACM. https://doi.org/10.1145/3152769
chicago: Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. “Nested Weighted
Automata.” ACM Transactions on Computational Logic (TOCL). ACM, 2017. https://doi.org/10.1145/3152769.
ieee: K. Chatterjee, T. A. Henzinger, and J. Otop, “Nested weighted automata,” ACM
Transactions on Computational Logic (TOCL), vol. 18, no. 4. ACM, 2017.
ista: Chatterjee K, Henzinger TA, Otop J. 2017. Nested weighted automata. ACM Transactions
on Computational Logic (TOCL). 18(4), 31.
mla: Chatterjee, Krishnendu, et al. “Nested Weighted Automata.” ACM Transactions
on Computational Logic (TOCL), vol. 18, no. 4, 31, ACM, 2017, doi:10.1145/3152769.
short: K. Chatterjee, T.A. Henzinger, J. Otop, ACM Transactions on Computational
Logic (TOCL) 18 (2017).
date_created: 2018-12-11T11:46:38Z
date_published: 2017-12-01T00:00:00Z
date_updated: 2023-02-23T12:26:19Z
day: '01'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1145/3152769
ec_funded: 1
external_id:
arxiv:
- '1606.03598'
intvolume: ' 18'
issue: '4'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1606.03598
month: '12'
oa: 1
oa_version: Preprint
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
- _id: 2584A770-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: P 23499-N23
name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 2587B514-B435-11E9-9278-68D0E5697425
name: Microsoft Research Faculty Fellowship
publication: ACM Transactions on Computational Logic (TOCL)
publication_identifier:
issn:
- '15293785'
publication_status: published
publisher: ACM
publist_id: '7354'
quality_controlled: '1'
related_material:
record:
- id: '1656'
relation: earlier_version
status: public
- id: '5415'
relation: earlier_version
status: public
- id: '5436'
relation: earlier_version
status: public
scopus_import: 1
status: public
title: Nested weighted automata
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 18
year: '2017'
...
---
_id: '471'
abstract:
- lang: eng
text: 'We present a new algorithm for the statistical model checking of Markov chains
with respect to unbounded temporal properties, including full linear temporal
logic. The main idea is that we monitor each simulation run on the fly, in order
to detect quickly if a bottom strongly connected component is entered with high
probability, in which case the simulation run can be terminated early. As a result,
our simulation runs are often much shorter than required by termination bounds
that are computed a priori for a desired level of confidence on a large state
space. In comparison to previous algorithms for statistical model checking our
method is not only faster in many cases but also requires less information about
the system, namely, only the minimum transition probability that occurs in the
Markov chain. In addition, our method can be generalised to unbounded quantitative
properties such as mean-payoff bounds. '
article_number: '12'
author:
- first_name: Przemyslaw
full_name: Daca, Przemyslaw
id: 49351290-F248-11E8-B48F-1D18A9856A87
last_name: Daca
- 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: Jan
full_name: Kretinsky, Jan
id: 44CEF464-F248-11E8-B48F-1D18A9856A87
last_name: Kretinsky
orcid: 0000-0002-8122-2881
- first_name: Tatjana
full_name: Petrov, Tatjana
id: 3D5811FC-F248-11E8-B48F-1D18A9856A87
last_name: Petrov
orcid: 0000-0002-9041-0905
citation:
ama: Daca P, Henzinger TA, Kretinsky J, Petrov T. Faster statistical model checking
for unbounded temporal properties. ACM Transactions on Computational Logic
(TOCL). 2017;18(2). doi:10.1145/3060139
apa: Daca, P., Henzinger, T. A., Kretinsky, J., & Petrov, T. (2017). Faster
statistical model checking for unbounded temporal properties. ACM Transactions
on Computational Logic (TOCL). ACM. https://doi.org/10.1145/3060139
chicago: Daca, Przemyslaw, Thomas A Henzinger, Jan Kretinsky, and Tatjana Petrov.
“Faster Statistical Model Checking for Unbounded Temporal Properties.” ACM
Transactions on Computational Logic (TOCL). ACM, 2017. https://doi.org/10.1145/3060139.
ieee: P. Daca, T. A. Henzinger, J. Kretinsky, and T. Petrov, “Faster statistical
model checking for unbounded temporal properties,” ACM Transactions on Computational
Logic (TOCL), vol. 18, no. 2. ACM, 2017.
ista: Daca P, Henzinger TA, Kretinsky J, Petrov T. 2017. Faster statistical model
checking for unbounded temporal properties. ACM Transactions on Computational
Logic (TOCL). 18(2), 12.
mla: Daca, Przemyslaw, et al. “Faster Statistical Model Checking for Unbounded Temporal
Properties.” ACM Transactions on Computational Logic (TOCL), vol. 18, no.
2, 12, ACM, 2017, doi:10.1145/3060139.
short: P. Daca, T.A. Henzinger, J. Kretinsky, T. Petrov, ACM Transactions on Computational
Logic (TOCL) 18 (2017).
date_created: 2018-12-11T11:46:39Z
date_published: 2017-05-01T00:00:00Z
date_updated: 2023-02-21T16:48:11Z
day: '01'
department:
- _id: ToHe
doi: 10.1145/3060139
ec_funded: 1
intvolume: ' 18'
issue: '2'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1504.05739
month: '05'
oa: 1
oa_version: Submitted Version
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _id: 25F5A88A-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11402-N23
name: Moderne Concurrency Paradigms
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
- _id: 25681D80-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '291734'
name: International IST Postdoc Fellowship Programme
publication: ACM Transactions on Computational Logic (TOCL)
publication_identifier:
issn:
- '15293785'
publication_status: published
publisher: ACM
publist_id: '7349'
quality_controlled: '1'
related_material:
record:
- id: '1234'
relation: earlier_version
status: public
scopus_import: 1
status: public
title: Faster statistical model checking for unbounded temporal properties
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 18
year: '2017'
...
---
_id: '1227'
abstract:
- lang: eng
text: Many biological systems can be modeled as multiaffine hybrid systems. Due
to the nonlinearity of multiaffine systems, it is difficult to verify their properties
of interest directly. A common strategy to tackle this problem is to construct
and analyze a discrete overapproximation of the original system. However, the
conservativeness of a discrete abstraction significantly determines the level
of confidence we can have in the properties of the original system. In this paper,
in order to reduce the conservativeness of a discrete abstraction, we propose
a new method based on a sufficient and necessary decision condition for computing
discrete transitions between states in the abstract system. We assume the state
space partition of a multiaffine system to be based on a set of multivariate polynomials.
Hence, a rectangular partition defined in terms of polynomials of the form (xi
− c) is just a simple case of multivariate polynomial partition, and the new decision
condition applies naturally. We analyze and demonstrate the improvement of our
method over the existing methods using some examples.
acknowledgement: This research was supported in part by the Austrian Science Fund
(FWF) under grants S11402-N23, S11405-N23 and S11412-N23 (RiSE/SHiNE) and Z211-N23
(Wittgenstein Award).
alternative_title:
- LNCS
author:
- first_name: Hui
full_name: Kong, Hui
id: 3BDE25AA-F248-11E8-B48F-1D18A9856A87
last_name: Kong
orcid: 0000-0002-3066-6941
- first_name: Ezio
full_name: Bartocci, Ezio
last_name: Bartocci
- first_name: Sergiy
full_name: Bogomolov, Sergiy
id: 369D9A44-F248-11E8-B48F-1D18A9856A87
last_name: Bogomolov
orcid: 0000-0002-0686-0365
- first_name: Radu
full_name: Grosu, Radu
last_name: Grosu
- 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: Yu
full_name: Jiang, Yu
last_name: Jiang
- first_name: Christian
full_name: Schilling, Christian
id: 3A2F4DCE-F248-11E8-B48F-1D18A9856A87
last_name: Schilling
orcid: 0000-0003-3658-1065
citation:
ama: 'Kong H, Bartocci E, Bogomolov S, et al. Discrete abstraction of multiaffine
systems. In: Vol 9957. Springer; 2016:128-144. doi:10.1007/978-3-319-47151-8_9'
apa: 'Kong, H., Bartocci, E., Bogomolov, S., Grosu, R., Henzinger, T. A., Jiang,
Y., & Schilling, C. (2016). Discrete abstraction of multiaffine systems (Vol.
9957, pp. 128–144). Presented at the HSB: Hybrid Systems Biology, Grenoble, France:
Springer. https://doi.org/10.1007/978-3-319-47151-8_9'
chicago: Kong, Hui, Ezio Bartocci, Sergiy Bogomolov, Radu Grosu, Thomas A Henzinger,
Yu Jiang, and Christian Schilling. “Discrete Abstraction of Multiaffine Systems,”
9957:128–44. Springer, 2016. https://doi.org/10.1007/978-3-319-47151-8_9.
ieee: 'H. Kong et al., “Discrete abstraction of multiaffine systems,” presented
at the HSB: Hybrid Systems Biology, Grenoble, France, 2016, vol. 9957, pp. 128–144.'
ista: 'Kong H, Bartocci E, Bogomolov S, Grosu R, Henzinger TA, Jiang Y, Schilling
C. 2016. Discrete abstraction of multiaffine systems. HSB: Hybrid Systems Biology,
LNCS, vol. 9957, 128–144.'
mla: Kong, Hui, et al. Discrete Abstraction of Multiaffine Systems. Vol.
9957, Springer, 2016, pp. 128–44, doi:10.1007/978-3-319-47151-8_9.
short: H. Kong, E. Bartocci, S. Bogomolov, R. Grosu, T.A. Henzinger, Y. Jiang, C.
Schilling, in:, Springer, 2016, pp. 128–144.
conference:
end_date: 2016-10-21
location: Grenoble, France
name: 'HSB: Hybrid Systems Biology'
start_date: 2016-10-20
date_created: 2018-12-11T11:50:49Z
date_published: 2016-09-25T00:00:00Z
date_updated: 2021-01-12T06:49:13Z
day: '25'
ddc:
- '005'
department:
- _id: ToHe
doi: 10.1007/978-3-319-47151-8_9
file:
- access_level: open_access
checksum: 994e164b558c47bacf8dc066dd27c8fc
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:10:49Z
date_updated: 2020-07-14T12:44:39Z
file_id: '4840'
file_name: IST-2017-781-v1+1_main.pdf
file_size: 683955
relation: main_file
file_date_updated: 2020-07-14T12:44:39Z
has_accepted_license: '1'
intvolume: ' 9957'
language:
- iso: eng
month: '09'
oa: 1
oa_version: Submitted Version
page: 128 - 144
project:
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
- _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: '6107'
pubrep_id: '781'
quality_controlled: '1'
scopus_import: 1
status: public
title: Discrete abstraction of multiaffine systems
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 9957
year: '2016'
...
---
_id: '1230'
abstract:
- lang: eng
text: Concolic testing is a promising method for generating test suites for large
programs. However, it suffers from the path-explosion problem and often fails
to find tests that cover difficult-to-reach parts of programs. In contrast, model
checkers based on counterexample-guided abstraction refinement explore programs
exhaustively, while failing to scale on large programs with precision. In this
paper, we present a novel method that iteratively combines concolic testing and
model checking to find a test suite for a given coverage criterion. If concolic
testing fails to cover some test goals, then the model checker refines its program
abstraction to prove more paths infeasible, which reduces the search space for
concolic testing. We have implemented our method on top of the concolictesting
tool Crest and the model checker CpaChecker. We evaluated our tool on a collection
of programs and a category of SvComp benchmarks. In our experiments, we observed
an improvement in branch coverage compared to Crest from 48% to 63% in the best
case, and from 66% to 71% on average.
acknowledgement: "We thank Andrey Kupriyanov for feedback on the manuscript,\r\nand
Michael Tautschnig for help with preparing the experiments. This research was supported
in part by the European Research Council (ERC) under grant 267989 (QUAREM) and by
the Austrian Science Fund (FWF) under grants S11402-N23 (RiSE) and Z211-N23 (Wittgenstein
Award)."
alternative_title:
- LNCS
author:
- first_name: Przemyslaw
full_name: Daca, Przemyslaw
id: 49351290-F248-11E8-B48F-1D18A9856A87
last_name: Daca
- first_name: Ashutosh
full_name: Gupta, Ashutosh
id: 335E5684-F248-11E8-B48F-1D18A9856A87
last_name: Gupta
- 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: 'Daca P, Gupta A, Henzinger TA. Abstraction-driven concolic testing. In: Vol
9583. Springer; 2016:328-347. doi:10.1007/978-3-662-49122-5_16'
apa: 'Daca, P., Gupta, A., & Henzinger, T. A. (2016). Abstraction-driven concolic
testing (Vol. 9583, pp. 328–347). Presented at the VMCAI: Verification, Model
Checking and Abstract Interpretation, St. Petersburg, FL, USA: Springer. https://doi.org/10.1007/978-3-662-49122-5_16'
chicago: Daca, Przemyslaw, Ashutosh Gupta, and Thomas A Henzinger. “Abstraction-Driven
Concolic Testing,” 9583:328–47. Springer, 2016. https://doi.org/10.1007/978-3-662-49122-5_16.
ieee: 'P. Daca, A. Gupta, and T. A. Henzinger, “Abstraction-driven concolic testing,”
presented at the VMCAI: Verification, Model Checking and Abstract Interpretation,
St. Petersburg, FL, USA, 2016, vol. 9583, pp. 328–347.'
ista: 'Daca P, Gupta A, Henzinger TA. 2016. Abstraction-driven concolic testing.
VMCAI: Verification, Model Checking and Abstract Interpretation, LNCS, vol. 9583,
328–347.'
mla: Daca, Przemyslaw, et al. Abstraction-Driven Concolic Testing. Vol. 9583,
Springer, 2016, pp. 328–47, doi:10.1007/978-3-662-49122-5_16.
short: P. Daca, A. Gupta, T.A. Henzinger, in:, Springer, 2016, pp. 328–347.
conference:
end_date: 2016-01-19
location: St. Petersburg, FL, USA
name: 'VMCAI: Verification, Model Checking and Abstract Interpretation'
start_date: 2016-01-17
date_created: 2018-12-11T11:50:50Z
date_published: 2016-01-01T00:00:00Z
date_updated: 2023-09-07T11:58:33Z
day: '01'
department:
- _id: ToHe
doi: 10.1007/978-3-662-49122-5_16
ec_funded: 1
intvolume: ' 9583'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1511.02615
month: '01'
oa: 1
oa_version: Preprint
page: 328 - 347
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
- _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: '6104'
quality_controlled: '1'
related_material:
record:
- id: '1155'
relation: dissertation_contains
status: public
scopus_import: 1
status: public
title: Abstraction-driven concolic testing
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 9583
year: '2016'
...
---
_id: '1234'
abstract:
- lang: eng
text: We present a new algorithm for the statistical model checking of Markov chains
with respect to unbounded temporal properties, including full linear temporal
logic. The main idea is that we monitor each simulation run on the fly, in order
to detect quickly if a bottom strongly connected component is entered with high
probability, in which case the simulation run can be terminated early. As a result,
our simulation runs are often much shorter than required by termination bounds
that are computed a priori for a desired level of confidence on a large state
space. In comparison to previous algorithms for statistical model checking our
method is not only faster in many cases but also requires less information about
the system, namely, only the minimum transition probability that occurs in the
Markov chain. In addition, our method can be generalised to unbounded quantitative
properties such as mean-payoff bounds.
acknowledgement: "This research was funded in part by the European Research Council
(ERC) under\r\ngrant agreement 267989 (QUAREM), the Austrian Science Fund
\ (FWF) under\r\ngrants project S11402-N23 (RiSE) and Z211-N23 (Wittgenstein Award),
the Peo-\r\nple Programme (Marie Curie Actions) of the European Union’s Seventh
Framework\r\nProgramme (FP7/2007-2013) REA Grant No 291734, the SNSF Advanced Postdoc.\r\nMobility
Fellowship – grant number P300P2\r\n161067, and the Czech Science Foun-\r\ndation
under grant agreement P202/12/G061."
alternative_title:
- LNCS
author:
- first_name: Przemyslaw
full_name: Daca, Przemyslaw
id: 49351290-F248-11E8-B48F-1D18A9856A87
last_name: Daca
- 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: Jan
full_name: Kretinsky, Jan
id: 44CEF464-F248-11E8-B48F-1D18A9856A87
last_name: Kretinsky
orcid: 0000-0002-8122-2881
- first_name: Tatjana
full_name: Petrov, Tatjana
id: 3D5811FC-F248-11E8-B48F-1D18A9856A87
last_name: Petrov
orcid: 0000-0002-9041-0905
citation:
ama: 'Daca P, Henzinger TA, Kretinsky J, Petrov T. Faster statistical model checking
for unbounded temporal properties. In: Vol 9636. Springer; 2016:112-129. doi:10.1007/978-3-662-49674-9_7'
apa: 'Daca, P., Henzinger, T. A., Kretinsky, J., & Petrov, T. (2016). Faster
statistical model checking for unbounded temporal properties (Vol. 9636, pp. 112–129).
Presented at the TACAS: Tools and Algorithms for the Construction and Analysis
of Systems, Eindhoven, The Netherlands: Springer. https://doi.org/10.1007/978-3-662-49674-9_7'
chicago: Daca, Przemyslaw, Thomas A Henzinger, Jan Kretinsky, and Tatjana Petrov.
“Faster Statistical Model Checking for Unbounded Temporal Properties,” 9636:112–29.
Springer, 2016. https://doi.org/10.1007/978-3-662-49674-9_7.
ieee: 'P. Daca, T. A. Henzinger, J. Kretinsky, and T. Petrov, “Faster statistical
model checking for unbounded temporal properties,” presented at the TACAS: Tools
and Algorithms for the Construction and Analysis of Systems, Eindhoven, The Netherlands,
2016, vol. 9636, pp. 112–129.'
ista: 'Daca P, Henzinger TA, Kretinsky J, Petrov T. 2016. Faster statistical model
checking for unbounded temporal properties. TACAS: Tools and Algorithms for the
Construction and Analysis of Systems, LNCS, vol. 9636, 112–129.'
mla: Daca, Przemyslaw, et al. Faster Statistical Model Checking for Unbounded
Temporal Properties. Vol. 9636, Springer, 2016, pp. 112–29, doi:10.1007/978-3-662-49674-9_7.
short: P. Daca, T.A. Henzinger, J. Kretinsky, T. Petrov, in:, Springer, 2016, pp.
112–129.
conference:
end_date: 2016-04-08
location: Eindhoven, The Netherlands
name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
start_date: 2016-04-02
date_created: 2018-12-11T11:50:51Z
date_published: 2016-01-01T00:00:00Z
date_updated: 2023-09-07T11:58:33Z
day: '01'
department:
- _id: ToHe
- _id: CaGu
doi: 10.1007/978-3-662-49674-9_7
ec_funded: 1
intvolume: ' 9636'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1504.05739
month: '01'
oa: 1
oa_version: Preprint
page: 112 - 129
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: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
- _id: 25681D80-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '291734'
name: International IST Postdoc Fellowship Programme
publication_status: published
publisher: Springer
publist_id: '6099'
quality_controlled: '1'
related_material:
record:
- id: '471'
relation: later_version
status: public
- id: '1155'
relation: dissertation_contains
status: public
scopus_import: 1
status: public
title: Faster statistical model checking for unbounded temporal properties
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 9636
year: '2016'
...
---
_id: '1256'
abstract:
- lang: eng
text: Simulink is widely used for model driven development (MDD) of industrial software
systems. Typically, the Simulink based development is initiated from Stateflow
modeling, followed by simulation, validation and code generation mapped to physical
execution platforms. However, recent industrial trends have raised the demands
of rigorous verification on safety-critical applications, which is unfortunately
challenging for Simulink. In this paper, we present an approach to bridge the
Stateflow based model driven development and a well- defined rigorous verification.
First, we develop a self- contained toolkit to translate Stateflow model into
timed automata, where major advanced modeling features in Stateflow are supported.
Taking advantage of the strong verification capability of Uppaal, we can not only
find bugs in Stateflow models which are missed by Simulink Design Verifier, but
also check more important temporal properties. Next, we customize a runtime verifier
for the generated nonintrusive VHDL and C code of Stateflow model for monitoring.
The major strength of the customization is the flexibility to collect and analyze
runtime properties with a pure software monitor, which opens more opportunities
for engineers to achieve high reliability of the target system compared with the
traditional act that only relies on Simulink Polyspace. We incorporate these two
parts into original Stateflow based MDD seamlessly. In this way, safety-critical
properties are both verified at the model level, and at the consistent system
implementation level with physical execution environment in consideration. We
apply our approach on a train controller design, and the verified implementation
is tested and deployed on a real hardware platform.
acknowledgement: This work is supported in part by NSF CNS 13-30077, NSF CNS 13-29886,
NSF CNS 15-45002, NSFC 61303014, NSFC 61202010, and NSFC 91218302.
article_number: '7461337'
author:
- first_name: Yu
full_name: Jiang, Yu
last_name: Jiang
- first_name: Yixiao
full_name: Yang, Yixiao
last_name: Yang
- first_name: Han
full_name: Liu, Han
last_name: Liu
- first_name: Hui
full_name: Kong, Hui
id: 3BDE25AA-F248-11E8-B48F-1D18A9856A87
last_name: Kong
orcid: 0000-0002-3066-6941
- first_name: Ming
full_name: Gu, Ming
last_name: Gu
- first_name: Jiaguang
full_name: Sun, Jiaguang
last_name: Sun
- first_name: Lui
full_name: Sha, Lui
last_name: Sha
citation:
ama: 'Jiang Y, Yang Y, Liu H, et al. From stateflow simulation to verified implementation:
A verification approach and a real-time train controller design. In: IEEE; 2016.
doi:10.1109/RTAS.2016.7461337'
apa: 'Jiang, Y., Yang, Y., Liu, H., Kong, H., Gu, M., Sun, J., & Sha, L. (2016).
From stateflow simulation to verified implementation: A verification approach
and a real-time train controller design. Presented at the RTAS: Real-time and
Embedded Technology and Applications Symposium, Vienna, Austria: IEEE. https://doi.org/10.1109/RTAS.2016.7461337'
chicago: 'Jiang, Yu, Yixiao Yang, Han Liu, Hui Kong, Ming Gu, Jiaguang Sun, and
Lui Sha. “From Stateflow Simulation to Verified Implementation: A Verification
Approach and a Real-Time Train Controller Design.” IEEE, 2016. https://doi.org/10.1109/RTAS.2016.7461337.'
ieee: 'Y. Jiang et al., “From stateflow simulation to verified implementation:
A verification approach and a real-time train controller design,” presented at
the RTAS: Real-time and Embedded Technology and Applications Symposium, Vienna,
Austria, 2016.'
ista: 'Jiang Y, Yang Y, Liu H, Kong H, Gu M, Sun J, Sha L. 2016. From stateflow
simulation to verified implementation: A verification approach and a real-time
train controller design. RTAS: Real-time and Embedded Technology and Applications
Symposium, 7461337.'
mla: 'Jiang, Yu, et al. From Stateflow Simulation to Verified Implementation:
A Verification Approach and a Real-Time Train Controller Design. 7461337,
IEEE, 2016, doi:10.1109/RTAS.2016.7461337.'
short: Y. Jiang, Y. Yang, H. Liu, H. Kong, M. Gu, J. Sun, L. Sha, in:, IEEE, 2016.
conference:
end_date: 2016-04-14
location: Vienna, Austria
name: 'RTAS: Real-time and Embedded Technology and Applications Symposium'
start_date: 2016-04-11
date_created: 2018-12-11T11:50:58Z
date_published: 2016-04-27T00:00:00Z
date_updated: 2021-01-12T06:49:26Z
day: '27'
ddc:
- '005'
department:
- _id: ToHe
doi: 10.1109/RTAS.2016.7461337
file:
- access_level: open_access
checksum: 42f0462911cc9957f2356b12fb33b4b6
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:12:31Z
date_updated: 2020-07-14T12:44:41Z
file_id: '4949'
file_name: IST-2017-780-v1+1_RTAS-42-Camera-Ready.pdf
file_size: 1293599
relation: main_file
file_date_updated: 2020-07-14T12:44:41Z
has_accepted_license: '1'
language:
- iso: eng
month: '04'
oa: 1
oa_version: Submitted Version
publication_status: published
publisher: IEEE
publist_id: '6069'
pubrep_id: '780'
quality_controlled: '1'
scopus_import: 1
status: public
title: 'From stateflow simulation to verified implementation: A verification approach
and a real-time train controller design'
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
year: '2016'
...
---
_id: '1335'
abstract:
- lang: eng
text: In this paper we review various automata-theoretic formalisms for expressing
quantitative properties. We start with finite-state Boolean automata that express
the traditional regular properties. We then consider weighted ω-automata that
can measure the average density of events, which finite-state Boolean automata
cannot. However, even weighted ω-automata cannot express basic performance properties
like average response time. We finally consider two formalisms of weighted ω-automata
with monitors, where the monitors are either (a) counters or (b) weighted automata
themselves. We present a translation result to establish that these two formalisms
are equivalent. Weighted ω-automata with monitors generalize weighted ω-automata,
and can express average response time property. They present a natural, robust,
and expressive framework for quantitative specifications, with important decidable
properties.
alternative_title:
- LNCS
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: Jan
full_name: Otop, Jan
id: 2FC5DA74-F248-11E8-B48F-1D18A9856A87
last_name: Otop
citation:
ama: 'Chatterjee K, Henzinger TA, Otop J. Quantitative monitor automata. In: Vol
9837. Springer; 2016:23-38. doi:10.1007/978-3-662-53413-7_2'
apa: 'Chatterjee, K., Henzinger, T. A., & Otop, J. (2016). Quantitative monitor
automata (Vol. 9837, pp. 23–38). Presented at the SAS: Static Analysis Symposium,
Edinburgh, United Kingdom: Springer. https://doi.org/10.1007/978-3-662-53413-7_2'
chicago: Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. “Quantitative
Monitor Automata,” 9837:23–38. Springer, 2016. https://doi.org/10.1007/978-3-662-53413-7_2.
ieee: 'K. Chatterjee, T. A. Henzinger, and J. Otop, “Quantitative monitor automata,”
presented at the SAS: Static Analysis Symposium, Edinburgh, United Kingdom, 2016,
vol. 9837, pp. 23–38.'
ista: 'Chatterjee K, Henzinger TA, Otop J. 2016. Quantitative monitor automata.
SAS: Static Analysis Symposium, LNCS, vol. 9837, 23–38.'
mla: Chatterjee, Krishnendu, et al. Quantitative Monitor Automata. Vol. 9837,
Springer, 2016, pp. 23–38, doi:10.1007/978-3-662-53413-7_2.
short: K. Chatterjee, T.A. Henzinger, J. Otop, in:, Springer, 2016, pp. 23–38.
conference:
end_date: 2016-09-10
location: Edinburgh, United Kingdom
name: 'SAS: Static Analysis Symposium'
start_date: 2016-09-08
date_created: 2018-12-11T11:51:26Z
date_published: 2016-08-31T00:00:00Z
date_updated: 2021-01-12T06:49:58Z
day: '31'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1007/978-3-662-53413-7_2
ec_funded: 1
intvolume: ' 9837'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1604.06764
month: '08'
oa: 1
oa_version: Preprint
page: 23 - 38
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 25892FC0-B435-11E9-9278-68D0E5697425
grant_number: ICT15-003
name: Efficient Algorithms for Computer Aided Verification
publication_status: published
publisher: Springer
publist_id: '5932'
quality_controlled: '1'
scopus_import: 1
status: public
title: Quantitative monitor automata
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 9837
year: '2016'
...
---
_id: '1524'
abstract:
- lang: eng
text: "When designing genetic circuits, the typical primitives used in major existing
modelling formalisms are gene interaction graphs, where edges between genes denote
either an activation or inhibition relation. However, when designing experiments,
it is important to be precise about the low-level mechanistic details as to how
each such relation is implemented. The rule-based modelling language Kappa allows
to unambiguously specify mechanistic details such as DNA binding sites, dimerisation
of transcription factors, or co-operative interactions. Such a detailed description
comes with complexity and computationally costly executions. We propose a general
method for automatically transforming a rule-based program, by eliminating intermediate
species and adjusting the rate constants accordingly. To the best of our knowledge,
we show the first automated reduction of rule-based models based on equilibrium
approximations.\r\nOur algorithm is an adaptation of an existing algorithm, which
was designed for reducing reaction-based programs; our version of the algorithm
scans the rule-based Kappa model in search for those interaction patterns known
to be amenable to equilibrium approximations (e.g. Michaelis-Menten scheme). Additional
checks are then performed in order to verify if the reduction is meaningful in
the context of the full model. The reduced model is efficiently obtained by static
inspection over the rule-set. The tool is tested on a detailed rule-based model
of a λ-phage switch, which lists 92 rules and 13 agents. The reduced model has
11 rules and 5 agents, and provides a dramatic reduction in simulation time of
several orders of magnitude."
acknowledgement: This research was supported by the People Programme (Marie Curie
Actions) of the European Union’s Seventh Framework Programme (FP7/2007-2013) under
REA grant agreement no. 291734, and the SNSF Early Postdoc.Mobility Fellowship,
the grant number P2EZP2_148797.
alternative_title:
- LNCS
author:
- first_name: Andreea
full_name: Beica, Andreea
last_name: Beica
- first_name: Calin C
full_name: Guet, Calin C
id: 47F8433E-F248-11E8-B48F-1D18A9856A87
last_name: Guet
orcid: 0000-0001-6220-2052
- first_name: Tatjana
full_name: Petrov, Tatjana
id: 3D5811FC-F248-11E8-B48F-1D18A9856A87
last_name: Petrov
orcid: 0000-0002-9041-0905
citation:
ama: 'Beica A, Guet CC, Petrov T. Efficient reduction of kappa models by static
inspection of the rule-set. In: Vol 9271. Springer; 2016:173-191. doi:10.1007/978-3-319-26916-0_10'
apa: 'Beica, A., Guet, C. C., & Petrov, T. (2016). Efficient reduction of kappa
models by static inspection of the rule-set (Vol. 9271, pp. 173–191). Presented
at the HSB: Hybrid Systems Biology, Madrid, Spain: Springer. https://doi.org/10.1007/978-3-319-26916-0_10'
chicago: Beica, Andreea, Calin C Guet, and Tatjana Petrov. “Efficient Reduction
of Kappa Models by Static Inspection of the Rule-Set,” 9271:173–91. Springer,
2016. https://doi.org/10.1007/978-3-319-26916-0_10.
ieee: 'A. Beica, C. C. Guet, and T. Petrov, “Efficient reduction of kappa models
by static inspection of the rule-set,” presented at the HSB: Hybrid Systems Biology,
Madrid, Spain, 2016, vol. 9271, pp. 173–191.'
ista: 'Beica A, Guet CC, Petrov T. 2016. Efficient reduction of kappa models by
static inspection of the rule-set. HSB: Hybrid Systems Biology, LNCS, vol. 9271,
173–191.'
mla: Beica, Andreea, et al. Efficient Reduction of Kappa Models by Static Inspection
of the Rule-Set. Vol. 9271, Springer, 2016, pp. 173–91, doi:10.1007/978-3-319-26916-0_10.
short: A. Beica, C.C. Guet, T. Petrov, in:, Springer, 2016, pp. 173–191.
conference:
end_date: 2015-09-05
location: Madrid, Spain
name: 'HSB: Hybrid Systems Biology'
start_date: 2015-09-04
date_created: 2018-12-11T11:52:31Z
date_published: 2016-01-10T00:00:00Z
date_updated: 2021-01-12T06:51:22Z
day: '10'
department:
- _id: CaGu
- _id: ToHe
doi: 10.1007/978-3-319-26916-0_10
ec_funded: 1
intvolume: ' 9271'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1501.00440
month: '01'
oa: 1
oa_version: Preprint
page: 173 - 191
project:
- _id: 25681D80-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '291734'
name: International IST Postdoc Fellowship Programme
publication_status: published
publisher: Springer
publist_id: '5649'
quality_controlled: '1'
scopus_import: 1
status: public
title: Efficient reduction of kappa models by static inspection of the rule-set
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 9271
year: '2016'
...
---
_id: '1526'
abstract:
- lang: eng
text: 'We present the first study of robustness of systems that are both timed as
well as reactive (I/O). We study the behavior of such timed I/O systems in the
presence of uncertain inputs and formalize their robustness using the analytic
notion of Lipschitz continuity: a timed I/O system is K-(Lipschitz) robust if
the perturbation in its output is at most K times the perturbation in its input.
We quantify input and output perturbation using similarity functions over timed
words such as the timed version of the Manhattan distance and the Skorokhod distance.
We consider two models of timed I/O systems — timed transducers and asynchronous
sequential circuits. We show that K-robustness of timed transducers can be decided
in polynomial space under certain conditions. For asynchronous sequential circuits,
we reduce K-robustness w.r.t. timed Manhattan distances to K-robustness of discrete
letter-to-letter transducers and show PSpace-completeness of the problem.'
acknowledgement: This research was supported in part by the European Research Council
(ERC) under grant 267989 (QUAREM), by the Austrian Science Fund (FWF) under grants
S11402-N23 (RiSE) and Z211-N23 (Wittgenstein Award), and by the National Science
Centre (NCN), Poland under grant 2014/15/D/ST6/04543.
alternative_title:
- LNCS
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: Jan
full_name: Otop, Jan
id: 2FC5DA74-F248-11E8-B48F-1D18A9856A87
last_name: Otop
- first_name: Roopsha
full_name: Samanta, Roopsha
id: 3D2AAC08-F248-11E8-B48F-1D18A9856A87
last_name: Samanta
citation:
ama: 'Henzinger TA, Otop J, Samanta R. Lipschitz robustness of timed I/O systems.
In: Vol 9583. Springer; 2016:250-267. doi:10.1007/978-3-662-49122-5_12'
apa: 'Henzinger, T. A., Otop, J., & Samanta, R. (2016). Lipschitz robustness
of timed I/O systems (Vol. 9583, pp. 250–267). Presented at the VMCAI: Verification,
Model Checking and Abstract Interpretation, St. Petersburg, FL, USA: Springer.
https://doi.org/10.1007/978-3-662-49122-5_12'
chicago: Henzinger, Thomas A, Jan Otop, and Roopsha Samanta. “Lipschitz Robustness
of Timed I/O Systems,” 9583:250–67. Springer, 2016. https://doi.org/10.1007/978-3-662-49122-5_12.
ieee: 'T. A. Henzinger, J. Otop, and R. Samanta, “Lipschitz robustness of timed
I/O systems,” presented at the VMCAI: Verification, Model Checking and Abstract
Interpretation, St. Petersburg, FL, USA, 2016, vol. 9583, pp. 250–267.'
ista: 'Henzinger TA, Otop J, Samanta R. 2016. Lipschitz robustness of timed I/O
systems. VMCAI: Verification, Model Checking and Abstract Interpretation, LNCS,
vol. 9583, 250–267.'
mla: Henzinger, Thomas A., et al. Lipschitz Robustness of Timed I/O Systems.
Vol. 9583, Springer, 2016, pp. 250–67, doi:10.1007/978-3-662-49122-5_12.
short: T.A. Henzinger, J. Otop, R. Samanta, in:, Springer, 2016, pp. 250–267.
conference:
end_date: 2016-01-19
location: St. Petersburg, FL, USA
name: 'VMCAI: Verification, Model Checking and Abstract Interpretation'
start_date: 2016-01-17
date_created: 2018-12-11T11:52:32Z
date_published: 2016-01-01T00:00:00Z
date_updated: 2021-01-12T06:51:23Z
day: '01'
department:
- _id: ToHe
doi: 10.1007/978-3-662-49122-5_12
ec_funded: 1
intvolume: ' 9583'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1506.01233
month: '01'
oa: 1
oa_version: Preprint
page: 250 - 267
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
- _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: '5647'
quality_controlled: '1'
scopus_import: 1
status: public
title: Lipschitz robustness of timed I/O systems
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 9583
year: '2016'
...
---
_id: '1705'
abstract:
- lang: eng
text: Hybrid systems represent an important and powerful formalism for modeling
real-world applications such as embedded systems. A verification tool like SpaceEx
is based on the exploration of a symbolic search space (the region space). As
a verification tool, it is typically optimized towards proving the absence of
errors. In some settings, e.g., when the verification tool is employed in a feedback-directed
design cycle, one would like to have the option to call a version that is optimized
towards finding an error trajectory in the region space. A recent approach in
this direction is based on guided search. Guided search relies on a cost function
that indicates which states are promising to be explored, and preferably explores
more promising states first. In this paper, we propose an abstraction-based cost
function based on coarse-grained space abstractions for guiding the reachability
analysis. For this purpose, a suitable abstraction technique that exploits the
flexible granularity of modern reachability analysis algorithms is introduced.
The new cost function is an effective extension of pattern database approaches
that have been successfully applied in other areas. The approach has been implemented
in the SpaceEx model checker. The evaluation shows its practical potential.
article_processing_charge: Yes (via OA deal)
author:
- first_name: Sergiy
full_name: Bogomolov, Sergiy
id: 369D9A44-F248-11E8-B48F-1D18A9856A87
last_name: Bogomolov
orcid: 0000-0002-0686-0365
- first_name: Alexandre
full_name: Donzé, Alexandre
last_name: Donzé
- first_name: Goran
full_name: Frehse, Goran
last_name: Frehse
- first_name: Radu
full_name: Grosu, Radu
last_name: Grosu
- first_name: Taylor
full_name: Johnson, Taylor
last_name: Johnson
- first_name: Hamed
full_name: Ladan, Hamed
last_name: Ladan
- first_name: Andreas
full_name: Podelski, Andreas
last_name: Podelski
- first_name: Martin
full_name: Wehrle, Martin
last_name: Wehrle
citation:
ama: Bogomolov S, Donzé A, Frehse G, et al. Guided search for hybrid systems based
on coarse-grained space abstractions. International Journal on Software Tools
for Technology Transfer. 2016;18(4):449-467. doi:10.1007/s10009-015-0393-y
apa: Bogomolov, S., Donzé, A., Frehse, G., Grosu, R., Johnson, T., Ladan, H., …
Wehrle, M. (2016). Guided search for hybrid systems based on coarse-grained space
abstractions. International Journal on Software Tools for Technology Transfer.
Springer. https://doi.org/10.1007/s10009-015-0393-y
chicago: Bogomolov, Sergiy, Alexandre Donzé, Goran Frehse, Radu Grosu, Taylor Johnson,
Hamed Ladan, Andreas Podelski, and Martin Wehrle. “Guided Search for Hybrid Systems
Based on Coarse-Grained Space Abstractions.” International Journal on Software
Tools for Technology Transfer. Springer, 2016. https://doi.org/10.1007/s10009-015-0393-y.
ieee: S. Bogomolov et al., “Guided search for hybrid systems based on coarse-grained
space abstractions,” International Journal on Software Tools for Technology
Transfer, vol. 18, no. 4. Springer, pp. 449–467, 2016.
ista: Bogomolov S, Donzé A, Frehse G, Grosu R, Johnson T, Ladan H, Podelski A, Wehrle
M. 2016. Guided search for hybrid systems based on coarse-grained space abstractions.
International Journal on Software Tools for Technology Transfer. 18(4), 449–467.
mla: Bogomolov, Sergiy, et al. “Guided Search for Hybrid Systems Based on Coarse-Grained
Space Abstractions.” International Journal on Software Tools for Technology
Transfer, vol. 18, no. 4, Springer, 2016, pp. 449–67, doi:10.1007/s10009-015-0393-y.
short: S. Bogomolov, A. Donzé, G. Frehse, R. Grosu, T. Johnson, H. Ladan, A. Podelski,
M. Wehrle, International Journal on Software Tools for Technology Transfer 18
(2016) 449–467.
date_created: 2018-12-11T11:53:34Z
date_published: 2016-08-01T00:00:00Z
date_updated: 2021-01-12T06:52:38Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/s10009-015-0393-y
ec_funded: 1
file:
- access_level: open_access
checksum: 31561d7705599a9bd4ea816accc0752e
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:15:26Z
date_updated: 2020-07-14T12:45:13Z
file_id: '5146'
file_name: IST-2016-457-v1+1_s10009-015-0393-y.pdf
file_size: 2296522
relation: main_file
file_date_updated: 2020-07-14T12:45:13Z
has_accepted_license: '1'
intvolume: ' 18'
issue: '4'
language:
- iso: eng
month: '08'
oa: 1
oa_version: Published Version
page: 449 - 467
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
publication: International Journal on Software Tools for Technology Transfer
publication_status: published
publisher: Springer
publist_id: '5431'
pubrep_id: '457'
quality_controlled: '1'
scopus_import: 1
status: public
title: Guided search for hybrid systems based on coarse-grained space abstractions
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: journal_article
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 18
year: '2016'
...
---
_id: '1341'
abstract:
- lang: eng
text: In resource allocation games, selfish players share resources that are needed
in order to fulfill their objectives. The cost of using a resource depends on
the load on it. In the traditional setting, the players make their choices concurrently
and in one-shot. That is, a strategy for a player is a subset of the resources.
We introduce and study dynamic resource allocation games. In this setting, the
game proceeds in phases. In each phase each player chooses one resource. A scheduler
dictates the order in which the players proceed in a phase, possibly scheduling
several players to proceed concurrently. The game ends when each player has collected
a set of resources that fulfills his objective. The cost for each player then
depends on this set as well as on the load on the resources in it – we consider
both congestion and cost-sharing games. We argue that the dynamic setting is the
suitable setting for many applications in practice. We study the stability of
dynamic resource allocation games, where the appropriate notion of stability is
that of subgame perfect equilibrium, study the inefficiency incurred due to selfish
behavior, and also study problems that are particular to the dynamic setting,
like constraints on the order in which resources can be chosen or the problem
of finding a scheduler that achieves stability.
acknowledgement: This research was supported in part by the European Research Council
(ERC) under grants 267989 (QUAREM) and 278410 (QUALITY), and by the Austrian Science
Fund (FWF) under grants S11402-N23 (RiSE) and Z211-N23 (Wittgenstein Award).
alternative_title:
- LNCS
author:
- first_name: Guy
full_name: Avni, Guy
id: 463C8BC2-F248-11E8-B48F-1D18A9856A87
last_name: Avni
orcid: 0000-0001-5588-8287
- 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: Orna
full_name: Kupferman, Orna
last_name: Kupferman
citation:
ama: 'Avni G, Henzinger TA, Kupferman O. Dynamic resource allocation games. In:
Vol 9928. Springer; 2016:153-166. doi:10.1007/978-3-662-53354-3_13'
apa: 'Avni, G., Henzinger, T. A., & Kupferman, O. (2016). Dynamic resource allocation
games (Vol. 9928, pp. 153–166). Presented at the SAGT: Symposium on Algorithmic
Game Theory, Liverpool, United Kingdom: Springer. https://doi.org/10.1007/978-3-662-53354-3_13'
chicago: Avni, Guy, Thomas A Henzinger, and Orna Kupferman. “Dynamic Resource Allocation
Games,” 9928:153–66. Springer, 2016. https://doi.org/10.1007/978-3-662-53354-3_13.
ieee: 'G. Avni, T. A. Henzinger, and O. Kupferman, “Dynamic resource allocation
games,” presented at the SAGT: Symposium on Algorithmic Game Theory, Liverpool,
United Kingdom, 2016, vol. 9928, pp. 153–166.'
ista: 'Avni G, Henzinger TA, Kupferman O. 2016. Dynamic resource allocation games.
SAGT: Symposium on Algorithmic Game Theory, LNCS, vol. 9928, 153–166.'
mla: Avni, Guy, et al. Dynamic Resource Allocation Games. Vol. 9928, Springer,
2016, pp. 153–66, doi:10.1007/978-3-662-53354-3_13.
short: G. Avni, T.A. Henzinger, O. Kupferman, in:, Springer, 2016, pp. 153–166.
conference:
end_date: 2016-09-21
location: Liverpool, United Kingdom
name: 'SAGT: Symposium on Algorithmic Game Theory'
start_date: 2016-09-19
date_created: 2018-12-11T11:51:28Z
date_published: 2016-09-01T00:00:00Z
date_updated: 2023-08-17T13:52:49Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-662-53354-3_13
ec_funded: 1
file:
- access_level: open_access
checksum: 0825eefd4e22774f6f62cb7d7389b05a
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:14:22Z
date_updated: 2020-07-14T12:44:45Z
file_id: '5073'
file_name: IST-2016-645-v1+1_sagt-cr.pdf
file_size: 243458
relation: main_file
file_date_updated: 2020-07-14T12:44:45Z
has_accepted_license: '1'
intvolume: ' 9928'
language:
- iso: eng
month: '09'
oa: 1
oa_version: Preprint
page: 153 - 166
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: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
publication_status: published
publisher: Springer
publist_id: '5926'
pubrep_id: '645'
quality_controlled: '1'
related_material:
record:
- id: '6761'
relation: later_version
status: public
scopus_import: 1
status: public
title: Dynamic resource allocation games
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 9928
year: '2016'
...
---
_id: '1390'
abstract:
- lang: eng
text: "The goal of automatic program repair is to identify a set of syntactic changes
that can turn a program that is incorrect with respect\r\nto a given specification
into a correct one. Existing program repair techniques typically aim to find any
program that meets the given specification. Such “best-effort” strategies can
end up generating a program that is quite different from the original one. Novel
techniques have been proposed to compute syntactically minimal program fixes,
but the smallest syntactic fix to a program can still significantly alter the
original program’s behaviour. We propose a new approach to program repair based
on program distances, which can quantify changes not only to the program syntax
but also to the program semantics. We call this the quantitative program repair
problem where the “optimal” repair is derived using multiple distances. We implement
a solution to the quantitative repair\r\nproblem in a prototype tool called Qlose\r\n(Quantitatively
close), using the program synthesizer Sketch. We evaluate the effectiveness of
different distances in obtaining desirable repairs by evaluating\r\nQlose on programs
taken from educational tools such as CodeHunt and edX."
alternative_title:
- LNCS
author:
- first_name: Loris
full_name: D'Antoni, Loris
last_name: D'Antoni
- first_name: Roopsha
full_name: Samanta, Roopsha
id: 3D2AAC08-F248-11E8-B48F-1D18A9856A87
last_name: Samanta
- first_name: Rishabh
full_name: Singh, Rishabh
last_name: Singh
citation:
ama: 'D’Antoni L, Samanta R, Singh R. QLOSE: Program repair with quantitative objectives.
In: Vol 9780. Springer; 2016:383-401. doi:10.1007/978-3-319-41540-6_21'
apa: 'D’Antoni, L., Samanta, R., & Singh, R. (2016). QLOSE: Program repair with
quantitative objectives (Vol. 9780, pp. 383–401). Presented at the CAV: Computer
Aided Verification, Toronto, Canada: Springer. https://doi.org/10.1007/978-3-319-41540-6_21'
chicago: 'D’Antoni, Loris, Roopsha Samanta, and Rishabh Singh. “QLOSE: Program Repair
with Quantitative Objectives,” 9780:383–401. Springer, 2016. https://doi.org/10.1007/978-3-319-41540-6_21.'
ieee: 'L. D’Antoni, R. Samanta, and R. Singh, “QLOSE: Program repair with quantitative
objectives,” presented at the CAV: Computer Aided Verification, Toronto, Canada,
2016, vol. 9780, pp. 383–401.'
ista: 'D’Antoni L, Samanta R, Singh R. 2016. QLOSE: Program repair with quantitative
objectives. CAV: Computer Aided Verification, LNCS, vol. 9780, 383–401.'
mla: 'D’Antoni, Loris, et al. QLOSE: Program Repair with Quantitative Objectives.
Vol. 9780, Springer, 2016, pp. 383–401, doi:10.1007/978-3-319-41540-6_21.'
short: L. D’Antoni, R. Samanta, R. Singh, in:, Springer, 2016, pp. 383–401.
conference:
end_date: 2016-07-23
location: Toronto, Canada
name: 'CAV: Computer Aided Verification'
start_date: 2016-07-17
date_created: 2018-12-11T11:51:45Z
date_published: 2016-07-13T00:00:00Z
date_updated: 2021-01-12T06:50:21Z
day: '13'
department:
- _id: ToHe
doi: 10.1007/978-3-319-41540-6_21
ec_funded: 1
intvolume: ' 9780'
language:
- iso: eng
month: '07'
oa_version: None
page: 383 - 401
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: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
publication_status: published
publisher: Springer
publist_id: '5819'
quality_controlled: '1'
scopus_import: 1
status: public
title: 'QLOSE: Program repair with quantitative objectives'
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 9780
year: '2016'
...