Formal Methods in Systems Engineering E192-04
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.

Contact
- Head: Laura Kovacs
- Web: www.forsyte.tuwien.ac.at
- Phone: +43-1-58801-18404
- Location: Favoritenstrasse 9-11
On This Page
About
We at the Formal Methods in Systems Engineering (FORSYTE) group are concerned with the development of new methods and tools for the design and analysis of computer systems, including software, hardware and distributed systems.
Our techniques are based on solid mathematical foundations, with a special focus on program analysis and verification, model checking, synthesis, automated reasoning, symbolic computation and automated testing. Fundamental research topics include software model checking, test case generation, static analysis, protocol verification, and formal methods for distributed and concurrent systems. Industrial research is focusing on low-level software, and embedded systems in the avionics and automotive sector.
The research Unit Formal Methods in Systems Engineering is part of the Institute of Logic and Computation.
Professors
Scientific Staff
Administrative Staff
Student Staff
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 fü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 .