---
_id: '2167'
abstract:
- lang: eng
text: Model-based testing is a promising technology for black-box software and hardware
testing, in which test cases are generated automatically from high-level specifications.
Nowadays, systems typically consist of multiple interacting components and, due
to their complexity, testing presents a considerable portion of the effort and
cost in the design process. Exploiting the compositional structure of system specifications
can considerably reduce the effort in model-based testing. Moreover, inferring
properties about the system from testing its individual components allows the
designer to reduce the amount of integration testing. In this paper, we study
compositional properties of the ioco-testing theory. We propose a new approach
to composition and hiding operations, inspired by contract-based design and interface
theories. These operations preserve behaviors that are compatible under composition
and hiding, and prune away incompatible ones. The resulting specification characterizes
the input sequences for which the unit testing of components is sufficient to
infer the correctness of component integration without the need for further tests.
We provide a methodology that uses these results to minimize integration testing
effort, but also to detect potential weaknesses in specifications. While we focus
on asynchronous models and the ioco conformance relation, the resulting methodology
can be applied to a broader class of systems.
article_number: '6823899'
article_processing_charge: No
arxiv: 1
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: Willibald
full_name: Krenn, Willibald
last_name: Krenn
- first_name: Dejan
full_name: Nickovic, Dejan
last_name: Nickovic
citation:
ama: 'Daca P, Henzinger TA, Krenn W, Nickovic D. Compositional specifications for
IOCO testing. In: IEEE 7th International Conference on Software Testing, Verification
and Validation. IEEE; 2014. doi:10.1109/ICST.2014.50'
apa: 'Daca, P., Henzinger, T. A., Krenn, W., & Nickovic, D. (2014). Compositional
specifications for IOCO testing. In IEEE 7th International Conference on Software
Testing, Verification and Validation. Cleveland, USA: IEEE. https://doi.org/10.1109/ICST.2014.50'
chicago: Daca, Przemyslaw, Thomas A Henzinger, Willibald Krenn, and Dejan Nickovic.
“Compositional Specifications for IOCO Testing.” In IEEE 7th International
Conference on Software Testing, Verification and Validation. IEEE, 2014. https://doi.org/10.1109/ICST.2014.50.
ieee: P. Daca, T. A. Henzinger, W. Krenn, and D. Nickovic, “Compositional specifications
for IOCO testing,” in IEEE 7th International Conference on Software Testing,
Verification and Validation, Cleveland, USA, 2014.
ista: 'Daca P, Henzinger TA, Krenn W, Nickovic D. 2014. Compositional specifications
for IOCO testing. IEEE 7th International Conference on Software Testing, Verification
and Validation. ICST: International Conference on Software Testing, Verification
and Validation, 6823899.'
mla: Daca, Przemyslaw, et al. “Compositional Specifications for IOCO Testing.” IEEE
7th International Conference on Software Testing, Verification and Validation,
6823899, IEEE, 2014, doi:10.1109/ICST.2014.50.
short: P. Daca, T.A. Henzinger, W. Krenn, D. Nickovic, in:, IEEE 7th International
Conference on Software Testing, Verification and Validation, IEEE, 2014.
conference:
end_date: 2014-04-04
location: Cleveland, USA
name: 'ICST: International Conference on Software Testing, Verification and Validation'
start_date: 2014-03-31
date_created: 2018-12-11T11:56:06Z
date_published: 2014-03-01T00:00:00Z
date_updated: 2026-04-15T10:02:12Z
day: '01'
department:
- _id: ToHe
doi: 10.1109/ICST.2014.50
ec_funded: 1
external_id:
arxiv:
- '1904.07083'
isi:
- '000355985000040'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1904.07083
month: '03'
oa: 1
oa_version: Preprint
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
publication: IEEE 7th International Conference on Software Testing, Verification and
Validation
publication_identifier:
isbn:
- 978-1-4799-2255-0
issn:
- 2159-4848
publication_status: published
publisher: IEEE
publist_id: '4817'
quality_controlled: '1'
related_material:
record:
- id: '5411'
relation: earlier_version
status: public
- id: '1155'
relation: dissertation_contains
status: public
scopus_import: '1'
status: public
title: Compositional specifications for IOCO testing
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
year: '2014'
...
---
_id: '2063'
abstract:
- lang: eng
text: We consider Markov decision processes (MDPs) which are a standard model for
probabilistic systems.We focus on qualitative properties forMDPs that can express
that desired behaviors of the system arise almost-surely (with probability 1)
or with positive probability. We introduce a new simulation relation to capture
the refinement relation ofMDPs with respect to qualitative properties, and present
discrete graph theoretic algorithms with quadratic complexity to compute the simulation
relation.We present an automated technique for assume-guarantee style reasoning
for compositional analysis ofMDPs with qualitative properties by giving a counterexample
guided abstraction-refinement approach to compute our new simulation relation.
We have implemented our algorithms and show that the compositional analysis leads
to significant improvements.
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: Martin
full_name: Chmelik, Martin
id: 3624234E-F248-11E8-B48F-1D18A9856A87
last_name: Chmelik
- first_name: Przemyslaw
full_name: Daca, Przemyslaw
id: 49351290-F248-11E8-B48F-1D18A9856A87
last_name: Daca
citation:
ama: 'Chatterjee K, Chmelik M, Daca P. CEGAR for qualitative analysis of probabilistic
systems. In: Vol 8559. Springer; 2014:473-490. doi:10.1007/978-3-319-08867-9_31'
apa: 'Chatterjee, K., Chmelik, M., & Daca, P. (2014). CEGAR for qualitative
analysis of probabilistic systems (Vol. 8559, pp. 473–490). Presented at the CAV:
Computer Aided Verification, Vienna, Austria: Springer. https://doi.org/10.1007/978-3-319-08867-9_31'
chicago: Chatterjee, Krishnendu, Martin Chmelik, and Przemyslaw Daca. “CEGAR for
Qualitative Analysis of Probabilistic Systems,” 8559:473–90. Springer, 2014. https://doi.org/10.1007/978-3-319-08867-9_31.
ieee: 'K. Chatterjee, M. Chmelik, and P. Daca, “CEGAR for qualitative analysis of
probabilistic systems,” presented at the CAV: Computer Aided Verification, Vienna,
Austria, 2014, vol. 8559, pp. 473–490.'
ista: 'Chatterjee K, Chmelik M, Daca P. 2014. CEGAR for qualitative analysis of
probabilistic systems. CAV: Computer Aided Verification, LNCS, vol. 8559, 473–490.'
mla: Chatterjee, Krishnendu, et al. CEGAR for Qualitative Analysis of Probabilistic
Systems. Vol. 8559, Springer, 2014, pp. 473–90, doi:10.1007/978-3-319-08867-9_31.
short: K. Chatterjee, M. Chmelik, P. Daca, in:, Springer, 2014, pp. 473–490.
conference:
end_date: 2014-07-22
location: Vienna, Austria
name: 'CAV: Computer Aided Verification'
start_date: 2014-07-18
corr_author: '1'
date_created: 2018-12-11T11:55:30Z
date_published: 2014-07-01T00:00:00Z
date_updated: 2026-04-15T10:02:12Z
day: '01'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1007/978-3-319-08867-9_31
ec_funded: 1
intvolume: ' 8559'
language:
- iso: eng
month: '07'
oa_version: None
page: 473 - 490
project:
- _id: 2584A770-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: P 23499-N23
name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11407
name: Game Theory
- _id: 25F5A88A-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11402-N23
name: Moderne Concurrency Paradigms
- _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
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
publication_status: published
publisher: Springer
publist_id: '4978'
quality_controlled: '1'
related_material:
record:
- id: '5412'
relation: earlier_version
status: public
- id: '5413'
relation: earlier_version
status: public
- id: '5414'
relation: earlier_version
status: public
- id: '1155'
relation: dissertation_contains
status: public
scopus_import: '1'
status: public
title: CEGAR for qualitative analysis of probabilistic systems
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 8559
year: '2014'
...
---
_id: '2854'
abstract:
- lang: eng
text: We consider concurrent games played on graphs. At every round of a game, each
player simultaneously and independently selects a move; the moves jointly determine
the transition to a successor state. Two basic objectives are the safety objective
to stay forever in a given set of states, and its dual, the reachability objective
to reach a given set of states. First, we present a simple proof of the fact that
in concurrent reachability games, for all ε>0, memoryless ε-optimal strategies
exist. A memoryless strategy is independent of the history of plays, and an ε-optimal
strategy achieves the objective with probability within ε of the value of the
game. In contrast to previous proofs of this fact, our proof is more elementary
and more combinatorial. Second, we present a strategy-improvement (a.k.a. policy-iteration)
algorithm for concurrent games with reachability objectives. Finally, we present
a strategy-improvement algorithm for turn-based stochastic games (where each player
selects moves in turns) with safety objectives. Our algorithms yield sequences
of player-1 strategies which ensure probabilities of winning that converge monotonically
(from below) to the value of the game. © 2012 Elsevier Inc.
acknowledgement: This work was partially supported in part by the NSF grants CCR-0132780,
CNS-0720884, CCR-0225610, by the Swiss National Science Foundation, ERC Start Grant
Graph Games (Project No. 279307), FWF NFN Grant S11407-N23 (RiSE), and a Microsoft
faculty fellows
article_processing_charge: No
article_type: original
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Luca
full_name: De Alfaro, Luca
last_name: De Alfaro
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
citation:
ama: Chatterjee K, De Alfaro L, Henzinger TA. Strategy improvement for concurrent
reachability and turn based stochastic safety games. Journal of Computer and
System Sciences. 2013;79(5):640-657. doi:10.1016/j.jcss.2012.12.001
apa: Chatterjee, K., De Alfaro, L., & Henzinger, T. A. (2013). Strategy improvement
for concurrent reachability and turn based stochastic safety games. Journal
of Computer and System Sciences. Elsevier. https://doi.org/10.1016/j.jcss.2012.12.001
chicago: Chatterjee, Krishnendu, Luca De Alfaro, and Thomas A Henzinger. “Strategy
Improvement for Concurrent Reachability and Turn Based Stochastic Safety Games.”
Journal of Computer and System Sciences. Elsevier, 2013. https://doi.org/10.1016/j.jcss.2012.12.001.
ieee: K. Chatterjee, L. De Alfaro, and T. A. Henzinger, “Strategy improvement for
concurrent reachability and turn based stochastic safety games,” Journal of
Computer and System Sciences, vol. 79, no. 5. Elsevier, pp. 640–657, 2013.
ista: Chatterjee K, De Alfaro L, Henzinger TA. 2013. Strategy improvement for concurrent
reachability and turn based stochastic safety games. Journal of Computer and System
Sciences. 79(5), 640–657.
mla: Chatterjee, Krishnendu, et al. “Strategy Improvement for Concurrent Reachability
and Turn Based Stochastic Safety Games.” Journal of Computer and System Sciences,
vol. 79, no. 5, Elsevier, 2013, pp. 640–57, doi:10.1016/j.jcss.2012.12.001.
short: K. Chatterjee, L. De Alfaro, T.A. Henzinger, Journal of Computer and System
Sciences 79 (2013) 640–657.
corr_author: '1'
date_created: 2018-12-11T11:59:57Z
date_published: 2013-08-01T00:00:00Z
date_updated: 2025-09-29T13:40:38Z
day: '01'
ddc:
- '000'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1016/j.jcss.2012.12.001
ec_funded: 1
external_id:
isi:
- '000316837300011'
file:
- access_level: open_access
checksum: 6d3ee12cceb946a0abe69594b6a22409
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:18:48Z
date_updated: 2020-07-14T12:45:51Z
file_id: '5370'
file_name: IST-2015-388-v1+1_1-s2.0-S0022000012001778-main.pdf
file_size: 425488
relation: main_file
file_date_updated: 2020-07-14T12:45:51Z
has_accepted_license: '1'
intvolume: ' 79'
isi: 1
issue: '5'
language:
- iso: eng
license: https://creativecommons.org/licenses/by-nc-nd/4.0/
month: '08'
oa: 1
oa_version: Published Version
page: 640 - 657
project:
- _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
- _id: 2587B514-B435-11E9-9278-68D0E5697425
name: Microsoft Research Faculty Fellowship
publication: Journal of Computer and System Sciences
publication_status: published
publisher: Elsevier
publist_id: '3938'
pubrep_id: '388'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Strategy improvement for concurrent reachability and turn based stochastic
safety games
tmp:
image: /images/cc_by_nc_nd.png
legal_code_url: https://creativecommons.org/licenses/by-nc-nd/4.0/legalcode
name: Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International
(CC BY-NC-ND 4.0)
short: CC BY-NC-ND (4.0)
type: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 79
year: '2013'
...
---
_id: '2885'
abstract:
- lang: eng
text: 'This volume contains the post-proceedings of the 8th Doctoral Workshop on
Mathematical and Engineering Methods in Computer Science, MEMICS 2012, held in
Znojmo, Czech Republic, in October, 2012. The 13 thoroughly revised papers were
carefully selected out of 31 submissions and are presented together with 6 invited
papers. The topics covered by the papers include: computer-aided analysis and
verification, applications of game theory in computer science, networks and security,
modern trends of graph theory in computer science, electronic systems design and
testing, and quantum information processing.'
acknowledgement: Red Hat Czech Republic, Y Soft
alternative_title:
- LNCS
citation:
ama: Kucera A, Henzinger TA, Nesetril J, Vojnar T, Antos D, eds. Mathematical
and Engineering Methods in Computer Science. Vol 7721. Springer; 2013:1-228.
doi:10.1007/978-3-642-36046-6
apa: 'Kucera, A., Henzinger, T. A., Nesetril, J., Vojnar, T., & Antos, D. (Eds.).
(2013). Mathematical and Engineering Methods in Computer Science (Vol.
7721, pp. 1–228). Presented at the MEMICS: Mathematical and Engineering methods
in computer science, Znojmo, Czech Republic: Springer. https://doi.org/10.1007/978-3-642-36046-6'
chicago: Kucera, Antonin, Thomas A Henzinger, Jaroslav Nesetril, Tomas Vojnar, and
David Antos, eds. Mathematical and Engineering Methods in Computer Science.
Vol. 7721. Lecture Notes in Computer Science. Springer, 2013. https://doi.org/10.1007/978-3-642-36046-6.
ieee: A. Kucera, T. A. Henzinger, J. Nesetril, T. Vojnar, and D. Antos, Eds., Mathematical
and Engineering Methods in Computer Science, vol. 7721. Springer, 2013, pp.
1–228.
ista: Kucera A, Henzinger TA, Nesetril J, Vojnar T, Antos D eds. 2013. Mathematical
and Engineering Methods in Computer Science, Springer,p.
mla: Kucera, Antonin, et al., editors. Mathematical and Engineering Methods in
Computer Science. Vol. 7721, Springer, 2013, pp. 1–228, doi:10.1007/978-3-642-36046-6.
short: A. Kucera, T.A. Henzinger, J. Nesetril, T. Vojnar, D. Antos, eds., Mathematical
and Engineering Methods in Computer Science, Springer, 2013.
conference:
end_date: 2012-10-28
location: Znojmo, Czech Republic
name: 'MEMICS: Mathematical and Engineering methods in computer science'
start_date: 2012-10-25
date_created: 2018-12-11T12:00:08Z
date_published: 2013-01-09T00:00:00Z
date_updated: 2019-08-02T12:37:55Z
day: '09'
department:
- _id: ToHe
doi: 10.1007/978-3-642-36046-6
editor:
- first_name: Antonin
full_name: Kucera, Antonin
last_name: Kucera
- 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: Jaroslav
full_name: Nesetril, Jaroslav
last_name: Nesetril
- first_name: Tomas
full_name: Vojnar, Tomas
last_name: Vojnar
- first_name: David
full_name: Antos, David
last_name: Antos
intvolume: ' 7721'
language:
- iso: eng
month: '01'
oa_version: None
page: 1 - 228
publication_status: published
publisher: Springer
publist_id: '3874'
quality_controlled: '1'
series_title: Lecture Notes in Computer Science
status: public
title: Mathematical and Engineering Methods in Computer Science
type: conference_editor
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 7721
year: '2013'
...
---
OA_place: repository
OA_type: green
_id: '1376'
abstract:
- lang: eng
text: 'We consider the distributed synthesis problem for temporal logic specifications.
Traditionally, the problem has been studied for LTL, and the previous results
show that the problem is decidable iff there is no information fork in the architecture.
We consider the problem for fragments of LTL and our main results are as follows:
(1) We show that the problem is undecidable for architectures with information
forks even for the fragment of LTL with temporal operators restricted to next
and eventually. (2) For specifications restricted to globally along with non-nested
next operators, we establish decidability (in EXPSPACE) for star architectures
where the processes receive disjoint inputs, whereas we establish undecidability
for architectures containing an information fork-meet structure. (3) Finally,
we consider LTL without the next operator, and establish decidability (NEXPTIME-complete)
for all architectures for a fragment that consists of a set of safety assumptions,
and a set of guarantees where each guarantee is a safety, reachability, or liveness
condition.'
article_processing_charge: No
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
- first_name: Andreas
full_name: Pavlogiannis, Andreas
id: 49704004-F248-11E8-B48F-1D18A9856A87
last_name: Pavlogiannis
orcid: 0000-0002-8943-0722
citation:
ama: 'Chatterjee K, Henzinger TA, Otop J, Pavlogiannis A. Distributed synthesis
for LTL fragments. In: 13th International Conference on Formal Methods in Computer-Aided
Design. IEEE; 2013:18-25. doi:10.1109/FMCAD.2013.6679386'
apa: 'Chatterjee, K., Henzinger, T. A., Otop, J., & Pavlogiannis, A. (2013).
Distributed synthesis for LTL fragments. In 13th International Conference on
Formal Methods in Computer-Aided Design (pp. 18–25). Portland, OR, United
States: IEEE. https://doi.org/10.1109/FMCAD.2013.6679386'
chicago: Chatterjee, Krishnendu, Thomas A Henzinger, Jan Otop, and Andreas Pavlogiannis.
“Distributed Synthesis for LTL Fragments.” In 13th International Conference
on Formal Methods in Computer-Aided Design, 18–25. IEEE, 2013. https://doi.org/10.1109/FMCAD.2013.6679386.
ieee: K. Chatterjee, T. A. Henzinger, J. Otop, and A. Pavlogiannis, “Distributed
synthesis for LTL fragments,” in 13th International Conference on Formal Methods
in Computer-Aided Design, Portland, OR, United States, 2013, pp. 18–25.
ista: 'Chatterjee K, Henzinger TA, Otop J, Pavlogiannis A. 2013. Distributed synthesis
for LTL fragments. 13th International Conference on Formal Methods in Computer-Aided
Design. FMCAD: Formal Methods in Computer-Aided Design, 18–25.'
mla: Chatterjee, Krishnendu, et al. “Distributed Synthesis for LTL Fragments.” 13th
International Conference on Formal Methods in Computer-Aided Design, IEEE,
2013, pp. 18–25, doi:10.1109/FMCAD.2013.6679386.
short: K. Chatterjee, T.A. Henzinger, J. Otop, A. Pavlogiannis, in:, 13th International
Conference on Formal Methods in Computer-Aided Design, IEEE, 2013, pp. 18–25.
conference:
end_date: 2013-10-23
location: Portland, OR, United States
name: 'FMCAD: Formal Methods in Computer-Aided Design'
start_date: 2013-10-20
corr_author: '1'
date_created: 2018-12-11T11:51:40Z
date_published: 2013-12-11T00:00:00Z
date_updated: 2025-06-26T08:33:43Z
day: '11'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1109/FMCAD.2013.6679386
ec_funded: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.15479/AT:IST-2013-130-v1-1
month: '12'
oa: 1
oa_version: Preprint
page: 18 - 25
project:
- _id: 2584A770-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: P 23499-N23
name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _id: 2587B514-B435-11E9-9278-68D0E5697425
name: Microsoft Research Faculty Fellowship
publication: 13th International Conference on Formal Methods in Computer-Aided Design
publication_status: published
publisher: IEEE
publist_id: '5835'
quality_controlled: '1'
related_material:
record:
- id: '5406'
relation: earlier_version
status: public
scopus_import: '1'
status: public
title: Distributed synthesis for LTL fragments
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2013'
...
---
_id: '1385'
abstract:
- lang: eng
text: It is often difficult to correctly implement a Boolean controller for a complex
system, especially when concurrency is involved. Yet, it may be easy to formally
specify a controller. For instance, for a pipelined processor it suffices to state
that the visible behavior of the pipelined system should be identical to a non-pipelined
reference system (Burch-Dill paradigm). We present a novel procedure to efficiently
synthesize multiple Boolean control signals from a specification given as a quantified
first-order formula (with a specific quantifier structure). Our approach uses
uninterpreted functions to abstract details of the design. We construct an unsatisfiable
SMT formula from the given specification. Then, from just one proof of unsatisfiability,
we use a variant of Craig interpolation to compute multiple coordinated interpolants
that implement the Boolean control signals. Our method avoids iterative learning
and back-substitution of the control functions. We applied our approach to synthesize
a controller for a simple two-stage pipelined processor, and present first experimental
results.
acknowledgement: "This research was supported by the European Commission through project\r\nDIAMOND
\ (FP7-2009-IST-4-248613), and QUAINT (I774-N23), "
arxiv: 1
author:
- first_name: Georg
full_name: Hofferek, Georg
last_name: Hofferek
- first_name: Ashutosh
full_name: Gupta, Ashutosh
id: 335E5684-F248-11E8-B48F-1D18A9856A87
last_name: Gupta
- first_name: Bettina
full_name: Könighofer, Bettina
last_name: Könighofer
- first_name: Jie
full_name: Jiang, Jie
last_name: Jiang
- first_name: Roderick
full_name: Bloem, Roderick
last_name: Bloem
citation:
ama: 'Hofferek G, Gupta A, Könighofer B, Jiang J, Bloem R. Synthesizing multiple
boolean functions using interpolation on a single proof. In: 2013 Formal Methods
in Computer-Aided Design. IEEE; 2013:77-84. doi:10.1109/FMCAD.2013.6679394'
apa: 'Hofferek, G., Gupta, A., Könighofer, B., Jiang, J., & Bloem, R. (2013).
Synthesizing multiple boolean functions using interpolation on a single proof.
In 2013 Formal Methods in Computer-Aided Design (pp. 77–84). Portland,
OR, United States: IEEE. https://doi.org/10.1109/FMCAD.2013.6679394'
chicago: Hofferek, Georg, Ashutosh Gupta, Bettina Könighofer, Jie Jiang, and Roderick
Bloem. “Synthesizing Multiple Boolean Functions Using Interpolation on a Single
Proof.” In 2013 Formal Methods in Computer-Aided Design, 77–84. IEEE, 2013.
https://doi.org/10.1109/FMCAD.2013.6679394.
ieee: G. Hofferek, A. Gupta, B. Könighofer, J. Jiang, and R. Bloem, “Synthesizing
multiple boolean functions using interpolation on a single proof,” in 2013
Formal Methods in Computer-Aided Design, Portland, OR, United States, 2013,
pp. 77–84.
ista: 'Hofferek G, Gupta A, Könighofer B, Jiang J, Bloem R. 2013. Synthesizing multiple
boolean functions using interpolation on a single proof. 2013 Formal Methods in
Computer-Aided Design. FMCAD: Formal Methods in Computer-Aided Design, 77–84.'
mla: Hofferek, Georg, et al. “Synthesizing Multiple Boolean Functions Using Interpolation
on a Single Proof.” 2013 Formal Methods in Computer-Aided Design, IEEE,
2013, pp. 77–84, doi:10.1109/FMCAD.2013.6679394.
short: G. Hofferek, A. Gupta, B. Könighofer, J. Jiang, R. Bloem, in:, 2013 Formal
Methods in Computer-Aided Design, IEEE, 2013, pp. 77–84.
conference:
end_date: 2013-10-23
location: Portland, OR, United States
name: 'FMCAD: Formal Methods in Computer-Aided Design'
start_date: 2013-10-20
date_created: 2018-12-11T11:51:43Z
date_published: 2013-12-11T00:00:00Z
date_updated: 2024-10-21T06:02:56Z
day: '11'
department:
- _id: ToHe
doi: 10.1109/FMCAD.2013.6679394
ec_funded: 1
external_id:
arxiv:
- '1308.4767'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1308.4767
month: '12'
oa: 1
oa_version: Preprint
page: 77 - 84
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
publication: 2013 Formal Methods in Computer-Aided Design
publication_status: published
publisher: IEEE
publist_id: '5825'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Synthesizing multiple boolean functions using interpolation on a single proof
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2013'
...
---
_id: '1387'
abstract:
- lang: eng
text: Choices made by nondeterministic word automata depend on both the past (the
prefix of the word read so far) and the future (the suffix yet to be read). In
several applications, most notably synthesis, the future is diverse or unknown,
leading to algorithms that are based on deterministic automata. Hoping to retain
some of the advantages of nondeterministic automata, researchers have studied
restricted classes of nondeterministic automata. Three such classes are nondeterministic
automata that are good for trees (GFT; i.e., ones that can be expanded to tree
automata accepting the derived tree languages, thus whose choices should satisfy
diverse futures), good for games (GFG; i.e., ones whose choices depend only on
the past), and determinizable by pruning (DBP; i.e., ones that embody equivalent
deterministic automata). The theoretical properties and relative merits of the
different classes are still open, having vagueness on whether they really differ
from deterministic automata. In particular, while DBP ⊆ GFG ⊆ GFT, it is not known
whether every GFT automaton is GFG and whether every GFG automaton is DBP. Also
open is the possible succinctness of GFG and GFT automata compared to deterministic
automata. We study these problems for ω-regular automata with all common acceptance
conditions. We show that GFT=GFG⊃DBP, and describe a determinization construction
for GFG automata.
acknowledgement: and ERC Grant QUALITY.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Udi
full_name: Boker, Udi
id: 31E297B6-F248-11E8-B48F-1D18A9856A87
last_name: Boker
- first_name: Denis
full_name: Kuperberg, Denis
last_name: Kuperberg
- first_name: Orna
full_name: Kupferman, Orna
last_name: Kupferman
- first_name: Michał
full_name: Skrzypczak, Michał
last_name: Skrzypczak
citation:
ama: Boker U, Kuperberg D, Kupferman O, Skrzypczak M. Nondeterminism in the presence
of a diverse or unknown future. 2013;7966(PART 2):89-100. doi:10.1007/978-3-642-39212-2_11
apa: 'Boker, U., Kuperberg, D., Kupferman, O., & Skrzypczak, M. (2013). Nondeterminism
in the presence of a diverse or unknown future. Presented at the ICALP: Automata,
Languages and Programming, Riga, Latvia: Springer. https://doi.org/10.1007/978-3-642-39212-2_11'
chicago: Boker, Udi, Denis Kuperberg, Orna Kupferman, and Michał Skrzypczak. “Nondeterminism
in the Presence of a Diverse or Unknown Future.” Lecture Notes in Computer Science.
Springer, 2013. https://doi.org/10.1007/978-3-642-39212-2_11.
ieee: U. Boker, D. Kuperberg, O. Kupferman, and M. Skrzypczak, “Nondeterminism in
the presence of a diverse or unknown future,” vol. 7966, no. PART 2. Springer,
pp. 89–100, 2013.
ista: Boker U, Kuperberg D, Kupferman O, Skrzypczak M. 2013. Nondeterminism in the
presence of a diverse or unknown future. 7966(PART 2), 89–100.
mla: Boker, Udi, et al. Nondeterminism in the Presence of a Diverse or Unknown
Future. Vol. 7966, no. PART 2, Springer, 2013, pp. 89–100, doi:10.1007/978-3-642-39212-2_11.
short: U. Boker, D. Kuperberg, O. Kupferman, M. Skrzypczak, 7966 (2013) 89–100.
conference:
end_date: 2013-07-12
location: Riga, Latvia
name: 'ICALP: Automata, Languages and Programming'
start_date: 2013-07-08
date_created: 2018-12-11T11:51:44Z
date_published: 2013-07-01T00:00:00Z
date_updated: 2020-08-11T10:09:09Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-642-39212-2_11
ec_funded: 1
file:
- access_level: open_access
checksum: 98bc02e3793072e279ec8d364b381ff3
content_type: application/pdf
creator: dernst
date_created: 2020-05-15T11:05:50Z
date_updated: 2020-07-14T12:44:48Z
file_id: '7857'
file_name: 2013_ICALP_Boker.pdf
file_size: 276982
relation: main_file
file_date_updated: 2020-07-14T12:44:48Z
has_accepted_license: '1'
intvolume: ' 7966'
issue: PART 2
language:
- iso: eng
month: '07'
oa: 1
oa_version: Submitted Version
page: 89 - 100
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
publication_status: published
publisher: Springer
publist_id: '5823'
quality_controlled: '1'
scopus_import: 1
series_title: Lecture Notes in Computer Science
status: public
title: Nondeterminism in the presence of a diverse or unknown future
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 7966
year: '2013'
...
---
_id: '10898'
abstract:
- lang: eng
text: A prominent remedy to multicore scalability issues in concurrent data structure
implementations is to relax the sequential specification of the data structure.
We present distributed queues (DQ), a new family of relaxed concurrent queue implementations.
DQs implement relaxed queues with linearizable emptiness check and either configurable
or bounded out-of-order behavior or pool behavior. Our experiments show that DQs
outperform and outscale in micro- and macrobenchmarks all strict and relaxed queue
as well as pool implementations that we considered.
acknowledgement: This work has been supported by the European Research Council advanced
grant on Quantitative Reactive Modeling (QUAREM) and the National Research Network
RiSE on Rigorous Systems Engineering (Austrian Science Fund S11402-N23 and S11404-N23).
article_number: '17'
article_processing_charge: No
author:
- first_name: Andreas
full_name: Haas, Andreas
last_name: Haas
- first_name: Michael
full_name: Lippautz, Michael
last_name: Lippautz
- 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: Hannes
full_name: Payer, Hannes
last_name: Payer
- first_name: Ana
full_name: Sokolova, Ana
last_name: Sokolova
- first_name: Christoph M.
full_name: Kirsch, Christoph M.
last_name: Kirsch
- first_name: Ali
full_name: Sezgin, Ali
id: 4C7638DA-F248-11E8-B48F-1D18A9856A87
last_name: Sezgin
citation:
ama: 'Haas A, Lippautz M, Henzinger TA, et al. Distributed queues in shared memory:
Multicore performance and scalability through quantitative relaxation. In: Proceedings
of the ACM International Conference on Computing Frontiers - CF ’13. ACM;
2013. doi:10.1145/2482767.2482789'
apa: 'Haas, A., Lippautz, M., Henzinger, T. A., Payer, H., Sokolova, A., Kirsch,
C. M., & Sezgin, A. (2013). Distributed queues in shared memory: Multicore
performance and scalability through quantitative relaxation. In Proceedings
of the ACM International Conference on Computing Frontiers - CF ’13. Ischia,
Italy: ACM. https://doi.org/10.1145/2482767.2482789'
chicago: 'Haas, Andreas, Michael Lippautz, Thomas A Henzinger, Hannes Payer, Ana
Sokolova, Christoph M. Kirsch, and Ali Sezgin. “Distributed Queues in Shared Memory:
Multicore Performance and Scalability through Quantitative Relaxation.” In Proceedings
of the ACM International Conference on Computing Frontiers - CF ’13. ACM,
2013. https://doi.org/10.1145/2482767.2482789.'
ieee: 'A. Haas et al., “Distributed queues in shared memory: Multicore performance
and scalability through quantitative relaxation,” in Proceedings of the ACM
International Conference on Computing Frontiers - CF ’13, Ischia, Italy, 2013,
no. 5.'
ista: 'Haas A, Lippautz M, Henzinger TA, Payer H, Sokolova A, Kirsch CM, Sezgin
A. 2013. Distributed queues in shared memory: Multicore performance and scalability
through quantitative relaxation. Proceedings of the ACM International Conference
on Computing Frontiers - CF ’13. CF: Conference on Computing Frontiers, 17.'
mla: 'Haas, Andreas, et al. “Distributed Queues in Shared Memory: Multicore Performance
and Scalability through Quantitative Relaxation.” Proceedings of the ACM International
Conference on Computing Frontiers - CF ’13, no. 5, 17, ACM, 2013, doi:10.1145/2482767.2482789.'
short: A. Haas, M. Lippautz, T.A. Henzinger, H. Payer, A. Sokolova, C.M. Kirsch,
A. Sezgin, in:, Proceedings of the ACM International Conference on Computing Frontiers
- CF ’13, ACM, 2013.
conference:
end_date: 2013-05-16
location: Ischia, Italy
name: 'CF: Conference on Computing Frontiers'
start_date: 2013-05-14
date_created: 2022-03-21T07:33:22Z
date_published: 2013-05-14T00:00:00Z
date_updated: 2025-05-14T11:23:58Z
day: '14'
department:
- _id: ToHe
doi: 10.1145/2482767.2482789
ec_funded: 1
issue: '5'
language:
- iso: eng
month: '05'
oa_version: None
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
publication: Proceedings of the ACM International Conference on Computing Frontiers
- CF '13
publication_identifier:
isbn:
- 978-145032053-5
publication_status: published
publisher: ACM
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'Distributed queues in shared memory: Multicore performance and scalability
through quantitative relaxation'
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2013'
...
---
_id: '2181'
abstract:
- lang: eng
text: 'There is a trade-off between performance and correctness in implementing
concurrent data structures. Better performance may be achieved at the expense
of relaxing correctness, by redefining the semantics of data structures. We address
such a redefinition of data structure semantics and present a systematic and formal
framework for obtaining new data structures by quantitatively relaxing existing
ones. We view a data structure as a sequential specification S containing all
"legal" sequences over an alphabet of method calls. Relaxing the data
structure corresponds to defining a distance from any sequence over the alphabet
to the sequential specification: the k-relaxed sequential specification contains
all sequences over the alphabet within distance k from the original specification.
In contrast to other existing work, our relaxations are semantic (distance in
terms of data structure states). As an instantiation of our framework, we present
two simple yet generic relaxation schemes, called out-of-order and stuttering
relaxation, along with several ways of computing distances. We show that the out-of-order
relaxation, when further instantiated to stacks, queues, and priority queues,
amounts to tolerating bounded out-of-order behavior, which cannot be captured
by a purely syntactic relaxation (distance in terms of sequence manipulation,
e.g. edit distance). We give concurrent implementations of relaxed data structures
and demonstrate that bounded relaxations provide the means for trading correctness
for performance in a controlled way. The relaxations are monotonic which further
highlights the trade-off: increasing k increases the number of permitted sequences,
which as we demonstrate can lead to better performance. Finally, since a relaxed
stack or queue also implements a pool, we actually have new concurrent pool implementations
that outperform the state-of-the-art ones.'
acknowledgement: ' and an Elise Richter Fellowship (Austrian Science Fund V00125). '
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: Christoph
full_name: Kirsch, Christoph
last_name: Kirsch
- first_name: Hannes
full_name: Payer, Hannes
last_name: Payer
- first_name: Ali
full_name: Sezgin, Ali
id: 4C7638DA-F248-11E8-B48F-1D18A9856A87
last_name: Sezgin
- first_name: Ana
full_name: Sokolova, Ana
last_name: Sokolova
citation:
ama: 'Henzinger TA, Kirsch C, Payer H, Sezgin A, Sokolova A. Quantitative relaxation
of concurrent data structures. In: Proceedings of the 40th Annual ACM SIGPLAN-SIGACT
Symposium on Principles of Programming Language. ACM; 2013:317-328. doi:10.1145/2429069.2429109'
apa: 'Henzinger, T. A., Kirsch, C., Payer, H., Sezgin, A., & Sokolova, A. (2013).
Quantitative relaxation of concurrent data structures. In Proceedings of the
40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming language
(pp. 317–328). Rome, Italy: ACM. https://doi.org/10.1145/2429069.2429109'
chicago: Henzinger, Thomas A, Christoph Kirsch, Hannes Payer, Ali Sezgin, and Ana
Sokolova. “Quantitative Relaxation of Concurrent Data Structures.” In Proceedings
of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Language,
317–28. ACM, 2013. https://doi.org/10.1145/2429069.2429109.
ieee: T. A. Henzinger, C. Kirsch, H. Payer, A. Sezgin, and A. Sokolova, “Quantitative
relaxation of concurrent data structures,” in Proceedings of the 40th annual
ACM SIGPLAN-SIGACT symposium on Principles of programming language, Rome,
Italy, 2013, pp. 317–328.
ista: 'Henzinger TA, Kirsch C, Payer H, Sezgin A, Sokolova A. 2013. Quantitative
relaxation of concurrent data structures. Proceedings of the 40th annual ACM SIGPLAN-SIGACT
symposium on Principles of programming language. POPL: Principles of Programming
Languages, 317–328.'
mla: Henzinger, Thomas A., et al. “Quantitative Relaxation of Concurrent Data Structures.”
Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of
Programming Language, ACM, 2013, pp. 317–28, doi:10.1145/2429069.2429109.
short: T.A. Henzinger, C. Kirsch, H. Payer, A. Sezgin, A. Sokolova, in:, Proceedings
of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Language,
ACM, 2013, pp. 317–328.
conference:
end_date: 2013-01-25
location: Rome, Italy
name: 'POPL: Principles of Programming Languages'
start_date: 2013-01-23
date_created: 2018-12-11T11:56:11Z
date_published: 2013-01-01T00:00:00Z
date_updated: 2023-02-21T16:06:49Z
day: '01'
ddc:
- '000'
- '004'
department:
- _id: ToHe
doi: 10.1145/2429069.2429109
ec_funded: 1
file:
- access_level: open_access
checksum: adf465e70948f4e80e48057524516456
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:14:33Z
date_updated: 2020-07-14T12:45:31Z
file_id: '5086'
file_name: IST-2014-198-v1+1_popl128-henzinger-clean.pdf
file_size: 294689
relation: main_file
file_date_updated: 2020-07-14T12:45:31Z
has_accepted_license: '1'
language:
- iso: eng
month: '01'
oa: 1
oa_version: Submitted Version
page: 317 - 328
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
publication: Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles
of programming language
publication_identifier:
isbn:
- 978-1-4503-1832-7
publication_status: published
publisher: ACM
publist_id: '4801'
pubrep_id: '198'
quality_controlled: '1'
related_material:
record:
- id: '10901'
relation: later_version
status: deleted
scopus_import: 1
status: public
title: Quantitative relaxation of concurrent data structures
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2013'
...
---
_id: '2182'
abstract:
- lang: eng
text: We propose a general framework for abstraction with respect to quantitative
properties, such as worst-case execution time, or power consumption. Our framework
provides a systematic way for counter-example guided abstraction refinement for
quantitative properties. The salient aspect of the framework is that it allows
anytime verification, that is, verification algorithms that can be stopped at
any time (for example, due to exhaustion of memory), and report approximations
that improve monotonically when the algorithms are given more time. We instantiate
the framework with a number of quantitative abstractions and refinement schemes,
which differ in terms of how much quantitative information they keep from the
original system. We introduce both state-based and trace-based quantitative abstractions,
and we describe conditions that define classes of quantitative properties for
which the abstractions provide over-approximations. We give algorithms for evaluating
the quantitative properties on the abstract systems. We present algorithms for
counter-example based refinements for quantitative properties for both state-based
and segment-based abstractions. We perform a case study on worst-case execution
time of executables to evaluate the anytime verification aspect and the quantitative
abstractions we proposed.
author:
- first_name: Pavol
full_name: Cerny, Pavol
id: 4DCBEFFE-F248-11E8-B48F-1D18A9856A87
last_name: Cerny
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Arjun
full_name: Radhakrishna, Arjun
id: 3B51CAC4-F248-11E8-B48F-1D18A9856A87
last_name: Radhakrishna
citation:
ama: 'Cerny P, Henzinger TA, Radhakrishna A. Quantitative abstraction refinement.
In: Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles
of Programming Language. ACM; 2013:115-128. doi:10.1145/2429069.2429085'
apa: 'Cerny, P., Henzinger, T. A., & Radhakrishna, A. (2013). Quantitative abstraction
refinement. In Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium
on Principles of programming language (pp. 115–128). Rome, Italy: ACM. https://doi.org/10.1145/2429069.2429085'
chicago: Cerny, Pavol, Thomas A Henzinger, and Arjun Radhakrishna. “Quantitative
Abstraction Refinement.” In Proceedings of the 40th Annual ACM SIGPLAN-SIGACT
Symposium on Principles of Programming Language, 115–28. ACM, 2013. https://doi.org/10.1145/2429069.2429085.
ieee: P. Cerny, T. A. Henzinger, and A. Radhakrishna, “Quantitative abstraction
refinement,” in Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium
on Principles of programming language, Rome, Italy, 2013, pp. 115–128.
ista: 'Cerny P, Henzinger TA, Radhakrishna A. 2013. Quantitative abstraction refinement.
Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming
language. POPL: Principles of Programming Languages, 115–128.'
mla: Cerny, Pavol, et al. “Quantitative Abstraction Refinement.” Proceedings
of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Language,
ACM, 2013, pp. 115–28, doi:10.1145/2429069.2429085.
short: P. Cerny, T.A. Henzinger, A. Radhakrishna, in:, Proceedings of the 40th Annual
ACM SIGPLAN-SIGACT Symposium on Principles of Programming Language, ACM, 2013,
pp. 115–128.
conference:
end_date: 2013-01-25
location: Rome, Italy
name: 'POPL: Principles of Programming Languages'
start_date: 2013-07-23
corr_author: '1'
date_created: 2018-12-11T11:56:11Z
date_published: 2013-01-01T00:00:00Z
date_updated: 2024-10-09T20:55:21Z
day: '01'
department:
- _id: ToHe
doi: 10.1145/2429069.2429085
ec_funded: 1
language:
- iso: eng
month: '01'
oa_version: None
page: 115 - 128
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
publication: Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles
of programming language
publication_status: published
publisher: ACM
publist_id: '4800'
quality_controlled: '1'
scopus_import: 1
status: public
title: Quantitative abstraction refinement
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2013'
...
---
_id: '2237'
abstract:
- lang: eng
text: We describe new extensions of the Vampire theorem prover for computing tree
interpolants. These extensions generalize Craig interpolation in Vampire, and
can also be used to derive sequence interpolants. We evaluated our implementation
on a large number of examples over the theory of linear integer arithmetic and
integer-indexed arrays, with and without quantifiers. When compared to other methods,
our experiments show that some examples could only be solved by our implementation.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Régis
full_name: Blanc, Régis
last_name: Blanc
- first_name: Ashutosh
full_name: Gupta, Ashutosh
id: 335E5684-F248-11E8-B48F-1D18A9856A87
last_name: Gupta
- first_name: Laura
full_name: Kovács, Laura
last_name: Kovács
- first_name: Bernhard
full_name: Kragl, Bernhard
id: 320FC952-F248-11E8-B48F-1D18A9856A87
last_name: Kragl
orcid: 0000-0001-7745-9117
citation:
ama: Blanc R, Gupta A, Kovács L, Kragl B. Tree interpolation in Vampire. 2013;8312:173-181.
doi:10.1007/978-3-642-45221-5_13
apa: 'Blanc, R., Gupta, A., Kovács, L., & Kragl, B. (2013). Tree interpolation
in Vampire. Presented at the LPAR: Logic for Programming, Artificial Intelligence,
and Reasoning, Stellenbosch, South Africa: Springer. https://doi.org/10.1007/978-3-642-45221-5_13'
chicago: Blanc, Régis, Ashutosh Gupta, Laura Kovács, and Bernhard Kragl. “Tree Interpolation
in Vampire.” Lecture Notes in Computer Science. Springer, 2013. https://doi.org/10.1007/978-3-642-45221-5_13.
ieee: R. Blanc, A. Gupta, L. Kovács, and B. Kragl, “Tree interpolation in Vampire,”
vol. 8312. Springer, pp. 173–181, 2013.
ista: Blanc R, Gupta A, Kovács L, Kragl B. 2013. Tree interpolation in Vampire.
8312, 173–181.
mla: Blanc, Régis, et al. Tree Interpolation in Vampire. Vol. 8312, Springer,
2013, pp. 173–81, doi:10.1007/978-3-642-45221-5_13.
short: R. Blanc, A. Gupta, L. Kovács, B. Kragl, 8312 (2013) 173–181.
conference:
end_date: 2013-12-19
location: Stellenbosch, South Africa
name: 'LPAR: Logic for Programming, Artificial Intelligence, and Reasoning'
start_date: 2013-12-14
date_created: 2018-12-11T11:56:29Z
date_published: 2013-01-14T00:00:00Z
date_updated: 2020-08-11T10:09:42Z
day: '14'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-642-45221-5_13
file:
- access_level: open_access
checksum: 9cebaafca032e6769d273f393305c705
content_type: application/pdf
creator: dernst
date_created: 2020-05-15T11:10:40Z
date_updated: 2020-07-14T12:45:34Z
file_id: '7858'
file_name: 2013_LPAR_Blanc.pdf
file_size: 279206
relation: main_file
file_date_updated: 2020-07-14T12:45:34Z
has_accepted_license: '1'
intvolume: ' 8312'
language:
- iso: eng
month: '01'
oa: 1
oa_version: Submitted Version
page: 173 - 181
project:
- _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: '4724'
quality_controlled: '1'
scopus_import: 1
series_title: Lecture Notes in Computer Science
status: public
title: Tree interpolation in Vampire
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 8312
year: '2013'
...
---
_id: '2243'
abstract:
- lang: eng
text: We show that modal logic over universally first-order definable classes of
transitive frames is decidable. More precisely, let K be an arbitrary class of
transitive Kripke frames definable by a universal first-order sentence. We show
that the global and finite global satisfiability problems of modal logic over
K are decidable in NP, regardless of choice of K. We also show that the local
satisfiability and the finite local satisfiability problems of modal logic over
K are decidable in NEXPTIME.
alternative_title:
- LIPIcs
author:
- first_name: Jakub
full_name: Michaliszyn, Jakub
last_name: Michaliszyn
- first_name: Jan
full_name: Otop, Jan
id: 2FC5DA74-F248-11E8-B48F-1D18A9856A87
last_name: Otop
citation:
ama: Michaliszyn J, Otop J. Elementary modal logics over transitive structures.
2013;23:563-577. doi:10.4230/LIPIcs.CSL.2013.563
apa: 'Michaliszyn, J., & Otop, J. (2013). Elementary modal logics over transitive
structures. Presented at the CSL: Computer Science Logic, Torino, Italy: Schloss
Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CSL.2013.563'
chicago: Michaliszyn, Jakub, and Jan Otop. “Elementary Modal Logics over Transitive
Structures.” Leibniz International Proceedings in Informatics. Schloss Dagstuhl
- Leibniz-Zentrum für Informatik, 2013. https://doi.org/10.4230/LIPIcs.CSL.2013.563.
ieee: J. Michaliszyn and J. Otop, “Elementary modal logics over transitive structures,”
vol. 23. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, pp. 563–577, 2013.
ista: Michaliszyn J, Otop J. 2013. Elementary modal logics over transitive structures.
23, 563–577.
mla: Michaliszyn, Jakub, and Jan Otop. Elementary Modal Logics over Transitive
Structures. Vol. 23, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2013,
pp. 563–77, doi:10.4230/LIPIcs.CSL.2013.563.
short: J. Michaliszyn, J. Otop, 23 (2013) 563–577.
conference:
end_date: 2013-09-05
location: Torino, Italy
name: 'CSL: Computer Science Logic'
start_date: 2013-09-02
date_created: 2018-12-11T11:56:32Z
date_published: 2013-09-01T00:00:00Z
date_updated: 2020-08-11T10:09:42Z
day: '01'
ddc:
- '000'
- '004'
department:
- _id: ToHe
doi: 10.4230/LIPIcs.CSL.2013.563
ec_funded: 1
file:
- access_level: open_access
checksum: e0732e73a8b1e39483df7717d53e3e35
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:12:11Z
date_updated: 2020-07-14T12:45:34Z
file_id: '4929'
file_name: IST-2016-136-v1+2_39.pdf
file_size: 454915
relation: main_file
file_date_updated: 2020-07-14T12:45:34Z
has_accepted_license: '1'
intvolume: ' 23'
language:
- iso: eng
license: https://creativecommons.org/licenses/by/4.0/
month: '09'
oa: 1
oa_version: Published Version
page: 563 - 577
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '4708'
pubrep_id: '136'
quality_controlled: '1'
scopus_import: 1
series_title: Leibniz International Proceedings in Informatics
status: public
title: Elementary modal logics over transitive structures
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: 23
year: '2013'
...
---
_id: '2288'
abstract:
- lang: eng
text: This book constitutes the proceedings of the 11th International Conference
on Computational Methods in Systems Biology, CMSB 2013, held in Klosterneuburg,
Austria, in September 2013. The 15 regular papers included in this volume were
carefully reviewed and selected from 27 submissions. They deal with computational
models for all levels, from molecular and cellular, to organs and entire organisms.
alternative_title:
- LNCS
citation:
ama: Gupta A, Henzinger TA, eds. Computational Methods in Systems Biology.
Vol 8130. Springer; 2013. doi:10.1007/978-3-642-40708-6
apa: 'Gupta, A., & Henzinger, T. A. (Eds.). (2013). Computational Methods
in Systems Biology (Vol. 8130). Presented at the CMSB: Computational Methods
in Systems Biology, Klosterneuburg, Austria: Springer. https://doi.org/10.1007/978-3-642-40708-6'
chicago: Gupta, Ashutosh, and Thomas A Henzinger, eds. Computational Methods
in Systems Biology. Vol. 8130. Springer, 2013. https://doi.org/10.1007/978-3-642-40708-6.
ieee: A. Gupta and T. A. Henzinger, Eds., Computational Methods in Systems Biology,
vol. 8130. Springer, 2013.
ista: Gupta A, Henzinger TA eds. 2013. Computational Methods in Systems Biology,
Springer,p.
mla: Gupta, Ashutosh, and Thomas A. Henzinger, editors. Computational Methods
in Systems Biology. Vol. 8130, Springer, 2013, doi:10.1007/978-3-642-40708-6.
short: A. Gupta, T.A. Henzinger, eds., Computational Methods in Systems Biology,
Springer, 2013.
conference:
end_date: 2013-09-24
location: Klosterneuburg, Austria
name: 'CMSB: Computational Methods in Systems Biology'
start_date: 2013-09-22
corr_author: '1'
date_created: 2018-12-11T11:56:47Z
date_published: 2013-07-01T00:00:00Z
date_updated: 2024-10-09T20:55:17Z
day: '01'
department:
- _id: ToHe
doi: 10.1007/978-3-642-40708-6
editor:
- 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
intvolume: ' 8130'
language:
- iso: eng
month: '07'
oa_version: None
publication_identifier:
isbn:
- 978-3-642-40707-9
publication_status: published
publisher: Springer
publist_id: '4643'
quality_controlled: '1'
status: public
title: Computational Methods in Systems Biology
type: conference_editor
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 8130
year: '2013'
...
---
_id: '2289'
abstract:
- lang: eng
text: Formal verification aims to improve the quality of software by detecting errors
before they do harm. At the basis of formal verification is the logical notion
of correctness, which purports to capture whether or not a program behaves as
desired. We suggest that the boolean partition of software into correct and incorrect
programs falls short of the practical need to assess the behavior of software
in a more nuanced fashion against multiple criteria. We therefore propose to introduce
quantitative fitness measures for programs, specifically for measuring the function,
performance, and robustness of reactive programs such as concurrent processes.
This article describes the goals of the ERC Advanced Investigator Project QUAREM.
The project aims to build and evaluate a theory of quantitative fitness measures
for reactive models. Such a theory must strive to obtain quantitative generalizations
of the paradigms that have been success stories in qualitative reactive modeling,
such as compositionality, property-preserving abstraction and abstraction refinement,
model checking, and synthesis. The theory will be evaluated not only in the context
of software and hardware engineering, but also in the context of systems biology.
In particular, we will use the quantitative reactive models and fitness measures
developed in this project for testing hypotheses about the mechanisms behind data
from biological experiments.
author:
- 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: Henzinger TA. Quantitative reactive modeling and verification. Computer
Science Research and Development. 2013;28(4):331-344. doi:10.1007/s00450-013-0251-7
apa: Henzinger, T. A. (2013). Quantitative reactive modeling and verification. Computer
Science Research and Development. Springer. https://doi.org/10.1007/s00450-013-0251-7
chicago: Henzinger, Thomas A. “Quantitative Reactive Modeling and Verification.”
Computer Science Research and Development. Springer, 2013. https://doi.org/10.1007/s00450-013-0251-7.
ieee: T. A. Henzinger, “Quantitative reactive modeling and verification,” Computer
Science Research and Development, vol. 28, no. 4. Springer, pp. 331–344, 2013.
ista: Henzinger TA. 2013. Quantitative reactive modeling and verification. Computer
Science Research and Development. 28(4), 331–344.
mla: Henzinger, Thomas A. “Quantitative Reactive Modeling and Verification.” Computer
Science Research and Development, vol. 28, no. 4, Springer, 2013, pp. 331–44,
doi:10.1007/s00450-013-0251-7.
short: T.A. Henzinger, Computer Science Research and Development 28 (2013) 331–344.
corr_author: '1'
date_created: 2018-12-11T11:56:47Z
date_published: 2013-10-05T00:00:00Z
date_updated: 2024-10-09T20:55:17Z
day: '05'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/s00450-013-0251-7
ec_funded: 1
file:
- access_level: open_access
checksum: f117a00f9f046165bfa95595681e08a0
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:17:51Z
date_updated: 2020-07-14T12:45:37Z
file_id: '5308'
file_name: IST-2016-626-v1+1_s00450-013-0251-7.pdf
file_size: 570361
relation: main_file
file_date_updated: 2020-07-14T12:45:37Z
has_accepted_license: '1'
intvolume: ' 28'
issue: '4'
language:
- iso: eng
month: '10'
oa: 1
oa_version: Published Version
page: 331 - 344
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
publication: Computer Science Research and Development
publication_status: published
publisher: Springer
publist_id: '4642'
pubrep_id: '626'
quality_controlled: '1'
scopus_import: 1
status: public
title: Quantitative reactive modeling and verification
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: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 28
year: '2013'
...
---
_id: '2298'
abstract:
- lang: eng
text: "We present a shape analysis for programs that manipulate overlaid data structures
which share sets of objects. The abstract domain contains Separation Logic formulas
that (1) combine a per-object separating conjunction with a per-field separating
conjunction and (2) constrain a set of variables interpreted as sets of objects.
The definition of the abstract domain operators is based on a notion of homomorphism
between formulas, viewed as graphs, used recently to define optimal decision procedures
for fragments of the Separation Logic. Based on a Frame Rule that supports the
two versions of the separating conjunction, the analysis is able to reason in
a modular manner about non-overlaid data structures and then, compose information
only at a few program points, e.g., procedure returns. We have implemented this
analysis in a prototype tool and applied it on several interesting case studies
that manipulate overlaid and nested linked lists.\r\n"
alternative_title:
- LNCS
author:
- first_name: Cezara
full_name: Dragoi, Cezara
id: 2B2B5ED0-F248-11E8-B48F-1D18A9856A87
last_name: Dragoi
- first_name: Constantin
full_name: Enea, Constantin
last_name: Enea
- first_name: Mihaela
full_name: Sighireanu, Mihaela
last_name: Sighireanu
citation:
ama: 'Dragoi C, Enea C, Sighireanu M. Local shape analysis for overlaid data structures.
In: Vol 7935. Springer; 2013:150-171. doi:10.1007/978-3-642-38856-9_10'
apa: 'Dragoi, C., Enea, C., & Sighireanu, M. (2013). Local shape analysis for
overlaid data structures (Vol. 7935, pp. 150–171). Presented at the SAS: Static
Analysis Symposium, Seattle, WA, United States: Springer. https://doi.org/10.1007/978-3-642-38856-9_10'
chicago: Dragoi, Cezara, Constantin Enea, and Mihaela Sighireanu. “Local Shape Analysis
for Overlaid Data Structures,” 7935:150–71. Springer, 2013. https://doi.org/10.1007/978-3-642-38856-9_10.
ieee: 'C. Dragoi, C. Enea, and M. Sighireanu, “Local shape analysis for overlaid
data structures,” presented at the SAS: Static Analysis Symposium, Seattle, WA,
United States, 2013, vol. 7935, pp. 150–171.'
ista: 'Dragoi C, Enea C, Sighireanu M. 2013. Local shape analysis for overlaid data
structures. SAS: Static Analysis Symposium, LNCS, vol. 7935, 150–171.'
mla: Dragoi, Cezara, et al. Local Shape Analysis for Overlaid Data Structures.
Vol. 7935, Springer, 2013, pp. 150–71, doi:10.1007/978-3-642-38856-9_10.
short: C. Dragoi, C. Enea, M. Sighireanu, in:, Springer, 2013, pp. 150–171.
conference:
end_date: 2013-06-22
location: Seattle, WA, United States
name: 'SAS: Static Analysis Symposium'
start_date: 2013-06-20
date_created: 2018-12-11T11:56:50Z
date_published: 2013-01-01T00:00:00Z
date_updated: 2021-01-12T06:56:36Z
day: '01'
ddc:
- '000'
- '004'
department:
- _id: ToHe
doi: 10.1007/978-3-642-38856-9_10
ec_funded: 1
file:
- access_level: open_access
checksum: 907edd33a5892e3af093365f1fd57ed7
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:10:36Z
date_updated: 2020-07-14T12:45:37Z
file_id: '4824'
file_name: IST-2014-196-v1+1_sas13.pdf
file_size: 299004
relation: main_file
file_date_updated: 2020-07-14T12:45:37Z
has_accepted_license: '1'
intvolume: ' 7935'
language:
- iso: eng
month: '01'
oa: 1
oa_version: Submitted Version
page: 150 - 171
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
publication_status: published
publisher: Springer
publist_id: '4630'
pubrep_id: '196'
quality_controlled: '1'
scopus_import: 1
status: public
title: Local shape analysis for overlaid data structures
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 7935
year: '2013'
...
---
_id: '2299'
abstract:
- lang: eng
text: 'The standard hardware design flow involves: (a) design of an integrated circuit
using a hardware description language, (b) extensive functional and formal verification,
and (c) logical synthesis. However, the above-mentioned processes consume significant
effort and time. An alternative approach is to use a formal specification language
as a high-level hardware description language and synthesize hardware from formal
specifications. Our work is a case study of the synthesis of the widely and industrially
used AMBA AHB protocol from formal specifications. Bloem et al. presented the
first formal specifications for the AMBA AHB Arbiter and synthesized the AHB Arbiter
circuit. However, in the first formal specification some important assumptions
were missing. Our contributions are as follows: (a) We present detailed formal
specifications for the AHB Arbiter incorporating the missing details, and obtain
significant improvements in the synthesis results (both with respect to the number
of gates in the synthesized circuit and with respect to the time taken to synthesize
the circuit), and (b) we present formal specifications to generate compact circuits
for the remaining two main components of AMBA AHB, namely, AHB Master and AHB
Slave. Thus with systematic description we are able to automatically and completely
synthesize an important and widely used industrial protocol.'
author:
- first_name: Yashdeep
full_name: Godhal, Yashdeep
id: 5B547124-EB61-11E9-8887-89D9C04DBDF5
last_name: Godhal
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
citation:
ama: 'Godhal Y, Chatterjee K, Henzinger TA. Synthesis of AMBA AHB from formal specification:
A case study. International Journal on Software Tools for Technology Transfer.
2013;15(5-6):585-601. doi:10.1007/s10009-011-0207-9'
apa: 'Godhal, Y., Chatterjee, K., & Henzinger, T. A. (2013). Synthesis of AMBA
AHB from formal specification: A case study. International Journal on Software
Tools for Technology Transfer. Springer. https://doi.org/10.1007/s10009-011-0207-9'
chicago: 'Godhal, Yashdeep, Krishnendu Chatterjee, and Thomas A Henzinger. “Synthesis
of AMBA AHB from Formal Specification: A Case Study.” International Journal
on Software Tools for Technology Transfer. Springer, 2013. https://doi.org/10.1007/s10009-011-0207-9.'
ieee: 'Y. Godhal, K. Chatterjee, and T. A. Henzinger, “Synthesis of AMBA AHB from
formal specification: A case study,” International Journal on Software Tools
for Technology Transfer, vol. 15, no. 5–6. Springer, pp. 585–601, 2013.'
ista: 'Godhal Y, Chatterjee K, Henzinger TA. 2013. Synthesis of AMBA AHB from formal
specification: A case study. International Journal on Software Tools for Technology
Transfer. 15(5–6), 585–601.'
mla: 'Godhal, Yashdeep, et al. “Synthesis of AMBA AHB from Formal Specification:
A Case Study.” International Journal on Software Tools for Technology Transfer,
vol. 15, no. 5–6, Springer, 2013, pp. 585–601, doi:10.1007/s10009-011-0207-9.'
short: Y. Godhal, K. Chatterjee, T.A. Henzinger, International Journal on Software
Tools for Technology Transfer 15 (2013) 585–601.
corr_author: '1'
date_created: 2018-12-11T11:56:51Z
date_published: 2013-10-01T00:00:00Z
date_updated: 2024-10-09T20:55:16Z
day: '01'
ddc:
- '000'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1007/s10009-011-0207-9
file:
- access_level: open_access
checksum: 57b06a732dd8d6349190dba6b5b0d33b
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:11:53Z
date_updated: 2020-07-14T12:45:37Z
file_id: '4910'
file_name: IST-2012-87-v1+1_Synthesis_of_AMBA_AHB_from_formal_specifications-_A_case_study.pdf
file_size: 277372
relation: main_file
file_date_updated: 2020-07-14T12:45:37Z
has_accepted_license: '1'
intvolume: ' 15'
issue: 5-6
language:
- iso: eng
month: '10'
oa: 1
oa_version: Submitted Version
page: 585 - 601
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 2587B514-B435-11E9-9278-68D0E5697425
name: Microsoft Research Faculty Fellowship
publication: International Journal on Software Tools for Technology Transfer
publication_status: published
publisher: Springer
publist_id: '4629'
pubrep_id: '87'
quality_controlled: '1'
scopus_import: 1
status: public
title: 'Synthesis of AMBA AHB from formal specification: A case study'
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 15
year: '2013'
...
---
_id: '2301'
abstract:
- lang: eng
text: We describe the design and implementation of P, a domain-specific language
to write asynchronous event driven code. P allows the programmer to specify the
system as a collection of interacting state machines, which communicate with each
other using events. P unifies modeling and programming into one activity for the
programmer. Not only can a P program be compiled into executable code, but it
can also be tested using model checking techniques. P allows the programmer to
specify the environment, used to "close" the system during testing,
as nondeterministic ghost machines. Ghost machines are erased during compilation
to executable code; a type system ensures that the erasure is semantics preserving.
The P language is designed so that a P program can be checked for responsiveness-the
ability to handle every event in a timely manner. By default, a machine needs
to handle every event that arrives in every state. But handling every event in
every state is impractical. The language provides a notion of deferred events
where the programmer can annotate when she wants to delay processing an event.
The default safety checker looks for presence of unhan-dled events. The language
also provides default liveness checks that an event cannot be potentially deferred
forever. P was used to implement and verify the core of the USB device driver
stack that ships with Microsoft Windows 8. The resulting driver is more reliable
and performs better than its prior incarnation (which did not use P); we have
more confidence in the robustness of its design due to the language abstractions
and verification provided by P.
author:
- first_name: Ankush
full_name: Desai, Ankush
last_name: Desai
- first_name: Vivek
full_name: Gupta, Vivek
last_name: Gupta
- first_name: Ethan
full_name: Jackson, Ethan
last_name: Jackson
- first_name: Shaz
full_name: Qadeer, Shaz
last_name: Qadeer
- first_name: Sriram
full_name: Rajamani, Sriram
last_name: Rajamani
- first_name: Damien
full_name: Zufferey, Damien
id: 4397AC76-F248-11E8-B48F-1D18A9856A87
last_name: Zufferey
orcid: 0000-0002-3197-8736
citation:
ama: 'Desai A, Gupta V, Jackson E, Qadeer S, Rajamani S, Zufferey D. P: Safe asynchronous
event-driven programming. In: Proceedings of the 34th ACM SIGPLAN Conference
on Programming Language Design and Implementation. ACM; 2013:321-331. doi:10.1145/2491956.2462184'
apa: 'Desai, A., Gupta, V., Jackson, E., Qadeer, S., Rajamani, S., & Zufferey,
D. (2013). P: Safe asynchronous event-driven programming. In Proceedings of
the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation
(pp. 321–331). Seattle, WA, United States: ACM. https://doi.org/10.1145/2491956.2462184'
chicago: 'Desai, Ankush, Vivek Gupta, Ethan Jackson, Shaz Qadeer, Sriram Rajamani,
and Damien Zufferey. “P: Safe Asynchronous Event-Driven Programming.” In Proceedings
of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation,
321–31. ACM, 2013. https://doi.org/10.1145/2491956.2462184.'
ieee: 'A. Desai, V. Gupta, E. Jackson, S. Qadeer, S. Rajamani, and D. Zufferey,
“P: Safe asynchronous event-driven programming,” in Proceedings of the 34th
ACM SIGPLAN Conference on Programming Language Design and Implementation,
Seattle, WA, United States, 2013, pp. 321–331.'
ista: 'Desai A, Gupta V, Jackson E, Qadeer S, Rajamani S, Zufferey D. 2013. P: Safe
asynchronous event-driven programming. Proceedings of the 34th ACM SIGPLAN Conference
on Programming Language Design and Implementation. PLDI: Programming Languages
Design and Implementation, 321–331.'
mla: 'Desai, Ankush, et al. “P: Safe Asynchronous Event-Driven Programming.” Proceedings
of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation,
ACM, 2013, pp. 321–31, doi:10.1145/2491956.2462184.'
short: A. Desai, V. Gupta, E. Jackson, S. Qadeer, S. Rajamani, D. Zufferey, in:,
Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design
and Implementation, ACM, 2013, pp. 321–331.
conference:
end_date: 2013-06-19
location: Seattle, WA, United States
name: 'PLDI: Programming Languages Design and Implementation'
start_date: 2013-06-16
date_created: 2018-12-11T11:56:52Z
date_published: 2013-06-01T00:00:00Z
date_updated: 2021-01-12T06:56:38Z
day: '01'
department:
- _id: ToHe
doi: 10.1145/2491956.2462184
ec_funded: 1
language:
- iso: eng
main_file_link:
- url: http://research.microsoft.com/pubs/191069/pldi212_desai.pdf
month: '06'
oa_version: None
page: 321 - 331
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
publication: Proceedings of the 34th ACM SIGPLAN Conference on Programming Language
Design and Implementation
publication_status: published
publisher: ACM
publist_id: '4626'
quality_controlled: '1'
scopus_import: 1
status: public
title: 'P: Safe asynchronous event-driven programming'
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2013'
...
---
_id: '2327'
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, and robustness
problems that measure how much a model can be perturbed without violating the
specification. We show that for automatic distance functions, and ω-regular linear-time
and branching-time specifications, the model-measuring problem can be solved.
We use automata-theoretic model-checking methods for model measuring, replacing
the emptiness question for standard word and tree automata by the optimal-weight
question for the weighted versions of these automata. We consider weighted automata
that accumulate weights by maximizing, summing, discounting, and limit averaging.
We give several examples of using the model-measuring problem to compute various
notions of robustness and quantitative satisfaction for temporal specifications.'
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
citation:
ama: Henzinger TA, Otop J. From model checking to model measuring. 2013;8052:273-287.
doi:10.1007/978-3-642-40184-8_20
apa: 'Henzinger, T. A., & Otop, J. (2013). From model checking to model measuring.
Presented at the CONCUR: Concurrency Theory, Buenos Aires, Argentina: Springer.
https://doi.org/10.1007/978-3-642-40184-8_20'
chicago: Henzinger, Thomas A, and Jan Otop. “From Model Checking to Model Measuring.”
Lecture Notes in Computer Science. Springer, 2013. https://doi.org/10.1007/978-3-642-40184-8_20.
ieee: T. A. Henzinger and J. Otop, “From model checking to model measuring,” vol.
8052. Springer, pp. 273–287, 2013.
ista: Henzinger TA, Otop J. 2013. From model checking to model measuring. 8052,
273–287.
mla: Henzinger, Thomas A., and Jan Otop. From Model Checking to Model Measuring.
Vol. 8052, Springer, 2013, pp. 273–87, doi:10.1007/978-3-642-40184-8_20.
short: T.A. Henzinger, J. Otop, 8052 (2013) 273–287.
conference:
end_date: 2013-08-30
location: Buenos Aires, Argentina
name: 'CONCUR: Concurrency Theory'
start_date: 2013-08-27
corr_author: '1'
date_created: 2018-12-11T11:57:00Z
date_published: 2013-08-01T00:00:00Z
date_updated: 2024-10-21T06:02:58Z
day: '01'
ddc:
- '005'
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-642-40184-8_20
file:
- access_level: open_access
checksum: 4c04695c4bfdf2119cd4f5d1babc3e8a
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:17:45Z
date_updated: 2020-07-14T12:45:38Z
file_id: '5301'
file_name: IST-2013-129-v1+1_concur.pdf
file_size: 378587
relation: main_file
file_date_updated: 2020-07-14T12:45:38Z
has_accepted_license: '1'
intvolume: ' 8052'
language:
- iso: eng
month: '08'
oa: 1
oa_version: Submitted Version
page: 273 - 287
publication_status: published
publisher: Springer
publist_id: '4599'
pubrep_id: '129'
quality_controlled: '1'
related_material:
record:
- id: '5417'
relation: earlier_version
status: public
scopus_import: '1'
series_title: Lecture Notes in Computer Science
status: public
title: From model checking to model measuring
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 8052
year: '2013'
...
---
_id: '2328'
abstract:
- lang: eng
text: "Linearizability of concurrent data structures is usually proved by monolithic
simulation arguments relying on identifying the so-called linearization points.
Regrettably, such proofs, whether manual or automatic, are often complicated and
scale poorly to advanced non-blocking concurrency patterns, such as helping and
optimistic updates.\r\nIn response, we propose a more modular way of checking
linearizability of concurrent queue algorithms that does not involve identifying
linearization points. We reduce the task of proving linearizability with respect
to the queue specification to establishing four basic properties, each of which
can be proved independently by simpler arguments. As a demonstration of our approach,
we verify the Herlihy and Wing queue, an algorithm that is challenging to verify
by a simulation proof."
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: Ali
full_name: Sezgin, Ali
id: 4C7638DA-F248-11E8-B48F-1D18A9856A87
last_name: Sezgin
- first_name: Viktor
full_name: Vafeiadis, Viktor
last_name: Vafeiadis
citation:
ama: Henzinger TA, Sezgin A, Vafeiadis V. Aspect-oriented linearizability proofs.
2013;8052:242-256. doi:10.1007/978-3-642-40184-8_18
apa: 'Henzinger, T. A., Sezgin, A., & Vafeiadis, V. (2013). Aspect-oriented
linearizability proofs. Presented at the CONCUR: Concurrency Theory, Buenos Aires,
Argentina: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.1007/978-3-642-40184-8_18'
chicago: Henzinger, Thomas A, Ali Sezgin, and Viktor Vafeiadis. “Aspect-Oriented
Linearizability Proofs.” Lecture Notes in Computer Science. Schloss Dagstuhl -
Leibniz-Zentrum für Informatik, 2013. https://doi.org/10.1007/978-3-642-40184-8_18.
ieee: T. A. Henzinger, A. Sezgin, and V. Vafeiadis, “Aspect-oriented linearizability
proofs,” vol. 8052. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, pp. 242–256,
2013.
ista: Henzinger TA, Sezgin A, Vafeiadis V. 2013. Aspect-oriented linearizability
proofs. 8052, 242–256.
mla: Henzinger, Thomas A., et al. Aspect-Oriented Linearizability Proofs.
Vol. 8052, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2013, pp. 242–56,
doi:10.1007/978-3-642-40184-8_18.
short: T.A. Henzinger, A. Sezgin, V. Vafeiadis, 8052 (2013) 242–256.
conference:
end_date: 2013-08-30
location: Buenos Aires, Argentina
name: 'CONCUR: Concurrency Theory'
start_date: 2013-08-27
date_created: 2018-12-11T11:57:01Z
date_published: 2013-08-01T00:00:00Z
date_updated: 2025-09-23T07:56:19Z
day: '01'
ddc:
- '000'
- '004'
department:
- _id: ToHe
doi: 10.1007/978-3-642-40184-8_18
ec_funded: 1
file:
- access_level: open_access
checksum: bdbb520de91751fe0136309ad4ef67e4
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:08:58Z
date_updated: 2020-07-14T12:45:39Z
file_id: '4721'
file_name: IST-2014-197-v1+1_main-queue-verification.pdf
file_size: 337059
relation: main_file
file_date_updated: 2020-07-14T12:45:39Z
has_accepted_license: '1'
intvolume: ' 8052'
language:
- iso: eng
month: '08'
oa: 1
oa_version: Submitted Version
page: 242 - 256
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '4598'
pubrep_id: '197'
quality_controlled: '1'
related_material:
record:
- id: '1832'
relation: later_version
status: public
scopus_import: 1
series_title: Lecture Notes in Computer Science
status: public
title: Aspect-oriented linearizability proofs
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 8052
year: '2013'
...
---
_id: '2447'
abstract:
- lang: eng
text: "Separation logic (SL) has gained widespread popularity because of its ability
to succinctly express complex invariants of a program’s heap configurations. Several
specialized provers have been developed for decidable SL fragments. However, these
provers cannot be easily extended or combined with solvers for other theories
that are important in program verification, e.g., linear arithmetic. In this paper,
we present a reduction of decidable SL fragments to a decidable first-order theory
that fits well into the satisfiability modulo theories (SMT) framework. We show
how to use this reduction to automate satisfiability, entailment, frame inference,
and abduction problems for separation logic using SMT solvers. Our approach provides
a simple method of integrating separation logic into existing verification tools
that provide SMT backends, and an elegant way of combining SL fragments with other
decidable first-order theories. We implemented this approach in a verification
tool and applied it to heap-manipulating programs whose verification involves
reasoning in theory combinations.\r\n"
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Ruzica
full_name: Piskac, Ruzica
last_name: Piskac
- first_name: Thomas
full_name: Wies, Thomas
id: 447BFB88-F248-11E8-B48F-1D18A9856A87
last_name: Wies
- first_name: Damien
full_name: Zufferey, Damien
id: 4397AC76-F248-11E8-B48F-1D18A9856A87
last_name: Zufferey
orcid: 0000-0002-3197-8736
citation:
ama: Piskac R, Wies T, Zufferey D. Automating separation logic using SMT. 2013;8044:773-789.
doi:10.1007/978-3-642-39799-8_54
apa: 'Piskac, R., Wies, T., & Zufferey, D. (2013). Automating separation logic
using SMT. Presented at the CAV: Computer Aided Verification, St. Petersburg,
Russia: Springer. https://doi.org/10.1007/978-3-642-39799-8_54'
chicago: Piskac, Ruzica, Thomas Wies, and Damien Zufferey. “Automating Separation
Logic Using SMT.” Lecture Notes in Computer Science. Springer, 2013. https://doi.org/10.1007/978-3-642-39799-8_54.
ieee: R. Piskac, T. Wies, and D. Zufferey, “Automating separation logic using SMT,”
vol. 8044. Springer, pp. 773–789, 2013.
ista: Piskac R, Wies T, Zufferey D. 2013. Automating separation logic using SMT.
8044, 773–789.
mla: Piskac, Ruzica, et al. Automating Separation Logic Using SMT. Vol. 8044,
Springer, 2013, pp. 773–89, doi:10.1007/978-3-642-39799-8_54.
short: R. Piskac, T. Wies, D. Zufferey, 8044 (2013) 773–789.
conference:
end_date: 2013-07-19
location: St. Petersburg, Russia
name: 'CAV: Computer Aided Verification'
start_date: 2013-07-13
date_created: 2018-12-11T11:57:43Z
date_published: 2013-07-01T00:00:00Z
date_updated: 2020-08-11T10:09:47Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-642-39799-8_54
file:
- access_level: open_access
checksum: 2e866932ab688f47ecd504acb4d5c7d4
content_type: application/pdf
creator: dernst
date_created: 2020-05-15T11:13:01Z
date_updated: 2020-07-14T12:45:41Z
file_id: '7859'
file_name: 2013_CAV_Piskac.pdf
file_size: 309182
relation: main_file
file_date_updated: 2020-07-14T12:45:41Z
has_accepted_license: '1'
intvolume: ' 8044'
language:
- iso: eng
month: '07'
oa: 1
oa_version: Submitted Version
page: 773 - 789
publication_status: published
publisher: Springer
publist_id: '4456'
quality_controlled: '1'
scopus_import: 1
series_title: Lecture Notes in Computer Science
status: public
title: Automating separation logic using SMT
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 8044
year: '2013'
...