---
_id: '11362'
abstract:
- lang: eng
  text: "Deep learning has enabled breakthroughs in challenging computing problems
    and has emerged as the standard problem-solving tool for computer vision and natural
    language processing tasks.\r\nOne exception to this trend is safety-critical tasks
    where robustness and resilience requirements contradict the black-box nature of
    neural networks. \r\nTo deploy deep learning methods for these tasks, it is vital
    to provide guarantees on neural network agents' safety and robustness criteria.
    \r\nThis can be achieved by developing formal verification methods to verify the
    safety and robustness properties of neural networks.\r\n\r\nOur goal is to design,
    develop and assess safety verification methods for neural networks to improve
    their reliability and trustworthiness in real-world applications.\r\nThis thesis
    establishes techniques for the verification of compressed and adversarially trained
    models as well as the design of novel neural networks for verifiably safe decision-making.\r\n\r\nFirst,
    we establish the problem of verifying quantized neural networks. Quantization
    is a technique that trades numerical precision for the computational efficiency
    of running a neural network and is widely adopted in industry.\r\nWe show that
    neglecting the reduced precision when verifying a neural network can lead to wrong
    conclusions about the robustness and safety of the network, highlighting that
    novel techniques for quantized network verification are necessary. We introduce
    several bit-exact verification methods explicitly designed for quantized neural
    networks and experimentally confirm on realistic networks that the network's robustness
    and other formal properties are affected by the quantization.\r\n\r\nFurthermore,
    we perform a case study providing evidence that adversarial training, a standard
    technique for making neural networks more robust, has detrimental effects on the
    network's performance. This robustness-accuracy tradeoff has been studied before
    regarding the accuracy obtained on classification datasets where each data point
    is independent of all other data points. On the other hand, we investigate the
    tradeoff empirically in robot learning settings where a both, a high accuracy
    and a high robustness, are desirable.\r\nOur results suggest that the negative
    side-effects of adversarial training outweigh its robustness benefits in practice.\r\n\r\nFinally,
    we consider the problem of verifying safety when running a Bayesian neural network
    policy in a feedback loop with systems over the infinite time horizon. Bayesian
    neural networks are probabilistic models for learning uncertainties in the data
    and are therefore often used on robotic and healthcare applications where data
    is inherently stochastic.\r\nWe introduce a method for recalibrating Bayesian
    neural networks so that they yield probability distributions over safe decisions
    only.\r\nOur method learns a safety certificate that guarantees safety over the
    infinite time horizon to determine which decisions are safe in every possible
    state of the system.\r\nWe demonstrate the effectiveness of our approach on a
    series of reinforcement learning benchmarks."
alternative_title:
- ISTA Thesis
article_processing_charge: No
author:
- first_name: Mathias
  full_name: Lechner, Mathias
  id: 3DC22916-F248-11E8-B48F-1D18A9856A87
  last_name: Lechner
citation:
  ama: Lechner M. Learning verifiable representations. 2022. doi:<a href="https://doi.org/10.15479/at:ista:11362">10.15479/at:ista:11362</a>
  apa: Lechner, M. (2022). <i>Learning verifiable representations</i>. Institute of
    Science and Technology Austria. <a href="https://doi.org/10.15479/at:ista:11362">https://doi.org/10.15479/at:ista:11362</a>
  chicago: Lechner, Mathias. “Learning Verifiable Representations.” Institute of Science
    and Technology Austria, 2022. <a href="https://doi.org/10.15479/at:ista:11362">https://doi.org/10.15479/at:ista:11362</a>.
  ieee: M. Lechner, “Learning verifiable representations,” Institute of Science and
    Technology Austria, 2022.
  ista: Lechner M. 2022. Learning verifiable representations. Institute of Science
    and Technology Austria.
  mla: Lechner, Mathias. <i>Learning Verifiable Representations</i>. Institute of
    Science and Technology Austria, 2022, doi:<a href="https://doi.org/10.15479/at:ista:11362">10.15479/at:ista:11362</a>.
  short: M. Lechner, Learning Verifiable Representations, Institute of Science and
    Technology Austria, 2022.
date_created: 2022-05-12T07:14:01Z
date_published: 2022-05-12T00:00:00Z
date_updated: 2025-07-14T09:10:11Z
day: '12'
ddc:
- '004'
degree_awarded: PhD
department:
- _id: GradSch
- _id: ToHe
doi: 10.15479/at:ista:11362
ec_funded: 1
file:
- access_level: closed
  checksum: 8eefa9c7c10ca7e1a2ccdd731962a645
  content_type: application/zip
  creator: mlechner
  date_created: 2022-05-13T12:33:26Z
  date_updated: 2022-05-13T12:49:00Z
  file_id: '11378'
  file_name: src.zip
  file_size: 13210143
  relation: source_file
- access_level: open_access
  checksum: 1b9e1e5a9a83ed9d89dad2f5133dc026
  content_type: application/pdf
  creator: mlechner
  date_created: 2022-05-16T08:02:28Z
  date_updated: 2022-05-17T15:19:39Z
  file_id: '11382'
  file_name: thesis_main-a2.pdf
  file_size: 2732536
  relation: main_file
file_date_updated: 2022-05-17T15:19:39Z
has_accepted_license: '1'
keyword:
- neural networks
- verification
- machine learning
language:
- iso: eng
month: '05'
oa: 1
oa_version: Published Version
page: '124'
project:
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: Z211
  name: The Wittgenstein Prize
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
  call_identifier: H2020
  grant_number: '101020093'
  name: Vigilant Algorithmic Monitoring of Software
publication_identifier:
  isbn:
  - 978-3-99078-017-6
publication_status: published
publisher: Institute of Science and Technology Austria
related_material:
  record:
  - id: '11366'
    relation: part_of_dissertation
    status: public
  - id: '7808'
    relation: part_of_dissertation
    status: public
  - id: '10666'
    relation: part_of_dissertation
    status: public
  - id: '10665'
    relation: part_of_dissertation
    status: public
  - id: '10667'
    relation: part_of_dissertation
    status: public
status: public
supervisor:
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000-0002-2985-7724
title: Learning verifiable representations
tmp:
  image: /image/cc_by_nd.png
  legal_code_url: https://creativecommons.org/licenses/by-nd/4.0/legalcode
  name: Creative Commons Attribution-NoDerivatives 4.0 International (CC BY-ND 4.0)
  short: CC BY-ND (4.0)
type: dissertation
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
year: '2022'
...
---
_id: '10002'
abstract:
- lang: eng
  text: 'We present a faster symbolic algorithm for the following central problem
    in probabilistic verification: Compute the maximal end-component (MEC) decomposition
    of Markov decision processes (MDPs). This problem generalizes the SCC decomposition
    problem of graphs and closed recurrent sets of Markov chains. The model of symbolic
    algorithms is widely used in formal verification and model-checking, where access
    to the input model is restricted to only symbolic operations (e.g., basic set
    operations and computation of one-step neighborhood). For an input MDP with  n  vertices
    and  m  edges, the classical symbolic algorithm from the 1990s for the MEC decomposition
    requires  O(n2)  symbolic operations and  O(1)  symbolic space. The only other
    symbolic algorithm for the MEC decomposition requires  O(nm−−√)  symbolic operations
    and  O(m−−√)  symbolic space. A main open question is whether the worst-case  O(n2)  bound
    for symbolic operations can be beaten. We present a symbolic algorithm that requires  O˜(n1.5)  symbolic
    operations and  O˜(n−−√)  symbolic space. Moreover, the parametrization of our
    algorithm provides a trade-off between symbolic operations and symbolic space:
    for all  0<ϵ≤1/2  the symbolic algorithm requires  O˜(n2−ϵ)  symbolic operations
    and  O˜(nϵ)  symbolic space ( O˜  hides poly-logarithmic factors). Using our techniques
    we present faster algorithms for computing the almost-sure winning regions of  ω
    -regular objectives for MDPs. We consider the canonical parity objectives for  ω
    -regular objectives, and for parity objectives with  d -priorities we present
    an algorithm that computes the almost-sure winning region with  O˜(n2−ϵ)  symbolic
    operations and  O˜(nϵ)  symbolic space, for all  0<ϵ≤1/2 .'
acknowledgement: The authors are grateful to the anonymous referees for their valuable
  comments. A. S. is fully supported by the Vienna Science and Technology Fund (WWTF)
  through project ICT15–003. K. C. is supported by the Austrian Science Fund (FWF)
  NFN Grant No S11407-N23 (RiSE/SHiNE) and by the ERC CoG 863818 (ForM-SMArt). For
  M. H. the research leading to these results has received funding from the European
  Research Council under the European Unions Seventh Framework Programme (FP/2007–2013)
  / ERC Grant Agreement no. 340506.
article_processing_charge: No
arxiv: 1
author:
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Wolfgang
  full_name: Dvorak, Wolfgang
  last_name: Dvorak
- first_name: Monika H
  full_name: Henzinger, Monika H
  id: 540c9bbd-f2de-11ec-812d-d04a5be85630
  last_name: Henzinger
  orcid: 0000-0002-5008-6530
- first_name: Alexander
  full_name: Svozil, Alexander
  last_name: Svozil
citation:
  ama: 'Chatterjee K, Dvorak W, Henzinger MH, Svozil A. Symbolic time and space tradeoffs
    for probabilistic verification. In: <i>Proceedings of the 36th Annual ACM/IEEE
    Symposium on Logic in Computer Science</i>. Institute of Electrical and Electronics
    Engineers; 2021:1-13. doi:<a href="https://doi.org/10.1109/LICS52264.2021.9470739">10.1109/LICS52264.2021.9470739</a>'
  apa: 'Chatterjee, K., Dvorak, W., Henzinger, M. H., &#38; Svozil, A. (2021). Symbolic
    time and space tradeoffs for probabilistic verification. In <i>Proceedings of
    the 36th Annual ACM/IEEE Symposium on Logic in Computer Science</i> (pp. 1–13).
    Rome, Italy: Institute of Electrical and Electronics Engineers. <a href="https://doi.org/10.1109/LICS52264.2021.9470739">https://doi.org/10.1109/LICS52264.2021.9470739</a>'
  chicago: Chatterjee, Krishnendu, Wolfgang Dvorak, Monika H Henzinger, and Alexander
    Svozil. “Symbolic Time and Space Tradeoffs for Probabilistic Verification.” In
    <i>Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science</i>,
    1–13. Institute of Electrical and Electronics Engineers, 2021. <a href="https://doi.org/10.1109/LICS52264.2021.9470739">https://doi.org/10.1109/LICS52264.2021.9470739</a>.
  ieee: K. Chatterjee, W. Dvorak, M. H. Henzinger, and A. Svozil, “Symbolic time and
    space tradeoffs for probabilistic verification,” in <i>Proceedings of the 36th
    Annual ACM/IEEE Symposium on Logic in Computer Science</i>, Rome, Italy, 2021,
    pp. 1–13.
  ista: 'Chatterjee K, Dvorak W, Henzinger MH, Svozil A. 2021. Symbolic time and space
    tradeoffs for probabilistic verification. Proceedings of the 36th Annual ACM/IEEE
    Symposium on Logic in Computer Science. LICS: Symposium on Logic in Computer Science,
    1–13.'
  mla: Chatterjee, Krishnendu, et al. “Symbolic Time and Space Tradeoffs for Probabilistic
    Verification.” <i>Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in
    Computer Science</i>, Institute of Electrical and Electronics Engineers, 2021,
    pp. 1–13, doi:<a href="https://doi.org/10.1109/LICS52264.2021.9470739">10.1109/LICS52264.2021.9470739</a>.
  short: K. Chatterjee, W. Dvorak, M.H. Henzinger, A. Svozil, in:, Proceedings of
    the 36th Annual ACM/IEEE Symposium on Logic in Computer Science, Institute of
    Electrical and Electronics Engineers, 2021, pp. 1–13.
conference:
  end_date: 2021-07-02
  location: Rome, Italy
  name: 'LICS: Symposium on Logic in Computer Science'
  start_date: 2021-06-29
date_created: 2021-09-12T22:01:24Z
date_published: 2021-07-07T00:00:00Z
date_updated: 2025-07-14T09:10:07Z
day: '07'
department:
- _id: KrCh
doi: 10.1109/LICS52264.2021.9470739
ec_funded: 1
external_id:
  arxiv:
  - '2104.07466'
  isi:
  - '000947350400089'
isi: 1
keyword:
- Computer science
- Computational modeling
- Markov processes
- Probabilistic logic
- Formal verification
- Game Theory
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://arxiv.org/abs/2104.07466
month: '07'
oa: 1
oa_version: Preprint
page: 1-13
project:
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S11407
  name: Game Theory
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
  call_identifier: H2020
  grant_number: '863818'
  name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
publication: Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer
  Science
publication_identifier:
  eisbn:
  - 978-1-6654-4895-6
  isbn:
  - 978-1-6654-4896-3
  issn:
  - 1043-6871
publication_status: published
publisher: Institute of Electrical and Electronics Engineers
quality_controlled: '1'
scopus_import: '1'
status: public
title: Symbolic time and space tradeoffs for probabilistic verification
type: conference
user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
year: '2021'
...
---
_id: '10108'
abstract:
- lang: eng
  text: We argue that the time is ripe to investigate differential monitoring, in
    which the specification of a program's behavior is implicitly given by a second
    program implementing the same informal specification. Similar ideas have been
    proposed before, and are currently implemented in restricted form for testing
    and specialized run-time analyses, aspects of which we combine. We discuss the
    challenges of implementing differential monitoring as a general-purpose, black-box
    run-time monitoring framework, and present promising results of a preliminary
    implementation, showing low monitoring overheads for diverse programs.
acknowledgement: The authors would like to thank Borzoo Bonakdarpour, Derek Dreyer,
  Adrian Francalanza, Owolabi Legunsen, Mae Milano, Manuel Rigger, Cesar Sanchez,
  and the members of the IST Verification Seminar for their helpful comments and insights
  on various stages of this work, as well as the reviewers of RV’21 for their helpful
  suggestions on the actual paper.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Fabian
  full_name: Mühlböck, Fabian
  id: 6395C5F6-89DF-11E9-9C97-6BDFE5697425
  last_name: Mühlböck
  orcid: 0000-0003-1548-0177
- 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: 'Mühlböck F, Henzinger TA. Differential monitoring. In: <i>International Conference
    on Runtime Verification</i>. Vol 12974. Cham: Springer Nature; 2021:231-243. doi:<a
    href="https://doi.org/10.1007/978-3-030-88494-9_12">10.1007/978-3-030-88494-9_12</a>'
  apa: 'Mühlböck, F., &#38; Henzinger, T. A. (2021). Differential monitoring. In <i>International
    Conference on Runtime Verification</i> (Vol. 12974, pp. 231–243). Cham: Springer
    Nature. <a href="https://doi.org/10.1007/978-3-030-88494-9_12">https://doi.org/10.1007/978-3-030-88494-9_12</a>'
  chicago: 'Mühlböck, Fabian, and Thomas A Henzinger. “Differential Monitoring.” In
    <i>International Conference on Runtime Verification</i>, 12974:231–43. Cham: Springer
    Nature, 2021. <a href="https://doi.org/10.1007/978-3-030-88494-9_12">https://doi.org/10.1007/978-3-030-88494-9_12</a>.'
  ieee: F. Mühlböck and T. A. Henzinger, “Differential monitoring,” in <i>International
    Conference on Runtime Verification</i>, Virtual, 2021, vol. 12974, pp. 231–243.
  ista: 'Mühlböck F, Henzinger TA. 2021. Differential monitoring. International Conference
    on Runtime Verification. RV: Runtime Verification, LNCS, vol. 12974, 231–243.'
  mla: Mühlböck, Fabian, and Thomas A. Henzinger. “Differential Monitoring.” <i>International
    Conference on Runtime Verification</i>, vol. 12974, Springer Nature, 2021, pp.
    231–43, doi:<a href="https://doi.org/10.1007/978-3-030-88494-9_12">10.1007/978-3-030-88494-9_12</a>.
  short: F. Mühlböck, T.A. Henzinger, in:, International Conference on Runtime Verification,
    Springer Nature, Cham, 2021, pp. 231–243.
conference:
  end_date: 2021-10-14
  location: Virtual
  name: 'RV: Runtime Verification'
  start_date: 2021-10-11
date_created: 2021-10-07T23:30:10Z
date_published: 2021-10-06T00:00:00Z
date_updated: 2023-08-14T07:20:30Z
day: '06'
ddc:
- '005'
department:
- _id: ToHe
doi: 10.1007/978-3-030-88494-9_12
external_id:
  isi:
  - '000719383800012'
file:
- access_level: open_access
  checksum: 554c7fdb259eda703a8b6328a6dad55a
  content_type: application/pdf
  creator: fmuehlbo
  date_created: 2021-10-07T23:32:18Z
  date_updated: 2021-10-07T23:32:18Z
  file_id: '10109'
  file_name: differentialmonitoring-cameraready-openaccess.pdf
  file_size: 350632
  relation: main_file
  success: 1
file_date_updated: 2021-10-07T23:32:18Z
has_accepted_license: '1'
intvolume: '     12974'
isi: 1
keyword:
- run-time verification
- software engineering
- implicit specification
language:
- iso: eng
month: '10'
oa: 1
oa_version: Preprint
page: 231-243
place: Cham
project:
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: Z211
  name: The Wittgenstein Prize
publication: International Conference on Runtime Verification
publication_identifier:
  eisbn:
  - 978-3-030-88494-9
  eissn:
  - 1611-3349
  isbn:
  - 978-3-030-88493-2
  issn:
  - 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
related_material:
  record:
  - id: '9946'
    relation: extended_version
    status: public
scopus_import: '1'
status: public
title: Differential monitoring
type: conference
user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
volume: 12974
year: '2021'
...
---
_id: '10199'
abstract:
- lang: eng
  text: The design and verification of concurrent systems remains an open challenge
    due to the non-determinism that arises from the inter-process communication. In
    particular, concurrent programs are notoriously difficult both to be written correctly
    and to be analyzed formally, as complex thread interaction has to be accounted
    for. The difficulties are further exacerbated when concurrent programs get executed
    on modern-day hardware, which contains various buffering and caching mechanisms
    for efficiency reasons. This causes further subtle non-determinism, which can
    often produce very unintuitive behavior of the concurrent programs. Model checking
    is at the forefront of tackling the verification problem, where the task is to
    decide, given as input a concurrent system and a desired property, whether the
    system satisfies the property. The inherent state-space explosion problem in model
    checking of concurrent systems causes naïve explicit methods not to scale, thus
    more inventive methods are required. One such method is stateless model checking
    (SMC), which explores in memory-efficient manner the program executions rather
    than the states of the program. State-of-the-art SMC is typically coupled with
    partial order reduction (POR) techniques, which argue that certain executions
    provably produce identical system behavior, thus limiting the amount of executions
    one needs to explore in order to cover all possible behaviors. Another method
    to tackle the state-space explosion is symbolic model checking, where the considered
    techniques operate on a succinct implicit representation of the input system rather
    than explicitly accessing the system. In this thesis we present new techniques
    for verification of concurrent systems. We present several novel POR methods for
    SMC of concurrent programs under various models of semantics, some of which account
    for write-buffering mechanisms. Additionally, we present novel algorithms for
    symbolic model checking of finite-state concurrent systems, where the desired
    property of the systems is to ensure a formally defined notion of fairness.
acknowledged_ssus:
- _id: SSU
alternative_title:
- ISTA Thesis
article_processing_charge: No
author:
- first_name: Viktor
  full_name: Toman, Viktor
  id: 3AF3DA7C-F248-11E8-B48F-1D18A9856A87
  last_name: Toman
  orcid: 0000-0001-9036-063X
citation:
  ama: Toman V. Improved verification techniques for concurrent systems. 2021. doi:<a
    href="https://doi.org/10.15479/at:ista:10199">10.15479/at:ista:10199</a>
  apa: Toman, V. (2021). <i>Improved verification techniques for concurrent systems</i>.
    Institute of Science and Technology Austria. <a href="https://doi.org/10.15479/at:ista:10199">https://doi.org/10.15479/at:ista:10199</a>
  chicago: Toman, Viktor. “Improved Verification Techniques for Concurrent Systems.”
    Institute of Science and Technology Austria, 2021. <a href="https://doi.org/10.15479/at:ista:10199">https://doi.org/10.15479/at:ista:10199</a>.
  ieee: V. Toman, “Improved verification techniques for concurrent systems,” Institute
    of Science and Technology Austria, 2021.
  ista: Toman V. 2021. Improved verification techniques for concurrent systems. Institute
    of Science and Technology Austria.
  mla: Toman, Viktor. <i>Improved Verification Techniques for Concurrent Systems</i>.
    Institute of Science and Technology Austria, 2021, doi:<a href="https://doi.org/10.15479/at:ista:10199">10.15479/at:ista:10199</a>.
  short: V. Toman, Improved Verification Techniques for Concurrent Systems, Institute
    of Science and Technology Austria, 2021.
date_created: 2021-10-29T20:09:01Z
date_published: 2021-10-31T00:00:00Z
date_updated: 2025-07-14T09:10:16Z
day: '31'
ddc:
- '000'
degree_awarded: PhD
department:
- _id: GradSch
- _id: KrCh
doi: 10.15479/at:ista:10199
ec_funded: 1
file:
- access_level: open_access
  checksum: 4f412a1ee60952221b499a4b1268df35
  content_type: application/pdf
  creator: vtoman
  date_created: 2021-11-08T14:12:22Z
  date_updated: 2021-11-08T14:12:22Z
  file_id: '10225'
  file_name: toman_th_final.pdf
  file_size: 2915234
  relation: main_file
- access_level: closed
  checksum: 9584943f99127be2dd2963f6784c37d4
  content_type: application/zip
  creator: vtoman
  date_created: 2021-11-08T14:12:46Z
  date_updated: 2021-11-09T09:00:50Z
  file_id: '10226'
  file_name: toman_thesis.zip
  file_size: 8616056
  relation: source_file
file_date_updated: 2021-11-09T09:00:50Z
has_accepted_license: '1'
keyword:
- concurrency
- verification
- model checking
language:
- iso: eng
month: '10'
oa: 1
oa_version: Published Version
page: '166'
project:
- _id: 2564DBCA-B435-11E9-9278-68D0E5697425
  call_identifier: H2020
  grant_number: '665385'
  name: International IST Doctoral Program
- _id: 25F2ACDE-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S11402-N23
  name: Rigorous Systems Engineering
- _id: 25892FC0-B435-11E9-9278-68D0E5697425
  grant_number: ICT15-003
  name: Efficient Algorithms for Computer Aided Verification
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
  call_identifier: H2020
  grant_number: '863818'
  name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
publication_identifier:
  issn:
  - 2663-337X
publication_status: published
publisher: Institute of Science and Technology Austria
related_material:
  record:
  - id: '10190'
    relation: part_of_dissertation
    status: public
  - id: '9987'
    relation: part_of_dissertation
    status: public
  - id: '141'
    relation: part_of_dissertation
    status: public
  - id: '10191'
    relation: part_of_dissertation
    status: public
status: public
supervisor:
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
title: Improved verification techniques for concurrent systems
type: dissertation
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
year: '2021'
...
---
_id: '9946'
abstract:
- lang: eng
  text: We argue that the time is ripe to investigate differential monitoring, in
    which the specification of a program's behavior is implicitly given by a second
    program implementing the same informal specification. Similar ideas have been
    proposed before, and are currently implemented in restricted form for testing
    and specialized run-time analyses, aspects of which we combine. We discuss the
    challenges of implementing differential monitoring as a general-purpose, black-box
    run-time monitoring framework, and present promising results of a preliminary
    implementation, showing low monitoring overheads for diverse programs.
acknowledgement: The authors would like to thank Borzoo Bonakdarpour, Derek Dreyer,
  Adrian Francalanza, Owolabi Legunsen, Matthew Milano, Manuel Rigger, Cesar Sanchez,
  and the members of the IST Verification Seminar for their helpful comments and insights
  on various stages of this work, as well as the reviewers of RV’21 for their helpful
  suggestions on the actual paper.
alternative_title:
- IST Austria Technical Report
article_processing_charge: No
author:
- first_name: Fabian
  full_name: Mühlböck, Fabian
  id: 6395C5F6-89DF-11E9-9C97-6BDFE5697425
  last_name: Mühlböck
  orcid: 0000-0003-1548-0177
- 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: Mühlböck F, Henzinger TA. <i>Differential Monitoring</i>. IST Austria; 2021.
    doi:<a href="https://doi.org/10.15479/AT:ISTA:9946">10.15479/AT:ISTA:9946</a>
  apa: Mühlböck, F., &#38; Henzinger, T. A. (2021). <i>Differential monitoring</i>.
    IST Austria. <a href="https://doi.org/10.15479/AT:ISTA:9946">https://doi.org/10.15479/AT:ISTA:9946</a>
  chicago: Mühlböck, Fabian, and Thomas A Henzinger. <i>Differential Monitoring</i>.
    IST Austria, 2021. <a href="https://doi.org/10.15479/AT:ISTA:9946">https://doi.org/10.15479/AT:ISTA:9946</a>.
  ieee: F. Mühlböck and T. A. Henzinger, <i>Differential monitoring</i>. IST Austria,
    2021.
  ista: Mühlböck F, Henzinger TA. 2021. Differential monitoring, IST Austria, 17p.
  mla: Mühlböck, Fabian, and Thomas A. Henzinger. <i>Differential Monitoring</i>.
    IST Austria, 2021, doi:<a href="https://doi.org/10.15479/AT:ISTA:9946">10.15479/AT:ISTA:9946</a>.
  short: F. Mühlböck, T.A. Henzinger, Differential Monitoring, IST Austria, 2021.
date_created: 2021-08-20T20:00:37Z
date_published: 2021-09-01T00:00:00Z
date_updated: 2023-08-14T07:20:29Z
day: '01'
ddc:
- '005'
department:
- _id: ToHe
doi: 10.15479/AT:ISTA:9946
file:
- access_level: open_access
  checksum: 0f9aafd59444cb6bdca6925d163ab946
  content_type: application/pdf
  creator: fmuehlbo
  date_created: 2021-08-20T19:59:44Z
  date_updated: 2021-09-03T12:34:28Z
  file_id: '9948'
  file_name: differentialmonitoring-techreport.pdf
  file_size: '320453'
  relation: main_file
file_date_updated: 2021-09-03T12:34:28Z
has_accepted_license: '1'
keyword:
- run-time verification
- software engineering
- implicit specification
language:
- iso: eng
month: '09'
oa: 1
oa_version: Published Version
page: '17'
project:
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: Z211
  name: The Wittgenstein Prize
publication_identifier:
  issn:
  - 2664-1690
publication_status: published
publisher: IST Austria
related_material:
  record:
  - id: '9281'
    relation: other
    status: public
  - id: '10108'
    relation: shorter_version
    status: public
status: public
title: Differential monitoring
type: technical_report
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
year: '2021'
...
---
_id: '5549'
abstract:
- lang: eng
  text: "This repository contains the experimental part of the CAV 2015 publication
    Counterexample Explanation by Learning Small Strategies in Markov Decision Processes.\r\nWe
    extended the probabilistic model checker PRISM to represent strategies of Markov
    Decision Processes as Decision Trees.\r\nThe archive contains a java executable
    version of the extended tool (prism_dectree.jar) together with a few examples
    of the PRISM benchmark library.\r\nTo execute the program, please have a look
    at the README.txt, which provides instructions and further information on the
    archive.\r\nThe archive contains scripts that (if run often enough) reproduces
    the data presented in the publication."
article_processing_charge: No
author:
- first_name: Andreas
  full_name: Fellner, Andreas
  id: 42BABFB4-F248-11E8-B48F-1D18A9856A87
  last_name: Fellner
citation:
  ama: 'Fellner A. Experimental part of CAV 2015 publication: Counterexample Explanation
    by Learning Small Strategies in Markov Decision Processes. 2015. doi:<a href="https://doi.org/10.15479/AT:ISTA:28">10.15479/AT:ISTA:28</a>'
  apa: 'Fellner, A. (2015). Experimental part of CAV 2015 publication: Counterexample
    Explanation by Learning Small Strategies in Markov Decision Processes. Institute
    of Science and Technology Austria. <a href="https://doi.org/10.15479/AT:ISTA:28">https://doi.org/10.15479/AT:ISTA:28</a>'
  chicago: 'Fellner, Andreas. “Experimental Part of CAV 2015 Publication: Counterexample
    Explanation by Learning Small Strategies in Markov Decision Processes.” Institute
    of Science and Technology Austria, 2015. <a href="https://doi.org/10.15479/AT:ISTA:28">https://doi.org/10.15479/AT:ISTA:28</a>.'
  ieee: 'A. Fellner, “Experimental part of CAV 2015 publication: Counterexample Explanation
    by Learning Small Strategies in Markov Decision Processes.” Institute of Science
    and Technology Austria, 2015.'
  ista: 'Fellner A. 2015. Experimental part of CAV 2015 publication: Counterexample
    Explanation by Learning Small Strategies in Markov Decision Processes, Institute
    of Science and Technology Austria, <a href="https://doi.org/10.15479/AT:ISTA:28">10.15479/AT:ISTA:28</a>.'
  mla: 'Fellner, Andreas. <i>Experimental Part of CAV 2015 Publication: Counterexample
    Explanation by Learning Small Strategies in Markov Decision Processes</i>. Institute
    of Science and Technology Austria, 2015, doi:<a href="https://doi.org/10.15479/AT:ISTA:28">10.15479/AT:ISTA:28</a>.'
  short: A. Fellner, (2015).
contributor:
- first_name: Jan
  id: 44CEF464-F248-11E8-B48F-1D18A9856A87
  last_name: Kretinsky
datarep_id: '28'
date_created: 2018-12-12T12:31:29Z
date_published: 2015-08-13T00:00:00Z
date_updated: 2024-02-21T13:52:07Z
day: '13'
ddc:
- '004'
department:
- _id: KrCh
- _id: ToHe
doi: 10.15479/AT:ISTA:28
ec_funded: 1
file:
- access_level: open_access
  checksum: b8bcb43c0893023cda66c1b69c16ac62
  content_type: application/zip
  creator: system
  date_created: 2018-12-12T13:02:31Z
  date_updated: 2020-07-14T12:47:00Z
  file_id: '5597'
  file_name: IST-2015-28-v1+2_Fellner_DataRep.zip
  file_size: 49557109
  relation: main_file
file_date_updated: 2020-07-14T12:47:00Z
has_accepted_license: '1'
keyword:
- Markov Decision Process
- Decision Tree
- Probabilistic Verification
- Counterexample Explanation
month: '08'
oa: 1
oa_version: Published Version
project:
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '279307'
  name: 'Quantitative Graph Games: Theory and Applications'
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S 11407_N23
  name: Rigorous Systems Engineering
publisher: Institute of Science and Technology Austria
publist_id: '5564'
related_material:
  record:
  - id: '1603'
    relation: popular_science
    status: public
status: public
title: 'Experimental part of CAV 2015 publication: Counterexample Explanation by Learning
  Small Strategies in Markov Decision Processes'
tmp:
  image: /images/cc_0.png
  legal_code_url: https://creativecommons.org/publicdomain/zero/1.0/legalcode
  name: Creative Commons Public Domain Dedication (CC0 1.0)
  short: CC0 (1.0)
type: research_data
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2015'
...