TU Wien Informatics

Overview
Services
Office of the Dean Infrastructure Communications eduLAB
Institutes
Computer Engineering Information Systems Engineering Logic and Computation Visual Computing and Human-Centered Technology
Research Units
Algorithms and Complexity Artifact-based Computing and User Research Artificial Intelligence Techniques Automation Systems Business Informatics Compilers and Languages Computational Sustainability Computer Graphics Computer Vision Cyber-Physical Systems Data Science Databases and Artificial Intelligence Distributed Systems Embedded Computing Systems Formal Methods in Systems Engineering Human Computer Interaction Knowledge-Based Systems Machine Learning Parallel Computing Privacy Enhancing Technologies Security and Privacy Software Engineering Theory and Logic Virtual and Augmented Reality Visual Analytics

Formal Methods in Systems Engineering E192-04

  • A Research Unit of The Institute of Logic and Computation

We at the Formal Methods in Systems Engineering (FORSYTE) group are concerned with the development of new methods and tools for the design and analysis of computer systems, including software, hardware and distributed systems.

Research Unit Formal Methods in Systems Engineering

Contact

On This Page

About People Activities

About

We at the Formal Methods in Systems Engineering (FORSYTE) group are concerned with the development of new methods and tools for the design and analysis of computer systems, including software, hardware and distributed systems.

Our techniques are based on solid mathematical foundations, with a special focus on program analysis and verification, model checking, synthesis, automated reasoning, symbolic computation and automated testing. Fundamental research topics include software model checking, test case generation, static analysis, protocol verification, and formal methods for distributed and concurrent systems. Industrial research is focusing on low-level software, and embedded systems in the avionics and automotive sector.

The research Unit Formal Methods in Systems Engineering is part of the Institute of Logic and Computation.

Katalin Fazekas
Katalin Fazekas K. Fazekas

Assistant Professor
Asst.Prof. DI.in Dr.in

Laura Kovacs
Laura Kovacs L. Kovacs

Head of Research Unit
Univ.Prof.in Dr.in / MSc

Georg Weissenbacher
Georg Weissenbacher G. Weissenbacher

Full Professor
Univ.Prof. DI / PhD

Florian Zuleger
Florian Zuleger F. Zuleger

Associate Professor
Assoc.Prof. Dipl.-Math. Dr.

Mark Jonathan Chimes
Mark Jonathan Chimes M. Chimes

PreDoc Researcher
BSc MSc

Robin Coutelier
Robin Coutelier R. Coutelier

PreDoc Researcher
MSc

Clemens Eisenhofer
Clemens Eisenhofer C. Eisenhofer

PreDoc Researcher
DI / BSc

Thomas Hader
Thomas Hader T. Hader

PreDoc Researcher
DI / BSc BSc

Marton Hajdu
Marton Hajdu M. Hajdu

PreDoc Researcher
DI / BSc

Matthias Hetzenberger
Matthias Hetzenberger M. Hetzenberger

PreDoc Researcher
DI / BSc

Daniela Kaufmann
Daniela Kaufmann D. Kaufmann

PostDoc Researcher
DI.in Dr.in

Tobias Nießen
Tobias Nießen T. Nießen

PreDoc Researcher / On Leave
MSc

Alexander Pluska
Alexander Pluska A. Pluska

PreDoc Researcher
MSc

Adrian Rebola Pardo
Adrian Rebola Pardo A. Rebola Pardo

PostDoc Researcher
Dr. / MSc

Sarah Sophie Sallinger
Sarah Sophie Sallinger S. Sallinger

PreDoc Researcher
MSc

Johannes Schoisswohl
Johannes Schoisswohl J. Schoisswohl

PreDoc Researcher
DI / BSc

Florian Sextl
Florian Sextl F. Sextl

PreDoc Researcher
MSc

Anton Varonka
Anton Varonka A. Varonka

PreDoc Researcher
MSc

Eva Maria Wagner
Eva Maria Wagner E. Wagner

PreDoc Researcher
DI.in / BSc

Mai Al-Zubi
Mai Al-Zubi M. Al-Zubi

Visiting Scientist
MA

Beatrix Buhl
Beatrix Buhl B. Buhl

Office Services

Andrea Hackl
Andrea Hackl A. Hackl

Project Services
BA MA

Matthias Nitzschke
Matthias Nitzschke M. Nitzschke

IT Services

2024W

2025S

 

2025

  • Automated Reasoning / Kovacs, L. (2025, June). Automated Reasoning [Conference Presentation]. Open Science Day 2025, Wien, Austria. https://doi.org/10.34726/9740
    Download: PDF (1.43 MB)
  • Compositional Shape Analysis with Shared Abduction and Biabductive Loop Acceleration / Sextl, F., Rogalewicz, A., Vojnar, T., & Zuleger, F. (2025). Compositional Shape Analysis with Shared Abduction and Biabductive Loop Acceleration. In V. Vafeiadis (Ed.), Programming Languages and Systems (pp. 230–257). Springer, Cham. https://doi.org/10.1007/978-3-031-91121-7_10
  • Compositional Shape Analysis with Shared Abduction and Biabductive Loop Acceleration (Extended Abstract) / Sextl, F., Rogalewicz, A., Vojnar, T., & Zuleger, F. (2025, January 21). Compositional Shape Analysis with Shared Abduction and Biabductive Loop Acceleration (Extended Abstract) [Conference Presentation]. Theory and Practice of Static Analysis 2025, Denver, Colorado, United States of America (the). http://hdl.handle.net/20.500.12708/212815
  • Polar: An Algebraic Analyzer for (Probabilistic) Loops / Moosbrugger, M., Müllner, J., Bartocci, E., & Kovacs, L. (2025). Polar: An Algebraic Analyzer for (Probabilistic) Loops. In Principles of Verification: Cycling the Probabilistic Landscape (Vol. 15260, pp. 179–200). https://doi.org/10.1007/978-3-031-75783-9_8
    Projects: ARTIST (2021–2026) / ProbInG (2020–2025) / QuAT (2024–2025)
  • Simple Linear Loops: Algebraic Invariants and Applications / Ait El Manssour, R., Kenison, G., Shirmohammadi, M., & Varonka, A. (2025). Simple Linear Loops: Algebraic Invariants and Applications. In M. Hicks (Ed.), Proceedings of the ACM on Programming Languages (pp. 745–771). Association for Computing Machinery. https://doi.org/10.1145/3704862
    Download: PDF (842 KB)
    Projects: ARTIST (2021–2026) / LCS (2017–2025) / ProbInG (2020–2025)

2024

2023

  • CheckMate: Automated Game-Theoretic Security Reasoning / Brugger, L. S., Kovács, L., Petkovic Komel, A., Rain, S., & Rawson, M. (2023). CheckMate: Automated Game-Theoretic Security Reasoning. In CCS ’23: Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security (pp. 1407–1421). Association for Computing Machinery. https://doi.org/10.1145/3576915.3623183
    Download: PDF (1.15 MB)
    Project: SFB SPyCoDe (2023–2026)
  • Automated Sensitivity Analysis for Probabilistic Loops / Moosbrugger, M., Müllner, J., & Kovács, L. (2023). Automated Sensitivity Analysis for Probabilistic Loops. In P. Herber & A. Wijs (Eds.), iFM 2023 : 18th International Conference, iFM 2023, Leiden, The Netherlands, November 13–15, 2023, Proceedings (pp. 21–39). Springer. https://doi.org/10.1007/978-3-031-47705-8_2
  • A Formalization of Heisenbugs and Their Causes / Sallinger, S., Weissenbacher, G., & Zuleger, F. (2023). A Formalization of Heisenbugs and Their Causes. In C. Ferreira & T. A. C. Willemse (Eds.), Software Engineering and Formal Methods : 21st International Conference, SEFM 2023, Eindhoven, The Netherlands, November 6-10, 2023, Proceedings (pp. 282–300). Springer. https://doi.org/10.34726/5381
    Download: Preprint for self-archivation (552 KB)
    Project: ARTIST (2021–2026)
  • Formal Verification of Correctness and Information Flow Security for an In-Order Pipelined Processor / Dong, N., Guanciale, R., Dam, M., & Lööw, A. (2023). Formal Verification of Correctness and Information Flow Security for an In-Order Pipelined Processor. In A. Nadel & K. Y. Rozier (Eds.), Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design – FMCAD 2023 (pp. 247–256). TU Wien Academic Press. https://doi.org/10.34727/2023/isbn.978-3-85448-060-0_33
    Download: PDF (432 KB)
  • Datapath Verification via Word-Level E-Graph Rewriting / Coward, S., Morini, E., Tan, B., Drane, T., & Constantinides, G. (2023). Datapath Verification via Word-Level E-Graph Rewriting. In A. Nadel & K. Y. Rozier (Eds.), Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design – FMCAD 2023 (pp. 92–100). TU Wien Academic Press. https://doi.org/10.34727/2023/isbn.978-3-85448-060-0_17
    Download: PDF (1.25 MB)
  • Lightweight Online Learning for Sets of Related Problems in Automated Reasoning / Wu, H., Hahn, C., Lonsing, F. M., Mann, M., Ramanujan, R., & Barrett, C. (2023). Lightweight Online Learning for Sets of Related Problems in Automated Reasoning. In A. Nadel & K. Y. Rozier (Eds.), Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design – FMCAD 2023 (pp. 23–33). TU Wien Academic Press. https://doi.org/10.34727/2023/isbn.978-3-85448-060-0_10
    Download: PDF (761 KB)
  • Formal Methods for Trusted AI / Könighofer, B. (2023). Formal Methods for Trusted AI. In A. Nadel & K. Y. Rozier (Eds.), Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design – FMCAD 2023 (pp. 3–3). TU Wien Academic Press. https://doi.org/10.34727/2023/isbn.978-3-85448-060-0_3
    Download: PDF (66.1 KB)
  • Modelling and Verification of Security-Oriented Resource Partitioning Schemes / Godbole, A., Ye, L., Manerkar, Y. A., & Seshia, S. (2023). Modelling and Verification of Security-Oriented Resource Partitioning Schemes. In A. Nadel & K. Y. Rozier (Eds.), Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design – FMCAD 2023 (pp. 268–273). TU Wien Academic Press. https://doi.org/10.34727/2023/isbn.978-3-85448-060-0_35
    Download: PDF (415 KB)
  • Fortis: A Tool for Analysis and Repair of Robust Software Systems / Zhang, C., Dardik, I., Meira-Góes, R., Garlan, D., & Kang, E. (2023). Fortis: A Tool for Analysis and Repair of Robust Software Systems. In A. Nadel & K. Y. Rozier (Eds.), Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design – FMCAD 2023 (pp. 228–236). TU Wien Academic Press. https://doi.org/10.34727/2023/isbn.978-3-85448-060-0_31
    Download: PDF (566 KB)
  • MediK: Towards Safe Guideline-based Clinical Decision Support / Saxena, M., Song, S., & Sha, L. (2023). MediK: Towards Safe Guideline-based Clinical Decision Support. In A. Nadel & K. Y. Rozier (Eds.), Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design – FMCAD 2023 (pp. 306–317). TU Wien Academic Press. https://doi.org/10.34727/2023/isbn.978-3-85448-060-0_39
    Download: PDF (587 KB)
  • Formally Explaining Neural Networks within Reactive Systems / Bassan, S., Amir, G., Corsi, D., Refaeli, I., & Katz, G. (2023). Formally Explaining Neural Networks within Reactive Systems. In A. Nadel & K. Y. Rozier (Eds.), Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design – FMCAD 2023 (pp. 10–22). TU Wien Academic Press. https://doi.org/10.34727/2023/isbn.978-3-85448-060-0_9
    Download: PDF (2.39 MB)
  • Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design – FMCAD 2023 / Nadel, A., & Rozier, K. Y. (Eds.). (2023). Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design – FMCAD 2023 (Vol. 4, pp. 1–317). TU Wien Academic Press. https://doi.org/10.34727/2023/isbn.978-3-85448-060-0
    Downloads: PDF (16.9 MB) / PDF (196 KB)
  • Reasoning about quantifiers in SMT: the QSMA algorithm / Bonacina, M. P. (2023). Reasoning about quantifiers in SMT: the QSMA algorithm. In A. Nadel & K. Y. Rozier (Eds.), Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design – FMCAD 2023 (pp. 1–1). TU Wien Academic Press. https://doi.org/10.34727/2023/isbn.978-3-85448-060-0_1
    Download: PDF (81.5 KB)
  • Local Search and Its Application in CDCL/CDCL(T) solvers for SAT/SMT / Cai, S. (2023). Local Search and Its Application in CDCL/CDCL(T) solvers for SAT/SMT. In A. Nadel & K. Y. Rozier (Eds.), Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design – FMCAD 2023 (pp. 6–6). TU Wien Academic Press. https://doi.org/10.34727/2023/isbn.978-3-85448-060-0_6
    Download: PDF (66 KB)
  • NASA’s core Flight System Framework Overview / Tutorial / Swartwout, D. (2023). NASA’s core Flight System Framework Overview / Tutorial. In A. Nadel & K. Y. Rozier (Eds.), Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design – FMCAD 2023 (pp. 7–7). TU Wien Academic Press. https://doi.org/10.34727/2023/isbn.978-3-85448-060-0_7
    Download: PDF (61.6 KB)
  • MiniZinc for Formal Methods / Stuckey, P. J. (2023). MiniZinc for Formal Methods. In A. Nadel & K. Y. Rozier (Eds.), Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design – FMCAD 2023 (pp. 5–5). TU Wien Academic Press. https://doi.org/10.34727/2023/isbn.978-3-85448-060-0_5
    Download: PDF (66.6 KB)
  • Developing an Open-Source, State-of-the-Art Symbolic Model-Checking Framework for the Model-Checking Research Community / Rozier, K. Y., Shankar, N., Tinelli, C., & Vardi, M. (2023). Developing an Open-Source, State-of-the-Art Symbolic Model-Checking Framework for the Model-Checking Research Community. In A. Nadel & K. Y. Rozier (Eds.), Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design – FMCAD 2023 (pp. 4–4). TU Wien Academic Press. https://doi.org/10.34727/2023/isbn.978-3-85448-060-0_4
    Download: PDF (69.8 KB)
  • The FMCAD 2023 Student Forum / Janota, M., & Narodytska, N. (2023). The FMCAD 2023 Student Forum. In A. Nadel & K. Y. Rozier (Eds.), Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design – FMCAD 2023 (pp. 8–9). TU Wien Academic Press. https://doi.org/10.34727/2023/isbn.978-3-85448-060-0_8
    Download: PDF (81.2 KB)
  • Distribution Testing: The New Frontier for Formal Methods / Meel, K. (2023). Distribution Testing: The New Frontier for Formal Methods. In A. Nadel & K. Y. Rozier (Eds.), Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design – FMCAD 2023 (pp. 2–2). TU Wien Academic Press. https://doi.org/10.34727/2023/isbn.978-3-85448-060-0_2
    Download: PDF (65 KB)
  • CRV: An Automated Resiliency Reasoner for System Design Models / Larraz, D., Lorch, R., Yahyazadeh, M., Arif, M. F., Chowdhury, O., & Tinelli, C. (2023). CRV: An Automated Resiliency Reasoner for System Design Models. In A. Nadel & K. Y. Rozier (Eds.), Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design – FMCAD 2023 (pp. 209–220). TU Wien Academic Press. https://doi.org/10.34727/2023/isbn.978-3-85448-060-0_29
    Download: PDF (984 KB)
  • DelBugV: Delta-Debugging Neural Network Verifiers / Elsaleh, R., & Katz, G. (2023). DelBugV: Delta-Debugging Neural Network Verifiers. In A. Nadel & K. Y. Rozier (Eds.), Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design – FMCAD 2023 (pp. 34–43). TU Wien Academic Press. https://doi.org/10.34727/2023/isbn.978-3-85448-060-0_11
    Download: PDF (388 KB)
  • A Procedure for SyGuS Solution Fitting via Matching and Rewrite Rule Discovery / Mohamed, A., Reynolds, A., Barrett, C., & Tinelli, C. (2023). A Procedure for SyGuS Solution Fitting via Matching and Rewrite Rule Discovery. In A. Nadel & K. Y. Rozier (Eds.), Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design – FMCAD 2023 (pp. 189–198). TU Wien Academic Press. https://doi.org/10.34727/2023/isbn.978-3-85448-060-0_27
    Download: PDF (382 KB)
  • Partitioning Strategies for Distributed SMT Solving / Wilson, A., Noetzli, A., Reynolds, A., Cook, B., Tinelli, C., & Barrett, C. (2023). Partitioning Strategies for Distributed SMT Solving. In A. Nadel & K. Y. Rozier (Eds.), Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design – FMCAD 2023 (pp. 199–208). TU Wien Academic Press. https://doi.org/10.34727/2023/isbn.978-3-85448-060-0_28
    Download: PDF (582 KB)
  • Mariposa: Measuring SMT Instability in Automated Program Verification / Zhou, Y., Bosamiya, J., Takashima, Y., Li, J. G., Heule, M., & Parno, B. (2023). Mariposa: Measuring SMT Instability in Automated Program Verification. In A. Nadel & K. Y. Rozier (Eds.), Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design – FMCAD 2023 (pp. 178–188). TU Wien Academic Press. https://doi.org/10.34727/2023/isbn.978-3-85448-060-0_26
    Download: PDF (571 KB)
  • µArchiFI: Formal Modeling and Verification Strategies for Microarchitetural Fault Injections / Tollec, S., Asavoae, M., Couroussé, D., Heydemann, K., & Jan, M. (2023). µArchiFI: Formal Modeling and Verification Strategies for Microarchitetural Fault Injections. In A. Nadel & K. Y. Rozier (Eds.), Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design – FMCAD 2023 (pp. 101–109). TU Wien Academic Press. https://doi.org/10.34727/2023/isbn.978-3-85448-060-0_18
    Download: PDF (492 KB)
  • Btor2MLIR: A Format for Hardware Verification / Tafese, J., Gurfinkel, A., & Garcia-Contreras, I. (2023). Btor2MLIR: A Format for Hardware Verification. In A. Nadel & K. Y. Rozier (Eds.), Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design – FMCAD 2023 (pp. 55–63). TU Wien Academic Press. https://doi.org/10.34727/2023/isbn.978-3-85448-060-0_13
    Download: PDF (324 KB)
  • Automating Cutoff-based Verification of Distributed Protocols / Bhat, S. G., & Nagar, K. (2023). Automating Cutoff-based Verification of Distributed Protocols. In A. Nadel & K. Y. Rozier (Eds.), Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design – FMCAD 2023 (pp. 75–85). TU Wien Academic Press. https://doi.org/10.34727/2023/isbn.978-3-85448-060-0_15
    Download: PDF (462 KB)
  • A provably correct floating-point implementation of Well Clear Avionics Concepts / Bernardes Fernandes Ferreira, N., Moscato, M., Titolo, L., & Ayala-Rincón, M. (2023). A provably correct floating-point implementation of Well Clear Avionics Concepts. In A. Nadel & K. Y. Rozier (Eds.), Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design – FMCAD 2023 (pp. 237–246). TU Wien Academic Press. https://doi.org/10.34727/2023/isbn.978-3-85448-060-0_32
    Download: PDF (427 KB)
  • Modular System Synthesis / Park, K., Johnson, K., D’Antoni, L., & Reps, T. (2023). Modular System Synthesis. In A. Nadel & K. Y. Rozier (Eds.), Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design – FMCAD 2023 (pp. 257–267). TU Wien Academic Press. https://doi.org/10.34727/2023/isbn.978-3-85448-060-0_34
    Download: PDF (437 KB)
  • Conformance Testing for Stochastic Cyber-Physical Systems / Qin, X., Hashemi, N., Lindemann, L., & Deshmukh, J. V. (2023). Conformance Testing for Stochastic Cyber-Physical Systems. In A. Nadel & K. Y. Rozier (Eds.), Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design – FMCAD 2023 (pp. 294–305). TU Wien Academic Press. https://doi.org/10.34727/2023/isbn.978-3-85448-060-0_38
    Download: PDF (691 KB)
  • Local Search For SMT On Linear and Multilinear Real Arithmetic / Li, B., & Cai, S. (2023). Local Search For SMT On Linear and Multilinear Real Arithmetic. In A. Nadel & K. Y. Rozier (Eds.), Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design – FMCAD 2023 (pp. 168–177). TU Wien Academic Press. https://doi.org/10.34727/2023/isbn.978-3-85448-060-0_25
    Download: PDF (1.5 MB)
  • Proofs for Incremental SAT with Inprocessing / Kiesl-Reiter, B., & Whalen, M. W. (2023). Proofs for Incremental SAT with Inprocessing. In A. Nadel & K. Y. Rozier (Eds.), Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design – FMCAD 2023 (pp. 132–140). TU Wien Academic Press. https://doi.org/10.34727/2023/isbn.978-3-85448-060-0_21
    Download: PDF (423 KB)
  • Sylvia: Countering the Path Explosion Problem in the Symbolic Execution of Hardware Designs / Ryan, K., & Sturton, C. (2023). Sylvia: Countering the Path Explosion Problem in the Symbolic Execution of Hardware Designs. In A. Nadel & K. Y. Rozier (Eds.), Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design – FMCAD 2023 (pp. 110–121). TU Wien Academic Press. https://doi.org/10.34727/2023/isbn.978-3-85448-060-0_19
    Download: PDF (309 KB)
  • BIG Backbones / Froleyks, N., Yu, E., & Biere, A. (2023). BIG Backbones. In A. Nadel & K. Y. Rozier (Eds.), Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design – FMCAD 2023 (pp. 162–167). TU Wien Academic Press. https://doi.org/10.34727/2023/isbn.978-3-85448-060-0_24
    Download: PDF (319 KB)
  • Data-Driven Learning of Strong Conjunctive Invariants / Thakkar, A. H., & D’Souza, D. (2023). Data-Driven Learning of Strong Conjunctive Invariants. In A. Nadel & K. Y. Rozier (Eds.), Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design – FMCAD 2023 (pp. 64–74). TU Wien Academic Press. https://doi.org/10.34727/2023/isbn.978-3-85448-060-0_14
    Download: PDF (490 KB)
  • Lift-off: Trustworthy ARMv8 semantics from formal specifications / Lam, K., & Coughlin, N. (2023). Lift-off: Trustworthy ARMv8 semantics from formal specifications. In A. Nadel & K. Y. Rozier (Eds.), Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design – FMCAD 2023 (pp. 274–283). TU Wien Academic Press. https://doi.org/10.34727/2023/isbn.978-3-85448-060-0_36
    Download: PDF (295 KB)
  • Optimal Bounded Partial Order Reduction / Marmanis, I., & Vafeiadis, V. (2023). Optimal Bounded Partial Order Reduction. In A. Nadel & K. Y. Rozier (Eds.), Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design – FMCAD 2023 (pp. 86–91). TU Wien Academic Press. https://doi.org/10.34727/2023/isbn.978-3-85448-060-0_16
    Download: PDF (287 KB)
  • SAT-Based Quantified Symmetric Minimization of the Reachable States of Distributed Protocols / Fazekas, K., Aman, G., & Sakallah, K. (2023). SAT-Based Quantified Symmetric Minimization of the Reachable States of Distributed Protocols. In A. Nadel & K. Y. Rozier (Eds.), Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design – FMCAD 2023 (pp. 152–161). TU Wien Academic Press. https://doi.org/10.34727/2023/isbn.978-3-85448-060-0_23
    Download: PDF (499 KB)
  • Verified Encodings for SAT Solvers / Codel, C., Avigad, J., & Heule, M. (2023). Verified Encodings for SAT Solvers. In A. Nadel & K. Y. Rozier (Eds.), Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design – FMCAD 2023 (pp. 141–151). TU Wien Academic Press. https://doi.org/10.34727/2023/isbn.978-3-85448-060-0_22
    Download: PDF (384 KB)
  • Binary decision diagrams on modern hardware / Pastva, S., & Henzinger, T. A. (2023). Binary decision diagrams on modern hardware. In A. Nadel & K. Y. Rozier (Eds.), Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design – FMCAD 2023 (pp. 122–131). TU Wien Academic Press. https://doi.org/10.34727/2023/isbn.978-3-85448-060-0_20
    Download: PDF (512 KB)
  • Cycle and Commute: Rare-Event Probability Verification for Chemical Reaction Networks / Taylor, L., Israelsen, B., & Zhang, Z. (2023). Cycle and Commute: Rare-Event Probability Verification for Chemical Reaction Networks. In A. Nadel & K. Y. Rozier (Eds.), Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design – FMCAD 2023 (pp. 284–293). TU Wien Academic Press. https://doi.org/10.34727/2023/isbn.978-3-85448-060-0_37
    Download: PDF (624 KB)
  • Towards a Correct-by-Construction Design of Integrated Modular Avionics / Meng, B., Debnath, J., Varanasi, S. C., Manolios, E., Durling, M., Paul, S., Prince, D., Alsabbagh, S., Haadsma, R., McMillan, C., Zhang, C., & Oates, T. (2023). Towards a Correct-by-Construction Design of Integrated Modular Avionics. In A. Nadel & K. Y. Rozier (Eds.), Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design – FMCAD 2023 (pp. 221–227). TU Wien Academic Press. https://doi.org/10.34727/2023/isbn.978-3-85448-060-0_30
    Download: PDF (487 KB)
  • Reshaping Unplugged Computer Science Workshops for Primary School Education / Landman, M., Rain, S., Kovács, L., & Gerald Futschek. (2023). Reshaping Unplugged Computer Science Workshops for Primary School Education. In J.-P. Pellet & G. Parriaux (Eds.), Informatics in Schools. Beyond Bits and Bytes: Nurturing Informatics Intelligence in Education : 16th International Conference on Informatics in Schools: Situation, Evolution, and Perspectives, ISSEP 2023, Lausanne, Switzerland, October 23–25, 2023, Proceedings (pp. 139–151). Springer. https://doi.org/10.1007/978-3-031-44900-0_11
    Download: PDF (1020 KB)
    Projects: AbInfVS (2023–2025) / SFB SPyCoDe (2023–2026)
  • Deductive Controller Synthesis for Probabilistic Hyperproperties / Andriushchenko, R., Bartocci, E., Češka, M., Pontiggia, F., & Sallinger, S. S. (2023). Deductive Controller Synthesis for Probabilistic Hyperproperties. In N. Jansen & M. Tribastone (Eds.), Quantitative Evaluation of Systems - 20th International Conference, QEST 2023 (pp. 47–64). Springer. https://doi.org/10.1007/978-3-031-43835-6_20
    Project: ProbInG (2020–2025)
  • Non-Classical Logics in Satisfiability Modulo Theories / Eisenhofer, C., Alassaf, R., Rawson, M., & Kovács, L. (2023). Non-Classical Logics in Satisfiability Modulo Theories. In D. R. S. Ramanayake & J. Urban (Eds.), Automated Reasoning with Analytic Tableaux and Related Methods: 32nd International Conference, TABLEAUX 2023, Prague, Czech Republic, September 18–21, 2023, Proceedings (pp. 24–36). Springer. https://doi.org/10.1007/978-3-031-43513-3_2
    Download: PDF (423 KB)
    Projects: ARTIST (2021–2026) / SFB SPyCoDe (2023–2026)
  • Lemmas: Generation, Selection, Application / Rawson, M., Wernhard, C., Zombori, Z., & Bibel, W. (2023). Lemmas: Generation, Selection, Application. In D. R. S. Ramanayake & J. Urban (Eds.), Automated Reasoning with Analytic Tableaux and Related Methods: 32nd International Conference, TABLEAUX 2023, Prague, Czech Republic, September 18–21, 2023, Proceedings (pp. 153–174). Springer. https://doi.org/10.1007/978-3-031-43513-3_9
    Project: ARTIST (2021–2026)
  • Superposition with Delayed Unification / Bhayat, A., Schoisswohl, J., & Rawson, M. (2023). Superposition with Delayed Unification. In B. Pientka & C. Tinelli (Eds.), Automated Deduction – CADE 29  29th International Conference on Automated Deduction, Rome, Italy, July 1–4, 2023, Proceedings (pp. 23–40). Springer. https://doi.org/10.1007/978-3-031-38499-8_2
    Projects: ARTIST (2021–2026) / SFB SPyCoDe (2023–2026)
  • Program Synthesis in Saturation / Hozzová, P., Kovács, L., Norman, C., & Voronkov, A. (2023). Program Synthesis in Saturation. In B. Pientka & C. Tinelli (Eds.), Automated Deduction – CADE 29  29th International Conference on Automated Deduction, Rome, Italy, July 1–4, 2023, Proceedings (pp. 307–324). Springer. https://doi.org/10.1007/978-3-031-38499-8_18
    Download: PDF (528 KB)
    Projects: ARTIST (2021–2026) / DK - Logic (2014–2023)
  • SAT-Based Subsumption Resolution / Coutelier, R., Kovács, L., Rawson, M., & Rath, J. (2023). SAT-Based Subsumption Resolution. In B. Pientka & C. Tinelli (Eds.), Automated Deduction – CADE 29  29th International Conference on Automated Deduction, Rome, Italy, July 1–4, 2023, Proceedings (pp. 190–206). Springer. https://doi.org/10.1007/978-3-031-38499-8_11
  • On Incremental Pre-processing for SMT / Bjørner, N., & Fazekas, K. (2023). On Incremental Pre-processing for SMT. In B. Pientka & C. Tinelli (Eds.), Automated Deduction – CADE 29  29th International Conference on Automated Deduction, Rome, Italy, July 1–4, 2023, Proceedings (pp. 41–60). Springer. https://doi.org/10.1007/978-3-031-38499-8_3
    Project: INCR (2021–2024)
  • The Emergence of 2D Building Units in Metal‐Organic Frameworks for Photocatalytic Hydrogen Evolution: A Case Study with COK‐47 / Ayala, P., Naghdi, S., Nandan, S. P., Myakala, S. N., Rath, J., Saito, H., Guggenberger, P., Lakhanlal, L., Kleitz, F., Toroker, M. C., Cherevan, A., & Eder, D. (2023). The Emergence of 2D Building Units in Metal‐Organic Frameworks for Photocatalytic Hydrogen Evolution: A Case Study with COK‐47. Advanced Energy Materials, 13(31), Article 2300961. https://doi.org/10.1002/aenm.202300961
  • IPASIR-UP: User Propagators for CDCL / Fazekas, K., Niemetz, A., Preiner, M., Kirchweger, M., Szeider, S., & Biere, A. (2023). IPASIR-UP: User Propagators for CDCL. In M. Mahajan & F. Slivovsky (Eds.), 26th International Conference on Theory and Applications of Satisfiability Testing (pp. 8:1-8:13). Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.SAT.2023.8
    Download: PDF (797 KB)
    Projects: INCR (2021–2024) / REVEAL-AI (2020–2024) / SLIM (2019–2024)
  • The Membership Problem for Hypergeometric Sequences with Quadratic Parameters / Kenison, G., Nosan, K., Shirmohammadi, M., & Worrell, J. (2023). The Membership Problem for Hypergeometric Sequences with Quadratic Parameters. In A. Dickenstein, E. Tsigaridas, & G. Jeronimo (Eds.), ISSAC ’23: Proceedings of the 2023 International Symposium on Symbolic and Algebraic Computation (pp. 407–416). Association for Computing Machinery. https://doi.org/10.1145/3597066.3597121
    Projects: ARTIST (2021–2026) / ProbInG (2020–2025)
  • Positivity Problems for Reversible Linear Recurrence Sequences / Kenison, G., Nieuwveld, J., Ouaknine, J., & Worrell, J. (2023). Positivity Problems for Reversible Linear Recurrence Sequences. In K. Etessami, U. Feige, & G. Puppis (Eds.), 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023) (pp. 1–17). Schloss Dagstuhl -- Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.ICALP.2023.130
    Projects: ARTIST (2021–2026) / ProbInG (2020–2025)
  • From Polynomial Invariants to Linear Loops / Kenison, G. J., Kovacs, L., & Varonka, A. (2023). From Polynomial Invariants to Linear Loops. In A. Dickenstein, E. Tsigaridas, & G. Jeronimo (Eds.), ISSAC ’23: Proceedings of the 2023 International Symposium on Symbolic and Algebraic Computation (pp. 398–406). Association for Computing Machinery. https://doi.org/10.1145/3597066.3597109
    Projects: ARTIST (2021–2026) / LCS (2017–2025) / ProbInG (2020–2025)
  • Overapproximation of Non-Linear Integer Arithmetic for Smart Contract Verification / Hozzová, P., Bendík, J., Nutz, A., & Rodeh, Y. (2023). Overapproximation of Non-Linear Integer Arithmetic for Smart Contract Verification. In R. Piskac & A. Voronkov (Eds.), Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (pp. 257–269). EasyChair. https://doi.org/10.29007/h4p7
    Download: PDF (464 KB)
    Projects: ARTIST (2021–2026) / DK - Logic (2014–2023)
  • Embedding Intuitionistic into Classical Logic / Pluska, A., & Zuleger, F. (2023). Embedding Intuitionistic into Classical Logic. In R. Piskac & A. Voronkov (Eds.), Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (pp. 329–349). https://doi.org/10.29007/b294
  • Refining Unification with Abstraction / Bhayat, A., Korovin, K., Kovács, L., & Schoisswohl, J. (2023). Refining Unification with Abstraction. In R. Piskac & A. Voronkov (Eds.), Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (pp. 36–47). EasyChair EPiC. https://doi.org/10.29007/h65j
    Download: PDF (394 KB)
    Projects: ARTIST (2021–2026) / SFB SPyCoDe (2023–2026)
  • SMT Solving over Finite Field Arithmetic / Hader, T., Kaufmann, D., & Kovacs, L. (2023). SMT Solving over Finite Field Arithmetic. In R. Piscac & A. Voronkov (Eds.), Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (pp. 238–256). https://doi.org/10.29007/4n6w
    Project: ARTIST (2021–2026)
  • Improving AMulet2 for verifying multiplier circuits using SAT solving and computer algebra / Kaufmann, D., & Biere, A. (2023). Improving AMulet2 for verifying multiplier circuits using SAT solving and computer algebra. International Journal on Software Tools for Technology Transfer, 25(2), 133–144. https://doi.org/10.1007/s10009-022-00688-6
    Download: PDF (1.23 MB)
  • Symbolic Computation in Automated Program Reasoning / Kovács, L. (2023). Symbolic Computation in Automated Program Reasoning. In M. Chechik, J.-P. Katoen, & M. Leucker (Eds.), Formal Methods : 25th International Symposium, FM 2023, Lübeck, Germany, March 6–10, 2023, Proceedings (pp. 3–9). Springer. https://doi.org/10.1007/978-3-031-27481-7_1
    Projects: ARTIST (2021–2026) / ProbInG (2020–2025)
  • What Else is Undecidable About Loops? / Kovács, L., & Varonka, A. (2023). What Else is Undecidable About Loops? In R. Glück, L. Santocanale, & M. Winter (Eds.), Relational and Algebraic Methods in Computer Science. RAMiCS 2023 (pp. 176–193). Springer. https://doi.org/10.1007/978-3-031-28083-2_11
    Projects: ARTIST (2021–2026) / ProbInG (2020–2025)
  • ALASCA: Reasoning in Quantified Linear Arithmetic / Korovin, K., Kovács, L., Reger, G., Schoisswohl, J., & Voronkov, A. (2023). ALASCA: Reasoning in Quantified Linear Arithmetic. In S. Sankaranarayanan & N. Sharygina (Eds.), Tools and Algorithms for the Construction and Analysis of Systems (pp. 647–665). Springer. https://doi.org/10.1007/978-3-031-30823-9_33
    Download: PDF (479 KB)
    Projects: ARTIST (2021–2026) / SFB SPyCoDe (2023–2026)
  • A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions / Matheja, C., Pagel, J., & Zuleger, F. (2023). A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions. ACM Transactions on Computational Logic, 24(1), 1–76. https://doi.org/10.1145/3534927
  • Stochastic Best-Effort Strategies for Borel Goals / Aminof, B., De Giacomo, G., Rubin, S., & Zuleger, F. (2023). Stochastic Best-Effort Strategies for Borel Goals. In 2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). 2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Boston, MA, United States of America (the). IEEE. https://doi.org/10.34726/6219
    Download: Personal use of this material is permitted. Permission from IEEE must be obtained for all other uses, in any current or future media, including reprinting/republishing this material for advertising or promotional purposes, creating new collective works, for resale or redistribution to servers or lists, or reuse of any copyrighted component of this work in other works. (456 KB)
    Project: REMASTER (2019–2022)
  • Algebraic Reasoning for (Un)Solvable Loops (Invited Talk) / Kovacs, L. (2023). Algebraic Reasoning for (Un)Solvable Loops (Invited Talk). In J. Leroux, S. Lombardy, & D. Peleg (Eds.), 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023) (pp. 4:1-4:2). Schloss-Dagstuhl - Leibniz Zentrum für Informatik. https://doi.org/10.4230/LIPICS.MFCS.2023.4
    Projects: ARTIST (2021–2026) / ProbInG (2020–2025)
  • Algebra-Based Loop Analysis / Kovács, L. (2023). Algebra-Based Loop Analysis. In A. Dickenstein, E. Tsigaridas, & G. Jeronimo (Eds.), ISSAC ’23: Proceedings of the 2023 International Symposium on Symbolic and Algebraic Computation (pp. 41–42). Association for Computing Machinery. https://doi.org/10.1145/3597066.3597150
    Projects: ARTIST (2021–2026) / ProbInG (2020–2025)
  • Even Shorter Proofs Without New Variables / Rebola Pardo, A. (2023). Even Shorter Proofs Without New Variables. In M. Mahajan & F. Slivovsky (Eds.), 26th International Conference on Theory and Applications of Satisfiability Testing (pp. 22:1-22:20). Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPICS.SAT.2023.22
    Project: LCS (2017–2025)
  • Satisfiability Modulo Custom Theories in Z3 / Bjørner, N., Eisenhofer, C., & Kovács, L. (2023). Satisfiability Modulo Custom Theories in Z3. In C. Dragoi, M. Emmi, & J. Wang (Eds.), Verification, Model Checking, and Abstract Interpretation. VMCAI 2023 (pp. 91–105). Springer. https://doi.org/10.1007/978-3-031-24950-1_5
    Project: ARTIST (2021–2026)
  • Expressiveness Results for an Inductive Logic of Separated Relations / Iosif, R., & Zuleger, F. (2023). Expressiveness Results for an Inductive Logic of Separated Relations. In 34th International Conference on Concurrency Theory (CONCUR 2023). 34th International Conference on Concurrency Theory, CONCUR 2023, Antwerp, Belgium. Schloss-Dagstuhl - Leibniz Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2023.20
    Download: PDF (918 KB)
  • Towards a Game-Theoretic Security Analysis of Off-Chain Protocols / Rain, S., Avarikioti, G., Kovacs, L., & Maffei, M. (2023). Towards a Game-Theoretic Security Analysis of Off-Chain Protocols. In 2023 IEEE 36th Computer Security Foundations Symposium (CSF) (pp. 107–122). IEEE. https://doi.org/10.1109/CSF57540.2023.00003
    Projects: Browsec (2018–2024) / CDL-BOT (2020–2027) / LCS (2017–2025) / PROFET (2019–2023) / ViSP (2019–2023)

2022

  • Getting Saturated with Induction / Hajdu, M., Hozzová, P., Kovács, L., Reger, G., & Voronkov, A. (2022). Getting Saturated with Induction. In J.-F. Raskin, K. Chatterjee, L. Doyen, & R. Majumdar (Eds.), Principles of Systems Design (Vol. 13660, pp. 306–322). Springer Cham. https://doi.org/10.1007/978-3-031-22337-2_15
    Download: PDF (446 KB)
    Projects: ARTIST (2021–2026) / DK - Logic (2014–2023)
  • First-Order Theorem Proving and Vampire / Kovacs, L. (2022, December 6). First-Order Theorem Proving and Vampire [Keynote Presentation]. 7th School of Theoretical Computer Science and Formal Methods (ETMF), online, Brazil.
    Project: ARTIST (2021–2026)
  • Linear Refutation and Clause Splitting / Rawson, M. (2022). Linear Refutation and Clause Splitting. EasyChair Preprints.
  • This Is the Moment for Probabilistic Loops / Moosbrugger, M., Stankovic, M., Bartocci, E., & Kovacs, L. (2022). This Is the Moment for Probabilistic Loops. Proceedings of the ACM on Programming Languages, 6(OOPSLA2), 1497–1525. https://doi.org/10.1145/3563341
  • Symbolic Computation for Software Analysis / Kovacs, L. (2022, October 25). Symbolic Computation for Software Analysis [Conference Presentation]. Symposium on the Occasion of the 80th Birthday of RISC-founder Bruno Buchberger, Linz, Austria.
    Project: ARTIST (2021–2026)
  • On the Undecidability of Loop Analysis / Varonka, A., & Kovacs, L. (2022, October 12). On the Undecidability of Loop Analysis [Conference Presentation]. Reachability Problems, Kaiserslautern, Germany. https://doi.org/10.1007/978-3-031-19135-0
  • First-Order Theorem Proving - Theory and Practice / Kovacs, L. (2022, October 10). First-Order Theorem Proving - Theory and Practice [Conference Presentation]. Dagstuhl Seminar 22411 on Theory and Practice of SAT and Combinatorial Solving, Dagstuhl, Germany. http://hdl.handle.net/20.500.12708/153840
    Project: ARTIST (2021–2026)
  • Reconciling Verified-Circuit Development and Verilog Development / Lööw, A. (2022). Reconciling Verified-Circuit Development and Verilog Development. In A. Griggio & N. Rungta (Eds.), Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design – FMCAD 2022 (pp. 89–98). TU Wien Academic Press. https://doi.org/10.34727/2022/isbn.978-3-85448-053-2_15
    Download: PDF (367 KB)
  • Why Do Things Go Wrong (or Right)_Applications of Causal Reasoning to Verification / Chockler, H. (2022). Why Do Things Go Wrong (or Right)_Applications of Causal Reasoning to Verification. In A. Griggio & N. Rungta (Eds.), Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design – FMCAD 2022 (pp. 2–2). TU Wien Academic Press. https://doi.org/10.34727/2022/isbn.978-3-85448-053-2_2
    Download: PDF (66 KB)
  • Stratified Certification for k-Induction / Yu, E., Froleyks, N., Biere, A., & Heljanko, K. (2022). Stratified Certification for k-Induction. In A. Griggio & N. Rungta (Eds.), Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design – FMCAD 2022 (pp. 59–64). TU Wien Academic Press. https://doi.org/10.34727/2022/isbn.978-3-85448-053-2_11
    Download: PDF (515 KB)
  • Divider Verification Using Symbolic Computer Algebra and Delayed Don’t Care Optimization / Konrad, A., Scholl, C., Mahzoon, A., Große, D., & Drechsler, R. (2022). Divider Verification Using Symbolic Computer Algebra and Delayed Don’t Care Optimization. In A. Griggio & N. Rungta (Eds.), Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design – FMCAD 2022 (pp. 108–117). TU Wien Academic Press. https://doi.org/10.34727/2022/isbn.978-3-85448-053-2_17
    Download: PDF (555 KB)
  • Reactive Synthesis Modulo Theories using Abstraction Refinement / Maderbacher, B., & Bloem, R. (2022). Reactive Synthesis Modulo Theories using Abstraction Refinement. In A. Griggio & N. Rungta (Eds.), Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design – FMCAD 2022 (pp. 315–324). TU Wien Academic Press. https://doi.org/10.34727/2022/isbn.978-3-85448-053-2_38
    Download: PDF (638 KB)
  • Formally Verified Quite OK Image Format / Bucev, M., & Kunčak, V. (2022). Formally Verified Quite OK Image Format. In A. Griggio & N. Rungta (Eds.), Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design – FMCAD 2022 (pp. 343–348). TU Wien Academic Press. https://doi.org/10.34727/2022/isbn.978-3-85448-053-2_41
    Download: PDF (301 KB)
  • The RAPID Software Verification Framework / Georgiou, P., Gleiss, B., Bhayat, A., Rawson, M., Kovács, L., & Reger, G. (2022). The RAPID Software Verification Framework. In A. Griggio & N. Rungta (Eds.), Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design – FMCAD 2022 (pp. 255–260). TU Wien Academic Press. https://doi.org/10.34727/2022/isbn.978-3-85448-053-2_32
    Download: PDF (308 KB)
  • Automating Geometric Proofs of Collision Avoidance with Active Corners / Kheterpal, N., Tang, E., & Jeannin, J.-B. (2022). Automating Geometric Proofs of Collision Avoidance with Active Corners. In A. Griggio & N. Rungta (Eds.), Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design – FMCAD 2022 (pp. 359–368). TU Wien Academic Press. https://doi.org/10.34727/2022/isbn.978-3-85448-053-2_43
    Download: PDF (789 KB)
  • On Optimizing Back-Substitution Methods for Neural Network Verification / Zelazny, T., Wu, H., Barrett, C., & Katz, G. (2022). On Optimizing Back-Substitution Methods for Neural Network Verification. In A. Griggio & N. Rungta (Eds.), Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design – FMCAD 2022 (pp. 17–26). TU Wien Academic Press. https://doi.org/10.34727/2022/isbn.978-3-85448-053-2_7
    Download: PDF (356 KB)
  • Neural Network Verification with Proof Production / Isac, O., Barrett, C., Zhang, M., & Katz, G. (2022). Neural Network Verification with Proof Production. In A. Griggio & N. Rungta (Eds.), Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design – FMCAD 2022 (pp. 38–48). TU Wien Academic Press. https://doi.org/10.34727/2022/isbn.978-3-85448-053-2_9
    Download: PDF (598 KB)
  • Verification-Aided Deep Ensemble Selection / Amir, G., Zelazny, T., Katz, G., & Schapira, M. (2022). Verification-Aided Deep Ensemble Selection. In A. Griggio & N. Rungta (Eds.), Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design – FMCAD 2022 (pp. 27–37). TU Wien Academic Press. https://doi.org/10.34727/2022/isbn.978-3-85448-053-2_8
    Download: PDF (402 KB)
  • Synthesizing Instruction Selection Rewrite Rules from RTL using SMT / Daly, R., Donovick, C., Melchert, J., Setaluri, R., Tsiskaridze, N., Raina, P., Barrett, C., & Hanrahan, P. (2022). Synthesizing Instruction Selection Rewrite Rules from RTL using SMT. In A. Griggio & N. Rungta (Eds.), Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design – FMCAD 2022 (pp. 139–150). TU Wien Academic Press. https://doi.org/10.34727/2022/isbn.978-3-85448-053-2_20
    Download: PDF (526 KB)
  • The FMCAD 2022 Student Forum / Preiner, M. (2022). The FMCAD 2022 Student Forum. In A. Griggio & N. Rungta (Eds.), Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design – FMCAD 2022 (pp. 5–6). TU Wien Academic Press. https://doi.org/10.34727/2022/isbn.978-3-85448-053-2_5
    Download: PDF (101 KB)
  • Reconstructing Fine-Grained Proofs of Rewrites Using a Domain-Specific Language / Noetzli, A., Barbosa, H., Niemetz, A., Preiner, M., Reynolds, A., Barrett, C., & Tinelli, C. (2022). Reconstructing Fine-Grained Proofs of Rewrites Using a Domain-Specific Language. In A. Griggio & N. Rungta (Eds.), Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design – FMCAD 2022 (pp. 65–74). TU Wien Academic Press. https://doi.org/10.34727/2022/isbn.978-3-85448-053-2_12
    Download: PDF (663 KB)
  • Proof-Stitch_Proof Combination for Divide-and-Conquer SAT Solvers / Nair, A., Chattopadhyay, S., Wu, H., Ozdemir, A., & Barrett, C. (2022). Proof-Stitch_Proof Combination for Divide-and-Conquer SAT Solvers. In A. Griggio & N. Rungta (Eds.), Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design – FMCAD 2022 (pp. 84–88). TU Wien Academic Press. https://doi.org/10.34727/2022/isbn.978-3-85448-053-2_14
    Download: PDF (405 KB)
  • Enumerative Data Types with Constraints / Walter, A. T., Greve, D., & Manolios, P. (2022). Enumerative Data Types with Constraints. In A. Griggio & N. Rungta (Eds.), Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design – FMCAD 2022 (pp. 189–198). TU Wien Academic Press. https://doi.org/10.34727/2022/isbn.978-3-85448-053-2_25
    Download: PDF (655 KB)
  • Plain and Simple Inductive Invariant Inference for Distributed Protocols in TLA+ / Schultz, W., Dardik, I., & Tripakis, S. (2022). Plain and Simple Inductive Invariant Inference for Distributed Protocols in TLA+. In A. Griggio & N. Rungta (Eds.), Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design – FMCAD 2022 (pp. 273–283). TU Wien Academic Press. https://doi.org/10.34727/2022/isbn.978-3-85448-053-2_34
    Download: PDF (451 KB)
  • Automated Conversion of Axiomatic to Operational Models: Theory and Practice / Godbole, A., Manerkar, Y. A., & Seshia, S. A. (2022). Automated Conversion of Axiomatic to Operational Models: Theory and Practice. In A. Griggio & N. Rungta (Eds.), Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design – FMCAD 2022 (pp. 331–342). TU Wien Academic Press. https://doi.org/10.34727/2022/isbn.978-3-85448-053-2_40
    Download: PDF (1.01 MB)
  • Learning Deterministic Finite Automata Decompositions from Examples and Demonstrations / Lauffer, N., Yalcinkaya, B., Vazquez-Chanlatte, M., Shah, A., & Seshia, S. A. (2022). Learning Deterministic Finite Automata Decompositions from Examples and Demonstrations. In A. Griggio & N. Rungta (Eds.), Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design – FMCAD 2022 (pp. 325–330). TU Wien Academic Press. https://doi.org/10.34727/2022/isbn.978-3-85448-053-2_39
    Download: PDF (429 KB)
  • Compact Symmetry Breaking for Tournaments / Lohn, E., Lambert, C., & Heule, M. (2022). Compact Symmetry Breaking for Tournaments. In A. Griggio & N. Rungta (Eds.), Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design – FMCAD 2022 (pp. 179–188). TU Wien Academic Press. https://doi.org/10.34727/2022/isbn.978-3-85448-053-2_24
    Download: PDF (406 KB)
  • TBUDDY: A Proof-Generating BDD Package / Bryant, R. (2022). TBUDDY: A Proof-Generating BDD Package. In A. Griggio & N. Rungta (Eds.), Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design – FMCAD 2022 (pp. 49–58). TU Wien Academic Press. https://doi.org/10.34727/2022/isbn.978-3-85448-053-2_10
    Download: PDF (378 KB)
  • Differential Testing of Pushdown Reachability with a Formally Verified Oracle / Schlichtkrull, A., Schou, M. K., Srba, J., & Traytel, D. (2022). Differential Testing of Pushdown Reachability with a Formally Verified Oracle. In A. Griggio & N. Rungta (Eds.), Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design – FMCAD 2022 (pp. 369–379). TU Wien Academic Press. https://doi.org/10.34727/2022/isbn.978-3-85448-053-2_44
    Download: PDF (411 KB)
  • Automatic Repair and Deadlock Detection for Parameterized Systems / Jacobs, S., Sakr, M., & Völp, M. (2022). Automatic Repair and Deadlock Detection for Parameterized Systems. In A. Griggio & N. Rungta (Eds.), Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design – FMCAD 2022 (pp. 225–234). TU Wien Academic Press. https://doi.org/10.34727/2022/isbn.978-3-85448-053-2_29
    Download: PDF (374 KB)
  • TRICERA Verifying C Programs Using the Theory of Heaps / Esen, Z., & Ruemmer, P. (2022). TRICERA Verifying C Programs Using the Theory of Heaps. In A. Griggio & N. Rungta (Eds.), Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design – FMCAD 2022 (pp. 360–391). TU Wien Academic Press. https://doi.org/10.34727/2022/isbn.978-3-85448-053-2_45
    Download: PDF (458 KB)
  • Awaiting for Godot Stateless Model Checking that Avoids Executions where Nothing Happens / Jonsson, B., Lång, M., & Sagonas, K. (2022). Awaiting for Godot Stateless Model Checking that Avoids Executions where Nothing Happens. In Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design – FMCAD 2022 (pp. 284–293). TU Wien Academic Press. https://doi.org/10.34727/2022/isbn.978-3-85448-053-2_35
    Download: PDF (336 KB)
  • BAXMC: a CEGAR approach to Max#SAT / Vigouroux, T., Ene, C., Monniaux, D., Mounier, L., & Potet, M.-L. (2022). BAXMC: a CEGAR approach to Max#SAT. In A. Griggio & N. Rungta (Eds.), Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design – FMCAD 2022 (pp. 170–178). TU Wien Academic Press. https://doi.org/10.34727/2022/isbn.978-3-85448-053-2_23
    Download: PDF (368 KB)
  • Bounded Model Checking for LLVM / Priya, S., Su, Y., Bao, Y., Zhou, X., Vizel, Y., & Gurfinkel, A. (2022). Bounded Model Checking for LLVM. In A. Griggio & N. Rungta (Eds.), Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design – FMCAD 2022 (pp. 214–224). TU Wien Academic Press. https://doi.org/10.34727/2022/isbn.978-3-85448-053-2_28
    Download: PDF (478 KB)
  • Synthesizing Locally Symmetric Parameterized Protocols from Temporal Specifications / Zhang, R., Trefler, R., & Namjoshi, K. (2022). Synthesizing Locally Symmetric Parameterized Protocols from Temporal Specifications. In A. Griggio & N. Rungta (Eds.), Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design – FMCAD 2022 (pp. 235–244). TU Wien Academic Press. https://doi.org/10.34727/2022/isbn.978-3-85448-053-2_30
    Download: PDF (1.16 MB)
  • INC A Scalable Incremental Weighted Sampler / Yang, S., Liang, V., & Meel, K. S. (2022). INC A Scalable Incremental Weighted Sampler. In A. Griggio & N. Rungta (Eds.), Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design – FMCAD 2022 (pp. 205–213). TU Wien Academic Press. https://doi.org/10.34727/2022/isbn.978-3-85448-053-2_27
    Download: PDF (327 KB)
  • Reducing NEXP-complete problems to DQBF / Chen, F.-H., Huang, S.-C., Lu, Y.-C., & Tan, T. (2022). Reducing NEXP-complete problems to DQBF. In A. Griggio & N. Rungta (Eds.), Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design – FMCAD 2022 (pp. 199–204). TU Wien Academic Press. https://doi.org/10.34727/2022/isbn.978-3-85448-053-2_26
    Download: PDF (327 KB)
  • Error Correction Code Algorithm and Implementation Verification Using Symbolic Representations / Gupta, A., Kaivola, R., Metha, M. P., & Singh, V. (2022). Error Correction Code Algorithm and Implementation Verification Using Symbolic Representations. In A. Griggio & N. Rungta (Eds.), Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design – FMCAD 2022 (pp. 151–159). TU Wien Academic Press. https://doi.org/10.34727/2022/isbn.978-3-85448-053-2_21
    Download: PDF (365 KB)
  • Timed Causal Fanin Analysis for Symbolic Circuit Simulation / Kaivola, R., & Bar Kama, N. (2022). Timed Causal Fanin Analysis for Symbolic Circuit Simulation. In A. Griggio & N. Rungta (Eds.), Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design – FMCAD 2022 (pp. 99–107). TU Wien Academic Press. https://doi.org/10.34727/2022/isbn.978-3-85448-053-2_16
    Download: PDF (555 KB)
  • Synthesis of Semantic Actions in Attribute Grammars / Kalita, P. K., Kumar, M. J., & Roy, S. (2022). Synthesis of Semantic Actions in Attribute Grammars. In A. Griggio & N. Rungta (Eds.), Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design – FMCAD 2022 (pp. 304–314). TU Wien Academic Press. https://doi.org/10.34727/2022/isbn.978-3-85448-053-2_37
    Download: PDF (591 KB)
  • Synthesizing Transducers from Complex Specifications / Grover, A., Ehlers, R., & D’Antoni, L. (2022). Synthesizing Transducers from Complex Specifications. In A. Griggio & N. Rungta (Eds.), Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design – FMCAD 2022 (pp. 294–303). TU Wien Academic Press. https://doi.org/10.34727/2022/isbn.978-3-85448-053-2_36
    Download: PDF (401 KB)
  • ACORN Network Control Plane Abstraction using Route Nondeterminism / Raghunathan, D., Beckett, R., Gupta, A., & Walker, D. (2022). ACORN Network Control Plane Abstraction using Route Nondeterminism. In A. Griggio & N. Rungta (Eds.), Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design – FMCAD 2022 (pp. 261–272). TU Wien Academic Press. https://doi.org/10.34727/2022/isbn.978-3-85448-053-2_33
    Download: PDF (1.8 MB)
  • Split Transition Power Abstraction for Unbounded Safety / Blicha, M., Fedyukovich, G., Hyvärinen, A., & Sharygina, N. (2022). Split Transition Power Abstraction for Unbounded Safety. In A. Griggio & N. Rungta (Eds.), Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design – FMCAD 2022 (pp. 349–358). TU Wien Academic Press. https://doi.org/10.34727/2022/isbn.978-3-85448-053-2_42
    Download: PDF (424 KB)
  • Proving Robustness of KNN Against Adversarial Data Poisoning / Li, Y., Wang, J., & Wang, C. (2022). Proving Robustness of KNN Against Adversarial Data Poisoning. In A. Griggio & N. Rungta (Eds.), Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design – FMCAD 2022 (pp. 7–16). TU Wien Academic Press. https://doi.org/10.34727/2022/isbn.978-3-85448-053-2_6
    Download: PDF (1.23 MB)
  • The seL4 Verification Journey: How Have the Challenges and Opportunities Evolved / Andronick, J. (2022). The seL4 Verification Journey: How Have the Challenges and Opportunities Evolved. In A. Griggio & N. Rungta (Eds.), Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design – FMCAD 2022 (pp. 1–1). TU Wien Academic Press. https://doi.org/10.34727/2022/isbn.978-3-85448-053-2_1
    Download: PDF (67.2 KB)
  • On Applying Model Checking in Formal Verification / Hjort, H. (2022). On Applying Model Checking in Formal Verification. In A. Griggio & N. Rungta (Eds.), Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design – FMCAD 2022 (pp. 3–3). TU Wien Academic Press. https://doi.org/10.34727/2022/isbn.978-3-85448-053-2_3
    Download: PDF (74.7 KB)
  • Verification of Distributed Protocols: Decidable Modeling and Invariant Inference / Padon, O. (2022). Verification of Distributed Protocols: Decidable Modeling and Invariant Inference. In A. Griggio & N. Rungta (Eds.), Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design – FMCAD 2022 (pp. 4–4). TU Wien Academic Press. https://doi.org/10.34727/2022/isbn.978-3-85448-053-2_4
    Download: PDF (66.8 KB)
  • Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design – FMCAD 2022 / Griggio, A., & Rungta, N. (Eds.). (2022). Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design – FMCAD 2022 (Vol. 3, pp. 1–391). TU Wien Academic Press. https://doi.org/10.34727/2022/isbn.978-3-85448-053-2
    Downloads: PDF (19.8 MB) / PDF (456 KB)
  • First-Order Subsumption via SAT Solving / Rath, J., Biere, A., & Kovács, L. (2022). First-Order Subsumption via SAT Solving. In A. Griggio & N. Rungta (Eds.), Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design – FMCAD 2022 (pp. 160–169). TU Wien Academic Press. https://doi.org/10.34727/2022/isbn.978-3-85448-053-2_22
    Download: PDF (551 KB)
  • Synthesizing Self-Stabilizing Parameterized Protocols with Unbounded Variables / Ebnenasir, A. (2022). Synthesizing Self-Stabilizing Parameterized Protocols with Unbounded Variables. In A. Griggio & N. Rungta (Eds.), Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design – FMCAD 2022 (pp. 245–254). TU Wien Academic Press. https://doi.org/10.34727/2022/isbn.978-3-85448-053-2_31
    Download: PDF (952 KB)
  • Small Proofs from Congruence Closure / Flatt, O., Coward, S., Willsey, M., Tatlock, Z., & Panchekha, P. (2022). Small Proofs from Congruence Closure. In A. Griggio & N. Rungta (Eds.), Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design – FMCAD 2022 (pp. 75–83). TU Wien Academic Press. https://doi.org/10.34727/2022/isbn.978-3-85448-053-2_13
    Download: PDF (412 KB)
  • Foundations and Tools in HOL4 for Analysis of Microarchitectural Out-of-Order Execution / Palmskog, K., Yao, X., Dong, N., Guanciale, R., & Dam, M. (2022). Foundations and Tools in HOL4 for Analysis of Microarchitectural Out-of-Order Execution. In A. Griggio & N. Rungta (Eds.), Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design – FMCAD 2022 (pp. 129–138). TU Wien Academic Press. https://doi.org/10.34727/2022/isbn.978-3-85448-053-2_19
    Download: PDF (407 KB)
  • Formally Verified Isolation of DMA / Haglund, J., & Guanciale, R. (2022). Formally Verified Isolation of DMA. In A. Griggio & N. Rungta (Eds.), Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design – FMCAD 2022 (pp. 118–128). TU Wien Academic Press. https://doi.org/10.34727/2022/isbn.978-3-85448-053-2_18
    Download: PDF (507 KB)
  • Lonely Points in Simplices / Jaroschek, M., Kauers, M., & Kovács, L. (2022). Lonely Points in Simplices. Discrete and Computational Geometry, 69, 4–25. https://doi.org/10.1007/s00454-022-00428-2
    Project: ARTIST (2021–2026)
  • Getting Saturated with Induction / Kovacs, L. (2022, September 29). Getting Saturated with Induction [Keynote Presentation]. Automated Reasoning Symposium of Amazon Web Services, United States of America (the). http://hdl.handle.net/20.500.12708/153839
    Project: ARTIST (2021–2026)
  • Algebra-Based Analysis of Polynomial Probabilistic Programs / Kovacs, L. (2022, September 22). Algebra-Based Analysis of Polynomial Probabilistic Programs [Keynote Presentation]. Distinguished Lecture Series of the Max Planck Institute for Software Systems (MPI-SWS), Germany. http://hdl.handle.net/20.500.12708/153258
    Project: ARTIST (2021–2026)
  • User-Propagation for Custom Theories in SMT Solving / Eisenhofer, C. (2022, September 14). User-Propagation for Custom Theories in SMT Solving [Presentation]. 14th Alpine Verification Meeting, Frauenchiemsee, Germany. http://hdl.handle.net/20.500.12708/154343
    Project: ARTIST (2021–2026)
  • Distribution Estimation for Probabilistic Loops / Karimi, A., Moosbrugger, M., Stankovič, M., Kovács, L., Bartocci, E., & Bura, E. (2022). Distribution Estimation for Probabilistic Loops. In E. Ábrahám & M. Paolieri (Eds.), Quantitative Evaluation of Systems (pp. 26–42). Springer-Verlag. https://doi.org/10.1007/978-3-031-16336-4_2
    Projects: ARTIST (2021–2026) / ProbInG (2020–2025)
  • PolySAT - a word-level solver for large bitvectors / Rath, J., Bjørner, N., Kovacs, L., Nutz, A., & Sagiv, M. (2022, September 1). PolySAT - a word-level solver for large bitvectors [Presentation]. Formal Reasoning about Financial Systems, Stanford, United States of America (the). http://hdl.handle.net/20.500.12708/154065
  • Strong-separation Logic (Extended Version) / Pagel, J., & Zuleger, F. (2022). Strong-separation Logic (Extended Version). ACM Letters on Programming Languages and Systems, 44(3), 1–40. https://doi.org/10.1145/3498847
  • Reuse of Introduced Symbols in Automatic Theorem Provers / Rawson, M., Suda, M., Hozzová, P., & Reger, G. (2022). Reuse of Introduced Symbols in Automatic Theorem Provers. In B. Konev, C. Schon, & A. Steen (Eds.), PAAR 2022. Practical Aspects of Automated Reasoning 2022.  Proceedings of the Workshop on Practical Aspects of Automated Reasoning. CEUR-WS.org. https://doi.org/10.34726/4343
    Download: PDF (859 KB)
    Project: ARTIST (2021–2026)
  • The Vampire Approach to Induction (short paper) / Hajdu, M., Kovács, L., Rawson, M., & Voronkov, A. (2022). The Vampire Approach to Induction (short paper). In B. Konev, C. Schon, & A. Steen (Eds.), PAAR 2022. Practical Aspects of Automated Reasoning 2022.  Proceedings of the Workshop on Practical Aspects of Automated Reasoning. https://doi.org/10.34726/4103
    Download: PDF (836 KB)
  • On the Skolem Problem for Reversible Sequences / Kenison, G. (2022). On the Skolem Problem for Reversible Sequences. In 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022) (pp. 61:1-61:15). Schloss Dagstuhl -- Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.MFCS.2022.61
    Projects: ARTIST (2021–2026) / ProbInG (2020–2025)
  • User-Propagation for Custom Theories in SMT Solving / Bjorner, N., Eisenhofer, C., & Kovács, L. (2022). User-Propagation for Custom Theories in SMT Solving. In D. Deharbe & A. Hyvärinen (Eds.), Satisfiability Modulo Theories. 20th International Workshop. SMT 2022. Proceedings (pp. 71–79). CEUR-WS.org. https://doi.org/10.34726/4104
    Download: PDF (1.15 MB)
    Project: ARTIST (2021–2026)
  • Automating Security Analysis of Off-Chain Protocols / Brugger, L. S., Kovacs, L., Petkovic Komel, A., Rain, S., & Rawson, M. (2022, August 11). Automating Security Analysis of Off-Chain Protocols [Conference Presentation]. 4th International Workshop on Formal Methods for Blockchains, Haifa, Israel. https://doi.org/10.34726/3523
    Download: PDF (265 KB)
    Project: ARTIST (2021–2026)
  • Automated Reasoning: 11th International Joint Conference (IJCAR 2022) / Blanchette, J. C., Kovacs, L., & Pattinson, D. (Eds.). (2022). Automated Reasoning: 11th International Joint Conference (IJCAR 2022) (Vol. 13385). Springer-Verlag. https://doi.org/10.1007/978-3-031-10769-6
    Project: ARTIST (2021–2026)
  • Automated Expected Amortised Cost Analysis of Probabilistic Data Structures / Leutgeb, L., Moser, G., & Zuleger, F. (2022). Automated Expected Amortised Cost Analysis of Probabilistic Data Structures. In Computer Aided Verification - 34th International Conference, CAV 2022 (pp. 70–91). https://doi.org/10.1007/978-3-031-13188-2_4
  • Interpolants and Interference / Rebola Pardo, A. (2022). Interpolants and Interference. In M. Benedikt, P. Rümmer, & C. Wernhard (Eds.), iPRA 2022 : The 4th Workshop on Interpolation: From Proofs to Applications : Book of Abstracts (pp. 27–35). http://hdl.handle.net/20.500.12708/198885
    Project: LCS (2017–2025)
  • The probabilistic termination tool amber / Moosbrugger, M., Bartocci, E., Katoen, J.-P., & Kovacs, L. (2022). The probabilistic termination tool amber. Formal Methods in System Design, 61(1), 90–109. https://doi.org/10.1007/s10703-023-00424-z
    Projects: ARTIST (2021–2026) / ProbInG (2020–2025)
  • An SMT Approach for Solving Polynomials over Finite Fields / Hader, T., & Kovacs, L. (2022). An SMT Approach for Solving Polynomials over Finite Fields. In Proceedings of the 20th Internal Workshop on Satisfiability Modulo Theories (SMT) (pp. 90–98).
    Project: ARTIST (2021–2026)
  • The essence of type-theoretic elaboration / Petkovic Komel, A. (2022, July 31). The essence of type-theoretic elaboration [Conference Presentation]. Women In Logic, Haifa, Israel. http://hdl.handle.net/20.500.12708/153703
    Download: talk slides (1.34 MB)
  • Verification of agent navigation in partially-known environments / Aminof, B., Murano, A., Rubin, S., & Zuleger, F. (2022). Verification of agent navigation in partially-known environments. Artificial Intelligence, 308, Article 103724. https://doi.org/10.1016/j.artint.2022.103724
  • Beyond Strong-Cyclic: Doing Your Best in Stochastic Environments / Aminof, B., De Giacomo, G., Rubin, S., & Zuleger, F. (2022). Beyond Strong-Cyclic: Doing Your Best in Stochastic Environments. In Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence (pp. 2525–2531). https://doi.org/10.24963/ijcai.2022/350
  • Low-Level Bi-Abduction / Holík, L., Peringer, P., Rogalewicz, A., Šoková, V., Vojnar, T., & Zuleger, F. (2022). Low-Level Bi-Abduction. In 36th European Conference on Object-Oriented Programming (ECOOP 2022) (pp. 1–30). Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.ECOOP.2022.19
    Download: PDF (1.2 MB)
  • Automated Reasoning for Trustworthy Software / Kovacs, L. (2022, June 21). Automated Reasoning for Trustworthy Software [Keynote Presentation]. Austrian Computer Science Day 2022, IST Austria, Austria. http://hdl.handle.net/20.500.12708/153819
    Project: ARTIST (2021–2026)
  • First-Order Theorem Proving and Vampire / Kovacs, L. (2022, June 17). First-Order Theorem Proving and Vampire [Keynote Presentation]. 15TH SUMMER SCHOOL ON MODELLING AND VERIFICATION OF PARALLEL PROCESSES (MOVEP2022), Aalborg, Denmark. http://hdl.handle.net/20.500.12708/153941
    Project: ARTIST (2021–2026)
  • Algebraic Synthesis of Loops and their Invariants / Kovacs, L. (2022, June 6). Algebraic Synthesis of Loops and their Invariants [Conference Presentation]. Workshop on Differential Algebra, Leipzig, Germany. http://hdl.handle.net/20.500.12708/153259
    Project: ARTIST (2021–2026)
  • Tests and Proofs / Meinke, K., & Kovacs, L. (Eds.). (2022). Tests and Proofs (Vol. 13361). Springer-Verlag. https://doi.org/10.1007/978-3-031-09827-7
    Project: ARTIST (2021–2026)
  • From Truth Degree Comparison Games to Sequents-of-Relations Calculi for Gödel Logic / Fermüller, C., Lang, T. A., & Pavlova, A. (2022). From Truth Degree Comparison Games to Sequents-of-Relations Calculi for Gödel Logic. Logica Universalis, 16(1–2), 221–235. https://doi.org/10.1007/s11787-022-00300-0
    Download: PDF (409 KB)
    Project: SEGACAB (2019–2023)
  • Automated Program Reasoning / Kovacs, L. (2022, May 30). Automated Program Reasoning [Keynote Presentation]. Informatics Europe Webinar Series, Switzerland.
    Project: ARTIST (2021–2026)
  • The essence of elaboration / Petkovic Komel, A. (2022, May 20). The essence of elaboration [Conference Presentation]. Workshop on Syntax and Semantics of Type Thoery, Stockholm, Sweden. http://hdl.handle.net/20.500.12708/153774
    Download: talk slides (1.62 MB)
    Project: ARTIST (2021–2026)
  • Enjoying Research at the Intersection of Math and Computer Science / Kovacs, L. (2022, April 3). Enjoying Research at the Intersection of Math and Computer Science [Keynote Presentation]. ETAPS 2022 Mentoring Workshop, Munich, Germany.
    Project: ARTIST (2021–2026)
  • Algebra-Based Reasoning for Loop Synthesis / Humenberger, A., Amrollahi, D., Bjørner, N., & Kovács, L. (2022). Algebra-Based Reasoning for Loop Synthesis. Formal Aspects of Computing, 34(1), 4:31. https://doi.org/10.1145/3527458
    Projects: ARTIST (2021–2026) / ProbInG (2020–2025)
  • Automated Instantiation of Control Flow Tracing Exercises / Eisenhofer, C., & Riener, M. (2022). Automated Instantiation of Control Flow Tracing Exercises. In J. Marcos, W. Neuper, & P. Quaresma (Eds.), Proceedings 10th International Workshop on Theorem Proving Components for Educational Software (pp. 43–58). EPTCS. https://doi.org/10.4204/EPTCS.354.4
    Download: PDF (629 KB)
  • Verifying safety of synchronous fault-tolerant algorithms by bounded model checking / Stoilkovska, I., Konnov, I., Widder, J., & Zuleger, F. (2022). Verifying safety of synchronous fault-tolerant algorithms by bounded model checking. International Journal on Software Tools for Technology Transfer, 24(1), 33–48. https://doi.org/10.1007/s10009-021-00637-9
  • Getting Saturated with Induction / Kovacs, L. (2022, January 27). Getting Saturated with Induction [Conference Presentation]. Automated Reasoning Seminar at TU Kaiserslautern, Kaiserslautern, Germany. http://hdl.handle.net/20.500.12708/153837
    Project: ARTIST (2021–2026)
  • Can Computers Think as Humans? / Kovacs, L. (2022, January 26). Can Computers Think as Humans? [Keynote Presentation]. WiSE Talk at the SCIENCE Lecture Series Talks of Wiener Volksshochsculen and City of Vienna, Austria.
    Project: ARTIST (2021–2026)
  • Solving Invariant Generation for Unsolvable Loops / Amrollahi, D., Bartocci, E., Kenison, G., Kovács, L., Moosbrugger, M., & Stankovič, M. (2022). Solving Invariant Generation for Unsolvable Loops. In Static Analysis: 29th International Symposium, SAS 2022 (pp. 19–43). https://doi.org/10.1007/978-3-031-22308-2_3
  • Lemmaless Induction in Trace Logic / Bhayat, A., Georgiou, P., Eisenhofer, C., Kovács, L., & Reger, G. (2022). Lemmaless Induction in Trace Logic. In K. Buzzard & T. Kutsia (Eds.), Intelligent Computer Mathematics : 15th International Conference, CICM 2022, Tbilisi, Georgia, September 19–23, 2022, Proceedings (pp. 191–208). https://doi.org/10.34726/5860
    Download: PDF (320 KB)
    Project: DK - Logic (2014–2023)
  • Moment-Based Invariants for Probabilistic Loops with Non-polynomial Assignments / Kofnov, A., Moosbrugger, M., Stankovič, M., Bartocci, E., & Bura, E. (2022). Moment-Based Invariants for Probabilistic Loops with Non-polynomial Assignments. In E. Ábrahám & M. Paolieri (Eds.), Quantitative Evaluation of Systems (pp. 3–25). Springer. https://doi.org/10.1007/978-3-031-16336-4_1
    Projects: ARTIST (2021–2026) / ProbInG (2020–2025)
  • ATLAS: Automated Amortised Complexity Analysis of Self-adjusting Data Structures / Leutgeb, L., Moser, G., & Zuleger, F. (2022). ATLAS: Automated Amortised Complexity Analysis of Self-adjusting Data Structures. In Computer Aided Verification (pp. 99–122). https://doi.org/10.1007/978-3-030-81688-9_5
  • Strong-separation Logic / Pagel, J., & Zuleger, F. (2022). Strong-separation Logic. In ESOP 2021: Programming Languages and Systems (pp. 664–692). Springer. https://doi.org/10.1007/978-3-030-72019-3_24
  • Moment-based analysis of Bayesian network properties / Stankovič, M., Bartocci, E., & Kovács, L. (2022). Moment-based analysis of Bayesian network properties. Theoretical Computer Science, 903, 113–133. https://doi.org/10.1016/j.tcs.2021.12.021

2021

  • Induction with Recursive Definitions in Superposition / Hajdu, M., Hozzová, P., Kovács, L., & Voronkov, A. (2021). Induction with Recursive Definitions in Superposition. In Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021 (Vol. 2, pp. 246–255). TU Wien Academic Press. https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_34
    Download: PDF (350 KB)
  • Single Clause Assumption without Activation Literals to Speed-up IC3 / Froleyks, N., & Biere, A. (2021). Single Clause Assumption without Activation Literals to Speed-up IC3. In Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021 (pp. 72–76). TU Wien Academic Press. https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_15
    Download: PDF (184 KB)
  • CocoAlma: A Versatile Masking Verifier / Hadžić, V., & Bloem, R. (2021). CocoAlma: A Versatile Masking Verifier. In Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021 (pp. 14–23). TU Wien Academic Press. https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_9
    Download: PDF (409 KB)
  • Stainless Verification System Tutorial / Kunčak, V., & Hamza, J. (2021). Stainless Verification System Tutorial. In Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021 (pp. 2–7). TU Wien Academic Press. https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_2
    Download: PDF (187 KB)
  • A Multithreaded Vampire with Shared Persistent Grounding / Rawson, M., & Reger, G. (2021). A Multithreaded Vampire with Shared Persistent Grounding. In Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021 (pp. 280–284). TU Wien Academic Press. https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_38
    Download: PDF (289 KB)
  • Towards an Automatic Proof of Lamport's Paxos / Goel, A., & Sakallah, K. (2021). Towards an Automatic Proof of Lamport’s Paxos. In Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021 (pp. 112–122). TU Wien Academic Press. https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_20
    Download: PDF (519 KB)
  • Scaling Up Hardware Accelerator Verification using A-QED with Functional Decomposition / Chattopadhyay, S., Lonsing, F., Piccolboni, L., Soni, D., Wei, P., Zhang, X., Zhou, Y., Carloni, L., Chen, D., Cong, J., Karri, R., Zhang, Z., Trippel, C., Barrett, C., & Mitra, S. (2021). Scaling Up Hardware Accelerator Verification using A-QED with Functional Decomposition. In Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021 (pp. 42–52). TU Wien Academic Press. https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_12
    Download: PDF (327 KB)
  • End-to-End Formal Verification of a RISC-V Processor Extended with Capability Pointers / Gao, D., & Melham, T. (2021). End-to-End Formal Verification of a RISC-V Processor Extended with Capability Pointers. In Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021 (pp. 24–33). TU Wien Academic Press. https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_10
    Download: PDF (291 KB)
  • Robustness between Weak Memory Models / Chakraborty, S. (2021). Robustness between Weak Memory Models. In Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021 (pp. 173–182). TU Wien Academic Press. https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_26
    Download: PDF (404 KB)
  • Towards Scalable Verification of Deep Reinforcement Learning / Amir, G., Schapira, M., & Katz, G. (2021). Towards Scalable Verification of Deep Reinforcement Learning. In Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021 (pp. 193–203). TU Wien Academic Press. https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_28
    Download: PDF (306 KB)
  • Pruning and Slicing Neural Networks using Formal Verification / Lahav, O., & Katz, G. (2021). Pruning and Slicing Neural Networks using Formal Verification. In Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021 (pp. 183–192). TU Wien Academic Press. https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_27
    Download: PDF (488 KB)
  • Engineering with Full-scale Formal Architecture: Morello, CHERI, Armv8-A, and RISC-V / Sewell, P. (2021). Engineering with Full-scale Formal Architecture: Morello, CHERI, Armv8-A, and RISC-V. In Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021 (pp. 12–12). TU Wien Academic Press. https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_7
    Download: PDF (68.2 KB)
  • Automating System Configuration / Tsiskaridze, N., Strange, M., Mann, M., Sreedhar, K., Liu, Q., Horowitz, M., & Barrett, C. (2021). Automating System Configuration. In Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021 (pp. 103–111). TU Wien Academic Press. https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_19
    Download: PDF (1.28 MB)
  • SAT Solving in the Serverless Cloud / Ozdemir, A., Wu, H., & Barrett, C. (2021). SAT Solving in the Serverless Cloud. In Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021 (pp. 241–245). TU Wien Academic Press. https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_33
    Download: PDF (239 KB)
  • Mathematical Programming Modulo Strings / Kumar, A., & Manolios, P. (2021). Mathematical Programming Modulo Strings. In Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021 (pp. 261–270). TU Wien Academic Press. https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_36
    Download: PDF (403 KB)
  • Active Automata Learning: from L* to L# / Vaandrager, F. (2021). Active Automata Learning: from L* to L#. In Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021 (pp. 9–9). TU Wien Academic Press. https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_4
    Download: PDF (116 KB)
  • Logical Characterization of Coherent Uninterpreted Programs / Govind V K, H., Shoham, S., & Gurfinkel, A. (2021). Logical Characterization of Coherent Uninterpreted Programs. In Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021 (pp. 77–85). TU Wien Academic Press. https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_16
    Download: PDF (425 KB)
  • SAT-Inspired Eliminations for Superposition / Vukmirović, P., Blanchette, J., & Heule, M. (2021). SAT-Inspired Eliminations for Superposition. In Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021 (pp. 231–240). TU Wien Academic Press. https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_32
    Download: PDF (274 KB)
  • Data-driven Optimization of Inductive Generalization / Le, N., Si, X., & Gurfinkel, A. (2021). Data-driven Optimization of Inductive Generalization. In Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021 (pp. 86–95). TU Wien Academic Press. https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_17
    Download: PDF (741 KB)
  • IC3 with Internal Signals / Dureja, R., Gurfinkel, A., Ivrii, A., & Vizel, Y. (2021). IC3 with Internal Signals. In Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021 (pp. 63–71). TU Wien Academic Press. https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_14
    Download: PDF (620 KB)
  • Model Checking AUTOSAR Components with CBMC / Durand, T., Fazekas, K., Weissenbacher, G., & Zwirchmayr, J. (2021). Model Checking AUTOSAR Components with CBMC. In Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021 (pp. 96–101). TU Wien Academic Press. https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_18
    Download: PDF (206 KB)
  • Designing Samplers is Easy: The Boon of Testers / Golia, P., Soos, M., Chakraborty, S., & Meel, K. S. (2021). Designing Samplers is Easy: The Boon of Testers. In Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021 (pp. 222–230). TU Wien Academic Press. https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_31
    Download: PDF (313 KB)
  • Fair and Adventurous Enumeration of Quantifier Instantiations / Janota, M., Barbosa, H., Fontaine, P., & Reynolds, A. (2021). Fair and Adventurous Enumeration of Quantifier Instantiations. In Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021 (pp. 256–260). TU Wien Academic Press. https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_35
    Download: PDF (278 KB)
  • Celestial: A Smart Contracts Verification Framework / Dharanikota, S., Mukherjee, S., Bhardwaj, C., Rastogi, A., & Lal, A. (2021). Celestial: A Smart Contracts Verification Framework. In Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021 (pp. 133–142). TU Wien Academic Press. https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_22
    Download: PDF (489 KB)
  • Exploiting Isomorphic Subgraphs in SAT / Ivrii, A., & Strichman, O. (2021). Exploiting Isomorphic Subgraphs in SAT. In Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021 (pp. 204–211). TU Wien Academic Press. https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_29
    Download: PDF (351 KB)
  • The Civl Verifier / Kragl, B., & Qadeer, S. (2021). The Civl Verifier. In Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021 (pp. 143–152). TU Wien Academic Press. https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_23
    Download: PDF (381 KB)
  • Hardware Security Leak Detection by Symbolic Simulation / Bar Kama, N., & Kaivola, R. (2021). Hardware Security Leak Detection by Symbolic Simulation. In Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021 (pp. 34–41). TU Wien Academic Press. https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_11
    Download: PDF (845 KB)
  • Sound and Automated Verification of Real-World RTL Multipliers / Temel, M., & Hunt, W. A., Jr. (2021). Sound and Automated Verification of Real-World RTL Multipliers. In Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021 (pp. 53–62). TU Wien Academic Press. https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_13
    Download: PDF (753 KB)
  • Algorithms for the People / Kamara, S. (2021). Algorithms for the People. In Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021 (pp. 11–11). TU Wien Academic Press. https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_6
    Download: PDF (65.1 KB)
  • Dynamic Partial Order Reductions for Spinloops / Kokologiannakis, M., Ren, X., & Vafeiadis, V. (2021). Dynamic Partial Order Reductions for Spinloops. In Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021 (pp. 163–172). TU Wien Academic Press. https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_25
    Download: PDF (501 KB)
  • From Viewstamped Replication to Blockchains / Liskov, B. (2021). From Viewstamped Replication to Blockchains. In Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021 (pp. 10–10). TU Wien Academic Press. https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_5
    Download: PDF (44.7 KB)
  • Lookahead in Partitioning SMT / Hyvärinen, A., Marescotti, M., & Sharygina, N. (2021). Lookahead in Partitioning SMT. In Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021 (pp. 271–279). TU Wien Academic Press. https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_37
    Download: PDF (779 KB)
  • Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021 / Piskac, R., & Whalen, M. W. (Eds.). (2021). Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021 (Vol. 2). TU Wien Academic Press. https://doi.org/10.34727/2021/isbn.978-3-85448-046-4
    Downloads: Published Version (10.8 MB) / Table of Contents (304 KB)
  • Refinement-Based Verification of Device-to-Device Information Flow / Dong, N., Guanciale, R., & Dam, M. (2021). Refinement-Based Verification of Device-to-Device Information Flow. In Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021 (pp. 123–132). TU Wien Academic Press. https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_21
    Download: PDF (1.74 MB)
  • Reactive Synthesis Beyond Realizability / Dimitrova, R. (2021). Reactive Synthesis Beyond Realizability. In Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021 (pp. 1–1). TU Wien Academic Press. https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_1
    Download: Abstract (79.8 KB)
  • On Decomposition of Maximal Satisfiable Subsets / Bendik, J. (2021). On Decomposition of Maximal Satisfiable Subsets. In Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021 (pp. 212–221). TU Wien Academic Press. https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_30
    Download: PDF (388 KB)
  • The FMCAD 2021 Student Forum / Santolucito, M. (2021). The FMCAD 2021 Student Forum. In Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021 (pp. 13–13). TU Wien Academic Press. https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_8
    Download: PDF (74.4 KB)
  • Formal Methods for the Security Analysis of Smart Contracts / Maffei, M. (2021). Formal Methods for the Security Analysis of Smart Contracts. In Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021 (pp. 8–8). TU Wien Academic Press. https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_3
    Download: PDF (47.5 KB)
  • Synthesizing Pareto-Optimal Interpretations for Black-Box Models / Torfah, H., Shah, S., Chakraborty, S., Akshay, S., & Seshia, S. A. (2021). Synthesizing Pareto-Optimal Interpretations for Black-Box Models. In Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021 (pp. 153–162). TU Wien Academic Press. https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_24
    Download: PDF (322 KB)
  • Inductive Benchmarks for Automated Reasoning / Hajdu, M., Hozzová, P., Kovács, L., Schoisswohl, J., & Voronkov, A. (2021). Inductive Benchmarks for Automated Reasoning. In Intelligent Computer Mathematics. 14th International Conference, CICM 2021, Timisoara, Romania, July 26–31, 2021. Proceedings (pp. 124–129). Springer. https://doi.org/10.34726/1563
    Download: PDF (216 KB)
    Projects: ARTIST (2021–2026) / Symcar (2016–2021)
  • Automated Generation of Exam Sheets for Automated Deduction / Hozzová, P., Kovács, L., & Rath, J. (2021). Automated Generation of Exam Sheets for Automated Deduction. In Intelligent Computer Mathematics. 14th International Conference, CICM 2021, Timisoara, Romania, July 26–31, 2021. Proceedings (pp. 185–196). Springer. https://doi.org/10.34726/1562
    Download: PDF (458 KB)
    Projects: ARTIST (2021–2026) / Symcar (2016–2021)
  • On Positivity and Minimality for Second-Order Holonomic Sequences / Kenison, G. J., Klurman, O., Lefaucheux, E., Luca, F., Moree, P., Ouaknine, J., Whiteland, M., & Worrell, J. (2021). On Positivity and Minimality for Second-Order Holonomic Sequences. In F. Bonchi & S. Puglisi (Eds.), 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021) (pp. 1–15). Schloss Dagstuhl -- Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.MFCS.2021.67
    Download: PDF (709 KB)
    Projects: ARTIST (2021–2026) / ProbInG (2020–2025)
  • Integer Induction in Saturation / Hozzová, P., Kovács, L., & Voronkov, A. (2021). Integer Induction in Saturation. In Proceedings of CADE 2021 (pp. 361–377). Springer, Cham. https://doi.org/10.34726/1561
    Download: Preprint submitted for publication as it is (345 KB)
    Projects: ARTIST (2021–2026) / Symcar (2016–2021)
  • Induction in Saturation-Based Reasoning / Kovacs, L. (2021, July 26). Induction in Saturation-Based Reasoning [Keynote Presentation]. 14th Conference on Intelligent Computer Mathematics (CICM 2021), Timisoara, Romania. http://hdl.handle.net/20.500.12708/154161
    Project: ARTIST (2021–2026)
  • The Probabilistic Termination Tool Amber / Marcel Moosbrugger, Ezio Bartocci, Katoen, J.-P., & Laura Kovács. (2021). The Probabilistic Termination Tool Amber. In Formal Methods. FM 2021 (pp. 667–675). https://doi.org/10.1007/978-3-030-90870-6_36
  • Automated Termination Analysis of Polynomial Probabilistic Programs / Moosbrugger, M., Bartocci, E., Katoen, J.-P., & Kovács, L. (2021). Automated Termination Analysis of Polynomial Probabilistic Programs. In Programming Languages and Systems (pp. 491–518). Springer. https://doi.org/10.1007/978-3-030-72019-3_18
  • Algebra-Based Synthesis of Loops and Their Invariants (Invited Paper) / Humenberger, A., & Kovács, L. (2021). Algebra-Based Synthesis of Loops and Their Invariants (Invited Paper). In F. Henglein, S. Shoham, & Y. Vizel (Eds.), Verification, Model Checking, and Abstract Interpretation (pp. 17–28). Springer LNCS. https://doi.org/10.1007/978-3-030-67067-2_2
  • Bounded Model Checking of Speculative Non-Interference / Pescosta, E., Weissenbacher, G., & Zuleger, F. (2021). Bounded Model Checking of Speculative Non-Interference. In 2021 IEEE/ACM International Conference On Computer Aided Design (ICCAD). 2021 IEEE/ACM International Conference On Computer Aided Design (ICCAD), München, Germany. IEEE. https://doi.org/10.1109/iccad51958.2021.9643462
  • Synthesizing Best-effort Strategies under Multiple Environment Specifications / Aminof, B., De Giacomo, G., Lomuscio, A., Murano, A., & Rubin, S. (2021). Synthesizing Best-effort Strategies under Multiple Environment Specifications. In Proceedings of the Eighteenth International Conference on Principles of Knowledge Representation and Reasoning. KR 2021 - 18th International Conference on Principles of Knowledge Representation and Reasoning, virtual event, Unknown. https://doi.org/10.24963/kr.2021/5
  • Best-Effort Synthesis: Doing Your Best Is Not Harder Than Giving Up / Aminof, B., De Giacomo, G., & Rubin, S. (2021). Best-Effort Synthesis: Doing Your Best Is Not Harder Than Giving Up. In Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence. IJCAI 2021 - 30th International Joint Conference on Artificial Intelligence, Montreal, Canada, Canada. https://doi.org/10.24963/ijcai.2021/243
  • Automating Induction by Reflection / Schoisswohl, J., & Kovács, L. (2021). Automating Induction by Reflection. In E. Pimentel & E. Tassi (Eds.), Electronic Proceedings in Theoretical Computer Science (pp. 39–54). EPTCS. https://doi.org/10.4204/eptcs.337.4
  • Eliminating Message Counters in Synchronous Threshold Automata / Stoilkovska, I., Konnov, I., Widder, J., & Zuleger, F. (2021). Eliminating Message Counters in Synchronous Threshold Automata. In VMCAI 2021: Verification, Model Checking, and Abstract Interpretation (pp. 196–218). Springer LNCS. https://doi.org/10.1007/978-3-030-67067-2_10
  • Summing up Smart Transitions / Elad, N., Rain, S., Immerman, N., Sagiv, M., & Kovacs, L. (2021). Summing up Smart Transitions. In A. Silva & R. Leino (Eds.), Computer Aided Verification (pp. 317–340). Springer LNCS. https://doi.org/10.1007/978-3-030-81685-8_15
  • Preface of the special issue on the conference on computer-aided verification 2018 / Chockler, H., & Weissenbacher, G. (2021). Preface of the special issue on the conference on computer-aided verification 2018. Formal Methods in System Design. https://doi.org/10.1007/s10703-021-00365-5
  • Mutation testing with hyperproperties / Fellner, A., Tabaei Befrouei, M., & Weissenbacher, G. (2021). Mutation testing with hyperproperties. Software and Systems Modeling, 20(2), 405–427. https://doi.org/10.1007/s10270-020-00850-1
  • Algorithm selection and instance space analysis for curriculum-based course timetabling / De Coster, A., Musliu, N., Schaerf, A., Schoisswohl, J., & Smith-Miles, K. (2021). Algorithm selection and instance space analysis for curriculum-based course timetabling. Journal of Scheduling, 25(1), 35–58. https://doi.org/10.1007/s10951-021-00701-x
  • Rely-guarantee bound analysis of parameterized concurrent shared-memory programs / Pani, T., Weissenbacher, G., & Zuleger, F. (2021). Rely-guarantee bound analysis of parameterized concurrent shared-memory programs. Formal Methods in System Design, 57(2), 270–302. https://doi.org/10.1007/s10703-021-00370-8

2020

  • Induction with Generalization in Superposition Reasoning / Hajdú, M., Hozzová, P., Kovács, L., Schoisswohl, J., & Voronkov, A. (2020). Induction with Generalization in Superposition Reasoning. In Proceedings of the 13th International Conference on Intelligent Computer Mathematics (CICM) (pp. 123–137). Springer. https://doi.org/10.34726/961
    Download: Postprint was published at CICM 2020. (300 KB)
    Projects: DoS-IoT (2019–2020) / Symcar (2016–2021) / SYMELS (2019–2020)
  • Towards Higher-order OWL / Homola, M., Kľuka, J., Hozzová, P., Svátek, V., & Vacura, M. (2020). Towards Higher-order OWL. Kuenstliche Intelligenz, 34, 417–421. https://doi.org/10.1007/s13218-020-00665-8
  • Portfolio SAT and SMT Solving of Cardinality Constraints in Sensor Network Optimization / Kovasznai, G., Gajdár, K., & Kovács, L. (2020). Portfolio SAT and SMT Solving of Cardinality Constraints in Sensor Network Optimization. In H. Hong, V. Negru, D. Petcu, & D. Zaharie (Eds.), Proceedings of the 21st International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (pp. 85–91). IEEE. https://doi.org/10.34726/341
    Download: accepted version (499 KB)
    Projects: Symcar (2016–2021) / SYMELS (2019–2020)
  • Superposition Reasoning about Quantified Bitvector Formulas / Damestani, D., Kovács, L., & Suda, M. (2020). Superposition Reasoning about Quantified Bitvector Formulas. In H. Hong, V. Negru, D. Petcu, & D. Zaharie (Eds.), Proceedings of the 21st International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (pp. 95–99). IEEE. https://doi.org/10.34726/342
    Download: accepted version (226 KB)
    Projects: Symcar (2016–2021) / SYMELS (2019–2020)
  • Parallelization Techniques for Verifying Neural Networks / Wu, H., Ozdemir, A., Zeljic, A., Julian, K., Irfan, A., Gopinath, D., Fouladi, S., Katz, G., Pasareanu, C., & Barrett, C. (2020). Parallelization Techniques for Verifying Neural Networks. In A. Ivrii & O. Strichman (Eds.), Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design – FMCAD 2020 (pp. 128–137). TU Wien Academic Press. https://doi.org/10.34727/2020/isbn.978-3-85448-042-6_20
    Download: Published version (1.07 MB)
  • The Proof Checkers Pacheck and Pastèque for the Practical Algebraic Calculus / Kaufmann, D., Fleury, M., & Biere, A. (2020). The Proof Checkers Pacheck and Pastèque for the Practical Algebraic Calculus. In A. Ivrii & O. Strichman (Eds.), Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design – FMCAD 2020 (pp. 264–269). TU Wien Academic Press. https://doi.org/10.34727/2020/isbn.978-3-85448-042-6_34
    Download: Published version (375 KB)
  • Angelic Checking within Static Driver Verifier: Towards high-precision defects without (modeling) cost / Lahiri, S. K., Lal, A., Gopinath, S., Nutz, A., Levin, V., Kumar, R., Deisinger, N., Lichtenberg, J., & Bansal, C. (2020). Angelic Checking within Static Driver Verifier: Towards high-precision defects without (modeling) cost. In A. Ivrii & O. Strichman (Eds.), Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design – FMCAD 2020 (pp. 169–178). TU Wien Academic Press. https://doi.org/10.34727/2020/isbn.978-3-85448-042-6_24
    Download: Published version (443 KB)
  • Tutorial on World-Level Model Checking / Biere, A. (2020). Tutorial on World-Level Model Checking. In A. Ivrii & O. Strichman (Eds.), Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design – FMCAD 2020. TU Wien Academic Press. https://doi.org/10.34727/2020/isbn.978-3-85448-042-6_3
    Download: Published version (159 KB)
  • Incremental Verification by SMT-based Summary Repair / Asadi, S., Blicha, M., Hyvärinen, A., Fedyukovich, G., & Sharygina, N. (2020). Incremental Verification by SMT-based Summary Repair. In A. Ivrii & O. Strichman (Eds.), Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design – FMCAD 2020 (pp. 77–82). TU Wien Academic Press. https://doi.org/10.34727/2020/isbn.978-3-85448-042-6_14
    Download: Published version (1.99 MB)
  • Automating Modular Verification of Secure Information Flow / Pick, L., Fedyukovich, G., & Gupta, A. (2020). Automating Modular Verification of Secure Information Flow. In A. Ivrii & O. Strichman (Eds.), Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design – FMCAD 2020 (pp. 158–168). TU Wien Academic Press. https://doi.org/10.34727/2020/isbn.978-3-85448-042-6_23
    Download: Published version (510 KB)
  • Selecting Stable Safe Configurations for Systems Modelled by Neural Networks with ReLU Activation / Brauße, F., Khasidashvili, Z., & Korovin, K. (2020). Selecting Stable Safe Configurations for Systems Modelled by Neural Networks with ReLU Activation. In A. Ivrii & O. Strichman (Eds.), Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design – FMCAD 2020 (pp. 119–127). TU Wien Academic Press. https://doi.org/10.34727/2020/isbn.978-3-85448-042-6_19
    Download: Published version (402 KB)
  • EUFicient Reachability for Software with Arrays / Bueno, D., Cox, A., & Sakallah, K. (2020). EUFicient Reachability for Software with Arrays. In A. Ivrii & O. Strichman (Eds.), Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design – FMCAD 2020 (pp. 57–66). TU Wien Academic Press. https://doi.org/10.34727/2020/isbn.978-3-85448-042-6_12
    Download: Published version (924 KB)
  • Accelerating Parallel Verification via Complementary Property Partitioning and Strategy Exploration / Dureja, R., Baumgartner, J., Kanzelman, R., Williams, M., & Kristin Y. Rozier. (2020). Accelerating Parallel Verification via Complementary Property Partitioning and Strategy Exploration. In A. Ivrii & O. Strichman (Eds.), Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design – FMCAD 2020 (pp. 16–25). TU Wien Academic Press. https://doi.org/10.34727/2020/isbn.978-3-85448-042-6_8
    Download: Published version (698 KB)
  • Verifying Properties of Bit-vector Multiplication Using Cutting Planes Reasoning / Liew, V., Beame, P., Devriendt, J., Elffers, J., & Nordström, J. (2020). Verifying Properties of Bit-vector Multiplication Using Cutting Planes Reasoning. In A. Ivrii & O. Strichman (Eds.), Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design – FMCAD 2020 (pp. 194–204). TU Wien Academic Press. https://doi.org/10.34727/2020/isbn.978-3-85448-042-6_27
    Download: PDF (1.02 MB)
  • Effective System Level Liveness Verification / Fedotov, A., Keiren, J., & Schmaltz, J. (2020). Effective System Level Liveness Verification. In A. Ivrii & O. Strichman (Eds.), Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design – FMCAD 2020 (pp. 7–15). TU Wien Academic Press. https://doi.org/10.34727/2020/isbn.978-3-85448-042-6_7
    Download: Published version (496 KB)
  • From Correctness to High Quality / Kupferman, O. (2020). From Correctness to High Quality. In A. Ivrii & O. Strichman (Eds.), Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design – FMCAD 2020. TU Wien Academic Press. https://doi.org/10.34727/2020/isbn.978-3-85448-042-6_5
    Download: Published version (570 KB)
  • A Theoretical Framework for Symbolic Quick Error Detection / Lonsing, F., Mitra, S., & Barrett, C. (2020). A Theoretical Framework for Symbolic Quick Error Detection. In A. Ivrii & O. Strichman (Eds.), Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design – FMCAD 2020 (pp. 26–35). TU Wien Academic Press. https://doi.org/10.34727/2020/isbn.978-3-85448-042-6_9
    Download: Published version (459 KB)
  • Reductions for Strings and Regular Expressions Revisited / Reynolds, A., Nötzli, A., Barrett, C., & Tinelli, C. (2020). Reductions for Strings and Regular Expressions Revisited. In A. Ivrii & O. Strichman (Eds.), Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design – FMCAD 2020 (pp. 225–235). TU Wien Academic Press. https://doi.org/10.34727/2020/isbn.978-3-85448-042-6_30
    Download: Published version (1.34 MB)
  • Ternary Propagation-Based Local Search for More Bit-Precise Reasoning / Niemetz, A., & Preiner, M. (2020). Ternary Propagation-Based Local Search for More Bit-Precise Reasoning. In A. Ivrii & O. Strichman (Eds.), Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design – FMCAD 2020 (pp. 214–224). TU Wien Academic Press. https://doi.org/10.34727/2020/isbn.978-3-85448-042-6_29
    Download: Published version (7.94 MB)
  • Using model checking tools to triage the severity of security bugs in the Xen hypervisor / Cook, B., Döbel, B., Kroening, D., Manthey, N., Pohlack, M., Polgreen, E., Tautschnig, M., & Wieczorkiewicz, P. (2020). Using model checking tools to triage the severity of security bugs in the Xen hypervisor. In A. Ivrii & O. Strichman (Eds.), Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design – FMCAD 2020 (pp. 185–193). TU Wien Academic Press. https://doi.org/10.34727/2020/isbn.978-3-85448-042-6_26
    Download: Published version (334 KB)
  • Automating Compositional Analysis of Authentication Protocols / Zhang, Z., de Amorim, A. A., Jia, L., & Pasareanu, C. S. (2020). Automating Compositional Analysis of Authentication Protocols. In A. Ivrii & O. Strichman (Eds.), Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design – FMCAD 2020 (pp. 113–118). TU Wien Academic Press. https://doi.org/10.34727/2020/isbn.978-3-85448-042-6_18
    Download: Published version (255 KB)
  • Runtime Verification on FPGAs with LTLf Specifications / Tracy II, T., Tabajara, L., Vardi, M., & Skadron, K. (2020). Runtime Verification on FPGAs with LTLf Specifications. In A. Ivrii & O. Strichman (Eds.), Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design – FMCAD 2020 (pp. 36–46). TU Wien Academic Press. https://doi.org/10.34727/2020/isbn.978-3-85448-042-6_10
    Download: Published version (731 KB)
  • Distributed Bounded Model Checking / Chatterje, P., Roy, S., Phi Diep, B., & Lal, A. (2020). Distributed Bounded Model Checking. In A. Ivrii & O. Strichman (Eds.), Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design – FMCAD 2020 (pp. 47–56). TU Wien Academic Press. https://doi.org/10.34727/2020/isbn.978-3-85448-042-6_11
    Download: Published version (966 KB)
  • Trace Logic for Inductive Loop Reasoning / Georgiou, P., Gleiss, B., & Kovacs, L. (2020). Trace Logic for Inductive Loop Reasoning. In A. Ivrii & O. Strichman (Eds.), Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design - FMCAD 2020 (pp. 255–263). IEEE. https://doi.org/10.34727/2020/isbn.978-3-85448-042-6_33
  • Layered Clause Selection for Theory Reasoning / Gleiss, B., & Suda, M. (2020). Layered Clause Selection for Theory Reasoning. In N. Peltier & V. Sofronie-Stokkermans (Eds.), Automated Reasoning (pp. 402–409). Lecture Notes in Computer Science, Springer. https://doi.org/10.1007/978-3-030-51074-9_23
  • Analysis of Bayesian Networks via Prob-Solvable Loops / Bartocci, E., Kovács, L., & Stankovič, M. (2020). Analysis of Bayesian Networks via Prob-Solvable Loops. In Theoretical Aspects of Computing – ICTAC 2020 (pp. 221–241). Springer. https://doi.org/10.1007/978-3-030-64276-1_12
  • Mora - Automatic Generation of Moment-Based Invariants / Bartocci, E., Kovács, L., & Stankovič, M. (2020). Mora - Automatic Generation of Moment-Based Invariants. In Tools and Algorithms for the Construction and Analysis of Systems (pp. 492–498). Springer. https://doi.org/10.1007/978-3-030-45190-5_28
  • Reactive Synthesis from Extended Bounded Response LTL Specifications / Cimatti, A., GEATTI, L., Gigante, N., MONTANARI, A., & Tonetta, S. (2020). Reactive Synthesis from Extended Bounded Response LTL Specifications. In A. Ivrii & O. Strichman (Eds.), Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design – FMCAD 2020 (pp. 83–92). TU Wien Academic Press. https://doi.org/10.34727/2020/isbn.978-3-85448-042-6_15
    Download: Published version (569 KB)
  • Formal Methods with a Touch of Magic / Alamdari, P. A., Avni, G., Henzinger, T. A., & Lukina, A. (2020). Formal Methods with a Touch of Magic. In A. Ivrii & O. Strichman (Eds.), Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design – FMCAD 2020 (pp. 138–147). TU Wien Academic Press. https://doi.org/10.34727/2020/isbn.978-3-85448-042-6_21
    Download: Published version (968 KB)
  • ART: Abstraction Refinement-Guided Training for Provably Correct Neural Networks / Lin, X., Zhu, H., Samanta, R., & Jagannathan, S. (2020). ART: Abstraction Refinement-Guided Training for Provably Correct Neural Networks. In A. Ivrii & O. Strichman (Eds.), Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design – FMCAD 2020 (pp. 148–157). TU Wien Academic Press. https://doi.org/10.34727/2020/isbn.978-3-85448-042-6_22
    Download: Published version (452 KB)
  • SWITSS: Computing Small Witnessing Subsystems / Jantsch, S., Harder, H., Funke, F., & Baier, C. (2020). SWITSS: Computing Small Witnessing Subsystems. In A. Ivrii & O. Strichman (Eds.), Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design – FMCAD 2020 (pp. 236–244). TU Wien Academic Press. https://doi.org/10.34727/2020/isbn.978-3-85448-042-6_31
    Download: Published version (896 KB)
  • Smart Induction for Isabelle/HOL (Tool Paper) / Nagashima, Y. (2020). Smart Induction for Isabelle/HOL (Tool Paper). In A. Ivrii & O. Strichman (Eds.), Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design – FMCAD 2020 (pp. 245–254). TU Wien Academic Press. https://doi.org/10.34727/2020/isbn.978-3-85448-042-6_32
    Download: Published version (662 KB)
  • Anytime Algorithms for MaxSAT and Beyond / Nadel, A. (2020). Anytime Algorithms for MaxSAT and Beyond. In A. Ivrii & O. Strichman (Eds.), Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design – FMCAD 2020. TU Wien Academic Press. https://doi.org/10.34727/2020/isbn.978-3-85448-042-6_1
    Download: Published version (637 KB)
  • Trace Logic for Inductive Loop Reasoning / Georgiou, P., Gleiss, B., & Kovács, L. (2020). Trace Logic for Inductive Loop Reasoning. In A. Ivrii & O. Strichman (Eds.), Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design – FMCAD 2020 (pp. 255–263). TU Wien Academic Press. https://doi.org/10.34727/2020/isbn.978-3-85448-042-6_33
    Download: Published version (490 KB)
  • Formal Verification for Natural and Engineered Biological Systems / Kugler, H. (2020). Formal Verification for Natural and Engineered Biological Systems. In A. Ivrii & O. Strichman (Eds.), Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design – FMCAD 2020. TU Wien Academic Press. https://doi.org/10.34727/2020/isbn.978-3-85448-042-6_2
    Download: Published version (623 KB)
  • How testable is business software? / Schrammel, P. (2020). How testable is business software? In A. Ivrii & O. Strichman (Eds.), Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design – FMCAD 2020. TU Wien Academic Press. https://doi.org/10.34727/2020/isbn.978-3-85448-042-6_4
    Download: Published version (552 KB)
  • SYSLITE: Syntax-Guided Synthesis of PLTL Formulas from Finite Traces / Arif, M. F., Larraz, D., Echeverria, M., Reynolds, A., Chowdhury, O., & Tinelli, C. (2020). SYSLITE: Syntax-Guided Synthesis of PLTL Formulas from Finite Traces. In A. Ivrii & O. Strichman (Eds.), Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design – FMCAD 2020 (pp. 93–103). TU Wien Academic Press. https://doi.org/10.34727/2020/isbn.978-3-85448-042-6_16
    Download: Published version (338 KB)
  • Learning Properties in LTL ∩ ACTL from Positive Examples Only / Ehlers, R., Gavran, I., & Neider, D. (2020). Learning Properties in LTL ∩ ACTL from Positive Examples Only. In A. Ivrii & O. Strichman (Eds.), Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design – FMCAD 2020 (pp. 104–112). TU Wien Academic Press. https://doi.org/10.34727/2020/isbn.978-3-85448-042-6_17
    Download: PDF (442 KB)
  • Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design – FMCAD 2020 / Ivrii, A., & Strichman, O. (Eds.). (2020). Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design – FMCAD 2020 (Vol. 1). TU Wien Academic Press. https://doi.org/10.34727/2020/isbn.978-3-85448-042-6
    Downloads: Table of Contents (325 KB) / Published version (18 MB)
  • Model Checking Software-Defined Networks with Flow Entries that Time Out / Klimis, V., Parisis, G., & Reus, B. (2020). Model Checking Software-Defined Networks with Flow Entries that Time Out. In A. Ivrii & O. Strichman (Eds.), Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design – FMCAD 2020 (pp. 179–184). TU Wien Academic Press. https://doi.org/10.34727/2020/isbn.978-3-85448-042-6_25
    Download: Published version (1.22 MB)
  • On Optimizing a Generic Function in SAT / Nadel, A. (2020). On Optimizing a Generic Function in SAT. In A. Ivrii & O. Strichman (Eds.), Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design – FMCAD 2020 (pp. 205–213). TU Wien Academic Press. https://doi.org/10.34727/2020/isbn.978-3-85448-042-6_28
    Download: Published version (391 KB)
  • Thread-modular Counter Abstraction for Parameterized Program Safety / Pani, T., Weissenbacher, G., & Zuleger, F. (2020). Thread-modular Counter Abstraction for Parameterized Program Safety. In A. Ivrii & O. Strichman (Eds.), Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design – FMCAD 2020 (pp. 67–76). TU Wien Academic Press. https://doi.org/10.34727/2020/isbn.978-3-85448-042-6_13
    Download: Published version (434 KB)
  • The FMCAD 2020 Student Forum / Schrammel, P. (2020). The FMCAD 2020 Student Forum. In A. Ivrii & O. Strichman (Eds.), Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design – FMCAD 2020. TU Wien Academic Press. https://doi.org/10.34727/2020/isbn.978-3-85448-042-6_6
    Download: Published version (590 KB)
  • Subsumption Demodulation in First-Order Theorem Proving / Gleiss, B., Kovacs, L., & Rath, J. (2020). Subsumption Demodulation in First-Order Theorem Proving. In N. Peltier & V. Sofronie-Stokkermans (Eds.), Automated Reasoning (pp. 297–315). Lecture Notes in Computer Science, Springer. https://doi.org/10.1007/978-3-030-51074-9_17
  • An ExpTime Upper Bound for ALC with Integers (Extended Version) / Labai, N., Simkus, M., & Ortiz, M. (2020). An ExpTime Upper Bound for ALC with Integers (Extended Version). arXiv. https://doi.org/10.48550/arXiv.2006.02078
  • Algebra-Based Loop Synthesis / Humenberger, A., Bjørner, N., & Kovacs, L. (2020). Algebra-Based Loop Synthesis. In B. Dongol & E. Troubitsyna (Eds.), Integrated Formal Methods. Proceedings of the 16th International Conference, IFM 2020 (pp. 440–459). Springer. https://doi.org/10.1007/978-3-030-63461-2_24
  • Language Inclusion for Finite Prime Event Structures / Fellner, A., Tarrach, T., & Weissenbacher, G. (2020). Language Inclusion for Finite Prime Event Structures. In Verification, Model Checking, and Abstract Interpretation 21st International Conference, VMCAI 2020, New Orleans, LA, USA, January 16–21, 2020, Proceedings (pp. 314–336). Springer. https://doi.org/10.1007/978-3-030-39322-9_15
  • Formalizing Graph Trail Properties in Isabelle/HOL / Kovács, L., Lachnitt, H., & Szeider, S. (2020). Formalizing Graph Trail Properties in Isabelle/HOL. In Intelligent Computer Mathematics 13th International Conference, CICM 2020, Bertinoro, Italy, July 26–31, 2020, Proceedings (pp. 190–205). LNCS. https://doi.org/10.1007/978-3-030-53518-6_12
  • The Polynomial Complexity of Vector Addition Systems with States / Zuleger, F. (2020). The Polynomial Complexity of Vector Addition Systems with States. In Foundations of Software Science and Computation Structures 23rd International Conference, FOSSACS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25–30, 2020, Proceedings (pp. 622–641). Springer LNCS. https://doi.org/10.1007/978-3-030-45231-5_32
  • Thread-modular Counter Abstraction for Parameterized Program Safety / Pani, T., Weissenbacher, G., & Zuleger, F. (2020). Thread-modular Counter Abstraction for Parameterized Program Safety. In Formal Methods in Computer-Aided Design (pp. 67–76). TU Wien Academic Press / IEEE. https://doi.org/10.34727/2020/isbn.978-3-85448-042-6_13
  • Pebble-Intervals Automata and FO² with Two Orders / Labai, N., Kotek, T., Ortiz, M., & Veith, H. (2020). Pebble-Intervals Automata and FO2 with Two Orders. In Language and Automata Theory and Applications (pp. 208–221). Lecture Notes in Computer Science (LNCS). https://doi.org/10.1007/978-3-030-40608-0_14
  • Multi-linear Strategy Extraction for QBF Expansion Proofs via Local Soundness / Schlaipfer, M., Slivovsky, F., Weissenbacher, G., & Zuleger, F. (2020). Multi-linear Strategy Extraction for QBF Expansion Proofs via Local Soundness. In Theory and Applications of Satisfiability Testing – SAT 2020 (pp. 429–446). LNCS. https://doi.org/10.1007/978-3-030-51825-7_30
  • An ExpTime Upper Bound for ALC with Integers / Labai, N., Simkus, M., & Ortiz de la Fuente, M. M. (2020). An ExpTime Upper Bound for ALC with Integers. In D. Calvanese, E. Erdem, & M. Thielscher (Eds.), Proceedings of the Seventeenth International Conference on Principles of Knowledge Representation and Reasoning. AAAI Press. https://doi.org/10.24963/kr.2020/61
  • RAT Elimination / Rebola Pardo, A., & Weissenbacher, G. (2020). RAT Elimination. In L. Kovacs & E. Albert (Eds.), EPiC Series in Computing. EasyChair. https://doi.org/10.29007/fccb
  • Layered Clause Selection for Theory Reasoning / Gleiss, B., & Suda, M. (2020). Layered Clause Selection for Theory Reasoning. In P. Fontaine, K. Korovin, & I. Kotsireas (Eds.), Joint Proceedings of the 7th Workshop on Practical Aspects of Automated Reasoning (PAAR) and the 5th Satisfiability Checking and Symbolic Computation Workshop (SC-Square) Workshop (pp. 34–52). CEUR Workshop Proceedings. http://hdl.handle.net/20.500.12708/58379
  • A typed parallel lambda-calculus via 1-depth intermediate proofs / Aschieri, F., Ciabattoni, A., & Genco, F. A. (2020). A typed parallel lambda-calculus via 1-depth intermediate proofs. In L. Kovacs (Ed.), EPiC Series in Computing. EasyChair EPiC Series in Computing. https://doi.org/10.29007/g15z
  • Synthesizing strategies under expected and exceptional environment behaviors / Aminof, B., De Giacomo, G., Lomuscio, A., Murano, A., & Rubin, S. (2020). Synthesizing strategies under expected and exceptional environment behaviors. In Proceedings of the Twenty-Ninth International Joint Conference on Artificial Intelligence. International Joint Conferences on Artificial Intelligence Organization. https://doi.org/10.24963/ijcai.2020/232
  • Stochastic Fairness and Language-Theoretic Fairness in Planning in Nondeterministic Domains / Aminof, B., De Giacomo, G., & Rubin, S. (2020). Stochastic Fairness and Language-Theoretic Fairness in Planning in Nondeterministic Domains. In Proceedings of the Thirtieth International Conference on Automated Planning and Scheduling, Nancy, France (pp. 20–28). AAAI Press. http://hdl.handle.net/20.500.12708/58428
  • Preface of the Special Issue on the Conference on Formal Methods in Computer-Aided Design 2017 / Stewart, D., & Weissenbacher, G. (2020). Preface of the Special Issue on the Conference on Formal Methods in Computer-Aided Design 2017. Formal Methods in System Design, 57(3), 303–304. https://doi.org/10.1007/s10703-020-00357-x
  • Extracting safe thread schedules from incomplete model checking results / Metzler, P., Suri, N., & Weissenbacher, G. (2020). Extracting safe thread schedules from incomplete model checking results. International Journal on Software Tools for Technology Transfer, 22(5), 565–581. https://doi.org/10.1007/s10009-020-00575-y
  • ProbInG: Distribution Recovery for Invariant Generation of Probabilistic Programs / Bartocci, E., Kovacs, L., & Bura, E. (2020). ProbInG: Distribution Recovery for Invariant Generation of Probabilistic Programs. Vienna Science, Research and Technology Fund - ProbInG, online, Austria. http://hdl.handle.net/20.500.12708/123229
  • Beyond Symbolic Heaps: Deciding Separation Logic With Inductive Definitions / Pagel, J., & Zuleger, F. (2020). Beyond Symbolic Heaps: Deciding Separation Logic With Inductive Definitions. In EPiC Series in Computing. EasyChair EPiC Series in Computing. https://doi.org/10.29007/vkmj
  • Proceedings of the 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-23) / Albert, E., & Kovacs, L. (Eds.). (2020). Proceedings of the 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-23). EasyChair EPiC Series in Computing. http://hdl.handle.net/20.500.12708/24792
  • Proceedings of the 31st International Conference on Concurrency Theory (CONCUR) / Konnov, I., & Kovacs, L. (Eds.). (2020). Proceedings of the 31st International Conference on Concurrency Theory (CONCUR). Dagstuhl Publishing LIPICS. http://hdl.handle.net/20.500.12708/24793

2019

  • Pebble-Intervals Automata and FO2 with Two Orders (Extended Version) / Labai, N., Kotek, T., Ortiz, M., & Veith, H. (2019). Pebble-Intervals Automata and FO2 with Two Orders (Extended Version). arXiv. https://doi.org/10.48550/arXiv.1912.00171
    Projects: KtoAPP (2018–2025) / OMEGA (2017–2022)
  • 60 Shades of Grey in Vampire / Kovacs, L. (2019). 60 Shades of Grey in Vampire. ANDREI-60: Automating New-Era Deductive Reasoning Event in Iberia, Tbilisi, Georgia. http://hdl.handle.net/20.500.12708/86990
  • Trace Reasoning for Formal Verification using the First-Order Superposition Calculus / Georgiou, P., Gleiss, B., Kovacs, L., & Maffei, M. (2019). Trace Reasoning for Formal Verification using the First-Order Superposition Calculus. FMCAD 2019 Student Forum, San Jose, United States of America (the). http://hdl.handle.net/20.500.12708/86988
  • Interactive Visualization of Saturation Attempts in Vampire / Gleiss, B., Kovács, L., & Schnedlitz, L. (2019). Interactive Visualization of Saturation Attempts in Vampire. In W. Ahrendt & S. Lizeth (Eds.), Integrated Formal Methods : 15th International Conference, IFM 2019, Bergen, Norway, December 2–6, 2019, Proceedings (pp. 504–513). Lecture Notes in Computer Science, Springer. https://doi.org/10.1007/978-3-030-34968-4_28
  • Verifying Relational Properties using Trace Logic / Barthe, G., Eilers, R., Georgiou, P., Gleiss, B., Kovacs, L., & Maffei, M. (2019). Verifying Relational Properties using Trace Logic. In B. Clark & J. Yang (Eds.), 2019 Formal Methods in Computer Aided Design (FMCAD). IEEE. https://doi.org/10.23919/fmcad.2019.8894277
  • Extracting Safe Thread Schedules from Incomplete Model Checking Results / Metzler, P., Suri, N., & Weissenbacher, G. (2019). Extracting Safe Thread Schedules from Incomplete Model Checking Results. In Model Checking Software (pp. 153–171). LNCS, Springer. https://doi.org/10.1007/978-3-030-30923-7_9
  • Model-Based Diagnosis with Multiple Observations / Ignatiev, A., Morgado, A., Marques-Silva, J., & Weissenbacher, G. (2019). Model-Based Diagnosis with Multiple Observations. In Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence. IJCAI 2019 - 28th International Joint Conference on Artificial Intelligence, Macao, Macao. https://doi.org/10.24963/ijcai.2019/155
  • Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops / Bartocci, E., Kovacs, L., & Stankovic, M. (2019). Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops. In Y.-F. Chen, C.-H. Cheng, & J. Esparza (Eds.), Automated Technology for Verification and Analysis (pp. 255–276). Springer. https://doi.org/10.1007/978-3-030-31784-3_15
  • Automatic Analysis for Prob-Solvable Loops / Stankovic, M. (2019). Automatic Analysis for Prob-Solvable Loops. 13th Alpine Verification Meeting (AVM), Brno, Czechia. http://hdl.handle.net/20.500.12708/87000
  • Formal Methods in the Digital World (in Hungarian) / Kovacs, L. (2019). Formal Methods in the Digital World (in Hungarian). JegKepzes Series of Presentations- Hungarian Scientists from the Bartok Bela Highschool, Timisoara, Romania. http://hdl.handle.net/20.500.12708/86998
  • First-Order Interpolation / Kovacs, L. (2019). First-Order Interpolation. PhD Research Seminar in Logic and Computation, Faculty of Informatics, West University of Timisoara, Timisoara, Romania. http://hdl.handle.net/20.500.12708/86997
  • Symbolic Computation and Automated Reasoning for Program Analysis / Kovacs, L. (2019). Symbolic Computation and Automated Reasoning for Program Analysis. 23rd IEEE International Conference on Intelligent Engineering Systems (INES) 2019, Gödöllõ, Hungary. http://hdl.handle.net/20.500.12708/86996
  • First Order Interpolation / Kovacs, L. (2019). First Order Interpolation. SAT/SMT/AR Summer School 2019, Lisbon, Portugal. http://hdl.handle.net/20.500.12708/86994
  • Forward Subsumption Demodulation - Fast Conditional Rewriting in Vampire / Gleiss, B., Kovacs, L., & Rath, J. (2019). Forward Subsumption Demodulation - Fast Conditional Rewriting in Vampire. Vampire 2019 - The Sixth Vampire Workshop, Lisbon, Portugal. http://hdl.handle.net/20.500.12708/86993
  • Subsumption Demodulation in First-Order Theorem Proving / Rath, J. (2019). Subsumption Demodulation in First-Order Theorem Proving. First International Workshop on Proof Theory for Automated Deduction, Automated Deduction for Proof Theory, Funchal, Portugal. http://hdl.handle.net/20.500.12708/86992
  • Verifying Relational Properties using Trace Logic / Kovacs, L. (2019). Verifying Relational Properties using Trace Logic. First International Workshop on Proof Theory for Automated Deduction, Automated Deduction for Proof Theory, Funchal, Portugal. http://hdl.handle.net/20.500.12708/86991
  • Symbol Elimination and Vampire / Kovacs, L. (2019). Symbol Elimination and Vampire. Dagstuhl Seminar 19062 - Bringing CP, SAT and SMT together: Next Challenges in Constraint Solving, Schloss Dagstuhl, Germany. http://hdl.handle.net/20.500.12708/86989
  • Mutation Testing with Hyperproperties / Fellner, A., Befrouei, M. T., & Weissenbacher, G. (2019). Mutation Testing with Hyperproperties. In Software Engineering and Formal Methods (pp. 203–221). https://doi.org/10.1007/978-3-030-30446-1_11
  • Verification of Randomized Consensus Algorithms Under Round-Rigid Adversaries / Bertrand, N., Konnov, I., Lazić, M., & Widder, J. (2019). Verification of Randomized Consensus Algorithms Under Round-Rigid Adversaries. In W. Fokkink & R. van Glabbeek (Eds.), 30th International Conference on Concurrency Theory (pp. 33:1-33:15). Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany. https://doi.org/10.4230/LIPIcs.CONCUR.2019.33
  • Verifying Safety of Synchronous Fault-Tolerant Algorithms by Bounded Model Checking / Stoilkovska, I., Konnov, I., Widder, J., & Zuleger, F. (2019). Verifying Safety of Synchronous Fault-Tolerant Algorithms by Bounded Model Checking. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems (pp. 357–374). Springer. http://hdl.handle.net/20.500.12708/56804
  • Probabilistic Strategy Logic / Aminof, B., Kwiatkowska, M., Maubert, B., Murano, A., & Rubin, S. (2019). Probabilistic Strategy Logic. In 28th International Joint Conference on Artificial Intelligence (pp. 32–38). International Joint Conferences on Artificial Intelligence. http://hdl.handle.net/20.500.12708/57510
  • Planning under LTL Environment Specifications / Aminof, B., De Giacomo, G., Murano, A., & Rubin, S. (2019). Planning under LTL Environment Specifications. In 29th International Conference on Automated Planning and Scheduling (pp. 31–39). AAAI Press. http://hdl.handle.net/20.500.12708/57528
  • Removing apparent singularities of linear difference systems / Barkatou, M. A., & Jaroschek, M. (2019). Removing apparent singularities of linear difference systems. Journal of Symbolic Computation, 102, 86–107. https://doi.org/10.1016/j.jsc.2019.10.010
  • Model-based, Mutation-driven Test-case Generation Via Heuristic-guided Branching Search / Fellner, A., Krenn, W., Schlick, R., Tarrach, T., & Weissenbacher, G. (2019). Model-based, Mutation-driven Test-case Generation Via Heuristic-guided Branching Search. ACM Transactions on Embedded Computing Systems, 18(1), 1–28. https://doi.org/10.1145/3289256
  • Foreword - Formalization of geometry, automated and interactive geometric reasoning / Schreck, P., Ida, T., & Kovacs, L. (2019). Foreword - Formalization of geometry, automated and interactive geometric reasoning. Annals of Mathematics and Artificial Intelligence, 85(2–4), 71–72. https://doi.org/10.1007/s10472-019-9617-2
  • Foreword / Davenport, J. H., Kovacs, L., & Zaharie, D. (2019). Foreword. Mathematics in Computer Science, 13(4), 459–460. https://doi.org/10.1007/s11786-019-00411-w
  • APRe, Vampire, Welcome in Vienna! / Kovacs, L. (2019). APRe, Vampire, Welcome in Vienna! APRe 2019 Workshop, TU Wien, TU Wien, Vienna, Austria. http://hdl.handle.net/20.500.12708/86999
  • Interpolation in the Grey Area of Proofs / Kovacs, L. (2019). Interpolation in the Grey Area of Proofs. Helmut Veith Memorial Workshop 2019, Turracher Höhe, Austria. http://hdl.handle.net/20.500.12708/86995
  • SL-COMP: Competition of Solvers for Separation Logic / Sighireanu, M., Pagel, J., Matheja, C., Noll, T., & Zuleger, F. (2019). SL-COMP: Competition of Solvers for Separation Logic. In 25th International Conference, TACAS 2019 (pp. 116–132). Springer. http://hdl.handle.net/20.500.12708/57483
  • Effective Entailment Checking for Separation Logic with Inductive Definitions / Pagel, J., Matheja, C., & Zuleger, F. (2019). Effective Entailment Checking for Separation Logic with Inductive Definitions. In 25th International Conference, TACAS 2019 (pp. 319–336). Springer. http://hdl.handle.net/20.500.12708/57482
  • Communication-Closed Asynchronous Protocols / Damian, A., Drăgoi, C., Militaru, A., & Widder, J. (2019). Communication-Closed Asynchronous Protocols. In Computer Aided Verification (pp. 344–363). Springer. https://doi.org/10.1007/978-3-030-25543-5_20

2018

  • ByMC: Byzantine Model Checker / Konnov, I., & Widder, J. (2018). ByMC: Byzantine Model Checker. In T. Margaria & B. Steffen (Eds.), Leveraging Applications of Formal Methods, Verification and Validation. Distributed Systems. ISoLA 2018, Proceedings, Part III (pp. 327–342). Springer. https://doi.org/10.1007/978-3-030-03424-5_22
  • Automated clustering and program repair for introductory programming assignments / Radicek, I., Gulwani, S., & Zuleger, F. (2018). Automated clustering and program repair for introductory programming assignments. In Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation. Conference on Programming Language Design and Implementation (PLDI), Ottawa, Canada. ACM. https://doi.org/10.1145/3192366.3192387
  • Loop Analysis by Quantification over Iterations / Gleiss, B., Kovács, L., & Robillard, S. (2018). Loop Analysis by Quantification over Iterations. In G. Barthe, G. Sutcliffe, & M. Veanes (Eds.), EPiC Series in Computing. EasyChair EPiC Series in Computing. https://doi.org/10.29007/269p
  • Rely-Guarantee Reasoning for Automated Bound Analysis of Lock-Free Algorithms / Pani, T., Weissenbacher, G., & Zuleger, F. (2018). Rely-Guarantee Reasoning for Automated Bound Analysis of Lock-Free Algorithms. In 2018 Formal Methods in Computer Aided Design (FMCAD). International Conference on Formal Methods in Computer-Aided Design (FMCAD), Portland, United States of America (the). FMCAD Inc. https://doi.org/10.23919/fmcad.2018.8603020
  • Communication-Closed Layers as Paradigm for Distributed Systems: A Manifesto / Dragoi, C., Lazić, M., & Widder, J. (2018). Communication-Closed Layers as Paradigm for Distributed Systems: A Manifesto. In Proceedings of the International Scientific Conference - Sinteza 2018. Sinteza 2018 International Scientific Conference on Information Technology and Data Related Research, Belgrad, Serbia. Singidunum University. https://doi.org/10.15308/sinteza-2018-131-138
  • Towards Smarter MACE-style Model Finders / Janota, M., & Suda, M. (2018). Towards Smarter MACE-style Model Finders. In EPiC Series in Computing. 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), Awassa, Ethiopia. EasyChair EPiC Series in Computing. https://doi.org/10.29007/w42s
  • Using Loop Bound Analysis For Invariant Generation / Cadek, P., Danninger, C., Sinn, M., & Zuleger, F. (2018). Using Loop Bound Analysis For Invariant Generation. In 2018 Formal Methods in Computer Aided Design (FMCAD). International Conference on Formal Methods in Computer-Aided Design (FMCAD), Portland, United States of America (the). FMCAD Inc. https://doi.org/10.23919/fmcad.2018.8603005
  • Monadic refinements for relational cost analysis / Radiček, I., Barthe, G., Gaboardi, M., Garg, D., & Zuleger, F. (2018). Monadic refinements for relational cost analysis. In Proceedings of the ACM on Programming Languages (pp. 1–32). ACM Digital Library. https://doi.org/10.1145/3158124
  • Desingularization of First Order Linear Difference Systems with Rational Function Coefficients / Barkatou, M. A., & Jaroschek, M. (2018). Desingularization of First Order Linear Difference Systems with Rational Function Coefficients. In M. Kauers (Ed.), Proceedings of the 2018 ACM International Symposium on Symbolic and Algebraic Computation. https://doi.org/10.1145/3208976.3208989
  • A Separation Logic with Data: Small Models and Automation / Pagel, J., Jovanovic, D., & Weissenbacher, G. (2018). A Separation Logic with Data: Small Models and Automation. In Automated Reasoning (pp. 455–471). LNCS. https://doi.org/10.1007/978-3-319-94205-6_30
  • Unification with Abstraction and Theory Instantiation in Saturation-Based Reasoning / Reger, G., Suda, M., & Voronkov, A. (2018). Unification with Abstraction and Theory Instantiation in Saturation-Based Reasoning. In D. Beyer & M. Huisman (Eds.), Proceedings of the 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) (pp. 3–22). LNCS. http://hdl.handle.net/20.500.12708/57680
  • Reachability in Parameterized Systems: All Flavors of Threshold Automata / Kukovec, J., Konnov, I., & Widder, J. (2018). Reachability in Parameterized Systems: All Flavors of Threshold Automata. In S. Schewe & L. Zhang (Eds.), 29th International Conference on Concurrency Theory (CONCUR 2018) (pp. 19:1-19:17). Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH, Dagstuhl Publishing. https://doi.org/10.4230/LIPIcs.CONCUR.2018.19
  • Efficient Algorithms for Asymptotic Bounds on Termination Time in VASS / Brázdil, T., Chatterjee, K., Kučera, A., Novotný, P., Velan, D., & Zuleger, F. (2018). Efficient Algorithms for Asymptotic Bounds on Termination Time in VASS. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science. Symposium on Logic in Computer Science (LICS), Edinburgh, United Kingdom of Great Britain and Northern Ireland (the). ACM. https://doi.org/10.1145/3209108.3209191
  • Inductive Termination Proofs with Transition Invariants and Their Relationship to the Size-Change Abstraction / Zuleger, F. (2018). Inductive Termination Proofs with Transition Invariants and Their Relationship to the Size-Change Abstraction. In Static Analysis (pp. 423–444). Springer. https://doi.org/10.1007/978-3-319-99725-4_25
  • Synthesis under Assumptions / Aminof, B., De Giacomo, G., Murano, A., & Rubin, S. (2018). Synthesis under Assumptions. In Principles of Knowledge Representation and Reasoning: Proceedings of the Sixteenth International Conference, KR 2018, Tempe, Arizona, 30 October - 2 November 2018 (pp. 615–616). AAAI Press. http://hdl.handle.net/20.500.12708/57751
  • Extended Resolution Simulates DRAT / Kiesl, B., Rebola Pardo, A., & Heule, M. (2018). Extended Resolution Simulates DRAT. In Automated Reasoning (pp. 516–531). LNCS. https://doi.org/10.1007/978-3-319-94205-6_34
  • Local Soundness for QBF Calculi / Suda, M., & Gleiss, B. (2018). Local Soundness for QBF Calculi. In O. Beyersdorff & C. M. Wintersteiger (Eds.), Theory and Applications of Satisfiability Testing – SAT 2018 (pp. 217–234). LNCS. https://doi.org/10.1007/978-3-319-94144-8_14
  • Automated Reasoning for Systems Engineering / Kovacs, L. (2018). Automated Reasoning for Systems Engineering. In Foundations of Information and Knowledge Systems (FOIKS) 2018 (p. 1). LNCS. http://hdl.handle.net/20.500.12708/57375
  • A FOOLish Encoding of the Next State Relations of Imperative Programs / Kotelnikov, E., Kovács, L., & Voronkov, A. (2018). A FOOLish Encoding of the Next State Relations of Imperative Programs. In Automated Reasoning (pp. 405–421). LNCS. https://doi.org/10.1007/978-3-319-94205-6_27
  • First-Order Interpolation / Kovacs, L. (2018). First-Order Interpolation. SAT/SMT/AR Summer School 2018, Manchester, United Kingdom of Great Britain and Northern Ireland (the). http://hdl.handle.net/20.500.12708/86712
  • Automated Reasoning for Systems Engineering / Kovacs, L. (2018). Automated Reasoning for Systems Engineering. 2018 IEEE International Conference on Future IoT Technologies (Future IoT 2018), Eger, Hungary. http://hdl.handle.net/20.500.12708/86713
  • First-Order Interpolation in the Grey Area of Proofs / Kovacs, L. (2018). First-Order Interpolation in the Grey Area of Proofs. Summer School on Syntax meets Semantics - Methods, Interactions, and Connections in Substructural Logics (SYSMICS), Les Diablerets, Switzerland. http://hdl.handle.net/20.500.12708/86840
  • Symbol Elimination for Program Analysis / Kovacs, L. (2018). Symbol Elimination for Program Analysis. Highlights of Logic, Games and Automata, Paris, France. http://hdl.handle.net/20.500.12708/86841
  • Symbol Elimination in Program Analysis / Kovacs, L. (2018). Symbol Elimination in Program Analysis. 2nd Facebook Testing and Veri cation Symposium (FaceTAV), London, United Kingdom of Great Britain and Northern Ireland (the). http://hdl.handle.net/20.500.12708/86842
  • Local proofs and AVATAR / Reger, G., & Suda, M. (2018). Local proofs and AVATAR. In L. Kovacs & A. Voronkov (Eds.), EPiC Series in Computing. EasyChair EPiC Series in Computing. https://doi.org/10.29007/qgdk
  • First-Order Theorem Proving in Rigorous Systems Engineering / Kovacs, L., & Voronkov, A. (2018). First-Order Theorem Proving in Rigorous Systems Engineering. RiSE/SHiNE Winter School 2018, Wien, Austria. http://hdl.handle.net/20.500.12708/86711
  • Vampire 2017. Proceedings of the 4th Vampire Workshop / Kovacs, L., & Voronkov, A. (Eds.). (2018). Vampire 2017. Proceedings of the 4th Vampire Workshop. EasyChair EPiC Series in Computing. http://hdl.handle.net/20.500.12708/24544
  • Invariant Generation for Multi-Path Loops with Polynomial Assignments / Humenberger, A., Jaroschek, M., & Kovacs, L. (2018). Invariant Generation for Multi-Path Loops with Polynomial Assignments. In I. Dillig & J. Palsberg (Eds.), Verification, Model Checking, and Abstract Interpretation (pp. 226–246). Springer. https://doi.org/10.1007/978-3-319-73721-8_11
  • Parameterized Model Checking of Synchronous Distributed Algorithms by Abstraction / Aminof, B., Rubin, S., Stoilkovska, I., Widder, J., & Zuleger, F. (2018). Parameterized Model Checking of Synchronous Distributed Algorithms by Abstraction. In I. Dillig & J. Palsberg (Eds.), Verification, Model Checking, and Abstract Interpretation : 19th International Conference, VMCAI 2018, Los Angeles, CA, USA, January 7-9, 2018, Proceedings. Cham. https://doi.org/10.1007/978-3-319-73721-8_1
    Download: PDF (538 KB)
  • Parameterized model checking of rendezvous systems / Aminof, B., Kotek, T., Rubin, S., Spegni, F., & Veith, H. (2018). Parameterized model checking of rendezvous systems. Distributed Computing, 31(3), 187–222. https://doi.org/10.1007/s00446-017-0302-6
  • Aligator.jl – A Julia Package for Loop Invariant Generation / Humenberger, A., Jaroschek, M., & Kovács, L. (2018). Aligator.jl – A Julia Package for Loop Invariant Generation. In F. Rabe (Ed.), Intelligent Computer Mathematics : 11th International Conference, CICM 2018, Hagenberg, Austria, August 13-17, 2018, Proceedings (pp. 111–117). LNCS. https://doi.org/10.1007/978-3-319-96812-4_10
  • Randomized testing of distributed systems with probabilistic guarantees / Ozkan, B. K., Majumdar, R., Niksic, F., Befrouei, M. T., & Weissenbacher, G. (2018). Randomized testing of distributed systems with probabilistic guarantees. Proceedings of the ACM on Programming Languages, 2(OOPSLA), 1–28. https://doi.org/10.1145/3276530
  • A Theory of Satisfiability-Preserving Proofs in SAT Solving / Rebola Pardo, A., & Suda, M. (2018). A Theory of Satisfiability-Preserving Proofs in SAT Solving. In EPiC Series in Computing. International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), Montevideo, Uruguay, Austria. EasyChair EPiC Series in Computing. https://doi.org/10.29007/tc7q
  • Reinterpreting Dependency Schemes: Soundness Meets Incompleteness in DQBF / Beyersdorff, O., Blinkhorn, J., Chew, L., Schmidt, R., & Suda, M. (2018). Reinterpreting Dependency Schemes: Soundness Meets Incompleteness in DQBF. Journal of Automated Reasoning, 63(3), 597–623. https://doi.org/10.1007/s10817-018-9482-4
  • Automated Reasoning for Rigorous Systems Engineering / Kovacs, L. (2018). Automated Reasoning for Rigorous Systems Engineering. RiSE/SHINE Media Seminar 2018, Vienna, Austria. http://hdl.handle.net/20.500.12708/86714
  • Foundations and Tools for the Static Analysis of Ethereum Smart Contracts / Gishchenko, I., Maffei, M., & Schneidewind, C. (2018). Foundations and Tools for the Static Analysis of Ethereum Smart Contracts. In G. Weissenbacher & H. Chockler (Eds.), Computer Aided Verification (pp. 51–78). Springer Open. https://doi.org/10.1007/978-3-319-96145-3_4
  • Incremental Solving with Vampire / Reger, G., & Suda, M. (2018). Incremental Solving with Vampire. In EPiC Series in Computing. EasyChair, Austria. EasyChair EPiC Series in Computing. https://doi.org/10.29007/6sjl
  • Computer Aided Verification / Computer Aided Verification. (2018). In H. Chockler & G. Weissenbacher (Eds.), Lecture Notes in Computer Science. Springer. https://doi.org/10.1007/978-3-319-96142-2
  • Computer Aided Verification / Computer Aided Verification. (2018). In H. Chockler & G. Weissenbacher (Eds.), Lecture Notes in Computer Science. Springer. https://doi.org/10.1007/978-3-319-96145-3

2017

  • On the Automated Verification of Web Applications with Embedded SQL / Shachar, I., Kotek, T., Rinetzky, N., Sagiv, M., Tamir, O., Veith, H., & Zuleger, F. (2017). On the Automated Verification of Web Applications with Embedded SQL. In 20th International Conference on Database Theory, ICDT 2017 (pp. 1–18). http://hdl.handle.net/20.500.12708/57152
  • Set of Support for Theory Reasoning / Reger, G., & Suda, M. (2017). Set of Support for Theory Reasoning. In IWIL@LPAR 2017 Workshop and LPAR-21 Short Presentations, Maun, Botswana, May 7-12, 2017 (pp. 124–134). EasyChair Kalpa Publications in Computing. http://hdl.handle.net/20.500.12708/57149
  • Automated Invention of Strategies and Term Orderings for Vampire / Jakubuv, J., Suda, M., & Urban, J. (2017). Automated Invention of Strategies and Term Orderings for Vampire. In GCAI 2017. 3rd Global Conference on Artificial Intelligence (pp. 121–133). EasyChair EPiC Series in Computing. http://hdl.handle.net/20.500.12708/57144
  • Dynamic Reductions for Model Checking Concurrent Software / Günther, H., Laarman, A., Sokolova, A., & Weissenbacher, G. (2017). Dynamic Reductions for Model Checking Concurrent Software. In Verification, Model Checking, and Abstract Interpretation 18th International Conference, VMCAI 2017, Paris, France, January 15–17, 2017, Proceedings (pp. 246–265). Springer. https://doi.org/10.1007/978-3-319-52234-0_14
  • Recent Improvements of Theory Reasoning in Vampire / Reger, G., Suda, M., & Voronkov, A. (2017). Recent Improvements of Theory Reasoning in Vampire. IWIL 2017 - 12th International Workshop on the Implementation of Logics, Maun, Botswana. http://hdl.handle.net/20.500.12708/86627
  • Symbol Elimination for Program Analysis / Kovacs, L. (2017). Symbol Elimination for Program Analysis. ETH Workshop on Software Correctness and Reliability, Zürich, Switzerland. http://hdl.handle.net/20.500.12708/86690
  • Constructive Satisfiability Procedure for ALCP(Z) (Preliminary Report) / Labai, N., Homola, M., & Ortiz de la Fuente, M. M. (2017). Constructive Satisfiability Procedure for ALCP(Z) (Preliminary Report). In A. Artale, B. Glimm, & R. Kontchakov (Eds.), Proceedings of the 30th International Workshop on Description Logics (pp. 1–13). CEUR Workshop Proceedings. http://hdl.handle.net/20.500.12708/55478
  • A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms / Konnov, I., Lazić, M., Veith, H., & Widder, J. (2017). A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages. 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), Paris, France. ACM. https://doi.org/10.1145/3009837.3009860
  • Coming to Terms with Quantified Reasoning / Kovacs, L., Robillard, S., & Voronkov, A. (2017). Coming to Terms with Quantified Reasoning. In G. Castagna & A. D. Gordon (Eds.), Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL). ACM. https://doi.org/10.1145/3009837
  • Deviation in Belief Change on Fragments of Propositional Logic / Haret, A., & Woltran, S. (2017). Deviation in Belief Change on Fragments of Propositional Logic. In C. Beierle, G. Kern-Isberner, M. Ragni, & F. Stolzenburg (Eds.), Proceedings of the 6th Workshop on Dynamics of Knowledge and Belief (DKB-2017) and the 5th Workshop KI & Kognition (KIK-2017) (p. 13). CEUR Workshop Proceedings. http://hdl.handle.net/20.500.12708/55459
    Project: Belief Change (2013–2017)
  • Testing a Saturation-Based Theorem Prover: Experiences and Challenges / Reger, G., Suda, M., & Voronkov, A. (2017). Testing a Saturation-Based Theorem Prover: Experiences and Challenges. In Tests and Proofs (pp. 152–161). Springer. https://doi.org/10.1007/978-3-319-61467-0_10
  • Checkable Proofs for First-Order Theorem Proving / Reger, G., & Suda, M. (2017). Checkable Proofs for First-Order Theorem Proving. In ARCADE 2017. 1st International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements (pp. 55–63). EasyChair EPiC Series in Computing. http://hdl.handle.net/20.500.12708/57143
  • Splitting Proofs for Interpolation / Gleiss, B., Kovács, L., & Suda, M. (2017). Splitting Proofs for Interpolation. In Automated Deduction – CADE 26 (pp. 291–309). Springer. https://doi.org/10.1007/978-3-319-63046-5_18
  • Automata and Program Analysis / Daviaud, L., Colcombet, T., & Zuleger, F. (2017). Automata and Program Analysis. In Fundamentals of Computation Theory - 21st International Symposium, FCT 2017 (pp. 3–10). http://hdl.handle.net/20.500.12708/57151
  • Logic-Based Merging in Fragments of Classical Logic with Inputs from Social Choice Theory / Haret, A. (2017). Logic-Based Merging in Fragments of Classical Logic with Inputs from Social Choice Theory. In J. Rothe (Ed.), Algorithmic Decision Theory (pp. 374–378). Lecture Notes in Computer Science. https://doi.org/10.1007/978-3-319-67504-6_30
  • Model-based, mutation-driven test case generation via heuristic-guided branching search / Fellner, A., Krenn, W., Schlick, R., Tarrach, T., & Weissenbacher, G. (2017). Model-based, mutation-driven test case generation via heuristic-guided branching search. In Proceedings of the 15th ACM-IEEE International Conference on Formal Methods and Models for System Design. MEMOCODE 2017: the 15th ACM-IEEE International Conference on Formal Methods and Models for System Design, Wien, Austria. ACM. https://doi.org/10.1145/3127041.3127049
  • Automated Generation of Non-Linear Loop Invariants Utilizing Hypergeometric Sequences / Humenberger, A., Jaroschek, M., & Kovács, L. (2017). Automated Generation of Non-Linear Loop Invariants Utilizing Hypergeometric Sequences. In Proceedings of the 2017 ACM on International Symposium on Symbolic and Algebraic Computation. International Symposium on Symbolic and Algebraic Computation (ISSAC), Kaiserslautern, Germany. ACM. https://doi.org/10.1145/3087604.3087623
  • lpopt: A Rule Optimization Tool for Answer Set Programming / Morak, M., Bichler, M., & Woltran, S. (2017). lpopt: A Rule Optimization Tool for Answer Set Programming. In M. Hermenegildo & P. Lopez-Garcia (Eds.), Logic-Based Program Synthesis and Transformation (pp. 114–130). Lecture Notes in Computer Science. https://doi.org/10.1007/978-3-319-63139-4_7
    Projects: D-Flat (2013–2017) / START (2014–2022)
  • Synthesis of Distributed Algorithms with Parameterized Threshold Guards / Lazić, M., Konnov, I., Widder, J., & Bloem, R. (2017). Synthesis of Distributed Algorithms with Parameterized Threshold Guards. In J. Aspnes, A. Bessani, P. Felber, & J. Leitao (Eds.), 21st International Conference on Principles of Distributed Systems (OPODIS 2017) (pp. 32:1-32:20). LIPIcs-Leibniz International Proceedings in Informatics. https://doi.org/10.4230/LIPIcs.OPODIS.2017.32
  • A Supervisory Control Algorithm Based on Property-Directed Reachability / Claessen, K., Kilhamn, J., Kovács, L., & Lennartson, B. (2017). A Supervisory Control Algorithm Based on Property-Directed Reachability. In O. Strichman & R. Tzoref-Brill (Eds.), Hardware and Software: Verification and Testing (pp. 115–130). Lecture Notes in Computer Science / Springer. https://doi.org/10.1007/978-3-319-70389-3_8
  • Instantiation and Pretending to be an SMT Solver with Vampire / Reger, G., Suda, M., & Voronkov, A. (2017). Instantiation and Pretending to be an SMT Solver with Vampire. SMT 2017 - 15th International Workshop on Satisfiability Modulo Theories, Heidelberg, Germany. http://hdl.handle.net/20.500.12708/86623
  • Incremental Solving with Vampire / Reger, G., & Suda, M. (2017). Incremental Solving with Vampire. Fourth Vampire Workshop - VAMPIRE 2017, Göteborg, Sweden. http://hdl.handle.net/20.500.12708/86625
  • Local proofs and AVATAR / Reger, G., & Suda, M. (2017). Local proofs and AVATAR. Fourth Vampire Workshop - VAMPIRE 2017, Göteborg, Sweden. http://hdl.handle.net/20.500.12708/86626
  • Interpolation-based Model Checking and IC3 / Weissenbacher, G. (2017). Interpolation-based Model Checking and IC3. Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science, Znaim, Czechia. http://hdl.handle.net/20.500.12708/86685
  • Algebraic Reasoning for Program Analysis / Kovacs, L. (2017). Algebraic Reasoning for Program Analysis. 33rd Conference on the Mathematical Foundations of Programming Semantics (MFPS), Laibach, Slovenia. http://hdl.handle.net/20.500.12708/86689
  • Polynomial Invariant Generation for Multi-Path Loops / Humenberger, A., Jaroschek, M., & Kovacs, L. (2017). Polynomial Invariant Generation for Multi-Path Loops. Second International Workshop on Satisfiability Checking and Symbolic Computation (SC2), Kaiserslautern, Germany. http://hdl.handle.net/20.500.12708/86847
  • Global Subsumption Revisited (Briefly) / Reger, G., & Suda, M. (2017). Global Subsumption Revisited (Briefly). In L. Kovacs & A. Voronkov (Eds.), Vampire@IJCAR 2016. Proceedings of the 3rd Vampire Workshop (pp. 61–73). http://hdl.handle.net/20.500.12708/57133
  • First-Order Interpolation and Interpolating Proof Systems / Kovacs, L., & Voronkov, A. (2017). First-Order Interpolation and Interpolating Proof Systems. In LPAR-21. 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning (pp. 49–64). EasyChair EPiC Series in Computing. http://hdl.handle.net/20.500.12708/57308
  • Towards a Semantics of Unsatisfiability Proofs with Inprocessing / Philipp, T., & Rebola Pardo, A. (2017). Towards a Semantics of Unsatisfiability Proofs with Inprocessing. In Logic Programming and Automated Reasoning (LPAR) (pp. 65–84). EasyChair EPiC Series in Computing. http://hdl.handle.net/20.500.12708/57273
    Project: BITVECTOR (2016–2020)
  • Fuzzing and Verifying RAT Refutations with Deletion Information / Forkel, W., Philipp, T., Rebola Pardo, A., & Werner, E. (2017). Fuzzing and Verifying RAT Refutations with Deletion Information. In Florida Artificial Intelligence Research Society Conference (pp. 190–193). AAAI Press. http://hdl.handle.net/20.500.12708/56283
    Project: BITVECTOR (2016–2020)
  • Para^2: Parameterized Path Reduction, Acceleration, and SMT for Reachability in Threshold-Guarded Distributed Algorithms / Konnov, I., Lazić, M., Veith, H., & Widder, J. (2017). Para^2: Parameterized Path Reduction, Acceleration, and SMT for Reachability in Threshold-Guarded Distributed Algorithms. Formal Methods in System Design, 51(2), 270–307. https://doi.org/10.1007/s10703-017-0297-4
  • Empirical software metrics for benchmarking of verification tools / Demyanova, Y., Pani, T., Veith, H., & Zuleger, F. (2017). Empirical software metrics for benchmarking of verification tools. Formal Methods in System Design, 50(2–3), 289–316. https://doi.org/10.1007/s10703-016-0264-5
  • On the completeness of bounded model checking for threshold-based distributed algorithms: Reachability / Konnov, I., Veith, H., & Widder, J. (2017). On the completeness of bounded model checking for threshold-based distributed algorithms: Reachability. Information and Computation, 252, 95–109. https://doi.org/10.1016/j.ic.2016.03.006
  • Preface of the Special Issue in Memoriam Helmut Veith / Gottlob, G., Henzinger, T. A., & Weissenbacher, G. (2017). Preface of the Special Issue in Memoriam Helmut Veith. Formal Methods in System Design, 51(2), 267–269. https://doi.org/10.1007/s10703-017-0307-6
  • Measuring progress to predict success: Can a good proof strategy be evolved? / Reger, G., & Suda, M. (2017). Measuring progress to predict success: Can a good proof strategy be evolved? AITP 2017 - The Second Conference on Artificial Intelligence and Theorem Proving, Obergurgl, Austria. http://hdl.handle.net/20.500.12708/86616
  • Proceedings of Formal Methods in Computer Aided Design, FMCAD 2017 / Stewart, D., & Weissenbacher, G. (Eds.). (2017). Proceedings of Formal Methods in Computer Aided Design, FMCAD 2017. FMCAD Inc. https://doi.org/10.15781/T2JS9HQ7C
  • CICM 2016 Doctoral Program / Suda, M. (2017). CICM 2016 Doctoral Program. In Joint Proceedings of the FM4M, MathUI, and ThEdu Workshops, Doctoral Program, and Work in Progress at the Conference on Intelligent Computer Mathematics 2016 co-located with the 9th Conference on Intelligent Computer Mathematics (CICM 2016), Bialystok, Poland, July 25-29, 2016. (p. 1). CEUR-Proceedings. http://hdl.handle.net/20.500.12708/57145

2016

  • Desingularization of First Order Linear Difference Systems with Rational Function Coefficients / Jaroschek, M., & Barkatou, M. (2016). Desingularization of First Order Linear Difference Systems with Rational Function Coefficients. RIMS workshop, Algebraic Statistics and Symbolic Computation, Kyoto, Japan. http://hdl.handle.net/20.500.12708/86472
  • Model Checking of Threshold-based Fault-Tolerant Distributed Algorithms / Lazić, M., Konnov, I., Veith, H., & Widder, J. (2016). Model Checking of Threshold-based Fault-Tolerant Distributed Algorithms. 7th Workshop on Program Semantics, Specification and Verification: Theory and Applications, St. Petersburg, Russian Federation (the). http://hdl.handle.net/20.500.12708/86426
  • Interpolation algorithms and their applications in model checking / Weissenbacher, G. (2016). Interpolation algorithms and their applications in model checking. Automata, Logic and Games, Singapore, Singapore. http://hdl.handle.net/20.500.12708/86305
  • The vampire and the FOOL / Kotelnikov, E., Kovács, L., Reger, G., & Voronkov, A. (2016). The vampire and the FOOL. In J. Avigad & A. Chlipala (Eds.), Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs. ACM. https://doi.org/10.1145/2854065.2854071
  • Distributing Knowledge Into Simple Bases / Haret, A., Mailly, J.-G., & Woltran, S. (2016). Distributing Knowledge Into Simple Bases. In S. Kambhampati (Ed.), Proceedings of the 25th International Joint Conference on Artificial Intelligence (pp. 1109–1115). IJCAI/AAAI Press. http://hdl.handle.net/20.500.12708/56772
  • Merging of Abstract Argumentation Frameworks / Delobelle, J., Haret, A., Konieczny, S., Mailly, J.-G., Rossit, J., & Woltran, S. (2016). Merging of Abstract Argumentation Frameworks. In C. Baral, J. P. Delgrande, & F. Wolter (Eds.), Principles of Knowledge Representation and Reasoning: Proceedings of the 15th International Conference (pp. 33–42). AAAI Press. http://hdl.handle.net/20.500.12708/56766
  • Distributing Knowledge Into Simple Bases / Haret, A., Mailly, J.-G., & Woltran, S. (2016). Distributing Knowledge Into Simple Bases. In G. Kern-Isberner & R. Wassermann (Eds.), Proceedings of the 16th International Workshop on Non-monotonic reasoning (p. 9). http://hdl.handle.net/20.500.12708/56764
  • Error Invariants for Concurrent Traces / Holzer, A., Schwartz-Narbonne, D., Tabaei Befrouei, M., Weissenbacher, G., & Wies, T. (2016). Error Invariants for Concurrent Traces. In FM 2016: Formal Methods (pp. 370–387). Lecture Notes in Computer Science/Springer. https://doi.org/10.1007/978-3-319-48989-6_23
  • Extended Graded Modalities in Strategy Logic / Aminof, B., Malvone, V., Murano, A., & Rubin, S. (2016). Extended Graded Modalities in Strategy Logic. In SR (pp. 1–14). http://hdl.handle.net/20.500.12708/56868
  • Prompt Alternating-Time Epistemic Logics / Aminof, B., Murano, A., Rubin, S., & Zuleger, F. (2016). Prompt Alternating-Time Epistemic Logics. In KR (pp. 258–267). http://hdl.handle.net/20.500.12708/56836
  • Parameterized Systems in BIP: Design and Model Checking / Konnov, I., Kotek, T., Wang, Q., Veith, H., Bliudze, S., & Sifakis, J. (2016). Parameterized Systems in BIP: Design and Model Checking. In J. Desharnais & R. Jagadeesan (Eds.), 27th International Conference on Concurrency Theory (CONCUR 2016) (pp. 30:1-30:16). Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2016.30
  • A Clausal Normal Form Translation for FOOL / Kotelnikov, E., Kovacs, L., Suda, M., & Voronkov, A. (2016). A Clausal Normal Form Translation for FOOL. In GCAI 2016. 2nd Global Conference on Artificial Intelligence (pp. 53–71). EasyChair. http://hdl.handle.net/20.500.12708/56716
  • AVATAR Modulo Theories / Reger, G., Bjørner, N., Suda, M., & Voronkov, A. (2016). AVATAR Modulo Theories. In GCAI 2016. 2nd Global Conference on Artificial Intelligence (pp. 39–52). EasyChair. http://hdl.handle.net/20.500.12708/56715
  • Finding Finite Models in Multi-sorted First-Order Logic / Reger, G., Suda, M., & Voronkov, A. (2016). Finding Finite Models in Multi-sorted First-Order Logic. In Theory and Applications of Satisfiability Testing – SAT 2016 (pp. 323–341). Springer. https://doi.org/10.1007/978-3-319-40970-2_20
  • Lifting QBF Resolution Calculi to DQBF / Beyersdorff, O., Chew, L., Schmidt, R. A., & Suda, M. (2016). Lifting QBF Resolution Calculi to DQBF. In Theory and Applications of Satisfiability Testing – SAT 2016 (pp. 490–499). Springer. https://doi.org/10.1007/978-3-319-40970-2_30
  • New Techniques in Clausal Form Generation / Reger, G., Suda, M., & Voronkov, A. (2016). New Techniques in Clausal Form Generation. In GCAI 2016. 2nd Global Conference on Artificial Intelligence (pp. 11–23). EasyChair. http://hdl.handle.net/20.500.12708/56698
  • Beyond IC Postulates: Classification Criteria for Merging Operators / Haret, A., Pfandler, A., & Woltran, S. (2016). Beyond IC Postulates: Classification Criteria for Merging Operators. In G. A. Kaminka, M. Fox, P. Bouquet, E. Hüllermeier, V. Dignum, F. Dignum, & F. van Harmelen (Eds.), ECAI 2016 - 22nd European Conference on Artificial Intelligence (pp. 372–380). IOS Press. http://hdl.handle.net/20.500.12708/56666
    Project: FAIR (2013–2018)
  • Selecting the Selection / Hoder, K., Reger, G., Suda, M., & Voronkov, A. (2016). Selecting the Selection. In Automated Reasoning (pp. 313–329). Springer. https://doi.org/10.1007/978-3-319-40229-1_22
  • Duality in STRIPS planning / Suda, M. (2016). Duality in STRIPS planning. In 8th Workshop on Heuristics and Search for Domain-independent Planning (HSDIP), London, UK, June 13, 2016, Proceedings (pp. 21–27). http://hdl.handle.net/20.500.12708/56505
  • Graded Strategy Logic: Reasoning about Uniqueness of Nash Equilibria / Aminof, B., Malvone, V., Murano, A., & Rubin, S. (2016). Graded Strategy Logic: Reasoning about Uniqueness of Nash Equilibria. In AAMAS (pp. 698–706). http://hdl.handle.net/20.500.12708/56867
  • Monadic Second Order Finite Satisfiability and Unbounded Tree-Width / Kotek, T., Veith, H., & Zuleger, F. (2016). Monadic Second Order Finite Satisfiability and Unbounded Tree-Width. In CSL (pp. 1–20). http://hdl.handle.net/20.500.12708/56860
  • Automatic Verification of Multi-Agent Systems in Parameterised Grid-Environments / Aminof, B., Murano, A., Rubin, S., & Zuleger, F. (2016). Automatic Verification of Multi-Agent Systems in Parameterised Grid-Environments. In AAMAS (pp. 1190–1199). http://hdl.handle.net/20.500.12708/56859
  • lpopt: A Rule Optimization Tool for Answer Set Programming / Bichler, M., Morak, M., & Woltran, S. (2016). lpopt: A Rule Optimization Tool for Answer Set Programming. In M. Hermenegildo & P. Lopez-Garcia (Eds.), Pre-proceedings of the 26th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2016) (p. 14). http://hdl.handle.net/20.500.12708/56841
    Projects: D-Flat (2013–2017) / START (2014–2022)
  • Revisiting Global Subsumption / Reger, G., & Suda, M. (2016). Revisiting Global Subsumption. The Third Vampire Workshop, VAMPIRE 2016, Coimbra, Portugal. http://hdl.handle.net/20.500.12708/86350
  • Blocked clauses in first-order logic / Biere, A., Kiesl, B., Seidl, M., & Suda, M. (2016). Blocked clauses in first-order logic. The Third Vampire Workshop, VAMPIRE 2016, Coimbra, Portugal. http://hdl.handle.net/20.500.12708/86389
  • First-Order Logic and Blocked Clauses / Kiesl, B., & Suda, M. (2016). First-Order Logic and Blocked Clauses. 4th International Workshop on Quantified Boolean Formulas (QBF 2016), Bordeaux, France. http://hdl.handle.net/20.500.12708/86390
  • New Techniques in Clausal Form Generation / Reger, G., Suda, M., & Voronkov, A. (2016). New Techniques in Clausal Form Generation. Prague Automated Reasoning Seminar, Prag, Czechia. http://hdl.handle.net/20.500.12708/86391
  • The mystery of QBF tautologies / Suda, M. (2016). The mystery of QBF tautologies. Prague Automated Reasoning Seminar, Prag, Czechia. http://hdl.handle.net/20.500.12708/86392
  • Enjoying Research at the Intersection of Math and Computer Science / Kovacs, L. (2016). Enjoying Research at the Intersection of Math and Computer Science. Women in Science Workshop Series (WISE), Gothenburg, Sweden. http://hdl.handle.net/20.500.12708/86439
  • With a Timisoara Background in the Scientific World of Computer Science and / Kovacs, L. (2016). With a Timisoara Background in the Scientific World of Computer Science and. Timisoara Hungarian Science Festival, Timisoara, Romania. http://hdl.handle.net/20.500.12708/86440
  • Desingularization of First Order Linear Difference Systems with Rational Function Coefficients / Barkatou, M., & Jaroschek, M. (2016). Desingularization of First Order Linear Difference Systems with Rational Function Coefficients. 22nd Conference on Applications of Computer Algebra, Kassel, Germany. http://hdl.handle.net/20.500.12708/86470
  • Quantifier Elimination Over The Reals / Jaroschek, M. (2016). Quantifier Elimination Over The Reals. Tutorial on SMT and Polynomial Arithmetic, Gothenburg, Sweden. http://hdl.handle.net/20.500.12708/86471
  • Vienna Verification Tool: IC3 for Parallel Software / Günther, H., Laarman, A., & Weissenbacher, G. (2016). Vienna Verification Tool: IC3 for Parallel Software. In M. Chechik & J.-F. Raskin (Eds.), Tools and Algorithms for the Construction and Analysis of Systems : 22nd International Conference, TACAS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings (pp. 954–957). Springer. https://doi.org/10.1007/978-3-662-49674-9_69
    Download: PDF (173 KB)
  • What You Always Wanted to Know About Model Checking of Fault-Tolerant Distributed Algorithms / Konnov, I., Veith, H., & Widder, J. (2016). What You Always Wanted to Know About Model Checking of Fault-Tolerant Distributed Algorithms. In Perspectives of System Informatics : 10th International Andrei Ershov Informatics Conference, PSI 2015, in Memory of Helmut Veith, Kazan and Innopolis, Russia, August 24-27, 2015, Revised Selected Papers (pp. 6–21). Springer. https://doi.org/10.1007/978-3-319-41579-6_2
    Download: PDF (346 KB)
  • Symbolic Computation and Automated Reasoning for Program Analysis / Kovács, L. (2016). Symbolic Computation and Automated Reasoning for Program Analysis. In E. Abraham & M. Huisman (Eds.), Integrated Formal Methods : 12th International Conference, IFM 2016, Reykjavik, Iceland, June 1-5, 2016, Proceedings (pp. 20–27). Springer / LNCS. https://doi.org/10.1007/978-3-319-33693-0_2
  • Decidability of Parameterized Verification / Bloem, R., Jacobs, S., Khalimov, A., Konnov, I., Rubin, S., Veith, H., & Widder, J. (2016). Decidability of Parameterized Verification. ACM SIGACT News, 47(2), 53–64. https://doi.org/10.1145/2951860.2951873
  • The Power of Non-Ground Rules in Answer Set Programming / BICHLER, M., MORAK, M., & WOLTRAN, S. (2016). The Power of Non-Ground Rules in Answer Set Programming. Theory and Practice of Logic Programming, 16(5–6), 552–569. https://doi.org/10.1017/s1471068416000338
    Projects: D-Flat (2013–2017) / START (2014–2022)
  • Labelled Interpolation Systems for Hyper-Resolution, Clausal, and Local Proofs / Schlaipfer, M., & Weissenbacher, G. (2016). Labelled Interpolation Systems for Hyper-Resolution, Clausal, and Local Proofs. Journal of Automated Reasoning, 57(1), 3–36. https://doi.org/10.1007/s10817-016-9364-6
  • Angry-HEX: an Artificial Player for Angry Birds Based on Declarative Knowledge Bases / Ianni, G., Calimeri, F., Germano, S., Humenberger, A., Redl, C., Stepanova, D., Tucci, A., & Wimmer, A. (2016). Angry-HEX: an Artificial Player for Angry Birds Based on Declarative Knowledge Bases. IEEE Transactions on Computational Intelligence and AI in Games, 8(2), 128–139. https://doi.org/10.1109/tciaig.2015.2509600
    Projects: ASP (2012–2015) / IE of ASP (2015–2018)
  • When Should We Add Theory Axioms And Which Ones? / Reger, G., & Suda, M. (2016). When Should We Add Theory Axioms And Which Ones? 1st Conference on Artificial Intelligence and Theorem Proving, AITP 2016, Obergurgl, Austria. http://hdl.handle.net/20.500.12708/86349
  • Automated Reasoning for Systems Engineering / Kovacs, L. (2016). Automated Reasoning for Systems Engineering. Austrian Computer Science Day 2018, Salzburg, Austria. http://hdl.handle.net/20.500.12708/86695
  • First-Order Theorem Proving and Vampire / Kovacs, L. (2016). First-Order Theorem Proving and Vampire. Spring School on Logic and Verification - LoVE, Vienna, Austria, Austria. http://hdl.handle.net/20.500.12708/86438
  • Parameterized Verification of Liveness of Distributed Algorithms / Konnov, I., Lazić, M., Veith, H., & Widder, J. (2016). Parameterized Verification of Liveness of Distributed Algorithms. Workshop on Formal Reasoning in Distributed Algorithms (FRiDA), Wien, Austria. http://hdl.handle.net/20.500.12708/86425
  • Treewidth-Preserving Modeling in ASP / Bichler, M., Bliem, B., Moldovan, M., Morak, M., & Woltran, S. (2016). Treewidth-Preserving Modeling in ASP (DBAI-TR-2016-97). http://hdl.handle.net/20.500.12708/39078
    Project: START (2014–2022)

2015

  • Asymptotically Precise Ranking Functions for Deterministic Size-Change Systems / Zuleger, F. (2015). Asymptotically Precise Ranking Functions for Deterministic Size-Change Systems. In Computer Science -- Theory and Applications 10th International Computer Science Symposium in Russia, CSR 2015, Listvyanka, Russia, July 13-17, 2015, Proceedings (pp. 426–442). Springer. https://doi.org/10.1007/978-3-319-20297-6_27
  • Abstraction and mining of traces to explain concurrency bugs / Tabaei Befrouei, M. (2015). Abstraction and mining of traces to explain concurrency bugs. In T. Ströder & W. Thomas (Eds.), Proceedings of the Young Researchers’ Conference “Frontiers of Formal Methods” (p. 5). http://hdl.handle.net/20.500.12708/56440
  • Logics of Finite Hankel Rank / Labai, N., & Makowsky, J. A. (2015). Logics of Finite Hankel Rank. In Fields of Logic and Computation II (pp. 237–252). Springer. https://doi.org/10.1007/978-3-319-23534-9_14
  • Compilation for Secure Two-Party Computations / Franz, M., Holzer, A., Katzenbeisser, S., Schallhart, C., & Veith, H. (2015). Compilation for Secure Two-Party Computations. In Software Engineering & Management 2015 (pp. 143–145). GI-Edition - Lecture Notes in Informatics (LNI). http://hdl.handle.net/20.500.12708/56383
  • Liveness of Parameterized Timed Networks / Aminof, B., Rubin, S., Spegni, F., & Zuleger, F. (2015). Liveness of Parameterized Timed Networks. In Automata, Languages, and Programming (pp. 375–387). Springer. https://doi.org/10.1007/978-3-662-47666-6_30
  • Proving Safety with Trace Automata and Bounded Model Checking / Lewis, M., Kroening, D., & Weissenbacher, G. (2015). Proving Safety with Trace Automata and Bounded Model Checking. In FM 2015: Formal Methods (pp. 325–341). Lecture Notes in Computer Science/Springer. https://doi.org/10.1007/978-3-319-19249-9_21
  • Under-approximating loops in C programs for fast counterexample detection / Lewis, M., Kroening, D., & Weissenbacher, G. (2015). Under-approximating loops in C programs for fast counterexample detection. Formal Methods in System Design, 47(1), 75–92. https://doi.org/10.1007/s10703-015-0228-1
  • Closure properties and complexity of rational sets of regular languages / Holzer, A., Schallhart, C., Tautschnig, M., & Veith, H. (2015). Closure properties and complexity of rational sets of regular languages. Theoretical Computer Science, 605, 62–79. https://doi.org/10.1016/j.tcs.2015.08.035
  • On the expressive power of communication primitives in parameterised systems / Aminof, B., Rubin, S., & Zuleger, F. (2015). On the expressive power of communication primitives in parameterised systems. In M. Davis, A. Fehnker, A. McIver, & A. Voronkov (Eds.), Logic for Programming, Artificial Intelligence, and Reasoning : 20th International Conference, LPAR-20 2015, Suva, Fiji, November 24-28, 2015, Proceedings (pp. 313–328). Springer. https://doi.org/10.1007/978-3-662-48899-7_22
    Download: PDF (438 KB)
  • Boolean Satisfiability Solvers and Their Applications in Model Checking / Vizel, Y., Weissenbacher, G., & Malik, S. (2015). Boolean Satisfiability Solvers and Their Applications in Model Checking. Proceedings of the IEEE, 103(11), 2021–2035. https://doi.org/10.1109/jproc.2015.2455034
  • Loop Patterns in C Programs / Pani, T., Veith, H., & Zuleger, F. (2015). Loop Patterns in C Programs. ECEASST, 72. http://hdl.handle.net/20.500.12708/151928
  • LTSmin: High-Performance Language-Independent Model Checking / Blom, S., van Dijk, T., Gijis, K., Laarman, A., Meijer, J., & van de Pol, J. (2015). LTSmin: High-Performance Language-Independent Model Checking. In Tools and Algorithms for the Construction and Analysis of Systems (pp. 692–707). Springer Berlin Heidelberg. https://doi.org/10.1007/978-3-662-46681-0_61
  • Time Complexity of Link Reversal Routing / Charron-Bost, B., Függer, M., Welch, J. L., & Widder, J. (2015). Time Complexity of Link Reversal Routing. ACM Transactions on Algorithms, 11(3), 1–39. https://doi.org/10.1145/2644815
  • Explaining Heisenbugs / Weissenbacher, G. (2015). Explaining Heisenbugs. In E. Bartocci & R. Majumdar (Eds.), Runtime Verification (p. XV). Lecture Notes in Computer Science/Springer. http://hdl.handle.net/20.500.12708/56231
  • SMT and POR Beat Counter Abstraction: Parameterized Model Checking of Threshold-Based Distributed Algorithms / Konnov, I., Veith, H., & Widder, J. (2015). SMT and POR Beat Counter Abstraction: Parameterized Model Checking of Threshold-Based Distributed Algorithms. In Computer Aided Verification (pp. 85–102). LNCS Springer. https://doi.org/10.1007/978-3-319-21690-4_6
  • Empirical Software Metrics for Benchmarking of Verification Tools / Demyanova, Y., Pani, T., Veith, H., & Zuleger, F. (2015). Empirical Software Metrics for Benchmarking of Verification Tools. In Computer Aided Verification (pp. 561–579). Springer. https://doi.org/10.1007/978-3-319-21690-4_39
  • Difference Constraints: An adequate Abstraction for Complexity Analysis of Imperative Programs / Sinn, M., Veith, H., & Zuleger, F. (2015). Difference Constraints: An adequate Abstraction for Complexity Analysis of Imperative Programs. In FMCAD (pp. 144–151). http://hdl.handle.net/20.500.12708/56391
  • Perspectives on White-Box Testing: Coverage, Concurrency, and Concolic Execution / Farzan, A., Holzer, A., & Veith, H. (2015). Perspectives on White-Box Testing: Coverage, Concurrency, and Concolic Execution. In 2015 IEEE 8th International Conference on Software Testing, Verification and Validation (ICST). International Conference on Software Testing, Verification and Validation (ICST), Graz, Austria. https://doi.org/10.1109/icst.2015.7102600
  • Merging in the Horn Fragment / Haret, A., Rümmele, S., & Woltran, S. (2015). Merging in the Horn Fragment. In Q. Yang & M. Wooldridge (Eds.), Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence - IJCAI 2015 (pp. 3041–3047). AAAI Press. http://hdl.handle.net/20.500.12708/56274
  • An extension-based approach to belief revision in abstract argumentation / Diller, M., Haret, A., Linsbichler, T., Rümmele, S., & Woltran, S. (2015). An extension-based approach to belief revision in abstract argumentation. In Q. Yang & M. Wooldridge (Eds.), Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence - IJCAI 2015 (pp. 2926–2932). AAAI Press. http://hdl.handle.net/20.500.12708/56273
  • Extending ALCQIO with Trees / Kotek, T., imkus, M., Veith, H., & Zuleger, F. (2015). Extending ALCQIO with Trees. In 2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science. 30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2015), Kyoto, Japan, Austria. IEEE. https://doi.org/10.1109/lics.2015.54
    Projects: Automated Bound Analysis (2013–2016) / FAIR (2013–2018) / PROSEED (2011–2015) / SEE (2012–2016)
  • Decidability of Parameterized Verification / Bloem, R., Jacobs, S., Khalimov, A., Konnov, I., Rubin, S., Veith, H., & Widder, J. (2015). Decidability of Parameterized Verification. In Synthesis Lectures on Distributed Computing Theory (p. 170). Morgan & Claypool Publishers. https://doi.org/10.2200/s00658ed1v01y201508dct013

2014

  • Reusing Information in Multi-Goal Reachability Analyses / Beyer, D., Holzer, A., Tautschnig, M., & Veith, H. (2014). Reusing Information in Multi-Goal Reachability Analyses. In Software Engineering 2014 (pp. 97–98). LNI. http://hdl.handle.net/20.500.12708/55321
  • CBMC-GC: An ANSI C Compiler for Secure Two-Party Computations / Franz, M., Holzer, A., Katzenbeisser, S., Schallhart, C., & Veith, H. (2014). CBMC-GC: An ANSI C Compiler for Secure Two-Party Computations. In Compiler Construction 23rd International Conference, CC 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings (pp. 244–249). Springer / LNCS. https://doi.org/10.1007/978-3-642-54807-9_15
  • Connection Matrices and the Definability of Graph Parameters / Kotek, T., & Makowsky, J. A. (2014). Connection Matrices and the Definability of Graph Parameters. Logical Methods in Computer Science, 10(4), 1–33. http://hdl.handle.net/20.500.12708/157260
  • Recurrence relations for graph polynomials on bi-iterative families of graphs / Kotek, T., & Makowsky, J. A. (2014). Recurrence relations for graph polynomials on bi-iterative families of graphs. European Journal of Combinatorics, 41, 47–67. https://doi.org/10.1016/j.ejc.2014.03.012
  • A representation theorem for (q-)holonomic sequences / Kotek, T., & Makowsky, J. A. (2014). A representation theorem for (q-)holonomic sequences. Journal of Computer and System Sciences, 80(2), 363–374. https://doi.org/10.1016/j.jcss.2013.05.004
  • Tutorial on Parameterized Model Checking of Fault-Tolerant Distributed Algorithms / Gmeiner, A., Konnov, I., Schmid, U., Veith, H., & Widder, J. (2014). Tutorial on Parameterized Model Checking of Fault-Tolerant Distributed Algorithms. In Formal Methods for Executable Software Models (pp. 122–171). Springer. https://doi.org/10.1007/978-3-319-07317-0_4
  • Parameterized Model Checking of Token-Passing Systems / Aminof, B., Jacobs, S., Khalimov, A., & Rubin, S. (2014). Parameterized Model Checking of Token-Passing Systems. In Verification, Model Checking, and Abstract Interpretation 15th International Conference, VMCAI 2014, San Diego, CA, USA, January 19-21, 2014, Proceedings (pp. 262–281). Springer / LNCS. https://doi.org/10.1007/978-3-642-54013-4_15
  • A Logic-Based Framework for Verifying Consensus Algorithms / Drăgoi, C., Henzinger, T. A., Veith, H., Widder, J., & Zufferey, D. (2014). A Logic-Based Framework for Verifying Consensus Algorithms. In Verification, Model Checking, and Abstract Interpretation 15th International Conference, VMCAI 2014, San Diego, CA, USA, January 19-21, 2014, Proceedings (pp. 161–181). Springer / LNCS. https://doi.org/10.1007/978-3-642-54013-4_10
  • Towards a Description Logic for Program Analysis: Extending ALCQIO with Reachability / Kotek, T., Simkus, M., Veith, H., & Zuleger, F. (2014). Towards a Description Logic for Program Analysis: Extending ALCQIO with Reachability. In International Workshop on Description Logics (p. 4). http://hdl.handle.net/20.500.12708/55329
  • Shape and Content: Incorporating Domain Knowledge into Shape Analysis / Calvanese, D., Kotek, T., Simkus, M., Veith, H., & Zuleger, F. (2014). Shape and Content: Incorporating Domain Knowledge into Shape Analysis. In International Workshop on Description Logics (p. 4). http://hdl.handle.net/20.500.12708/55330
  • On the Complexity of Symbolic Verification and Decision Problems in Bit-Vector Logic / Kovasznai, G., Veith, H., Fröhlich, A., & Biere, A. (2014). On the Complexity of Symbolic Verification and Decision Problems in Bit-Vector Logic. 15th International Workshop on Logic and Computational Complexity and Workshop in Honor of Neil Immerman’s 60th Birthday (LCC 2014/ImmermanFest), Wien, Austria. http://hdl.handle.net/20.500.12708/85894
  • On the Complexity of Symbolic Verification and Decision Problems in Bit-Vector Logic / Kovásznai, G., Veith, H., Fröhlich, A., & Biere, A. (2014). On the Complexity of Symbolic Verification and Decision Problems in Bit-Vector Logic. In Mathematical Foundations of Computer Science 2014 (pp. 481–492). Springer / LNCS. https://doi.org/10.1007/978-3-662-44465-8_41
  • On the Complexity of Symbolic Verification and Decision Problems in Bit-Vector Logic / Fröhlich, A., Kovasznai, G., Biere, A., & Veith, H. (2014). On the Complexity of Symbolic Verification and Decision Problems in Bit-Vector Logic. In POS (p. 14). http://hdl.handle.net/20.500.12708/55327
  • Shape and Content - A Database-Theoretic Perspective on the Analysis of Data Structures / Calvanese, D., Kotek, T., Šimkus, M., Veith, H., & Zuleger, F. (2014). Shape and Content - A Database-Theoretic Perspective on the Analysis of Data Structures. In E. Albert & E. Sekerinski (Eds.), Integrated Formal Methods (pp. 3–17). Springer / LNCS. https://doi.org/10.1007/978-3-319-10181-1_1
  • Vienna Summer of Logic / Baaz, M., Eiter, T., & Veith, H. (2014). Vienna Summer of Logic. Vienna Summer of Logic, Wien, Austria, Austria. http://hdl.handle.net/20.500.12708/121057
  • AngryHEX: An Angry Birds-playing Agent based on HEX-Programs / Calimeri, F., Fink, M., Germano, S., Humenberger, A., Ianni, G., Redl, C., Stepanova, D., & Tucci, A. (2014). AngryHEX: An Angry Birds-playing Agent based on HEX-Programs. AngryBirds Competition 2014, Prague, Czech Republic, EU. http://hdl.handle.net/20.500.12708/85870
    Project: ASP (2012–2015)
  • History of Model Checking / Veith, H. (2014). History of Model Checking. Clarke Symposium 2014: Celebrating 25 Years of Model Checking, Pittsburgh, PA, USA, Non-EU. http://hdl.handle.net/20.500.12708/86029
  • Model Checking of Fault-Tolerant Distributed Algorithms / Veith, H. (2014). Model Checking of Fault-Tolerant Distributed Algorithms. Summer School 2014: Verification Technology, Systems & Applications, Luxembourg, EU. http://hdl.handle.net/20.500.12708/86028
  • Concolic Testing of Concurrent Programs / Farzan, A., Holzer, A., Razavi, N., & Veith, H. (2014). Concolic Testing of Concurrent Programs. International Workshop on Exploiting Concurrency Efficiently and Correctly (EC2), Wien, Austria. http://hdl.handle.net/20.500.12708/85899
  • Parameterized Model Checking of Rendezvous Systems / Aminof, B., Kotek, T., Rubin, S., Spegni, F., & Veith, H. (2014). Parameterized Model Checking of Rendezvous Systems. Algorithmics of Infinite State Systems workshop, Wien, Austria. http://hdl.handle.net/20.500.12708/85898
  • Explaining the decompositionality of monadic second order logic using applications to combinatorics / Kotek, T. (2014). Explaining the decompositionality of monadic second order logic using applications to combinatorics. Fun With Formal Methods Workshop, Wien, Austria. http://hdl.handle.net/20.500.12708/85897
  • Parameterised Verification of Robot Protocols: An Automata Theoretic Approach / Rubin, S. (2014). Parameterised Verification of Robot Protocols: An Automata Theoretic Approach. Workshop on Formal Reasoning in Distributed Algorithms (FRiDA), Wien, Austria. http://hdl.handle.net/20.500.12708/85896
  • First Cycle Games / Rubin, S. (2014). First Cycle Games. Highlights of Logic, Games and Automata, Paris, Frankreich, EU. http://hdl.handle.net/20.500.12708/85895
  • Approaching Verification and Validation Challenges in Smart Grids / Deutsch, T., & Widder, J. (2014). Approaching Verification and Validation Challenges in Smart Grids. In Tagungsband ComForEn 2014 (p. 6). Eigenverlag des Österreich isch en Verbandes für Elektrotec h nik. http://hdl.handle.net/20.500.12708/55738
  • First Cycle Games / Aminof, B., & Rubin, S. (2014). First Cycle Games. In Electronic Proceedings in Theoretical Computer Science (pp. 83–90). EPTCS. https://doi.org/10.4204/eptcs.146.11
  • Counterexample to Induction-Guided Abstraction-Refinement (CTIGAR) / Birgmeier, J., Bradley, A. R., & Weissenbacher, G. (2014). Counterexample to Induction-Guided Abstraction-Refinement (CTIGAR). In Computer Aided Verification (pp. 831–848). Springer / LNCS. https://doi.org/10.1007/978-3-319-08867-9_55
  • An Open Alternative for SMT-Based Verification of Scade Models / Basold, H., Günther, H., Huhn, M., & Milius, S. (2014). An Open Alternative for SMT-Based Verification of Scade Models. In Formal Methods for Industrial Critical Systems (pp. 124–139). Springer / LNCS. https://doi.org/10.1007/978-3-319-10702-8_9
  • Size-Change Abstraction and Max-Plus Automata / Colcombet, T., Daviaud, L., & Zuleger, F. (2014). Size-Change Abstraction and Max-Plus Automata. In Mathematical Foundations of Computer Science 2014 (pp. 208–219). Springer / LNCS. https://doi.org/10.1007/978-3-662-44522-8_18
  • Concolic Testing of Concurrent Programs / Farzan, A., Holzer, A., Razavi, N., & Veith, H. (2014). Concolic Testing of Concurrent Programs. In Software Engineering 2014 (pp. 101–102). LNI. http://hdl.handle.net/20.500.12708/55320
  • Incremental bounded software model checking / Günther, H., & Weissenbacher, G. (2014). Incremental bounded software model checking. In Proceedings of the 2014 International SPIN Symposium on Model Checking of Software. International SPIN Symposium on Model Checking of Software (SPIN), Stony Brook, NY, USA, Non-EU. ACM New York, NY, USA. https://doi.org/10.1145/2632362.2632374
  • Feedback generation for performance problems in introductory programming assignments / Gulwani, S., Radiček, I., & Zuleger, F. (2014). Feedback generation for performance problems in introductory programming assignments. In Proceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering. ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE), Hong Kong, China, Non-EU. ACM New York, NY, USA. https://doi.org/10.1145/2635868.2635912
  • On the Completeness of Bounded Model Checking for Threshold-Based Distributed Algorithms: Reachability / Konnov, I., Veith, H., & Widder, J. (2014). On the Completeness of Bounded Model Checking for Threshold-Based Distributed Algorithms: Reachability. In CONCUR 2014 – Concurrency Theory (pp. 125–140). https://doi.org/10.1007/978-3-662-44584-6_10
  • Partial-Order Reduction for Multi-core LTL Model Checking / Laarman, A., & Wijs, A. (2014). Partial-Order Reduction for Multi-core LTL Model Checking. In Hardware and Software: Verification and Testing (pp. 267–283). Springer / LNCS. https://doi.org/10.1007/978-3-319-13338-6_20
  • Solvability-Based Comparison of Failure Detectors / Sastry, S., & Widder, J. (2014). Solvability-Based Comparison of Failure Detectors. In 2014 IEEE 13th International Symposium on Network Computing and Applications. International Symposium on Network Computing and Applications (NCA), Boston, MA, USA, Non-EU. IEEE Computer Society. https://doi.org/10.1109/nca.2014.46
  • A Simple and Scalable Static Analysis for Bound Analysis and Amortized Complexity Analysis / Sinn, M., Zuleger, F., & Veith, H. (2014). A Simple and Scalable Static Analysis for Bound Analysis and Amortized Complexity Analysis. In Computer Aided Verification (pp. 745–761). Springer / LNCS. https://doi.org/10.1007/978-3-319-08867-9_50
  • Abstraction and Mining of Traces to Explain Concurrency Bugs / Tabaei Befrouei, M., Wang, C., & Weissenbacher, G. (2014). Abstraction and Mining of Traces to Explain Concurrency Bugs. In Runtime Verification (pp. 162–177). Springer / LNCS. https://doi.org/10.1007/978-3-319-11164-3_14
  • Silicon fault diagnosis using sequence interpolation with backbones / Zhu, C. S., Weissenbacher, G., & Malik, S. (2014). Silicon fault diagnosis using sequence interpolation with backbones. In ICCAD (pp. 348–355). IEEE Press Piscataway, NJ, USA. http://hdl.handle.net/20.500.12708/55310
  • Parameterized Model Checking of Rendezvous Systems / Aminof, B., Kotek, T., Rubin, S., Spegni, F., & Veith, H. (2014). Parameterized Model Checking of Rendezvous Systems. In CONCUR 2014 – Concurrency Theory (pp. 109–124). Springer / LNCS. https://doi.org/10.1007/978-3-662-44584-6_9

2013

  • Under-Approximating Loops in C Programs for Fast Counterexample Detection / Kroening, D., Lewis, M., & Weissenbacher, G. (2013). Under-Approximating Loops in C Programs for Fast Counterexample Detection. In Computer Aided Verification (pp. 381–396). Springer / LNCS. https://doi.org/10.1007/978-3-642-39799-8_26
  • On the Structure and Complexity of Rational Sets of Regular Languages / Holzer, A., Schallhart, C., Tautschnig, M., & Veith, H. (2013). On the Structure and Complexity of Rational Sets of Regular Languages. In S. Anil & N. K. Vishnoi (Eds.), FSTTCS 2013 (pp. 377–388). Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik. https://doi.org/10.4230/LIPIcs.FSTTCS.2013.377
  • Information Reuse for Multi-goal Reachability Analyses / Beyer, D., Holzer, A., Tautschnig, M., & Veith, H. (2013). Information Reuse for Multi-goal Reachability Analyses. In Programming Languages and Systems (pp. 472–491). Springer / LNCS. https://doi.org/10.1007/978-3-642-37036-6_26
  • First-Order Theorem Proving and Vampire / Kovács, L., & Voronkov, A. (2013). First-Order Theorem Proving and Vampire. In N. Sharygina & H. Veith (Eds.), Computer Aided Verification (pp. 1–35). Springer LNCS 8044. https://doi.org/10.1007/978-3-642-39799-8_1
  • Verification across Intellectual Property Boundaries / Chaki, S., Schallhart, C., & Veith, H. (2013). Verification across Intellectual Property Boundaries. ACM Transactions on Software Engineering and Methodology, 22(2), 1–12. https://doi.org/10.1145/2430545.2430550
  • Advanced SAT Techniques for Abstract Argumentation / Wallner, J. P., Weissenbacher, G., & Woltran, S. (2013). Advanced SAT Techniques for Abstract Argumentation. In Computational Logic in Multi-Agent Systems 14th International Workshop, CLIMA XIV, Corunna, Spain, September 16-18, 2013, Proceedings (pp. 138–154). Springer / LNCS. https://doi.org/10.1007/978-3-642-40624-9_9
  • Solving Constraints for Generational Search / Pötzl, D., & Holzer, A. (2013). Solving Constraints for Generational Search. In 12 (pp. 197–213). Springer / LNCS. https://doi.org/10.1007/978-3-642-38916-0_12
  • Link Reversal Routing with Binary Link Labels: Work Complexity / Charron-Bost, B., Gaillard, A., Welch, J. L., & Widder, J. (2013). Link Reversal Routing with Binary Link Labels: Work Complexity. SIAM Journal on Computing, 42(2), 634–661. https://doi.org/10.1137/110843095
  • Formal Verification of Distributed Algorithms / Charron-Bost, B., Merz, S., Rybalchenko, A., & Widder, J. (Eds.). (2013). Formal Verification of Distributed Algorithms. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany. https://doi.org/10.4230/DagRep.3.4.1
  • Challenges in compiler construction for secure two-party computation / Holzer, A., Karvelas, N., Katzenbeisser, S., & Veith, H. (2013). Challenges in compiler construction for secure two-party computation. In Proceedings of the First ACM workshop on Language support for privacy-enhancing technologies - PETShop ’13. Workshop on language support for privacy-enhancing technologies (PETShop), Berlin, Deutschland, EU. ACM. https://doi.org/10.1145/2517872.2517876
  • The first workshop on language support for privacy-enhancing technologies (PETShop'13) / Franz, M., Holzer, A., Majumdar, R., Parno, B., & Veith, H. (2013). The first workshop on language support for privacy-enhancing technologies (PETShop’13). In Proceedings of the 2013 ACM SIGSAC conference on Computer & communications security - CCS ’13. ACM Conference on Computer and Communications Security (CCS), Washington, USA, Non-EU. ACM. https://doi.org/10.1145/2508859.2509032
  • Con2colic testing / Farzan, A., Holzer, A., Razavi, N., & Veith, H. (2013). Con2colic testing. In Proceedings of the 2013 9th Joint Meeting on Foundations of Software Engineering - ESEC/FSE 2013. Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE), Sankt Petersburg, Russland, Non-EU. ACM. https://doi.org/10.1145/2491411.2491453
  • Brief announcement / John, A., Konnov, I., Schmid, U., Veith, H., & Widder, J. (2013). Brief announcement. In Proceedings of the 2013 ACM symposium on Principles of distributed computing - PODC ’13. ACM SIGACT-SIGOPS Symposium on Principles of Distributed Computing (PODC), Montreal, Kanada, Non-EU. ACM. https://doi.org/10.1145/2484239.2484285
  • On the concept of variable roles and its use in software analysis / Demyanova, Y., Veith, H., & Zuleger, F. (2013). On the concept of variable roles and its use in software analysis. In FMCAD (pp. 226–230). IEEE. http://hdl.handle.net/20.500.12708/54835
  • Parameterized model checking of fault-tolerant distributed algorithms by abstraction / John, A., Konnov, I., Schmid, U., Veith, H., & Widder, J. (2013). Parameterized model checking of fault-tolerant distributed algorithms by abstraction. In FMCAD (pp. 201–209). http://hdl.handle.net/20.500.12708/54827
  • Mining Sequential Patterns to Explain Concurrent Counterexamples / Leue, S., & Befrouei, M. T. (2013). Mining Sequential Patterns to Explain Concurrent Counterexamples. In Model Checking Software (pp. 264–281). LNCS, Springer. https://doi.org/10.1007/978-3-642-39176-7_17
  • Towards Modeling and Model Checking Fault-Tolerant Distributed Algorithms / John, A., Konnov, I., Schmid, U., Veith, H., & Widder, J. (2013). Towards Modeling and Model Checking Fault-Tolerant Distributed Algorithms. In Model Checking Software (pp. 209–226). LNCS, Springer. https://doi.org/10.1007/978-3-642-39176-7_14
  • Ramsey vs. Lexicographic Termination Proving / Cook, B., See, A., & Zuleger, F. (2013). Ramsey vs. Lexicographic Termination Proving. In Tools and Algorithms for the Construction and Analysis of Systems (pp. 47–61). Lecture Notes in Computer Science. Springer Verlag. https://doi.org/10.1007/978-3-642-36742-7_4
  • CAV / CAV. (2013). In N. Sharygina & H. Veith (Eds.), Lecture Notes in Computer Science. Springer. https://doi.org/10.1007/978-3-642-39799-8

2012

  • Proving Reachability Using FShell / Holzer, A., Kroening, D., Schallhart, C., Tautschnig, M., & Veith, H. (2012). Proving Reachability Using FShell. In C. Flanagan & B. König (Eds.), Tools and Algorithms for the Construction and Analysis of Systems (pp. 538–541). Springer. https://doi.org/10.1007/978-3-642-28756-5_43
  • Bounded-Interference Sequentialization for Testing Concurrent Programs / Razavi, N., Farzan, A., & Holzer, A. (2012). Bounded-Interference Sequentialization for Testing Concurrent Programs. In T. Margaria & B. Steffen (Eds.), Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change. (ISoLA 2012), Proceedings, Part I (pp. 372–387). Springer. https://doi.org/10.1007/978-3-642-34026-0_28
  • Vinter: A Vampire-Based Tool for Interpolation / Hoder, K., Holzer, A., Kovács, L., & Voronkov, A. (2012). Vinter: A Vampire-Based Tool for Interpolation. In Programming Languages and Systems (pp. 148–156). Springer / LNCS. https://doi.org/10.1007/978-3-642-35182-2_11
  • Efficient Checking of Link-Reversal-Based Concurrent Systems / Függer, M., & Widder, J. (2012). Efficient Checking of Link-Reversal-Based Concurrent Systems. In CONCUR 2012- Concurrency Theory 23rd International Conference, CONCUR 2012, Newcastle upon Tyne, September 4-7, 2012. Proceedings (pp. 486–499). Lecture Notes in Computer Science. Springer Verlag. https://doi.org/10.1007/978-3-642-32940-1_34
  • Wait-Free Stabilizing Dining Using Regular Registers / Sastry, S., Welch, J. L., & Widder, J. (2012). Wait-Free Stabilizing Dining Using Regular Registers. In Principles of Distributed Systems 16th International Conference, OPODIS 2012, Rome, Italy, December 18-20, 2012, Proceedings (pp. 284–299). LNCS / Springer. https://doi.org/10.1007/978-3-642-35476-2_20
  • Special Issue: Games in Verification (foreword) / Veith, H. (2012). Special Issue: Games in Verification (foreword). Journal of Computer and System Sciences, 78(2), 393. https://doi.org/10.1016/j.jcss.2011.05.007
  • Secure two-party computations in ANSI C / Holzer, A., Franz, M., Katzenbeisser, S., & Veith, H. (2012). Secure two-party computations in ANSI C. In Proceedings of the 2012 ACM conference on Computer and communications security - CCS ’12. ACM Conference on Computer and Communications Security (CCS), Washington, USA, Non-EU. ACM. https://doi.org/10.1145/2382196.2382278
  • Selected Papers of the Conference "Computer Science Logic CSL 2010": Preface / Dawar, A., & Veith, H. (2012). Selected Papers of the Conference “Computer Science Logic CSL 2010”: Preface. Logical Methods in Computer Science. https://doi.org/10.2168/lmcs-csl:2010
  • Consensus in the presence of mortal Byzantine faulty processes / Widder, J., Biely, M., Gridling, G., Weiss, B., & Blanquart, J.-P. (2012). Consensus in the presence of mortal Byzantine faulty processes. Distributed Computing, 24(6), 299–321. https://doi.org/10.1007/s00446-011-0147-3
  • Who is afraid of Model Checking Distributed Algorithms? / Konnov, I., Veith, H., & Widder, J. (2012). Who is afraid of Model Checking Distributed Algorithms? Workshop on Exploiting Concurrency Efficiently and Correctly, Berkeley, CA, USA, Non-EU. http://hdl.handle.net/20.500.12708/85358
  • Who is afraid of Model Checking Distributed Algorithms? / John, A., Konnov, I., Schmid, U., Veith, H., & Widder, J. (2012). Who is afraid of Model Checking Distributed Algorithms? PUMA/RISE Seminar, Traunkirchen, Austria. http://hdl.handle.net/20.500.12708/85435
  • Secure Two-Party Computation in ANSI C / Veith, H. (2012). Secure Two-Party Computation in ANSI C. Dagstuhl Seminar 12461: Games and Decisions for Rigorous Systems Engineering, Dagstuhl, Deutschland, EU. http://hdl.handle.net/20.500.12708/85434
  • Labelled Interpolation Systems / Weissenbacher, G. (2012). Labelled Interpolation Systems. Dagstuhl Seminar 12461: Games and Decisions for Rigorous Systems Engineering, Dagstuhl, Deutschland, EU. http://hdl.handle.net/20.500.12708/85433
  • Parameterized Model Checking of Fault-tolerant Distributed Algorithms / John, A., Konnov, I., Schmid, U., Veith, H., & Widder, J. (2012). Parameterized Model Checking of Fault-tolerant Distributed Algorithms. Dagstuhl Seminar 12461: Games and Decisions for Rigorous Systems Engineering, Dagstuhl, Deutschland, EU. http://hdl.handle.net/20.500.12708/85432
  • Counter Attack against Byzantine Generals / John, A., Konnov, I., Schmid, U., Veith, H., & Widder, J. (2012). Counter Attack against Byzantine Generals. Alpine Verification Meeting, IST Austria, Austria. http://hdl.handle.net/20.500.12708/85359
  • Interpretations in Trees with Countably Many Branches / Rabinovich, A., & Rubin, S. (2012). Interpretations in Trees with Countably Many Branches. In 2012 27th Annual IEEE Symposium on Logic in Computer Science. Symposium on Logic in Computer Science (LICS), Edinburgh, United Kingdom, EU. IEEE. https://doi.org/10.1109/lics.2012.65
  • Interpolant Strength Revisited / Weissenbacher, G. (2012). Interpolant Strength Revisited. In Theory and Applications of Satisfiability Testing – SAT 2012 (pp. 312–326). LNCS / Springer. https://doi.org/10.1007/978-3-642-31612-8_24
  • A Myhill-Nerode theorem for automata with advice / Kruckman, A., Rubin, S., Sheridan, J., & Zax, B. (2012). A Myhill-Nerode theorem for automata with advice. In M. Faella & A. Murano (Eds.), Electronic Proceedings in Theoretical Computer Science (pp. 238–246). Electronic Proceedings in Theoretical Computer Science. https://doi.org/10.4204/eptcs.96.18
  • Coverage-Based Trace Signal Selection for Fault Localisation in Post-silicon Validation / Charlie Shucheng, Z., Weissenbacher, G., & Malik, S. (2012). Coverage-Based Trace Signal Selection for Fault Localisation in Post-silicon Validation. In Hardware and Software: Verification and Testing (pp. 132–147). Lecture Notes in Computer Science. Springer Verlag. https://doi.org/10.1007/978-3-642-39611-3_16
  • Parallel Assertions for Architectures with Weak Memory Models / Schwartz-Narbonne, D., Weissenbacher, G., & Malik, S. (2012). Parallel Assertions for Architectures with Weak Memory Models. In Automated Technology for Verification and Analysis (pp. 254–268). Lecture Notes in Computer Science. Springer Verlag. https://doi.org/10.1007/978-3-642-33386-6_21

2011

2010

  • An Introduction to Test Specification in FQL / Holzer, A., Tautschnig, M., Schallhart, C., & Veith, H. (2010). An Introduction to Test Specification in FQL. In S. Barner, J. G. Harris, D. Kroening, & O. Raz (Eds.), Hardware and Software: Verification and Testing (pp. 9–22). Springer. https://doi.org/10.1007/978-3-642-19583-9_5
    Project: FORTAS (2010–2011)
  • On the distributivity of LTL specifications / Samer, M., & Veith, H. (2010). On the distributivity of LTL specifications. ACM Transactions on Computational Logic, 11(3), 1–26. https://doi.org/10.1145/1740582.1740588
  • Comparing LTL Semantics for Runtime Verification / Bauer, A., Leucker, M., & Schallhart, C. (2010). Comparing LTL Semantics for Runtime Verification. Journal of Logic and Computation, 20(3), 651–674. https://doi.org/10.1093/logcom/exn075
  • How did you specify your test suite / Holzer, A., Schallhart, C., Tautschnig, M., & Veith, H. (2010). How did you specify your test suite. In C. Pecheur, J. Andrews, & E. Di Nitto (Eds.), Proceedings of the IEEE/ACM international conference on Automated software engineering - ASE ’10. ACM. https://doi.org/10.1145/1858996.1859084
  • Semantic Integrity in Large-Scale Online Simulations / Jha, S., Katzenbeisser, S., Schallhart, C., Veith, H., & Chenney, S. (2010). Semantic Integrity in Large-Scale Online Simulations. ACM Transactions on Internet Technology, 10(1), 1–24. https://doi.org/10.1145/1667067.1667069
  • Don't care in SMT---Building flexible yet efficient abstraction/refinement solvers / Bauer, A., Leucker, M., Schallhart, C., & Tautschnig, M. (2010). Don’t care in SMT---Building flexible yet efficient abstraction/refinement solvers. International Journal on Software Tools for Technology Transfer, 12(1), 23–37. https://doi.org/10.1007/s10009-009-0133-2
  • Proactive Detection of Computer Worms Using Model Checking / Kinder, J., Katzenbeisser, S., Schallhart, C., & Veith, H. (2010). Proactive Detection of Computer Worms Using Model Checking. IEEE Transactions on Dependable and Secure Computing, 7(4), 424–438. https://doi.org/10.1109/tdsc.2008.74
  • Timely Time Estimates / Holzer, A., Januzaj, V., Kugele, S., & Tautschnig, M. (2010). Timely Time Estimates. In T. Margaria & B. Steffen (Eds.), Leveraging Applications of Formal Methods, Verification, and Validation (pp. 33–46). Lecture Notes in Computer Science. https://doi.org/10.1007/978-3-642-16558-0_5
  • Seamless Model-Driven Development Put into Practice / Haberl, W., Herrmannsdoerfer, M., Kugele, S., Tautschnig, M., & Wechs, M. (2010). Seamless Model-Driven Development Put into Practice. In T. Margaria & B. Steffen (Eds.), Leveraging Applications of Formal Methods, Verification, and Validation (pp. 18–32). Lecture Notes in Computer Science. https://doi.org/10.1007/978-3-642-16558-0_4
  • The reachability-bound problem / Gulwani, S., & Zuleger, F. (2010). The reachability-bound problem. In B. G. Zorn & A. Aiken (Eds.), Proceedings of the 2010 ACM SIGPLAN conference on Programming language design and implementation - PLDI ’10. PLDI’10 Proceedings of teh ACM SIGPLAN conference on Programming language design and implementation. https://doi.org/10.1145/1806596.1806630

2007

2006

  • From Temporal Logic Queries to Vacuity Detection / Samer, M., & Veith, H. (2006). From Temporal Logic Queries to Vacuity Detection. In E. Clarke (Ed.), Verification of Infinite-State Systems with Applications to Security (pp. 149–167). IOS Press. http://hdl.handle.net/20.500.12708/25351

2005

  • Deterministic CTL Query Solving / Samer, M., & Veith, H. (2005). Deterministic CTL Query Solving. In J. Chomicki & D. Toman (Eds.), Proceedings of the 12th International Symposium on Temporal Representation and Reasoning (pp. 156–165). IEEE Computer Society. http://hdl.handle.net/20.500.12708/50996

2003

  • Integrating Publish/Subscribe into a Mobile Teamwork Support Platform / Sagar, N., Fenkam, P., Veith, H., Gall, H., Kirda, E., & Jha, S. (2003). Integrating Publish/Subscribe into a Mobile Teamwork Support Platform. In Proceedings of the 15th International Conference on Software Engineering and Knowledge Engineering (pp. 510–517). http://hdl.handle.net/20.500.12708/50936

2002

 

2025

2024

2023

2022

2021

2020

2019

2018

2016

2015

2014

2013

 

  • Florian Zuleger: Verication of Asynchronous Mobile-Robots in Partially-Known Environments
    2015 / Best Paper Award / Italy (South Tyrol)

Soon, this page will include additional information such as reference projects, conferences, events, and other research activities.

Until then, please visit Formal Methods in Systems Engineering’s research profile in TISS .