---
OA_place: publisher
OA_type: hybrid
_id: '20866'
abstract:
- lang: eng
text: In this work, we present hypernode automata as a specification formalism for
hyperproperties of systems whose executions may be misaligned among themselves,
such as concurrent systems. These automata consist of nodes labeled with hypernode
logic formulas and transitions marked with synchronizing actions. Hypernode logic
formulas establish relations between sequences of variable values among different
system executions. This logic enables both synchronous and asynchronous analysis
of traces. In its asynchronous view on execution traces, hypernode formulas establish
relations on the order of value changes for each variable without correlating
their timing. In both views, the analysis of different execution traces is synchronized
through the transitions of hypernode automata. By combining logic’s declarative
nature with automata’s procedural power, hypernode automata seamlessly integrate
asynchronicity requirements at the node level with synchronicity between node
transitions. We show that the model-checking problem for hypernode automata is
decidable for specifications where each node specifies either a synchronous or
an asynchronous requirement for the system’s executions, but not both.
acknowledgement: This work was supported in part by the Austrian Science Fund (FWF)
SFB project SpyCoDe 10.55776/F85, by the FWF projects ZK-35 and W1255-N23, and by
the ERC Advanced Grant VAMOS 101020093. Open access funding provided by Institute
of Science and Technology (IST Austria).
article_number: '43'
article_processing_charge: Yes (via OA deal)
article_type: original
arxiv: 1
author:
- first_name: Ezio
full_name: Bartocci, Ezio
last_name: Bartocci
- first_name: Marek
full_name: Chalupa, Marek
id: 87e34708-d6c6-11ec-9f5b-9391e7be2463
last_name: Chalupa
- 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: Dejan
full_name: Nickovic, Dejan
id: 41BCEE5C-F248-11E8-B48F-1D18A9856A87
last_name: Nickovic
- first_name: Ana
full_name: Oliveira da Costa, Ana
id: f347ec37-6676-11ee-b395-a888cb7b4fb4
last_name: Oliveira da Costa
orcid: 0000-0002-8741-5799
citation:
ama: Bartocci E, Chalupa M, Henzinger TA, Nickovic D, Oliveira da Costa A. Hypernode
automata. Acta Informatica. 2025;62(4). doi:10.1007/s00236-025-00509-8
apa: Bartocci, E., Chalupa, M., Henzinger, T. A., Nickovic, D., & Oliveira da
Costa, A. (2025). Hypernode automata. Acta Informatica. Springer Nature.
https://doi.org/10.1007/s00236-025-00509-8
chicago: Bartocci, Ezio, Marek Chalupa, Thomas A Henzinger, Dejan Nickovic, and
Ana Oliveira da Costa. “Hypernode Automata.” Acta Informatica. Springer
Nature, 2025. https://doi.org/10.1007/s00236-025-00509-8.
ieee: E. Bartocci, M. Chalupa, T. A. Henzinger, D. Nickovic, and A. Oliveira da
Costa, “Hypernode automata,” Acta Informatica, vol. 62, no. 4. Springer
Nature, 2025.
ista: Bartocci E, Chalupa M, Henzinger TA, Nickovic D, Oliveira da Costa A. 2025.
Hypernode automata. Acta Informatica. 62(4), 43.
mla: Bartocci, Ezio, et al. “Hypernode Automata.” Acta Informatica, vol.
62, no. 4, 43, Springer Nature, 2025, doi:10.1007/s00236-025-00509-8.
short: E. Bartocci, M. Chalupa, T.A. Henzinger, D. Nickovic, A. Oliveira da Costa,
Acta Informatica 62 (2025).
corr_author: '1'
date_created: 2025-12-29T12:07:12Z
date_published: 2025-12-09T00:00:00Z
date_updated: 2026-01-05T12:27:41Z
day: '09'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/s00236-025-00509-8
ec_funded: 1
external_id:
arxiv:
- '2305.02836'
file:
- access_level: open_access
checksum: 06ed45a1218ad8464818803ae2968aaf
content_type: application/pdf
creator: dernst
date_created: 2026-01-05T12:26:43Z
date_updated: 2026-01-05T12:26:43Z
file_id: '20944'
file_name: 2025_ActaInformatica_Bartocci.pdf
file_size: 7117003
relation: main_file
success: 1
file_date_updated: 2026-01-05T12:26:43Z
fulldoi: https://doi.org/10.1007/s00236-025-00509-8
has_accepted_license: '1'
intvolume: ' 62'
issue: '4'
language:
- iso: eng
license: https://creativecommons.org/licenses/by/4.0/
month: '12'
oa: 1
oa_version: Published Version
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
- _id: 34a1b658-11ca-11ed-8bc3-c75229f0241e
grant_number: F8502
name: Interface Theory for Security and Privacy
publication: Acta Informatica
publication_identifier:
eissn:
- 1432-0525
issn:
- 0001-5903
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
related_material:
record:
- id: '14405'
relation: earlier_version
status: public
scopus_import: '1'
status: public
title: Hypernode automata
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: 62
year: '2025'
...
---
OA_place: publisher
OA_type: hybrid
PlanS_conform: '1'
_id: '20186'
abstract:
- lang: eng
text: Enforcement of information-flow policies has been extensively studied by language-based
approaches over the past few decades. In this paper, we propose an alternative,
novel, general, and effective approach using enforcement of hyperproperties– a
powerful formalism for expressing and reasoning about a wide range of information-flow
security policies. We study black- vs. gray- vs. white-box enforcement of hyperproperties
expressed by nondeterministic finite-word hyperautomata (NFH), where the enforcer
has null, some, or complete information about the implementation of the system
under scrutiny. Given an NFH, in order to generate a runtime enforcer, we reduce
the problem to controller synthesis for hyperproperties and subsequently to the
satisfiability problem for quantified Boolean formulas (QBFs). The resulting enforcers
are transferable with low-overhead. We conduct a rich set of case studies, including
information-flow control for JavaScript code, as well as synthesizing obfuscators
for control plants.
acknowledgement: This project was funded in part by the Austrian Science Fund (FWF)
SFB project SpyCoDe F8502, Vienna Science and Technology Fund (WWTF) [10.47379/ICT19018]
(ProbInG) and WWTF project ICT22-023 (TAIGER), National Science Foundation (NSF)
CPS Award 1837680, NSF award ECCS-2144416 and NSF SaTC Award 2245114. Open access
funding provided by Institute of Science and Technology (IST Austria).
article_number: '30'
article_processing_charge: Yes (via OA deal)
article_type: original
author:
- first_name: Tzu Han
full_name: Hsu, Tzu Han
last_name: Hsu
- first_name: Ana A
full_name: Oliveira Da Costa, Ana A
id: 8b282559-50b0-11ef-861e-d6ace0d92e9b
last_name: Oliveira Da Costa
- first_name: Andrew
full_name: Wintenberg, Andrew
last_name: Wintenberg
- first_name: Ezio
full_name: Bartocci, Ezio
last_name: Bartocci
- first_name: Borzoo
full_name: Bonakdarpour, Borzoo
last_name: Bonakdarpour
citation:
ama: Hsu TH, Oliveira da Costa AA, Wintenberg A, Bartocci E, Bonakdarpour B. Gray-box
runtime enforcement of hyperproperties. Acta Informatica. 2025;62(3). doi:10.1007/s00236-025-00502-1
apa: Hsu, T. H., Oliveira da Costa, A. A., Wintenberg, A., Bartocci, E., & Bonakdarpour,
B. (2025). Gray-box runtime enforcement of hyperproperties. Acta Informatica.
Springer Nature. https://doi.org/10.1007/s00236-025-00502-1
chicago: Hsu, Tzu Han, Ana A Oliveira da Costa, Andrew Wintenberg, Ezio Bartocci,
and Borzoo Bonakdarpour. “Gray-Box Runtime Enforcement of Hyperproperties.” Acta
Informatica. Springer Nature, 2025. https://doi.org/10.1007/s00236-025-00502-1.
ieee: T. H. Hsu, A. A. Oliveira da Costa, A. Wintenberg, E. Bartocci, and B. Bonakdarpour,
“Gray-box runtime enforcement of hyperproperties,” Acta Informatica, vol.
62, no. 3. Springer Nature, 2025.
ista: Hsu TH, Oliveira da Costa AA, Wintenberg A, Bartocci E, Bonakdarpour B. 2025.
Gray-box runtime enforcement of hyperproperties. Acta Informatica. 62(3), 30.
mla: Hsu, Tzu Han, et al. “Gray-Box Runtime Enforcement of Hyperproperties.” Acta
Informatica, vol. 62, no. 3, 30, Springer Nature, 2025, doi:10.1007/s00236-025-00502-1.
short: T.H. Hsu, A.A. Oliveira da Costa, A. Wintenberg, E. Bartocci, B. Bonakdarpour,
Acta Informatica 62 (2025).
corr_author: '1'
date_created: 2025-08-17T22:01:36Z
date_published: 2025-09-01T00:00:00Z
date_updated: 2025-09-30T14:20:11Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/s00236-025-00502-1
external_id:
isi:
- '001546115300001'
file:
- access_level: open_access
checksum: 90a43350fd4a8c5cb5b1b0e1aea7970d
content_type: application/pdf
creator: dernst
date_created: 2025-09-02T05:53:47Z
date_updated: 2025-09-02T05:53:47Z
file_id: '20267'
file_name: 2025_ActaInformatica_Hsu.pdf
file_size: 6505049
relation: main_file
success: 1
file_date_updated: 2025-09-02T05:53:47Z
fulldoi: https://doi.org/10.1007/s00236-025-00502-1
has_accepted_license: '1'
intvolume: ' 62'
isi: 1
issue: '3'
language:
- iso: eng
month: '09'
oa: 1
oa_version: Published Version
project:
- _id: 34a1b658-11ca-11ed-8bc3-c75229f0241e
grant_number: F8502
name: Interface Theory for Security and Privacy
publication: Acta Informatica
publication_identifier:
eissn:
- 1432-0525
issn:
- 0001-5903
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Gray-box runtime enforcement of hyperproperties
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: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 62
year: '2025'
...
---
_id: '10602'
abstract:
- lang: eng
text: Transforming ω-automata into parity automata is traditionally done using appearance
records. We present an efficient variant of this idea, tailored to Rabin automata,
and several optimizations applicable to all appearance records. We compare the
methods experimentally and show that our method produces significantly smaller
automata than previous approaches.
acknowledgement: This work is partially funded by the German Research Foundation (DFG)
projects Verified Model Checkers (No. 317422601) and Statistical Unbounded Verification
(No. 383882557), and the Alexander von Humboldt Foundation with funds from the German
Federal Ministry of Education and Research. It is an extended version of [21], including
all proofs together with further explanations and examples. Moreover, we provide
a new, more efficient construction based on (total) preorders, unifying previous
optimizations. Experiments are performed with a new, performant implementation,
comparing our approach to the current state of the art.
article_processing_charge: Yes (via OA deal)
article_type: original
author:
- first_name: Jan
full_name: Kretinsky, Jan
id: 44CEF464-F248-11E8-B48F-1D18A9856A87
last_name: Kretinsky
orcid: 0000-0002-8122-2881
- first_name: Tobias
full_name: Meggendorfer, Tobias
id: b21b0c15-30a2-11eb-80dc-f13ca25802e1
last_name: Meggendorfer
orcid: 0000-0002-1712-2165
- first_name: Clara
full_name: Waldmann, Clara
last_name: Waldmann
- first_name: Maximilian
full_name: Weininger, Maximilian
last_name: Weininger
citation:
ama: Kretinsky J, Meggendorfer T, Waldmann C, Weininger M. Index appearance record
with preorders. Acta Informatica. 2022;59:585-618. doi:10.1007/s00236-021-00412-y
apa: Kretinsky, J., Meggendorfer, T., Waldmann, C., & Weininger, M. (2022).
Index appearance record with preorders. Acta Informatica. Springer Nature.
https://doi.org/10.1007/s00236-021-00412-y
chicago: Kretinsky, Jan, Tobias Meggendorfer, Clara Waldmann, and Maximilian Weininger.
“Index Appearance Record with Preorders.” Acta Informatica. Springer Nature,
2022. https://doi.org/10.1007/s00236-021-00412-y.
ieee: J. Kretinsky, T. Meggendorfer, C. Waldmann, and M. Weininger, “Index appearance
record with preorders,” Acta Informatica, vol. 59. Springer Nature, pp.
585–618, 2022.
ista: Kretinsky J, Meggendorfer T, Waldmann C, Weininger M. 2022. Index appearance
record with preorders. Acta Informatica. 59, 585–618.
mla: Kretinsky, Jan, et al. “Index Appearance Record with Preorders.” Acta Informatica,
vol. 59, Springer Nature, 2022, pp. 585–618, doi:10.1007/s00236-021-00412-y.
short: J. Kretinsky, T. Meggendorfer, C. Waldmann, M. Weininger, Acta Informatica
59 (2022) 585–618.
corr_author: '1'
date_created: 2022-01-06T12:37:27Z
date_published: 2022-10-01T00:00:00Z
date_updated: 2025-04-15T06:53:08Z
day: '01'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1007/s00236-021-00412-y
external_id:
isi:
- '000735765500001'
file:
- access_level: open_access
checksum: bf1c195b6aaf59e8530cf9e3a9d731f7
content_type: application/pdf
creator: cchlebak
date_created: 2022-01-07T07:50:31Z
date_updated: 2022-01-07T07:50:31Z
file_id: '10603'
file_name: 2021_ActaInfor_Křetínský.pdf
file_size: 1066082
relation: main_file
success: 1
file_date_updated: 2022-01-07T07:50:31Z
fulldoi: https://doi.org/10.1007/s00236-021-00412-y
has_accepted_license: '1'
intvolume: ' 59'
isi: 1
keyword:
- computer networks and communications
- information systems
- software
language:
- iso: eng
month: '10'
oa: 1
oa_version: Published Version
page: 585-618
project:
- _id: B67AFEDC-15C9-11EA-A837-991A96BB2854
name: IST Austria Open Access Fund
publication: Acta Informatica
publication_identifier:
eissn:
- 1432-0525
issn:
- 0001-5903
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Index appearance record with preorders
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: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
volume: 59
year: '2022'
...
---
_id: '1351'
abstract:
- lang: eng
text: The behaviour of gene regulatory networks (GRNs) is typically analysed using
simulation-based statistical testing-like methods. In this paper, we demonstrate
that we can replace this approach by a formal verification-like method that gives
higher assurance and scalability. We focus on Wagner’s weighted GRN model with
varying weights, which is used in evolutionary biology. In the model, weight parameters
represent the gene interaction strength that may change due to genetic mutations.
For a property of interest, we synthesise the constraints over the parameter space
that represent the set of GRNs satisfying the property. We experimentally show
that our parameter synthesis procedure computes the mutational robustness of GRNs—an
important problem of interest in evolutionary biology—more efficiently than the
classical simulation method. We specify the property in linear temporal logic.
We employ symbolic bounded model checking and SMT solving to compute the space
of GRNs that satisfy the property, which amounts to synthesizing a set of linear
constraints on the weights.
article_processing_charge: No
author:
- first_name: Mirco
full_name: Giacobbe, Mirco
id: 3444EA5E-F248-11E8-B48F-1D18A9856A87
last_name: Giacobbe
orcid: 0000-0001-8180-0904
- 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: 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
- first_name: Tiago
full_name: Paixao, Tiago
id: 2C5658E6-F248-11E8-B48F-1D18A9856A87
last_name: Paixao
orcid: 0000-0003-2361-3953
- first_name: Tatjana
full_name: Petrov, Tatjana
id: 3D5811FC-F248-11E8-B48F-1D18A9856A87
last_name: Petrov
orcid: 0000-0002-9041-0905
citation:
ama: Giacobbe M, Guet CC, Gupta A, Henzinger TA, Paixao T, Petrov T. Model checking
the evolution of gene regulatory networks. Acta Informatica. 2017;54(8):765-787.
doi:10.1007/s00236-016-0278-x
apa: Giacobbe, M., Guet, C. C., Gupta, A., Henzinger, T. A., Paixao, T., & Petrov,
T. (2017). Model checking the evolution of gene regulatory networks. Acta Informatica.
Springer. https://doi.org/10.1007/s00236-016-0278-x
chicago: Giacobbe, Mirco, Calin C Guet, Ashutosh Gupta, Thomas A Henzinger, Tiago
Paixao, and Tatjana Petrov. “Model Checking the Evolution of Gene Regulatory Networks.”
Acta Informatica. Springer, 2017. https://doi.org/10.1007/s00236-016-0278-x.
ieee: M. Giacobbe, C. C. Guet, A. Gupta, T. A. Henzinger, T. Paixao, and T. Petrov,
“Model checking the evolution of gene regulatory networks,” Acta Informatica,
vol. 54, no. 8. Springer, pp. 765–787, 2017.
ista: Giacobbe M, Guet CC, Gupta A, Henzinger TA, Paixao T, Petrov T. 2017. Model
checking the evolution of gene regulatory networks. Acta Informatica. 54(8), 765–787.
mla: Giacobbe, Mirco, et al. “Model Checking the Evolution of Gene Regulatory Networks.”
Acta Informatica, vol. 54, no. 8, Springer, 2017, pp. 765–87, doi:10.1007/s00236-016-0278-x.
short: M. Giacobbe, C.C. Guet, A. Gupta, T.A. Henzinger, T. Paixao, T. Petrov, Acta
Informatica 54 (2017) 765–787.
corr_author: '1'
date_created: 2018-12-11T11:51:32Z
date_published: 2017-12-01T00:00:00Z
date_updated: 2025-07-10T11:50:42Z
day: '01'
ddc:
- '006'
- '576'
department:
- _id: ToHe
- _id: CaGu
- _id: NiBa
doi: 10.1007/s00236-016-0278-x
ec_funded: 1
external_id:
isi:
- '000414343200003'
file:
- access_level: open_access
checksum: 4e661d9135d7f8c342e8e258dee76f3e
content_type: application/pdf
creator: dernst
date_created: 2019-01-17T15:57:29Z
date_updated: 2020-07-14T12:44:46Z
file_id: '5841'
file_name: 2017_ActaInformatica_Giacobbe.pdf
file_size: 755241
relation: main_file
file_date_updated: 2020-07-14T12:44:46Z
fulldoi: https://doi.org/10.1007/s00236-016-0278-x
has_accepted_license: '1'
intvolume: ' 54'
isi: 1
issue: '8'
language:
- iso: eng
month: '12'
oa: 1
oa_version: Published Version
page: 765 - 787
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: Formal methods for the design and analysis of complex systems
- _id: 25B1EC9E-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '618091'
name: Speed of Adaptation in Population Genetics and Evolutionary Computation
- _id: 25681D80-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '291734'
name: International IST Postdoc Fellowship Programme
- _id: 25B07788-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '250152'
name: Limits to selection in biology and in evolutionary computation
publication: Acta Informatica
publication_identifier:
issn:
- 0001-5903
publication_status: published
publisher: Springer
publist_id: '5898'
pubrep_id: '649'
quality_controlled: '1'
related_material:
record:
- id: '1835'
relation: earlier_version
status: public
scopus_import: '1'
status: public
title: Model checking the evolution of gene regulatory networks
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: 54
year: '2017'
...
---
_id: '719'
abstract:
- lang: eng
text: 'The ubiquity of computation in modern machines and devices imposes a need
to assert the correctness of their behavior. Especially in the case of safety-critical
systems, their designers need to take measures that enforce their safe operation.
Formal methods has emerged as a research field that addresses this challenge:
by rigorously proving that all system executions adhere to their specifications,
the correctness of an implementation under concern can be assured. To achieve
this goal, a plethora of techniques are nowadays available, all of which are optimized
for different system types and application domains.'
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: Rüdiger
full_name: Ehlers, Rüdiger
last_name: Ehlers
citation:
ama: 'Chatterjee K, Ehlers R. Special issue: Synthesis and SYNT 2014. Acta Informatica.
2017;54(6):543-544. doi:10.1007/s00236-017-0299-0'
apa: 'Chatterjee, K., & Ehlers, R. (2017). Special issue: Synthesis and SYNT
2014. Acta Informatica. Springer. https://doi.org/10.1007/s00236-017-0299-0'
chicago: 'Chatterjee, Krishnendu, and Rüdiger Ehlers. “Special Issue: Synthesis
and SYNT 2014.” Acta Informatica. Springer, 2017. https://doi.org/10.1007/s00236-017-0299-0.'
ieee: 'K. Chatterjee and R. Ehlers, “Special issue: Synthesis and SYNT 2014,” Acta
Informatica, vol. 54, no. 6. Springer, pp. 543–544, 2017.'
ista: 'Chatterjee K, Ehlers R. 2017. Special issue: Synthesis and SYNT 2014. Acta
Informatica. 54(6), 543–544.'
mla: 'Chatterjee, Krishnendu, and Rüdiger Ehlers. “Special Issue: Synthesis and
SYNT 2014.” Acta Informatica, vol. 54, no. 6, Springer, 2017, pp. 543–44,
doi:10.1007/s00236-017-0299-0.'
short: K. Chatterjee, R. Ehlers, Acta Informatica 54 (2017) 543–544.
corr_author: '1'
date_created: 2018-12-11T11:48:07Z
date_published: 2017-09-01T00:00:00Z
date_updated: 2025-09-10T10:59:19Z
day: '01'
department:
- _id: KrCh
doi: 10.1007/s00236-017-0299-0
external_id:
isi:
- '000407713300001'
fulldoi: https://doi.org/10.1007/s00236-017-0299-0
intvolume: ' 54'
isi: 1
issue: '6'
language:
- iso: eng
month: '09'
oa_version: None
page: 543 - 544
publication: Acta Informatica
publication_identifier:
issn:
- 0001-5903
publication_status: published
publisher: Springer
publist_id: '6961'
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'Special issue: Synthesis and SYNT 2014'
type: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 54
year: '2017'
...