2024W

• Bachelor Thesis / 184.695 / PR
• Doctoral & Master Students Seminar / 181.224 / SE
• Formal Methods in Computer Science / 185.A93 / UE
• Formal Methods in Computer Science / 185.291 / VU
• Introduction to Logical Methods in Computer Science / 184.766 / VO
• Orientation Bachelor with Honors of Informatics and Business Informatics / 180.767 / SE
• Program Analysis / 184.703 / VU
• Project in Computer Science 1 / 192.021 / PR
• Project in Computer Science 2 / 192.022 / PR
• Research Seminar LogiCS / 184.767 / SE
• Scientific Research and Writing / 193.052 / SE
• Seminar for Master Students in Logic and Computation / 180.773 / SE
• Seminar Formal Methods / 181.221 / SE

2025S

• Doctoral & Master Students Seminar / 181.224 / SE
• Introduction to Logical Methods in Computer Science / 184.766 / VO
• Logic and Reasoning in Computer Science / 192.033 / VU
• Program and System Verification / 184.741 / VU
• Project in Computer Science 1 / 192.021 / PR
• Project in Computer Science 2 / 192.022 / PR
• Research Seminar LogiCS / 184.767 / SE
• Semantics of Programming Languages / 184.749 / VU
• Seminar Formal Methods / 181.221 / SE

• Combining Computer Algebra with SAT for Word-Level Reasoning
  2024 – 2027 / Austrian Science Fund (FWF)
• CGC - Changing Gendered Cultures
  2024 – 2026 / WWTF Wiener Wissenschafts-, Forschu und Technologiefonds
• QuAT: Quantifiers and Arithmetic Theories are Friends with Benefits
  2024 – 2025 / Amazon Research Awards
• Effective Formal Methods for Smart-Contract Certification
  2023 – 2027 / Vienna Science and Technology Fund (WWTF)
  Publications: 192933 / 199514 / 199522 / 203882 / 203672 / 202379 / 203892 / 204116 / 205356 / 205513
• Automated Sublinear Amortised Resource Analysis of Data Structures
  2023 – 2027 / Austrian Science Fund (FWF)
• Co-Creationspace Einreichung Transformer
  2023 – 2026 / Fürst Möbel GmbH
• Semantic and Cryptographic Foundations of Security and Privacy by Compositional Design
  2023 – 2026 / Austrian Science Fund (FWF)
  Publications: 189688 / 190634 / 190025 / 193102 / 192933 / 193926 / 192946 / 193074 / 195542 / 199514 / 199522 / 200038 / 200888 / 200903 / 200896 / 200893 / 202379 / 202600 / 203695 / 203892 / 203814 / 203816 / 204116 / 204344 / 204483 / 204345
• Abenteuer Informatik für Volksschulen
  2023 – 2025 / BUNDESMINISTERIN FÜR FRAUEN, FAMILIE, INTEGRATION UND MEDIEN
  Publication: 189688
• Game-theoretic modelling of the fAsset protocol
  2023 – 2024 / Flare Networks Limited
• Automated Cost Analysis of Data Structures
  2023 – 2024 / Amazon Research Awards
• Automated Reasoning with Theories and Induction for Software Technologies
  2021 – 2026 / European Commission
  Publications: 152197 / 177097 / 154343 / 139734 / 152387 / 144346 / 150329 / 153774 / 150352 / 142174 / 153940 / 153941 / 154268 / 153819 / 153259 / 154161 / 153840 / 153839 / 153838 / 153837 / 153258 / 153836 / 153834 / 146113 / 193882 / 175984 / 177657 / 188020 / 188037 / 187706 / 18556 / 18557 / 18558 / 190634 / 190028 / 191945 / 192519 / 191930 / 193254 / 192768 / 193203 / 192933 / 193131 / 192842 / 192672 / 193926 / 192673 / 192946 / 193074 / 195542 / 199514 / 203670 / 203666 / 19886 / 101800
• Incremental SAT and SMT Reasoning for Scalable Verification
  2021 – 2024 / Austrian Science Fund (FWF)
  Publications: 189828 / 193053
• FOREST: First-Order Reasoning for Ensuring System Security
  2021 – 2022 / Amazon Research Awards
• Distribution Recovery for Invariant Generation of Probabilistic Programs
  2020 – 2025 / Vienna Science and Technology Fund (WWTF)
  Publications: 139734 / 146113 / 193882 / 188020 / 188037 / 187706 / 190598 / 191945 / 192191 / 192178 / 192195 / 193131 / 192842 / 192672 / 192673 / 203670 / 203666 / 202371 / 202379 / 202373 / 19886 / 101800
• AutoTest
  2020 – 2021 / Vienna Science and Technology Fund (WWTF)
• Algorithms think differently
  2019 – 2022 / Federal Ministry of Transport, Innovation and Technology (bm:vit)
• Formal methods for Realistic Environments in MAS
  2019 – 2022 / Austrian Science Fund (FWF)
  Publication: 193997
• Symbol Elimination in Reliable System Engineering
  2019 – 2020 / European Commission
  Publications: 16308 / 16309 / 16998
• Domain-Specific Reasoning in IoT Applications
  2019 – 2020 / DoS-IoT
  Publication: 16998
• Holonomic Sequences in Program Verification
  2018 – 2021 / Austrian Science Fund (FWF)
• LogiCs-Scholarships
  2017 – 2025 / LCS
  Publications: 188020 / 190648 / 192587 / 198885
• Symbolic Computation and Automated Reasoning for Program Analysis
  2016 – 2021 / European Commission
  Publications: 16308 / 16309 / 16998 / 18556 / 18557 / 18558
• Bit-level Accurate Reasoning and Interpolation
  2016 – 2020 / Microsoft Research Limited
  Publications: 56283 / 57273
• Tools for Concurrent and distributed Systems
  2011 – 2019 / Austrian Science Fund (FWF)
  Publication: 53696

2024

• Solving String Constraints with Concatenation Using SAT / Lotz, K., Goel, A., Dutertre, B., Kiesl-Reiter, B., Kong, S., & Nowotka, D. (2024). Solving String Constraints with Concatenation Using SAT. In N. Narodytska & P. Rümmer (Eds.), Proceedings of the 24th Conference on Formal Methods in Computer-Aided Design – FMCAD 2024 (pp. 29–38). TU Wien Academic Press. https://doi.org/10.34727/2024/isbn.978-3-85448-065-5_9
  Download: Solving String Constraints with Concatenation Using SAT (909 KB)
• Leveraging LLMs for Program Verification / Kamath, A., Mohammed, N., Senthilnathan, A., Chakraborty, S., Deligiannis, P., Lahiri, S. K., Lal, A., Rastogi, A., Roy, S., & Sharma, R. (2024). Leveraging LLMs for Program Verification. In N. Narodytska & P. Rümmer (Eds.), Proceedings of the 24th Conference on Formal Methods in Computer-Aided Design – FMCAD 2024 (pp. 107–118). TU Wien Academic Press. https://doi.org/10.34727/2024/isbn.978-3-85448-065-5_16
  Download: Leveraging LLMs for Program Verification (581 KB)
• The FMCAD 2024 Student Forum / Blicha, M., & Tsiskaridze, N. (2024). The FMCAD 2024 Student Forum. In N. Narodytska & P. Rümmer (Eds.), Proceedings of the 24th Conference on Formal Methods in Computer-Aided Design – FMCAD 2024 (pp. 5–6). TU Wien Academic Press. https://doi.org/10.34727/2024/isbn.978-3-85448-065-5_5
  Download: The FMCAD 2024 Student Forum (83.4 KB)
• Recomposition: A New Technique for Efficient Compositional Verification / Dardik, I., Porter, A., & Kang, E. (2024). Recomposition: A New Technique for Efficient Compositional Verification. In N. Narodytska & P. Rümmer (Eds.), Proceedings of the 24th Conference on Formal Methods in Computer-Aided Design – FMCAD 2024 (pp. 130–141). TU Wien Academic Press. https://doi.org/10.34727/2024/isbn.978-3-85448-065-5_18
  Download: Recomposition: A New Technique for Efficient Compositional Verification (514 KB)
• Hardware Model Checking Competition 2024 / Biere, A., Froleyks, N., & Preiner, M. (2024). Hardware Model Checking Competition 2024. In N. Narodytska & P. Rümmer (Eds.), Proceedings of the 24th Conference on Formal Methods in Computer-Aided Design – FMCAD 2024 (pp. 7–7). TU Wien Academic Press. https://doi.org/10.34727/2024/isbn.978-3-85448-065-5_6
  Download: Hardware Model Checking Competition 2024 (90 KB)
• Clausal Equivalence Sweeping / Biere, A., Fazekas, K., Fleury, M., & Froleyks, N. (2024). Clausal Equivalence Sweeping. In N. Narodytska & P. Rümmer (Eds.), Proceedings of the 24th Conference on Formal Methods in Computer-Aided Design – FMCAD 2024 (pp. 236–241). TU Wien Academic Press. https://doi.org/10.34727/2024/isbn.978-3-85448-065-5_29
  Download: Clausal Equivalence Sweeping (688 KB)
• Symbolic Computer Algebra for Multipliers Revisited - It's All About Orders and Phases / Konrad, A., & Scholl, C. (2024). Symbolic Computer Algebra for Multipliers Revisited - It’s All About Orders and Phases. In N. Narodytska & P. Rümmer (Eds.), Proceedings of the 24th Conference on Formal Methods in Computer-Aided Design – FMCAD 2024 (pp. 261–271). TU Wien Academic Press. https://doi.org/10.34727/2024/isbn.978-3-85448-065-5_32
  Download: Symbolic Computer Algebra for Multipliers Revisited - It’s All About Orders and Phases (687 KB)
• Semi-open-state testing for in-silicon coherent interconnects / Schult, J., Fiedler, B., Cock, D., & Roscoe, T. (2024). Semi-open-state testing for in-silicon coherent interconnects. In N. Narodytska & P. Rümmer (Eds.), Proceedings of the 24th Conference on Formal Methods in Computer-Aided Design – FMCAD 2024 (pp. 153–162). TU Wien Academic Press. https://doi.org/10.34727/2024/isbn.978-3-85448-065-5_21
  Download: Semi-open-state testing for in-silicon coherent interconnects (325 KB)
• Formally Verifying Deep Reinforcement Learning Controllers with Lyapunov Barrier Certificates / Mandal, U., Amir, G., Wu, H., Daukantas, I., Newell, F. L., Ravaioli, U. J., Meng, B., Durling, M., Ganai, M., Shim, T., Katz, G., & Barrett, C. (2024). Formally Verifying Deep Reinforcement Learning Controllers with Lyapunov Barrier Certificates. In N. Narodytska & P. Rümmer (Eds.), Proceedings of the 24th Conference on Formal Methods in Computer-Aided Design – FMCAD 2024 (pp. 95–106). TU Wien Academic Press. https://doi.org/10.34727/2024/isbn.978-3-85448-065-5_15
  Download: Formally Verifying Deep Reinforcement Learning Controllers with Lyapunov Barrier Certificates (612 KB)
• Formally Verified Rounding Errors of the Logarithm-Sum-Exponential Function / Bonnot, P., Boyer, B., Faissole, F., Marché, C., & Rieu-Helft, R. (2024). Formally Verified Rounding Errors of the Logarithm-Sum-Exponential Function. In N. Narodytska & P. Rümmer (Eds.), Proceedings of the 24th Conference on Formal Methods in Computer-Aided Design – FMCAD 2024 (pp. 251–260). TU Wien Academic Press. https://doi.org/10.34727/2024/isbn.978-3-85448-065-5_31
  Download: Formally Verified Rounding Errors of the Logarithm-Sum-Exponential Function (468 KB)
• Ownership in low-level intermediate representation / Priya, S., & Gurfinkel, A. (2024). Ownership in low-level intermediate representation. In N. Narodytska & P. Rümmer (Eds.), Proceedings of the 24th Conference on Formal Methods in Computer-Aided Design – FMCAD 2024 (pp. 292–300). TU Wien Academic Press. https://doi.org/10.34727/2024/isbn.978-3-85448-065-5_35
  Download: Ownership in low-level intermediate representation (455 KB)
• SMT-D: New Strategies for Portfolio-Based SMT Solving / Barrett, C., Chen, P.-W., Cook, B., Dutertre, B., Jones, R. B., Le, N., Reynolds, A., Sheth, K., Stephens, C., & Whalen, M. W. (2024). SMT-D: New Strategies for Portfolio-Based SMT Solving. In N. Narodytska & P. Rümmer (Eds.), Proceedings of the 24th Conference on Formal Methods in Computer-Aided Design – FMCAD 2024 (pp. 39–48). TU Wien Academic Press. https://doi.org/10.34727/2024/isbn.978-3-85448-065-5_10
  Download: SMT-D: New Strategies for Portfolio-Based SMT Solving (1.41 MB)
• Easter Egg: Equality Reasoning Based on E-Graphs with Multiple Assumptions / Singher, E., & Shachar, I. (2024). Easter Egg: Equality Reasoning Based on E-Graphs with Multiple Assumptions. In N. Narodytska & P. Rümmer (Eds.), Proceedings of the 24th Conference on Formal Methods in Computer-Aided Design – FMCAD 2024 (pp. 70–83). TU Wien Academic Press. https://doi.org/10.34727/2024/isbn.978-3-85448-065-5_13
  Download: Easter Egg: Equality Reasoning Based on E-Graphs with Multiple Assumptions (1.07 MB)
• Efficiently Synthesizing Lowest Cost Rewrite Rules for Instruction Selection / Daly, R., Donovick, C., Terrill, C., Melchert, J., Raina, P., Barrett, C., & Hanrahan, P. (2024). Efficiently Synthesizing Lowest Cost Rewrite Rules for Instruction Selection. In N. Narodytska & P. Rümmer (Eds.), Proceedings of the 24th Conference on Formal Methods in Computer-Aided Design – FMCAD 2024 (pp. 8–17). TU Wien Academic Press. https://doi.org/10.34727/2024/isbn.978-3-85448-065-5_7
  Download: Efficiently Synthesizing Lowest Cost Rewrite Rules for Instruction Selection (540 KB)
• Memory Consistency Model-Aware Cache Coherence for Heterogeneous Hardware / Cleaveland, R., & Trippel, C. (2024). Memory Consistency Model-Aware Cache Coherence for Heterogeneous Hardware. In N. Narodytska & P. Rümmer (Eds.), Proceedings of the 24th Conference on Formal Methods in Computer-Aided Design – FMCAD 2024 (pp. 163–174). TU Wien Academic Press. https://doi.org/10.34727/2024/isbn.978-3-85448-065-5_22
  Download: Memory Consistency Model-Aware Cache Coherence for Heterogeneous Hardware (757 KB)
• Translating Natural Language to Temporal Logics with Large Language Models and Model Checkers / Mendoza, D., Hahn, C., & Trippel, C. (2024). Translating Natural Language to Temporal Logics with Large Language Models and Model Checkers. In N. Narodytska & P. Rümmer (Eds.), Proceedings of the 24th Conference on Formal Methods in Computer-Aided Design – FMCAD 2024 (pp. 119–129). TU Wien Academic Press. https://doi.org/10.34727/2024/isbn.978-3-85448-065-5_17
  Download: Translating Natural Language to Temporal Logics with Large Language Models and Model Checkers (1.83 MB)
• Extending DRAT to SMT / Hitharth, S., Codel, C., Lachnitt, H., & Dutertre, B. (2024). Extending DRAT to SMT. In N. Narodytska & P. Rümmer (Eds.), Extending DRAT to SMT (pp. 18–28). TU Wien Academic Press. https://doi.org/10.34727/2024/isbn.978-3-85448-065-5_8
  Download: Extending DRAT to SMT (539 KB)
• Automatic Verification of Right-greedy Numerical Linear Algebra Algorithms / Kwan, C., & Hunt, W. A., Jr. (2024). Automatic Verification of Right-greedy Numerical Linear Algebra Algorithms. In N. Narodytska & P. Rümmer (Eds.), Proceedings of the 24th Conference on Formal Methods in Computer-Aided Design – FMCAD 2024 (pp. 242–250). TU Wien Academic Press. https://doi.org/10.34727/2024/isbn.978-3-85448-065-5_30
  Download: Automatic Verification of Right-greedy Numerical Linear Algebra Algorithms (265 KB)
• Tackling Scalability Issues in Bit-Vector Reasoning / Niemetz, A. (2024). Tackling Scalability Issues in Bit-Vector Reasoning. In N. Narodytska & P. Rümmer (Eds.), Proceedings of the 24th Conference on Formal Methods in Computer-Aided Design – FMCAD 2024 (pp. 2–2). TU Wien Academic Press. https://doi.org/10.34727/2024/isbn.978-3-85448-065-5_2
  Download: Tackling Scalability Issues in Bit-Vector Reasoning (68.7 KB)
• Context Pruning for More Robust SMT-based Program Verification / Zhou, Y., Bosamiya, J., Li, J. G., Heule, M. J. H., & Parno, B. (2024). Context Pruning for More Robust SMT-based Program Verification. In N. Narodytska & P. Rümmer (Eds.), Proceedings of the 24th Conference on Formal Methods in Computer-Aided Design – FMCAD 2024 (pp. 59–69). TU Wien Academic Press. https://doi.org/10.34727/2024/isbn.978-3-85448-065-5_12
  Download: Context Pruning for More Robust SMT-based Program Verification (685 KB)
• Towards Verification Modulo Theories of asynchronous systems via abstraction refinement / Redondi, G., Cimatti, A., & Griggio, A. (2024). Towards Verification Modulo Theories of asynchronous systems via abstraction refinement. In N. Narodytska & P. Rümmer (Eds.), Proceedings of the 24th Conference on Formal Methods in Computer-Aided Design – FMCAD 2024 (pp. 148–152). TU Wien Academic Press. https://doi.org/10.34727/2024/isbn.978-3-85448-065-5_20
  Download: Towards Verification Modulo Theories of asynchronous systems via abstraction refinement (268 KB)
• Combining Symbolic Execution with Predicate Abstraction and CEGAR / Jonáš, M., Strejcek, J., & Griggio, A. (2024). Combining Symbolic Execution with Predicate Abstraction and CEGAR. In N. Narodytska & P. Rümmer (Eds.), Proceedings of the 24th Conference on Formal Methods in Computer-Aided Design – FMCAD 2024 (pp. 272–280). TU Wien Academic Press. https://doi.org/10.34727/2024/isbn.978-3-85448-065-5_33
  Download: Combining Symbolic Execution with Predicate Abstraction and CEGAR (582 KB)
• Efficient Synthesis of Symbolic Distributed Protocols by Sketching / Egolf, D., Schultz, W., & Tripakis, S. (2024). Efficient Synthesis of Symbolic Distributed Protocols by Sketching. In N. Narodytska & P. Rümmer (Eds.), Proceedings of the 24th Conference on Formal Methods in Computer-Aided Design – FMCAD 2024 (pp. 281–291). TU Wien Academic Press. https://doi.org/10.34727/2024/isbn.978-3-85448-065-5_34
  Download: Efficient Synthesis of Symbolic Distributed Protocols by Sketching (294 KB)
• Modernizing SMT-Based Type Error Localization / Kopinsky, M., Pientka, B., & Si, X. (2024). Modernizing SMT-Based Type Error Localization. In N. Narodytska & P. Rümmer (Eds.), Proceedings of the 24th Conference on Formal Methods in Computer-Aided Design – FMCAD 2024 (pp. 49–58). TU Wien Academic Press. https://doi.org/10.34727/2024/isbn.978-3-85448-065-5_11
  Download: Modernizing SMT-Based Type Error Localization (307 KB)
• Verified Substitution Redundancy Checking / Codel, C., Avigad, J., & Heule, M. J. H. (2024). Verified Substitution Redundancy Checking. In N. Narodytska & P. Rümmer (Eds.), Proceedings of the 24th Conference on Formal Methods in Computer-Aided Design – FMCAD 2024 (pp. 186–196). TU Wien Academic Press. https://doi.org/10.34727/2024/isbn.978-3-85448-065-5_24
  Download: Verified Substitution Redundancy Checking (478 KB)
• Toward Exhaustive Sequential Redundancy Removal / Dureja, R., Baumgartner, J., Gajavelly, R. K., Kanzelman, R., & Rozier, K. Y. (2024). Toward Exhaustive Sequential Redundancy Removal. In N. Narodytska & P. Rümmer (Eds.), Proceedings of the 24th Conference on Formal Methods in Computer-Aided Design – FMCAD 2024 (pp. 217–226). TU Wien Academic Press. https://doi.org/10.34727/2024/isbn.978-3-85448-065-5_27
  Download: Toward Exhaustive Sequential Redundancy Removal (599 KB)
• DAG-Based Compositional Approaches for LTLf to DFA Conversions / Bansal, S., Kankariya, Y., & Li, Y. (2024). DAG-Based Compositional Approaches for LTLf to DFA Conversions. In N. Narodytska & P. Rümmer (Eds.), Proceedings of the 24th Conference on Formal Methods in Computer-Aided Design – FMCAD 2024 (pp. 227–235). TU Wien Academic Press. https://doi.org/10.34727/2024/isbn.978-3-85448-065-5_28
  Download: DAG-Based Compositional Approaches for LTLf to DFA Conversions (315 KB)
• Translating Pseudo-Boolean Proofs into Boolean Clausal Proofs / Nukala, K., Choudhuri, S., Bryant, R., & Heule, M. J. H. (2024). Translating Pseudo-Boolean Proofs into Boolean Clausal Proofs. In N. Narodytska & P. Rümmer (Eds.), Proceedings of the 24th Conference on Formal Methods in Computer-Aided Design – FMCAD 2024 (pp. 175–185). TU Wien Academic Press. https://doi.org/10.34727/2024/isbn.978-3-85448-065-5_23
  Download: Translating Pseudo-Boolean Proofs into Boolean Clausal Proofs (423 KB)
• 2-DQBF Solving and Certification via Property-Directed Reachability Analysis / Fung, L.-H., Cheng, C., Fan, Y.-W., Tan, T., & Jiang, J.-H. R. (2024). 2-DQBF Solving and Certification via Property-Directed Reachability Analysis. In N. Narodytska & P. Rümmer (Eds.), Proceedings of the 24th Conference on Formal Methods in Computer-Aided Design – FMCAD 2024 (pp. 197–207). TU Wien Academic Press. https://doi.org/10.34727/2024/isbn.978-3-85448-065-5_25
  Download: 2-DQBF Solving and Certification via Property-Directed Reachability Analysis (596 KB)
• Evaluating LLM-driven User-Intent Formalization for Verification-Aware Languages / Lahiri, S. K. (2024). Evaluating LLM-driven User-Intent Formalization for Verification-Aware Languages. In N. Narodytska & P. Rümmer (Eds.), Proceedings of the 24th Conference on Formal Methods in Computer-Aided Design – FMCAD 2024 (pp. 142–147). TU Wien Academic Press. https://doi.org/10.34727/2024/isbn.978-3-85448-065-5_19
  Download: Evaluating LLM-driven User-Intent Formalization for Verification-Aware Languages (262 KB)
• Writing Proofs in Dafny / Leino, R. (2024). Writing Proofs in Dafny. In N. Narodytska & P. Rümmer (Eds.), Proceedings of the 24th Conference on Formal Methods in Computer-Aided Design – FMCAD 2024 (pp. 1–1). TU Wien Academic Press. https://doi.org/10.34727/2024/isbn.978-3-85448-065-5_1
  Download: Writing Proofs in Dafny (66.3 KB)
• Projective Model Counting for IP Addresses in Access Control Policies / D’Antoni, L., Gacek, A., Goel, A., Jovanovic, D., Kıcı, R. G., Peebles, D., Rungta, N., Sharoda, Y., & Sung, C. (2024). Projective Model Counting for IP Addresses in Access Control Policies. In N. Narodytska & P. Rümmer (Eds.), Proceedings of the 24th Conference on Formal Methods in Computer-Aided Design – FMCAD 2024 (pp. 208–216). TU Wien Academic Press. https://doi.org/10.34727/2024/isbn.978-3-85448-065-5_26
  Download: Projective Model Counting for IP Addresses in Access Control Policies (292 KB)
• Harnessing SMT Solvers for Reasoning about DeFi Protocols / Sagiv, M. (2024). Harnessing SMT Solvers for Reasoning about DeFi Protocols. In N. Narodytska & P. Rümmer (Eds.), Proceedings of the 24th Conference on Formal Methods in Computer-Aided Design – FMCAD 2024 (pp. 4–4). TU Wien Academic Press. https://doi.org/10.34727/2024/isbn.978-3-85448-065-5_4
  Download: Harnessing SMT Solvers for Reasoning about DeFi Protocols (67.8 KB)
• Word Equations as Abstract Domain for String Manipulating Programs / Nepeivoda, A. (2024). Word Equations as Abstract Domain for String Manipulating Programs. In N. Narodytska & P. Rümmer (Eds.), Proceedings of the 24th Conference on Formal Methods in Computer-Aided Design – FMCAD 2024 (pp. 84–94). TU Wien Academic Press. https://doi.org/10.34727/2024/isbn.978-3-85448-065-5_14
  Download: Word Equations as Abstract Domain for String Manipulating Programs (504 KB)
• Proceedings of the 24th Conference on Formal Methods in Computer-Aided Design – FMCAD 2024 / Narodytska, N., & Rümmer, P. (Eds.). (2024). Proceedings of the 24th Conference on Formal Methods in Computer-Aided Design – FMCAD 2024. TU Wien Academic Press. https://doi.org/10.34727/2024/isbn.978-3-85448-065-5
  Downloads: Proceedings of the 24th Conference on Formal Methods in Computer- Aided Design – FMCAD 2024 (11.2 MB) / Front Matter (367 KB)
• Some Adventures in Learning Proving, Instantiation and Synthesis / Urban, J. (2024). Some Adventures in Learning Proving, Instantiation and Synthesis. In N. Narodytska & P. Rümmer (Eds.), Proceedings of the 24th Conference on Formal Methods in Computer-Aided Design – FMCAD 2024 (pp. 3–3). TU Wien Academic Press. https://doi.org/10.34727/2024/isbn.978-3-85448-065-5_3
  Download: Some Adventures in Learning Proving, Instantiation and Synthesis (68.5 KB)
• With Biabduction towards Memory Safety across the Rust-C-FFI / Sextl, F. (2024, September 17). With Biabduction towards Memory Safety across the Rust-C-FFI [Presentation]. Doctoral Symposium, TU Wien, Austria. http://hdl.handle.net/20.500.12708/204201
• Exact and Approximate Moment Derivation for Probabilistic Loops With Non-Polynomial Assignments / Kofnov, A., Moosbrugger, M., Stankovic, M., Bartocci, E., & Bura, E. (2024). Exact and Approximate Moment Derivation for Probabilistic Loops With Non-Polynomial Assignments. ACM Transactions on Modeling and Computer Simulation, 34(3), Article 18. https://doi.org/10.1145/3641545
  Download: PDF (2.59 MB)
  Projects: ARTIST (2021–2026) / ProbInG (2020–2025)
• Distillation based Robustness Verification with PAC Guarantees / Indri, P., Blohm, P., Athavale, A., Bartocci, E., Weissenbacher, G., Maffei, M., Nickovic, D., Gärtner, T., & Malhotra, S. (2024). Distillation based Robustness Verification with PAC Guarantees. In Volume 235: International Conference on Machine Learning, 21-27 July 2024, Vienna, Austria. 41st International Conference on Machine Learning (ICML 2024), Vienna, Austria. http://hdl.handle.net/20.500.12708/200890
• High-yield liquid phase exfoliation of graphene utilizing low boiling co-solvent solutions and ammonia / Nastran, M., Peschek, P., Walendzik, I., Rath, J., Fickl, B., Schubert, J. S., Szabo, G., Wilhelm, R. A., Schmidt, J., Eder, D., & Bayer-Skoff, B. (2024, June 24). High-yield liquid phase exfoliation of graphene utilizing low boiling co-solvent solutions and ammonia [Poster Presentation]. NT24, Cambridge, Boston, United States of America (the). http://hdl.handle.net/20.500.12708/203125
• Logical Distillation of Graph Neural Networks / Pluska, A., Welke, P., Gärtner, T., & Malhotra, S. (2024). Logical Distillation of Graph Neural Networks. In ICML 2024 Workshop on Mechanistic Interpretability. 21st International Conference on Principles of Knowledge Representation and Reasoning, Hanoi, Viet Nam. https://doi.org/10.34726/7099
  Download: PDF (309 KB)
  Project: StruDL (2023–2027)
• (Un)Solvable loop analysis / Amrollahi, D., Bartocci, E., Kenison, G. J., Kovacs, L., Moosbrugger, M., & Stankovic, M. (2024). (Un)Solvable loop analysis. Formal Methods in System Design. https://doi.org/10.1007/s10703-024-00455-0
  Projects: ARTIST (2021–2026) / ProbInG (2020–2025)
• VIRAS: Conflict-Driven Quantifier Elimination for Integer-Real Arithmetic / Schoisswohl, J., Kovács, L., & Korovin, K. (2024). VIRAS: Conflict-Driven Quantifier Elimination for Integer-Real Arithmetic. In N. Bjørner, M. Heule, & A. Voronkov (Eds.), Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning (pp. 147–164). https://doi.org/10.29007/kg4v
  Download: PDF (597 KB)
  Projects: ForSmart (2023–2027) / SFB SPyCoDe (2023–2026)
• Saturating Sorting without Sorts / Georgiou, P., Hajdu, M., & Kovács, L. (2024). Saturating Sorting without Sorts. arXiv. https://doi.org/10.34726/5861
  Download: Preprint (322 KB)
  Projects: ARTIST (2021–2026) / SFB SPyCoDe (2023–2026)
• Fuzzing-based grammar learning from a minimal set of seed inputs / Sochor, H., Ferrarotti, F., & Kaufmann, D. (2024). Fuzzing-based grammar learning from a minimal set of seed inputs. JOURNAL OF COMPUTER LANGUAGES, 78, Article 101252. https://doi.org/10.1016/j.cola.2023.101252
  Project: ARTIST (2021–2026)
• Finding counterexamples to ∀∃ hyperproperties / Nießen, T., & Weissenbacher, G. (2024, January 16). Finding counterexamples to ∀∃ hyperproperties [Conference Presentation]. Formal Methods for Incorrectness 2024, London, United Kingdom of Great Britain and Northern Ireland (the). https://doi.org/10.34726/5455
  Download: Extended abstract (432 KB)
• Strong Invariants Are Hard: On the Hardness of Strongest Polynomial Invariants for (Probabilistic) Programs / Müllner, J., Moosbrugger, M., & Kovács, L. (2024). Strong Invariants Are Hard: On the Hardness of Strongest Polynomial Invariants for (Probabilistic) Programs. Proceedings of the ACM on Programming Languages, 8(POPL), 882–910. https://doi.org/10.1145/3632872
• Strongly Analytic Calculi for KLM Logics with SMT-Based Prover / Ciabattoni, A., Eisenhofer, C., & Rozplokhas, D. (2024). Strongly Analytic Calculi for KLM Logics with SMT-Based Prover. In Proceedings of the 21st International Conference on Principles of Knowledge Representation and Reasoning (pp. 284–294). https://doi.org/10.24963/kr.2024/27
  Project: TAIGER (2023–2027)
• Verifying Global Two-Safety Properties in Neural Networks with Confidence / Athavale, A., Bartocci, E., Christakis, M., Maffei, M., Ničković, D., & Weissenbacher, G. (2024). Verifying Global Two-Safety Properties in Neural Networks with Confidence. In A. Gurfinkel & V. Ganesh (Eds.), Computer Aided Verification (pp. 329–351). Springer. https://doi.org/10.1007/978-3-031-65630-9_17
  Projects: Browsec (2018–2024) / ForSmart (2023–2027) / ProbInG (2020–2025) / SFB SPyCoDe (2023–2026) / TAIGER (2023–2027)
• Scaling CheckMate for Game-Theoretic Security / Rain, S., Brugger, L. S., Petković Komel, A., Kovács, L., & Rawson, M. (2024). Scaling CheckMate for Game-Theoretic Security. In N. Bjorner, M. Heule, & A. Voronkov (Eds.), Proceedings of 25th Conference on Logic for Pro gramming, Artificial Intelligence and Reasoning (pp. 222–231). https://doi.org/10.29007/llnq
• Synthesis of Recursive Programs in Saturation / Hozzová, P., Amrollahi, D., Hajdu, M., Kovács, L., Voronkov, A., & Wagner, E. M. (2024). Synthesis of Recursive Programs in Saturation. In Automated Reasoning: 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3–6, 2024, Proceedings, Part I (pp. 154–171). Springer International Publishing. https://doi.org/10.1007/978-3-031-63498-7_10
• Reducibility Constraints in Superposition / Hajdu, M., Kovács, L., Rawson, M., & Voronkov, A. (2024). Reducibility Constraints in Superposition. In Automated Reasoning: 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3–6, 2024, Proceedings, Part I (pp. 115–132). https://doi.org/10.1007/978-3-031-63498-7_8
  Download: PDF (541 KB)
• Induction in Saturation / Kovács, L., Hozzová, P., Hajdu, M., & Voronkov, A. (2024). Induction in Saturation. In Automated Reasoning: 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3–6, 2024, Proceedings, Part I (pp. 21–29). Springer. https://doi.org/10.1007/978-3-031-63498-7_2
  Download: Verlags-PDF (345 KB)
  Projects: ARTIST (2021–2026) / ForSmart (2023–2027) / SFB SPyCoDe (2023–2026)
• CryptoVampire: Automated Reasoning for the Complete Symbolic Attacker Cryptographic Model / Jeanteur, S., Kovács, L., Maffei, M., & Rawson, M. (2024). CryptoVampire: Automated Reasoning for the Complete Symbolic Attacker Cryptographic Model. In 2024 IEEE Symposium on Security and Privacy (SP) (pp. 3165–3183). IEEE. https://doi.org/10.1109/SP54263.2024.00246
  Projects: Browsec (2018–2024) / CDL-BOT (2020–2025) / DLDaI (2022–2024) / ForSmart (2023–2027) / SFB SPyCoDe (2023–2026) / SPFBT (2020–2025)
• Embedding the Connection Calculus in Satisfiability Modulo Theories / Eisenhofer, C., Kovács, L., & Rawson, M. (2024). Embedding the Connection Calculus in Satisfiability Modulo Theories. In Proceedings of the 1st International Workshop on Automated Reasoning with Connection Calculi (AReCCa 2023) (pp. 54–63). CEUR-WS.org. https://doi.org/10.34726/5394
  Download: PDF (248 KB)
  Projects: ARTIST (2021–2026) / ForSmart (2023–2027) / SFB SPyCoDe (2023–2026)

2023

• CheckMate: Automated Game-Theoretic Security Reasoning / Brugger, L. S., Kovács, L., Petkovic Komel, A., Rain, S., & Rawson, M. (2023). CheckMate: Automated Game-Theoretic Security Reasoning. In CCS ’23: Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security (pp. 1407–1421). Association for Computing Machinery. https://doi.org/10.1145/3576915.3623183
  Download: PDF (1.15 MB)
  Project: SFB SPyCoDe (2023–2026)
• Automated Sensitivity Analysis for Probabilistic Loops / Moosbrugger, M., Müllner, J., & Kovács, L. (2023). Automated Sensitivity Analysis for Probabilistic Loops. In P. Herber & A. Wijs (Eds.), iFM 2023 : 18th International Conference, iFM 2023, Leiden, The Netherlands, November 13–15, 2023, Proceedings (pp. 21–39). Springer. https://doi.org/10.1007/978-3-031-47705-8_2
• A Formalization of Heisenbugs and Their Causes / Sallinger, S., Weissenbacher, G., & Zuleger, F. (2023). A Formalization of Heisenbugs and Their Causes. In C. Ferreira & T. A. C. Willemse (Eds.), Software Engineering and Formal Methods : 21st International Conference, SEFM 2023, Eindhoven, The Netherlands, November 6-10, 2023, Proceedings (pp. 282–300). Springer. https://doi.org/10.34726/5381
  Download: Preprint for self-archivation (552 KB)
  Project: ARTIST (2021–2026)
• 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)
• 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)
• 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)
• A provably correct floating-point implementation of Well Clear Avionics Concepts / Bernardes Fernandes Ferreira, N., Moscato, M., Titolo, L., & Ayala-Rincón, M. (2023). A provably correct floating-point implementation of Well Clear Avionics Concepts. In A. Nadel & K. Y. Rozier (Eds.), Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design – FMCAD 2023 (pp. 237–246). TU Wien Academic Press. https://doi.org/10.34727/2023/isbn.978-3-85448-060-0_32
  Download: PDF (427 KB)
• 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)
• 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)
• 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)
• 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)
• 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)
• µArchiFI: Formal Modeling and Verification Strategies for Microarchitetural Fault Injections / Tollec, S., Asavoae, M., Couroussé, D., Heydemann, K., & Jan, M. (2023). µArchiFI: Formal Modeling and Verification Strategies for Microarchitetural Fault Injections. In A. Nadel & K. Y. Rozier (Eds.), Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design – FMCAD 2023 (pp. 101–109). TU Wien Academic Press. https://doi.org/10.34727/2023/isbn.978-3-85448-060-0_18
  Download: PDF (492 KB)
• Btor2MLIR: A Format for Hardware Verification / Tafese, J., Gurfinkel, A., & Garcia-Contreras, I. (2023). Btor2MLIR: A Format for Hardware Verification. In A. Nadel & K. Y. Rozier (Eds.), Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design – FMCAD 2023 (pp. 55–63). TU Wien Academic Press. https://doi.org/10.34727/2023/isbn.978-3-85448-060-0_13
  Download: PDF (324 KB)
• 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)
• 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)
• 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)
• 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)
• 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)
• 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)
• 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)
• 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)
• 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)
• 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)
• 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)
• 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)
• 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)
• 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)
• 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)
• 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)
• 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)
• 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)
• 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)
• 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)
• 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)
• SAT-Based Quantified Symmetric Minimization of the Reachable States of Distributed Protocols / Fazekas, K., Aman, G., & Sakallah, K. (2023). SAT-Based Quantified Symmetric Minimization of the Reachable States of Distributed Protocols. In A. Nadel & K. Y. Rozier (Eds.), Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design – FMCAD 2023 (pp. 152–161). TU Wien Academic Press. https://doi.org/10.34727/2023/isbn.978-3-85448-060-0_23
  Download: PDF (499 KB)
• Verified Encodings for SAT Solvers / Codel, C., Avigad, J., & Heule, M. (2023). Verified Encodings for SAT Solvers. In A. Nadel & K. Y. Rozier (Eds.), Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design – FMCAD 2023 (pp. 141–151). TU Wien Academic Press. https://doi.org/10.34727/2023/isbn.978-3-85448-060-0_22
  Download: PDF (384 KB)
• 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)
• 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)
• 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)
• 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)
• Reshaping Unplugged Computer Science Workshops for Primary School Education / Landman, M., Rain, S., Kovács, L., & Gerald Futschek. (2023). Reshaping Unplugged Computer Science Workshops for Primary School Education. In J.-P. Pellet & G. Parriaux (Eds.), Informatics in Schools. Beyond Bits and Bytes: Nurturing Informatics Intelligence in Education : 16th International Conference on Informatics in Schools: Situation, Evolution, and Perspectives, ISSEP 2023, Lausanne, Switzerland, October 23–25, 2023, Proceedings (pp. 139–151). Springer. https://doi.org/10.1007/978-3-031-44900-0_11
  Download: PDF (1020 KB)
  Projects: AbInfVS (2023–2025) / SFB SPyCoDe (2023–2026)
• Deductive Controller Synthesis for Probabilistic Hyperproperties / Andriushchenko, R., Bartocci, E., Češka, M., Pontiggia, F., & Sallinger, S. S. (2023). Deductive Controller Synthesis for Probabilistic Hyperproperties. In N. Jansen & M. Tribastone (Eds.), Quantitative Evaluation of Systems - 20th International Conference, QEST 2023 (pp. 47–64). Springer. https://doi.org/10.1007/978-3-031-43835-6_20
  Project: ProbInG (2020–2025)
• Non-Classical Logics in Satisfiability Modulo Theories / Eisenhofer, C., Alassaf, R., Rawson, M., & Kovács, L. (2023). Non-Classical Logics in Satisfiability Modulo Theories. In D. R. S. Ramanayake & J. Urban (Eds.), Automated Reasoning with Analytic Tableaux and Related Methods: 32nd International Conference, TABLEAUX 2023, Prague, Czech Republic, September 18–21, 2023, Proceedings (pp. 24–36). Springer. https://doi.org/10.1007/978-3-031-43513-3_2
  Download: PDF (423 KB)
  Projects: ARTIST (2021–2026) / SFB SPyCoDe (2023–2026)
• Lemmas: Generation, Selection, Application / Rawson, M., Wernhard, C., Zombori, Z., & Bibel, W. (2023). Lemmas: Generation, Selection, Application. In D. R. S. Ramanayake & J. Urban (Eds.), Automated Reasoning with Analytic Tableaux and Related Methods: 32nd International Conference, TABLEAUX 2023, Prague, Czech Republic, September 18–21, 2023, Proceedings (pp. 153–174). Springer. https://doi.org/10.1007/978-3-031-43513-3_9
  Project: ARTIST (2021–2026)
• Superposition with Delayed Unification / Bhayat, A., Schoisswohl, J., & Rawson, M. (2023). Superposition with Delayed Unification. In B. Pientka & C. Tinelli (Eds.), Automated Deduction – CADE 29  29th International Conference on Automated Deduction, Rome, Italy, July 1–4, 2023, Proceedings (pp. 23–40). Springer. https://doi.org/10.1007/978-3-031-38499-8_2
  Projects: ARTIST (2021–2026) / SFB SPyCoDe (2023–2026)
• Program Synthesis in Saturation / Hozzová, P., Kovács, L., Norman, C., & Voronkov, A. (2023). Program Synthesis in Saturation. In B. Pientka & C. Tinelli (Eds.), Automated Deduction – CADE 29  29th International Conference on Automated Deduction, Rome, Italy, July 1–4, 2023, Proceedings (pp. 307–324). Springer. https://doi.org/10.1007/978-3-031-38499-8_18
  Download: PDF (528 KB)
  Projects: ARTIST (2021–2026) / DK - Logic (2014–2023)
• 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)
• 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
• 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)
• 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)
• 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)
• Stochastic Best-Effort Strategies for Borel Goals / Aminof, B., De Giacomo, G., Rubin, S., & Zuleger, F. (2023). Stochastic Best-Effort Strategies for Borel Goals. In 2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). 2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Boston, MA, United States of America (the). IEEE. https://doi.org/10.34726/6219
  Download: Personal use of this material is permitted. Permission from IEEE must be obtained for all other uses, in any current or future media, including reprinting/republishing this material for advertising or promotional purposes, creating new collective works, for resale or redistribution to servers or lists, or reuse of any copyrighted component of this work in other works. (456 KB)
  Project: REMASTER (2019–2022)
• Even Shorter Proofs Without New Variables / Rebola Pardo, A. (2023). Even Shorter Proofs Without New Variables. In M. Mahajan & F. Slivovsky (Eds.), 26th International Conference on Theory and Applications of Satisfiability Testing (pp. 22:1-22:20). Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPICS.SAT.2023.22
  Project: LCS (2017–2025)
• Satisfiability Modulo Custom Theories in Z3 / Bjørner, N., Eisenhofer, C., & Kovács, L. (2023). Satisfiability Modulo Custom Theories in Z3. In C. Dragoi, M. Emmi, & J. Wang (Eds.), Verification, Model Checking, and Abstract Interpretation. VMCAI 2023 (pp. 91–105). Springer. https://doi.org/10.1007/978-3-031-24950-1_5
  Project: ARTIST (2021–2026)
• 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)
• 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)
• 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
• 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)
• 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)

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)
• 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)
• 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)
• 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)
• 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)
• 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)
• 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)
• 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)
• Automatic Repair and Deadlock Detection for Parameterized Systems / Jacobs, S., Sakr, M., & Völp, M. (2022). Automatic Repair and Deadlock Detection for Parameterized Systems. In A. Griggio & N. Rungta (Eds.), Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design – FMCAD 2022 (pp. 225–234). TU Wien Academic Press. https://doi.org/10.34727/2022/isbn.978-3-85448-053-2_29
  Download: PDF (374 KB)
• TRICERA Verifying C Programs Using the Theory of Heaps / Esen, Z., & Ruemmer, P. (2022). TRICERA Verifying C Programs Using the Theory of Heaps. In A. Griggio & N. Rungta (Eds.), Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design – FMCAD 2022 (pp. 360–391). TU Wien Academic Press. https://doi.org/10.34727/2022/isbn.978-3-85448-053-2_45
  Download: PDF (458 KB)
• 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)
• 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)
• 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)
• Bounded Model Checking for LLVM / Priya, S., Su, Y., Bao, Y., Zhou, X., Vizel, Y., & Gurfinkel, A. (2022). Bounded Model Checking for LLVM. In A. Griggio & N. Rungta (Eds.), Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design – FMCAD 2022 (pp. 214–224). TU Wien Academic Press. https://doi.org/10.34727/2022/isbn.978-3-85448-053-2_28
  Download: PDF (478 KB)
• Synthesizing Locally Symmetric Parameterized Protocols from Temporal Specifications / Zhang, R., Trefler, R., & Namjoshi, K. (2022). Synthesizing Locally Symmetric Parameterized Protocols from Temporal Specifications. In A. Griggio & N. Rungta (Eds.), Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design – FMCAD 2022 (pp. 235–244). TU Wien Academic Press. https://doi.org/10.34727/2022/isbn.978-3-85448-053-2_30
  Download: PDF (1.16 MB)
• 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)
• 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)
• 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)
• 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)
• 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)
• 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)
• 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)
• 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)
• 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)
• 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)
• 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)
• 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)
• 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)
• 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)
• 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 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)
• 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)
• 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)
• 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)
• 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)
• 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)
• 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)
• 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)
• 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)
• 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)
• 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)
• 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)
• 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)
• 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)
• 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)
• 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)
• 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)
• Lonely Points in Simplices / Jaroschek, M., Kauers, M., & Kovács, L. (2022). Lonely Points in Simplices. Discrete and Computational Geometry, 69, 4–25. https://doi.org/10.1007/s00454-022-00428-2
  Project: ARTIST (2021–2026)
• Getting Saturated with Induction / Kovacs, L. (2022, September 29). Getting Saturated with Induction [Keynote Presentation]. Automated Reasoning Symposium of Amazon Web Services, United States of America (the). http://hdl.handle.net/20.500.12708/153839
  Project: ARTIST (2021–2026)
• Algebra-Based Analysis of Polynomial Probabilistic Programs / Kovacs, L. (2022, September 22). Algebra-Based Analysis of Polynomial Probabilistic Programs [Keynote Presentation]. Distinguished Lecture Series of the Max Planck Institute for Software Systems (MPI-SWS), Germany. http://hdl.handle.net/20.500.12708/153258
  Project: ARTIST (2021–2026)
• User-Propagation for Custom Theories in SMT Solving / Eisenhofer, C. (2022, September 14). User-Propagation for Custom Theories in SMT Solving [Presentation]. 14th Alpine Verification Meeting, Frauenchiemsee, Germany. http://hdl.handle.net/20.500.12708/154343
  Project: ARTIST (2021–2026)
• Distribution Estimation for Probabilistic Loops / Karimi, A., Moosbrugger, M., Stankovič, M., Kovács, L., Bartocci, E., & Bura, E. (2022). Distribution Estimation for Probabilistic Loops. In E. Ábrahám & M. Paolieri (Eds.), Quantitative Evaluation of Systems (pp. 26–42). Springer-Verlag. https://doi.org/10.1007/978-3-031-16336-4_2
  Projects: ARTIST (2021–2026) / ProbInG (2020–2025)
• PolySAT - a word-level solver for large bitvectors / Rath, J., Bjørner, N., Kovacs, L., Nutz, A., & Sagiv, M. (2022, September 1). PolySAT - a word-level solver for large bitvectors [Presentation]. Formal Reasoning about Financial Systems, Stanford, United States of America (the). http://hdl.handle.net/20.500.12708/154065
• Strong-separation Logic (Extended Version) / Pagel, J., & Zuleger, F. (2022). Strong-separation Logic (Extended Version). ACM Letters on Programming Languages and Systems, 44(3), 1–40. https://doi.org/10.1145/3498847
• The Vampire Approach to Induction (short paper) / Hajdu, M., Kovács, L., Rawson, M., & Voronkov, A. (2022). The Vampire Approach to Induction (short paper). In B. Konev, C. Schon, & A. Steen (Eds.), PAAR 2022. Practical Aspects of Automated Reasoning 2022.  Proceedings of the Workshop on Practical Aspects of Automated Reasoning. https://doi.org/10.34726/4103
  Download: PDF (836 KB)
• Reuse of Introduced Symbols in Automatic Theorem Provers / Rawson, M., Suda, M., Hozzová, P., & Reger, G. (2022). Reuse of Introduced Symbols in Automatic Theorem Provers. In B. Konev, C. Schon, & A. Steen (Eds.), PAAR 2022. Practical Aspects of Automated Reasoning 2022.  Proceedings of the Workshop on Practical Aspects of Automated Reasoning. CEUR-WS.org. https://doi.org/10.34726/4343
  Download: PDF (859 KB)
  Project: ARTIST (2021–2026)
• On the Skolem Problem for Reversible Sequences / Kenison, G. (2022). On the Skolem Problem for Reversible Sequences. In 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022) (pp. 61:1-61:15). Schloss Dagstuhl -- Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.MFCS.2022.61
  Projects: ARTIST (2021–2026) / ProbInG (2020–2025)
• User-Propagation for Custom Theories in SMT Solving / Bjorner, N., Eisenhofer, C., & Kovács, L. (2022). User-Propagation for Custom Theories in SMT Solving. In D. Deharbe & A. Hyvärinen (Eds.), Satisfiability Modulo Theories. 20th International Workshop. SMT 2022. Proceedings (pp. 71–79). CEUR-WS.org. https://doi.org/10.34726/4104
  Download: PDF (1.15 MB)
  Project: ARTIST (2021–2026)
• Automating Security Analysis of Off-Chain Protocols / Brugger, L. S., Kovacs, L., Petkovic Komel, A., Rain, S., & Rawson, M. (2022, August 11). Automating Security Analysis of Off-Chain Protocols [Conference Presentation]. 4th International Workshop on Formal Methods for Blockchains, Haifa, Israel. https://doi.org/10.34726/3523
  Download: PDF (265 KB)
  Project: ARTIST (2021–2026)
• Automated Reasoning: 11th International Joint Conference (IJCAR 2022) / Blanchette, J. C., Kovacs, L., & Pattinson, D. (Eds.). (2022). Automated Reasoning: 11th International Joint Conference (IJCAR 2022) (Vol. 13385). Springer-Verlag. https://doi.org/10.1007/978-3-031-10769-6
  Project: ARTIST (2021–2026)
• Automated Expected Amortised Cost Analysis of Probabilistic Data Structures / Leutgeb, L., Moser, G., & Zuleger, F. (2022). Automated Expected Amortised Cost Analysis of Probabilistic Data Structures. In Computer Aided Verification - 34th International Conference, CAV 2022 (pp. 70–91). https://doi.org/10.1007/978-3-031-13188-2_4
• Interpolants and Interference / Rebola Pardo, A. (2022). Interpolants and Interference. In M. Benedikt, P. Rümmer, & C. Wernhard (Eds.), iPRA 2022 : The 4th Workshop on Interpolation: From Proofs to Applications : Book of Abstracts (pp. 27–35). http://hdl.handle.net/20.500.12708/198885
  Project: LCS (2017–2025)
• The probabilistic termination tool amber / Moosbrugger, M., Bartocci, E., Katoen, J.-P., & Kovacs, L. (2022). The probabilistic termination tool amber. Formal Methods in System Design, 61(1), 90–109. https://doi.org/10.1007/s10703-023-00424-z
  Projects: ARTIST (2021–2026) / ProbInG (2020–2025)
• An SMT Approach for Solving Polynomials over Finite Fields / Hader, T., & Kovacs, L. (2022). An SMT Approach for Solving Polynomials over Finite Fields. In Proceedings of the 20th Internal Workshop on Satisfiability Modulo Theories (SMT) (pp. 90–98).
  Project: ARTIST (2021–2026)
• The essence of type-theoretic elaboration / Petkovic Komel, A. (2022, July 31). The essence of type-theoretic elaboration [Conference Presentation]. Women In Logic, Haifa, Israel. http://hdl.handle.net/20.500.12708/153703
  Download: talk slides (1.34 MB)
• 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
• Low-Level Bi-Abduction / Holík, L., Peringer, P., Rogalewicz, A., Šoková, V., Vojnar, T., & Zuleger, F. (2022). Low-Level Bi-Abduction. In 36th European Conference on Object-Oriented Programming (ECOOP 2022) (pp. 1–30). Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.ECOOP.2022.19
  Download: PDF (1.2 MB)
• Automated Reasoning for Trustworthy Software / Kovacs, L. (2022, June 21). Automated Reasoning for Trustworthy Software [Keynote Presentation]. Austrian Computer Science Day 2022, IST Austria, Austria. http://hdl.handle.net/20.500.12708/153819
  Project: ARTIST (2021–2026)
• First-Order Theorem Proving and Vampire / Kovacs, L. (2022, June 17). First-Order Theorem Proving and Vampire [Keynote Presentation]. 15TH SUMMER SCHOOL ON MODELLING AND VERIFICATION OF PARALLEL PROCESSES (MOVEP2022), Aalborg, Denmark. http://hdl.handle.net/20.500.12708/153941
  Project: ARTIST (2021–2026)
• Algebraic Synthesis of Loops and their Invariants / Kovacs, L. (2022, June 6). Algebraic Synthesis of Loops and their Invariants [Conference Presentation]. Workshop on Differential Algebra, Leipzig, Germany. http://hdl.handle.net/20.500.12708/153259
  Project: ARTIST (2021–2026)
• Tests and Proofs / Meinke, K., & Kovacs, L. (Eds.). (2022). Tests and Proofs (Vol. 13361). Springer-Verlag. https://doi.org/10.1007/978-3-031-09827-7
  Project: ARTIST (2021–2026)
• From Truth Degree Comparison Games to Sequents-of-Relations Calculi for Gödel Logic / Fermüller, C., Lang, T. A., & Pavlova, A. (2022). From Truth Degree Comparison Games to Sequents-of-Relations Calculi for Gödel Logic. Logica Universalis, 16(1–2), 221–235. https://doi.org/10.1007/s11787-022-00300-0
  Download: PDF (409 KB)
  Project: SEGACAB (2019–2023)
• Automated Program Reasoning / Kovacs, L. (2022, May 30). Automated Program Reasoning [Keynote Presentation]. Informatics Europe Webinar Series, Switzerland.
  Project: ARTIST (2021–2026)
• The essence of elaboration / Petkovic Komel, A. (2022, May 20). The essence of elaboration [Conference Presentation]. Workshop on Syntax and Semantics of Type Thoery, Stockholm, Sweden. http://hdl.handle.net/20.500.12708/153774
  Download: talk slides (1.62 MB)
  Project: ARTIST (2021–2026)
• Enjoying Research at the Intersection of Math and Computer Science / Kovacs, L. (2022, April 3). Enjoying Research at the Intersection of Math and Computer Science [Keynote Presentation]. ETAPS 2022 Mentoring Workshop, Munich, Germany.
  Project: ARTIST (2021–2026)
• Algebra-Based Reasoning for Loop Synthesis / Humenberger, A., Amrollahi, D., Bjørner, N., & Kovács, L. (2022). Algebra-Based Reasoning for Loop Synthesis. Formal Aspects of Computing, 34(1), 4:31. https://doi.org/10.1145/3527458
  Projects: ARTIST (2021–2026) / ProbInG (2020–2025)
• Automated Instantiation of Control Flow Tracing Exercises / Eisenhofer, C., & Riener, M. (2022). Automated Instantiation of Control Flow Tracing Exercises. In J. Marcos, W. Neuper, & P. Quaresma (Eds.), Proceedings 10th International Workshop on Theorem Proving Components for Educational Software (pp. 43–58). EPTCS. https://doi.org/10.4204/EPTCS.354.4
  Download: PDF (629 KB)
• Verifying safety of synchronous fault-tolerant algorithms by bounded model checking / Stoilkovska, I., Konnov, I., Widder, J., & Zuleger, F. (2022). Verifying safety of synchronous fault-tolerant algorithms by bounded model checking. International Journal on Software Tools for Technology Transfer, 24(1), 33–48. https://doi.org/10.1007/s10009-021-00637-9
• Getting Saturated with Induction / Kovacs, L. (2022, January 27). Getting Saturated with Induction [Conference Presentation]. Automated Reasoning Seminar at TU Kaiserslautern, Kaiserslautern, Germany. http://hdl.handle.net/20.500.12708/153837
  Project: ARTIST (2021–2026)
• Can Computers Think as Humans? / Kovacs, L. (2022, January 26). Can Computers Think as Humans? [Keynote Presentation]. WiSE Talk at the SCIENCE Lecture Series Talks of Wiener Volksshochsculen and City of Vienna, Austria.
  Project: ARTIST (2021–2026)
• Lemmaless Induction in Trace Logic / Bhayat, A., Georgiou, P., Eisenhofer, C., Kovács, L., & Reger, G. (2022). Lemmaless Induction in Trace Logic. In K. Buzzard & T. Kutsia (Eds.), Intelligent Computer Mathematics : 15th International Conference, CICM 2022, Tbilisi, Georgia, September 19–23, 2022, Proceedings (pp. 191–208). https://doi.org/10.34726/5860
  Download: PDF (320 KB)
  Project: DK - Logic (2014–2023)
• Moment-Based Invariants for Probabilistic Loops with Non-polynomial Assignments / Kofnov, A., Moosbrugger, M., Stankovič, M., Bartocci, E., & Bura, E. (2022). Moment-Based Invariants for Probabilistic Loops with Non-polynomial Assignments. In E. Ábrahám & M. Paolieri (Eds.), Quantitative Evaluation of Systems (pp. 3–25). Springer. https://doi.org/10.1007/978-3-031-16336-4_1
  Projects: ARTIST (2021–2026) / ProbInG (2020–2025)
• ATLAS: Automated Amortised Complexity Analysis of Self-adjusting Data Structures / Leutgeb, L., Moser, G., & Zuleger, F. (2022). ATLAS: Automated Amortised Complexity Analysis of Self-adjusting Data Structures. In Computer Aided Verification (pp. 99–122). https://doi.org/10.1007/978-3-030-81688-9_5
• Strong-separation Logic / Pagel, J., & Zuleger, F. (2022). Strong-separation Logic. In ESOP 2021: Programming Languages and Systems (pp. 664–692). Springer. https://doi.org/10.1007/978-3-030-72019-3_24
• 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

• 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)
• 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)
• 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)
• 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)
• 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)
• 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)
• 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)
• 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)
• Induction with Recursive Definitions in Superposition / Hajdu, M., Hozzová, P., Kovács, L., & Voronkov, A. (2021). Induction with Recursive Definitions in Superposition. In Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021 (Vol. 2, pp. 246–255). TU Wien Academic Press. https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_34
  Download: PDF (350 KB)
• 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)
• 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)
• 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)
• 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)
• 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)
• 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)
• 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)
• 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)
• 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)
• 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)
• 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)
• 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)
• 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)
• 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)
• 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)
• Towards Scalable Verification of Deep Reinforcement Learning / Amir, G., Schapira, M., & Katz, G. (2021). Towards Scalable Verification of Deep Reinforcement Learning. In Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021 (pp. 193–203). TU Wien Academic Press. https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_28
  Download: PDF (306 KB)
• Pruning and Slicing Neural Networks using Formal Verification / Lahav, O., & Katz, G. (2021). Pruning and Slicing Neural Networks using Formal Verification. In Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021 (pp. 183–192). TU Wien Academic Press. https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_27
  Download: PDF (488 KB)
• 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)
• The FMCAD 2021 Student Forum / Santolucito, M. (2021). The FMCAD 2021 Student Forum. In Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021 (pp. 13–13). TU Wien Academic Press. https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_8
  Download: PDF (74.4 KB)
• Formal Methods for the Security Analysis of Smart Contracts / Maffei, M. (2021). Formal Methods for the Security Analysis of Smart Contracts. In Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021 (pp. 8–8). TU Wien Academic Press. https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_3
  Download: PDF (47.5 KB)
• 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)
• 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)
• 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)
• 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)
• 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)
• Synthesizing Pareto-Optimal Interpretations for Black-Box Models / Torfah, H., Shah, S., Chakraborty, S., Akshay, S., & Seshia, S. A. (2021). Synthesizing Pareto-Optimal Interpretations for Black-Box Models. In Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021 (pp. 153–162). TU Wien Academic Press. https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_24
  Download: PDF (322 KB)
• Inductive Benchmarks for Automated Reasoning / Hajdu, M., Hozzová, P., Kovács, L., Schoisswohl, J., & Voronkov, A. (2021). Inductive Benchmarks for Automated Reasoning. In Intelligent Computer Mathematics. 14th International Conference, CICM 2021, Timisoara, Romania, July 26–31, 2021. Proceedings (pp. 124–129). Springer. https://doi.org/10.34726/1563
  Download: PDF (216 KB)
  Projects: ARTIST (2021–2026) / Symcar (2016–2021)
• Automated Generation of Exam Sheets for Automated Deduction / Hozzová, P., Kovács, L., & Rath, J. (2021). Automated Generation of Exam Sheets for Automated Deduction. In Intelligent Computer Mathematics. 14th International Conference, CICM 2021, Timisoara, Romania, July 26–31, 2021. Proceedings (pp. 185–196). Springer. https://doi.org/10.34726/1562
  Download: PDF (458 KB)
  Projects: ARTIST (2021–2026) / Symcar (2016–2021)
• On Positivity and Minimality for Second-Order Holonomic Sequences / Kenison, G. J., Klurman, O., Lefaucheux, E., Luca, F., Moree, P., Ouaknine, J., Whiteland, M., & Worrell, J. (2021). On Positivity and Minimality for Second-Order Holonomic Sequences. In F. Bonchi & S. Puglisi (Eds.), 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021) (pp. 1–15). Schloss Dagstuhl -- Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.MFCS.2021.67
  Download: PDF (709 KB)
  Projects: ARTIST (2021–2026) / ProbInG (2020–2025)
• Integer Induction in Saturation / Hozzová, P., Kovács, L., & Voronkov, A. (2021). Integer Induction in Saturation. In Proceedings of CADE 2021 (pp. 361–377). Springer, Cham. https://doi.org/10.34726/1561
  Download: Preprint submitted for publication as it is (345 KB)
  Projects: ARTIST (2021–2026) / Symcar (2016–2021)
• Induction in Saturation-Based Reasoning / Kovacs, L. (2021, July 26). Induction in Saturation-Based Reasoning [Keynote Presentation]. 14th Conference on Intelligent Computer Mathematics (CICM 2021), Timisoara, Romania. http://hdl.handle.net/20.500.12708/154161
  Project: ARTIST (2021–2026)
• The Probabilistic Termination Tool Amber / Marcel Moosbrugger, Ezio Bartocci, Katoen, J.-P., & Laura Kovács. (2021). The Probabilistic Termination Tool Amber. In Formal Methods. FM 2021 (pp. 667–675). https://doi.org/10.1007/978-3-030-90870-6_36
• Algebra-Based Synthesis of Loops and Their Invariants (Invited Paper) / Humenberger, A., & Kovács, L. (2021). Algebra-Based Synthesis of Loops and Their Invariants (Invited Paper). In F. Henglein, S. Shoham, & Y. Vizel (Eds.), Verification, Model Checking, and Abstract Interpretation (pp. 17–28). Springer LNCS. https://doi.org/10.1007/978-3-030-67067-2_2
• 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
• Bounded Model Checking of Speculative Non-Interference / Pescosta, E., Weissenbacher, G., & Zuleger, F. (2021). Bounded Model Checking of Speculative Non-Interference. In 2021 IEEE/ACM International Conference On Computer Aided Design (ICCAD). 2021 IEEE/ACM International Conference On Computer Aided Design (ICCAD), München, Germany. IEEE. https://doi.org/10.1109/iccad51958.2021.9643462
• Synthesizing Best-effort Strategies under Multiple Environment Specifications / Aminof, B., De Giacomo, G., Lomuscio, A., Murano, A., & Rubin, S. (2021). Synthesizing Best-effort Strategies under Multiple Environment Specifications. In Proceedings of the Eighteenth International Conference on Principles of Knowledge Representation and Reasoning. KR 2021 - 18th International Conference on Principles of Knowledge Representation and Reasoning, virtual event, Unknown. https://doi.org/10.24963/kr.2021/5
• Best-Effort Synthesis: Doing Your Best Is Not Harder Than Giving Up / Aminof, B., De Giacomo, G., & Rubin, S. (2021). Best-Effort Synthesis: Doing Your Best Is Not Harder Than Giving Up. In Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence. IJCAI 2021 - 30th International Joint Conference on Artificial Intelligence, Montreal, Canada, Canada. https://doi.org/10.24963/ijcai.2021/243
• Automating Induction by Reflection / Schoisswohl, J., & Kovács, L. (2021). Automating Induction by Reflection. In E. Pimentel & E. Tassi (Eds.), Electronic Proceedings in Theoretical Computer Science (pp. 39–54). EPTCS. https://doi.org/10.4204/eptcs.337.4
• Eliminating Message Counters in Synchronous Threshold Automata / Stoilkovska, I., Konnov, I., Widder, J., & Zuleger, F. (2021). Eliminating Message Counters in Synchronous Threshold Automata. In VMCAI 2021: Verification, Model Checking, and Abstract Interpretation (pp. 196–218). Springer LNCS. https://doi.org/10.1007/978-3-030-67067-2_10
• Summing up Smart Transitions / Elad, N., Rain, S., Immerman, N., Sagiv, M., & Kovacs, L. (2021). Summing up Smart Transitions. In A. Silva & R. Leino (Eds.), Computer Aided Verification (pp. 317–340). Springer LNCS. https://doi.org/10.1007/978-3-030-81685-8_15
• Preface of the special issue on the conference on computer-aided verification 2018 / Chockler, H., & Weissenbacher, G. (2021). Preface of the special issue on the conference on computer-aided verification 2018. Formal Methods in System Design. https://doi.org/10.1007/s10703-021-00365-5
• Mutation testing with hyperproperties / Fellner, A., Tabaei Befrouei, M., & Weissenbacher, G. (2021). Mutation testing with hyperproperties. Software and Systems Modeling, 20(2), 405–427. https://doi.org/10.1007/s10270-020-00850-1
• Algorithm selection and instance space analysis for curriculum-based course timetabling / De Coster, A., Musliu, N., Schaerf, A., Schoisswohl, J., & Smith-Miles, K. (2021). Algorithm selection and instance space analysis for curriculum-based course timetabling. Journal of Scheduling, 25(1), 35–58. https://doi.org/10.1007/s10951-021-00701-x
• Rely-guarantee bound analysis of parameterized concurrent shared-memory programs / Pani, T., Weissenbacher, G., & Zuleger, F. (2021). Rely-guarantee bound analysis of parameterized concurrent shared-memory programs. Formal Methods in System Design, 57(2), 270–302. https://doi.org/10.1007/s10703-021-00370-8

2020

• Induction with Generalization in Superposition Reasoning / Hajdú, M., Hozzová, P., Kovács, L., Schoisswohl, J., & Voronkov, A. (2020). Induction with Generalization in Superposition Reasoning. In Proceedings of the 13th International Conference on Intelligent Computer Mathematics (CICM) (pp. 123–137). Springer. https://doi.org/10.34726/961
  Download: Postprint was published at CICM 2020. (300 KB)
  Projects: DoS-IoT (2019–2020) / Symcar (2016–2021) / SYMELS (2019–2020)
• Towards Higher-order OWL / Homola, M., Kľuka, J., Hozzová, P., Svátek, V., & Vacura, M. (2020). Towards Higher-order OWL. Kuenstliche Intelligenz, 34, 417–421. https://doi.org/10.1007/s13218-020-00665-8
• Superposition Reasoning about Quantified Bitvector Formulas / Damestani, D., Kovács, L., & Suda, M. (2020). Superposition Reasoning about Quantified Bitvector Formulas. In H. Hong, V. Negru, D. Petcu, & D. Zaharie (Eds.), Proceedings of the 21st International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (pp. 95–99). IEEE. https://doi.org/10.34726/342
  Download: accepted version (226 KB)
  Projects: Symcar (2016–2021) / SYMELS (2019–2020)
• Portfolio SAT and SMT Solving of Cardinality Constraints in Sensor Network Optimization / Kovasznai, G., Gajdár, K., & Kovács, L. (2020). Portfolio SAT and SMT Solving of Cardinality Constraints in Sensor Network Optimization. In H. Hong, V. Negru, D. Petcu, & D. Zaharie (Eds.), Proceedings of the 21st International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (pp. 85–91). IEEE. https://doi.org/10.34726/341
  Download: accepted version (499 KB)
  Projects: Symcar (2016–2021) / SYMELS (2019–2020)
• An ExpTime Upper Bound for ALC with Integers (Extended Version) / Labai, N., Simkus, M., & Ortiz, M. (2020). An ExpTime Upper Bound for ALC with Integers (Extended Version). arXiv. https://doi.org/10.48550/arXiv.2006.02078
• 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)
• 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)
• 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)
• 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)
• 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)
• 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)
• 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)
• 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)
• 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)
• 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)
• 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)
• 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)
• 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)
• 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)
• 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)
• 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)
• A Theoretical Framework for Symbolic Quick Error Detection / Lonsing, F., Mitra, S., & Barrett, C. (2020). A Theoretical Framework for Symbolic Quick Error Detection. In A. Ivrii & O. Strichman (Eds.), Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design – FMCAD 2020 (pp. 26–35). TU Wien Academic Press. https://doi.org/10.34727/2020/isbn.978-3-85448-042-6_9
  Download: Published version (459 KB)
• Reductions for Strings and Regular Expressions Revisited / Reynolds, A., Nötzli, A., Barrett, C., & Tinelli, C. (2020). Reductions for Strings and Regular Expressions Revisited. In A. Ivrii & O. Strichman (Eds.), Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design – FMCAD 2020 (pp. 225–235). TU Wien Academic Press. https://doi.org/10.34727/2020/isbn.978-3-85448-042-6_30
  Download: Published version (1.34 MB)
• 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)
• 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)
• 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)
• 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)
• 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)
• 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)
• 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)
• 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)
• 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)
• 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)
• 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)
• 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)
• 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)
• 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)
• 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)
• Algebra-Based Loop Synthesis / Humenberger, A., Bjørner, N., & Kovacs, L. (2020). Algebra-Based Loop Synthesis. In B. Dongol & E. Troubitsyna (Eds.), Integrated Formal Methods. Proceedings of the 16th International Conference, IFM 2020 (pp. 440–459). Springer. https://doi.org/10.1007/978-3-030-63461-2_24
• Language Inclusion for Finite Prime Event Structures / Fellner, A., Tarrach, T., & Weissenbacher, G. (2020). Language Inclusion for Finite Prime Event Structures. In Verification, Model Checking, and Abstract Interpretation 21st International Conference, VMCAI 2020, New Orleans, LA, USA, January 16–21, 2020, Proceedings (pp. 314–336). Springer. https://doi.org/10.1007/978-3-030-39322-9_15
• Formalizing Graph Trail Properties in Isabelle/HOL / Kovács, L., Lachnitt, H., & Szeider, S. (2020). Formalizing Graph Trail Properties in Isabelle/HOL. In Intelligent Computer Mathematics 13th International Conference, CICM 2020, Bertinoro, Italy, July 26–31, 2020, Proceedings (pp. 190–205). LNCS. https://doi.org/10.1007/978-3-030-53518-6_12
• The Polynomial Complexity of Vector Addition Systems with States / Zuleger, F. (2020). The Polynomial Complexity of Vector Addition Systems with States. In Foundations of Software Science and Computation Structures 23rd International Conference, FOSSACS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25–30, 2020, Proceedings (pp. 622–641). Springer LNCS. https://doi.org/10.1007/978-3-030-45231-5_32
• 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
• 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
• 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
• Pebble-Intervals Automata and FO² with Two Orders / Labai, N., Kotek, T., Ortiz, M., & Veith, H. (2020). Pebble-Intervals Automata and FO2 with Two Orders. In Language and Automata Theory and Applications (pp. 208–221). Lecture Notes in Computer Science (LNCS). https://doi.org/10.1007/978-3-030-40608-0_14
• Multi-linear Strategy Extraction for QBF Expansion Proofs via Local Soundness / Schlaipfer, M., Slivovsky, F., Weissenbacher, G., & Zuleger, F. (2020). Multi-linear Strategy Extraction for QBF Expansion Proofs via Local Soundness. In Theory and Applications of Satisfiability Testing – SAT 2020 (pp. 429–446). LNCS. https://doi.org/10.1007/978-3-030-51825-7_30
• 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
• An ExpTime Upper Bound for ALC with Integers / Labai, N., Simkus, M., & Ortiz de la Fuente, M. M. (2020). An ExpTime Upper Bound for ALC with Integers. In D. Calvanese, E. Erdem, & M. Thielscher (Eds.), Proceedings of the Seventeenth International Conference on Principles of Knowledge Representation and Reasoning. AAAI Press. https://doi.org/10.24963/kr.2020/61
• RAT Elimination / Rebola Pardo, A., & Weissenbacher, G. (2020). RAT Elimination. In L. Kovacs & E. Albert (Eds.), EPiC Series in Computing. EasyChair. https://doi.org/10.29007/fccb
• Layered Clause Selection for Theory Reasoning / Gleiss, B., & Suda, M. (2020). Layered Clause Selection for Theory Reasoning. In P. Fontaine, K. Korovin, & I. Kotsireas (Eds.), Joint Proceedings of the 7th Workshop on Practical Aspects of Automated Reasoning (PAAR) and the 5th Satisfiability Checking and Symbolic Computation Workshop (SC-Square) Workshop (pp. 34–52). CEUR Workshop Proceedings. http://hdl.handle.net/20.500.12708/58379
• A typed parallel lambda-calculus via 1-depth intermediate proofs / Aschieri, F., Ciabattoni, A., & Genco, F. A. (2020). A typed parallel lambda-calculus via 1-depth intermediate proofs. In L. Kovacs (Ed.), EPiC Series in Computing. EasyChair EPiC Series in Computing. https://doi.org/10.29007/g15z
• Synthesizing strategies under expected and exceptional environment behaviors / Aminof, B., De Giacomo, G., Lomuscio, A., Murano, A., & Rubin, S. (2020). Synthesizing strategies under expected and exceptional environment behaviors. In Proceedings of the Twenty-Ninth International Joint Conference on Artificial Intelligence. International Joint Conferences on Artificial Intelligence Organization. https://doi.org/10.24963/ijcai.2020/232
• Stochastic Fairness and Language-Theoretic Fairness in Planning in Nondeterministic Domains / Aminof, B., De Giacomo, G., & Rubin, S. (2020). Stochastic Fairness and Language-Theoretic Fairness in Planning in Nondeterministic Domains. In Proceedings of the Thirtieth International Conference on Automated Planning and Scheduling, Nancy, France (pp. 20–28). AAAI Press. http://hdl.handle.net/20.500.12708/58428
• Preface of the Special Issue on the Conference on Formal Methods in Computer-Aided Design 2017 / Stewart, D., & Weissenbacher, G. (2020). Preface of the Special Issue on the Conference on Formal Methods in Computer-Aided Design 2017. Formal Methods in System Design, 57(3), 303–304. https://doi.org/10.1007/s10703-020-00357-x
• 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
• 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
• 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
• Proceedings of the 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-23) / Albert, E., & Kovacs, L. (Eds.). (2020). Proceedings of the 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-23). EasyChair EPiC Series in Computing. http://hdl.handle.net/20.500.12708/24792
• Proceedings of the 31st International Conference on Concurrency Theory (CONCUR) / Konnov, I., & Kovacs, L. (Eds.). (2020). Proceedings of the 31st International Conference on Concurrency Theory (CONCUR). Dagstuhl Publishing LIPICS. http://hdl.handle.net/20.500.12708/24793

2019

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

2018

• ByMC: Byzantine Model Checker / Konnov, I., & Widder, J. (2018). ByMC: Byzantine Model Checker. In T. Margaria & B. Steffen (Eds.), Leveraging Applications of Formal Methods, Verification and Validation. Distributed Systems. ISoLA 2018, Proceedings, Part III (pp. 327–342). Springer. https://doi.org/10.1007/978-3-030-03424-5_22
• Parameterized Model Checking of Synchronous Distributed Algorithms by Abstraction / Aminof, B., Rubin, S., Stoilkovska, I., Widder, J., & Zuleger, F. (2018). Parameterized Model Checking of Synchronous Distributed Algorithms by Abstraction. In I. Dillig & J. Palsberg (Eds.), Verification, Model Checking, and Abstract Interpretation : 19th International Conference, VMCAI 2018, Los Angeles, CA, USA, January 7-9, 2018, Proceedings. Cham. https://doi.org/10.1007/978-3-319-73721-8_1
  Download: PDF (538 KB)
• Parameterized model checking of rendezvous systems / Aminof, B., Kotek, T., Rubin, S., Spegni, F., & Veith, H. (2018). Parameterized model checking of rendezvous systems. Distributed Computing, 31(3), 187–222. https://doi.org/10.1007/s00446-017-0302-6
• Aligator.jl – A Julia Package for Loop Invariant Generation / Humenberger, A., Jaroschek, M., & Kovács, L. (2018). Aligator.jl – A Julia Package for Loop Invariant Generation. In F. Rabe (Ed.), Intelligent Computer Mathematics : 11th International Conference, CICM 2018, Hagenberg, Austria, August 13-17, 2018, Proceedings (pp. 111–117). LNCS. https://doi.org/10.1007/978-3-319-96812-4_10
• 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
• 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
• 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
• 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

• Dynamic Reductions for Model Checking Concurrent Software / Günther, H., Laarman, A., Sokolova, A., & Weissenbacher, G. (2017). Dynamic Reductions for Model Checking Concurrent Software. In Verification, Model Checking, and Abstract Interpretation 18th International Conference, VMCAI 2017, Paris, France, January 15–17, 2017, Proceedings (pp. 246–265). Springer. https://doi.org/10.1007/978-3-319-52234-0_14
• 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
• 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

• Vienna Verification Tool: IC3 for Parallel Software / Günther, H., Laarman, A., & Weissenbacher, G. (2016). Vienna Verification Tool: IC3 for Parallel Software. In M. Chechik & J.-F. Raskin (Eds.), Tools and Algorithms for the Construction and Analysis of Systems : 22nd International Conference, TACAS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings (pp. 954–957). Springer. https://doi.org/10.1007/978-3-662-49674-9_69
  Download: PDF (173 KB)
• What You Always Wanted to Know About Model Checking of Fault-Tolerant Distributed Algorithms / Konnov, I., Veith, H., & Widder, J. (2016). What You Always Wanted to Know About Model Checking of Fault-Tolerant Distributed Algorithms. In Perspectives of System Informatics : 10th International Andrei Ershov Informatics Conference, PSI 2015, in Memory of Helmut Veith, Kazan and Innopolis, Russia, August 24-27, 2015, Revised Selected Papers (pp. 6–21). Springer. https://doi.org/10.1007/978-3-319-41579-6_2
  Download: PDF (346 KB)
• 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
• Symbolic Computation and Automated Reasoning for Program Analysis / Kovács, L. (2016). Symbolic Computation and Automated Reasoning for Program Analysis. In E. Abraham & M. Huisman (Eds.), Integrated Formal Methods : 12th International Conference, IFM 2016, Reykjavik, Iceland, June 1-5, 2016, Proceedings (pp. 20–27). Springer / LNCS. https://doi.org/10.1007/978-3-319-33693-0_2
• 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
• 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
• 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

• On the expressive power of communication primitives in parameterised systems / Aminof, B., Rubin, S., & Zuleger, F. (2015). On the expressive power of communication primitives in parameterised systems. In M. Davis, A. Fehnker, A. McIver, & A. Voronkov (Eds.), Logic for Programming, Artificial Intelligence, and Reasoning : 20th International Conference, LPAR-20 2015, Suva, Fiji, November 24-28, 2015, Proceedings (pp. 313–328). Springer. https://doi.org/10.1007/978-3-662-48899-7_22
  Download: PDF (438 KB)
• 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
• 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
• 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
• Asymptotically Precise Ranking Functions for Deterministic Size-Change Systems / Zuleger, F. (2015). Asymptotically Precise Ranking Functions for Deterministic Size-Change Systems. In Computer Science -- Theory and Applications 10th International Computer Science Symposium in Russia, CSR 2015, Listvyanka, Russia, July 13-17, 2015, Proceedings (pp. 426–442). Springer. https://doi.org/10.1007/978-3-319-20297-6_27
• LTSmin: High-Performance Language-Independent Model Checking / Blom, S., van Dijk, T., Gijis, K., Laarman, A., Meijer, J., & van de Pol, J. (2015). LTSmin: High-Performance Language-Independent Model Checking. In Tools and Algorithms for the Construction and Analysis of Systems (pp. 692–707). Springer Berlin Heidelberg. https://doi.org/10.1007/978-3-662-46681-0_61
• Time Complexity of Link Reversal Routing / Charron-Bost, B., Függer, M., Welch, J. L., & Widder, J. (2015). Time Complexity of Link Reversal Routing. ACM Transactions on Algorithms, 11(3), 1–39. https://doi.org/10.1145/2644815
• 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
• 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
• Difference Constraints: An adequate Abstraction for Complexity Analysis of Imperative Programs / Sinn, M., Veith, H., & Zuleger, F. (2015). Difference Constraints: An adequate Abstraction for Complexity Analysis of Imperative Programs. In FMCAD (pp. 144–151). http://hdl.handle.net/20.500.12708/56391
• Perspectives on White-Box Testing: Coverage, Concurrency, and Concolic Execution / Farzan, A., Holzer, A., & Veith, H. (2015). Perspectives on White-Box Testing: Coverage, Concurrency, and Concolic Execution. In 2015 IEEE 8th International Conference on Software Testing, Verification and Validation (ICST). International Conference on Software Testing, Verification and Validation (ICST), Graz, Austria. https://doi.org/10.1109/icst.2015.7102600
• 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

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

2013

• 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
• Verification across Intellectual Property Boundaries / Chaki, S., Schallhart, C., & Veith, H. (2013). Verification across Intellectual Property Boundaries. ACM Transactions on Software Engineering and Methodology, 22(2), 1–12. https://doi.org/10.1145/2430545.2430550
• Advanced SAT Techniques for Abstract Argumentation / Wallner, J. P., Weissenbacher, G., & Woltran, S. (2013). Advanced SAT Techniques for Abstract Argumentation. In Computational Logic in Multi-Agent Systems 14th International Workshop, CLIMA XIV, Corunna, Spain, September 16-18, 2013, Proceedings (pp. 138–154). Springer / LNCS. https://doi.org/10.1007/978-3-642-40624-9_9
• Solving Constraints for Generational Search / Pötzl, D., & Holzer, A. (2013). Solving Constraints for Generational Search. In 12 (pp. 197–213). Springer / LNCS. https://doi.org/10.1007/978-3-642-38916-0_12
• Link Reversal Routing with Binary Link Labels: Work Complexity / Charron-Bost, B., Gaillard, A., Welch, J. L., & Widder, J. (2013). Link Reversal Routing with Binary Link Labels: Work Complexity. SIAM Journal on Computing, 42(2), 634–661. https://doi.org/10.1137/110843095
• Formal Verification of Distributed Algorithms / Charron-Bost, B., Merz, S., Rybalchenko, A., & Widder, J. (Eds.). (2013). Formal Verification of Distributed Algorithms. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany. https://doi.org/10.4230/DagRep.3.4.1
• 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
• 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
• 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

• Bounded-Interference Sequentialization for Testing Concurrent Programs / Razavi, N., Farzan, A., & Holzer, A. (2012). Bounded-Interference Sequentialization for Testing Concurrent Programs. In T. Margaria & B. Steffen (Eds.), Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change. (ISoLA 2012), Proceedings, Part I (pp. 372–387). Springer. https://doi.org/10.1007/978-3-642-34026-0_28
• 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
• Efficient Checking of Link-Reversal-Based Concurrent Systems / Függer, M., & Widder, J. (2012). Efficient Checking of Link-Reversal-Based Concurrent Systems. In CONCUR 2012- Concurrency Theory 23rd International Conference, CONCUR 2012, Newcastle upon Tyne, September 4-7, 2012. Proceedings (pp. 486–499). Lecture Notes in Computer Science. Springer Verlag. https://doi.org/10.1007/978-3-642-32940-1_34
• Wait-Free Stabilizing Dining Using Regular Registers / Sastry, S., Welch, J. L., & Widder, J. (2012). Wait-Free Stabilizing Dining Using Regular Registers. In Principles of Distributed Systems 16th International Conference, OPODIS 2012, Rome, Italy, December 18-20, 2012, Proceedings (pp. 284–299). LNCS / Springer. https://doi.org/10.1007/978-3-642-35476-2_20
• Special Issue: Games in Verification (foreword) / Veith, H. (2012). Special Issue: Games in Verification (foreword). Journal of Computer and System Sciences, 78(2), 393. https://doi.org/10.1016/j.jcss.2011.05.007
• Secure two-party computations in ANSI C / Holzer, A., Franz, M., Katzenbeisser, S., & Veith, H. (2012). Secure two-party computations in ANSI C. In Proceedings of the 2012 ACM conference on Computer and communications security - CCS ’12. ACM Conference on Computer and Communications Security (CCS), Washington, USA, Non-EU. ACM. https://doi.org/10.1145/2382196.2382278
• Selected Papers of the Conference "Computer Science Logic CSL 2010": Preface / Dawar, A., & Veith, H. (2012). Selected Papers of the Conference “Computer Science Logic CSL 2010”: Preface. Logical Methods in Computer Science. https://doi.org/10.2168/lmcs-csl:2010
• Consensus in the presence of mortal Byzantine faulty processes / Widder, J., Biely, M., Gridling, G., Weiss, B., & Blanquart, J.-P. (2012). Consensus in the presence of mortal Byzantine faulty processes. Distributed Computing, 24(6), 299–321. https://doi.org/10.1007/s00446-011-0147-3
• Who is afraid of Model Checking Distributed Algorithms? / Konnov, I., Veith, H., & Widder, J. (2012). Who is afraid of Model Checking Distributed Algorithms? Workshop on Exploiting Concurrency Efficiently and Correctly, Berkeley, CA, USA, Non-EU. http://hdl.handle.net/20.500.12708/85358
• Who is afraid of Model Checking Distributed Algorithms? / John, A., Konnov, I., Schmid, U., Veith, H., & Widder, J. (2012). Who is afraid of Model Checking Distributed Algorithms? PUMA/RISE Seminar, Traunkirchen, Austria. http://hdl.handle.net/20.500.12708/85435
• Secure Two-Party Computation in ANSI C / Veith, H. (2012). Secure Two-Party Computation in ANSI C. Dagstuhl Seminar 12461: Games and Decisions for Rigorous Systems Engineering, Dagstuhl, Deutschland, EU. http://hdl.handle.net/20.500.12708/85434
• Labelled Interpolation Systems / Weissenbacher, G. (2012). Labelled Interpolation Systems. Dagstuhl Seminar 12461: Games and Decisions for Rigorous Systems Engineering, Dagstuhl, Deutschland, EU. http://hdl.handle.net/20.500.12708/85433
• Parameterized Model Checking of Fault-tolerant Distributed Algorithms / John, A., Konnov, I., Schmid, U., Veith, H., & Widder, J. (2012). Parameterized Model Checking of Fault-tolerant Distributed Algorithms. Dagstuhl Seminar 12461: Games and Decisions for Rigorous Systems Engineering, Dagstuhl, Deutschland, EU. http://hdl.handle.net/20.500.12708/85432
• Counter Attack against Byzantine Generals / John, A., Konnov, I., Schmid, U., Veith, H., & Widder, J. (2012). Counter Attack against Byzantine Generals. Alpine Verification Meeting, IST Austria, Austria. http://hdl.handle.net/20.500.12708/85359
• Interpretations in Trees with Countably Many Branches / Rabinovich, A., & Rubin, S. (2012). Interpretations in Trees with Countably Many Branches. In 2012 27th Annual IEEE Symposium on Logic in Computer Science. Symposium on Logic in Computer Science (LICS), Edinburgh, United Kingdom, EU. IEEE. https://doi.org/10.1109/lics.2012.65
• Interpolant Strength Revisited / Weissenbacher, G. (2012). Interpolant Strength Revisited. In Theory and Applications of Satisfiability Testing – SAT 2012 (pp. 312–326). LNCS / Springer. https://doi.org/10.1007/978-3-642-31612-8_24
• 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

2011

• Decision Procedures in Soft, Hard and Bio-ware - Follow Up (Dagstuhl Seminar 11272) / Bjørner, N., Nieuwenhuis, R., Veith, H., & Voronkov, A. (2011). Decision Procedures in Soft, Hard and Bio-ware - Follow Up (Dagstuhl Seminar 11272). Dagstuhl Reports, 1(7), 23–35. https://doi.org/10.4230/DagRep.1.7.23
• Seamless Testing for Models and Code / Holzer, A., Januzaj, V., Kugele, S., Langer, B., Schallhart, C., Tautschnig, M., & Veith, H. (2011). Seamless Testing for Models and Code. In G. Goos, J. Hartmanis, & J. van Leeuwen (Eds.), Fundamental Approaches to Software Engineering (pp. 278–293). Springer. https://doi.org/10.1007/978-3-642-19811-3_20
  Project: FORTAS (2010–2011)
• Malware Detection / Katzenbeisser, S., Kinder, J., & Veith, H. (2011). Malware Detection. In H. C. A. van Tilborg & S. Jajodia (Eds.), Encyclopedia of Cryptography and Security (pp. 752–755). Springer-Verlag. https://doi.org/10.1007/978-1-4419-5906-5_838
• Improving the Confidence in Measurement-Based Timing Analysis / Bünte, S., Zolda, M., Tautschnig, M., & Kirner, R. (2011). Improving the Confidence in Measurement-Based Timing Analysis. In 2011 14th IEEE International Symposium on Object/Component/Service-Oriented Real-Time Distributed Computing (ISORC 2011) (pp. 144–151). IEEE. http://hdl.handle.net/20.500.12708/53907
• Termination and Bound Analysis of Imperative Programs / Zuleger, F. (2011). Termination and Bound Analysis of Imperative Programs. Workshop on Logic and Computer Science, Vienna, Austria. http://hdl.handle.net/20.500.12708/85314
• Bound Analysis of Imperative Programs with the Size-change Abstraction / Zuleger, F. (2011). Bound Analysis of Imperative Programs with the Size-change Abstraction. Software Systems Group Seminar, NICTA, Australien, Non-EU. http://hdl.handle.net/20.500.12708/85313
• On Efficient Checking of Link-reversal-based Concurrent Systems / Függer, M., & Widder, J. (2011). On Efficient Checking of Link-reversal-based Concurrent Systems. PUMA/RISE Seminar, Traunkirchen, Austria. http://hdl.handle.net/20.500.12708/85311
• Bound Analysis of Imperative Programs with the Size-change Abstraction / Zuleger, F. (2011). Bound Analysis of Imperative Programs with the Size-change Abstraction. Austrian Society for Rigorous Systems Engineering (ARiSE) workshop together with PUMA workshop, Traunkirchen, Austria, Austria. http://hdl.handle.net/20.500.12708/85312
• How did you specify your test suite? / Veith, H. (2011). How did you specify your test suite? Alpine Verification Meeting, IST Austria, Austria. http://hdl.handle.net/20.500.12708/85158
• Resource Bound Analysis of Imperative Programs / Zuleger, F. (2011). Resource Bound Analysis of Imperative Programs. RiSE Seminar, Klosterneuburg, Austria. http://hdl.handle.net/20.500.12708/85142
• Bound Analysis of Imperative Programs with the Size-change Abstraction / Zuleger, F. (2011). Bound Analysis of Imperative Programs with the Size-change Abstraction. Microsoft Research Lecture, Microsoft Research Cambridge, UK, EU. http://hdl.handle.net/20.500.12708/84682
• Bound Analysis of Imperative Programs with the Size-change Abstraction / Zuleger, F. (2011). Bound Analysis of Imperative Programs with the Size-change Abstraction. Theory Seminar, Queen Mary University, UK, EU. http://hdl.handle.net/20.500.12708/84681
• Bound Analysis of Imperative Programs with the Size-Change Abstraction / Zuleger, F., Sinn, M., Gulwani, S., & Veith, H. (2011). Bound Analysis of Imperative Programs with the Size-Change Abstraction. In E. Yahav (Ed.), Static Analysis (pp. 280–297). Springer. https://doi.org/10.1007/978-3-642-23702-7_22
  Projects: PROSEED (2011–2015) / Rise-TOOLS (2011–2019)

2010

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

2007

• Towards a Systematic Design of Fault-Tolerant Asynchronous Circuits / Schmid, U., Steininger, A., & Veith, H. (2007). Towards a Systematic Design of Fault-Tolerant Asynchronous Circuits. In Fachtagung Zuverlässigkeit und Entwurf (pp. 173–174). VDE Verlag. http://hdl.handle.net/20.500.12708/51805

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

• Verfahren zur Komplexitätsreduktion im Model Checking / Veith, H. (2002). Verfahren zur Komplexitätsreduktion im Model Checking. Technische Universität München, Austria. http://hdl.handle.net/20.500.12708/84107
• Verfahren zur Komplexitätsreduktion im Model Checking / Veith, H. (2002). Verfahren zur Komplexitätsreduktion im Model Checking. Technische Universität Graz, Austria. http://hdl.handle.net/20.500.12708/84106
• Model Checking - Recent Results and Developments / Veith, H. (2002). Model Checking - Recent Results and Developments. University of Leeds, Leeds, United Kingdom, Austria. http://hdl.handle.net/20.500.12708/84105
• Verfahren zur Komplexitätsreduktion im Model Checking / Veith, H. (2002). Verfahren zur Komplexitätsreduktion im Model Checking. Universität Saarbrücken, Saarbrücken, Deutschland, Austria. http://hdl.handle.net/20.500.12708/84104

2024

• Consistency-based Software Fault Localization with Multiple Observations / Graussam, L. (2024). Consistency-based Software Fault Localization with Multiple Observations [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2024.109000
  Download: PDF (964 KB)
• Verified Rank-Balanced trees using LiquidHaskell / Genser, A. (2024). Verified Rank-Balanced trees using LiquidHaskell [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2024.124487
  Download: PDF (812 KB)
• Join operators for bi-abductive analysis of low-level code / Rysavy, L. (2024). Join operators for bi-abductive analysis of low-level code [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2024.119373
  Download: PDF (1.3 MB)
• Inductive Reasoning in Superposition / Hozzová, P. (2024). Inductive Reasoning in Superposition [Dissertation, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2024.123241
  Download: PDF (1.43 MB)
• Supporting register pairs in CompCert / Loitzl, A. (2024). Supporting register pairs in CompCert [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2024.120444
  Download: PDF (746 KB)
• Program synthesis of provable recursive functions / Wagner, E. M. (2024). Program synthesis of provable recursive functions [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2024.120500
  Download: PDF (1.18 MB)
• Automated Analysis of Probabilistic Loops / Moosbrugger, M. (2024). Automated Analysis of Probabilistic Loops [Dissertation, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2024.123240
  Download: PDF (3.18 MB)
• Towards Automating Induction for Software Verification - Guiding Inductive Reasoning in Superposition-based Theorem Proving / Georgiou, P. (2024). Towards Automating Induction for Software Verification - Guiding Inductive Reasoning in Superposition-based Theorem Proving [Dissertation, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2024.123801
  Download: PDF (1.4 MB)
• Symbolic Verification of TLA+ Specifications with Applications to Distributed Algorithms / Tran, T. H. (2024). Symbolic Verification of TLA+ Specifications with Applications to Distributed Algorithms [Dissertation, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2024.117518
  Download: PDF (2.37 MB)

2023

• Enhancing abstraction and symbolic execution for shape analysis of C-programs operating on linked lists / Kaindlstorfer, D. M. (2023). Enhancing abstraction and symbolic execution for shape analysis of C-programs operating on linked lists [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2023.109623
  Download: PDF (591 KB)
• Moment-based loop analysis / Stankovic, M. (2023). Moment-based loop analysis [Dissertation, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2023.113863
  Download: PDF (1.26 MB)
• Exact inference for probabilistic loops / Müllner, J. (2023). Exact inference for probabilistic loops [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2023.107471
  Download: PDF (1020 KB)
• Constraint superposition for higher-order logic / Hetzenberger, M. (2023). Constraint superposition for higher-order logic [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2023.108280
  Download: PDF (1.3 MB)

2022

• Automating proofs of game-theoretic security properties of off-chain protocols / Brugger, L. S. (2022). Automating proofs of game-theoretic security properties of off-chain protocols [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2022.104340
  Download: PDF (666 KB)
• User propagators for satisfiability modulo custom theories / Eisenhofer, C. (2022). User propagators for satisfiability modulo custom theories [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2022.100221
  Download: PDF (1.13 MB)
• Non-Linear reasoning in the superposition calculus / Lackner, A. (2022). Non-Linear reasoning in the superposition calculus [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2022.90765
  Download: PDF (734 KB)
• Non-linear SMT-reasoning over finite fields / Hader, T. (2022). Non-linear SMT-reasoning over finite fields [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2022.89445
  Download: PDF (512 KB)

2021

• Modeling and verification of synchronous fault-tolerant distributed algorithms / Stoilkovska, I. (2021). Modeling and verification of synchronous fault-tolerant distributed algorithms [Dissertation, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2021.90331
  Download: PDF (2.67 MB)
• ATLAS: Automated amortised complexity analysis of self-adjusting data structures / Leutgeb, L. (2021). ATLAS: Automated amortised complexity analysis of self-adjusting data structures [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2021.91302
  Download: PDF (931 KB)
• Thread-modular verification of parameterized programs / Pani, T. (2021). Thread-modular verification of parameterized programs [Dissertation, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2022.100625
  Download: PDF (1.57 MB)
• Interference-based proofs in SAT solving / Rebola-Pardo, A. (2021). Interference-based proofs in SAT solving [Dissertation, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2022.102507
  Download: PDF (2.86 MB)
• Algebra-based loop reasoning - invariant generation and synthesis for numeric loops / Humenberger, A. (2021). Algebra-based loop reasoning - invariant generation and synthesis for numeric loops [Dissertation, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2021.89761
  Download: PDF (1.15 MB)
• Starkes modellbasiertes Mutationstesten / Fellner, A. (2021). Starkes modellbasiertes Mutationstesten [Dissertation, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2021.88481
  Download: PDF (1.68 MB)

2020

• Automated induction by reflection / Schoisswohl, J. (2020). Automated induction by reflection [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2020.75342
  Download: PDF (591 KB)
• SpecBMC : bounded model checker for speculative non-interference / Pescosta, E. (2020). SpecBMC : bounded model checker for speculative non-interference [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2020.76820
  Download: PDF (1.89 MB)
• Automated feedback generation in introductory programming education : a dynamic program analysis approach / Radiček, I. (2020). Automated feedback generation in introductory programming education : a dynamic program analysis approach [Dissertation, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2020.78440
  Download: PDF (1.36 MB)
• Decision procedures for separation logic: beyond symbolic heaps / Pagel, J. (2020). Decision procedures for separation logic: beyond symbolic heaps [Dissertation, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2020.85941
  Download: PDF (2.17 MB)
• Superposition reasoning about quantied bitvector formulas / Damestani, D. (2020). Superposition reasoning about quantied bitvector formulas [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2023.77502
  Download: PDF (383 KB)
• Automating inductive reasoning with recursive functions / Hajdu, M. (2020). Automating inductive reasoning with recursive functions [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2021.84140
  Download: PDF (961 KB)
• Automated software verification using superposition-based theorem proving / Gleiss, B. (2020). Automated software verification using superposition-based theorem proving [Dissertation, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2020.86611
  Download: PDF (1.24 MB)
• Eine Entscheidungsprozedur für Separation-Logic mit Daten / Krulj, S. (2020). Eine Entscheidungsprozedur für Separation-Logic mit Daten [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2020.59461
  Download: PDF (3.11 MB)
• Verifying automotive software components using C model checkers / Durand, T. (2020). Verifying automotive software components using C model checkers [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2020.77681
  Download: PDF (1.36 MB)
• Automated reasoning over Arrays in the superposition calculus / Hochrainer, C. (2020). Automated reasoning over Arrays in the superposition calculus [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2020.77511
  Download: PDF (705 KB)
• Automating termination analysis of probabilistic programs / Moosbrugger, M. (2020). Automating termination analysis of probabilistic programs [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2020.77501
  Download: PDF (710 KB)
• First-order reasoning with aggregates / Rain, S. (2020). First-order reasoning with aggregates [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2020.74620
  Download: PDF (794 KB)
• Formalizing graph trail properties / Lachnitt, H. E. (2020). Formalizing graph trail properties [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2020.77262
  Download: PDF (564 KB)

2019

• A Tiny tweak to proof generation in miniSat-based SAT solvers & a complete and efficient DRAT proof checker / Altmanninger, J. (2019). A Tiny tweak to proof generation in miniSat-based SAT solvers & a complete and efficient DRAT proof checker [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2019.62440
  Download: PDF (3.44 MB)
• Trace Reasoning for formal verification : guiding vampire in induction / Georgiou, P. (2019). Trace Reasoning for formal verification : guiding vampire in induction [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2019.71683
  Download: PDF (501 KB)
• Subsumption demodulation in first-order theorem proving / Rath, J. (2019). Subsumption demodulation in first-order theorem proving [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2019.69280
  Download: PDF (4.58 MB)
• Angriffe gegen Neuronale Netzwerke / Matak, M. (2019). Angriffe gegen Neuronale Netzwerke [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2019.61021
  Download: PDF (5.07 MB)

2018

• Systematic study of variable roles and their use in software verification / Demyanova, Y. (2018). Systematic study of variable roles and their use in software verification [Dissertation, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2018.54905
  Download: PDF (2.2 MB)
• Interactive lecture notes : a computer-aided education system for mastery learning via flipped classrooms / Geiger, S. S. (2018). Interactive lecture notes : a computer-aided education system for mastery learning via flipped classrooms [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2018.58222
  Download: PDF (2.62 MB)
• Rendezvous-multiple broadcast networks / Hafner, J. (2018). Rendezvous-multiple broadcast networks [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2018.32122
  Download: PDF (1.28 MB)
• Techniques and tools for automated verification of fault-tolerant and parameterized distributed systems / Konnov, I. (2018). Techniques and tools for automated verification of fault-tolerant and parameterized distributed systems [Professorial Dissertation, Technische Universität Wien]. reposiTUm. http://hdl.handle.net/20.500.12708/159441

2016

• Resource Bound-Analyse von Lisp-Programmen / Danninger, C. F. (2016). Resource Bound-Analyse von Lisp-Programmen [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2016.40480
  Download: PDF (511 KB)
• Automated complexity analysis for imperative programs / Sinn, M. (2016). Automated complexity analysis for imperative programs [Dissertation, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2016.40011
  Download: PDF (1.49 MB)
• Effective error explanation techniques for concurrent software / Tabaei Befrouei, M. (2016). Effective error explanation techniques for concurrent software [Dissertation, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2016.40440
  Download: PDF (1.8 MB)
• Interpolation and local proofs / Gleiss, B. (2016). Interpolation and local proofs [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2016.36061
  Download: PDF (761 KB)
• Logical methods in automated hardware and software verification / Weissenbacher, G. (2016). Logical methods in automated hardware and software verification [Professorial Dissertation, Technische Universität Wien]. reposiTUm. http://hdl.handle.net/20.500.12708/158852

2015

• First-order theorem proving for program analysis and theory reasoning / Dragan, I.-D. (2015). First-order theorem proving for program analysis and theory reasoning [Dissertation, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2015.28456
  Download: PDF (975 KB)

2014

• Bounds for variables and loops: better together / Souczek, F. (2014). Bounds for variables and loops: better together [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2014.25323
  Download: PDF (843 KB)
• Complexity results and algorithms for argumentation : Dung's frameworks and beyond / Wallner, J. (2014). Complexity results and algorithms for argumentation : Dung’s frameworks and beyond [Dissertation, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2014.24438
  Download: PDF (1.13 MB)
• Reasoning in first-order theories with extensionality / Kragl, B. (2014). Reasoning in first-order theories with extensionality [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2014.23884
  Download: PDF (503 KB)

2013

• Symbolic methods for the timing analysis of programs / Zwirchmayr, J. (2013). Symbolic methods for the timing analysis of programs [Dissertation, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2013.22070
  Download: PDF (1.22 MB)
• Loop patterns in C programs / Pani, T. (2013). Loop patterns in C programs [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2013.23344
  Download: PDF (710 KB)
• Software verification with IC3 via abstraction and interpolation / Birgmeier, J. (2013). Software verification with IC3 via abstraction and interpolation [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2013.22441
  Download: PDF (1010 KB)
• An evaluation of symbol elimination for generating first-order loop invariants / Jucu, I. (2013). An evaluation of symbol elimination for generating first-order loop invariants [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2013.22624
  Download: PDF (705 KB)

2003

• Preemptive scheduling in real-time systems with cyclic precedence constraints / Prianichnikova, A. (2003). Preemptive scheduling in real-time systems with cyclic precedence constraints [Dissertation, Technische Universität Wien]. reposiTUm. http://hdl.handle.net/20.500.12708/183072

• 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 .