2022W

• Bachelor Thesis / 184.695 / PR
• Computer Aided Verification / 181.145 / VU
• Computer-Aided Verification / 181.144 / 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

• Automated Reasoning with Theories and Induction for Software Technologies
  2021 – 2026 / European Commission
• 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)
• 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
• Domain-Specific Reasoning in IoT Applications
  2019 – 2020 / DoS-IoT
• 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
• Bit-level Accurate Reasoning and Interpolation
  2016 – 2020 / Microsoft Research Limited
• Tools for Concurrent and distributed Systems
  2011 – 2019 / Austrian Science Fund (FWF)

Note: Due to the rollout of TU Wien’s new publication database, the list below may be slightly outdated. Once APIs for the new database have been released, everything will be up to date again.

2022

• Moment-based Invariants for Probabilistic Loops with non-polynomial assignments / A. Kofnov, M. Moosbrugger, S. Stankovic, E. Bartocci, E. Bura / accepted as talk for: Proc. of QEST 2022: the 19th International Conference on Quantitative Evaluation of SysTems, Warsaw, Poland; 2022-09-12 - 2022-09-16; in: "Proc. of QEST'22: the 19th International Conference on Quantitative Evaluation of SysTems", (2022)
• Distribution Estimation for Probabilistic Loops / A. Karimi, S. Stankovic, M. Moosbrugger, L. Kovacs, E. Bartocci, E. Bura / accepted as talk for: Proc. of QEST 2022: the 19th International Conference on Quantitative Evaluation of SysTems, Warsaw, Poland; 2022-09-12 - 2022-09-16; in: "Proc. of QEST'22: the 19th International Conference on Quantitative Evaluation of SysTems", (2022)
• ATLAS: Automated Amortised Complexity Analysis of Self-adjusting Data Structures / L. Leutgeb, G. Moser, F. Zuleger / Talk: International Conference on Computer Aided Verification (CAV), virtuell; 2022-07-20 - 2022-07-23; in: "CAV 2021: Computer Aided Verification", (2022), 99 - 122
• Moment-based analysis of Bayesian network properties / S. Stankovic, E. Bartocci, L. Kovacs / Theoretical Computer Science, 903 (2022), 113 - 133

2021

• Bounded Model Checking of Speculative Non-Interference / E. Pescosta, G. Weissenbacher, F. Zuleger / Talk: 2021 IEEE/ACM International Conference On Computer Aided Design (ICCAD), München, Deutschland; 2021-11-01 - 2021-11-04; in: "2021 IEEE/ACM International Conference On Computer Aided Design (ICCAD)", IEEE, (2021), ISBN: 978-1-6654-4507-8; 1 - 9
• Induction with Recursive Definitions in Superposition / M. Hajdu, P. Hozzova, L. Kovacs, A. Voronkov / Talk: Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design - FMCAD 2021, New Haven, Connecticut, USA; 2021-10-19 - 2021-10-22; in: "Proceedings of the 21st International Conference on Formal Methods in Computer Aided Design (FMCAD)", R. Piskac, M. Wahlen (ed.); TU Wien Academic Press, 2 (2021), ISBN: 978-3-85448-046-4; 1 - 10
• Model Checking AUTOSAR Components with CBMC / T. Durand, K. Fazekas, G. Weissenbacher, J. Zwirchmayr / Talk: Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design - FMCAD 2021, New Haven, Connecticut, USA; 2021-10-19 - 2021-10-22; in: "Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design - FMCAD 2021", R. Piskac, M. Whalen (ed.); TU Wien Academic Press, 2 (2021), ISBN: 978-3-85448-046-4; 96 - 101
• Best-Effort Synthesis: Doing Your Best Is Not Harder Than Giving Up / B. Aminof, G. De Giacomo, S. Rubin / Talk: IJCAI 2021 - 30th International Joint Conference on Artificial Intelligence, Montreal, Canada; 2021-08-19 - 2021-08-27; in: "Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence (IJCAI-21)", (2021), 1766 - 1772
• Automated Generation of Exam Sheets for Automated Deduction / P. Hozzova, L. Kovacs, J. Rath / Talk: Proceedings of the 14th International Conference on Intelligent Computer Mathematics (CICM), Timisoara, Romania; 2021-07-26 - 2021-07-31; in: "Proceedings of the 14th International Conference on Intelligent Computer Mathematics (CICM)", Springer LNCS, 12833 (2021), 185 - 196
• Inductive Benchmarks for Automated Reasoning / M. Hajdu, P. Hozzova, L. Kovacs, J. Schoisswohl, A. Voronkov / Talk: Proceedings of the 14th International Conference on Intelligent Computer Mathematics (CICM), Timisoara, Romania; 2021-07-26 - 2021-07-31; in: "Proceedings of the 14th International Conference on Intelligent Computer Mathematics (CICM)", F. Kamareddine, C. Sacerdoti Coen (ed.); Springer LNCS, 12833 (2021), 124 - 129
• Summing Up Smart Transitions / N. Elad, S. Rain, N. Immerman, M. Sagiv, L. Kovacs / Talk: 33rd International Conference on Computer Aided Verification (CAV), Los Angeles, US; 2021-07-20 - 2021-07-23; in: "Proceedings of the 33rd International Conference on Computer Aided Verification (CAV)", A. Silva, R. Leino (ed.); Springer LNCS, 12759 (2021), 317 - 340
• Automating Induction by Reflection / J. Schoisswohl, L. Kovacs / Talk: 16th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP), Pittsburgh, USA; 2021-07-16; in: "Proceedings of the 16th Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP)", E. Pimentel, E. Tassi (ed.); EPTCS, 337 (2021), 39 - 54
• Integer Induction in Saturation / P. Hozzova, L. Kovacs, A. Voronkov / Talk: 28th International Conference on Automated Deduction (CADE 28), Virtual Event; 2021-07-12 - 2021-07-15; in: "Proceedings of the 28th International Conference on Automated Deduction (CADE-28)", A. Platzer, G. Sutcliffe (ed.); Springer LNCS, 12669 (2021), 361 - 377
• Strong-Separation Logic / J. Pagel, F. Zuleger / Talk: 30th European Symposium on Programming (ESOP 2021), Luxembourg (online); 2021-03-27 - 2021-04-01; in: "30th European Symposium on Programming, ESOP 2021", Springer, 12648 (2021), 664 - 692
• Automated Termination Analysis of Polynomial Probabilistic Programs / M. Moosbrugger, E. Bartocci, J. Katoen, L. Kovacs / Talk: 30th European Symposium on Programming (ESOP 2021), Luxembourg (online); 2021-03-27 - 2021-04-01; in: "Proc. of ESOP 2021: the 30th European Symposium on Programming", Springer, 12648 (2021), 491 - 518
• Eliminating Message Counters in Synchronous Threshold Automata / I. Stoilkovska, I. Konnov, J. Widder, F. Zuleger / Talk: 22nd International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), Copenhagen, Denmark; 2021-01-17 - 2021-01-19; in: "Proceedings of the 22nd International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI)", Springer LNCS, 12597 (2021), 196 - 218
• Algebra-Based Synthesis of Loops and Their Invariants / A. Humenberger, L. Kovacs / Talk: 22nd International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), Copenhagen, Denmark (invited); 2021-01-17 - 2021-01-19; in: "Proceedings of the 22n International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI)", F. Henglein, S. Shoham, Y. Vizel (ed.); Springer LNCS, 12597 (2021), 17 - 28
• Rely-guarantee bound analysis of parameterized concurrent shared-memory programs / T. Pani, G. Weissenbacher, F. Zuleger / Formal Methods in System Design, 57 (2021), 2; 270 - 302
• Mutation testing with hyperproperties / A. Fellner, M. Tabaei Befrouei, G. Weissenbacher / Journal of Software and Systems Modeling (online-edition), 20 (2021), 2; 405 - 427
• Algorithm selection and instance space analysis for curriculum-based course timetabling / A. De Coster, N. Musliu, A. Schaerf, J. Schoisswohl, K. Smith-Miles / Journal of Scheduling, 26 (2021), 4; 1 - 24
• Preface of the special issue on the conference on computer-aided verification 2018 / H. Chockler, G. Weissenbacher / Formal Methods in System Design, 57 (2021), 1; 1 - 2

2020

• ProbInG: Distribution Recovery for Invariant Generation of Probabilistic Programs / E. Bartocci, L. Kovacs, E. Bura / Talk: Vienna Science, Research and Technology Fund - ProbInG, online; 2020-12-14 - 2020-12-15
• Analysis of Bayesian Networks via Prob-Solvable Loops / E. Bartocci, L. Kovacs, S. Stankovic / Talk: Proc. of ICTAC 2020: the 17th International Colloquium on Theoretical Aspects of Computing, Macau S.A.R., China; 2020-11-30 - 2020-12-04; in: "Proc. of ICTAC 2020: the 17th International Colloquium on Theoretical Aspects of Computing", Springer, 12545 (2020), ISBN: 978-3-030-64275-4; 221 - 241
• Algebra-Based Loop Synthesis / A. Humenberger, N. Bjorner, L. Kovacs / Talk: Proceedings of the 16th International Conference on Integrated Formal Methods (iFM), Lugano, Switzerland; 2020-11-16 - 2020-11-20; in: "Proceedings of the 16th International Conference on Integrated Formal Methods", B. Dongol, E. Troubitsyna (ed.); Lecture Notes in Computer Science, Springer, 12546 (2020), ISBN: 978-0-9835678-9-9; 440 - 459
• Thread-modular Counter Abstraction for Parameterized Program Safety / T. Pani, G. Weissenbacher, F. Zuleger / Talk: International Conference on Formal Methods in Computer-Aided Design (FMCAD), Haifa, Israel; 2020-09-22 - 2020-09-24; in: "Formal Methods in Computer-Aided Design", TU Wien Academic Press / IEEE, 1 (2020), ISBN: 978-3-85448-042-6; 67 - 76
• Trace Logic for Inductive Loop Reasoning / P. Georgiou, B. Gleiss, L. Kovacs / Talk: 20th International Conference on Formal Methods in Computer-Aided Design (FMCAD), Haifa, Israel; 2020-09-21 - 2020-09-24; in: "Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design - FMCAD 2020", A. Ivrii, O. Strichman (ed.); IEEE, (2020), ISBN: 978-3-85448-042-6; 255 - 263
• An ExpTime Upper Bound for ALC with Integers / N. Labai, M. Simkus, M. Ortiz de la Fuente / Talk: 17th International Conference on Principles of Knowledge Representation and Reasoning, KR 2020, Rhodes, Greece; 2020-09-12 - 2020-09-18; in: "Proceedings of the 17th International Conference on Principles of Knowledge Representation and Reasoning, KR 2020", D. Calvanese, E. Erdem, M. Thielscher (ed.); AAAI Press, (2020), ISSN: 2334-1033; 614 - 623
• Synthesizing Best-effort Strategies under Multiple Environment Specifications / B. Aminof, G. De Giacomo, A. Lomuscio, A. Murano, S. Rubin / Talk: KR 2021 - 18th International Conference on Principles of Knowledge Representation and Reasoning, Rhodes, Greece; 2020-08-13 - 2020-08-14; in: "KR 2021 - 18th International Conference on Principles of Knowledge Representation and Reasoning", (2020), 42 - 51
• Induction with Generalization in Superposition Reasoning / M. Hajdu, P. Hozzova, L. Kovacs, J. Schoisswohl, A. Voronkov / Talk: Proceedings of the 13th International Conference on Intelligent Computer Mathematics (CICM), Bertinoro, Italy; 2020-07-26 - 2020-07-31; in: "Proceedings of the 13th International Conference on Intelligent Computer Mathematics", Lecture Notes in Computer Science, Springer, 12236 (2020), ISBN: 978-0-9835678-9-9; 123 - 137
• Formalizing Graph Trail Properties in Isabelle/HOL / L. Kovacs, Hanna Lachnitt, S. Szeider / Talk: International Conference on Intelligent Computer Mathematics (CICM), Bertinoro, Forli, Italy; 2020-07-26 - 2020-07-31; in: "CICM 2020: Intelligent Computer Mathematics", LNCS, 12236 (2020), ISBN: 978-3-030-53518-6; 190 - 205
• Multi-linear Strategy Extraction for QBF Expansion Proofs via Local Soundness / M. Schlaipfer, F. Slivovsky, G. Weissenbacher, F. Zuleger / Talk: International Conference on the Theory and Applications of Satisfiability Testing, Alghero, Italien; 2020-07-03 - 2020-07-10; in: "SAT 2020: Theory and Applications of Satisfiability Testing - SAT 2020", LNCS, 12178 (2020), ISBN: 978-3-030-51824-0; 429 - 446
• Subsumption Demodulation in First-Order Theorem Proving / B. Gleiss, L. Kovacs, J. Rath / Talk: 10th International Joint Conference on Automated Reasoning (IJCAR), Paris; 2020-07-01 - 2020-07-04; in: "Proceedings of the 10th International Joint Conference on Automated Reasoning (IJCAR)", N. Peltier, V. Sofronie-Stokkermans (ed.); Lecture Notes in Computer Science, Springer, 12166 (2020), ISBN: 978-3-030-51073-2; 297 - 315
• Layered Clause Selection for Theory Reasoning (Short Paper) / B. Gleiss, M. Suda / Talk: 10th International Joint Conference on Automated Reasoning (IJCAR), Paris; 2020-07-01 - 2020-07-04; in: "Proceedings of the 10th International Joint Conference on Automated Reasoning (IJCAR)", N. Peltier, V. Sofronie-Stokkermans (ed.); Lecture Notes in Computer Science, Springer, 12166 (2020), ISBN: 978-3-030-51073-2; 402 - 409
• Layered Clause Selection for Saturation-Based Theorem Proving / B. Gleiss, M. Suda / Talk: Joint Proceedings of the 7th Workshop on Practical Aspects of Automated Reasoning (PAAR) and the 5th Satisfiability Checking and Symbolic Computation Workshop (SC-Square) Workshop, Paris; 2020-06-30 - 2020-07-01; in: "Joint Proceedings of the 7th Workshop on Practical Aspects of Automated Reasoning (PAAR) and the 5th Satisfiability Checking and Symbolic Computation Workshop (SC-Square) Workshop", P. Fontaine, K. Korovin, I. Kotsireas et al. (ed.); CEUR Workshop Proceedings, 2752 (2020), 34 - 52
• RAT Elimination / A. Rebola Pardo, G. Weissenbacher / Talk: International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), Alicante, Spain; 2020-05-22 - 2020-05-27; in: "Logic for Programming, Artificial Intelligence and Reasoning", L. Kovacs, E. Albert (ed.); EasyChair, 73 (2020), 423 - 448
• Mora - Automatic Generation of Moment-Based Invariants / E. Bartocci, L. Kovacs, S. Stankovic / Talk: Proc. of TACAS 2020: the 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Dublin, Ireland; 2020-04-25 - 2020-04-30; in: "Proc. of TACAS 2020: the 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems", Springer, 12078 (2020), ISBN: 978-3-030-45189-9; 492 - 498
• Pebble-Intervals Automata and FO2 with Two Orders / N. Labai, T. Kotek, M. Ortiz de la Fuente, H. Veith / Talk: Language and Automata Theory and Applications (LATA), Milan, Italy; 2020-03-04 - 2020-03-06; in: "14th International Conference on Language and Automata Theory and Applications", Lecture Notes in Computer Science (LNCS), 12038 (2020), ISBN: 978-3-030-40608-0; 208 - 221
• Language Inclusion for Finite Prime Event Structures / A. Fellner, T. Tarrach, G. Weissenbacher / Talk: International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), New Orleans, LA, USA; 2020-01-16 - 2020-01-21; in: "Verification, Model Checking, and Abstract Interpretation", Springer, LNCS 11990 (2020), ISBN: 978-3-030-39321-2; 314 - 336
• Proceedings of the 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-23) / E Albert, L. Kovacs / EasyChair EPiC Series in Computing, Alicante, Spain, 2020, ISSN: 2398-7340; 516 pages
• Proceedings of the 31st International Conference on Concurrency Theory (CONCUR) / I. Konnov, L. Kovacs / Dagstuhl Publishing LIPICS, Vienna, Austria, 2020, ISBN: 978-3-95977-160-3; 984 pages
• Extracting safe thread schedules from incomplete model checking results / P. Metzler, N. Suri, G. Weissenbacher / International Journal on Software Tools for Technology Transfer, 22 (2020), 5; 565 - 581
• Synthesizing strategies under expected and exceptional environment behaviors / B. Aminof, G. De Giacomo, A. Lomuscio, A. Murano, S. Rubin / in: "Proceedings of the Twenty-Ninth International Joint Conference on Artificial Intelligence", International Joint Conferences on Artificial Intelligence Organization, 2020, 1674 - 1680
• Stochastic Fairness and Language-Theoretic Fairness in Planning in Nondeterministic Domains / B. Aminof, G. De Giacomo, S. Rubin / in: "Proceedings of the Thirtieth International Conference on Automated Planning and Scheduling, Nancy, France", AAAI Press, 2020, 20 - 28
• Beyond Symbolic Heaps: Deciding Separation Logic With Inductive Definitions / J. Pagel, F. Zuleger / in: "23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Alicante, Spain", 73; EasyChair EPiC Series in Computing, 2020, 390 - 408
• The Polynomial Complexity of Vector Addition Systems with States / F. Zuleger / in: "Foundations of Software Science and Computation Structures - 23rd International Conference, Dublin, Ireland", 12077; Springer LNCS, 2020, 622 - 641
• Eliminating Message Counters in Threshold Automata / I. Stoilkovska, I. Konnov, J. Widder, F. Zuleger / in: "Automated Technology for Verification and Analysis - 18th Symposium, 2020, Hanoi, Vietnam", 12302; Springer LNCS, 2020, 196 - 212
• Preface of the Special Issue on the Conference on Formal Methods in Computer-Aided Design 2017 / D. Stewart, G. Weissenbacher / Formal Methods in System Design, 56 (2020), 1-3; 1
• An ExpTime Upper Bound for ALC with Integers (Extended Version) / N. Labai, M. Simkus, M. Ortiz de la Fuente / Report for arXiv; Report No. 2006.02078, 2020; 36 pages

2019

• Interactive Visualization of Saturation Attempts in Vampire / B. Gleiss, L. Kovacs, L. Schnedlitz / Talk: 15th International Conference on Integrated Formal Methods (iFM) 2019, Bergen, Norway; 2019-12-02 - 2019-12-06; in: "Proceedings of the 15th International Conference on Integrated Formal Methods (iFM) 2019", W. Ahrendt, S. Lizeth (ed.); Lecture Notes in Computer Science, Springer, 11918 (2019), 504 - 513
• First-Order Interpolation / L. Kovacs / Talk: PhD Research Seminar in Logic and Computation, Faculty of Informatics, West University of Timisoara, Timisoara, Romania (invited); 2019-11-29
• Formal Methods in the Digital World (in Hungarian) / L. Kovacs / Keynote Lecture: JegKepzes Series of Presentations- Hungarian Scientists from the Bartok Bela Highschool, Timisoara, Romania (invited); 2019-11-27
• APRe, Vampire, Welcome in Vienna! / L. Kovacs / Talk: APRe 2019 Workshop, TU Wien, TU Wien, Vienna; 2019-11-05 - 2019-11-06
• Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops / E. Bartocci, L. Kovacs, S. Stankovic / Talk: ATVA 2019: the 17th International Symposium on Automated Technology for Verification and Analysis, Taipei, Taiwan; 2019-10-28 - 2019-10-31; in: "Proc. of ATVA 2019: the 17th International Symposium on Automated Technology for Verification and Analysis", 11781 (2019), 255 - 276
• Subsumption Demodulation in First-Order Theorem Proving / J. Rath / Talk: First International Workshop on Proof Theory for Automated Deduction, Automated Deduction for Proof Theory, Funchal, Portugal; 2019-10-23 - 2019-10-25
• Verifying Relational Properties using Trace Logic / L. Kovacs / Talk: First International Workshop on Proof Theory for Automated Deduction, Automated Deduction for Proof Theory, Funchal, Portugal; 2019-10-23 - 2019-10-25
• Verifying Relational Properties using Trace Logic / G. Barthe, R. Eilers, P. Georgiou, B. Gleiss, L. Kovacs, M. Maffei / Talk: International Conference on Formal Methods in Computer Aided Design (FMCAD) 2019, San Jose, US; 2019-10-22 - 2019-10-25; in: "Proceedings of Formal Methods in Computer Aided Design (FMCAD)", B. Clark, J. Yang (ed.); IEEE, https://ieeexplore.ieee.org/xpl/conhome/8891869/proceeding (2019), ISBN: 978-0-9835678-9-9; 170 - 178
• Trace Reasoning for Formal Verification using the First-Order Superposition Calculus / P. Georgiou, B. Gleiss, L. Kovacs, M. Maffei / Poster: FMCAD 2019 Student Forum, San Jose, US; 2019-10-22 - 2019-10-25
• Mutation Testing with Hyperproperties / A. Fellner, M. Tabaei Befrouei, G. Weissenbacher / Talk: 17th International Conference on Software Engineering and Formal Methods, Oslo, Norway; 2019-09-18 - 2019-09-20; in: "Proc. of SEFM 2019: the 17th International Conference on Software Engineering and Formal Methods", 11724 (2019), 203 - 221
• Automatic Analysis for Prob-Solvable Loops / S. Stankovic / Talk: 13th Alpine Verification Meeting (AVM), Brno, Czech Republic; 2019-09-09 - 2019-09-11
• Superposition Reasoning about Quantified Bitvector Formulas / D. Damestani, L. Kovacs, M. Suda / Talk: 21st International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC) 2019, Timisoara, Romania; 2019-09-04 - 2019-09-07; in: "Proceedings of the 21st International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC), 2019", H. Hong, D. Zaharie (ed.); IEEE, (2019), ISBN: 978-1-7281-5724-5; 95 - 99
• Portfolio SAT and SMT Solving of Cardinality Constraints in Sensor Network Optimization / G. Kovasznai, K. Gajdar, L. Kovacs / Talk: 21st International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC) 2019, Timisoara, Romania; 2019-09-04 - 2019-09-07; in: "Proceedings of the 21st International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC), 2019", H. Hong, D. Zaharie (ed.); IEEE, (2019), ISBN: 978-1-7281-5724-5; 85 - 91
• Model-Based Diagnosis with Multiple Observations / A. Ignatiev, A. Morgado, J. Marques-Silva, G. Weissenbacher / Talk: IJCAI 2019 - 28th International Joint Conference on Artificial Intelligence, Macao, China; 2019-08-10 - 2019-08-16; in: "International Joint Conference on Artificial Intelligence", (2019), ISBN: 978-0-9992411-4-1; 1108 - 1115
• Extracting Safe Thread Schedules from Incomplete Model Checking Results / P. Metzler, N. Suri, G. Weissenbacher / Talk: International SPIN Symposium on Model Checking of Software (SPIN), Beijing, China; 2019-07-15 - 2019-07-16; in: "Model Checking Software", LNCS, Springer, 11636 (2019), ISBN: 978-3-030-30922-0; 153 - 171
• Forward Subsumption Demodulation - Fast Conditional Rewriting in Vampire / B. Gleiss, L. Kovacs, J. Rath / Talk: Vampire 2019 - The Sixth Vampire Workshop, Lisbon, Portugal; 2019-07-07
• First Order Interpolation / L. Kovacs / Keynote Lecture: SAT/SMT/AR Summer School 2019, Lisbon, Portugal (invited); 2019-07-03 - 2019-07-06
• 60 Shades of Grey in Vampire / L. Kovacs / Talk: ANDREI-60: Automating New-Era Deductive Reasoning Event in Iberia, Tbilisi, Georgia; 2019-05-19 - 2019-05-23
• Symbolic Computation and Automated Reasoning for Program Analysis / L. Kovacs / Keynote Lecture: 23rd IEEE International Conference on Intelligent Engineering Systems (INES) 2019, Gödöllõ, Hungary (invited); 2019-04-25 - 2019-04-27
• Interpolation in the Grey Area of Proofs / L. Kovacs / Talk: Helmut Veith Memorial Workshop 2019, Turracher Höhe; 2019-03-17 - 2019-03-20
• Symbol Elimination and Vampire / L. Kovacs / Talk: Dagstuhl Seminar 19062 - Bringing CP, SAT and SMT together: Next Challenges in Constraint Solving, Schloss Dagstuhl, Germany; 2019-02-03 - 2019-02-06
• Removing apparent singularities of linear difference systems / M. Barkatou, M. Jaroschek / Journal of Symbolic Computation, to appear (2019)
• Model-based, Mutation-driven Test-case Generation Via Heuristic-guided Branching Search / A. Fellner, W. Krenn, R. Schlick, T. Tarrach, G. Weissenbacher / ACM Transactions on Embedded Computing Systems, 18 (2019), 1
• Planning under LTL Environment Specifications / B. Aminof, G. De Giacomo, A. Murano, S. Rubin / in: "29th International Conference on Automated Planning and Scheduling", AAAI Press, 2019, 31 - 39
• Probabilistic Strategy Logic / B. Aminof, M. Kwiatkowska, B. Maubert, A. Murano, S. Rubin / in: "28th International Joint Conference on Artificial Intelligence", International Joint Conferences on Artificial Intelligence, 2019, 32 - 38
• Effective Entailment Checking for Separation Logic with Inductive Definitions / J. Pagel, C. Matheja, F. Zuleger / in: "25th International Conference, TACAS 2019", Springer, 2019, 319 - 336
• SL-COMP: Competition of Solvers for Separation Logic / M. Sighireanu, J. Pagel, C. Matheja, T. Noll, F. Zuleger et al. / in: "25th International Conference, TACAS 2019", Springer, 2019, 116 - 132
• Verifying Safety of Synchronous Fault-Tolerant Algorithms by Bounded Model Checking / I. Stoilkovska, I. Konnov, J. Widder, F. Zuleger / in: "International Conference on Tools and Algorithms for the Construction and Analysis of Systems", Springer, 2019, 357 - 374
• Verification of Randomized Consensus Algorithms Under Round-Rigid Adversaries / N. Bertrand, I. Konnov, M. Lazić, J. Widder / in: "30th International Conference on Concurrency Theory", Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany, 2019, 33:1 - 33:15
• Communication-Closed Asynchronous Protocols / A. Damian, C. Dragoi, A. Militaru, J. Widder / in: "International Conference on Computer Aided Verification", Springer, 2019, 344 - 363
• Foreword / J. Davenport, L. Kovacs, D. Zaharie / Mathematics in Computer Science, 13 (2019), 4; 459 - 460
• Foreword - Formalization of geometry, automated and interactive geometric reasoning / P. Schreck, T. Ida, L. Kovacs / Annals of Mathematics and Artificial Intelligence, 85 (2019), 2-4; 71 - 72
• Pebble-Intervals Automata and FO2 with Two Orders (Extended Version / N. Labai, T. Kotek, M. Ortiz de la Fuente, H. Veith / Report for CoRR; Report No. 1912.00171, 2019; 45 pages

2018

• Symbol Elimination in Program Analysis / L. Kovacs / Keynote Lecture: 2nd Facebook Testing and Veri cation Symposium (FaceTAV), London, UK (invited); 2018-11-28 - 2018-11-29
• Loop Analysis by Quantification over Iterations / B. Gleiss, L. Kovacs, S. Robillard / Talk: 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), Awassa, Ethiopia; 2018-11-16 - 2018-11-21; in: "Proceedings of the 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR)", G. Barthe, G. Sutcliffe, M. Veanes (ed.); EasyChair EPiC Series in Computing, 57 (2018), 381 - 399
• Towards Smarter MACE-style Model Finders / M. Janota, M. Suda / Talk: 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), Awassa, Ethiopia; 2018-11-16 - 2018-11-21; in: "LPAR-22. 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Awassa, Ethiopia, 16-21 November 2018.", EasyChair EPiC Series in Computing, 57 (2018), 454 - 470
• A Theory of Satisfiability-Preserving Proofs in SAT Solving / A. Rebola Pardo, M. Suda / Talk: International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), Awassa, Ethiopia; 2018-11-16 - 2018-11-21; in: "International Conference on Logic for Programming, Artificial Intelligence and Reasoning", EasyChair EPiC Series in Computing, 57 / Lpar-22 (2018), 583 - 603
• ByMC: Byzantine Model Checker / I. Konnov, J. Widder / Talk: International Symposium on Leveraging Applications of Formal Methods (ISoLA), Limasol, Zypern; 2018-11-05 - 2018-11-09; in: "ISOLA", Lecture Notes in Computer Science. Springer Verlag., 11246 (2018), ISBN: 978-3-642-34025-3; 327 - 342
• Synthesis under Assumptions / B. Aminof, G. De Giacomo, A. Murano, S. Rubin / Poster: Principles of Knowledge Representation and Reasoning (KR), Tempe, Arizona; 2018-10-30 - 2018-11-02; in: "Principles of Knowledge Representation and Reasoning: Proceedings of the Sixteenth International Conference, KR 2018, Tempe, Arizona, 30 October - 2 November 2018", AAAI Press, (2018), ISBN: 978-1-57735-803-9; 615 - 616
• Rely-Guarantee Reasoning for Automated Bound Analysis of Lock-Free Algorithms / T. Pani, G. Weissenbacher, F. Zuleger / Talk: International Conference on Formal Methods in Computer-Aided Design (FMCAD), Austin, TX; 2018-10-30 - 2018-11-02; in: "Formal Methods in Computer-Aided Design", FMCAD Inc., (2018), ISBN: 978-0-9835678-8-2; 1 - 9
• Using Loop Bound Analysis For Invariant Generation / P. Čadek, C. Danninger, M. Sinn, F. Zuleger / Talk: International Conference on Formal Methods in Computer-Aided Design (FMCAD), Austin, TX; 2018-10-30 - 2018-11-02; in: "Formal Methods in Computer-Aided Design", FMCAD Inc., (2018), ISBN: 978-0-9835678-8-2; 1 - 9
• Symbol Elimination for Program Analysis / L. Kovacs / Keynote Lecture: Highlights of Logic, Games and Automata, Berlin, Germany (invited); 2018-09-18 - 2018-09-21
• Reachability in Parameterized Systems: All Flavors of Threshold Automata / J. Kukovec, I. Konnov, J. Widder / Talk: International Conference on Concurrency Theory (CONCUR), Bejing, China; 2018-09-04 - 2018-09-07; in: "29th International Conference on Concurrency Theory (CONCUR 2018)", Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH, Dagstuhl Publishing, 118 (2018), ISBN: 978-3-95977-087-3; 19:1 - 19:17
• Inductive Termination Proofs with Transition Invariants and Their Relationship to the Size-Change Abstraction / F. Zuleger / Talk: International Static Analysis Symposium (SAS), Freiburg, Germany; 2018-08-29 - 2018-08-31; in: "Static Analysis - 25th International Symposium, SAS 2018, Freiburg, Germany, August 29-31, 2018, Proceedings", Springer, Lecture Notes in Computer Science (2018), ISBN: 978-3-319-99724-7; 423 - 444
• First-Order Interpolation in the Grey Area of Proofs / L. Kovacs / Keynote Lecture: Summer School on Syntax meets Semantics - Methods, Interactions, and Connections in Substructural Logics (SYSMICS), Les Diablerets, Switzerland (invited); 2018-08-22 - 2018-08-26
• Extended Resolution Simulates DRAT / B. Kiesl, A. Rebola Pardo, M. Heule / Keynote Lecture: 9th International Joint Conference on Automated Reasoning (IJCAR) 2018, Oxford; 2018-08-14 - 2018-08-17; in: "Proceedings of the 9th International Joint Conference on Automated Reasoning (IJCAR) 2018", LNCS, 10900 (2018), ISBN: 978-3-319-94204-9; 516 - 531
• A Separation Logic with Data: Small Models and Automation / J. Pagel, D. Jovanovic, G. Weissenbacher / Talk: 9th International Joint Conference on Automated Reasoning (IJCAR) 2018, Oxford; 2018-08-14 - 2018-08-17; in: "Automated Reasoning", LNCS, 10900 (2018), ISBN: 978-3-319-94204-9; 455 - 471
• A FOOLish Encoding of the Next State Relations of Imperative Programs. / E. Kotelnikov, L. Kovacs, A. Voronkov / Talk: 9th International Joint Conference on Automated Reasoning (IJCAR) 2018, Oxford; 2018-08-14 - 2018-08-17; in: "Proceedings of the 9th International Joint Conference on Automated Reasoning (IJCAR) 2018", LNCS, 10900 (2018), 405 - 421
• Aligator.jl - A Julia Package for Loop Invariant Generation / A. Humenberger, M. Jaroschek, L. Kovacs / Talk: 11th International Conference on Intelligent Computer Mathematics (CICM), Hagenberg; 2018-08-13 - 2018-08-17; in: "Proceedings of the 11th International Conference on Intelligent Computer Mathematics (CICM)", F. Rabe et al. (ed.); LNCS, 11006 (2018), 111 - 117
• Desingularization of First Order Linear Difference Systems with Rational Function Coefficients / M. Barkatou, M. Jaroschek / Talk: 2018 ACM International Symposium on Symbolic and Algebraic Computation (ISSAC), New York, US; 2018-07-16 - 2018-07-19; in: "Proceedings of the 2018 ACM International Symposium on Symbolic and Algebraic Computation (ISSAC)", M. Kauers et al. (ed.); (2018), 39 - 46
• Efficient Algorithms for Asymptotic Bounds on Termination Time in VASS / T. Brazdil, K. Chatterjee, A. Kucera, P. Novotny, D. Velan, F. Zuleger / Talk: Symposium on Logic in Computer Science (LICS), Oxford; 2018-07-09 - 2018-07-12; in: "Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018", ACM, Oxford (2018), 185 - 194
• Local Soundness for QBF Calculi / M. Suda, B. Gleiss / Talk: 21st International Conference on Theory and Applications of Satisfiability Testing (SAT), Oxford, UK; 2018-07-09 - 2018-07-12; in: "Proceedings of the 21st International Conference on Theory and Applications of Satisfiability Testing (SAT)", O. Beyersdorff, C. Wintersteiger (ed.); LNCS, 10929 (2018), 217 - 234
• First-Order Interpolation / L. Kovacs / Keynote Lecture: SAT/SMT/AR Summer School 2018, Manchester (invited); 2018-07-03 - 2018-07-06
• Automated clustering and program repair for introductory programming assignments / I. Radicek, S. Gulwani, F. Zuleger / Talk: Conference on Programming Language Design and Implementation (PLDI), Philadelphia, PA, USA; 2018-06-18 - 2018-06-22; in: "Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2018, Philadelphia, PA, USA, June 18-22, 2018", ACM, (2018), 465 - 480
• Automated Reasoning for Systems Engineering / L. Kovacs / Keynote Lecture: Foundations of Information and Knowledge Systems (FOIKS) 2018, Budapest, Hungary (invited); 2018-05-14 - 2018-05-18; in: "Foundations of Information and Knowledge Systems (FOIKS) 2018", LNCS, 10833 (2018), 1
• Automated Reasoning for Rigorous Systems Engineering / L. Kovacs / Keynote Lecture: RiSE/SHINE Media Seminar 2018, Vienna (invited); 2018-05-07
• Communication-Closed Layers as Paradigm for Distributed Systems: A Manifesto / C. Dragoi, M. Lazić, J. Widder / Talk: Sinteza 2018 International Scientific Conference on Information Technology and Data Related Research, Belgrad, Serbien (invited); 2018-04-20; in: "Sinteza 2018 International Scientific Conference on Information Technology and Data Related Research", Singidunum University, 15 (2018), 131 - 138
• Unification with Abstraction and Theory Instantiation in Saturation-Based Reasoning / G. Reger, M. Suda, A. Voronkov / Talk: 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Thessaloniki, Greece; 2018-04-14 - 2018-04-20; in: "Proceedings of the 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)", D. Beyer, M. Huisman (ed.); LNCS, 10805 (2018), 3 - 22
• First-Order Theorem Proving in Rigorous Systems Engineering / L. Kovacs, A. Voronkov / Keynote Lecture: RiSE/SHiNE Winter School 2018, Wien (invited); 2018-02-05 - 2018-02-09
• Automated Reasoning for Systems Engineering / L. Kovacs / Keynote Lecture: 2018 IEEE International Conference on Future IoT Technologies (Future IoT 2018), Eger, Hungary (invited); 2018-01-18 - 2018-01-19
• Monadic refinements for relational cost analysis / I. Radicek, G. Barthe, M. Gaboardi, D. Garg, F. Zuleger / Talk: 45th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2018), Los Angeles; 2018-01-10 - 2018-01-12; in: "Proceedings of the ACM on Programming Languages", ACM Digital Library, New York, NY, USA (2018), 1 - 32
• From Shapes to Amortized Complexity / T. Fiedor, L. Holik, A. Rogalewicz, M. Sinn, T. Vojnar, F. Zuleger / Talk: International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), Los Angeles; 2018-01-07 - 2018-01-09; in: "Verification, Model Checking, and Abstract Interpretation - 19th International Conference, VMCAI 2018, Los Angeles, CA, USA, January 7-9, 2018, Proceedings", LNCS, 10747 (2018), ISBN: 978-3-319-73720-1; 205 - 225
• Parameterized Model Checking of Synchronous Distributed Algorithms by Abstraction / B. Aminof, I. Stoilkovska, S. Rubin, J. Widder, F. Zuleger / Talk: International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), Los Angeles; 2018-01-07 - 2018-01-09; in: "Verification, Model Checking, and Abstract Interpretation - 19th International Conference, VMCAI 2018, Los Angeles, CA, USA, January 7-9, 2018, Proceedings", LNCS, 10747 (2018), ISBN: 978-3-319-73720-1; 1 - 24
• Parameterized Model Checking of Synchronous Distributed Algorithms by Abstraction / B. Aminof, S. Rubin, I. Stoilkovska, J. Widder, F. Zuleger / Talk: Verification, Model Checking, and Abstract Interpretation (VMCAI), Los Angeles; 2018-01-07 - 2018-01-09; in: "VMCAI", LNCS/Springer, 10747 (2018), 1 - 24
• Invariant Generation for Multi-Path Loops with Polynomial Assignments / A. Humenberger, M. Jaroschek, L. Kovacs / Talk: Verification, Model Checking, and Abstract Interpretation (VMCAI), Los Angeles; 2018-01-07 - 2018-01-09; in: "Verification, Model Checking, and Abstract Interpretation - 19th International Conference", Springer, (2018), ISBN: 978-3-319-73720-1; 226 - 246
• Computer Aided Verification 2018 - Part II / H. Chockler, G. Weissenbacher / Springer, 2018, ISBN: 978-3-319-96141-5
• Computer Aided Verification 2018 - Part I / H. Chockler, G. Weissenbacher / Springer, 2018, ISBN: 978-3-319-96144-6
• Vampire 2017. Proceedings of the 4th Vampire Workshop / L. Kovacs, A. Voronkov / in series "Vampire 2017. Proceedings of the 4th Vampire Workshop", series editor: A. Voronkov; issued by: EasyChair; EasyChair EPiC Series in Computing, EasyChair, 2018
• Reinterpreting Dependency Schemes: Soundness Meets Incompleteness in DQBF / O. Beyersdorff, J. Blinkhorn, L. Chew, R. Schmidt, M. Suda / Journal of Automated Reasoning, J Autom Reasoning (2018), 1 - 27
• CTL* with graded path modalities / B. Aminof, A. Murano, S. Rubin / Information and Computation, 262 (2018), Part 1; 1 - 21
• Graded modalities in Strategy Logic / B. Aminof, V. Malvone, A. Murano, S. Rubin / Information and Computation, 261 (2018), Part 4; 634 - 649
• Parameterized model checking of rendezvous systems / B. Aminof, T. Kotek, S. Rubin, F. Spegni, H. Veith / Distributed Computing, 31 (2018), 3; 187 - 222
• Randomized testing of distributed systems with probabilistic guarantees / B. Kulahcioglu Ozkan, R. Majumdar, F. Niksic, M. Tabaei Befrouei, G. Weissenbacher / Proceedings of the ACM on Programming Languages, 2 (2018), OOPSLA
• Efficient Translation of Sequent Calculus Proofs Into Natural Deduction Proofs / G. Ebner, M. Schlaipfer / in: "PAAR 2018 Practical Aspects of Automated Reasoning", 2162; University of Liverpool, UK, 2018, 17 - 33
• Incremental Solving with Vampire / G. Reger, M. Suda / in: "Proceedings of the 4th Vampire Workshop", 53; issued by: EasyChair; EasyChair EPiC Series in Computing, EasyChair, 2018, 12 pages
• Local proofs and AVATAR / G. Reger, M. Suda / in: "Proceedings of the 4th Vampire Workshop", 53; L. Kovacs, A. Voronkov (ed.); issued by: EasyChair; EasyChair EPiC Series in Computing, EasyChair, 2018, 9 pages

2017

• Synthesis of Distributed Algorithms with Parameterized Threshold Guards / M. Lazić, I. Konnov, J. Widder, R. Bloem / Talk: International Conference On Principles Of Distributed Systems (OPODIS), Lissabon; 2017-12-18 - 2017-12-20; in: "OPODIS", LIPIcs-Leibniz International Proceedings in Informatics, (2017), 32:1 - 32:20
• A Supervisory Control Algorithm Based on Property-Directed Reachability / K. Claessen, J. Kilhamn, L. Kovacs, B. Lennartson / Talk: 13th International Haifa Verification Conference (HVC 2017), Haifa, Israel; 2017-11-13 - 2017-11-15; in: "13th International Haifa Verification Conference (HVC)", O. Strichman, R. Tzoref-Brill (ed.); Lecture Notes in Computer Science / Springer, 10629 / Cham (2017), ISBN: 978-3-319-70388-6; 115 - 130
• Logic-Based Merging in Fragments of Classical Logic with Inputs from Social Choice Theory / A. Haret / Talk: 5th International Conference on Algorithmic Decision Theory (ADT 2017), Luxemburg; 2017-10-25 - 2017-10-27; in: "Proceedings of the 5th International Conference on Algorithmic Decision Theory (ADT 2017)", J. Rothe (ed.); Lecture Notes in Computer Science, 10576 (2017), ISBN: 978-3-319-67503-9; 374 - 378
• Automated Invention of Strategies and Term Orderings for Vampire / J. Jakubuv, M. Suda, J. Urban / Talk: GCAI 2017 / 3rd Global Conference on Artificial Intelligence, Miami, USA; 2017-10-19 - 2017-10-22; in: "GCAI 2017. 3rd Global Conference on Artificial Intelligence", EasyChair EPiC Series in Computing, Volume 50 (2017), 121 - 133
• Symbol Elimination for Program Analysis / L. Kovacs / Keynote Lecture: ETH Workshop on Software Correctness and Reliability, Zürich, Switzerland (invited); 2017-10-13 - 2017-10-14
• Interpolation-based Model Checking and IC3 / G. Weissenbacher / Keynote Lecture: Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science, Telč, Czech Republic (invited); 2017-10-13 - 2017-10-15
• Model-based, mutation-driven test case generation via heuristic-guided branching search / A. Fellner, W. Krenn, R. Schlick, T. Tarrach, G. Weissenbacher / Talk: MEMOCODE 2017: the 15th ACM-IEEE International Conference on Formal Methods and Models for System Design, Wien; 2017-09-29 - 2017-10-02; in: "Proceedings of the 15th ACM-IEEE International Conference on Formal Methods and Models for System Design, MEMOCODE 2017, Vienna, Austria, September 29 - October 02, 2017", ACM, (2017), ISBN: 978-1-4503-5093-8; 56 - 66
• Deviation in Belief Change on Fragments of Propositional Logic / A. Haret, S. Woltran / Talk: 6th Workshop on Dynamics of Knowledge and Belief (DKB-2017) and 5th Workshop KI & Kognition (KIK-2017) on Formal and Cognitive Reasoning, Dortmund; 2017-09-26; in: "Proceedings of the 6th Workshop on Dynamics of Knowledge and Belief (DKB-2017) and the 5th Workshop KI & Kognition (KIK-2017)", C. Beierle, G. Kern-Isberner, M. Ragni, F. Stolzenburg (ed.); CEUR Workshop Proceedings, 1928 (2017), ISSN: 1613-0073; Paper ID 6, 13 pages
• Automata and Program Analysis / L. Daviaud, T. Colcombet, F. Zuleger / Talk: Fundamentals of Computation Theory, Bordeaux, France (invited); 2017-09-11 - 2017-09-13; in: "Fundamentals of Computation Theory - 21st International Symposium, FCT 2017", (2017), 3 - 10
• lpopt: A Rule Optimization Tool for Answer Set Programming / M. Morak, M. Bichler, S. Woltran / Poster: 26th InternationalSymposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2016), Edinburgh, UK; 2017-09-06 - 2017-09-08; in: "Proceedings of the 26th InternationalSymposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2016)", M. Hermenegildo, P. Lopez-Garcia (ed.); Lecture Notes in Computer Science, 10184 (2017), ISBN: 978-3-319-63138-7; 114 - 130
• First-Order Interpolation and Grey Areas of Proofs / L. Kovacs / Keynote Lecture: 26th EACSL Annual Conference on Computer Science Logic (CSL), Stockholm, Sweden (invited); 2017-08-20 - 2017-08-24; in: "Proceedings of the 26th EACSL Annual Conference on Computer Science Logic (CSL)", V. Goranko, M. Dam (ed.); LIPIcs, 82 (2017), ISBN: 978-3-95977-045-3; 3:1
• Local proofs and AVATAR / G. Reger, M. Suda / Talk: Fourth Vampire Workshop - VAMPIRE 2017, Gothenburg, Sweden; 2017-08-07
• Incremental Solving with Vampire / G. Reger, M. Suda / Talk: Fourth Vampire Workshop - VAMPIRE 2017, Gothenburg, Sweden; 2017-08-07
• Splitting Proofs for Interpolation / B. Gleiss, L. Kovacs, M. Suda / Talk: CADE 26 - 26th International Conference on Automated Deduction, Gothenburg, Sweden; 2017-08-06 - 2017-08-11; in: "Automated Deduction - CADE 26 - 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings", Springer, Lecture Notes in Computer Science / 10395 (2017), ISBN: 978-3-319-63046-5; 291 - 309
• A Unifying Principle for Clause Elimination in First-Order Logic / B. Kiesl, M. Suda / Talk: CADE 26 - 26th International Conference on Automated Deduction, Gothenburg, Sweden; 2017-08-06 - 2017-08-11; in: "Automated Deduction - CADE 26 - 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings", Springer, Lecture Notes in Computer Science / 10395 (2017), ISBN: 978-3-319-63046-5; 274 - 290
• Checkable Proofs for First-Order Theorem Proving / G. Reger, M. Suda / Talk: The First International ARCADE (Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements) Workshop, Gothenburg, Sweden; 2017-08-06; in: "ARCADE 2017. 1st International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements", EasyChair EPiC Series in Computing, Volume 51 (2017), 55 - 63
• Polynomial Invariant Generation for Multi-Path Loops / A. Humenberger, M. Jaroschek, L. Kovacs / Talk: Second International Workshop on Satisfiability Checking and Symbolic Computation (SC2), Kaiserslautern, Germany; 2017-07-29
• Automated Generation of Non-Linear Loop Invariants Utilizing Hypergeometric Sequences / A. Humenberger, M. Jaroschek, L. Kovacs / Talk: International Symposium on Symbolic and Algebraic Computation (ISSAC), Kaiserslautern; 2017-07-23 - 2017-07-28; in: "ISSAC '17 Proceedings of the 2017 ACM on International Symposium on Symbolic and Algebraic Computation", ACM, (2017), ISBN: 978-1-4503-5064-8; 221 - 228
• Instantiation and Pretending to be an SMT Solver with Vampire / G. Reger, M. Suda, A. Voronkov / Talk: SMT 2017 - 15th International Workshop on Satisfiability Modulo Theories, Heidelberg, Germany; 2017-07-22 - 2017-07-23
• Testing a Saturation-Based Theorem Prover: Experiences and Challenges / G. Reger, M. Suda, A. Voronkov / Talk: TAP 2017 - 11th International Conference on Tests & Proofs, Marburg, Germany; 2017-07-19 - 2017-07-20; in: "Tests and Proofs - 11th International Conference, TAP 2017, Held as Part of STAF 2017, Marburg, Germany, July 19-20, 2017, Proceedings", Springer, 10375 / Lecture Notes in Computer Science (2017), ISBN: 978-3-319-61466-3; 152 - 161
• Constructive Satisfiability Procedure for ALCP(Z) (Preliminary Report) / N. Labai, M. Homola, M. Ortiz de la Fuente / Talk: 30th International Workshop on Description Logics, Montpellier, France; 2017-07-18 - 2017-07-21; in: "Proceedings of the 30th International Workshop on Description Logics", A. Artale, B. Glimm, R. Kontchakov (ed.); CEUR Workshop Proceedings, 1879 (2017), ISSN: 1613-0073; 1 - 13
• Algebraic Reasoning for Program Analysis / L. Kovacs / Keynote Lecture: 33rd Conference on the Mathematical Foundations of Programming Semantics (MFPS), Ljubljana, Slovenia (invited); 2017-06-12 - 2017-06-16
• Systematic Predicate Abstraction Using Variable Roles / Y. Demyanova, P. Rümmer, F. Zuleger / Talk: NASA Formal Methods (NFM), Moffett Field, CA, USA; 2017-05-16 - 2017-05-18; in: "NASA Formal Methods - 9th International Symposium, NFM 2017", (2017), 265 - 281
• Set of Support for Theory Reasoning / G. Reger, M. Suda / Talk: IWIL 2017 - 12th International Workshop on the Implementation of Logics, Maun, Botswana; 2017-05-07; in: "IWIL@LPAR 2017 Workshop and LPAR-21 Short Presentations, Maun, Botswana, May 7-12, 2017", EasyChair Kalpa Publications in Computing, 1 (2017), 124 - 134
• Blocked Clauses in First-Order Logic / B. Kiesl, M. Suda, M. Seidl, H. Tompits, A. Biere / Talk: Lpar-21: 21st International Conference On Logic For Programming, Artificial Intelligence And Reasoning, Maun, Botswana; 2017-05-07 - 2017-05-12; in: "LPAR-21. 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning", EasyChair EPiC Series in Computing, Volume 46 (2017), 31 - 48
• Recent Improvements of Theory Reasoning in Vampire / G. Reger, M. Suda, A. Voronkov / Talk: IWIL 2017 - 12th International Workshop on the Implementation of Logics, Maun, Botswana (invited); 2017-05-07
• Unified Reasoning About Robustness Properties of Symbolic-Heap Separation Logic / J. Pagel, C. Jansen, F. Zuleger, C. Matheja, T. Noll / Talk: European Symposium on Programming (ESOP), Uppsala; 2017-04-22 - 2017-04-29; in: "Programming Languages and Systems - 26th European Symposium on Programming", (2017), 611 - 638
• Measuring progress to predict success: Can a good proof strategy be evolved? / G. Reger, M. Suda / Talk: AITP 2017 - The Second Conference on Artificial Intelligence and Theorem Proving, Obergurgl (invited); 2017-03-26 - 2017-03-30
• On the Automated Verification of Web Applications with Embedded SQL / I. Shachar, T. Kotek, N. Rinetzky, M. Sagiv, O. Tamir, H. Veith, F. Zuleger / Talk: International Conference on Database Theory (ICDT), Venice, Italy; 2017-03-21 - 2017-03-24; in: "20th International Conference on Database Theory, ICDT 2017", (2017), 1 - 18
• A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms / I. Konnov, M. Lazić, H. Veith, J. Widder / Talk: 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), Paris, France; 2017-01-18 - 2017-01-20; in: "POPL", ACM, Paris (2017), ISBN: 978-1-4503-4660-3; 719 - 734
• Coming to Terms with Quantified Reasoning / L. Kovacs, S. Robillard, A. Voronkov / Talk: 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), Paris, France; 2017-01-18 - 2017-01-20; in: "Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL)", G. Castagna, A. Gordon (ed.); ACM, (2017), ISBN: 978-1-4503-4660-3; 260 - 270
• Dynamic Reductions for Model Checking Concurrent Software / H. Günther, A. Laarman, A. Sokolova, G. Weissenbacher / Talk: Verification, Model Checking, and Abstract Interpretation (VMCAI), Paris; 2017-01-15 - 2017-01-17; in: "Verification, Model Checking, and Abstract Interpretation", Springer, Lecture Notes in Computer Science 10145 (2017), 246 - 265
• FMCAD'17: Proceedings of the 17th Conference on Formal Methods in Computer-Aided Design / D. Stewart, G. Weissenbacher / FMCAD Inc., Austin, TX, 2017, ISBN: 978-0-9835678-7-5; 241 pages
• First-cycle games / B. Aminof, S. Rubin / Information and Computation, 254 (2017), 1; 195 - 216
• Complexity and Resource Bound Analysis of Imperative Programs Using Difference Constraints / M. Sinn, H. Veith, F. Zuleger / Journal of Automated Reasoning, 59 (2017), 1; 3 - 45
• On the completeness of bounded model checking for threshold-based distributed algorithms: Reachability / I. Konnov, H. Veith, J. Widder / Information and Computation, 252 (2017), 95 - 109
• Para^2: Parameterized Path Reduction, Acceleration, and SMT for Reachability in Threshold-Guarded Distributed Algorithms / I. Konnov, M. Lazić, H. Veith, J. Widder / Formal Methods in System Design (invited), 51 (2017), 2; 270 - 307
• Empirical software metrics for benchmarking of verification tools / Y. Demyanova, T. Pani, H. Veith, F. Zuleger / Formal Methods in System Design, 50 (2017), 2; 289 - 316
• Formal solutions of completely integrable Pfaffian systems with normal crossings / M. Jaroschek, M. Barkatou, S. Maddah / Journal of Symbolic Computation, 81 (2017), 41 - 68
• Replacing conjectures by positive knowledge: Inferring proven precise worst-case execution time bounds using symbolic execution / J. Knoop, L. Kovacs, J. Zwirchmayr / Journal of Symbolic Computation, 80 (2017), 101 - 124
• First-Order Interpolation and Interpolating Proof Systems / L. Kovacs, A. Voronkov / in: "LPAR-21. 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning", EasyChair EPiC Series in Computing, Volume 46, 2017, 49 - 64
• Global Subsumption Revisited (Briefly) / G. Reger, M. Suda / in: "Vampire@IJCAR 2016. Proceedings of the 3rd Vampire Workshop, Coimbra, Portugal, July 2, 2016.", 44; issued by: Laura Kovács and Andrei Voronkov; EasyChair EPiC Series in Computing, 2017, 61 - 73
• Optimizing Big-Data Queries Using Program Synthesis / M. Schlaipfer, K. Rajan, A. Lal, M. Samak / in: "Symposium on Operating Systems Principles", ACM, 2017, ISBN: 978-1-4503-5085-3, 631 - 646
• Fuzzing and Verifying RAT Refutations with Deletion Information / W. Forkel, T. Philipp, A. Rebola Pardo, E. Werner / in: "Florida Artificial Intelligence Research Society Conference", AAAI Press, 2017, 190 - 193
• Towards a Semantics of Unsatisfiability Proofs with Inprocessing / T. Philipp, A. Rebola Pardo / in: "Logic Programming and Automated Reasoning (LPAR)", EasyChair EPiC Series in Computing, 2017, 65 - 84
• CICM 2016 Doctoral Program / M. Suda / 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.", 1785; CEUR-Proceedings, 2017, 1 pages
• Preface of the Special Issue in Memoriam Helmut Veith / G. Gottlob, T. Henzinger, G. Weissenbacher / Formal Methods in System Design, 51 (2017), 2; 267 - 269

2016

• The mystery of QBF tautologies / M. Suda / Talk: Prague Automated Reasoning Seminar, Prague, Czech Republick; 2016-12-27
• With a Timisoara Background in the Scientific World of Computer Science and / L. Kovacs / Keynote Lecture: Timisoara Hungarian Science Festival, Timisoara, Romania (invited); 2016-11-26
• DRAT Proofs for XOR Reasoning / T. Philipp, A. Rebola Pardo / Talk: European Conference on Logics in Artificial Intelligence (JELIA), Cyprus; 2016-11-09 - 2016-11-11; in: "Logics in Artificial Intelligence", Springer, Lecture Notes in Computer Science/10021 (2016), 415 - 429
• Error Invariants for Concurrent Traces / A. Holzer, D. Schwartz-Narbonne, M. Tabaei Befrouei, G. Weissenbacher, T. Wies / Talk: International Symposium on Formal Methods, Cyprus; 2016-11-07 - 2016-11-11; in: "Formal Methods", Lecture Notes in Computer Science/Springer, 9995 (2016), ISBN: 978-3-319-48988-9; 370 - 387
• New Techniques in Clausal Form Generation / G. Reger, M. Suda, A. Voronkov / Talk: Prague Automated Reasoning Seminar, Prague, Czech Republick; 2016-10-31
• New Techniques in Clausal Form Generation / G. Reger, M. Suda, A. Voronkov / Talk: GCAI 2016 / 2nd Global Conference on Artificial Intelligence, Berlin, Germany; 2016-09-29 - 2016-10-02; in: "GCAI 2016. 2nd Global Conference on Artificial Intelligence", EasyChair, EPiC Series in Computing / 41 / Berlin (2016), 11 - 23
• A Clausal Normal Form Translation for FOOL / E. Kotelnikov, L. Kovacs, M. Suda, A. Voronkov / Talk: GCAI 2016 / 2nd Global Conference on Artificial Intelligence, Berlin, Germany; 2016-09-29 - 2016-10-02; in: "GCAI 2016. 2nd Global Conference on Artificial Intelligence", EasyChair, EPiC Series in Computing / 41 / Berlin (2016), 53 - 71
• AVATAR Modulo Theories / G. Reger, N. Bjorner, M. Suda, A. Voronkov / Talk: GCAI 2016 / 2nd Global Conference on Artificial Intelligence, Berlin, Germany; 2016-09-29 - 2016-10-02; in: "GCAI 2016. 2nd Global Conference on Artificial Intelligence", EasyChair, EPiC Series in Computing / 41 / Berlin (2016), 39 - 52
• lpopt: A Rule Optimization Tool for Answer Set Programming / M. Bichler, M. Morak, S. Woltran / Talk: International Symposium on Logic-Based Program Synthesis and Transformation, Edinburgh, UK; 2016-09-06 - 2016-09-08; in: "Pre-proceedings of the 26th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2016)", M. Hermenegildo, P. Lopez-Garcia (ed.); (2016), 14 pages
• Beyond IC Postulates: Classification Criteria for Merging Operators / A. Haret, A. Pfandler, S. Woltran / Talk: ECAI 2016 - 22nd European Conference on Artificial Intelligence, Den Haag, Niederlande; 2016-08-29 - 2016-09-02; in: "ECAI 2016 - 22nd European Conference on Artificial Intelligence", G. Kaminka, M. Fox, P. Bouquet, E. Hüllermeier, V. Dignum, F. Dignum, F. van Harmelen (ed.); IOS Press, 285 (2016), ISBN: 978-1-61499-671-2; 372 - 380
• Monadic Second Order Finite Satisfiability and Unbounded Tree-Width / T. Kotek, H. Veith, F. Zuleger / Talk: 25th EACSL Annual Conference on Computer Science Logic, CSL 2016, Marseille; 2016-08-29 - 2016-09-01; in: "CSL", 62 (2016), ISBN: 978-3-95977-022-4; 1 - 20
• Interpolation algorithms and their applications in model checking / G. Weissenbacher / Talk: Automata, Logic and Games, Singapore (invited); 2016-08-29 - 2016-09-02
• Parameterized Systems in BIP: Design and Model Checking / I. Konnov, T. Kotek, Q. Wang, H. Veith, S. Bliudze, J. Sifakis / Talk: International Conference on Concurrency Theory (CONCUR), Quebec City, Canada; 2016-08-23 - 2016-08-26; in: "CONCUR", Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, Vol. 59 (2016), ISBN: 978-3-95977-017-0; 30:1 - 30:16
• Desingularization of First Order Linear Difference Systems with Rational Function Coefficients / M. Barkatou, M. Jaroschek / Talk: 22nd Conference on Applications of Computer Algebra, Universität Kassel, Kassel, Deutschland; 2016-08-01 - 2016-08-04
• Desingularization of First Order Linear Difference Systems with Rational Function Coefficients / M. Jaroschek, M. Barkatou / Talk: RIMS workshop, Algebraic Statistics and Symbolic Computation, RIMS, Kyoto University, Kyoto, Japan (invited); 2016-07-25 - 2016-07-29
• Model Checking of Threshold-based Fault-Tolerant Distributed Algorithms / M. Lazić, I. Konnov, H. Veith, J. Widder / Talk: 7th Workshop on Program Semantics, Specification and Verification: Theory and Applications, St. Petersburg, Russia (invited); 2016-07-14 - 2016-07-15
• Extended Graded Modalities in Strategy Logic / B. Aminof, V. Malvone, A. Murano, S. Rubin / Talk: 4th International Workshop on Strategic Reasoning, New York; 2016-07-10; in: "SR", (2016), 1 - 14
• Distributing Knowledge Into Simple Bases / A. Haret, J. Mailly, S. Woltran / Talk: Twenty-Fifth International Joint Conference on Artificial Intelligence - IJCAI 2016, New York, NY, USA; 2016-07-09 - 2016-07-15; in: "Proceedings of the 25th International Joint Conference on Artificial Intelligence", S. Kambhampati (ed.); IJCAI/AAAI Press, (2016), ISBN: 978-1-57735-770-4; 1109 - 1115
• Finding Finite Models in Multi-sorted First-Order Logic / G. Reger, M. Suda, A. Voronkov / Talk: 19th International Conference on Theory and Applications of Satisfiability Testing, SAT 2016, Bordeaux, France; 2016-07-05 - 2016-07-08; in: "Theory and Applications of Satisfiability Testing - SAT 2016 - 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings", Springer, LNCS 9710 (2016), 323 - 341
• Lifting QBF Resolution Calculi to DQBF / O. Beyersdorff, L. Chew, R. Schmidt, M. Suda / Talk: 19th International Conference on Theory and Applications of Satisfiability Testing, SAT 2016, Bordeaux, France; 2016-07-05 - 2016-07-08; in: "Theory and Applications of Satisfiability Testing - SAT 2016 - 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings", Springer, LNCS 9710 (2016), 490 - 499
• First-Order Logic and Blocked Clauses / B. Kiesl, M. Suda / Talk: 4th International Workshop on Quantified Boolean Formulas (QBF 2016), Bordeaux, France; 2016-07-04
• Revisiting Global Subsumption / G. Reger, M. Suda / Talk: The Third Vampire Workshop, VAMPIRE 2016, Coimbra, Portugal; 2016-07-02
• Blocked clauses in first-order logic / A. Biere, B. Kiesl, M. Seidl, M. Suda / Talk: The Third Vampire Workshop, VAMPIRE 2016, Coimbra, Portugal; 2016-07-02
• Model Checking Parameterised Multi-token Systems via the Composition Method / B. Aminof, S. Rubin / Talk: IJCAR, Coimbra; 2016-06-27 - 2016-07-02; in: "IJCAR", LNCS/Springer, 8562 (2016), ISBN: 978-3-319-08587-6; 499 - 515
• Selecting the Selection / K. Hoder, G. Reger, M. Suda, A. Voronkov / Talk: IJCAR 2016, Coimbra; 2016-06-27 - 2016-07-02; in: "Automated Reasoning - 8th International Joint Conference, IJCAR 2016, Coimbra, Portugal, June 27 - July 2, 2016, Proceedings", Springer, LNCS 9706 (2016), ISBN: 978-3-319-40229-1; 313 - 329
• Automated Reasoning for Systems Engineering / L. Kovacs / Keynote Lecture: Austrian Computer Science Day 2018, Salzburg (invited); 2016-06-15
• Duality in STRIPS planning / M. Suda / Talk: 8th Workshop on Heuristics and Search for Domain-independent Planning (HSDIP), London; 2016-06-13; in: "8th Workshop on Heuristics and Search for Domain-independent Planning (HSDIP), London, UK, June 13, 2016, Proceedings", (2016), 21 - 27
• Enjoying Research at the Intersection of Math and Computer Science / L. Kovacs / Keynote Lecture: Women in Science Workshop Series (WISE), Gothenburg, Schweden (invited); 2016-06-08
• Symbolic Computation and Automated Reasoning for Program Analysis / L. Kovacs / Keynote Lecture: 12th International Conference on Integrated Formal Methods (iFM), Bertinoro, Italy (invited); 2016-06-01 - 2016-06-05; in: "Proceedings of the 12th International Conference on Integrated Formal Methods (iFM)", E. Abraham, M. Huisman (ed.); Springer / LNCS, 9681 (2016), ISBN: 978-3-319-33692-3; 20 - 27
• Quantifier Elimination Over The Reals / M. Jaroschek / Talk: Tutorial on SMT and Polynomial Arithmetic, Chalmers University, Gothenburg, Sweden (invited); 2016-05-26 - 2016-05-27
• Parameterized Verification of Liveness of Distributed Algorithms / I. Konnov, M. Lazić, H. Veith, J. Widder / Talk: Workshop on Formal Reasoning in Distributed Algorithms (FRiDA), Marrakech, Marocco; 2016-05-17
• Graded Strategy Logic: Reasoning about Uniqueness of Nash Equilibria / B. Aminof, V. Malvone, A. Murano, S. Rubin / Talk: International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS), Singapur; 2016-05-09 - 2016-05-13; in: "AAMAS", (2016), 698 - 706
• Automatic Verification of Multi-Agent Systems in Parameterised Grid-Environments / B. Aminof, A. Murano, S. Rubin, F. Zuleger / Talk: International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS), Singapur; 2016-05-09 - 2016-05-13; in: "AAMAS", (2016), 1190 - 1199
• Prompt Alternating-Time Epistemic Logics / B. Aminof, A. Murano, S. Rubin, F. Zuleger / Talk: 15th International Conference on Principles of Knowledge Representation and Reasoning (KR 2016), Kapstadt; 2016-04-25 - 2016-04-29; in: "KR", (2016), 258 - 267
• Merging of Abstract Argumentation Frameworks / J. Delobelle, A. Haret, S. Konieczny, J. Mailly, J. Rossit, S. Woltran / Talk: 15th International Conference on Principles of Knowledge Representation and Reasoning (KR 2016), Kapstadt; 2016-04-25 - 2016-04-29; in: "Principles of Knowledge Representation and Reasoning: Proceedings of the 15th International Conference", C. Baral, J. Delgrande, F. Wolter (ed.); AAAI Press, (2016), 33 - 42
• Distributing Knowledge Into Simple Bases / A. Haret, J. Mailly, S. Woltran / Talk: 16th International Workshop on Non-monotonic reasoning (NMR 2016), Kapstadt; 2016-04-22 - 2016-04-24; in: "Proceedings of the 16th International Workshop on Non-monotonic reasoning", G. Kern-Isberner, R. Wassermann (ed.); (2016), 9 pages
• First-Order Theorem Proving and Vampire / L. Kovacs / Keynote Lecture: Spring School on Logic and Verification - LoVE, Vienna, Austria (invited); 2016-04-15 - 2016-04-17
• When Should We Add Theory Axioms And Which Ones? / G. Reger, M. Suda / Talk: 1st Conference on Artificial Intelligence and Theorem Proving, AITP 2016, Obergurgl; 2016-04-03 - 2016-04-07
• The Vampire and the FOOL / E. Kotelnikov, L. Kovacs, G. Reger, A. Voronkov / Talk: 5th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP), Saint Petersburg, Florida, USA; 2016-01-20 - 2016-01-22; in: "Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP)", J. Avigad, A. Chlipala (ed.); ACM, (2016), ISBN: 978-1-4503-4127-1; 37 - 48
• Proceedings of the 1st and 2nd Vampire Workshops / L. Kovacs, A. Voronkov / in series "Proceedings of the 1st and 2nd Vampire Workshops", series editor: L. Kovacs, A. Voronkov; issued by: EasyChair; EasyChair EPiC Series in Computing, 2016
• Angry-HEX: an Artificial Player for Angry Birds Based on Declarative Knowledge Bases / G. Ianni, F. Calimeri, S. Germano, A. Humenberger, C. Redl, D. Stepanova, A. Tucci, A. Wimmer / IEEE Transactions on Computational Intelligence and AI in Games, 8 (2016), 128 - 139
• The Power of Non-Ground Rules in Answer Set Programming / M. Bichler, M. Morak, S. Woltran / Theory and Practice of Logic Programming, 16 (2016), 5-6; 552 - 569
• Decidability of Parameterized Verification / R. Bloem, S. Jacobs, A. Khalimov, I. Konnov, S. Rubin, H. Veith, J. Widder / ACM SIGACT News, 47 (2016), 2; 53 - 64
• Abstraction and mining of traces to explain concurrency bugs / M. Tabaei Befrouei, C. Wang, G. Weissenbacher / Formal Methods in System Design, 49 (2016), 1; 1 - 32
• Labelled Interpolation Systems for Hyper-Resolution, Clausal, and Local Proofs / M. Schlaipfer, G. Weissenbacher / Journal of Automated Reasoning, 57 (2016), 1; 3 - 36
• Treewidth-Preserving Modeling in ASP / M. Bichler, B. Bliem, M. Moldovan, M. Morak, S. Woltran / Report No. DBAI-TR-2016-97, 2016; 37 pages

2015

• On the Expressive Power of Communication Primitives in Parameterised Systems / B. Aminof, S. Rubin, F. Zuleger / Talk: Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), Suva, Fiji; 2015-11-24 - 2015-11-28; in: "LPAR", Springer, 9450 (2015), 313 - 328
• Difference Constraints: An adequate Abstraction for Complexity Analysis of Imperative Programs / M. Sinn, H. Veith, F. Zuleger / Talk: International Conference on Formal Methods in Computer-Aided Design (FMCAD), Austin, Texas, USA; 2015-09-27 - 2015-09-30; in: "FMCAD", (2015), 144 - 151
• Explaining Heisenbugs / G. Weissenbacher / Keynote Lecture: RV 2015, the 6th International Conference on Runtime Verification, Vienna (invited); 2015-09-22 - 2015-09-25; in: "Runtime Verification", E. Bartocci, R. Majumdar (ed.); Lecture Notes in Computer Science/Springer, 7408 (2015), ISBN: 978-3-319-23819-7; XV
• Logics of Finite Hankel Rank / N. Labai, J. A. Makowsky / Talk: Fields of Logic and Computation II, Berlin, Germany; 2015-09-11 - 2015-09-12; in: "Fields of Logic and Computation II", Springer, 9300 (2015), ISBN: 978-3-319-23533-2; 237 - 252
• What You Always Wanted to Know About Model Checking of Fault-Tolerant Distributed Algorithms / I. Konnov, H. Veith, J. Widder / Keynote Lecture: Perspectives of System Informatics: 10th International Andrei Ershov Informatics Conference, Kazan, Russland (invited); 2015-08-25 - 2015-08-27; in: "Perspectives of System Informatics: 10th International Andrei Ershov Informatics Conference, PSI 2015", LNCS / Springer, 9609 (2016), 6 - 21
• Merging in the Horn Fragment / A. Haret, St. Rümmele, S. Woltran / Talk: Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI 2015, Buenos Aires, Argentina; 2015-07-25 - 2015-07-31; in: "Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence - IJCAI 2015", Q. Yang, M. Wooldridge (ed.); AAAI Press, (2015), ISBN: 978-1-57735-738-4; 3041 - 3047
• An extension-based approach to belief revision in abstract argumentation / M. Diller, A. Haret, T. Linsbichler, St. Rümmele, S. Woltran / Talk: Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI 2015, Buenos Aires, Argentina; 2015-07-25 - 2015-07-31; in: "Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence - IJCAI 2015", Q. Yang, M. Wooldridge (ed.); AAAI Press, (2015), ISBN: 978-1-57735-738-4; 2926 - 2932
• Empirical Software Metrics for Benchmarking of Verification Tools / Y. Demyanova, T. Pani, H. Veith, F. Zuleger / Talk: International Conference on Computer Aided Verification (CAV), San Francisco, CA, USA; 2015-07-18 - 2015-07-24; in: "CAV", Springer, 9206 (2015), ISBN: 978-3-319-21667-6; 561 - 579
• SMT and POR beat Counter Abstraction: Parameterized Model Checking of Threshold-Based Distributed Algorithms / I. Konnov, H. Veith, J. Widder / Talk: International Conference on Computer Aided Verification (CAV), San Francisco, CA, USA; 2015-07-18 - 2015-07-24; in: "Computer Aided Verification", LNCS Springer, 9206 (2015), ISBN: 978-3-319-21689-8; 85 - 102
• Asymptotically Precise Ranking Functions for Deterministic Size-Change Systems / F. Zuleger / Talk: International Computer Science Symposium in Russia (CSR), Listvyanka, Russia; 2015-07-13 - 2015-07-17; in: "CSR", Springer, 9139 (2015), 426 - 442
• Extending ALCQIO with Trees / T. Kotek, M. Simkus, H. Veith, F. Zuleger / Talk: 30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2015), Kyoto, Japan; 2015-07-06 - 2015-07-10; in: "LICS 2015", IEEE, (2015), ISBN: 978-1-4799-8875-4; 511 - 522
• Liveness of Parameterized Timed Networks / B. Aminof, S. Rubin, F. Spegni, F. Zuleger / Talk: International Colloquium on Automata, Languages and Programming (ICALP), Kyoto, Japan; 2015-07-06 - 2015-07-10; in: "ICALP", Springer, 9135 (2015), 375 - 387
• Proving Safety with Trace Automata and Bounded Model Checking / M. Lewis, D. Kroening, G. Weissenbacher / Talk: International Symposium on Formal Methods, Oslo, Norway; 2015-06-22 - 2015-06-25; in: "Formal Methods", Lecture Notes in Computer Science/Springer, 9109 (2015), ISBN: 978-3-319-19248-2; 325 - 341
• Verification of Asynchronous Mobile-Robots in Partially-Known Environments / B. Aminof, A. Murano, S. Rubin, F. Zuleger / Talk: Principles and Practice of Multi-Agent Systems, Graz; 2015-05-18 - 2015-05-19; in: "PRIMA", Springer, 9387 (2015), 185 - 200
• Perspectives on White-Box Testing: Coverage, Concurrency, and Concolic Execution / A. Farzan, A. Holzer, H. Veith / Keynote Lecture: International Conference on Software Testing, Verification and Validation (ICST), Graz; 2015-04-14 - 2015-04-16; in: "ICST", (2015), 1 - 11
• LTSmin: High-Performance Language-Independent Model Checking / S. Blom, T. van Dijk, K. Gijis, A. Laarman, J. Meijer, J. van de Pol / Talk: Tools and Algorithms for the Construction and Analysis of Systems, London, UK; 2015-04-13 - 2015-04-17; in: "TACAS", Springer Berlin Heidelberg, 9035 (2015), ISBN: 978-3-662-46680-3; 692 - 707
• Compilation for Secure Two-Party Computations / M. Franz, A. Holzer, S. Katzenbeisser, C. Schallhart, H. Veith / Talk: Software Engineering & Management 2015, Dresden; 2015-03-17 - 2015-03-20; in: "Software Engineering & Management 2015", GI-Edition - Lecture Notes in Informatics (LNI), 239 (2015), 143 - 145
• Abstraction and mining of traces to explain concurrency bugs / M. Tabaei Befrouei / Talk: Frontiers of Formal Methods, Aachen; 2015-02-25 - 2015-02-27; in: "Proceedings of the Young Researchers' Conference "Frontiers of Formal Methods"", T. Ströder, W. Thomas (ed.); (2015), 5 pages
• Decidability of Parameterized Verification / R. Bloem, S. Jacobs, A. Khalimov, I. Konnov, S. Rubin, H. Veith, J. Widder / Morgan & Claypool Publishers, San Rafael, CA, USA, 2015, ISBN: 9781627057431; 170 pages
• Under-approximating loops in C programs for fast counterexample detection / M. Lewis, D. Kroening, G. Weissenbacher / Formal Methods in System Design, 47 (2015), 1; 75 - 92
• Boolean Satisfiability Solvers and Their Applications in Model Checking / Y. Vizel, G. Weissenbacher, S. Malik / Proceedings of the IEEE (invited), 103 (2015), 11; 2021 - 2035
• Loop Patterns in C Programs / T. Pani, H. Veith, F. Zuleger / ECEASST, 72 (2015)
• Efficient computation of generalized Ising polynomials on graphs with fixed clique-width / T. Kotek, J. A. Makowsky / Topics in Theoretical Computer Science (TTCS), 9541 (2015), 135 - 146
• Bipartition polynomials, the Ising model and domination in graphs / M. Dod, T. Kotek, J. Preen, P. Tittmann / Discussiones Mathematicae Graph Theory, 35 (2015), 2; 335 - 353
• Closure properties and complexity of rational sets of regular languages / A. Holzer, C. Schallhart, M. Tautschnig, H. Veith / Theoretical Computer Science, 605 (2015), 62 - 79
• Time Complexity of Link Reversal Routing / B. Charron-Bost, M Függer, L. Welch, J. Widder / ACM Transactions on Algorithms, 11 (2015), 3; 1 - 39

2014

• Reduction of Resolution Refutations and Interpolants via Subsumption / R. Bloem, S. Malik, M. Schlaipfer, G. Weissenbacher / Talk: Haifa Verification Conference (HVC), Haifa, Isral; 2014-11-18 - 2014-11-20; in: "Haifa Verification Conference (HVC)", Springer / LNCS, 8855 (2014), ISBN: 978-3-319-13337-9; 188 - 203
• Partial-Order Reduction for Multi-core LTL Model Checking / A. Laarman, A. Wijs / Talk: Haifa Verification Conference (HVC), Haifa, Isral; 2014-11-18 - 2014-11-20; in: "Haifa Verification Conference (HVC)", Springer / LNCS, 8855 (2014), ISBN: 978-3-319-13337-9; 267 - 283
• Feedback generation for performance problems in introductory programming assignments / S. Gulwani, I. Radicek, F. Zuleger / Talk: ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE), Hong Kong, China; 2014-11-16 - 2014-11-22; in: "FSE", ACM New York, NY, USA, (2014), ISBN: 978-1-4503-3056-5; 41 - 51
• Silicon fault diagnosis using sequence interpolation with backbones / C. Zhu, G. Weissenbacher, S. Malik / Talk: The IEEE/ACM International Conference on Computer-Aided Design (ICCAD), San Jose, CA, USA; 2014-11-03 - 2014-11-06; in: "ICCAD", IEEE Press Piscataway, NJ, USA, (2014), ISBN: 978-1-4799-6277-8; 348 - 355
• Model Checking of Fault-Tolerant Distributed Algorithms / H. Veith / Talk: Summer School 2014: Verification Technology, Systems & Applications, Luxembourg (invited); 2014-10-27 - 2014-10-31
• Approaching Verification and Validation Challenges in Smart Grids / T. Deutsch, J. Widder / Talk: Symposium Communications for Energy Systems, Wien; 2014-09-29 - 2014-10-01; in: "Tagungsband ComForEn 2014", Eigenverlag des Österreich isch en Verbandes für Elektrotec h nik, (2014), ISBN: 978-3-85133-083-0; 6 pages
• Abstraction and Mining of Traces to Explain Concurrency Bugs / M. Tabaei Befrouei, C. Wang, G. Weissenbacher / Talk: nternational Conference on Runtime Verification, Toronto, Kanada; 2014-09-22 - 2014-09-25; in: "Runtime Verification", Springer / LNCS, 8734 (2014), ISBN: 978-3-319-11163-6; 162 - 177
• History of Model Checking / H. Veith / Keynote Lecture: Clarke Symposium 2014: Celebrating 25 Years of Model Checking, Pittsburgh, PA, USA (invited); 2014-09-19 - 2014-09-20
• An Open Alternative for SMT-Based Verification of Scade Models / H. Basold, H. Günther, M. Huhn, S. Milius / Poster: International Conference on Formal Methods for Industrial Critical Systems (FMICS), Florenz, Italien; 2014-09-11 - 2014-09-12; in: "FMICS", Springer / LNCS, 8718 (2014), ISBN: 978-3-319-10701-1; 124 - 139
• Shape and Content - A Database-Theoretic Perspective on the Analysis of Data Structures / D. Calvanese, T. Kotek, M. Simkus, H. Veith, F. Zuleger / Keynote Lecture: International Conference in Integrated Formal Methods (IFM), Bertinoro, Italy (invited); 2014-09-09 - 2014-09-11; in: "IFM", Springer / LNCS, 8739 (2014), ISBN: 978-3-319-10180-4; 3 - 17
• First Cycle Games / S. Rubin / Talk: Highlights of Logic, Games and Automata, Paris, Frankreich; 2014-09-03 - 2014-09-05
• On the Completeness of Bounded Model Checking for Threshold-Based Distributed Algorithms: Reachability / I. Konnov, H. Veith, J. Widder / Talk: International Conference on Concurrency Theory (CONCUR), Rom, Italien; 2014-09-02 - 2014-09-05; in: "CONCUR", (2014), 125 - 140
• Parameterized Model Checking of Rendezvous Systems / B. Aminof, T. Kotek, S. Rubin, F. Spegni, H. Veith / Talk: International Conference on Concurrency Theory (CONCUR), Rom, Italien; 2014-09-02 - 2014-09-05; in: "CONCUR", Springer / LNCS, 8704 (2014), 109 - 124
• Size-Change Abstraction and Max-Plus Automata / T. Colcombet, L. Daviaud, F. Zuleger / Talk: International Symposium on Mathematical Foundations of Computer Science (MFCS), Budapest, Ungarn; 2014-08-25 - 2014-08-29; in: "MFCS", Springer / LNCS, 8634 (2014), ISBN: 978-3-662-44521-1; 208 - 219
• On the Complexity of Symbolic Verification and Decision Problems in Bit-Vector Logic / G. Kovasznai, H. Veith, A. Fröhlich, A. Biere / Talk: International Symposium on Mathematical Foundations of Computer Science (MFCS), Budapest, Ungarn; 2014-08-25 - 2014-08-29; in: "MFCS", Springer / LNCS, 8635 (2014), 481 - 492
• Solvability-Based Comparison of Failure Detectors / S. Sastry, J. Widder / Talk: International Symposium on Network Computing and Applications (NCA), Boston, MA, USA; 2014-08-21 - 2014-08-23; in: "NCA", IEEE Computer Society, (2014), ISBN: 978-1-4799-5392-9; 269 - 276
• AngryHEX: An Angry Birds-playing Agent based on HEX-Programs / F. Calimeri, M. Fink, S. Germano, A. Humenberger, G. Ianni, C. Redl, D. Stepanova, A. Tucci / Poster: AngryBirds Competition 2014, Prague, Czech Republic; 2014-08-20 - 2014-08-22
• Parameterised Verification of Robot Protocols: An Automata Theoretic Approach / S. Rubin / Talk: Workshop on Formal Reasoning in Distributed Algorithms (FRiDA), Wien; 2014-07-23 - 2014-07-24
• Incremental bounded software model checking / H. Günther, G. Weissenbacher / Talk: International SPIN Symposium on Model Checking of Software (SPIN), San Jose, CA, USA; 2014-07-21 - 2014-07-23; in: "SPIN", ACM New York, NY, USA, (2014), ISBN: 978-1-4503-2452-6; 40 - 47
• Counterexample to Induction-Guided Abstraction-Refinement (CTIGAR) / J. Birgmeier, A. Bradley, G. Weissenbacher / Talk: International Conference on Computer Aided Verification (CAV), Wien; 2014-07-18 - 2014-07-22; in: "CAV", Springer / LNCS, 8559 (2014), ISBN: 978-3-319-08866-2; 829 - 846
• A Simple and Scalable Static Analysis for Bound Analysis and Amortized Complexity Analysis / M. Sinn, F. Zuleger, H. Veith / Talk: International Conference on Computer Aided Verification (CAV), Wien; 2014-07-18 - 2014-07-22; in: "CAV", Springer / LNCS, 8559 (2014), ISBN: 978-3-319-08866-2; 745 - 761
• Parameterized Model Checking of Rendezvous Systems / B. Aminof, T. Kotek, S. Rubin, F. Spegni, H. Veith / Talk: Algorithmics of Infinite State Systems workshop, Wien; 2014-07-18
• Towards a Description Logic for Program Analysis: Extending ALCQIO with Reachability / T. Kotek, M. Simkus, H. Veith, F. Zuleger / Keynote Lecture: International Workshop on Description Logics, Wien; 2014-07-17 - 2014-07-20; in: "International Workshop on Description Logics", (2014), 4 pages
• Shape and Content: Incorporating Domain Knowledge into Shape Analysis / D. Calvanese, T. Kotek, M. Simkus, H. Veith, F. Zuleger / Talk: International Workshop on Description Logics, Wien; 2014-07-17 - 2014-07-20; in: "International Workshop on Description Logics", (2014), 4 pages
• Concolic Testing of Concurrent Programs / A. Farzan, A. Holzer, N. Razavi, H. Veith / Talk: International Workshop on Exploiting Concurrency Efficiently and Correctly (EC2), Wien; 2014-07-17 - 2014-07-18
• On the Complexity of Symbolic Verification and Decision Problems in Bit-Vector Logic / A. Fröhlich, G. Kovasznai, A. Biere, H. Veith / Talk: International Workshop on Pragmatics of SAT (POS), Wien; 2014-07-13; in: "POS", (2014), 14 pages
• Explaining the decompositionality of monadic second order logic using applications to combinatorics / T. Kotek / Talk: Fun With Formal Methods Workshop, Wien; 2014-07-13
• On the Complexity of Symbolic Verification and Decision Problems in Bit-Vector Logic / G. Kovasznai, H. Veith, A. Fröhlich, A. Biere / Talk: 15th International Workshop on Logic and Computational Complexity and Workshop in Honor of Neil Immerman's 60th Birthday (LCC 2014/ImmermanFest), Wien; 2014-07-12 - 2014-07-13
• Vienna Summer of Logic / M. Baaz, T. Eiter, H. Veith / Talk: Vienna Summer of Logic, Wien, Austria (invited); 2014-07-09 - 2014-07-24
• First Cycle Games / B. Aminof, S. Rubin / Talk: International Workshop on Strategic Reasoning (SR), Grenoble, Frankreich; 2014-04-05 - 2014-04-06; in: "SR", EPTCS, 146 (2014), 83 - 90
• CBMC-GC: An ANSI C Compiler for Secure Two-Party Computations / M. Franz, A. Holzer, S. Katzenbeisser, C. Schallhart, H. Veith / Talk: International Conference on Compiler Construction, Grenoble, France; 2014-04-05 - 2014-04-13; in: "Compiler Construction", Springer / LNCS, 8409 (2014), ISBN: 978-3-642-54806-2; 244 - 249
• Reusing Information in Multi-Goal Reachability Analyses / D. Beyer, A. Holzer, M. Tautschnig, H. Veith / Talk: Fachtagung des GI-Fachbereichs Softwaretechnik, Kiel, Deutschland; 2014-02-25 - 2014-02-28; in: "Software Engineering 2014", LNI, 227 (2014), ISBN: 978-388579-621-3; 97 - 98
• Concolic Testing of Concurrent Programs / A. Farzan, A. Holzer, N. Razavi, H. Veith / Talk: Fachtagung des GI-Fachbereichs Softwaretechnik, Kiel, Deutschland; 2014-02-25 - 2014-02-28; in: "Software Engineering 2014", LNI, 227 (2014), ISBN: 978-388579-621-3; 101 - 102
• A Logic-Based Framework for Verifying Consensus Algorithms / C. Dragoi, T. Henzinger, H. Veith, J. Widder, D. Zufferey / Talk: Verification, Model Checking, and Abstract Interpretation (VMCAI), San Diego; 2014-02-19 - 2014-02-21; in: "VMCAI", Springer / LNCS, 8318 (2014), ISBN: 978-3-642-54012-7; 161 - 181
• Parameterized Model Checking of Token-Passing Systems / B. Aminof, S. Jacobs, A. Khalimov, S. Rubin / Talk: Verification, Model Checking, and Abstract Interpretation (VMCAI), San Diego; 2014-02-19; in: "VMCAI", Springer / LNCS, 8318 (2014), 262 - 281
• Tutorial on Parameterized Model Checking of Fault-Tolerant Distributed Algorithms / A. Gmeiner, I. Konnov, U. Schmid, H. Veith, J. Widder / in: "Formal Methods for Executable Software Models", Springer, 2014, (invited), ISBN: 978-3-319-07316-3, 122 - 171
• A representation theorem for (q-)holonomic sequences / T. Kotek, J. A. Makowsky / Journal of Computer and System Sciences, 80 (2014), 2; 363 - 374
• Recurrence relations for graph polynomials on bi-iterative families of graphs / T. Kotek, J. A. Makowsky / European Journal of Combinatorics, 41 (2014), 47 - 67
• Connection Matrices and the Definability of Graph Parameters / T. Kotek, J. A. Makowsky / Logical Methods in Computer Science, 10 (2014), 4; 1 - 33

2013

• On the Structure and Complexity of Rational Sets of Regular Languages / A. Holzer, C. Schallhart, M. Tautschnig, H. Veith / Talk: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS), Guwahati, Indien; 2013-12-12 - 2013-12-14; in: "FSTTCS", Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, (2013), ISBN: 978-3-939897-64-4; 377 - 388
• The first workshop on language support for privacy-enhancing technologies (PETShop'13) / M. Franz, A. Holzer, R. Majumdar, B. Parno, H. Veith / Talk: ACM Conference on Computer and Communications Security (CCS), Berlin, Deutschland (invited); 2013-11-04 - 2013-11-08; in: "CCS", ACM, (2013), ISBN: 978-1-4503-2477-9; 1485 - 1486
• Challenges in Compiler Construction for Secure Two-Party Computation / A. Holzer, N. Karvelas, S. Katzenbeisser, H. Veith / Talk: Workshop on language support for privacy-enhancing technologies (PETShop), Berlin, Deutschland; 2013-11-04; in: "PETShop", ACM, (2013), ISBN: 978-1-4503-2489-2; 3 - 6
• On the concept of variable roles and its use in software analysis / Y. Demyanova, H. Veith, F. Zuleger / Talk: International Conference on Formal Methods in Computer-Aided Design (FMCAD), Portland, OR, USA; 2013-10-20 - 2013-10-23; in: "FMCAD", IEEE, (2013), ISBN: 978-0-9835678-3-7; 226 - 230
• Parameterized model checking of fault-tolerant distributed algorithms by abstraction / A. John, I. Konnov, U. Schmid, H. Veith, J. Widder / Talk: International Conference on Formal Methods in Computer-Aided Design (FMCAD), Portland, OR, USA; 2013-10-20 - 2013-10-23; in: "FMCAD", (2013), ISBN: 978-0-9835678-3-7; 201 - 209
• Advanced SAT Techniques for Abstract Argumentation / J. P. Wallner, G. Weissenbacher, S. Woltran / Talk: International Workshop on Computational Logic in Multi-Agent Systems (CLIMA), Corunna, Spanien; 2013-09-16 - 2013-09-18; in: "CLIMA", Springer / LNCS, 8143 (2013), ISBN: 978-3-642-40623-2; 138 - 154
• Con2colic testing / A. Farzan, A. Holzer, N. Razavi, H. Veith / Talk: Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE), Sankt Petersburg, Russland; 2013-08-18 - 2013-08-26; in: "Esec/sigsoft Fse", ACM, (2013), ISBN: 978-1-4503-2237-9; 37 - 47
• Brief announcement: parameterized model checking of fault-tolerant distributed algorithms by abstraction / A. John, I. Konnov, U. Schmid, H. Veith, J. Widder / Talk: ACM SIGACT-SIGOPS Symposium on Principles of Distributed Computing (PODC), Montreal, Kanada; 2013-07-22 - 2013-07-24; in: "PODC", ACM, (2013), ISBN: 978-1-4503-2065-8; 119 - 121
• Under-Approximating Loops in C Programs for Fast Counterexample Detection / D. Kroening, M. Lewis, G. Weissenbacher / Talk: International Conference on Computer Aided Verification (CAV), Sankt Petersburg, Russland; 2013-07-13 - 2013-07-19; in: "CAV", Springer / LNCS, 8044 (2013), ISBN: 978-3-642-39798-1; 381 - 396
• Mining Sequential Patterns to Explain Concurrent Counterexamples / S. Leue, M. Tabaei Befrouei / Talk: International SPIN Symposium on Model Checking of Software (SPIN), Stony Brook, NY, USA; 2013-07-08 - 2013-07-09; in: "SPIN", LNCS, Springer, 7976 (2013), ISBN: 978-3-642-39175-0; 264 - 281
• Towards Modeling and Model Checking Fault-Tolerant Distributed Algorithms / A. John, I. Konnov, U. Schmid, H. Veith, J. Widder / Talk: International SPIN Symposium on Model Checking of Software (SPIN), Stony Brook, NY, USA; 2013-07-08 - 2013-07-09; in: "SPIN", LNCS, Springer, 7976 (2013), ISBN: 978-3-642-39175-0; 209 - 226
• Solving Constraints for Generational Search / D. Pötzl, A. Holzer / Talk: International Conference on Tests and Proofs (TAP), Budapest, Ungarn; 2013-06-16 - 2013-06-20; in: "TAP", Springer / LNCS, 7942 (2013), ISBN: 978-3-642-38915-3; 197 - 213
• Ramsey vs. Lexicographic Termination Proving / B. Cook, A. See, F. Zuleger / Talk: Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Rom, Italien; 2013-04-05 - 2013-04-13; in: "Tools and Algorithms for the Construction and Analysis of Systems", Lecture Notes in Computer Science. Springer Verlag., 7795 (2013), ISBN: 978-3-642-36741-0; 47 - 61
• Information Reuse for Multi-goal Reachability Analyses / D. Beyer, A. Holzer, M. Tautschnig, H. Veith / Talk: European Symposium on Programming (ESOP), Rom, Italien; 2013-03-16 - 2013-03-24; in: "ESOP", Springer / LNCS, 7792 (2013), ISBN: 978-3-642-37035-9; 472 - 491
• CAV / N. Sharygina, H. Veith / in series "Lecture Notes in Computer Science (LNCS 8044)", series editor: Springer Verlag; Springer, 2013, ISBN: 978-3-642-39798-1, 1015 pages
• Formal Verification of Distributed Algorithms (Dagstuhl Seminar 13141) / B. Charron-Bost, A. Rybalchenko, S. Merz, J. Widder / in series "Dagstuhl Reports", series editor: Schloss Dagstuhl; issued by: Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik; Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany, Dagstuhl, Deutschland, 2013, ISSN: 2192-5283, 16 pages
• Verification across Intellectual Property Boundaries / S. Chaki, C. Schallhart, H. Veith / ACM Transactions on Software Engineering and Methodology, 22 (2013), 2; Article 15
• Link Reversal Routing with Binary Link Labels: Work Complexity / B. Charron-Bost, A. Gaillard, L. Welch, J. Widder / SIAM JOURNAL ON COMPUTING, 42 (2013), 2; 634 - 661

2012

• Wait-Free Stabilizing Dining Using Regular Registers / S. Sastry, L. Welch, J. Widder / Talk: International Conference On Principles Of Distributed Systems (OPODIS), Rom; 2012-12-17 - 2012-12-20; in: "OPODIS", LNCS / Springer, 7702 (2012), ISBN: 978-3-642-35475-5; 284 - 299
• Vinter: A Vampire-Based Tool for Interpolation / K. Hoder, A. Holzer, L. Kovacs, A. Voronkov / Talk: Asian Symposium on Programming Languages and Systems (APLAS), Kyoto, Japan; 2012-12-11 - 2012-12-13; in: "APLAS", Springer / LNCS, 7705 (2012), ISBN: 978-3-642-35181-5; 148 - 156
• Secure Two-Party Computation in ANSI C / H. Veith / Talk: Dagstuhl Seminar 12461: Games and Decisions for Rigorous Systems Engineering, Dagstuhl, Deutschland (invited); 2012-11-11 - 2012-11-16
• Parameterized Model Checking of Fault-tolerant Distributed Algorithms / A. John, I. Konnov, U. Schmid, H. Veith, J. Widder / Talk: Dagstuhl Seminar 12461: Games and Decisions for Rigorous Systems Engineering, Dagstuhl, Deutschland (invited); 2012-11-11 - 2012-11-16
• Labelled Interpolation Systems / G. Weissenbacher / Talk: Dagstuhl Seminar 12461: Games and Decisions for Rigorous Systems Engineering, Dagstuhl, Deutschland (invited); 2012-11-11 - 2012-11-16
• Coverage-based Trace Signal Selection for Fault Localisation in Post-Silicon Validation / Z. Charlie Shucheng, G. Weissenbacher, S. Malik / Talk: Haifa Verification Conference (HVC), Haifa, Isral; 2012-11-06 - 2012-11-08; in: "Haifa Verification Conference (HVC)", Lecture Notes in Computer Science. Springer Verlag., 7857 (2012), ISBN: 978-3-642-39610-6; 132 - 147
• Secure two-party computations in ANSI C / A. Holzer, M. Franz, S. Katzenbeisser, H. Veith / Talk: ACM Conference on Computer and Communications Security (CCS), Raleigh, NC, USA; 2012-10-16 - 2012-10-18; in: "ACM Conference on Computer and Communications Security", ACM, New York, NY, USA (2012), ISBN: 978-1-4503-1651-4; 772 - 783
• Bounded-Interference Sequentialization for Testing Concurrent Programs / N. Razavi, A. Farzan, A. Holzer / Talk: International Symposium on Leveraging Applications of Formal Methods (ISoLA), Heraklion, Kreta, Griechenland; 2012-10-15 - 2012-10-18; in: "Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change", Lecture Notes in Computer Science. Springer Verlag., 7609 (2012), ISBN: 978-3-642-34025-3; 372 - 387
• Parallel Assertions for Architectures with Weak Memory Models / D. Schwartz-Narbonne, G. Weissenbacher, S. Malik / Talk: Automated Technology for Verification and Analysis (ATVA), Thiruvananthapuram, India; 2012-10-03 - 2012-10-06; in: "Automated Technology for Verification and Analysis", Lecture Notes in Computer Science. Springer Verlag., 7561 (2012), ISBN: 978-3-642-33385-9; 254 - 268
• Who is afraid of Model Checking Distributed Algorithms? / A. John, I. Konnov, U. Schmid, H. Veith, J. Widder / Talk: PUMA/RISE Seminar, Goldegg; 2012-09-24 - 2012-09-28
• Efficient Checking of Link-Reversal-Based Concurrent Systems / M Függer, J. Widder / Talk: International Conference on Concurrency Theory (CONCUR), Newcaslte upon Tyne, UK; 2012-09-03 - 2012-09-08; in: "CONCUR 2012 - Concurrency Theory", Lecture Notes in Computer Science. Springer Verlag., 7454 (2012), ISBN: 978-3-642-32939-5; 486 - 499
• Who is afraid of Model Checking Distributed Algorithms? / I. Konnov, H. Veith, J. Widder / Talk: Workshop on Exploiting Concurrency Efficiently and Correctly, Berkeley, CA, USA; 2012-07-07 - 2012-07-08
• Interpretations in Trees with Countably Many Branches / A. Rabinovic, S. Rubin / Talk: Symposium on Logic in Computer Science (LICS), Dubrovnik, Kroatien; 2012-06-25 - 2012-06-28; in: "Logic in Computer Science", IEEE, (2012), ISBN: 978-1-4673-2263-8; 551 - 560
• Interpolant Strength Revisited / G. Weissenbacher / Talk: International Conference on Theory and Applications of Satisfiability Testing (SAT), Trient, Italien; 2012-06-17 - 2012-06-20; in: "International Conference on Theory and Applications of Satisfiability Testing (SAT)", LNCS / Springer, 7317 (2012), 312 - 326
• Counter Attack against Byzantine Generals / A. John, I. Konnov, U. Schmid, H. Veith, J. Widder / Talk: Alpine Verification Meeting, Passau, Bayern, Deutschland; 2012-05-21 - 2012-05-22
• Proving Reachability Using FShell / A. Holzer, D. Kroening, C. Schallhart, M. Tautschnig, H. Veith / Talk: Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Tallinn, Estland; 2012-03-24 - 2012-04-01; in: "Proc. of 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)", Springer, LNCS 7214 (2012), ISBN: 978-3-642-28755-8; 538 - 541
• Selected Papers of the Conference "Computer Science Logic CSL 2010": Preface / A. Dawar, H. Veith / Logical Methods in Computer Science, (2012)
• Special Issue: Games in Verification (foreword) / H. Veith / Journal of Computer and System Sciences, 78 (2012), 2; 393
• Consensus in the presence of mortal Byzantine faulty processes / J. Widder, M. Biely, G. Gridling, B. Weiss, J. Blanquart / Distributed Computing, 24 (2012), 6; 299 - 321
• A Myhill-Nerode theorem for automata with advice / A. Kruckman, S. Rubin, J. Sheridan, B. Zax / in: "Symposium on Games, Automata, Logics and Formal Verification", M. Faella, A. Murano (ed.); Electronic Proceedings in Theoretical Computer Science, 2012, 238 - 246

2011

• Bound Analysis of Imperative Programs with the Size-change Abstraction / F. Zuleger / Talk: Microsoft Research Lecture, Microsoft Research Cambridge, UK (invited); 2011-12-01
• Bound Analysis of Imperative Programs with the Size-change Abstraction / F. Zuleger / Talk: Theory Seminar, Queen Mary University, UK (invited); 2011-11-30
• Bound Analysis of Imperative Programs with the Size-change Abstraction / F. Zuleger / Talk: Austrian Society for Rigorous Systems Engineering (ARiSE) workshop together with PUMA workshop, Traunkirchen, Austria; 2011-10-03 - 2011-10-07
• On Efficient Checking of Link-reversal-based Concurrent Systems / M Függer, J. Widder / Talk: PUMA/RISE Seminar, Traunkirchen; 2011-10-03 - 2011-10-07
• Bound Analysis of Imperative Programs with the Size-change Abstraction / F. Zuleger, M. Sinn, S. Gulwani, H. Veith / Talk: International Static Analysis Symposium, Venice, Italy; 2011-09-14 - 2011-09-16; in: "Lecture Notes in Computer Science", E. Yahav (ed.); Springer, 6887 (2011), ISBN: 978-3-642-23701-0; 280 - 297
• Bound Analysis of Imperative Programs with the Size-change Abstraction / F. Zuleger / Talk: Software Systems Group Seminar, NICTA, Australien; 2011-07-19
• Resource Bound Analysis of Imperative Programs / F. Zuleger / Talk: RiSE Seminar, Klosterneuburg; 2011-05-05
• Improving the Confidence in Measurement-Based Timing Analysis / S. Bünte, M. Zolda, M. Tautschnig, R. Kirner / Talk: 14th IEEE International Symposium on Object/Component/Service-Oriented Real-Time Distributed Computing (ISORC 2011), Newport Beach, California, USA; 2011-03-28 - 2011-03-31; in: "2011 14th IEEE International Symposium on Object/Component/Service-Oriented Real-Time Distributed Computing (ISORC 2011)", IEEE, (2011), ISBN: 978-1-61284-433-6; 144 - 151
• Seamless testing for models and code / A. Holzer, V. Januzaj, St. Kugele, B. Langer, C. Schallhart, M. Tautschnig, H. Veith / Talk: ETAPS, Saarbrücken, Deutschland; 2011-03-26 - 2011-04-03; in: "Lecture Notes in Computer Science", G. Goos, J. Hartmanis, J. van Leeuwen (ed.); Springer, 6603 (2011), ISBN: 978-3-642-19810-6; 278 - 293
• Termination and Bound Analysis of Imperative Programs / F. Zuleger / Talk: Workshop on Logic and Computer Science, Vienna; 2011-03-24 - 2011-03-25
• How did you specify your test suite? / H. Veith / Talk: Alpine Verification Meeting, IST Austria; 2011-03-14
• Malware Detection / S. Katzenbeisser, J. Kinder, H. Veith / in: "Encyclopedia of Cryptography and Security", H. van Tilborg, S. Jajodia (ed.); Springer-Verlag, 2011, ISBN: 978-1-4419-5905-8, 752 - 755
• Decision Procedures in Soft, Hard and Bio-ware - Follow Up (Dagstuhl Seminar 11272) / N. Bjorner, R. Nieuwenhuis, H. Veith, A. Voronkov / Dagstuhl Reports, 1 (2011), 7; 23 - 35

2010

• Seamless Model-driven Development put into Practice / W. Haberl, M. Herrmannsdoerfer, St. Kugele, M. Tautschnig, M. Wechs / Talk: 4th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2010), Heraklion, Griechenland; 2010-10-18 - 2010-10-20; in: "Proceedings of 4th International Symposium on Leveraging Applications", T. Margaria, B. Steffen (ed.); Lecture Notes in Computer Science, 6415 (2010), 18 - 32
• Timely Time Estimates / A. Holzer, V. Januzaj, St. Kugele, M. Tautschnig / Talk: 4th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2010), Heraklion, Griechenland; 2010-10-18 - 2010-10-20; in: "Proceedings of 4th International Symposium on Leveraging Applications (ISoLA 2010)", T. Margaria, B. Steffen (ed.); Lecture Notes in Computer Science, 6415 (2010), ISBN: 978-3-642-16557-3; 33 - 46
• An Introduction to Test Specification in FQL / A. Holzer, C. Schallhart, M. Tautschnig, H. Veith / Talk: Haifa Verification Conference, Haifa, Israel; 2010-10-05 - 2010-10-07; in: "Lecture Notes in Computer Science", S. Barner, J.G. Harris, D. Kroening, O. Raz (ed.); Springer, 6504 (2010), ISSN: 0302-9743; 9 - 22
• How did you specify your test suite? / A. Holzer, C. Schallhart, M. Tautschnig, H. Veith / Talk: The 25th IEEE/ACM International Conference on Automated Software Engineering (ASE 2010), Antwerpen, Belgien; 2010-09-20 - 2010-09-24; in: "Proceedings of the 25th IEEE/ACM International Conference on Automated Software Engineering (ASE 2010)", Ch. Pecheur, J. Andrews, E. Di Nitto (ed.); ACM, (2010), ISBN: 978-1-4503-0116-9; 407 - 416
• The reachability-bound problem / S. Gulwani, F. Zuleger / Talk: Conference on Programming Language Design and Implementation (PLDI), Toronto, Canada; 2010-06-05 - 2010-06-10; in: "PLDI'10 Proceedings of teh ACM SIGPLAN conference on Programming language design and implementation", B. G. Zorn, A. Aiken (ed.); PLDI'10 Proceedings of teh ACM SIGPLAN conference on Programming language design and implementation, (2010), ISBN: 978-1-4503-0019-3; 292 - 304
• Proactive Detection of Computer Worms Using Model Checking / J. Kinder, S. Katzenbeisser, C. Schallhart, H. Veith / IEEE Transactions on Dependable and Secure Computing, 7 (2010), 4; 424 - 438
• Semantic Integrity in Large-Scale Online Simulations / S. Jha, S. Katzenbeisser, C. Schallhart, H. Veith, St. Chenney / ACM Transactions on Internet Technology, 10 (2010), 1
• On the distributivity of LTL specifications / M. Samer, H. Veith / ACM Transactions on Computational Logic, 11 (2010), 3
• Don't care in SMT---Building flexible yet efficient abstraction/refinement solvers / A. Bauer, M. Leucker, C. Schallhart, M. Tautschnig / International Journal on Software Tools for Technology Transfer, 12 (2010), 1; 23 - 37

2007

• Towards a Systematic Design of Fault-Tolerant Asynchronous Circuits / U. Schmid, A. Steininger, H. Veith / Poster: GMM/GI/ITG-Fachtagung Zuverlässigkeit und Entwurf, München; 2007-03-26 - 2007-03-28; in: "Fachtagung Zuverlässigkeit und Entwurf", VDE Verlag, (2007), ISBN: 978-3-8007-3023-0; 173 - 174

2006

• From Temporal Logic Queries to Vacuity Detection / M. Samer, H. Veith / in: "Verification of Infinite-State Systems with Applications to Security", E. Clarke et al. (ed.); issued by: NATO Security through Science Series D: Information and Communication Security; IOS Press, 2006, (invited), ISBN: 1-58603-570-3, 149 - 167

2005

• Deterministic CTL Query Solving / M. Samer, H. Veith / Talk: International Symposium on Temporal Representation and Reasoning (TIME), Burlington, Vermont, USA; 2005-06-23 - 2005-06-25; in: "Proceedings of the 12th International Symposium on Temporal Representation and Reasoning", J. Chomicki, D. Toman (ed.); IEEE Computer Society, (2005), ISBN: 0-7695-2370-6; 156 - 165

2004

• Parameterized Vacuity / M. Samer, H. Veith / Talk: International Conference on Formal Methods in Computer-Aided Design (FMCAD), Austin, Texas, USA; 2004-11-14 - 2004-11-17; in: "Proceedings of the 5th International Conference on Formal Methods in Computer-Aided Design", A. Hu, A. Martin (ed.); Springer-Verlag Berlin Heidelberg, Lecture Notes in Computer Science Vol. 3312 (2004), ISBN: 3-540-23738-0; 322 - 336
• A Syntactic Characterization of Distributive LTL Queries / M. Samer, H. Veith / Talk: International Colloquium on Automata, Languages and Programming (ICALP), Turku, Finnland; 2004-07-12 - 2004-07-16; in: "Proceedings of the 31st International Colloquium on Automata, Languages and Programming", J. Diaz et al. (ed.); Springer-Verlag Berlin Heidelberg, Lecture Notes in Computer Science Vol. 3142 (2004), ISBN: 3-540-22849-7; 1099 - 1110
• Counterexamples Revisited: Principles, Algorithms, Applications / E. Clarke, H. Veith / in: "Verification: Theory and Practice: Essays Dedicated to Zohar Manna on the Occasion of his 64th Birthday", Springer, LNCS, Heidelberg, 2004, ISBN: 3-540-21002-4, 208 - 224

2003

• Watermarking schemes provably secure against copy and ambiguity attacks / A. Adelsbach, S. Katzenbeisser, H. Veith / Poster: ACM Workshop On Digital Rights Management, Washington, DC, USA; 2003-10-27; in: "Porceedings of the 2003 ACM workshop on Digital rights management", ACM Press, New York, NY, USA (2003), ISBN: 1-58113-786-9; 111 - 119
• Validity of CTL Queries Revisited / M. Samer, H. Veith / Talk: Annual Conference of the European Association for Computer Science Logic (CSL), Wien, Österreich; 2003-08-25 - 2003-08-30; in: "Proceedings of the 12th Annual Conference of the European Association for Computer Science Logic", M. Baaz, J. A. Makowsky (ed.); Springer-Verlag Berlin Heidelberg, Lecture Notes in Computer Science Vol. 2803 (2003), ISBN: 3-540-40801-0; 470 - 483
• Friends or Foes? Communities in Software Verification / H. Veith / Talk: Computer Science Logic (CSL´3), Wien, Österreich (invited); 2003-08-25 - 2003-08-30; in: "Lecture Notes in Computer Science", Spronger-Verlag Heidelberg, Volume 2803 / 2003 (2003), ISBN: 3-540-40801-0; 528 - 529
• Integrating Publish/Subscribe into a Mobile Teamwork Support Platform / Sagar, P. Fenkam, H. Veith, H. Gall, E. Kirda, S. Jha / Talk: International Conference on Software Engineering and Knowledge Engineering (SEKE), USA, San Francisco Bay; 2003-07-01 - 2003-07-03; in: "Proceedings of the 15th International Conference on Software Engineering and Knowledge Engineering", (2003), ISBN: 1-891706-12-8; 510 - 517
• SAT Based Predicate Abstraction for Hardware Verification / E. Clarke, M. Talupur, H. Veith, D. Wang / Talk: SAT 2003, Satisfiably Testing: 6 Internationall Conference, Santa Margherita, Ligurien, Italien (invited); 2003-05-05 - 2003-05-08; in: "Lecture Notes in Computer Science", Springer-Verlag Heidelberg, Volume 2919 / 2004 (2004), ISBN: 3-540-20851-8; 78 - 92
• Counterexample-Guided Abstraction Refinement for Symbolic Model Checking / E. Clarke, O. Grumberg, S. Jha, Y. Lu, H. Veith / Journal of the ACM, Volume 50 (2003), Issue 5; 752 - 794
• Modular Verification of Software Components in C* / S. Chaki, E. Clarke, A. Groce, S. Jha, H. Veith / in: "Proceedings of the 25th Conference on Software Engineering ", issued by: 25thConference on Software Engineering; IEEE, 2003, ISBN: 0-7695-1877-x, 385 - 395

2002

• Verfahren zur Komplexitätsreduktion im Model Checking / H. Veith / Talk: Technische Universität München, München, Deutschland; 2002-11-27 - 2002-11-28
• Automated Abstraction Refinement for Model Checking Large State Spaces using SAT based Conflict Analysis / P. Chauhan, E. Clarke, J. Kukula, S. Sapra, H. Veith, D. Wang / Talk: Fourth International Conference on Formal Methods in Computer-Aided Design (FMCAD2002), Portland, Oregon, USA (invited); 2002-11-06 - 2002-11-08; in: "Proceedings of the 4th International Conference on Formal Methods in Computer-Aided Design", M. Aagaard, J. O´Leary (ed.); Springer/LNCS, 2517 (2002), ISBN: 3-540-00116-6; 33 - 51
• Tree-Like Counterexamples in Model Cheking / E. Clarke, S. Jha, Y. Lu, H. Veith / Talk: 17th Annual IEEE Symposium on Logic in Computer Science (LIC'S02), Copenhagen, Denmark; 2002-07-22 - 2002-07-25; in: "Proceedings of the Seventeenth Annual IEEE Symposium on Logic in Computer Science (LICS' 2002)", (2002), ISBN: 0-7695-1483-9; 19 - 29
• Verfahren zur Komplexitätsreduktion im Model Checking / H. Veith / Talk: Technische Universität Graz, Graz, Österreich; 2002-05-06
• Model Checking - Recent Results and Developments / H. Veith / Talk: University of Leeds, Leeds, United Kingdom; 2002-03-09 - 2002-03-13
• Securing Symmetric Watermarking Schemes Against Protocol Attacks / S. Katzenbeisser, H. Veith / Talk: Conference Security and Watermarking of Multimedia Contents IV, San Jose, California, USA; 2002-01-21 - 2002-01-24; in: "Proceedings of SPIE 2002", E. Delp, P. Wong (ed.); Vol. 4675 (2002), ISBN: 0-8194-4415-4; 260 - 268
• Verfahren zur Komplexitätsreduktion im Model Checking / H. Veith / Talk: Universität Saarbrücken, Saarbrücken, Deutschland (invited); 2002-01-02
• On the complexity of Data Disjunctions / T. Eiter, H. Veith / Theoretical Computer Science, 288 (2002), 101 - 128
• Datalog LITE: a deductive query language with linear time model checking / G. Gottlob, E. Grädel, H. Veith / ACM Transactions on Computational Logic, Volume 3 (2002), 1; 42 - 79

Note: Due to the rollout of TU Wien’s new publication database, the list below may be slightly outdated. Once APIs for the new database have been released, everything will be up to date again.

2021

• Automating inductive reasoning with recursive functions / Master Thesis by M. Hajdu / Supervisor: L. Kovacs; Institut for Logic and Computation, E192.04, FORSYTE division, 2021; final examination: 2021-03-25
• Algebra-based loop reasoning - invariant generation and synthesis for numeric loops / Doctoral Thesis by A. Humenberger / Supervisor, Reviewer: E. Abraham, J. Worrell; Institute of Logic and Computation, FORSYTE division, 2021; oral examination: 2021-02-08
• Static Analysis of Low-Level Code / Doctoral Thesis by I. Grishchenko / Supervisor, Reviewer: M. Maffei, G. Weissenbacher, A. Sabelfeld, K. Bhargavan; Institut of Logic and Computation, Security and Privacy, 2021; oral examination: 2021-01-25
• Automated induction by reflection / Master Thesis by J. Schoisswohl / Supervisor: L. Kovacs; Institut for Logic and Computation, E192.04, FORSYTE division, 2021; final examination: 2021-01-11

2020

• Automated Software Verification using Superposition-based Theorem Proving / Doctoral Thesis by B. Gleiss / Supervisor, Reviewer: L. Kovacs, S. Schulz; Institut for Logic and Computation, E192.04, 2020; oral examination: 2020-12-07
• Automated Reasoning over Arrays in the Superposition Calculus / Master Thesis by C. Hochrainer / Supervisor: L. Kovacs; Institut for Logic and Computation, E192.04, 2020; final examination: 2020-07-21
• Automating Termination Analysis of Probabilistic Programs / Master Thesis by M. Moosbrugger / Supervisor: L. Kovacs; Institut for Logic and Computation, E192.04, 2020; final examination: 2020-06-23
• First-Order Reasoning with Aggregates / Master Thesis by S. Rain / Supervisor: L. Kovacs; Institut for Logic and Computation, E192.04, 2020; final examination: 2020-06-18
• Formalizing Graph Trail Properties / Master Thesis by H. Lachnitt / Supervisor: L. Kovacs; Institut for Logic and Computation, E192.04, 2020; final examination: 2020-06-04
• SpecBMC : bounded model checker for speculative non-interference / Master Thesis by E. Pescosta / Supervisor: G. Weissenbacher, F. Zuleger; Logic and Computation, 2020
• Verifying automotive software components using C model checkers / Master Thesis by T. Durand / Supervisor: G. Weissenbacher, W. Steiner; Logic and Computation, 2020

2019

• Abstraction for Reasoning about Agent Behavior with Answer Set Programming / Doctoral Thesis by Z. G. Saribatur / Supervisor, Reviewer: T. Eiter, G. Weissenbacher; Institut für Logic and Computation, 2019; oral examination: 2019-12-17
• Trace Reasoning in Formal Verification - Guiding Vampire in Induction / Master Thesis by P. Georgiou / Supervisor: L. Kovacs; Institut for Logic and Computation, E192.04, 2019; final examination: 2019-11-22
• Subsumption Demodulation in First-Order Theorem Proving / Master Thesis by J. Rath / Supervisor: L. Kovacs; Institut for Logic and Computation, E192.04, 2019; final examination: 2019-10-07

2016

• Effective Error Explanation Techniques for Concurrent Software / Doctoral Thesis by M. Tabaei Befrouei / Supervisor, Reviewer: G. Weissenbacher, T. Eiter, R. Majumdar; Informationssysteme, 2016; oral examination: 2016-12-06
• Logical Methods in Automated Hardware and Software Verification / Habilitation Thesis by G. Weissenbacher / TU Wien/Fakultät für Informatik, 2016
• Automated Complexity Analysis for Imperative Programs / Doctoral Thesis by M. Sinn / Supervisor, Reviewer: F. Zuleger, T. Vojnar; Institut für Informationssysteme, 2016

2014

• Merging in the Horn fragment / Master Thesis by A. Haret / Supervisor: S. Woltran, St. Rümmele; Institut für Informationssysteme, 2014; final examination: 2014-09-23
• Complexity Results and Algorithms for Argumentation - Dung's Frameworks and Beyond / Doctoral Thesis by J. P. Wallner / Supervisor, Reviewer: S. Woltran, G. Weissenbacher; Institute of Information Systems, 2014; oral examination: 2014-05-28

2013

• Query-Based Test Case Generation / Doctoral Thesis by A. Holzer / Supervisor, Reviewer: H. Veith, D. Beyer; Fakultät für Informatik der Technischen Universität Wien, 2013
• Loop Patterns in C Programs / Master Thesis by T. Pani / Supervisor: F. Zuleger, H. Veith; Fakultät für Informatik der Technischen Universität Wien, 2013
• Software Verification with IC3 via Abstraction and Interpolation / Master Thesis by J. Birgmeier / Supervisor: G. Weissenbacher, H. Veith; Fakultät für Informatik der Technischen Universität Wien, 2013

2011

• Resource bound analysis of imperative programs / Doctoral Thesis by F. Zuleger / Supervisor, Reviewer: H. Veith, S. Gulwani; Institut für Informationssysteme, 2011; oral examination: 2011-05-11
• Query-Driven Program Testing / Doctoral Thesis by M. Tautschnig / Supervisor, Reviewer: H. Veith, D. Kroening; Institut für Informationssysteme, 2011; oral examination: 2011-04-11

2007

• Architecture and Security in Networked Virtual Environments / Doctoral Thesis by C. Schallhart / Supervisor, Reviewer: G. Gottlob, H. Veith; Institut für Informationssysteme, Arbeitsbereich Datenbanken & Artificial Intelligence, 2007; oral examination: 2007-06-12

2004

• Reasoning about Specifications in Model Checking / Doctoral Thesis by M. Samer / Supervisor, Reviewer: H. Veith, G. Gottlob; Institut für Informationssysteme, 2004
• Cryptographic Watermarking / Doctoral Thesis by S. Katzenbeisser / Supervisor, Reviewer: H. Veith, G. Gottlob; Institut für Informationssysteme, ARGR Datenbanken & Artificial Intelligence, 2004

2003

• Symbolic Model Checking using NUSMV / Master Thesis by A. Plaickner / Supervisor: H. Veith; Institut für Informationssysteme, 2003
• Symbolic Model Checking using NUSMV / Master Thesis by A. Plaickner / Supervisor: H. Veith; Institut für Informationssysteme, 2003

2002

• Temporal Logic Queries in Model Checking / Master Thesis by M. Samer / Supervisor: H. Veith; Institut für Informationssysteme, 2002

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

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

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