TU Wien Informatics

About

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

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

Formal Methods in Systems Engineering is part of the faculty’s Institute of Logic and Computation.

Laura Kovacs
Laura Kovacs L. Kovacs

Head of Research Unit
Univ.Prof. Dr. /MSc

Georg Weissenbacher
Georg Weissenbacher G. Weissenbacher

Associate Professor
Assoc.Prof. DI /PhD

Florian Zuleger
Florian Zuleger F. Zuleger

Associate Professor
Assoc.Prof. Dipl.-Math. Dr.

Bernhard Gleiss
Bernhard Gleiss B. Gleiss

PreDoc Researcher
DI /BSc

Andreas Humenberger
Andreas Humenberger A. Humenberger

PreDoc Researcher
DI /BSc

Jens Katelaan
Jens Katelaan J. Katelaan

PreDoc Researcher
MSc

Jure Kukovec
Jure Kukovec J. Kukovec

PreDoc Researcher
Mag.

Timo Achim Lang
Timo Achim Lang T. Lang

PreDoc Researcher
MSc

Vedran Marinkovic
Vedran Marinkovic V. Marinkovic

PreDoc Researcher
DI /BSc

Thomas Pani
Thomas Pani T. Pani

PreDoc Researcher
DI /BSc

Anna Prianichnikova
Anna Prianichnikova A. Prianichnikova

PostDoc Researcher
Mag. Dr.

Matthias Schlaipfer
Matthias Schlaipfer M. Schlaipfer

PreDoc Researcher
DI /BSc

Thanh Hai Tran
Thanh Hai Tran T. Tran

PreDoc Researcher
DI /BSc

Beatrix Buhl
Beatrix Buhl B. Buhl

Administration

Pamina Georgiou
Pamina Georgiou P. Georgiou

Project Administration
BSc

Mihaela Rozman
Mihaela Rozman M. Rozman

Project Administration
MA

2018W

2019S

 

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

2014

2013

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

2007

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

 

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