Formal Methods in Systems Engineering E192-04

A Research Unit of The Institute of Logic and Computation

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

Research Unit Formal Methods in Systems Engineering

Contact

About

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

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

Professors

Scientific Staff

Administrative Staff

Student Staff

Daneshvar Amrollahi D. Amrollahi

Student Staff

Julian Müllner J. Müllner

Student Staff
BSc

External Lecturers

Courses

2022W

Bachelor Thesis / 184.695 / PR
Computer Aided Verification / 181.145 / VU
Computer-Aided Verification / 181.144 / UE
Declarative Problem Solving / 184.701 / UE
Doctoral & Master Students Seminar / 181.224 / SE
Domain Science and Engineering / 199.103 / VU
Formal Methods in Computer Science / 185.A93 / UE
Formal Methods in Computer Science / 185.291 / VU
Introduction to Knowledge-based Systems / 184.737 / VU
Introduction to Logical Methods in Computer Science / 184.766 / VO
Introduction to Programming 1 / 185.A91 / VU
Orientation Bachelor with Honors of Informatics and Business Informatics / 180.767 / SE
Program Analysis / 184.703 / VU
Project in Computer Science 1 / 184.692 / PR
Project in Computer Science 2 / 184.693 / 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

2023S

Automated Deduction / 184.774 / VU
Bachelor Thesis / 184.695 / PR
Computer Aided Verification / 181.145 / VU
Computer-Aided Verification / 181.144 / UE
Digital Ethics and the Connected World / 199.108 / VU
Doctoral & Master Students Seminar / 181.224 / SE
Formal Methods in Computer Science / 185.291 / VU
Introduction to Logical Methods in Computer Science / 184.766 / VO
Introduction to Programming 1 / 185.A91 / VU
Introduction to Type Theories / 192.142 / VU
Knowledge-based Systems / 184.730 / VU
Orientation Bachelor with Honors of Informatics and Business Informatics / 180.767 / SE
Program and System Verification / 184.741 / VU
Project in Computer Science 1 / 184.692 / PR
Project in Computer Science 2 / 184.693 / PR
Research Seminar LogiCS / 184.767 / SE
SAT Solving / 184.090 / VU
Scientific Research and Writing / 193.052 / SE
Semantics of Programming Languages / 184.749 / VU
Seminar for Master Students in Logic and Computation / 180.773 / SE
Seminar Formal Methods / 181.221 / SE

Projects

Automated Sublinear Amortised Resource Analysis of Data Structures
2023 – 2027 / Austrian Science Fund (FWF)
Semantic and Cryptographic Foundations of Security and Privacy by Compositional Design
2023 – 2026 / Austrian Science Fund (FWF)
Automated Cost Analysis of Data Structures
2023 – 2024 / Amazon Research Awards
Abenteuer Informatik für Volksschulen
2023 – 2024 / BUNDESMINISTERIN FÜR FRAUEN, FAMILIE, INTEGRATION UND MEDIEN
Game-theoretic modelling of the fAsset protocol
2023 / Flare Networks Limited
Automated Reasoning with Theories and Induction for Software Technologies
2021 – 2026 / European Commission / Publications: 147988, 148242, 148506, 148512, 148523, 148534, 148538, 148592, 148602, 148604, 148608, 148616, 148620, 148847, 148849, 148854, 148855, 148858, 148861, 148862, 148865, 148867, 148920, 152204, 19923, 19924, 19925, 22762, 85733
Incremental SAT and SMT Reasoning for Scalable Verification
2021 – 2024 / Austrian Science Fund (FWF)
FOREST: First-Order Reasoning for Ensuring System Security
2021 – 2022 / Amazon Research Awards
Distribution Recovery for Invariant Generation of Probabilistic Programs
2020 – 2024 / Vienna Science and Technology Fund (WWTF) / Publications: 148506, 148920, 22762, 85733
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)
Symbol Elimination in Reliable System Engineering
2019 – 2020 / European Commission / Publications: 16466, 16467, 17857
Domain-Specific Reasoning in IoT Applications
2019 – 2020 / DoS-IoT / Publication: 17857
Holonomic Sequences in Program Verification
2018 – 2021 / Austrian Science Fund (FWF)
LogiCs-Scholarships
2017 – 2025 / LCS
Symbolic Computation and Automated Reasoning for Program Analysis
2016 – 2021 / European Commission / Publications: 16466, 16467, 17857, 19923, 19924, 19925
Bit-level Accurate Reasoning and Interpolation
2016 – 2020 / Microsoft Research Limited / Publications: 60070, 61064
Tools for Concurrent and distributed Systems
2011 – 2019 / Austrian Science Fund (FWF) / Publication: 57366

Publications

Note: Due to the rollout of TU Wien’s new publication database, the list below may be slightly outdated. Once the migration is complete, everything will be up to date again.

2023

Satisfiability Modulo Custom Theories in Z3 / Bjørner, N., Eisenhofer, C., & Kovács, L. (2023). Satisfiability Modulo Custom Theories in Z3. In C. Dragoi, M. Emmi, & J. Wang (Eds.), Verification, Model Checking, and Abstract Interpretation. VMCAI 2023 (pp. 91–105). Springer. https://doi.org/10.1007/978-3-031-24950-1_5 / Project: ARTIST

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
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
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
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/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. / Project: ARTIST
First-Order Subsumption via SAT Solving / Rath, J., Biere, A., & Kovacs, 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
The RAPID Software Verification Framework / Georgiou, P., Gleiss, B., Bhayat, A., Rawson, M., Kovacs, 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
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
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
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
Differential Testing of Pushdown Reachability with a Formally Verified Oracle / Schlichtkrull, A., Konggaard Schou, M., 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
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
Synthesizing Transducers from Complex Specifications / Grover, A., Ehlers, A., & 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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
Stratified Certification for k-Induction / Yu, E., Frolyeks, 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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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). / Project: ARTIST
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
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
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
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., Kovacs, L., Rawson, M., & Voronkov, A. (2022). The Vampire Approach to Induction (short paper). In B. Konev, C. Schon, & A. Steen (Eds.), PAAR 2022. Practical Aspects of Automated Reasoning 2022. Proceedings of the Workshop on Practical Aspects of Automated Reasoning. https://doi.org/10.34726/4103
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, ProbInG
User-Propagation for Custom Theories in SMT Solving / Bjorner, N., Eisenhofer, C., & Kovacs, L. (2022). User-Propagation for Custom Theories in SMT Solving. In D. Deharbe & A. Hyvärinen (Eds.), Satisfiability Modulo Theories. 20th International Workshop. SMT 2022. Proceedings (pp. 71–79). CEUR-WS.org. https://doi.org/10.34726/4104 / Project: ARTIST
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 / Project: ARTIST
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
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
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
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.
Verification of agent navigation in partially-known environments / Aminof, B., Murano, A., Rubin, S., & Zuleger, F. (2022). Verification of agent navigation in partially-known environments. Artificial Intelligence, 308, Article 103724. https://doi.org/10.1016/j.artint.2022.103724
Beyond Strong-Cyclic: Doing Your Best in Stochastic Environments / Aminof, B., De Giacomo, G., Rubin, S., & Zuleger, F. (2022). Beyond Strong-Cyclic: Doing Your Best in Stochastic Environments. In Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence (pp. 2525–2531). https://doi.org/10.24963/ijcai.2022/350
Low-Level Bi-Abduction / Holík, L., Peringer, P., Rogalewicz, A., Šoková, V., Vojnar, T., & Zuleger, F. (2022). Low-Level Bi-Abduction. In 36th European Conference on Object-Oriented Programming (ECOOP 2022) (pp. 1–30). Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.ECOOP.2022.19
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. / Project: ARTIST
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. / Project: ARTIST
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
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
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 / Project: SEGACAB
Automated Program Reasoning / Kovacs, L. (2022, May 30). Automated Program Reasoning [Keynote Presentation]. Informatics Europe Webinar Series, Switzerland. / Project: ARTIST
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. / Project: ARTIST
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
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, ProbInG
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
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. / Project: ARTIST
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
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, ProbInG
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
Strong-separation Logic / Pagel, J., & Zuleger, F. (2022). Strong-separation Logic. In ACM Transactions on Programming Languages and Systems (pp. 1–40). Springer. https://doi.org/10.1145/3498847
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
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

2021

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
Induction with Recursive Definitions in Superposition / Hajdu, M., Hozzova, P., Kovacs, L., & Voronkov, A. (2021). Induction with Recursive Definitions in Superposition. In Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021 (pp. 246–255). TU Wien Academic Press. https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_34
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
Automated Generation of Exam Sheets for Automated Deduction / Hozzova, P., Kovacs, L., & Rath, J. (2021). Automated Generation of Exam Sheets for Automated Deduction. In Intelligent Computer Mathematics. 14th International Conference, CICM 2021, Timisoara, Romania, July 26–31, 2021. Proceedings (pp. 185–196). Springer. https://doi.org/10.34726/1562 / Projects: ARTIST, Symcar
Inductive Benchmarks for Automated Reasoning / Hajdu, M., Hozzova, P., Kovacs, L., Schoisswohl, J., & Voronkov, A. (2021). Inductive Benchmarks for Automated Reasoning. In Intelligent Computer Mathematics. 14th International Conference, CICM 2021, Timisoara, Romania, July 26–31, 2021. Proceedings (pp. 124–129). Springer. https://doi.org/10.34726/1563 / Projects: ARTIST, Symcar
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 / Projects: ARTIST, ProbInG
Integer Induction in Saturation / Hozzova, P., Kovacs, L., & Voronkov, A. (2021). Integer Induction in Saturation. In Proceedings of CADE 2021 (pp. 361–377). Springer, Cham. https://doi.org/10.34726/1561 / Projects: ARTIST, Symcar
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. / Project: ARTIST
Preface of the special issue on the conference on computer-aided verification 2018 / Chockler, H., & Weissenbacher, G. (2021). Preface of the special issue on the conference on computer-aided verification 2018. Formal Methods in System Design. https://doi.org/10.1007/s10703-021-00365-5
Mutation testing with hyperproperties / Fellner, A., Tabaei Befrouei, M., & Weissenbacher, G. (2021). Mutation testing with hyperproperties. Software and Systems Modeling, 20(2), 405–427. https://doi.org/10.1007/s10270-020-00850-1
The Probabilistic Termination Tool Amber / Marcel Moosbrugger, Ezio Bartocci, Katoen, J.-P., & Laura Kovács. (2021). The Probabilistic Termination Tool Amber. In Formal Methods. FM 2021 (pp. 667–675). https://doi.org/10.1007/978-3-030-90870-6_36
Algorithm selection and instance space analysis for curriculum-based course timetabling / De Coster, A., Musliu, N., Schaerf, A., Schoisswohl, J., & Smith-Miles, K. (2021). Algorithm selection and instance space analysis for curriculum-based course timetabling. Journal of Scheduling, 25(1), 35–58. https://doi.org/10.1007/s10951-021-00701-x
Rely-guarantee bound analysis of parameterized concurrent shared-memory programs / Pani, T., Weissenbacher, G., & Zuleger, F. (2021). Rely-guarantee bound analysis of parameterized concurrent shared-memory programs. Formal Methods in System Design, 57(2), 270–302. https://doi.org/10.1007/s10703-021-00370-8
Bounded Model Checking of Speculative Non-Interference / Pescosta, E., Weissenbacher, G., & Zuleger, F. (2021). Bounded Model Checking of Speculative Non-Interference. In 2021 IEEE/ACM International Conference On Computer Aided Design (ICCAD). 2021 IEEE/ACM International Conference On Computer Aided Design (ICCAD), München, Deutschland, EU. IEEE. https://doi.org/10.1109/iccad51958.2021.9643462
Eliminating Message Counters in Synchronous Threshold Automata / Stoilkovska, I., Konnov, I., Widder, J., & Zuleger, F. (2021). Eliminating Message Counters in Synchronous Threshold Automata. In Lecture Notes in Computer Science (pp. 196–218). Springer LNCS. https://doi.org/10.1007/978-3-030-67067-2_10
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
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
Model Checking AUTOSAR Components with CBMC / Durand, T., Fazekas, K., Weissenbacher, G., & Zwirchmayr, J. (2021). Model Checking AUTOSAR Components with CBMC. In R. Piskac & M. W. Whalen (Eds.), 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
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, International. https://doi.org/10.24963/ijcai.2021/243
Algebra-Based Synthesis of Loops and Their Invariants (Invited Paper) / Humenberger, A., & Kovács, L. (2021). Algebra-Based Synthesis of Loops and Their Invariants (Invited Paper). In F. Henglein, S. Shoham, & Y. Vizel (Eds.), Lecture Notes in Computer Science (pp. 17–28). Springer LNCS. https://doi.org/10.1007/978-3-030-67067-2_2
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

2020

Induction with Generalization in Superposition Reasoning / Hajdú, M., Hozzova, P., Kovacs, 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 / Projects: DoS-IoT, Symcar, SYMELS
Towards Higher-order OWL / Homola, M., Kľuka, J., Hozzová, P., Svátek, V., & Vacura, M. (2020). Towards Higher-order OWL. Kuenstliche Intelligenz, 34, 417–421. https://doi.org/10.1007/s13218-020-00665-8
Portfolio SAT and SMT Solving of Cardinality Constraints in Sensor Network Optimization / Kovasznai, G., Gajdár, K., & Kovacs, L. (2020). Portfolio SAT and SMT Solving of Cardinality Constraints in Sensor Network Optimization. In H. Hong, V. Negru, D. Petcu, & D. Zaharie (Eds.), Proceedings of the 21st International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (pp. 85–91). IEEE. https://doi.org/10.34726/341 / Projects: Symcar, SYMELS
Superposition Reasoning about Quantified Bitvector Formulas / Damestani, D., Kovacs, L., & Suda, M. (2020). Superposition Reasoning about Quantified Bitvector Formulas. In H. Hong, V. Negru, D. Petcu, & D. Zaharie (Eds.), Proceedings of the 21st International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (pp. 95–99). IEEE. https://doi.org/10.34726/342 / Projects: Symcar, SYMELS
Preface of the Special Issue on the Conference on Formal Methods in Computer-Aided Design 2017 / Stewart, D., & Weissenbacher, G. (2020). Preface of the Special Issue on the Conference on Formal Methods in Computer-Aided Design 2017. Formal Methods in System Design, 57(3), 303–304. https://doi.org/10.1007/s10703-020-00357-x
Layered Clause Selection for Theory Reasoning / Gleiss, B., & Suda, M. (2020). Layered Clause Selection for Theory Reasoning. In N. Peltier & V. Sofronie-Stokkermans (Eds.), Automated Reasoning (pp. 402–409). Lecture Notes in Computer Science, Springer. https://doi.org/10.1007/978-3-030-51074-9_23
Subsumption Demodulation in First-Order Theorem Proving / Gleiss, B., Kovacs, L., & Rath, J. (2020). Subsumption Demodulation in First-Order Theorem Proving. In N. Peltier & V. Sofronie-Stokkermans (Eds.), Automated Reasoning (pp. 297–315). Lecture Notes in Computer Science, Springer. https://doi.org/10.1007/978-3-030-51074-9_17
Algebra-Based Loop Synthesis / Humenberger, A., Bjørner, N., & Kovacs, L. (2020). Algebra-Based Loop Synthesis. In B. Dongol & E. Troubitsyna (Eds.), Lecture Notes in Computer Science (pp. 440–459). Lecture Notes in Computer Science, Springer. https://doi.org/10.1007/978-3-030-63461-2_24
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
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
Accelerating Parallel Verification via Complementary Property Partitioning and Strategy Exploration / Dureja, R., Baumgartner, J., Kanzelman, R., Williams, M., & Rozier, K. Y. (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
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
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
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
Beyond Symbolic Heaps: Deciding Separation Logic With Inductive Definitions / Pagel, J., & Zuleger, F. (2020). Beyond Symbolic Heaps: Deciding Separation Logic With Inductive Definitions. In EPiC Series in Computing. EasyChair EPiC Series in Computing. https://doi.org/10.29007/vkmj
The Polynomial Complexity of Vector Addition Systems with States / Zuleger, F. (2020). The Polynomial Complexity of Vector Addition Systems with States. In Lecture Notes in Computer Science (pp. 622–641). Springer LNCS. https://doi.org/10.1007/978-3-030-45231-5_32
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
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.), Automated Reasoning (pp. 402–409). CEUR Workshop Proceedings. https://doi.org/10.1007/978-3-030-51074-9_23
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
Thread-modular Counter Abstraction for Parameterized Program Safety / Pani, T., Weissenbacher, G., & Zuleger, F. (2020). Thread-modular Counter Abstraction for Parameterized Program Safety. In Formal Methods in Computer-Aided Design (pp. 67–76). TU Wien Academic Press / IEEE. https://doi.org/10.34727/2020/isbn.978-3-85448-042-6_13
Language Inclusion for Finite Prime Event Structures / Fellner, A., Tarrach, T., & Weissenbacher, G. (2020). Language Inclusion for Finite Prime Event Structures. In Lecture Notes in Computer Science (pp. 314–336). Springer. https://doi.org/10.1007/978-3-030-39322-9_15
Multi-linear Strategy Extraction for QBF Expansion Proofs via Local Soundness / Schlaipfer, M., Slivovsky, F., Weissenbacher, G., & Zuleger, F. (2020). Multi-linear Strategy Extraction for QBF Expansion Proofs via Local Soundness. In Theory and Applications of Satisfiability Testing – SAT 2020 (pp. 429–446). LNCS. https://doi.org/10.1007/978-3-030-51825-7_30
Formalizing Graph Trail Properties in Isabelle/HOL / Kovács, L., Lachnitt, H., & Szeider, S. (2020). Formalizing Graph Trail Properties in Isabelle/HOL. In Lecture Notes in Computer Science (pp. 190–205). LNCS. https://doi.org/10.1007/978-3-030-53518-6_12
Analysis of Bayesian Networks via Prob-Solvable Loops / Bartocci, E., Kovács, L., & Stankovič, M. (2020). Analysis of Bayesian Networks via Prob-Solvable Loops. In Theoretical Aspects of Computing – ICTAC 2020 (pp. 221–241). Springer. https://doi.org/10.1007/978-3-030-64276-1_12
Mora - Automatic Generation of Moment-Based Invariants / Bartocci, E., Kovács, L., & Stankovič, M. (2020). Mora - Automatic Generation of Moment-Based Invariants. In Tools and Algorithms for the Construction and Analysis of Systems (pp. 492–498). Springer. https://doi.org/10.1007/978-3-030-45190-5_28
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
Pebble-Intervals Automata and FO$$^2$$ with Two Orders / Labai, N., Kotek, T., Ortiz, M., & Veith, H. (2020). Pebble-Intervals Automata and FO$$^2$$ with Two Orders. In Language and Automata Theory and Applications (pp. 208–221). Lecture Notes in Computer Science (LNCS). https://doi.org/10.1007/978-3-030-40608-0_14
Trace Logic for Inductive Loop Reasoning / Georgiou, P., Gleiss, B., & Kovacs, L. (2020). Trace Logic for Inductive Loop Reasoning. In A. Ivrii & O. Strichman (Eds.), Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design - FMCAD 2020 (pp. 255–263). IEEE. https://doi.org/10.34727/2020/isbn.978-3-85448-042-6_33
An ExpTime Upper Bound for ALC with Integers / 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
Synthesizing Best-effort Strategies under Multiple Environment Specifications / Aminof, B., De Giacomo, G., Lomuscio, A., Murano, A., & Rubin, S. (2020). Synthesizing Best-effort Strategies under Multiple Environment Specifications. In Proceedings of the Eighteenth International Conference on Principles of Knowledge Representation and Reasoning. KR 2021 - 18th International Conference on Principles of Knowledge Representation and Reasoning, virtual event, International. https://doi.org/10.24963/kr.2021/5
An ExpTime Upper Bound for ALC with Integers (Extended Version) / Labai, N., Simkus, M., & Ortiz de la Fuente, M. M. (2020). An ExpTime Upper Bound for ALC with Integers (Extended Version) (2006.02078). http://hdl.handle.net/20.500.12708/40248
Proceedings of the 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-23) / Albert, E., & Kovacs, L. (Eds.). (2020). Proceedings of the 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-23). EasyChair EPiC Series in Computing. http://hdl.handle.net/20.500.12708/24792
Proceedings of the 31st International Conference on Concurrency Theory (CONCUR) / Konnov, I., & Kovacs, L. (Eds.). (2020). Proceedings of the 31st International Conference on Concurrency Theory (CONCUR). Dagstuhl Publishing LIPICS. http://hdl.handle.net/20.500.12708/24793
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
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
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
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
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
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
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
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
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
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
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
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
Effective System Level Liveness Verification / Fedotov, A., Keiren, J. J. A., & 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
Runtime Verification on FPGAs with LTLf Specifications / Tracy II, T., Tabajara, L. M., 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
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
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). TU Wien Academic Press. https://doi.org/10.34727/2020/isbn.978-3-85448-042-6_33
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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

2019

Removing apparent singularities of linear difference systems / Barkatou, M. A., & Jaroschek, M. (2019). Removing apparent singularities of linear difference systems. Journal of Symbolic Computation, 102, 86–107. https://doi.org/10.1016/j.jsc.2019.10.010
Model-based, Mutation-driven Test-case Generation Via Heuristic-guided Branching Search / Fellner, A., Krenn, W., Schlick, R., Tarrach, T., & Weissenbacher, G. (2019). Model-based, Mutation-driven Test-case Generation Via Heuristic-guided Branching Search. ACM Transactions on Embedded Computing Systems, 18(1), 1–28. https://doi.org/10.1145/3289256
Foreword - Formalization of geometry, automated and interactive geometric reasoning / Schreck, P., Ida, T., & Kovacs, L. (2019). Foreword - Formalization of geometry, automated and interactive geometric reasoning. Annals of Mathematics and Artificial Intelligence, 85(2–4), 71–72. https://doi.org/10.1007/s10472-019-9617-2
Foreword / Davenport, J. H., Kovacs, L., & Zaharie, D. (2019). Foreword. Mathematics in Computer Science, 13(4), 459–460. https://doi.org/10.1007/s11786-019-00411-w
Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops / Bartocci, E., Kovacs, L., & Stankovic, M. (2019). Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops. In Y.-F. Chen, C.-H. Cheng, & J. Esparza (Eds.), Automated Technology for Verification and Analysis (pp. 255–276). Springer. https://doi.org/10.1007/978-3-030-31784-3_15
Trace Reasoning for Formal Verification using the First-Order Superposition Calculus / Georgiou, P., Gleiss, B., Kovacs, L., & Maffei, M. (2019). Trace Reasoning for Formal Verification using the First-Order Superposition Calculus. FMCAD 2019 Student Forum, San Jose, US, Non-EU. http://hdl.handle.net/20.500.12708/86988
Automatic Analysis for Prob-Solvable Loops / Stankovic, M. (2019). Automatic Analysis for Prob-Solvable Loops. 13th Alpine Verification Meeting (AVM), Brno, Czech Republic, EU. http://hdl.handle.net/20.500.12708/87000
APRe, Vampire, Welcome in Vienna! / Kovacs, L. (2019). APRe, Vampire, Welcome in Vienna! APRe 2019 Workshop, TU Wien, TU Wien, Vienna, Austria. http://hdl.handle.net/20.500.12708/86999
Formal Methods in the Digital World (in Hungarian) / Kovacs, L. (2019). Formal Methods in the Digital World (in Hungarian). JegKepzes Series of Presentations- Hungarian Scientists from the Bartok Bela Highschool, Timisoara, Romania, EU. http://hdl.handle.net/20.500.12708/86998
First-Order Interpolation / Kovacs, L. (2019). First-Order Interpolation. PhD Research Seminar in Logic and Computation, Faculty of Informatics, West University of Timisoara, Timisoara, Romania, EU. http://hdl.handle.net/20.500.12708/86997
Symbolic Computation and Automated Reasoning for Program Analysis / Kovacs, L. (2019). Symbolic Computation and Automated Reasoning for Program Analysis. 23rd IEEE International Conference on Intelligent Engineering Systems (INES) 2019, Gödöllõ, Hungary, EU. http://hdl.handle.net/20.500.12708/86996
Interpolation in the Grey Area of Proofs / Kovacs, L. (2019). Interpolation in the Grey Area of Proofs. Helmut Veith Memorial Workshop 2019, Turracher Höhe, Austria. http://hdl.handle.net/20.500.12708/86995
First Order Interpolation / Kovacs, L. (2019). First Order Interpolation. SAT/SMT/AR Summer School 2019, Lisbon, Portugal, EU. http://hdl.handle.net/20.500.12708/86994
Forward Subsumption Demodulation - Fast Conditional Rewriting in Vampire / Gleiss, B., Kovacs, L., & Rath, J. (2019). Forward Subsumption Demodulation - Fast Conditional Rewriting in Vampire. Vampire 2019 - The Sixth Vampire Workshop, Lisbon, Portugal, EU. http://hdl.handle.net/20.500.12708/86993
Subsumption Demodulation in First-Order Theorem Proving / Rath, J. (2019). Subsumption Demodulation in First-Order Theorem Proving. First International Workshop on Proof Theory for Automated Deduction, Automated Deduction for Proof Theory, Funchal, Portugal, EU. http://hdl.handle.net/20.500.12708/86992
Verifying Relational Properties using Trace Logic / Kovacs, L. (2019). Verifying Relational Properties using Trace Logic. First International Workshop on Proof Theory for Automated Deduction, Automated Deduction for Proof Theory, Funchal, Portugal, EU. http://hdl.handle.net/20.500.12708/86991
60 Shades of Grey in Vampire / Kovacs, L. (2019). 60 Shades of Grey in Vampire. ANDREI-60: Automating New-Era Deductive Reasoning Event in Iberia, Tbilisi, Georgia, Non-EU. http://hdl.handle.net/20.500.12708/86990
Symbol Elimination and Vampire / Kovacs, L. (2019). Symbol Elimination and Vampire. Dagstuhl Seminar 19062 - Bringing CP, SAT and SMT together: Next Challenges in Constraint Solving, Schloss Dagstuhl, Germany, EU. http://hdl.handle.net/20.500.12708/86989
Interactive Visualization of Saturation Attempts in Vampire / Gleiss, B., Kovács, L., & Schnedlitz, L. (2019). Interactive Visualization of Saturation Attempts in Vampire. In W. Ahrendt & S. Lizeth (Eds.), Lecture Notes in Computer Science (pp. 504–513). Lecture Notes in Computer Science, Springer. https://doi.org/10.1007/978-3-030-34968-4_28
Verifying Relational Properties using Trace Logic / Barthe, G., Eilers, R., Georgiou, P., Gleiss, B., Kovacs, L., & Maffei, M. (2019). Verifying Relational Properties using Trace Logic. In B. Clark & J. Yang (Eds.), 2019 Formal Methods in Computer Aided Design (FMCAD). IEEE. https://doi.org/10.23919/fmcad.2019.8894277
Extracting Safe Thread Schedules from Incomplete Model Checking Results / Metzler, P., Suri, N., & Weissenbacher, G. (2019). Extracting Safe Thread Schedules from Incomplete Model Checking Results. In Model Checking Software (pp. 153–171). LNCS, Springer. https://doi.org/10.1007/978-3-030-30923-7_9
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
Model-Based Diagnosis with Multiple Observations / Ignatiev, A., Morgado, A., Marques-Silva, J., & Weissenbacher, G. (2019). Model-Based Diagnosis with Multiple Observations. In Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence. IJCAI 2019 - 28th International Joint Conference on Artificial Intelligence, Macao, China, Non-EU. https://doi.org/10.24963/ijcai.2019/155
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
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
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
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
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 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
Communication-Closed Asynchronous Protocols / Damian, A., Drăgoi, C., Militaru, A., & Widder, J. (2019). Communication-Closed Asynchronous Protocols. In Computer Aided Verification (pp. 344–363). Springer. https://doi.org/10.1007/978-3-030-25543-5_20
Pebble-Intervals Automata and FO2 with Two Orders (Extended Version / Labai, N., Kotek, T., Ortiz de la Fuente, M. M., & Veith, H. (2019). Pebble-Intervals Automata and FO2 with Two Orders (Extended Version (1912.00171). http://hdl.handle.net/20.500.12708/39866 / Projects: KtoAPP, OMEGA

2018

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
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
Parameterized Model Checking of Synchronous Distributed Algorithms by Abstraction / Aminof, B., Rubin, S., Stoilkovska, I., Widder, J., & Zuleger, F. (2018). Parameterized Model Checking of Synchronous Distributed Algorithms by Abstraction. In Verification, Model Checking, and Abstract Interpretation - 19th International Conference, VMCAI 2018, Los Angeles, CA, USA, January 7-9, 2018, Proceedings ; Dillig, Isil; Palsberg, Jens. Cham. https://doi.org/10.1007/978-3-319-73721-8_1
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
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
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
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
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
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
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 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
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
Aligator.jl – A Julia Package for Loop Invariant Generation / Humenberger, A., Jaroschek, M., & Kovács, L. (2018). Aligator.jl – A Julia Package for Loop Invariant Generation. In F. Rabe (Ed.), Lecture Notes in Computer Science (pp. 111–117). LNCS. https://doi.org/10.1007/978-3-319-96812-4_10
Rely-Guarantee Reasoning for Automated Bound Analysis of Lock-Free Algorithms / Pani, T., Weissenbacher, G., & Zuleger, F. (2018). Rely-Guarantee Reasoning for Automated Bound Analysis of Lock-Free Algorithms. In 2018 Formal Methods in Computer Aided Design (FMCAD). International Conference on Formal Methods in Computer-Aided Design (FMCAD), Portland, OR, USA, Non-EU. FMCAD Inc. https://doi.org/10.23919/fmcad.2018.8603020
A Separation Logic with Data: Small Models and Automation / Pagel, J., Jovanovic, D., & Weissenbacher, G. (2018). A Separation Logic with Data: Small Models and Automation. In Automated Reasoning (pp. 455–471). LNCS. https://doi.org/10.1007/978-3-319-94205-6_30
ByMC: Byzantine Model Checker / Konnov, I., & Widder, J. (2018). ByMC: Byzantine Model Checker. In Leveraging Applications of Formal Methods, Verification and Validation. Distributed Systems (pp. 327–342). Lecture Notes in Computer Science. Springer Verlag. https://doi.org/10.1007/978-3-030-03424-5_22
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
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
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
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
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
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

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
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
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
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
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 OPODIS (pp. 32:1-32:20). LIPIcs-Leibniz International Proceedings in Informatics. https://doi.org/10.4230/LIPIcs.OPODIS.2017.32
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, START
Model-based, mutation-driven test case generation via heuristic-guided branching search / Fellner, A., Krenn, W., Schlick, R., Tarrach, T., & Weissenbacher, G. (2017). Model-based, mutation-driven test case generation via heuristic-guided branching search. In Proceedings of the 15th ACM-IEEE International Conference on Formal Methods and Models for System Design. MEMOCODE 2017: the 15th ACM-IEEE International Conference on Formal Methods and Models for System Design, Vienna, Austria, EU. ACM. https://doi.org/10.1145/3127041.3127049
A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms / Konnov, I., Lazić, M., Veith, H., & Widder, J. (2017). A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages. 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), Paris, France, EU. ACM. https://doi.org/10.1145/3009837.3009860
Dynamic Reductions for Model Checking Concurrent Software / Günther, H., Laarman, A., Sokolova, A., & Weissenbacher, G. (2017). Dynamic Reductions for Model Checking Concurrent Software. In Lecture Notes in Computer Science (pp. 246–265). Springer. https://doi.org/10.1007/978-3-319-52234-0_14
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
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

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, START
Labelled Interpolation Systems for Hyper-Resolution, Clausal, and Local Proofs / Schlaipfer, M., & Weissenbacher, G. (2016). Labelled Interpolation Systems for Hyper-Resolution, Clausal, and Local Proofs. Journal of Automated Reasoning, 57(1), 3–36. https://doi.org/10.1007/s10817-016-9364-6
AVATAR Modulo Theories / Reger, G., Bjørner, N., Suda, M., & Voronkov, A. (2016). AVATAR Modulo Theories. In GCAI 2016. 2nd Global Conference on Artificial Intelligence (pp. 39–52). EasyChair. http://hdl.handle.net/20.500.12708/56715
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
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, IE of ASP
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
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
When Should We Add Theory Axioms And Which Ones? / Reger, G., & Suda, M. (2016). When Should We Add Theory Axioms And Which Ones? 1st Conference on Artificial Intelligence and Theorem Proving, AITP 2016, Obergurgl, Austria. http://hdl.handle.net/20.500.12708/86349
Revisiting Global Subsumption / Reger, G., & Suda, M. (2016). Revisiting Global Subsumption. The Third Vampire Workshop, VAMPIRE 2016, Coimbra, Portugal, EU. http://hdl.handle.net/20.500.12708/86350
Automated Reasoning for Systems Engineering / Kovacs, L. (2016). Automated Reasoning for Systems Engineering. Austrian Computer Science Day 2018, Salzburg, Austria. http://hdl.handle.net/20.500.12708/86695
Desingularization of First Order Linear Difference Systems with Rational Function Coefficients / Jaroschek, M., & Barkatou, M. (2016). Desingularization of First Order Linear Difference Systems with Rational Function Coefficients. RIMS workshop, Algebraic Statistics and Symbolic Computation, RIMS, Kyoto University, Kyoto, Japan, Non-EU. http://hdl.handle.net/20.500.12708/86472
Quantifier Elimination Over The Reals / Jaroschek, M. (2016). Quantifier Elimination Over The Reals. Tutorial on SMT and Polynomial Arithmetic, Chalmers University, Gothenburg, Sweden, EU. http://hdl.handle.net/20.500.12708/86471
Desingularization of First Order Linear Difference Systems with Rational Function Coefficients / Barkatou, M., & Jaroschek, M. (2016). Desingularization of First Order Linear Difference Systems with Rational Function Coefficients. 22nd Conference on Applications of Computer Algebra, Universität Kassel, Kassel, Deutschland, EU. http://hdl.handle.net/20.500.12708/86470
With a Timisoara Background in the Scientific World of Computer Science and / Kovacs, L. (2016). With a Timisoara Background in the Scientific World of Computer Science and. Timisoara Hungarian Science Festival, Timisoara, Romania, EU. http://hdl.handle.net/20.500.12708/86440
Enjoying Research at the Intersection of Math and Computer Science / Kovacs, L. (2016). Enjoying Research at the Intersection of Math and Computer Science. Women in Science Workshop Series (WISE), Gothenburg, Schweden, EU. http://hdl.handle.net/20.500.12708/86439
First-Order Theorem Proving and Vampire / Kovacs, L. (2016). First-Order Theorem Proving and Vampire. Spring School on Logic and Verification - LoVE, Vienna, Austria, Austria. http://hdl.handle.net/20.500.12708/86438
Model Checking of Threshold-based Fault-Tolerant Distributed Algorithms / Lazić, M., Konnov, I., Veith, H., & Widder, J. (2016). Model Checking of Threshold-based Fault-Tolerant Distributed Algorithms. 7th Workshop on Program Semantics, Specification and Verification: Theory and Applications, St. Petersburg, Russia, Non-EU. http://hdl.handle.net/20.500.12708/86426
Parameterized Verification of Liveness of Distributed Algorithms / Konnov, I., Lazić, M., Veith, H., & Widder, J. (2016). Parameterized Verification of Liveness of Distributed Algorithms. Workshop on Formal Reasoning in Distributed Algorithms (FRiDA), Wien, Austria. http://hdl.handle.net/20.500.12708/86425
Interpolation algorithms and their applications in model checking / Weissenbacher, G. (2016). Interpolation algorithms and their applications in model checking. Automata, Logic and Games, Singapore, Non-EU. http://hdl.handle.net/20.500.12708/86305
Extended Graded Modalities in Strategy Logic / Aminof, B., Malvone, V., Murano, A., & Rubin, S. (2016). Extended Graded Modalities in Strategy Logic. In SR (pp. 1–14). http://hdl.handle.net/20.500.12708/56868
Graded Strategy Logic: Reasoning about Uniqueness of Nash Equilibria / Aminof, B., Malvone, V., Murano, A., & Rubin, S. (2016). Graded Strategy Logic: Reasoning about Uniqueness of Nash Equilibria. In AAMAS (pp. 698–706). http://hdl.handle.net/20.500.12708/56867
Monadic Second Order Finite Satisfiability and Unbounded Tree-Width / Kotek, T., Veith, H., & Zuleger, F. (2016). Monadic Second Order Finite Satisfiability and Unbounded Tree-Width. In CSL (pp. 1–20). http://hdl.handle.net/20.500.12708/56860
Automatic Verification of Multi-Agent Systems in Parameterised Grid-Environments / Aminof, B., Murano, A., Rubin, S., & Zuleger, F. (2016). Automatic Verification of Multi-Agent Systems in Parameterised Grid-Environments. In AAMAS (pp. 1190–1199). http://hdl.handle.net/20.500.12708/56859
Prompt Alternating-Time Epistemic Logics / Aminof, B., Murano, A., Rubin, S., & Zuleger, F. (2016). Prompt Alternating-Time Epistemic Logics. In KR (pp. 258–267). http://hdl.handle.net/20.500.12708/56836
The vampire and the FOOL / Kotelnikov, E., Kovács, L., Reger, G., & Voronkov, A. (2016). The vampire and the FOOL. In J. Avigad & A. Chlipala (Eds.), Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs. ACM. https://doi.org/10.1145/2854065.2854071
Symbolic Computation and Automated Reasoning for Program Analysis / Kovács, L. (2016). Symbolic Computation and Automated Reasoning for Program Analysis. In E. Abraham & M. Huisman (Eds.), Lecture Notes in Computer Science (pp. 20–27). Springer / LNCS. https://doi.org/10.1007/978-3-319-33693-0_2
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 CONCUR (pp. 30:1-30:16). Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2016.30
A Clausal Normal Form Translation for FOOL / Kotelnikov, E., Kovacs, L., Suda, M., & Voronkov, A. (2016). A Clausal Normal Form Translation for FOOL. In GCAI 2016. 2nd Global Conference on Artificial Intelligence (pp. 53–71). EasyChair. http://hdl.handle.net/20.500.12708/56716
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, START
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
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
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

2015

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
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
Loop Patterns in C Programs / Pani, T., Veith, H., & Zuleger, F. (2015). Loop Patterns in C Programs. ECEASST, 72. http://hdl.handle.net/20.500.12708/151928
Closure properties and complexity of rational sets of regular languages / Holzer, A., Schallhart, C., Tautschnig, M., & Veith, H. (2015). Closure properties and complexity of rational sets of regular languages. Theoretical Computer Science, 605, 62–79. https://doi.org/10.1016/j.tcs.2015.08.035
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
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
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
Empirical Software Metrics for Benchmarking of Verification Tools / Demyanova, Y., Pani, T., Veith, H., & Zuleger, F. (2015). Empirical Software Metrics for Benchmarking of Verification Tools. In Computer Aided Verification (pp. 561–579). Springer. https://doi.org/10.1007/978-3-319-21690-4_39
LTSmin: High-Performance Language-Independent Model Checking / Blom, S., van Dijk, T., Gijis, K., Laarman, A., Meijer, J., & van de Pol, J. (2015). LTSmin: High-Performance Language-Independent Model Checking. In Tools and Algorithms for the Construction and Analysis of Systems (pp. 692–707). Springer Berlin Heidelberg. https://doi.org/10.1007/978-3-662-46681-0_61
Difference Constraints: An adequate Abstraction for Complexity Analysis of Imperative Programs / Sinn, M., Veith, H., & Zuleger, F. (2015). Difference Constraints: An adequate Abstraction for Complexity Analysis of Imperative Programs. In FMCAD (pp. 144–151). http://hdl.handle.net/20.500.12708/56391
Asymptotically Precise Ranking Functions for Deterministic Size-Change Systems / Zuleger, F. (2015). Asymptotically Precise Ranking Functions for Deterministic Size-Change Systems. In Lecture Notes in Computer Science (pp. 426–442). Springer. https://doi.org/10.1007/978-3-319-20297-6_27
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
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, FAIR, PROSEED, SEE
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
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

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
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
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
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
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
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
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
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
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
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
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
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
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
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 Lecture Notes in Computer Science (pp. 161–181). Springer / LNCS. https://doi.org/10.1007/978-3-642-54013-4_10
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 Lecture Notes in Computer Science (pp. 244–249). Springer / LNCS. https://doi.org/10.1007/978-3-642-54807-9_15
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
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
Parameterized Model Checking of Token-Passing Systems / Aminof, B., Jacobs, S., Khalimov, A., & Rubin, S. (2014). Parameterized Model Checking of Token-Passing Systems. In Lecture Notes in Computer Science (pp. 262–281). Springer / LNCS. https://doi.org/10.1007/978-3-642-54013-4_15
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 Lecture Notes in Computer Science (pp. 122–171). Springer. https://doi.org/10.1007/978-3-319-07317-0_4

2013

Under-Approximating Loops in C Programs for Fast Counterexample Detection / Kroening, D., Lewis, M., & Weissenbacher, G. (2013). Under-Approximating Loops in C Programs for Fast Counterexample Detection. In Computer Aided Verification (pp. 381–396). Springer / LNCS. https://doi.org/10.1007/978-3-642-39799-8_26
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
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
Advanced SAT Techniques for Abstract Argumentation / Wallner, J. P., Weissenbacher, G., & Woltran, S. (2013). Advanced SAT Techniques for Abstract Argumentation. In Lecture Notes in Computer Science (pp. 138–154). Springer / LNCS. https://doi.org/10.1007/978-3-642-40624-9_9
First-Order Theorem Proving and Vampire / Kovács, L., & Voronkov, A. (2013). First-Order Theorem Proving and Vampire. In N. Sharygina & H. Veith (Eds.), Computer Aided Verification (pp. 1–35). Springer LNCS 8044. https://doi.org/10.1007/978-3-642-39799-8_1
Challenges in compiler construction for secure two-party computation / Holzer, A., Karvelas, N., Katzenbeisser, S., & Veith, H. (2013). Challenges in compiler construction for secure two-party computation. In Proceedings of the First ACM workshop on Language support for privacy-enhancing technologies - PETShop ’13. Workshop on language support for privacy-enhancing technologies (PETShop), Berlin, Deutschland, EU. ACM. https://doi.org/10.1145/2517872.2517876
The first workshop on language support for privacy-enhancing technologies (PETShop'13) / Franz, M., Holzer, A., Majumdar, R., Parno, B., & Veith, H. (2013). The first workshop on language support for privacy-enhancing technologies (PETShop’13). In Proceedings of the 2013 ACM SIGSAC conference on Computer & communications security - CCS ’13. ACM Conference on Computer and Communications Security (CCS), Washington, USA, Non-EU. ACM. https://doi.org/10.1145/2508859.2509032
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 FSTTCS (pp. 377–388). Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik. https://doi.org/10.4230/LIPIcs.FSTTCS.2013.377
Solving Constraints for Generational Search / Pötzl, D., & Holzer, A. (2013). Solving Constraints for Generational Search. In Tests and Proofs (pp. 197–213). Springer / LNCS. https://doi.org/10.1007/978-3-642-38916-0_12
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
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
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

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
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
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
Proving Reachability Using FShell / Holzer, A., Kroening, D., Schallhart, C., Tautschnig, M., & Veith, H. (2012). Proving Reachability Using FShell. In C. Flanagan & B. König (Eds.), Tools and Algorithms for the Construction and Analysis of Systems (pp. 538–541). Springer. https://doi.org/10.1007/978-3-642-28756-5_43
Who is afraid of Model Checking Distributed Algorithms? / Konnov, I., Veith, H., & Widder, J. (2012). Who is afraid of Model Checking Distributed Algorithms? Workshop on Exploiting Concurrency Efficiently and Correctly, Berkeley, CA, USA, Non-EU. http://hdl.handle.net/20.500.12708/85358
Who is afraid of Model Checking Distributed Algorithms? / John, A., Konnov, I., Schmid, U., Veith, H., & Widder, J. (2012). Who is afraid of Model Checking Distributed Algorithms? PUMA/RISE Seminar, Traunkirchen, Austria. http://hdl.handle.net/20.500.12708/85435
Secure Two-Party Computation in ANSI C / Veith, H. (2012). Secure Two-Party Computation in ANSI C. Dagstuhl Seminar 12461: Games and Decisions for Rigorous Systems Engineering, Dagstuhl, Deutschland, EU. http://hdl.handle.net/20.500.12708/85434
Labelled Interpolation Systems / Weissenbacher, G. (2012). Labelled Interpolation Systems. Dagstuhl Seminar 12461: Games and Decisions for Rigorous Systems Engineering, Dagstuhl, Deutschland, EU. http://hdl.handle.net/20.500.12708/85433
Parameterized Model Checking of Fault-tolerant Distributed Algorithms / John, A., Konnov, I., Schmid, U., Veith, H., & Widder, J. (2012). Parameterized Model Checking of Fault-tolerant Distributed Algorithms. Dagstuhl Seminar 12461: Games and Decisions for Rigorous Systems Engineering, Dagstuhl, Deutschland, EU. http://hdl.handle.net/20.500.12708/85432
Counter Attack against Byzantine Generals / John, A., Konnov, I., Schmid, U., Veith, H., & Widder, J. (2012). Counter Attack against Byzantine Generals. Alpine Verification Meeting, IST Austria, Austria. http://hdl.handle.net/20.500.12708/85359
Interpretations in Trees with Countably Many Branches / Rabinovich, A., & Rubin, S. (2012). Interpretations in Trees with Countably Many Branches. In 2012 27th Annual IEEE Symposium on Logic in Computer Science. Symposium on Logic in Computer Science (LICS), Edinburgh, United Kingdom, EU. IEEE. https://doi.org/10.1109/lics.2012.65
Interpolant Strength Revisited / Weissenbacher, G. (2012). Interpolant Strength Revisited. In Theory and Applications of Satisfiability Testing – SAT 2012 (pp. 312–326). LNCS / Springer. https://doi.org/10.1007/978-3-642-31612-8_24
Wait-Free Stabilizing Dining Using Regular Registers / Sastry, S., Welch, J. L., & Widder, J. (2012). Wait-Free Stabilizing Dining Using Regular Registers. In Lecture Notes in Computer Science (pp. 284–299). LNCS / Springer. https://doi.org/10.1007/978-3-642-35476-2_20
Vinter: A Vampire-Based Tool for Interpolation / Hoder, K., Holzer, A., Kovács, L., & Voronkov, A. (2012). Vinter: A Vampire-Based Tool for Interpolation. In Programming Languages and Systems (pp. 148–156). Springer / LNCS. https://doi.org/10.1007/978-3-642-35182-2_11
A Myhill-Nerode theorem for automata with advice / Kruckman, A., Rubin, S., Sheridan, J., & Zax, B. (2012). A Myhill-Nerode theorem for automata with advice. In M. Faella & A. Murano (Eds.), Electronic Proceedings in Theoretical Computer Science (pp. 238–246). Electronic Proceedings in Theoretical Computer Science. https://doi.org/10.4204/eptcs.96.18
Coverage-Based Trace Signal Selection for Fault Localisation in Post-silicon Validation / Charlie Shucheng, Z., Weissenbacher, G., & Malik, S. (2012). Coverage-Based Trace Signal Selection for Fault Localisation in Post-silicon Validation. In Hardware and Software: Verification and Testing (pp. 132–147). Lecture Notes in Computer Science. Springer Verlag. https://doi.org/10.1007/978-3-642-39611-3_16
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
Parallel Assertions for Architectures with Weak Memory Models / Schwartz-Narbonne, D., Weissenbacher, G., & Malik, S. (2012). Parallel Assertions for Architectures with Weak Memory Models. In Automated Technology for Verification and Analysis (pp. 254–268). Lecture Notes in Computer Science. Springer Verlag. https://doi.org/10.1007/978-3-642-33386-6_21
Efficient Checking of Link-Reversal-Based Concurrent Systems / Függer, M., & Widder, J. (2012). Efficient Checking of Link-Reversal-Based Concurrent Systems. In Lecture Notes in Computer Science (pp. 486–499). Lecture Notes in Computer Science. Springer Verlag. https://doi.org/10.1007/978-3-642-32940-1_34
Bounded-Interference Sequentialization for Testing Concurrent Programs / Razavi, N., Farzan, A., & Holzer, A. (2012). Bounded-Interference Sequentialization for Testing Concurrent Programs. In Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change (pp. 372–387). Lecture Notes in Computer Science. Springer Verlag. https://doi.org/10.1007/978-3-642-34026-0_28

2011

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
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
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
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
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, Rise-TOOLS
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

2010

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

2007

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

Theses

Note: Due to the rollout of TU Wien’s new publication database, the list below may be slightly outdated. Once the migration is complete, everything will be up to date again.

2023

Enhancing Abstraction and Symbolic Execution for Shape Analysis of C-Programs operating on Linked Lists / Kaindlstorfer, D. (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

2022

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

2021

Starkes modellbasiertes Mutationstesten / Fellner, A. (2021). Starkes modellbasiertes Mutationstesten [Dissertation, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2021.88481
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
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
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
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
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

2020

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
Automated reasoning over Arrays in the superposition calculus
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
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
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
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
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
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
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
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
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
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

2019

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

2018

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

2014

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

Awards

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

And more…

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 .

Services

Institutes

Research Units

Formal Methods in Systems Engineering E192-04

Contact

On This Page

About

Professors

Scientific Staff

Administrative Staff

Student Staff

External Lecturers

Courses

2022W

2023S

Projects

Publications

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

2007

2006

2005

2003

2002

Theses

2023

2022

2021

2020

2019

2018

2016

2015

2014

Awards

And more…