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.