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.

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

Pavol Cerny
Pavol Cerny P. Cerny

Full Professor
Univ.Prof. / PhD

Laura Kovacs
Laura Kovacs L. Kovacs

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

Georg Weissenbacher
Georg Weissenbacher G. Weissenbacher

Full Professor
Univ.Prof. DI / PhD

Florian Zuleger
Florian Zuleger F. Zuleger

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

Benjamin Aminof
Benjamin Aminof B. Aminof

PostDoc Researcher
PhD

Pamina Georgiou
Pamina Georgiou P. Georgiou

PreDoc Researcher
DI / BSc

Marton Hajdu
Marton Hajdu M. Hajdu

PreDoc Researcher
DI / BSc

Petra Hozzova
Petra Hozzova P. Hozzova

PreDoc Researcher
Mag.

George James Kenison
George James Kenison G. Kenison

PostDoc Researcher
PhD

Jure Kukovec
Jure Kukovec J. Kukovec

PreDoc Researcher
Mag.

Vedran Marinkovic
Vedran Marinkovic V. Marinkovic

PreDoc Researcher
DI / BSc

Marcel Moosbrugger
Marcel Moosbrugger M. Moosbrugger

PreDoc Researcher
DI / BSc BA (Hons)

Thomas Pani
Thomas Pani T. Pani

PreDoc Researcher
DI / BSc

Anna Prianichnikova
Anna Prianichnikova A. Prianichnikova

PostDoc Researcher
Mag. Dr.

Sophie Rain
Sophie Rain S. Rain

PreDoc Researcher
DI / BSc

Jakob Rath
Jakob Rath J. Rath

PreDoc Researcher
DI / BSc

Thanh Hai Tran
Thanh Hai Tran T. Tran

PreDoc Researcher
DI / BSc

Friedrich Weber
Friedrich Weber F. Weber

PreDoc Researcher
MSc

2020

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

2019

2018

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

2017

2016

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

2015

2014

2013

2012

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

2011

2010

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

2007

2006

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

2005

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

2004

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

2003

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

2002

 

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

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

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