Formal Methods in Systems Engineering E192-04

A Research Unit of The Institute of Logic and Computation

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.

Research Unit Formal Methods in Systems Engineering

Contact

About

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

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

Professors

Scientific Staff

Administrative Staff

Student Staff

Courses

2021W

Formal Methods in Computer Science / 185.A93 / UE
Formal Methods in Computer Science / 185.291 / VU
Project in Computer Science 1 / 184.692 / PR
Project in Computer Science 2 / 184.693 / PR

Projects

Automated Reasoning with Theories and Induction for Software Technologies
2021 – 2026 / European Commission
FOREST: First-Order Reasoning for Ensuring System Security
2021 – 2022 / Amazon Research Awards
Distribution Recovery for Invariant Generation of Probabilistic Programs
2020 – 2024 / Vienna Science and Technology Fund (WWFT)
AutoTest
2020 – 2021 / Vienna Science and Technology Fund (WWFT)
Algorithms think differently
2019 – 2022 / Federal Ministry of Transport, Innovation and Technology (bm:vit)
Formal methods for Realistic Environments in MAS
2019 – 2022 / Austrian Science Fund (FWF)
Symbol Elimination in Reliable System Engineering
2019 – 2020 / European Commission
Domain-Specific Reasoning in IoT Applications
2019 – 2020 / DoS-IoT
Holonomic Sequences in Program Verification
2018 – 2021 / Austrian Science Fund (FWF)
LogiCs-Scholarships
2017 – 2025 / LCS
Symbolic Computation and Automated Reasoning for Program Analysis
2016 – 2021 / European Commission
Bit-level Accurate Reasoning and Interpolation
2016 – 2020 / Microsoft Research Limited
Tools for Concurrent and distributed Systems
2011 – 2019 / Austrian Science Fund (FWF)

Publications

2021

The Probabilistic Termination Tool Amber / M. Moosbrugger, E. Bartocci, J. Katoen, L. Kovacs / accepted as talk for: FM 2021: the 24th international symposium of Formal Methods, China; 2021-11-20 - 2021-11-25; in: "Proc. of FM 2021: the 24th international symposium of Formal Methods", (2021)
Automated Termination Analysis of Polynomial Probabilistic Programs / M. Moosbrugger, E. Bartocci, J. Katoen, L. Kovacs / Talk: 30th European Symposium on Programming (ESOP 2021), Luxembourg (online); 2021-03-27 - 2021-04-01; in: "Proc. of ESOP 2021: the 30th European Symposium on Programming", Springer, 12648 (2021), 491 - 518

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

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

2018

Symbol Elimination in Program Analysis / L. Kovacs / Keynote Lecture: 2nd Facebook Testing and Veri cation Symposium (FaceTAV), London, UK (invited); 2018-11-28 - 2018-11-29
Loop Analysis by Quantification over Iterations / B. Gleiss, L. Kovacs, S. Robillard / Talk: 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), Awassa, Ethiopia; 2018-11-16 - 2018-11-21; in: "Proceedings of the 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR)", G. Barthe, G. Sutcliffe, M. Veanes (ed.); EasyChair EPiC Series in Computing, 57 (2018), 381 - 399
Towards Smarter MACE-style Model Finders / M. Janota, M. Suda / Talk: 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), Awassa, Ethiopia; 2018-11-16 - 2018-11-21; in: "LPAR-22. 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Awassa, Ethiopia, 16-21 November 2018.", EasyChair EPiC Series in Computing, 57 (2018), 454 - 470
A Theory of Satisfiability-Preserving Proofs in SAT Solving / A. Rebola Pardo, M. Suda / Talk: International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), Awassa, Ethiopia; 2018-11-16 - 2018-11-21; in: "International Conference on Logic for Programming, Artificial Intelligence and Reasoning", EasyChair EPiC Series in Computing, 57 / Lpar-22 (2018), 583 - 603
ByMC: Byzantine Model Checker / I. Konnov, J. Widder / Talk: International Symposium on Leveraging Applications of Formal Methods (ISoLA), Limasol, Zypern; 2018-11-05 - 2018-11-09; in: "ISOLA", Lecture Notes in Computer Science. Springer Verlag., 11246 (2018), ISBN: 978-3-642-34025-3; 327 - 342
Synthesis under Assumptions / B. Aminof, G. De Giacomo, A. Murano, S. Rubin / Poster: Principles of Knowledge Representation and Reasoning (KR), Tempe, Arizona; 2018-10-30 - 2018-11-02; in: "Principles of Knowledge Representation and Reasoning: Proceedings of the Sixteenth International Conference, KR 2018, Tempe, Arizona, 30 October - 2 November 2018", AAAI Press, (2018), ISBN: 978-1-57735-803-9; 615 - 616
Rely-Guarantee Reasoning for Automated Bound Analysis of Lock-Free Algorithms / T. Pani, G. Weissenbacher, F. Zuleger / Talk: International Conference on Formal Methods in Computer-Aided Design (FMCAD), Austin, TX; 2018-10-30 - 2018-11-02; in: "Formal Methods in Computer-Aided Design", FMCAD Inc., (2018), ISBN: 978-0-9835678-8-2; 1 - 9
Using Loop Bound Analysis For Invariant Generation / P. Čadek, C. Danninger, M. Sinn, F. Zuleger / Talk: International Conference on Formal Methods in Computer-Aided Design (FMCAD), Austin, TX; 2018-10-30 - 2018-11-02; in: "Formal Methods in Computer-Aided Design", FMCAD Inc., (2018), ISBN: 978-0-9835678-8-2; 1 - 9
Symbol Elimination for Program Analysis / L. Kovacs / Keynote Lecture: Highlights of Logic, Games and Automata, Berlin, Germany (invited); 2018-09-18 - 2018-09-21
Reachability in Parameterized Systems: All Flavors of Threshold Automata / J. Kukovec, I. Konnov, J. Widder / Talk: International Conference on Concurrency Theory (CONCUR), Bejing, China; 2018-09-04 - 2018-09-07; in: "29th International Conference on Concurrency Theory (CONCUR 2018)", Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH, Dagstuhl Publishing, 118 (2018), ISBN: 978-3-95977-087-3; 19:1 - 19:17
Inductive Termination Proofs with Transition Invariants and Their Relationship to the Size-Change Abstraction / F. Zuleger / Talk: International Static Analysis Symposium (SAS), Freiburg, Germany; 2018-08-29 - 2018-08-31; in: "Static Analysis - 25th International Symposium, SAS 2018, Freiburg, Germany, August 29-31, 2018, Proceedings", Springer, Lecture Notes in Computer Science (2018), ISBN: 978-3-319-99724-7; 423 - 444
First-Order Interpolation in the Grey Area of Proofs / L. Kovacs / Keynote Lecture: Summer School on Syntax meets Semantics - Methods, Interactions, and Connections in Substructural Logics (SYSMICS), Les Diablerets, Switzerland (invited); 2018-08-22 - 2018-08-26
Extended Resolution Simulates DRAT / B. Kiesl, A. Rebola Pardo, M. Heule / Keynote Lecture: 9th International Joint Conference on Automated Reasoning (IJCAR) 2018, Oxford; 2018-08-14 - 2018-08-17; in: "Proceedings of the 9th International Joint Conference on Automated Reasoning (IJCAR) 2018", LNCS, 10900 (2018), ISBN: 978-3-319-94204-9; 516 - 531
A Separation Logic with Data: Small Models and Automation / J. 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

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

2016

The mystery of QBF tautologies / M. Suda / Talk: Prague Automated Reasoning Seminar, Prague, Czech Republick; 2016-12-27
With a Timisoara Background in the Scientific World of Computer Science and / L. Kovacs / Keynote Lecture: Timisoara Hungarian Science Festival, Timisoara, Romania (invited); 2016-11-26
DRAT Proofs for XOR Reasoning / T. Philipp, A. Rebola Pardo / Talk: European Conference on Logics in Artificial Intelligence (JELIA), Cyprus; 2016-11-09 - 2016-11-11; in: "Logics in Artificial Intelligence", Springer, Lecture Notes in Computer Science/10021 (2016), 415 - 429
Error Invariants for Concurrent Traces / A. Holzer, D. Schwartz-Narbonne, M. Tabaei Befrouei, G. Weissenbacher, T. Wies / Talk: International Symposium on Formal Methods, Cyprus; 2016-11-07 - 2016-11-11; in: "Formal Methods", Lecture Notes in Computer Science/Springer, 9995 (2016), ISBN: 978-3-319-48988-9; 370 - 387
New Techniques in Clausal Form Generation / G. Reger, M. Suda, A. Voronkov / Talk: Prague Automated Reasoning Seminar, Prague, Czech Republick; 2016-10-31
New Techniques in Clausal Form Generation / G. Reger, M. Suda, A. Voronkov / Talk: GCAI 2016 / 2nd Global Conference on Artificial Intelligence, Berlin, Germany; 2016-09-29 - 2016-10-02; in: "GCAI 2016. 2nd Global Conference on Artificial Intelligence", EasyChair, EPiC Series in Computing / 41 / Berlin (2016), 11 - 23
A Clausal Normal Form Translation for FOOL / E. Kotelnikov, L. Kovacs, M. Suda, A. Voronkov / Talk: GCAI 2016 / 2nd Global Conference on Artificial Intelligence, Berlin, Germany; 2016-09-29 - 2016-10-02; in: "GCAI 2016. 2nd Global Conference on Artificial Intelligence", EasyChair, EPiC Series in Computing / 41 / Berlin (2016), 53 - 71
AVATAR Modulo Theories / G. Reger, N. Bjorner, M. Suda, A. Voronkov / Talk: GCAI 2016 / 2nd Global Conference on Artificial Intelligence, Berlin, Germany; 2016-09-29 - 2016-10-02; in: "GCAI 2016. 2nd Global Conference on Artificial Intelligence", EasyChair, EPiC Series in Computing / 41 / Berlin (2016), 39 - 52
lpopt: A Rule Optimization Tool for Answer Set Programming / M. Bichler, M. Morak, S. Woltran / Talk: International Symposium on Logic-Based Program Synthesis and Transformation, Edinburgh, UK; 2016-09-06 - 2016-09-08; in: "Pre-proceedings of the 26th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2016)", M. Hermenegildo, P. Lopez-Garcia (ed.); (2016), 14 pages
Beyond IC Postulates: Classification Criteria for Merging Operators / A. Haret, A. Pfandler, S. Woltran / Talk: ECAI 2016 - 22nd European Conference on Artificial Intelligence, Den Haag, Niederlande; 2016-08-29 - 2016-09-02; in: "ECAI 2016 - 22nd European Conference on Artificial Intelligence", G. Kaminka, M. Fox, P. Bouquet, E. Hüllermeier, V. Dignum, F. Dignum, F. van Harmelen (ed.); IOS Press, 285 (2016), ISBN: 978-1-61499-671-2; 372 - 380
Monadic Second Order Finite Satisfiability and Unbounded Tree-Width / T. Kotek, H. Veith, F. Zuleger / Talk: 25th EACSL Annual Conference on Computer Science Logic, CSL 2016, Marseille; 2016-08-29 - 2016-09-01; in: "CSL", 62 (2016), ISBN: 978-3-95977-022-4; 1 - 20
Interpolation algorithms and their applications in model checking / G. Weissenbacher / Talk: Automata, Logic and Games, Singapore (invited); 2016-08-29 - 2016-09-02
Parameterized Systems in BIP: Design and Model Checking / I. Konnov, T. Kotek, Q. Wang, H. Veith, S. Bliudze, J. Sifakis / Talk: International Conference on Concurrency Theory (CONCUR), Quebec City, Canada; 2016-08-23 - 2016-08-26; in: "CONCUR", Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, Vol. 59 (2016), ISBN: 978-3-95977-017-0; 30:1 - 30:16
Desingularization of First Order Linear Difference Systems with Rational Function Coefficients / M. Barkatou, M. Jaroschek / Talk: 22nd Conference on Applications of Computer Algebra, Universität Kassel, Kassel, Deutschland; 2016-08-01 - 2016-08-04
Desingularization of First Order Linear Difference Systems with Rational Function Coefficients / M. Jaroschek, M. Barkatou / Talk: RIMS workshop, Algebraic Statistics and Symbolic Computation, RIMS, Kyoto University, Kyoto, Japan (invited); 2016-07-25 - 2016-07-29
Model Checking of Threshold-based Fault-Tolerant Distributed Algorithms / M. Lazić, I. Konnov, H. Veith, J. Widder / Talk: 7th Workshop on Program Semantics, Specification and Verification: Theory and Applications, St. Petersburg, Russia (invited); 2016-07-14 - 2016-07-15
Extended Graded Modalities in Strategy Logic / B. Aminof, V. Malvone, A. Murano, S. Rubin / Talk: 4th International Workshop on Strategic Reasoning, New York; 2016-07-10; in: "SR", (2016), 1 - 14
Distributing Knowledge Into Simple Bases / A. Haret, J. Mailly, S. Woltran / Talk: Twenty-Fifth International Joint Conference on Artificial Intelligence - IJCAI 2016, New York, NY, USA; 2016-07-09 - 2016-07-15; in: "Proceedings of the 25th International Joint Conference on Artificial Intelligence", S. Kambhampati (ed.); IJCAI/AAAI Press, (2016), ISBN: 978-1-57735-770-4; 1109 - 1115
Finding Finite Models in Multi-sorted First-Order Logic / G. Reger, M. Suda, A. Voronkov / Talk: 19th International Conference on Theory and Applications of Satisfiability Testing, SAT 2016, Bordeaux, France; 2016-07-05 - 2016-07-08; in: "Theory and Applications of Satisfiability Testing - SAT 2016 - 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings", Springer, LNCS 9710 (2016), 323 - 341
Lifting QBF Resolution Calculi to DQBF / O. Beyersdorff, L. Chew, R. Schmidt, M. Suda / Talk: 19th International Conference on Theory and Applications of Satisfiability Testing, SAT 2016, Bordeaux, France; 2016-07-05 - 2016-07-08; in: "Theory and Applications of Satisfiability Testing - SAT 2016 - 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings", Springer, LNCS 9710 (2016), 490 - 499
First-Order Logic and Blocked Clauses / B. Kiesl, M. Suda / Talk: 4th International Workshop on Quantified Boolean Formulas (QBF 2016), Bordeaux, France; 2016-07-04
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

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

2014

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

2013

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

2012

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

2011

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

2010

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

2007

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

2006

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

2005

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

2004

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

2003

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

2002

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

Theses

Automated Software Verification using Superposition-based Theorem Proving / Doctoral Thesis by B. Gleiss / Supervisor, Reviewer: L. Kovacs, S. Schulz; Institut for Logic and Computation, E192.04, 2020; oral examination: 2020-12-07
Automated Reasoning over Arrays in the Superposition Calculus / Master Thesis by C. Hochrainer / Supervisor: L. Kovacs; Institut for Logic and Computation, E192.04, 2020; final examination: 2020-07-21
Automating Termination Analysis of Probabilistic Programs / Master Thesis by M. Moosbrugger / Supervisor: L. Kovacs; Institut for Logic and Computation, E192.04, 2020; final examination: 2020-06-23
First-Order Reasoning with Aggregates / Master Thesis by S. Rain / Supervisor: L. Kovacs; Institut for Logic and Computation, E192.04, 2020; final examination: 2020-06-18
Formalizing Graph Trail Properties / Master Thesis by H. Lachnitt / Supervisor: L. Kovacs; Institut for Logic and Computation, E192.04, 2020; final examination: 2020-06-04
Abstraction for Reasoning about Agent Behavior with Answer Set Programming / Doctoral Thesis by Z. G. Saribatur / Supervisor, Reviewer: T. Eiter, G. Weissenbacher; Institut für Logic and Computation, 2019; oral examination: 2019-12-17
Trace Reasoning in Formal Verification - Guiding Vampire in Induction / Master Thesis by P. Georgiou / Supervisor: L. Kovacs; Institut for Logic and Computation, E192.04, 2019; final examination: 2019-11-22
Subsumption Demodulation in First-Order Theorem Proving / Master Thesis by J. Rath / Supervisor: L. Kovacs; Institut for Logic and Computation, E192.04, 2019; final examination: 2019-10-07
Effective Error Explanation Techniques for Concurrent Software / Doctoral Thesis by M. Tabaei Befrouei / Supervisor, Reviewer: G. Weissenbacher, T. Eiter, R. Majumdar; Informationssysteme, 2016; oral examination: 2016-12-06
Logical Methods in Automated Hardware and Software Verification / Habilitation Thesis by G. Weissenbacher / TU Wien/Fakultät für Informatik, 2016
Automated Complexity Analysis for Imperative Programs / Doctoral Thesis by M. Sinn / Supervisor, Reviewer: F. Zuleger, T. Vojnar; Institut für Informationssysteme, 2016
Merging in the Horn fragment / Master Thesis by A. Haret / Supervisor: S. Woltran, St. Rümmele; Institut für Informationssysteme, 2014; final examination: 2014-09-23
Complexity Results and Algorithms for Argumentation - Dung's Frameworks and Beyond / Doctoral Thesis by J. P. Wallner / Supervisor, Reviewer: S. Woltran, G. Weissenbacher; Institute of Information Systems, 2014; oral examination: 2014-05-28
Query-Based Test Case Generation / Doctoral Thesis by A. Holzer / Supervisor, Reviewer: H. Veith, D. Beyer; Fakultät für Informatik der Technischen Universität Wien, 2013
Loop Patterns in C Programs / Master Thesis by T. Pani / Supervisor: F. Zuleger, H. Veith; Fakultät für Informatik der Technischen Universität Wien, 2013
Software Veriﬁcation 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 / Doctoral Thesis by F. Zuleger / Supervisor, Reviewer: H. Veith, S. Gulwani; Institut für Informationssysteme, 2011; oral examination: 2011-05-11
Query-Driven Program Testing / Doctoral Thesis by M. Tautschnig / Supervisor, Reviewer: H. Veith, D. Kroening; Institut für Informationssysteme, 2011; oral examination: 2011-04-11
Architecture and Security in Networked Virtual Environments / Doctoral Thesis by C. Schallhart / Supervisor, Reviewer: G. Gottlob, H. Veith; Institut für Informationssysteme, Arbeitsbereich Datenbanken & Artificial Intelligence, 2007; oral examination: 2007-06-12
Reasoning about Specifications in Model Checking / Doctoral Thesis by M. Samer / Supervisor, Reviewer: H. Veith, G. Gottlob; Institut für Informationssysteme, 2004
Cryptographic Watermarking / Doctoral Thesis by S. Katzenbeisser / Supervisor, Reviewer: H. Veith, G. Gottlob; Institut für Informationssysteme, ARGR Datenbanken & Artificial Intelligence, 2004
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

Awards

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

And more…

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

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

Services

Institutes

Research Units