2019W

• Bachelor Thesis / PR / 184.695
• Doctoral & Master Students Seminar / SE / 181.224
• Formal Methods in Computer Science / UE / 185.A93
• Formal Methods in Computer Science / VU / 185.291
• Introduction to Logical Methods in Computer Science / VO / 184.766
• Orientation Bachelor with Honors of Informatics and Business Informatics / SE / 180.767
• Program Analysis / VU / 184.703
• Project in computational logic / PR / 181.222
• Project in Computer Science 1 / PR / 184.692
• Project in Computer Science 2 / PR / 184.693
• Project in Software Engineering & Internet Computing / PR / 184.697
• Research Seminar LogiCS / SE / 184.767
• Seminar for Master Students in Logic and Computation / SE / 180.773
• Seminar Formal Methods / SE / 181.221
• Theoretical Computer Science and Logics / VU / 185.278

2020S

• Automated Deduction / VU / 184.774

• Algorithms think differently
  2019 – 2022 / Federal Ministry of Transport, Innovation and Technology (bm:vit)
• Symbol Elimination in Reliable System Engineering
  2019 – 2020 / European Commission
• Formal methods for Realistic Environments in MAS
  2019 – 2022 / Austrian Science Fund (FWF)
• Domain-Specific Reasoning in IoT Applications
  2019 – 2020 / Osztrák-Magyar Akció Alapítvány Stiftung Aktion Österreich-Ungarn
• Holonomic Sequences in Program Verification
  2018 – 2021 / Austrian Science Fund (FWF)
• LogiCs-Scholarships
  2017 – 2021 / LCS
• Bit-level Accurate Reasoning and Interpolation
  2016 – 2020 / Microsoft Research Limited
• Symbolic Computation and Automated Reasoning for Program Analysis
  2016 – 2021 / European Commission
• Tools for Concurrent and distributed Systems
  2011 – 2019 / Austrian Science Fund (FWF)

2019

• Removing apparent singularities of linear difference systems / M. Barkatou, M. Jaroschek / accepted for publication in Journal of Symbolic Computation (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
• 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

2018

• 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
• 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
• 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
• 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
• 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
• 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
• 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
• 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
• 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
• 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
• 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
• 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
• 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
• 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
• 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
• 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
• 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
• 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
• A Separation Logic with Data: Small Models and Automation / J. Katelaan, 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
• 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
• 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
• 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
• 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

2017

• 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
• 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
• 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
• 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
• 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
• 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
• 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
• 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
• 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
• 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
• 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
• Unified Reasoning About Robustness Properties of Symbolic-Heap Separation Logic / J. Katelaan, 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
• 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
• 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
• 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
• 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
• 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
• 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
• 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
• 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
• 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

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

2015

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

2014

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

2013

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

2012

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

2011

• 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

2010

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

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

2004

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

2003

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

2002

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

• Abstraction for Reasoning about Agent Behavior with Answer Set Programming / PhD 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
• 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 / PhD Thesis by M. Sinn / Supervisor, Reviewer: F. Zuleger, T. Vojnar; Institut für Informationssysteme, 2016
• Effective Error Explanation Techniques for Concurrent Software / PhD Thesis by M. Tabaei Befrouei / Supervisor, Reviewer: G. Weissenbacher, T. Eiter, R. Majumdar; Informationssysteme, 2016; oral examination: 2016-12-06
• Complexity Results and Algorithms for Argumentation - Dung's Frameworks and Beyond / PhD Thesis by J. P. Wallner / Supervisor, Reviewer: S. Woltran, G. Weissenbacher; Institute of Information Systems, 2014; oral examination: 2014-05-28
• 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
• Query-Based Test Case Generation / PhD 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
• Resource bound analysis of imperative programs / PhD Thesis by F. Zuleger / Supervisor, Reviewer: H. Veith, S. Gulwani; Institut für Informationssysteme, 2011; oral examination: 2011-05-11
• Query-Driven Program Testing / PhD Thesis by M. Tautschnig / Supervisor, Reviewer: H. Veith, D. Kroening; Institut für Informationssysteme, 2011; oral examination: 2011-04-11
• Architecture and Security in Networked Virtual Environments / PhD Thesis by C. Schallhart / Supervisor, Reviewer: G. Gottlob, H. Veith; Institut für Informationssysteme, Arbeitsbereich Datenbanken & Artificial Intelligence, 2007; oral examination: 2007-06-12
• Reasoning about Specifications in Model Checking / PhD Thesis by M. Samer / Supervisor, Reviewer: H. Veith, G. Gottlob; Institut für Informationssysteme, 2004
• Cryptographic Watermarking / PhD Thesis by S. Katzenbeisser / Supervisor, Reviewer: H. Veith, G. Gottlob; Institut für Informationssysteme, ARGR Datenbanken & Artificial Intelligence, 2004
• 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
• 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 / Best Paper Award / Italy / 2015

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 .