TU Wien Informatics

20 Years

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.

Pavol Cerny
Pavol Cerny P. Cerny

Full Professor
Univ.Prof. / PhD

Laura Kovacs
Laura Kovacs L. Kovacs

Head of Research Unit
Univ.Prof. Dr. / 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.

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

PreDoc Researcher
MA

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

Katalin Fazekas
Katalin Fazekas K. Fazekas

PostDoc Researcher
DI Dr.

Thomas Hader
Thomas Hader T. Hader

PreDoc Researcher
DI / BSc BSc

Marton Hajdu
Marton Hajdu M. Hajdu

PreDoc Researcher
DI / BSc

Islam Hamada
Islam Hamada I. Hamada

PreDoc Researcher
MSc

Matthias Hetzenberger
Matthias Hetzenberger M. Hetzenberger

PreDoc Researcher
DI / BSc

Petra Hozzova
Petra Hozzova P. Hozzova

PreDoc Researcher
Mag.

Daniela Kaufmann
Daniela Kaufmann D. Kaufmann

PostDoc Researcher
DI Dr.

Marcel Moosbrugger
Marcel Moosbrugger M. Moosbrugger

PreDoc Researcher
DI / BSc BA (Hons)

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

PreDoc Researcher

Anja Petkovic Komel
Anja Petkovic Komel A. Petkovic Komel

PostDoc Researcher / On Leave
Dr.

Alexander Pluska
Alexander Pluska A. Pluska

PreDoc Researcher
MSc

Anna Prianichnikova
Anna Prianichnikova A. Prianichnikova

PostDoc Researcher
Mag. Dr.

Sophie Rain
Sophie Rain S. Rain

PreDoc Researcher
DI / BSc

Jakob Rath
Jakob Rath J. Rath

PreDoc Researcher
DI / BSc

Michael Rawson
Michael Rawson M. Rawson

PostDoc Researcher
PhD

Adrian Rebola Pardo
Adrian Rebola Pardo A. Rebola Pardo

PostDoc Researcher
Dr. / 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

2023W

2024S

 

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
    Project: ARTIST (2021–2026)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • µ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)
  • 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)
  • 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)
  • 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)
  • A provably correct floating-point implementation of Well Clear Avionics Concepts / Bernardes Fernandes Ferreira, N., Moscato, M., Titolo, L., & Ayala-Rincon, 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)
  • 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)
  • 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)
  • 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–2024) / 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)
  • Program Synthesis in Saturation / Hozzova, 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)
  • 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)
  • 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)
  • 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)
  • 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
  • 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)
  • 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)
  • 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
  • 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)
  • 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)
  • 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–2025) / LCS (2017–2025) / PROFET (2019–2023) / ViSP (2019–2023)
  • 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)

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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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., Hozzova, 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., Kovacs, 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., & Kovacs, 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
  • 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)
  • 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
  • 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
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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 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)
  • 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
  • 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

  • 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)
  • Induction with Recursive Definitions in Superposition / Hajdu, M., Hozzova, P., Kovacs, 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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., Hozzova, P., Kovacs, 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 / Hozzova, P., Kovacs, 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 / Hozzova, P., Kovacs, 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)
  • 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, Deutschland, EU. IEEE. https://doi.org/10.1109/iccad51958.2021.9643462
  • 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
  • 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.), Lecture Notes in Computer Science (pp. 17–28). Springer LNCS. https://doi.org/10.1007/978-3-030-67067-2_2
  • 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
  • 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
  • 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
  • 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

2020

  • Induction with Generalization in Superposition Reasoning / Hajdú, M., Hozzova, 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., & Kovacs, 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., Kovacs, 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)
  • 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)
  • 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)
  • 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)
  • 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
  • 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)
  • 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
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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)
  • Synthesizing Best-effort Strategies under Multiple Environment Specifications / Aminof, B., De Giacomo, G., Lomuscio, A., Murano, A., & Rubin, S. (2020). 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
  • 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
  • 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
  • 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
  • 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
  • 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
  • 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
  • The Polynomial Complexity of Vector Addition Systems with States / Zuleger, F. (2020). The Polynomial Complexity of Vector Addition Systems with States. In Lecture Notes in Computer Science (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
  • Language Inclusion for Finite Prime Event Structures / Fellner, A., Tarrach, T., & Weissenbacher, G. (2020). Language Inclusion for Finite Prime Event Structures. In Lecture Notes in Computer Science (pp. 314–336). Springer. https://doi.org/10.1007/978-3-030-39322-9_15
  • 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
  • Formalizing Graph Trail Properties in Isabelle/HOL / Kovács, L., Lachnitt, H., & Szeider, S. (2020). Formalizing Graph Trail Properties in Isabelle/HOL. In Lecture Notes in Computer Science (pp. 190–205). LNCS. https://doi.org/10.1007/978-3-030-53518-6_12
  • 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
  • Pebble-Intervals Automata and FO$$^2$$ with Two Orders / Labai, N., Kotek, T., Ortiz, M., & Veith, H. (2020). Pebble-Intervals Automata and FO$$^2$$ 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
  • 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
  • An ExpTime Upper Bound for ALC with Integers (Extended Version) / Labai, N., Simkus, M., & Ortiz de la Fuente, M. M. (2020). An ExpTime Upper Bound for ALC with Integers (Extended Version) (2006.02078). http://hdl.handle.net/20.500.12708/40248
  • 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

  • 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
  • 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
  • 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, US, Non-EU. http://hdl.handle.net/20.500.12708/86988
  • Automatic Analysis for Prob-Solvable Loops / Stankovic, M. (2019). Automatic Analysis for Prob-Solvable Loops. 13th Alpine Verification Meeting (AVM), Brno, Czech Republic, EU. http://hdl.handle.net/20.500.12708/87000
  • 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
  • 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, EU. 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, EU. 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, EU. http://hdl.handle.net/20.500.12708/86996
  • 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
  • First Order Interpolation / Kovacs, L. (2019). First Order Interpolation. SAT/SMT/AR Summer School 2019, Lisbon, Portugal, EU. 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, EU. 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, EU. 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, EU. http://hdl.handle.net/20.500.12708/86991
  • 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, Non-EU. http://hdl.handle.net/20.500.12708/86990
  • 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, EU. http://hdl.handle.net/20.500.12708/86989
  • 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.), Lecture Notes in Computer Science (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, China, Non-EU. https://doi.org/10.24963/ijcai.2019/155
  • 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
  • Pebble-Intervals Automata and FO2 with Two Orders (Extended Version / Labai, N., Kotek, T., Ortiz de la Fuente, M. M., & Veith, H. (2019). Pebble-Intervals Automata and FO2 with Two Orders (Extended Version (1912.00171). http://hdl.handle.net/20.500.12708/39866
    Projects: KtoAPP (2018–2025) / OMEGA (2017–2022)

2018

  • 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 Verification, Model Checking, and Abstract Interpretation - 19th International Conference, VMCAI 2018, Los Angeles, CA, USA, January 7-9, 2018, Proceedings ; Dillig, Isil; Palsberg, Jens. Cham. https://doi.org/10.1007/978-3-319-73721-8_1
    Download: PDF (538 KB)
  • 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, OR, USA, Non-EU. FMCAD Inc. https://doi.org/10.23919/fmcad.2018.8603005
  • 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
  • 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
  • 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
  • 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
  • ByMC: Byzantine Model Checker / Konnov, I., & Widder, J. (2018). ByMC: Byzantine Model Checker. In Leveraging Applications of Formal Methods, Verification and Validation. Distributed Systems (pp. 327–342). Lecture Notes in Computer Science. Springer Verlag. https://doi.org/10.1007/978-3-030-03424-5_22
  • 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
  • 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
  • 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
  • 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
  • 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
  • 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
  • Symbol Elimination in Program Analysis / Kovacs, L. (2018). Symbol Elimination in Program Analysis. 2nd Facebook Testing and Veri cation Symposium (FaceTAV), London, UK, EU. http://hdl.handle.net/20.500.12708/86842
  • 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, EU. 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, Frankreich, EU. http://hdl.handle.net/20.500.12708/86841
  • 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
  • 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, EU. http://hdl.handle.net/20.500.12708/86713
  • First-Order Interpolation / Kovacs, L. (2018). First-Order Interpolation. SAT/SMT/AR Summer School 2018, Manchester, EU. http://hdl.handle.net/20.500.12708/86712
  • 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
  • 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
  • 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
  • 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, EU. ACM. https://doi.org/10.1145/3209108.3209191
  • 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
  • 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, Non-EU. EasyChair EPiC Series in Computing. https://doi.org/10.29007/w42s
  • 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.), Lecture Notes in Computer Science (pp. 111–117). LNCS. https://doi.org/10.1007/978-3-319-96812-4_10
  • 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, OR, USA, Non-EU. FMCAD Inc. https://doi.org/10.23919/fmcad.2018.8603020
  • 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
  • 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, Non-EU. ACM. https://doi.org/10.1145/3192366.3192387
  • 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
  • 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, Serbien, Non-EU. Singidunum University. https://doi.org/10.15308/sinteza-2018-131-138
  • 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
  • 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
  • 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
  • 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
  • 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
  • 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
  • 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

2017

  • 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
  • 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
  • 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
  • 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, Tschechien, EU. http://hdl.handle.net/20.500.12708/86685
  • 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, Non-EU. http://hdl.handle.net/20.500.12708/86627
  • Local proofs and AVATAR / Reger, G., & Suda, M. (2017). Local proofs and AVATAR. Fourth Vampire Workshop - VAMPIRE 2017, Gothenburg, Sweden, EU. http://hdl.handle.net/20.500.12708/86626
  • Incremental Solving with Vampire / Reger, G., & Suda, M. (2017). Incremental Solving with Vampire. Fourth Vampire Workshop - VAMPIRE 2017, Gothenburg, Sweden, EU. http://hdl.handle.net/20.500.12708/86625
  • 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, EU. http://hdl.handle.net/20.500.12708/86623
  • 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
  • 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, EU. http://hdl.handle.net/20.500.12708/86847
  • Algebraic Reasoning for Program Analysis / Kovacs, L. (2017). Algebraic Reasoning for Program Analysis. 33rd Conference on the Mathematical Foundations of Programming Semantics (MFPS), Ljubljana, Slovenia, EU. http://hdl.handle.net/20.500.12708/86689
  • Symbol Elimination for Program Analysis / Kovacs, L. (2017). Symbol Elimination for Program Analysis. ETH Workshop on Software Correctness and Reliability, Zürich, Switzerland, Non-EU. http://hdl.handle.net/20.500.12708/86690
  • 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
  • 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
  • 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)
  • 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
  • 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
  • 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
  • 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, EU. ACM. https://doi.org/10.1145/3087604.3087623
  • 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
  • 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
  • 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
  • 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
  • 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
  • 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
  • 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
  • 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
  • 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)
  • 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, Vienna, Austria, EU. ACM. https://doi.org/10.1145/3127041.3127049
  • 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, EU. ACM. https://doi.org/10.1145/3009837.3009860
  • 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 Lecture Notes in Computer Science (pp. 246–265). Springer. https://doi.org/10.1007/978-3-319-52234-0_14
  • 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

2016

  • 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)
  • 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, EU. http://hdl.handle.net/20.500.12708/86389
  • 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
  • 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
  • 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
  • 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)
  • The mystery of QBF tautologies / Suda, M. (2016). The mystery of QBF tautologies. Prague Automated Reasoning Seminar, Prague, Czech Republick, EU. http://hdl.handle.net/20.500.12708/86392
  • New Techniques in Clausal Form Generation / Reger, G., Suda, M., & Voronkov, A. (2016). New Techniques in Clausal Form Generation. Prague Automated Reasoning Seminar, Prague, Czech Republick, EU. http://hdl.handle.net/20.500.12708/86391
  • 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, EU. http://hdl.handle.net/20.500.12708/86390
  • 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
  • Revisiting Global Subsumption / Reger, G., & Suda, M. (2016). Revisiting Global Subsumption. The Third Vampire Workshop, VAMPIRE 2016, Coimbra, Portugal, EU. http://hdl.handle.net/20.500.12708/86350
  • 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
  • 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, RIMS, Kyoto University, Kyoto, Japan, Non-EU. http://hdl.handle.net/20.500.12708/86472
  • Quantifier Elimination Over The Reals / Jaroschek, M. (2016). Quantifier Elimination Over The Reals. Tutorial on SMT and Polynomial Arithmetic, Chalmers University, Gothenburg, Sweden, EU. http://hdl.handle.net/20.500.12708/86471
  • 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, Universität Kassel, Kassel, Deutschland, EU. http://hdl.handle.net/20.500.12708/86470
  • 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, EU. http://hdl.handle.net/20.500.12708/86440
  • 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, Schweden, EU. http://hdl.handle.net/20.500.12708/86439
  • 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
  • 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, Russia, Non-EU. http://hdl.handle.net/20.500.12708/86426
  • 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
  • Interpolation algorithms and their applications in model checking / Weissenbacher, G. (2016). Interpolation algorithms and their applications in model checking. Automata, Logic and Games, Singapore, Non-EU. http://hdl.handle.net/20.500.12708/86305
  • 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
  • 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
  • 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
  • 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
  • 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.), Lecture Notes in Computer Science (pp. 20–27). Springer / LNCS. https://doi.org/10.1007/978-3-319-33693-0_2
  • 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
  • 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
  • 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
  • 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
  • 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
  • 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
  • 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)
  • 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
  • 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

  • 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
  • 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
  • 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
  • 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
  • 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
  • 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
  • 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
  • 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
  • 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
  • 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
  • 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
  • Asymptotically Precise Ranking Functions for Deterministic Size-Change Systems / Zuleger, F. (2015). Asymptotically Precise Ranking Functions for Deterministic Size-Change Systems. In Lecture Notes in Computer Science (pp. 426–442). Springer. https://doi.org/10.1007/978-3-319-20297-6_27
  • 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
  • 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
  • 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

2013

  • 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
  • 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
  • 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
  • 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
  • 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
  • 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 Lecture Notes in Computer Science (pp. 138–154). Springer / LNCS. https://doi.org/10.1007/978-3-642-40624-9_9
  • 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
  • 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

  • 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
  • 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
  • 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
  • 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
  • Wait-Free Stabilizing Dining Using Regular Registers / Sastry, S., Welch, J. L., & Widder, J. (2012). Wait-Free Stabilizing Dining Using Regular Registers. In Lecture Notes in Computer Science (pp. 284–299). LNCS / Springer. https://doi.org/10.1007/978-3-642-35476-2_20
  • 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
  • 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
  • Efficient Checking of Link-Reversal-Based Concurrent Systems / Függer, M., & Widder, J. (2012). Efficient Checking of Link-Reversal-Based Concurrent Systems. In Lecture Notes in Computer Science (pp. 486–499). Lecture Notes in Computer Science. Springer Verlag. https://doi.org/10.1007/978-3-642-32940-1_34
  • Bounded-Interference Sequentialization for Testing Concurrent Programs / Razavi, N., Farzan, A., & Holzer, A. (2012). Bounded-Interference Sequentialization for Testing Concurrent Programs. In Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change (pp. 372–387). Lecture Notes in Computer Science. Springer Verlag. https://doi.org/10.1007/978-3-642-34026-0_28

2011

2010

  • 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
  • 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
  • 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
  • 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
  • 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)
  • Timely Time Estimates / Holzer, A., Januzaj, V., Kugele, S., & Tautschnig, M. (2010). Timely Time Estimates. In T. Margaria & B. Steffen (Eds.), Lecture Notes in Computer Science (pp. 33–46). Lecture Notes in Computer Science. https://doi.org/10.1007/978-3-642-16558-0_5
  • 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
  • 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
  • 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.), Lecture Notes in Computer Science (pp. 18–32). Lecture Notes in Computer Science. https://doi.org/10.1007/978-3-642-16558-0_4

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

 

2024

2023

2022

2021

2020

2019

2018

2016

2015

2014

2013

2003

 

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

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 .