TU Home
This publication list has been generated automatically from the publication data of the Faculty of Informatics. Please invoke the page "Publications of the Faculty" directly for more complex searches and queries, or use the global search function of the Publication Database of the Vienna University of Technology!


Publication Database Home  

Publication list for members of
E192 - Institute of Logic and Computation
E192-04 Formal Methods in Systems Engineering
as authors or essentially involved persons

395 records (2002 - 2022)


Books and Book Editorships


E Albert, L. Kovacs (ed.):
"Proceedings of the 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-23)";
EasyChair EPiC Series in Computing, Alicante, Spain, 2020, ISSN: 2398-7340; 516 pages.

R. Bloem, S. Jacobs, A. Khalimov, I. Konnov, S. Rubin, H. Veith, J. Widder:
"Decidability of Parameterized Verification";
Morgan & Claypool Publishers, San Rafael, CA, USA, 2015, ISBN: 9781627057431; 170 pages.

B. Charron-Bost, A. Rybalchenko, S. Merz, J. Widder:
"Formal Verification of Distributed Algorithms (Dagstuhl Seminar 13141)";
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.

H. Chockler, G. Weissenbacher (ed.):
"Computer Aided Verification 2018 - Part I";
Springer, 2018, ISBN: 978-3-319-96144-6.

H. Chockler, G. Weissenbacher (ed.):
"Computer Aided Verification 2018 - Part II";
Springer, 2018, ISBN: 978-3-319-96141-5.

A. Ivrii, O. Strichman:
"Formal Methods in Computer-Aided Design";
in series "Conference Series: Formal Methods in Computer-Aided Design", series editor: W. Hunt, G. Weissenbacher; TU Wien Academic Press, 2020, ISBN: 978-3-85448-042-6.

I. Konnov, L. Kovacs (ed.):
"Proceedings of the 31st International Conference on Concurrency Theory (CONCUR)";
Dagstuhl Publishing LIPICS, Vienna, Austria, 2020, ISBN: 978-3-95977-160-3; 984 pages.

L. Kovacs, A. Voronkov:
"Proceedings of the 1st and 2nd Vampire Workshops";
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.

L. Kovacs, A. Voronkov:
"Vampire 2017. Proceedings of the 4th Vampire Workshop";
in series "Vampire 2017. Proceedings of the 4th Vampire Workshop", series editor: A. Voronkov; issued by: EasyChair; EasyChair EPiC Series in Computing, EasyChair, 2018.

N. Sharygina, H. Veith:
"CAV";
in series "Lecture Notes in Computer Science (LNCS 8044)", series editor: Springer Verlag; Springer, 2013, ISBN: 978-3-642-39798-1, 1015 pages.

D. Stewart, G. Weissenbacher (ed.):
"FMCAD'17: Proceedings of the 17th Conference on Formal Methods in Computer-Aided Design";
FMCAD Inc., Austin, TX, 2017, ISBN: 978-0-9835678-7-5; 241 pages.


Publications in Scientific Journals


B. Aminof, T. Kotek, S. Rubin, F. Spegni, H. Veith:
"Parameterized model checking of rendezvous systems";
Distributed Computing, 31 (2018), 3; 187 - 222.

B. Aminof, V. Malvone, A. Murano, S. Rubin:
"Graded modalities in Strategy Logic";
Information and Computation, 261 (2018), Part 4; 634 - 649.

B. Aminof, A. Murano, S. Rubin:
"CTL* with graded path modalities";
Information and Computation, 262 (2018), Part 1; 1 - 21.

B. Aminof, S. Rubin:
"First-cycle games";
Information and Computation, 254 (2017), 1; 195 - 216.

M. Barkatou, M. Jaroschek:
"Removing apparent singularities of linear difference systems";
Journal of Symbolic Computation, to appear (2019).

A. Bauer, M. Leucker, C. Schallhart, M. Tautschnig:
"Don't care in SMT---Building flexible yet efficient abstraction/refinement solvers";
International Journal on Software Tools for Technology Transfer, 12 (2010), 1; 23 - 37.

O. Beyersdorff, J. Blinkhorn, L. Chew, R. Schmidt, M. Suda:
"Reinterpreting Dependency Schemes: Soundness Meets Incompleteness in DQBF";
Journal of Automated Reasoning, J Autom Reasoning (2018), 1 - 27.

M. Bichler, M. Morak, S. Woltran:
"The Power of Non-Ground Rules in Answer Set Programming";
Theory and Practice of Logic Programming, 16 (2016), 5-6; 552 - 569.

N. Bjorner, R. Nieuwenhuis, H. Veith, A. Voronkov:
"Decision Procedures in Soft, Hard and Bio-ware - Follow Up (Dagstuhl Seminar 11272)";
Dagstuhl Reports, 1 (2011), 7; 23 - 35.

R. Bloem, S. Jacobs, A. Khalimov, I. Konnov, S. Rubin, H. Veith, J. Widder:
"Decidability of Parameterized Verification";
ACM SIGACT News, 47 (2016), 2; 53 - 64.

S. Chaki, C. Schallhart, H. Veith:
"Verification across Intellectual Property Boundaries";
ACM Transactions on Software Engineering and Methodology, 22 (2013), 2; Article 15.

B. Charron-Bost, M Függer, L. Welch, J. Widder:
"Time Complexity of Link Reversal Routing";
ACM Transactions on Algorithms, 11 (2015), 3; 1 - 39.

B. Charron-Bost, A. Gaillard, L. Welch, J. Widder:
"Link Reversal Routing with Binary Link Labels: Work Complexity";
SIAM JOURNAL ON COMPUTING, 42 (2013), 2; 634 - 661.

E. Clarke, O. Grumberg, S. Jha, Y. Lu, H. Veith:
"Counterexample-Guided Abstraction Refinement for Symbolic Model Checking";
Journal of the ACM, Volume 50 (2003), Issue 5; 752 - 794.

A. Dawar, H. Veith:
"Selected Papers of the Conference "Computer Science Logic CSL 2010": Preface";
Logical Methods in Computer Science, (2012).

A. De Coster, N. Musliu, A. Schaerf, J. Schoisswohl, K. Smith-Miles:
"Algorithm selection and instance space analysis for curriculum-based course timetabling";
Journal of Scheduling, 26 (2021), 4; 1 - 24.

Y. Demyanova, T. Pani, H. Veith, F. Zuleger:
"Empirical software metrics for benchmarking of verification tools";
Formal Methods in System Design, 50 (2017), 2; 289 - 316.

M. Dod, T. Kotek, J. Preen, P. Tittmann:
"Bipartition polynomials, the Ising model and domination in graphs";
Discussiones Mathematicae Graph Theory, 35 (2015), 2; 335 - 353.

T. Eiter, H. Veith:
"On the complexity of Data Disjunctions";
Theoretical Computer Science, 288 (2002), 101 - 128.

A. Fellner, W. Krenn, R. Schlick, T. Tarrach, G. Weissenbacher:
"Model-based, Mutation-driven Test-case Generation Via Heuristic-guided Branching Search";
ACM Transactions on Embedded Computing Systems, 18 (2019), 1.

A. Fellner, M. Tabaei Befrouei, G. Weissenbacher:
"Mutation testing with hyperproperties";
Journal of Software and Systems Modeling (online-edition), 20 (2021), 2; 405 - 427.

G. Gottlob, E. Grädel, H. Veith:
"Datalog LITE: a deductive query language with linear time model checking";
ACM Transactions on Computational Logic, Volume 3 (2002), 1; 42 - 79.

A. Holzer, C. Schallhart, M. Tautschnig, H. Veith:
"Closure properties and complexity of rational sets of regular languages";
Theoretical Computer Science, 605 (2015), 62 - 79.

G. Ianni, F. Calimeri, S. Germano, A. Humenberger, C. Redl, D. Stepanova, A. Tucci, A. Wimmer:
"Angry-HEX: an Artificial Player for Angry Birds Based on Declarative Knowledge Bases";
IEEE Transactions on Computational Intelligence and AI in Games, 8 (2016), 128 - 139.

M. Jaroschek, M. Barkatou, S. Maddah:
"Formal solutions of completely integrable Pfaffian systems with normal crossings";
Journal of Symbolic Computation, 81 (2017), 41 - 68.

S. Jha, S. Katzenbeisser, C. Schallhart, H. Veith, St. Chenney:
"Semantic Integrity in Large-Scale Online Simulations";
ACM Transactions on Internet Technology, 10 (2010), 1.

J. Kinder, S. Katzenbeisser, C. Schallhart, H. Veith:
"Proactive Detection of Computer Worms Using Model Checking";
IEEE Transactions on Dependable and Secure Computing, 7 (2010), 4; 424 - 438.

J. Knoop, L. Kovacs, J. Zwirchmayr:
"Replacing conjectures by positive knowledge: Inferring proven precise worst-case execution time bounds using symbolic execution";
Journal of Symbolic Computation, 80 (2017), 101 - 124.

I. Konnov, M. Lazić, H. Veith, J. Widder:
"Para^2: Parameterized Path Reduction, Acceleration, and SMT for Reachability in Threshold-Guarded Distributed Algorithms";
Formal Methods in System Design (invited), 51 (2017), 2; 270 - 307.

I. Konnov, H. Veith, J. Widder:
"On the completeness of bounded model checking for threshold-based distributed algorithms: Reachability";
Information and Computation, 252 (2017), 95 - 109.

T. Kotek, J. A. Makowsky:
"A representation theorem for (q-)holonomic sequences";
Journal of Computer and System Sciences, 80 (2014), 2; 363 - 374.

T. Kotek, J. A. Makowsky:
"Connection Matrices and the Definability of Graph Parameters";
Logical Methods in Computer Science, 10 (2014), 4; 1 - 33.

T. Kotek, J. A. Makowsky:
"Efficient computation of generalized Ising polynomials on graphs with fixed clique-width";
Topics in Theoretical Computer Science (TTCS), 9541 (2015), 135 - 146.

T. Kotek, J. A. Makowsky:
"Recurrence relations for graph polynomials on bi-iterative families of graphs";
European Journal of Combinatorics, 41 (2014), 47 - 67.

B. Kulahcioglu Ozkan, R. Majumdar, F. Niksic, M. Tabaei Befrouei, G. Weissenbacher:
"Randomized testing of distributed systems with probabilistic guarantees";
Proceedings of the ACM on Programming Languages, 2 (2018), OOPSLA.

M. Lewis, D. Kroening, G. Weissenbacher:
"Under-approximating loops in C programs for fast counterexample detection";
Formal Methods in System Design, 47 (2015), 1; 75 - 92.

P. Metzler, N. Suri, G. Weissenbacher:
"Extracting safe thread schedules from incomplete model checking results";
International Journal on Software Tools for Technology Transfer, 22 (2020), 5; 565 - 581.

T. Pani, H. Veith, F. Zuleger:
"Loop Patterns in C Programs";
ECEASST, 72 (2015).

T. Pani, G. Weissenbacher, F. Zuleger:
"Rely-guarantee bound analysis of parameterized concurrent shared-memory programs";
Formal Methods in System Design, 57 (2021), 2; 270 - 302.

M. Samer, H. Veith:
"On the distributivity of LTL specifications";
ACM Transactions on Computational Logic, 11 (2010), 3.

M. Schlaipfer, G. Weissenbacher:
"Labelled Interpolation Systems for Hyper-Resolution, Clausal, and Local Proofs";
Journal of Automated Reasoning, 57 (2016), 1; 3 - 36.

M. Sinn, H. Veith, F. Zuleger:
"Complexity and Resource Bound Analysis of Imperative Programs Using Difference Constraints";
Journal of Automated Reasoning, 59 (2017), 1; 3 - 45.

S. Stankovic, E. Bartocci, L. Kovacs:
"Moment-based analysis of Bayesian network properties";
Theoretical Computer Science, 903 (2022), 113 - 133.

M. Tabaei Befrouei, C. Wang, G. Weissenbacher:
"Abstraction and mining of traces to explain concurrency bugs";
Formal Methods in System Design, 49 (2016), 1; 1 - 32.

H. Veith:
"Special Issue: Games in Verification (foreword)";
Journal of Computer and System Sciences, 78 (2012), 2; 393.

Y. Vizel, G. Weissenbacher, S. Malik:
"Boolean Satisfiability Solvers and Their Applications in Model Checking";
Proceedings of the IEEE (invited), 103 (2015), 11; 2021 - 2035.

J. Widder, M. Biely, G. Gridling, B. Weiss, J. Blanquart:
"Consensus in the presence of mortal Byzantine faulty processes";
Distributed Computing, 24 (2012), 6; 299 - 321.


Editorials in Scientific Journals


H. Chockler, G. Weissenbacher:
"Preface of the special issue on the conference on computer-aided verification 2018";
Formal Methods in System Design, 57 (2021), 1; 1 - 2.

J. Davenport, L. Kovacs, D. Zaharie:
"Foreword";
Mathematics in Computer Science, 13 (2019), 4; 459 - 460.

G. Gottlob, T. Henzinger, G. Weissenbacher:
"Preface of the Special Issue in Memoriam Helmut Veith";
Formal Methods in System Design, 51 (2017), 2; 267 - 269.

P. Schreck, T. Ida, L. Kovacs:
"Foreword - Formalization of geometry, automated and interactive geometric reasoning";
Annals of Mathematics and Artificial Intelligence, 85 (2019), 2-4; 71 - 72.

D. Stewart, G. Weissenbacher:
"Preface of the Special Issue on the Conference on Formal Methods in Computer-Aided Design 2017";
Formal Methods in System Design, 56 (2020), 1-3; 1.


Contributions to Books


E. Clarke, H. Veith:
"Counterexamples Revisited: Principles, Algorithms, Applications";
in: "Verification: Theory and Practice: Essays Dedicated to Zohar Manna on the Occasion of his 64th Birthday", Springer, LNCS, Heidelberg, 2004, ISBN: 3-540-21002-4, 208 - 224.

A. Gmeiner, I. Konnov, U. Schmid, H. Veith, J. Widder:
"Tutorial on Parameterized Model Checking of Fault-Tolerant Distributed Algorithms";
in: "Formal Methods for Executable Software Models", Springer, 2014, (invited), ISBN: 978-3-319-07316-3, 122 - 171.

S. Katzenbeisser, J. Kinder, H. Veith:
"Malware Detection";
in: "Encyclopedia of Cryptography and Security", H. van Tilborg, S. Jajodia (ed.); Springer-Verlag, 2011, ISBN: 978-1-4419-5905-8, 752 - 755.

M. Samer, H. Veith:
"From Temporal Logic Queries to Vacuity Detection";
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.


Contributions to Proceedings


B. Aminof, G. De Giacomo, A. Lomuscio, A. Murano, S. Rubin:
"Synthesizing strategies under expected and exceptional environment behaviors";
in: "Proceedings of the Twenty-Ninth International Joint Conference on Artificial Intelligence", International Joint Conferences on Artificial Intelligence Organization, 2020, 1674 - 1680.

B. Aminof, G. De Giacomo, A. Murano, S. Rubin:
"Planning under LTL Environment Specifications";
in: "29th International Conference on Automated Planning and Scheduling", AAAI Press, 2019, 31 - 39.

B. Aminof, G. De Giacomo, S. Rubin:
"Stochastic Fairness and Language-Theoretic Fairness in Planning in Nondeterministic Domains";
in: "Proceedings of the Thirtieth International Conference on Automated Planning and Scheduling, Nancy, France", AAAI Press, 2020, 20 - 28.

B. Aminof, M. Kwiatkowska, B. Maubert, A. Murano, S. Rubin:
"Probabilistic Strategy Logic";
in: "28th International Joint Conference on Artificial Intelligence", International Joint Conferences on Artificial Intelligence, 2019, 32 - 38.

N. Bertrand, I. Konnov, M. Lazić, J. Widder:
"Verification of Randomized Consensus Algorithms Under Round-Rigid Adversaries";
in: "30th International Conference on Concurrency Theory", Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany, 2019, 33:1 - 33:15.

S. Chaki, E. Clarke, A. Groce, S. Jha, H. Veith:
"Modular Verification of Software Components in C*";
in: "Proceedings of the 25th Conference on Software Engineering ", issued by: 25thConference on Software Engineering; IEEE, 2003, ISBN: 0-7695-1877-x, 385 - 395.

A. Damian, C. Dragoi, A. Militaru, J. Widder:
"Communication-Closed Asynchronous Protocols";
in: "International Conference on Computer Aided Verification", Springer, 2019, 344 - 363.

G. Ebner, M. Schlaipfer:
"Efficient Translation of Sequent Calculus Proofs Into Natural Deduction Proofs";
in: "PAAR 2018 Practical Aspects of Automated Reasoning", 2162; University of Liverpool, UK, 2018, 17 - 33.

W. Forkel, T. Philipp, A. Rebola Pardo, E. Werner:
"Fuzzing and Verifying RAT Refutations with Deletion Information";
in: "Florida Artificial Intelligence Research Society Conference", AAAI Press, 2017, 190 - 193.

L. Kovacs, A. Voronkov:
"First-Order Interpolation and Interpolating Proof Systems";
in: "LPAR-21. 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning", EasyChair EPiC Series in Computing, Volume 46, 2017, 49 - 64.

A. Kruckman, S. Rubin, J. Sheridan, B. Zax:
"A Myhill-Nerode theorem for automata with advice";
in: "Symposium on Games, Automata, Logics and Formal Verification", M. Faella, A. Murano (ed.); Electronic Proceedings in Theoretical Computer Science, 2012, 238 - 246.

J. Pagel, C. Matheja, F. Zuleger:
"Effective Entailment Checking for Separation Logic with Inductive Definitions";
in: "25th International Conference, TACAS 2019", Springer, 2019, 319 - 336.

J. Pagel, F. Zuleger:
"Beyond Symbolic Heaps: Deciding Separation Logic With Inductive Definitions";
in: "23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Alicante, Spain", 73; EasyChair EPiC Series in Computing, 2020, 390 - 408.

T. Philipp, A. Rebola Pardo:
"Towards a Semantics of Unsatisfiability Proofs with Inprocessing";
in: "Logic Programming and Automated Reasoning (LPAR)", EasyChair EPiC Series in Computing, 2017, 65 - 84.

G. Reger, M. Suda:
"Global Subsumption Revisited (Briefly)";
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.

G. Reger, M. Suda:
"Incremental Solving with Vampire";
in: "Proceedings of the 4th Vampire Workshop", 53; issued by: EasyChair; EasyChair EPiC Series in Computing, EasyChair, 2018, 12 pages.

G. Reger, M. Suda:
"Local proofs and AVATAR";
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.

M. Schlaipfer, K. Rajan, A. Lal, M. Samak:
"Optimizing Big-Data Queries Using Program Synthesis";
in: "Symposium on Operating Systems Principles", ACM, 2017, ISBN: 978-1-4503-5085-3, 631 - 646.

M. Sighireanu, J. Pagel, C. Matheja, T. Noll, F. Zuleger et al.:
"SL-COMP: Competition of Solvers for Separation Logic";
in: "25th International Conference, TACAS 2019", Springer, 2019, 116 - 132.

I. Stoilkovska, I. Konnov, J. Widder, F. Zuleger:
"Eliminating Message Counters in Threshold Automata";
in: "Automated Technology for Verification and Analysis - 18th Symposium, 2020, Hanoi, Vietnam", 12302; Springer LNCS, 2020, 196 - 212.

I. Stoilkovska, I. Konnov, J. Widder, F. Zuleger:
"Verifying Safety of Synchronous Fault-Tolerant Algorithms by Bounded Model Checking";
in: "International Conference on Tools and Algorithms for the Construction and Analysis of Systems", Springer, 2019, 357 - 374.

F. Zuleger:
"The Polynomial Complexity of Vector Addition Systems with States";
in: "Foundations of Software Science and Computation Structures - 23rd International Conference, Dublin, Ireland", 12077; Springer LNCS, 2020, 622 - 641.


Editorials in Proceedings


M. Suda:
"CICM 2016 Doctoral Program";
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.


Talks and Poster Presentations (with Proceedings-Entry)


P. Čadek, C. Danninger, M. Sinn, F. Zuleger:
"Using Loop Bound Analysis For Invariant Generation";
Talk: International Conference on Formal Methods in Computer-Aided Design (FMCAD), Austin, TX; 2018-10-30 - 2018-11-02; in: "Formal Methods in Computer-Aided Design", FMCAD Inc., (2018), ISBN: 978-0-9835678-8-2; 1 - 9.

A. Adelsbach, S. Katzenbeisser, H. Veith:
"Watermarking schemes provably secure against copy and ambiguity attacks";
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.

B. Aminof, G. De Giacomo, A. Lomuscio, A. Murano, S. Rubin:
"Synthesizing Best-effort Strategies under Multiple Environment Specifications";
Talk: KR 2021 - 18th International Conference on Principles of Knowledge Representation and Reasoning, Rhodes, Greece; 2020-08-13 - 2020-08-14; in: "KR 2021 - 18th International Conference on Principles of Knowledge Representation and Reasoning", (2020), 42 - 51.

B. Aminof, G. De Giacomo, A. Murano, S. Rubin:
"Synthesis under Assumptions";
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.

B. Aminof, G. De Giacomo, S. Rubin:
"Best-Effort Synthesis: Doing Your Best Is Not Harder Than Giving Up";
Talk: IJCAI 2021 - 30th International Joint Conference on Artificial Intelligence, Montreal, Canada; 2021-08-19 - 2021-08-27; in: "Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence (IJCAI-21)", (2021), 1766 - 1772.

B. Aminof, S. Jacobs, A. Khalimov, S. Rubin:
"Parameterized Model Checking of Token-Passing Systems";
Talk: Verification, Model Checking, and Abstract Interpretation (VMCAI), San Diego; 2014-02-19; in: "VMCAI", Springer / LNCS, 8318 (2014), 262 - 281.

B. Aminof, T. Kotek, S. Rubin, F. Spegni, H. Veith:
"Parameterized Model Checking of Rendezvous Systems";
Talk: International Conference on Concurrency Theory (CONCUR), Rom, Italien; 2014-09-02 - 2014-09-05; in: "CONCUR", Springer / LNCS, 8704 (2014), 109 - 124.

B. Aminof, V. Malvone, A. Murano, S. Rubin:
"Extended Graded Modalities in Strategy Logic";
Talk: 4th International Workshop on Strategic Reasoning, New York; 2016-07-10; in: "SR", (2016), 1 - 14.

B. Aminof, V. Malvone, A. Murano, S. Rubin:
"Graded Strategy Logic: Reasoning about Uniqueness of Nash Equilibria";
Talk: International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS), Singapur; 2016-05-09 - 2016-05-13; in: "AAMAS", (2016), 698 - 706.

B. Aminof, A. Murano, S. Rubin, F. Zuleger:
"Automatic Verification of Multi-Agent Systems in Parameterised Grid-Environments";
Talk: International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS), Singapur; 2016-05-09 - 2016-05-13; in: "AAMAS", (2016), 1190 - 1199.

B. Aminof, A. Murano, S. Rubin, F. Zuleger:
"Prompt Alternating-Time Epistemic Logics";
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.

B. Aminof, A. Murano, S. Rubin, F. Zuleger:
"Verification of Asynchronous Mobile-Robots in Partially-Known Environments";
Talk: Principles and Practice of Multi-Agent Systems, Graz; 2015-05-18 - 2015-05-19; in: "PRIMA", Springer, 9387 (2015), 185 - 200.

B. Aminof, S. Rubin:
"First Cycle Games";
Talk: International Workshop on Strategic Reasoning (SR), Grenoble, Frankreich; 2014-04-05 - 2014-04-06; in: "SR", EPTCS, 146 (2014), 83 - 90.

B. Aminof, S. Rubin:
"Model Checking Parameterised Multi-token Systems via the Composition Method";
Talk: IJCAR, Coimbra; 2016-06-27 - 2016-07-02; in: "IJCAR", LNCS/Springer, 8562 (2016), ISBN: 978-3-319-08587-6; 499 - 515.

B. Aminof, S. Rubin, F. Spegni, F. Zuleger:
"Liveness of Parameterized Timed Networks";
Talk: International Colloquium on Automata, Languages and Programming (ICALP), Kyoto, Japan; 2015-07-06 - 2015-07-10; in: "ICALP", Springer, 9135 (2015), 375 - 387.

B. Aminof, S. Rubin, I. Stoilkovska, J. Widder, F. Zuleger:
"Parameterized Model Checking of Synchronous Distributed Algorithms by Abstraction";
Talk: Verification, Model Checking, and Abstract Interpretation (VMCAI), Los Angeles; 2018-01-07 - 2018-01-09; in: "VMCAI", LNCS/Springer, 10747 (2018), 1 - 24.

B. Aminof, S. Rubin, F. Zuleger:
"On the Expressive Power of Communication Primitives in Parameterised Systems";
Talk: Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), Suva, Fiji; 2015-11-24 - 2015-11-28; in: "LPAR", Springer, 9450 (2015), 313 - 328.

B. Aminof, I. Stoilkovska, S. Rubin, J. Widder, F. Zuleger:
"Parameterized Model Checking of Synchronous Distributed Algorithms by Abstraction";
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.

M. Barkatou, M. Jaroschek:
"Desingularization of First Order Linear Difference Systems with Rational Function Coefficients";
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.

G. Barthe, R. Eilers, P. Georgiou, B. Gleiss, L. Kovacs, M. Maffei:
"Verifying Relational Properties using Trace Logic";
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.

E. Bartocci, L. Kovacs, S. Stankovic:
"Analysis of Bayesian Networks via Prob-Solvable Loops";
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.

E. Bartocci, L. Kovacs, S. Stankovic:
"Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops";
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.

E. Bartocci, L. Kovacs, S. Stankovic:
"Mora - Automatic Generation of Moment-Based Invariants";
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.

H. Basold, H. Günther, M. Huhn, S. Milius:
"An Open Alternative for SMT-Based Verification of Scade Models";
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.

D. Beyer, A. Holzer, M. Tautschnig, H. Veith:
"Information Reuse for Multi-goal Reachability Analyses";
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.

D. Beyer, A. Holzer, M. Tautschnig, H. Veith:
"Reusing Information in Multi-Goal Reachability Analyses";
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.

O. Beyersdorff, L. Chew, R. Schmidt, M. Suda:
"Lifting QBF Resolution Calculi to DQBF";
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.

M. Bichler, M. Morak, S. Woltran:
"lpopt: A Rule Optimization Tool for Answer Set Programming";
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.

J. Birgmeier, A. Bradley, G. Weissenbacher:
"Counterexample to Induction-Guided Abstraction-Refinement (CTIGAR)";
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.

R. Bloem, S. Malik, M. Schlaipfer, G. Weissenbacher:
"Reduction of Resolution Refutations and Interpolants via Subsumption";
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.

S. Blom, T. van Dijk, K. Gijis, A. Laarman, J. Meijer, J. van de Pol:
"LTSmin: High-Performance Language-Independent Model Checking";
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.

T. Brazdil, K. Chatterjee, A. Kucera, P. Novotny, D. Velan, F. Zuleger:
"Efficient Algorithms for Asymptotic Bounds on Termination Time in VASS";
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.

S. Bünte, M. Zolda, M. Tautschnig, R. Kirner:
"Improving the Confidence in Measurement-Based Timing Analysis";
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.

D. Calvanese, T. Kotek, M. Simkus, H. Veith, F. Zuleger:
"Shape and Content - A Database-Theoretic Perspective on the Analysis of Data Structures";
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.

D. Calvanese, T. Kotek, M. Simkus, H. Veith, F. Zuleger:
"Shape and Content: Incorporating Domain Knowledge into Shape Analysis";
Talk: International Workshop on Description Logics, Wien; 2014-07-17 - 2014-07-20; in: "International Workshop on Description Logics", (2014), 4 pages.

Z. Charlie Shucheng, G. Weissenbacher, S. Malik:
"Coverage-based Trace Signal Selection for Fault Localisation in Post-Silicon Validation";
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.

P. Chauhan, E. Clarke, J. Kukula, S. Sapra, H. Veith, D. Wang:
"Automated Abstraction Refinement for Model Checking Large State Spaces using SAT based Conflict Analysis";
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.

K. Claessen, J. Kilhamn, L. Kovacs, B. Lennartson:
"A Supervisory Control Algorithm Based on Property-Directed Reachability";
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.

E. Clarke, S. Jha, Y. Lu, H. Veith:
"Tree-Like Counterexamples in Model Cheking";
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.

E. Clarke, M. Talupur, H. Veith, D. Wang:
"SAT Based Predicate Abstraction for Hardware Verification";
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.

T. Colcombet, L. Daviaud, F. Zuleger:
"Size-Change Abstraction and Max-Plus Automata";
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.

B. Cook, A. See, F. Zuleger:
"Ramsey vs. Lexicographic Termination Proving";
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.

D. Damestani, L. Kovacs, M. Suda:
"Superposition Reasoning about Quantified Bitvector Formulas";
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.

L. Daviaud, T. Colcombet, F. Zuleger:
"Automata and Program Analysis";
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.

J. Delobelle, A. Haret, S. Konieczny, J. Mailly, J. Rossit, S. Woltran:
"Merging of Abstract Argumentation Frameworks";
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.

Y. Demyanova, T. Pani, H. Veith, F. Zuleger:
"Empirical Software Metrics for Benchmarking of Verification Tools";
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.

Y. Demyanova, P. Rümmer, F. Zuleger:
"Systematic Predicate Abstraction Using Variable Roles";
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.

Y. Demyanova, H. Veith, F. Zuleger:
"On the concept of variable roles and its use in software analysis";
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.

T. Deutsch, J. Widder:
"Approaching Verification and Validation Challenges in Smart Grids";
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.

M. Diller, A. Haret, T. Linsbichler, St. Rümmele, S. Woltran:
"An extension-based approach to belief revision in abstract argumentation";
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.

C. Dragoi, T. Henzinger, H. Veith, J. Widder, D. Zufferey:
"A Logic-Based Framework for Verifying Consensus Algorithms";
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.

C. Dragoi, M. Lazić, J. Widder:
"Communication-Closed Layers as Paradigm for Distributed Systems: A Manifesto";
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.

T. Durand, K. Fazekas, G. Weissenbacher, J. Zwirchmayr:
"Model Checking AUTOSAR Components with CBMC";
Talk: Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design - FMCAD 2021, New Haven, Connecticut, USA; 2021-10-19 - 2021-10-22; in: "Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design - FMCAD 2021", R. Piskac, M. Whalen (ed.); TU Wien Academic Press, 2 (2021), ISBN: 978-3-85448-046-4; 96 - 101.

N. Elad, S. Rain, N. Immerman, M. Sagiv, L. Kovacs:
"Summing Up Smart Transitions";
Talk: 33rd International Conference on Computer Aided Verification (CAV), Los Angeles, US; 2021-07-20 - 2021-07-23; in: "Proceedings of the 33rd International Conference on Computer Aided Verification (CAV)", A. Silva, R. Leino (ed.); Springer LNCS, 12759 (2021), 317 - 340.

A. Farzan, A. Holzer, N. Razavi, H. Veith:
"Con2colic testing";
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.

A. Farzan, A. Holzer, N. Razavi, H. Veith:
"Concolic Testing of Concurrent Programs";
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. Farzan, A. Holzer, H. Veith:
"Perspectives on White-Box Testing: Coverage, Concurrency, and Concolic Execution";
Keynote Lecture: International Conference on Software Testing, Verification and Validation (ICST), Graz; 2015-04-14 - 2015-04-16; in: "ICST", (2015), 1 - 11.

A. Fellner, W. Krenn, R. Schlick, T. Tarrach, G. Weissenbacher:
"Model-based, mutation-driven test case generation via heuristic-guided branching search";
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.

A. Fellner, M. Tabaei Befrouei, G. Weissenbacher:
"Mutation Testing with Hyperproperties";
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.

A. Fellner, T. Tarrach, G. Weissenbacher:
"Language Inclusion for Finite Prime Event Structures";
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.

T. Fiedor, L. Holik, A. Rogalewicz, M. Sinn, T. Vojnar, F. Zuleger:
"From Shapes to Amortized Complexity";
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.

M. Franz, A. Holzer, S. Katzenbeisser, C. Schallhart, H. Veith:
"CBMC-GC: An ANSI C Compiler for Secure Two-Party Computations";
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.

M. Franz, A. Holzer, S. Katzenbeisser, C. Schallhart, H. Veith:
"Compilation for Secure Two-Party Computations";
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.

M. Franz, A. Holzer, R. Majumdar, B. Parno, H. Veith:
"The first workshop on language support for privacy-enhancing technologies (PETShop'13)";
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.

A. Fröhlich, G. Kovasznai, A. Biere, H. Veith:
"On the Complexity of Symbolic Verification and Decision Problems in Bit-Vector Logic";
Talk: International Workshop on Pragmatics of SAT (POS), Wien; 2014-07-13; in: "POS", (2014), 14 pages.

M Függer, J. Widder:
"Efficient Checking of Link-Reversal-Based Concurrent Systems";
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.

P. Georgiou, B. Gleiss, L. Kovacs:
"Trace Logic for Inductive Loop Reasoning";
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.

B. Gleiss, L. Kovacs, J. Rath:
"Subsumption Demodulation in First-Order Theorem Proving";
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.

B. Gleiss, L. Kovacs, S. Robillard:
"Loop Analysis by Quantification over Iterations";
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.

B. Gleiss, L. Kovacs, L. Schnedlitz:
"Interactive Visualization of Saturation Attempts in Vampire";
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.

B. Gleiss, L. Kovacs, M. Suda:
"Splitting Proofs for Interpolation";
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.

B. Gleiss, M. Suda:
"Layered Clause Selection for Saturation-Based Theorem Proving";
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.

B. Gleiss, M. Suda:
"Layered Clause Selection for Theory Reasoning (Short Paper)";
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.

H. Günther, A. Laarman, A. Sokolova, G. Weissenbacher:
"Dynamic Reductions for Model Checking Concurrent Software";
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.

H. Günther, G. Weissenbacher:
"Incremental bounded software model checking";
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.

S. Gulwani, I. Radicek, F. Zuleger:
"Feedback generation for performance problems in introductory programming assignments";
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.

S. Gulwani, F. Zuleger:
"The reachability-bound problem";
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.

W. Haberl, M. Herrmannsdoerfer, St. Kugele, M. Tautschnig, M. Wechs:
"Seamless Model-driven Development put into Practice";
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.

M. Hajdu, P. Hozzova, L. Kovacs, J. Schoisswohl, A. Voronkov:
"Induction with Generalization in Superposition Reasoning";
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.

M. Hajdu, P. Hozzova, L. Kovacs, J. Schoisswohl, A. Voronkov:
"Inductive Benchmarks for Automated Reasoning";
Talk: Proceedings of the 14th International Conference on Intelligent Computer Mathematics (CICM), Timisoara, Romania; 2021-07-26 - 2021-07-31; in: "Proceedings of the 14th International Conference on Intelligent Computer Mathematics (CICM)", F. Kamareddine, C. Sacerdoti Coen (ed.); Springer LNCS, 12833 (2021), 124 - 129.

M. Hajdu, P. Hozzova, L. Kovacs, A. Voronkov:
"Induction with Recursive Definitions in Superposition";
Talk: Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design - FMCAD 2021, New Haven, Connecticut, USA; 2021-10-19 - 2021-10-22; in: "Proceedings of the 21st International Conference on Formal Methods in Computer Aided Design (FMCAD)", R. Piskac, M. Wahlen (ed.); TU Wien Academic Press, 2 (2021), ISBN: 978-3-85448-046-4; 1 - 10.

A. Haret:
"Logic-Based Merging in Fragments of Classical Logic with Inputs from Social Choice Theory";
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.

A. Haret, J. Mailly, S. Woltran:
"Distributing Knowledge Into Simple Bases";
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.

A. Haret, J. Mailly, S. Woltran:
"Distributing Knowledge Into Simple Bases";
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.

A. Haret, A. Pfandler, S. Woltran:
"Beyond IC Postulates: Classification Criteria for Merging Operators";
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.

A. Haret, St. Rümmele, S. Woltran:
"Merging in the Horn Fragment";
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.

A. Haret, S. Woltran:
"Deviation in Belief Change on Fragments of Propositional Logic";
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.

K. Hoder, A. Holzer, L. Kovacs, A. Voronkov:
"Vinter: A Vampire-Based Tool for Interpolation";
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.

K. Hoder, G. Reger, M. Suda, A. Voronkov:
"Selecting the Selection";
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.

A. Holzer, M. Franz, S. Katzenbeisser, H. Veith:
"Secure two-party computations in ANSI C";
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.

A. Holzer, V. Januzaj, St. Kugele, B. Langer, C. Schallhart, M. Tautschnig, H. Veith:
"Seamless testing for models and code";
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.

A. Holzer, V. Januzaj, St. Kugele, M. Tautschnig:
"Timely Time Estimates";
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.

A. Holzer, N. Karvelas, S. Katzenbeisser, H. Veith:
"Challenges in Compiler Construction for Secure Two-Party Computation";
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.

A. Holzer, D. Kroening, C. Schallhart, M. Tautschnig, H. Veith:
"Proving Reachability Using FShell";
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.

A. Holzer, C. Schallhart, M. Tautschnig, H. Veith:
"An Introduction to Test Specification in FQL";
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.

A. Holzer, C. Schallhart, M. Tautschnig, H. Veith:
"How did you specify your test suite?";
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.

A. Holzer, C. Schallhart, M. Tautschnig, H. Veith:
"On the Structure and Complexity of Rational Sets of Regular Languages";
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.

A. Holzer, D. Schwartz-Narbonne, M. Tabaei Befrouei, G. Weissenbacher, T. Wies:
"Error Invariants for Concurrent Traces";
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.

P. Hozzova, L. Kovacs, J. Rath:
"Automated Generation of Exam Sheets for Automated Deduction";
Talk: Proceedings of the 14th International Conference on Intelligent Computer Mathematics (CICM), Timisoara, Romania; 2021-07-26 - 2021-07-31; in: "Proceedings of the 14th International Conference on Intelligent Computer Mathematics (CICM)", Springer LNCS, 12833 (2021), 185 - 196.

P. Hozzova, L. Kovacs, A. Voronkov:
"Integer Induction in Saturation";
Talk: 28th International Conference on Automated Deduction (CADE 28), Virtual Event; 2021-07-12 - 2021-07-15; in: "Proceedings of the 28th International Conference on Automated Deduction (CADE-28)", A. Platzer, G. Sutcliffe (ed.); Springer LNCS, 12669 (2021), 361 - 377.

A. Humenberger, N. Bjorner, L. Kovacs:
"Algebra-Based Loop Synthesis";
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.

A. Humenberger, M. Jaroschek, L. Kovacs:
"Aligator.jl - A Julia Package for Loop Invariant Generation";
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.

A. Humenberger, M. Jaroschek, L. Kovacs:
"Automated Generation of Non-Linear Loop Invariants Utilizing Hypergeometric Sequences";
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.

A. Humenberger, M. Jaroschek, L. Kovacs:
"Invariant Generation for Multi-Path Loops with Polynomial Assignments";
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.

A. Humenberger, L. Kovacs:
"Algebra-Based Synthesis of Loops and Their Invariants";
Talk: 22nd International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), Copenhagen, Denmark (invited); 2021-01-17 - 2021-01-19; in: "Proceedings of the 22n International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI)", F. Henglein, S. Shoham, Y. Vizel (ed.); Springer LNCS, 12597 (2021), 17 - 28.

A. Ignatiev, A. Morgado, J. Marques-Silva, G. Weissenbacher:
"Model-Based Diagnosis with Multiple Observations";
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.

J. Jakubuv, M. Suda, J. Urban:
"Automated Invention of Strategies and Term Orderings for Vampire";
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.

M. Janota, M. Suda:
"Towards Smarter MACE-style Model Finders";
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. John, I. Konnov, U. Schmid, H. Veith, J. Widder:
"Brief announcement: parameterized model checking of fault-tolerant distributed algorithms by abstraction";
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.

A. John, I. Konnov, U. Schmid, H. Veith, J. Widder:
"Parameterized model checking of fault-tolerant distributed algorithms by abstraction";
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.

A. John, I. Konnov, U. Schmid, H. Veith, J. Widder:
"Towards Modeling and Model Checking Fault-Tolerant Distributed Algorithms";
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.

A. Karimi, S. Stankovic, M. Moosbrugger, L. Kovacs, E. Bartocci, E. Bura:
"Distribution Estimation for Probabilistic Loops";
accepted as talk for: Proc. of QEST 2022: the 19th International Conference on Quantitative Evaluation of SysTems, Warsaw, Poland; 2022-09-12 - 2022-09-16; in: "Proc. of QEST'22: the 19th International Conference on Quantitative Evaluation of SysTems", (2022).

S. Katzenbeisser, H. Veith:
"Securing Symmetric Watermarking Schemes Against Protocol Attacks";
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.

B. Kiesl, A. Rebola Pardo, M. Heule:
"Extended Resolution Simulates DRAT";
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.

B. Kiesl, M. Suda:
"A Unifying Principle for Clause Elimination in First-Order Logic";
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.

B. Kiesl, M. Suda, M. Seidl, H. Tompits, A. Biere:
"Blocked Clauses in First-Order Logic";
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.

A. Kofnov, M. Moosbrugger, S. Stankovic, E. Bartocci, E. Bura:
"Moment-based Invariants for Probabilistic Loops with non-polynomial assignments";
accepted as talk for: Proc. of QEST 2022: the 19th International Conference on Quantitative Evaluation of SysTems, Warsaw, Poland; 2022-09-12 - 2022-09-16; in: "Proc. of QEST'22: the 19th International Conference on Quantitative Evaluation of SysTems", (2022).

I. Konnov, T. Kotek, Q. Wang, H. Veith, S. Bliudze, J. Sifakis:
"Parameterized Systems in BIP: Design and Model Checking";
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.

I. Konnov, M. Lazić, H. Veith, J. Widder:
"A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms";
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.

I. Konnov, H. Veith, J. Widder:
"On the Completeness of Bounded Model Checking for Threshold-Based Distributed Algorithms: Reachability";
Talk: International Conference on Concurrency Theory (CONCUR), Rom, Italien; 2014-09-02 - 2014-09-05; in: "CONCUR", (2014), 125 - 140.

I. Konnov, H. Veith, J. Widder:
"SMT and POR beat Counter Abstraction: Parameterized Model Checking of Threshold-Based Distributed Algorithms";
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.

I. Konnov, H. Veith, J. Widder:
"What You Always Wanted to Know About Model Checking of Fault-Tolerant Distributed Algorithms";
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.

I. Konnov, J. Widder:
"ByMC: Byzantine Model Checker";
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.

T. Kotek, M. Simkus, H. Veith, F. Zuleger:
"Extending ALCQIO with Trees";
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.

T. Kotek, M. Simkus, H. Veith, F. Zuleger:
"Towards a Description Logic for Program Analysis: Extending ALCQIO with Reachability";
Keynote Lecture: International Workshop on Description Logics, Wien; 2014-07-17 - 2014-07-20; in: "International Workshop on Description Logics", (2014), 4 pages.

T. Kotek, H. Veith, F. Zuleger:
"Monadic Second Order Finite Satisfiability and Unbounded Tree-Width";
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.

E. Kotelnikov, L. Kovacs, G. Reger, A. Voronkov:
"The Vampire and the FOOL";
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.

E. Kotelnikov, L. Kovacs, M. Suda, A. Voronkov:
"A Clausal Normal Form Translation for FOOL";
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.

E. Kotelnikov, L. Kovacs, A. Voronkov:
"A FOOLish Encoding of the Next State Relations of Imperative Programs.";
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.

L. Kovacs:
"Automated Reasoning for Systems Engineering";
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.

L. Kovacs:
"First-Order Interpolation and Grey Areas of Proofs";
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.

L. Kovacs:
"Symbolic Computation and Automated Reasoning for Program Analysis";
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.

L. Kovacs, Hanna Lachnitt, S. Szeider:
"Formalizing Graph Trail Properties in Isabelle/HOL";
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.

L. Kovacs, S. Robillard, A. Voronkov:
"Coming to Terms with Quantified Reasoning";
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.

G. Kovasznai, K. Gajdar, L. Kovacs:
"Portfolio SAT and SMT Solving of Cardinality Constraints in Sensor Network Optimization";
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.

G. Kovasznai, H. Veith, A. Fröhlich, A. Biere:
"On the Complexity of Symbolic Verification and Decision Problems in Bit-Vector Logic";
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.

D. Kroening, M. Lewis, G. Weissenbacher:
"Under-Approximating Loops in C Programs for Fast Counterexample Detection";
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.

J. Kukovec, I. Konnov, J. Widder:
"Reachability in Parameterized Systems: All Flavors of Threshold Automata";
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.

A. Laarman, A. Wijs:
"Partial-Order Reduction for Multi-core LTL Model Checking";
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.

N. Labai, M. Homola, M. Ortiz de la Fuente:
"Constructive Satisfiability Procedure for ALCP(Z) (Preliminary Report)";
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.

N. Labai, T. Kotek, M. Ortiz de la Fuente, H. Veith:
"Pebble-Intervals Automata and FO2 with Two Orders";
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.

N. Labai, J. A. Makowsky:
"Logics of Finite Hankel Rank";
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.

N. Labai, M. Simkus, M. Ortiz de la Fuente:
"An ExpTime Upper Bound for ALC with Integers";
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.

M. Lazić, I. Konnov, J. Widder, R. Bloem:
"Synthesis of Distributed Algorithms with Parameterized Threshold Guards";
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.

S. Leue, M. Tabaei Befrouei:
"Mining Sequential Patterns to Explain Concurrent Counterexamples";
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.

L. Leutgeb, G. Moser, F. Zuleger:
"ATLAS: Automated Amortised Complexity Analysis of Self-adjusting Data Structures";
Talk: International Conference on Computer Aided Verification (CAV), virtuell; 2022-07-20 - 2022-07-23; in: "CAV 2021: Computer Aided Verification", (2022), 99 - 122.

M. Lewis, D. Kroening, G. Weissenbacher:
"Proving Safety with Trace Automata and Bounded Model Checking";
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.

P. Metzler, N. Suri, G. Weissenbacher:
"Extracting Safe Thread Schedules from Incomplete Model Checking Results";
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.

M. Moosbrugger, E. Bartocci, J. Katoen, L. Kovacs:
"Automated Termination Analysis of Polynomial Probabilistic Programs";
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.

M. Morak, M. Bichler, S. Woltran:
"lpopt: A Rule Optimization Tool for Answer Set Programming";
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.

J. Pagel, C. Jansen, F. Zuleger, C. Matheja, T. Noll:
"Unified Reasoning About Robustness Properties of Symbolic-Heap Separation Logic";
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.

J. Pagel, D. Jovanovic, G. Weissenbacher:
"A Separation Logic with Data: Small Models and Automation";
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.

J. Pagel, F. Zuleger:
"Strong-Separation Logic";
Talk: 30th European Symposium on Programming (ESOP 2021), Luxembourg (online); 2021-03-27 - 2021-04-01; in: "30th European Symposium on Programming, ESOP 2021", Springer, 12648 (2021), 664 - 692.

T. Pani, G. Weissenbacher, F. Zuleger:
"Rely-Guarantee Reasoning for Automated Bound Analysis of Lock-Free Algorithms";
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.

T. Pani, G. Weissenbacher, F. Zuleger:
"Thread-modular Counter Abstraction for Parameterized Program Safety";
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.

E. Pescosta, G. Weissenbacher, F. Zuleger:
"Bounded Model Checking of Speculative Non-Interference";
Talk: 2021 IEEE/ACM International Conference On Computer Aided Design (ICCAD), München, Deutschland; 2021-11-01 - 2021-11-04; in: "2021 IEEE/ACM International Conference On Computer Aided Design (ICCAD)", IEEE, (2021), ISBN: 978-1-6654-4507-8; 1 - 9.

T. Philipp, A. Rebola Pardo:
"DRAT Proofs for XOR Reasoning";
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.

D. Pötzl, A. Holzer:
"Solving Constraints for Generational Search";
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.

A. Rabinovic, S. Rubin:
"Interpretations in Trees with Countably Many Branches";
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.

I. Radicek, G. Barthe, M. Gaboardi, D. Garg, F. Zuleger:
"Monadic refinements for relational cost analysis";
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.

I. Radicek, S. Gulwani, F. Zuleger:
"Automated clustering and program repair for introductory programming assignments";
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.

N. Razavi, A. Farzan, A. Holzer:
"Bounded-Interference Sequentialization for Testing Concurrent Programs";
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.

A. Rebola Pardo, M. Suda:
"A Theory of Satisfiability-Preserving Proofs in SAT Solving";
Talk: International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), Awassa, Ethiopia; 2018-11-16 - 2018-11-21; in: "International Conference on Logic for Programming, Artificial Intelligence and Reasoning", EasyChair EPiC Series in Computing, 57 / Lpar-22 (2018), 583 - 603.

A. Rebola Pardo, G. Weissenbacher:
"RAT Elimination";
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.

G. Reger, N. Bjorner, M. Suda, A. Voronkov:
"AVATAR Modulo Theories";
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.

G. Reger, M. Suda:
"Checkable Proofs for First-Order Theorem Proving";
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.

G. Reger, M. Suda:
"Set of Support for Theory Reasoning";
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.

G. Reger, M. Suda, A. Voronkov:
"Finding Finite Models in Multi-sorted First-Order Logic";
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.

G. Reger, M. Suda, A. Voronkov:
"New Techniques in Clausal Form Generation";
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.

G. Reger, M. Suda, A. Voronkov:
"Testing a Saturation-Based Theorem Prover: Experiences and Challenges";
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.

G. Reger, M. Suda, A. Voronkov:
"Unification with Abstraction and Theory Instantiation in Saturation-Based Reasoning";
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.

Sagar, P. Fenkam, H. Veith, H. Gall, E. Kirda, S. Jha:
"Integrating Publish/Subscribe into a Mobile Teamwork Support Platform";
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.

M. Samer, H. Veith:
"A Syntactic Characterization of Distributive LTL Queries";
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.

M. Samer, H. Veith:
"Deterministic CTL Query Solving";
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.

M. Samer, H. Veith:
"Parameterized Vacuity";
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.

M. Samer, H. Veith:
"Validity of CTL Queries Revisited";
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.

S. Sastry, L. Welch, J. Widder:
"Wait-Free Stabilizing Dining Using Regular Registers";
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.

S. Sastry, J. Widder:
"Solvability-Based Comparison of Failure Detectors";
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.

M. Schlaipfer, F. Slivovsky, G. Weissenbacher, F. Zuleger:
"Multi-linear Strategy Extraction for QBF Expansion Proofs via Local Soundness";
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.

U. Schmid, A. Steininger, H. Veith:
"Towards a Systematic Design of Fault-Tolerant Asynchronous Circuits";
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.

J. Schoisswohl, L. Kovacs:
"Automating Induction by Reflection";
Talk: 16th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP), Pittsburgh, USA; 2021-07-16; in: "Proceedings of the 16th Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP)", E. Pimentel, E. Tassi (ed.); EPTCS, 337 (2021), 39 - 54.

D. Schwartz-Narbonne, G. Weissenbacher, S. Malik:
"Parallel Assertions for Architectures with Weak Memory Models";
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.

I. Shachar, T. Kotek, N. Rinetzky, M. Sagiv, O. Tamir, H. Veith, F. Zuleger:
"On the Automated Verification of Web Applications with Embedded SQL";
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.

M. Sinn, H. Veith, F. Zuleger:
"Difference Constraints: An adequate Abstraction for Complexity Analysis of Imperative Programs";
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.

M. Sinn, F. Zuleger, H. Veith:
"A Simple and Scalable Static Analysis for Bound Analysis and Amortized Complexity Analysis";
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.

I. Stoilkovska, I. Konnov, J. Widder, F. Zuleger:
"Eliminating Message Counters in Synchronous Threshold Automata";
Talk: 22nd International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), Copenhagen, Denmark; 2021-01-17 - 2021-01-19; in: "Proceedings of the 22nd International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI)", Springer LNCS, 12597 (2021), 196 - 218.

M. Suda:
"Duality in STRIPS planning";
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.

M. Suda, B. Gleiss:
"Local Soundness for QBF Calculi";
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.

M. Tabaei Befrouei:
"Abstraction and mining of traces to explain concurrency bugs";
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.

M. Tabaei Befrouei, C. Wang, G. Weissenbacher:
"Abstraction and Mining of Traces to Explain Concurrency Bugs";
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.

H. Veith:
"Friends or Foes? Communities in Software Verification";
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.

J. P. Wallner, G. Weissenbacher, S. Woltran:
"Advanced SAT Techniques for Abstract Argumentation";
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.

G. Weissenbacher:
"Explaining Heisenbugs";
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.

G. Weissenbacher:
"Interpolant Strength Revisited";
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.

C. Zhu, G. Weissenbacher, S. Malik:
"Silicon fault diagnosis using sequence interpolation with backbones";
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.

F. Zuleger:
"Asymptotically Precise Ranking Functions for Deterministic Size-Change Systems";
Talk: International Computer Science Symposium in Russia (CSR), Listvyanka, Russia; 2015-07-13 - 2015-07-17; in: "CSR", Springer, 9139 (2015), 426 - 442.

F. Zuleger:
"Inductive Termination Proofs with Transition Invariants and Their Relationship to the Size-Change Abstraction";
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.

F. Zuleger, M. Sinn, S. Gulwani, H. Veith:
"Bound Analysis of Imperative Programs with the Size-change Abstraction";
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.


Talks and Poster Presentations (without Proceedings-Entry)


B. Aminof, T. Kotek, S. Rubin, F. Spegni, H. Veith:
"Parameterized Model Checking of Rendezvous Systems";
Talk: Algorithmics of Infinite State Systems workshop, Wien; 2014-07-18.

M. Baaz, T. Eiter, H. Veith:
"Vienna Summer of Logic";
Talk: Vienna Summer of Logic, Wien, Austria (invited); 2014-07-09 - 2014-07-24.

M. Barkatou, M. Jaroschek:
"Desingularization of First Order Linear Difference Systems with Rational Function Coefficients";
Talk: 22nd Conference on Applications of Computer Algebra, Universität Kassel, Kassel, Deutschland; 2016-08-01 - 2016-08-04.

E. Bartocci, L. Kovacs, E. Bura:
"ProbInG: Distribution Recovery for Invariant Generation of Probabilistic Programs";
Talk: Vienna Science, Research and Technology Fund - ProbInG, online; 2020-12-14 - 2020-12-15.

A. Biere, B. Kiesl, M. Seidl, M. Suda:
"Blocked clauses in first-order logic";
Talk: The Third Vampire Workshop, VAMPIRE 2016, Coimbra, Portugal; 2016-07-02.

F. Calimeri, M. Fink, S. Germano, A. Humenberger, G. Ianni, C. Redl, D. Stepanova, A. Tucci:
"AngryHEX: An Angry Birds-playing Agent based on HEX-Programs";
Poster: AngryBirds Competition 2014, Prague, Czech Republic; 2014-08-20 - 2014-08-22.

A. Farzan, A. Holzer, N. Razavi, H. Veith:
"Concolic Testing of Concurrent Programs";
Talk: International Workshop on Exploiting Concurrency Efficiently and Correctly (EC2), Wien; 2014-07-17 - 2014-07-18.

M Függer, J. Widder:
"On Efficient Checking of Link-reversal-based Concurrent Systems";
Talk: PUMA/RISE Seminar, Traunkirchen; 2011-10-03 - 2011-10-07.

P. Georgiou, B. Gleiss, L. Kovacs, M. Maffei:
"Trace Reasoning for Formal Verification using the First-Order Superposition Calculus";
Poster: FMCAD 2019 Student Forum, San Jose, US; 2019-10-22 - 2019-10-25.

B. Gleiss, L. Kovacs, J. Rath:
"Forward Subsumption Demodulation - Fast Conditional Rewriting in Vampire";
Talk: Vampire 2019 - The Sixth Vampire Workshop, Lisbon, Portugal; 2019-07-07.

A. Humenberger, M. Jaroschek, L. Kovacs:
"Polynomial Invariant Generation for Multi-Path Loops";
Talk: Second International Workshop on Satisfiability Checking and Symbolic Computation (SC2), Kaiserslautern, Germany; 2017-07-29.

M. Jaroschek:
"Quantifier Elimination Over The Reals";
Talk: Tutorial on SMT and Polynomial Arithmetic, Chalmers University, Gothenburg, Sweden (invited); 2016-05-26 - 2016-05-27.

M. Jaroschek, M. Barkatou:
"Desingularization of First Order Linear Difference Systems with Rational Function Coefficients";
Talk: RIMS workshop, Algebraic Statistics and Symbolic Computation, RIMS, Kyoto University, Kyoto, Japan (invited); 2016-07-25 - 2016-07-29.

A. John, I. Konnov, U. Schmid, H. Veith, J. Widder:
"Counter Attack against Byzantine Generals";
Talk: Alpine Verification Meeting, Passau, Bayern, Deutschland; 2012-05-21 - 2012-05-22.

A. John, I. Konnov, U. Schmid, H. Veith, J. Widder:
"Parameterized Model Checking of Fault-tolerant Distributed Algorithms";
Talk: Dagstuhl Seminar 12461: Games and Decisions for Rigorous Systems Engineering, Dagstuhl, Deutschland (invited); 2012-11-11 - 2012-11-16.

A. John, I. Konnov, U. Schmid, H. Veith, J. Widder:
"Who is afraid of Model Checking Distributed Algorithms?";
Talk: PUMA/RISE Seminar, Goldegg; 2012-09-24 - 2012-09-28.

B. Kiesl, M. Suda:
"First-Order Logic and Blocked Clauses";
Talk: 4th International Workshop on Quantified Boolean Formulas (QBF 2016), Bordeaux, France; 2016-07-04.

I. Konnov, M. Lazić, H. Veith, J. Widder:
"Parameterized Verification of Liveness of Distributed Algorithms";
Talk: Workshop on Formal Reasoning in Distributed Algorithms (FRiDA), Marrakech, Marocco; 2016-05-17.

I. Konnov, H. Veith, J. Widder:
"Who is afraid of Model Checking Distributed Algorithms?";
Talk: Workshop on Exploiting Concurrency Efficiently and Correctly, Berkeley, CA, USA; 2012-07-07 - 2012-07-08.

T. Kotek:
"Explaining the decompositionality of monadic second order logic using applications to combinatorics";
Talk: Fun With Formal Methods Workshop, Wien; 2014-07-13.

L. Kovacs:
"60 Shades of Grey in Vampire";
Talk: ANDREI-60: Automating New-Era Deductive Reasoning Event in Iberia, Tbilisi, Georgia; 2019-05-19 - 2019-05-23.

L. Kovacs:
"Algebraic Reasoning for Program Analysis";
Keynote Lecture: 33rd Conference on the Mathematical Foundations of Programming Semantics (MFPS), Ljubljana, Slovenia (invited); 2017-06-12 - 2017-06-16.

L. Kovacs:
"APRe, Vampire, Welcome in Vienna!";
Talk: APRe 2019 Workshop, TU Wien, TU Wien, Vienna; 2019-11-05 - 2019-11-06.

L. Kovacs:
"Automated Reasoning for Rigorous Systems Engineering";
Keynote Lecture: RiSE/SHINE Media Seminar 2018, Vienna (invited); 2018-05-07.

L. Kovacs:
"Automated Reasoning for Systems Engineering";
Keynote Lecture: Austrian Computer Science Day 2018, Salzburg (invited); 2016-06-15.

L. Kovacs:
"Automated Reasoning for Systems Engineering";
Keynote Lecture: 2018 IEEE International Conference on Future IoT Technologies (Future IoT 2018), Eger, Hungary (invited); 2018-01-18 - 2018-01-19.

L. Kovacs:
"Enjoying Research at the Intersection of Math and Computer Science";
Keynote Lecture: Women in Science Workshop Series (WISE), Gothenburg, Schweden (invited); 2016-06-08.

L. Kovacs:
"First Order Interpolation";
Keynote Lecture: SAT/SMT/AR Summer School 2019, Lisbon, Portugal (invited); 2019-07-03 - 2019-07-06.

L. Kovacs:
"First-Order Interpolation";
Keynote Lecture: SAT/SMT/AR Summer School 2018, Manchester (invited); 2018-07-03 - 2018-07-06.

L. Kovacs:
"First-Order Interpolation";
Talk: PhD Research Seminar in Logic and Computation, Faculty of Informatics, West University of Timisoara, Timisoara, Romania (invited); 2019-11-29.

L. Kovacs:
"First-Order Interpolation in the Grey Area of Proofs";
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.

L. Kovacs:
"First-Order Theorem Proving and Vampire";
Keynote Lecture: Spring School on Logic and Verification - LoVE, Vienna, Austria (invited); 2016-04-15 - 2016-04-17.

L. Kovacs:
"Formal Methods in the Digital World (in Hungarian)";
Keynote Lecture: JegKepzes Series of Presentations- Hungarian Scientists from the Bartok Bela Highschool, Timisoara, Romania (invited); 2019-11-27.

L. Kovacs:
"Interpolation in the Grey Area of Proofs";
Talk: Helmut Veith Memorial Workshop 2019, Turracher Höhe; 2019-03-17 - 2019-03-20.

L. Kovacs:
"Symbol Elimination and Vampire";
Talk: Dagstuhl Seminar 19062 - Bringing CP, SAT and SMT together: Next Challenges in Constraint Solving, Schloss Dagstuhl, Germany; 2019-02-03 - 2019-02-06.

L. Kovacs:
"Symbol Elimination for Program Analysis";
Keynote Lecture: ETH Workshop on Software Correctness and Reliability, Zürich, Switzerland (invited); 2017-10-13 - 2017-10-14.

L. Kovacs:
"Symbol Elimination for Program Analysis";
Keynote Lecture: Highlights of Logic, Games and Automata, Berlin, Germany (invited); 2018-09-18 - 2018-09-21.

L. Kovacs:
"Symbol Elimination in Program Analysis";
Keynote Lecture: 2nd Facebook Testing and Veri cation Symposium (FaceTAV), London, UK (invited); 2018-11-28 - 2018-11-29.

L. Kovacs:
"Symbolic Computation and Automated Reasoning for Program Analysis";
Keynote Lecture: 23rd IEEE International Conference on Intelligent Engineering Systems (INES) 2019, Gödöllõ, Hungary (invited); 2019-04-25 - 2019-04-27.

L. Kovacs:
"Verifying Relational Properties using Trace Logic";
Talk: First International Workshop on Proof Theory for Automated Deduction, Automated Deduction for Proof Theory, Funchal, Portugal; 2019-10-23 - 2019-10-25.

L. Kovacs:
"With a Timisoara Background in the Scientific World of Computer Science and";
Keynote Lecture: Timisoara Hungarian Science Festival, Timisoara, Romania (invited); 2016-11-26.

L. Kovacs, A. Voronkov:
"First-Order Theorem Proving in Rigorous Systems Engineering";
Keynote Lecture: RiSE/SHiNE Winter School 2018, Wien (invited); 2018-02-05 - 2018-02-09.

G. Kovasznai, H. Veith, A. Fröhlich, A. Biere:
"On the Complexity of Symbolic Verification and Decision Problems in Bit-Vector Logic";
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.

M. Lazić, I. Konnov, H. Veith, J. Widder:
"Model Checking of Threshold-based Fault-Tolerant Distributed Algorithms";
Talk: 7th Workshop on Program Semantics, Specification and Verification: Theory and Applications, St. Petersburg, Russia (invited); 2016-07-14 - 2016-07-15.

J. Rath:
"Subsumption Demodulation in First-Order Theorem Proving";
Talk: First International Workshop on Proof Theory for Automated Deduction, Automated Deduction for Proof Theory, Funchal, Portugal; 2019-10-23 - 2019-10-25.

G. Reger, M. Suda:
"Incremental Solving with Vampire";
Talk: Fourth Vampire Workshop - VAMPIRE 2017, Gothenburg, Sweden; 2017-08-07.

G. Reger, M. Suda:
"Local proofs and AVATAR";
Talk: Fourth Vampire Workshop - VAMPIRE 2017, Gothenburg, Sweden; 2017-08-07.

G. Reger, M. Suda:
"Measuring progress to predict success: Can a good proof strategy be evolved?";
Talk: AITP 2017 - The Second Conference on Artificial Intelligence and Theorem Proving, Obergurgl (invited); 2017-03-26 - 2017-03-30.

G. Reger, M. Suda:
"Revisiting Global Subsumption";
Talk: The Third Vampire Workshop, VAMPIRE 2016, Coimbra, Portugal; 2016-07-02.

G. Reger, M. Suda:
"When Should We Add Theory Axioms And Which Ones?";
Talk: 1st Conference on Artificial Intelligence and Theorem Proving, AITP 2016, Obergurgl; 2016-04-03 - 2016-04-07.

G. Reger, M. Suda, A. Voronkov:
"Instantiation and Pretending to be an SMT Solver with Vampire";
Talk: SMT 2017 - 15th International Workshop on Satisfiability Modulo Theories, Heidelberg, Germany; 2017-07-22 - 2017-07-23.

G. Reger, M. Suda, A. Voronkov:
"New Techniques in Clausal Form Generation";
Talk: Prague Automated Reasoning Seminar, Prague, Czech Republick; 2016-10-31.

G. Reger, M. Suda, A. Voronkov:
"Recent Improvements of Theory Reasoning in Vampire";
Talk: IWIL 2017 - 12th International Workshop on the Implementation of Logics, Maun, Botswana (invited); 2017-05-07.

S. Rubin:
"First Cycle Games";
Talk: Highlights of Logic, Games and Automata, Paris, Frankreich; 2014-09-03 - 2014-09-05.

S. Rubin:
"Parameterised Verification of Robot Protocols: An Automata Theoretic Approach";
Talk: Workshop on Formal Reasoning in Distributed Algorithms (FRiDA), Wien; 2014-07-23 - 2014-07-24.

S. Stankovic:
"Automatic Analysis for Prob-Solvable Loops";
Talk: 13th Alpine Verification Meeting (AVM), Brno, Czech Republic; 2019-09-09 - 2019-09-11.

M. Suda:
"The mystery of QBF tautologies";
Talk: Prague Automated Reasoning Seminar, Prague, Czech Republick; 2016-12-27.

H. Veith:
"History of Model Checking";
Keynote Lecture: Clarke Symposium 2014: Celebrating 25 Years of Model Checking, Pittsburgh, PA, USA (invited); 2014-09-19 - 2014-09-20.

H. Veith:
"How did you specify your test suite?";
Talk: Alpine Verification Meeting, IST Austria; 2011-03-14.

H. Veith:
"Model Checking - Recent Results and Developments";
Talk: University of Leeds, Leeds, United Kingdom; 2002-03-09 - 2002-03-13.

H. Veith:
"Model Checking of Fault-Tolerant Distributed Algorithms";
Talk: Summer School 2014: Verification Technology, Systems & Applications, Luxembourg (invited); 2014-10-27 - 2014-10-31.

H. Veith:
"Secure Two-Party Computation in ANSI C";
Talk: Dagstuhl Seminar 12461: Games and Decisions for Rigorous Systems Engineering, Dagstuhl, Deutschland (invited); 2012-11-11 - 2012-11-16.

H. Veith:
"Verfahren zur Komplexitätsreduktion im Model Checking";
Talk: Universität Saarbrücken, Saarbrücken, Deutschland (invited); 2002-01-02.

H. Veith:
"Verfahren zur Komplexitätsreduktion im Model Checking";
Talk: Technische Universität Graz, Graz, Österreich; 2002-05-06.

H. Veith:
"Verfahren zur Komplexitätsreduktion im Model Checking";
Talk: Technische Universität München, München, Deutschland; 2002-11-27 - 2002-11-28.

G. Weissenbacher:
"Interpolation algorithms and their applications in model checking";
Talk: Automata, Logic and Games, Singapore (invited); 2016-08-29 - 2016-09-02.

G. Weissenbacher:
"Interpolation-based Model Checking and IC3";
Keynote Lecture: Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science, Telč, Czech Republic (invited); 2017-10-13 - 2017-10-15.

G. Weissenbacher:
"Labelled Interpolation Systems";
Talk: Dagstuhl Seminar 12461: Games and Decisions for Rigorous Systems Engineering, Dagstuhl, Deutschland (invited); 2012-11-11 - 2012-11-16.

F. Zuleger:
"Bound Analysis of Imperative Programs with the Size-change Abstraction";
Talk: Microsoft Research Lecture, Microsoft Research Cambridge, UK (invited); 2011-12-01.

F. Zuleger:
"Bound Analysis of Imperative Programs with the Size-change Abstraction";
Talk: Theory Seminar, Queen Mary University, UK (invited); 2011-11-30.

F. Zuleger:
"Bound Analysis of Imperative Programs with the Size-change Abstraction";
Talk: Austrian Society for Rigorous Systems Engineering (ARiSE) workshop together with PUMA workshop, Traunkirchen, Austria; 2011-10-03 - 2011-10-07.

F. Zuleger:
"Bound Analysis of Imperative Programs with the Size-change Abstraction";
Talk: Software Systems Group Seminar, NICTA, Australien; 2011-07-19.

F. Zuleger:
"Resource Bound Analysis of Imperative Programs";
Talk: RiSE Seminar, Klosterneuburg; 2011-05-05.

F. Zuleger:
"Termination and Bound Analysis of Imperative Programs";
Talk: Workshop on Logic and Computer Science, Vienna; 2011-03-24 - 2011-03-25.


Habilitation Theses


G. Weissenbacher:
"Logical Methods in Automated Hardware and Software Verification";
TU Wien/Fakultät für Informatik, 2016.


Doctor's Theses (authored and supervised)


B. Gleiss:
"Automated Software Verification using Superposition-based Theorem Proving";
Supervisor, Reviewer: L. Kovacs, S. Schulz; Institut for Logic and Computation, E192.04, 2020; oral examination: 2020-12-07.

I. Grishchenko:
"Static Analysis of Low-Level Code";
Supervisor, Reviewer: M. Maffei, G. Weissenbacher, A. Sabelfeld, K. Bhargavan; Institut of Logic and Computation, Security and Privacy, 2021; oral examination: 2021-01-25.

A. Holzer:
"Query-Based Test Case Generation";
Supervisor, Reviewer: H. Veith, D. Beyer; Fakultät für Informatik der Technischen Universität Wien, 2013.

A. Humenberger:
"Algebra-based loop reasoning - invariant generation and synthesis for numeric loops";
Supervisor, Reviewer: E. Abraham, J. Worrell; Institute of Logic and Computation, FORSYTE division, 2021; oral examination: 2021-02-08.

S. Katzenbeisser:
"Cryptographic Watermarking";
Supervisor, Reviewer: H. Veith, G. Gottlob; Institut für Informationssysteme, ARGR Datenbanken & Artificial Intelligence, 2004.

M. Samer:
"Reasoning about Specifications in Model Checking";
Supervisor, Reviewer: H. Veith, G. Gottlob; Institut für Informationssysteme, 2004.

Z. G. Saribatur:
"Abstraction for Reasoning about Agent Behavior with Answer Set Programming";
Supervisor, Reviewer: T. Eiter, G. Weissenbacher; Institut für Logic and Computation, 2019; oral examination: 2019-12-17.

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

M. Sinn:
"Automated Complexity Analysis for Imperative Programs";
Supervisor, Reviewer: F. Zuleger, T. Vojnar; Institut für Informationssysteme, 2016.

M. Tabaei Befrouei:
"Effective Error Explanation Techniques for Concurrent Software";
Supervisor, Reviewer: G. Weissenbacher, T. Eiter, R. Majumdar; Informationssysteme, 2016; oral examination: 2016-12-06.

M. Tautschnig:
"Query-Driven Program Testing";
Supervisor, Reviewer: H. Veith, D. Kroening; Institut für Informationssysteme, 2011; oral examination: 2011-04-11.

J. P. Wallner:
"Complexity Results and Algorithms for Argumentation - Dung's Frameworks and Beyond";
Supervisor, Reviewer: S. Woltran, G. Weissenbacher; Institute of Information Systems, 2014; oral examination: 2014-05-28.

F. Zuleger:
"Resource bound analysis of imperative programs";
Supervisor, Reviewer: H. Veith, S. Gulwani; Institut für Informationssysteme, 2011; oral examination: 2011-05-11.


Diploma and Master Theses (authored and supervised)


J. Birgmeier:
"Software Verification with IC3 via Abstraction and Interpolation";
Supervisor: G. Weissenbacher, H. Veith; Fakultät für Informatik der Technischen Universität Wien, 2013.

T. Durand:
"Verifying automotive software components using C model checkers";
Supervisor: G. Weissenbacher, W. Steiner; Logic and Computation, 2020.

P. Georgiou:
"Trace Reasoning in Formal Verification - Guiding Vampire in Induction";
Supervisor: L. Kovacs; Institut for Logic and Computation, E192.04, 2019; final examination: 2019-11-22.

M. Hajdu:
"Automating inductive reasoning with recursive functions";
Supervisor: L. Kovacs; Institut for Logic and Computation, E192.04, FORSYTE division, 2021; final examination: 2021-03-25.

A. Haret:
"Merging in the Horn fragment";
Supervisor: S. Woltran, St. Rümmele; Institut für Informationssysteme, 2014; final examination: 2014-09-23.

C. Hochrainer:
"Automated Reasoning over Arrays in the Superposition Calculus";
Supervisor: L. Kovacs; Institut for Logic and Computation, E192.04, 2020; final examination: 2020-07-21.

H. Lachnitt:
"Formalizing Graph Trail Properties";
Supervisor: L. Kovacs; Institut for Logic and Computation, E192.04, 2020; final examination: 2020-06-04.

M. Moosbrugger:
"Automating Termination Analysis of Probabilistic Programs";
Supervisor: L. Kovacs; Institut for Logic and Computation, E192.04, 2020; final examination: 2020-06-23.

T. Pani:
"Loop Patterns in C Programs";
Supervisor: F. Zuleger, H. Veith; Fakultät für Informatik der Technischen Universität Wien, 2013.

E. Pescosta:
"SpecBMC : bounded model checker for speculative non-interference";
Supervisor: G. Weissenbacher, F. Zuleger; Logic and Computation, 2020.

A. Plaickner:
"Symbolic Model Checking using NUSMV";
Supervisor: H. Veith; Institut für Informationssysteme, 2003.

A. Plaickner:
"Symbolic Model Checking using NUSMV";
Supervisor: H. Veith; Institut für Informationssysteme, 2003.

S. Rain:
"First-Order Reasoning with Aggregates";
Supervisor: L. Kovacs; Institut for Logic and Computation, E192.04, 2020; final examination: 2020-06-18.

J. Rath:
"Subsumption Demodulation in First-Order Theorem Proving";
Supervisor: L. Kovacs; Institut for Logic and Computation, E192.04, 2019; final examination: 2019-10-07.

M. Samer:
"Temporal Logic Queries in Model Checking";
Supervisor: H. Veith; Institut für Informationssysteme, 2002.

J. Schoisswohl:
"Automated induction by reflection";
Supervisor: L. Kovacs; Institut for Logic and Computation, E192.04, FORSYTE division, 2021; final examination: 2021-01-11.


Scientific Reports


M. Bichler, B. Bliem, M. Moldovan, M. Morak, S. Woltran:
"Treewidth-Preserving Modeling in ASP";
Report No. DBAI-TR-2016-97, 2016; 37 pages.

N. Labai, T. Kotek, M. Ortiz de la Fuente, H. Veith:
"Pebble-Intervals Automata and FO2 with Two Orders (Extended Version";
Report for CoRR; Report No. 1912.00171, 2019; 45 pages.

N. Labai, M. Simkus, M. Ortiz de la Fuente:
"An ExpTime Upper Bound for ALC with Integers (Extended Version)";
Report for arXiv; Report No. 2006.02078, 2020; 36 pages.