Publications

Publications

 

2017
[276] Complexity and Resource Bound Analysis of Imperative Programs Using Difference Constraints
Moritz Sinn, Florian Zuleger, Helmut Veith
Journal of Automated Reasoning, pages 1-43, 2017.
[bibtex] [pdf] [doi]
[275] Accuracy of Message Counting Abstraction in Fault-Tolerant Distributed Algorithms
Igor V. Konnov, Josef Widder, Francesco Spegni, Luca Spalazzi
Verification, Model Checking, and Abstract Interpretation - 18th International Conference, VMCAI 2017, Paris, France, January 15-17, 2017, Proceedings, pages 347-366, 2017.
[bibtex] [pdf] [doi]
[274] On the completeness of bounded model checking for threshold-based distributed algorithms: Reachability
Igor V. Konnov, Helmut Veith, Josef Widder
Information and Computation, volume 252, pages 95-109, 2017.
[bibtex] [pdf] [doi]
[273] A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms
Igor V. Konnov, Marijana Lazic, Helmut Veith, Josef Widder
Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, pages 719-734, 2017.
Note: A pre-print including the proofs is available at http://arxiv.org/abs/1608.05327
[bibtex] [pdf]
[272]Para^2: Parameterized Path Reduction, Acceleration, and SMT for Reachability in Threshold-Guarded Distributed Algorithms
Igor Konnov, Marijana Lazic, Helmut Veith, Josef Widder
Formal Methods in System Design, 2017, Springer.
Note: to appear
[bibtex]
[271] Dynamic Reductions for Model Checking Concurrent Software
Henning Günther, Alfons Laarman, Ana Sokolova, Georg Weissenbacher
Verification, Model Checking and Abstract Interpretation (VMCAI), volume 10145 of Lecture Notes in Computer Science, 2017, Springer.
[bibtex] [pdf] [doi]
[270] Empirical software metrics for benchmarking of verification tools
Yulia Demyanova, Thomas Pani, Helmut Veith, Florian Zuleger
Formal Methods in System Design, volume 50, number 2-3, pages 289-316, 2017.
[bibtex] [pdf] [doi]
2016
[269] Abstraction and Mining of Traces to Explain Concurrency Bugs
Mitra Tabaei Befrouei, Chao Wang, Georg Weissenbacher
Formal Methods in Systems Design (FMSD), volume 49, pages 1-32, October 2016, Springer.
[bibtex] [pdf] [doi]
[268] Decidability of Parameterized Verification
Roderick Bloem, Swen Jacobs, Ayrat Khalimov, Igor Konnov, Sasha Rubin, Helmut Veith, Josef Widder
ACM SIGACT News, volume 47, number 2, pages 53-64, jun 2016.
[bibtex] [pdf]
[267] Vienna Verification Tool: IC3 for Parallel Software
Henning Günther, Alfons Laarman, Georg Weissenbacher
TACAS 2016 (Marsha Chechik, Jean-François Raskin, eds.), pages 954-957, 2016, Springer.
[bibtex] [pdf] [doi]
[266] Multi-core On-the-fly SCC Decomposition
Vincent Bloemen, Alfons Laarman, Jaco van de Pol
Proceedings of the 21st ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, pages 8:1-8:12, 2016, ACM.
[bibtex] [pdf]
[265] Parameterized Systems in BIP: Design and Model Checking
Igor Konnov, Tomer Kotek, Qiang Wang, Helmut Veith, Simon Bliudze, Joseph Sifakis
27th International Conference on Concurrency Theory (CONCUR 2016) (Josée Desharnais, Radha Jagadeesan, eds.), volume 59 of Leibniz International Proceedings in Informatics (LIPIcs), pages 30:1-30:16, 2016, Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik.
[bibtex] [pdf]
[264] Tighter Loop Bound Analysis (Technical report)
Pavel Cadek, Jan Strejcek, Marek Trtík
CoRR, volume abs/1605.03636, 2016.
[bibtex] [pdf]
[263] Formal Solutions of Completely Integrable Pfaffian Systems With Normal Crossings
Moulay A. Barkatou, Maximilian Jaroschek, Suzy S. Maddah
Journal of Symbolic Computation, volume to appear, 2016.
[bibtex] [pdf]
[262] A simple and scalable static analysis for bound analysis and amortized complexity analysis
Moritz Sinn, Florian Zuleger, Helmut Veith
Software Engineering 2016, Fachtagung des GI-Fachbereichs Softwaretechnik, 23.-26. Februar 2016, Wien, Österreich, pages 101-102, 2016.
[bibtex] [pdf]
[261] Prompt Alternating-Time Epistemic Logics
Benjamin Aminof, Aniello Murano, Sasha Rubin, Florian Zuleger
Principles of Knowledge Representation and Reasoning: Proceedings of the Fifteenth International Conference, KR 2016, Cape Town, South Africa, April 25-29, 2016., pages 258-267, 2016.
[bibtex] [pdf]
[260]Monadic Second Order Finite Satisfiability and Unbounded Tree-Width
Tomer Kotek, Helmut Veith, Florian Zuleger
25th EACSL Annual Conference on Computer Science Logic, CSL 2016, August 29 - September 1, 2016, Marseille, France, pages 13:1-13:20, 2016.
[bibtex] [doi]
[259] Tighter Loop Bound Analysis
Pavel Cadek, Jan Strejcek, Marek Trtík
Automated Technology for Verification and Analysis - 14th International Symposium, ATVA 2016, Chiba, Japan, October 17-20, 2016, Proceedings, pages 512-527, 2016.
[bibtex] [pdf]
[258] Automatic Verification of Multi-Agent Systems in Parameterised Grid-Environments
Benjamin Aminof, Aniello Murano, Sasha Rubin, Florian Zuleger
Proceedings of the 2016 International Conference on Autonomous Agents & Multiagent Systems, Singapore, May 9-13, 2016, pages 1190-1199, 2016.
[bibtex] [pdf]
[257] Labelled Interpolation Systems for Hyper-Resolution, Clausal, and Local Proofs
Matthias Schlaipfer, Georg Weissenbacher
Journal of Automated Reasoning, 2016, Springer.
[bibtex] [pdf]
[256] DRAT Proofs for XOR Reasoning
Tobias Philipp, Adrian Rebola-Pardo
Logics in Artificial Intelligence (JELIA), pages 415-429, 2016, Springer.
[bibtex] [pdf]
[255] What You Always Wanted to Know About Model Checking of Fault-Tolerant Distributed Algorithms
Igor Konnov, Helmut Veith, Josef Widder
Perspectives of System Informatics: 10th International Andrei Ershov Informatics Conference, PSI 2015, in Memory of Helmut Veith, Kazan and Innopolis, Russia, August 24-27, 2015, Revised Selected Papers (Manuel Mazzara, Andrei Voronkov, eds.), volume 9609 of LNCS, pages 6-21, 2016, Springer International Publishing.
[bibtex] [pdf]
[254] A Short Counterexample Property for Safety and Liveness Verification of Fault-Tolerant Distributed Algorithms
Igor Konnov, Marijana Lazic, Helmut Veith, Josef Widder
arXiv/CoRR, volume 1608.05327, 2016.
Note: (accepted to POPL 2017)
[bibtex] [pdf]
[253] Error Invariants for Concurrent Traces
Andreas Holzer, Daniel Schwartz-Narbonne, Mitra Tabaei Befrouei, Georg Weissenbacher, Thomas Wies
Formal Methods - 21st International Symposium, FM 2016, volume 9995 of Lecture Notes in Computer Science, pages 370-387, 2016, Springer.
[bibtex] [pdf] [doi]
[252] Duality in STRIPS planning
Martin Suda
8th Workshop on Heuristics and Search for Domain-independent Planning (HSDIP), London, UK, June 13, 2016, Proceedings (J. Benton, Daniel Bryce, Michael Katz, Nir Lipovetzky, Christian Muise, Miquel Ramırez, Alvaro Torralba, eds.), pages 21-27, 2016.
[bibtex] [pdf]
[251] New Techniques in Clausal Form Generation
Giles Reger, Martin Suda, Andrei Voronkov
GCAI 2016. 2nd Global Conference on Artificial Intelligence (Christoph Benzm\verb=\="uller, Geoff Sutcliffe, Raul Rojas, eds.), volume 41 of EPiC Series in Computing, pages 11-23, 2016, EasyChair.
[bibtex] [pdf]
[250] A Clausal Normal Form Translation for FOOL
Evgenii Kotelnikov, Laura Kov\verb=\='acs, Martin Suda, Andrei Voronkov
GCAI 2016. 2nd Global Conference on Artificial Intelligence (Christoph Benzm\verb=\="uller, Geoff Sutcliffe, Raul Rojas, eds.), volume 41 of EPiC Series in Computing, pages 53-71, 2016, EasyChair.
[bibtex] [pdf]
[249] AVATAR Modulo Theories
Giles Reger, Nikolaj Bjorner, Martin Suda, Andrei Voronkov
GCAI 2016. 2nd Global Conference on Artificial Intelligence (Christoph Benzm\verb=\="uller, Geoff Sutcliffe, Raul Rojas, eds.), volume 41 of EPiC Series in Computing, pages 39-52, 2016, EasyChair.
[bibtex] [pdf]
[248] Automated Clustering and Program Repair for Introductory Programming Assignments
Sumit Gulwani, Ivan Radicek, Florian Zuleger
CoRR, volume abs/1603.03165, 2016.
[bibtex] [pdf]
[247] Feedback generation for performance problems in introductory programming assignments
Florian Zuleger, Ivan Radicek, Sumit Gulwani
Software Engineering 2016, Fachtagung des GI-Fachbereichs Softwaretechnik, 23.-26. Februar 2016, Wien, Österreich, pages 49-50, 2016.
[bibtex] [pdf]
[246] Empirical software metrics for benchmarking of verification tools
Yulia Demyanova, Thomas Pani, Helmut Veith, Florian Zuleger
Software Engineering 2016, Fachtagung des GI-Fachbereichs Softwaretechnik, 23.-26. Februar 2016, Wien, Österreich, pages 67-68, 2016.
[bibtex] [pdf]
[245] Finding Finite Models in Multi-sorted First-Order Logic
Giles Reger, Martin Suda, Andrei Voronkov
Theory and Applications of Satisfiability Testing - SAT 2016 - 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings (Nadia Creignou, Daniel Le Berre, eds.), volume 9710 of Lecture Notes in Computer Science, pages 323-341, 2016, Springer.
[bibtex] [pdf] [doi]
[244] Lifting QBF Resolution Calculi to DQBF
Olaf Beyersdorff, Leroy Chew, Renate A. Schmidt, Martin Suda
Theory and Applications of Satisfiability Testing - SAT 2016 - 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings (Nadia Creignou, Daniel Le Berre, eds.), volume 9710 of Lecture Notes in Computer Science, pages 490-499, 2016, Springer.
[bibtex] [pdf] [doi]
[243] Selecting the Selection
Krystof Hoder, Giles Reger, Martin Suda, Andrei Voronkov
Automated Reasoning - 8th International Joint Conference, IJCAR 2016, Coimbra, Portugal, June 27 - July 2, 2016, Proceedings (Nicola Olivetti, Ashish Tiwari, eds.), volume 9706 of Lecture Notes in Computer Science, pages 313-329, 2016, Springer.
[bibtex] [pdf] [doi]
2015
[242] Boolean Satisfiability Solvers and Their Applications in Model Checking
Yakir Vizel, Georg Weissenbacher, Sharad Malik
Proceedings of the IEEE, volume 103, number 11, pages 1-15, November 2015, IEEE.
[bibtex] [pdf] [doi]
[241] Empirical Software Metrics for Benchmarking of Verification Tools
Yulia Demyanova, Thomas Pani, Helmut Veith, Florian Zuleger
Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I, pages 561-579, July 2015.
[bibtex] [pdf] [doi]
[240] Under-approximating loops in C programs for fast counterexample detection
Daniel Kroening, Matt Lewis, Georg Weissenbacher
Formal Methods in Systems Design (FMSD), April 2015, Springer.
[bibtex] [pdf] [doi]
[239] Time Complexity of Link Reversal Routing
Bernadette Charron-Bost, Matthias Függer, Jennifer L. Welch, Josef Widder
ACM Trans. Algorithms, volume 11, number 3, pages 18:1-18:39, jan 2015.
[bibtex] [pdf] [doi]
[238] Abstraction and Mining of Traces to Explain Concurrency Bugs
Mitra Tabaei Befrouei
Proceedings of the Young Researchers' Conference "Frontiers of Formal Methods", pages 249-253, 2015, RWTH Aachen, Department of Computer Science.
Note: technical report/summary version of RV14 paper
[bibtex] [pdf]
[237] Decidability of Parameterized Verification
Roderick Bloem, Swen Jacobs, Ayrat Khalimov, Igor Konnov, Sasha Rubin, Helmut Veith, Josef Widder
pages 170, 2015.
[bibtex] [pdf] [doi]
[236] Extending ALCQIO with Trees
Tomer Kotek, Mantas Simkus, Helmut Veith, Florian Zuleger
30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015, Kyoto, Japan, July 6-10, 2015, pages 511-522, 2015.
[bibtex] [pdf] [doi]
[235]Efficient computation of generalized Ising polynomials on graphs with fixed clique-width
Tomer Kotek, Johann A. Makowsky
Topics in Theoretical Computer Science (TTCS), 2015.
[bibtex]
[234]Verification of Asynchronous Mobile-Robots in Partially-Known Environments
Sasha Rubin, Florian Zuleger, Aniello Murano, Benjamin Aminof
PRIMA 2015: Principles and Practice of Multi-Agent Systems - 18th International Conference, Bertinoro, Italy, October 26-30, 2015, Proceedings, volume 9387 of Lecture Notes in Computer Science, pages 185-200, 2015, Springer.
[bibtex] [doi]
[233]On the Expressive Power of Communication Primitives in Parameterised Systems
Benjamin Aminof, Sasha Rubin, Florian Zuleger
Logic for Programming, Artificial Intelligence, and Reasoning - 20th International Conference, LPAR-20 2015, Suva, Fiji, November 24-28, 2015, Proceedings, volume 9450 of Lecture Notes in Computer Science, pages 313-328, 2015, Springer.
[bibtex] [doi]
[232]Liveness of Parameterized Timed Networks
Benjamin Aminof, Sasha Rubin, Florian Zuleger, Francesco Spegni
Automata, Languages, and Programming - 42nd International Colloquium, ICALP 2015, Kyoto, Japan, July 6-10, 2015, Proceedings, Part II, volume 9135 of Lecture Notes in Computer Science, pages 375-387, 2015, Springer.
[bibtex] [doi]
[231]Asymptotically Precise Ranking Functions for Deterministic Size-Change Systems
Florian Zuleger
Computer Science - Theory and Applications - 10th International Computer Science Symposium in Russia, CSR 2015, Listvyanka, Russia, July 13-17, 2015, Proceedings, volume 9139 of Lecture Notes in Computer Science, pages 426-442, 2015, Springer.
[bibtex] [doi]
[230] Logics of Finite Hankel Rank
Nadia Labai, Johann A. Makowsky
Chapter in Fields of Logic and Computation II (Lev D. Beklemishev, Andreas Blass, Nachum Dershowitz, Bernd Finkbeiner, Wolfram Schulte, eds.), volume 9300 of Lecture Notes in Computer Science, pages 237-252, 2015, Springer International Publishing.
[bibtex] [pdf] [doi]
[229]Difference Constraints: An adequate Abstraction for Complexity Analysis of Imperative Programs
Moritz Sinn, Florian Zuleger, Helmut Veith
Formal Methods in Computer-Aided Design (FMCAD) (Roope Kaivola, Thomas Wahl, eds.), pages 144-151, 2015, IEEE.
[bibtex]
[228]A Combined Toolset for the Verification of Real-Time Distributed Systems
D.Yu. Volkanov, V.A. Zakharov, D.A. Zorin, V.V. Podymov, I.V. Konnov
Programming and Computer Software, volume 41, number 6, pages 325-335, 2015.
[bibtex] [doi]
[227] LTSmin: High-Performance Language-Independent Model Checking
Gijs Kant, Alfons Laarman, Jeroen Meijer, Jaco van de Pol, Stefan Blom, Tom van Dijk
Chapter in Tools and Algorithms for the Construction and Analysis of Systems (Christel Baier, Cesare Tinelli, eds.), volume 9035 of Lecture Notes in Computer Science, pages 692-707, 2015, Springer Berlin Heidelberg.
[bibtex] [pdf] [doi]
[226] SMT and POR beat Counter Abstraction: Parameterized Model Checking of Threshold-Based Distributed Algorithms
Igor Konnov, Helmut Veith, Josef Widder
CAV (Part I), volume 9206 of LNCS, pages 85-102, 2015.
[bibtex] [pdf]
[225] Proving Safety with Trace Automata and Bounded Model Checking
Daniel Kroening, Matt Lewis, Georg Weissenbacher
Formal Methods - 20th International Symposium, FM 2015, volume 9109 of Lecture Notes in Computer Science, pages 325-341, 2015, Springer.
[bibtex] [pdf] [doi]
[224] Closure properties and complexity of rational sets of regular languages
Andreas Holzer, Christian Schallhart, Michael Tautschnig, Helmut Veith
Theor. Comput. Sci., volume 605, pages 62-79, 2015.
[bibtex] [pdf] [doi]
[223] Loop Patterns in C Programs
Thomas Pani, Helmut Veith, Florian Zuleger
ECEASST, volume 72, 2015.
[bibtex] [pdf]
[222] Bipartition polynomials, the Ising model and domination in graphs
Markus Dod, Tomer Kotek, James Preen, Peter Tittmann
Discussiones Mathematicae Graph Theory, volume 35, number 2, pages 335-353, 2015.
[bibtex] [pdf]
[221]Compilation for Secure Two-Party Computations
Martin Franz, Andreas Holzer, Stefan Katzenbeisser, Christian Schallhart, Helmut Veith
Software Engineering & Management 2015, Multikonferenz der GI-Fachbereiche Softwaretechnik (SWT) und Wirtschaftsinformatik (WI), FA WI-MAW, 17. März - 20. März 2015, Dresden, Germany (Uwe Aßmann, Birgit Demuth, Thorsten Spitta, Georg Püschel, Ronny Kaiser, eds.), volume 239 of LNI, pages 143-145, 2015, GI.
[bibtex]
[220] Perspectives on White-Box Testing: Coverage, Concurrency, and Concolic Execution
Azadeh Farzan, Andreas Holzer, Helmut Veith
8th IEEE International Conference on Software Testing, Verification and Validation, ICST 2015, Graz, Austria, April 13-17, 2015, pages 1-11, 2015, IEEE.
[bibtex] [pdf] [doi]
2014
[219] On the Complexity of Symbolic Verification and Decision Problems in Bit-Vector Logic
Gergely Kovásznai, Helmut Veith, Andreas Fröhlich, Armin Biere
Proceedings of the 39th International Symposium on Mathematical Foundations of Computer Science (MFCS 2014), volume 8635 of Lecture Notes in Computer Science, pages 481-492, August 2014, Springer.
[bibtex] [pdf]
[218] EPR Encodings of Bit-Vector Problems Even With Quantifiers
Gergely Kovásznai, Andreas Fröhlich, Armin Biere
July 2014, Invited talk at the 1st International Workshop on Quantification (QUANTIFY 2014).
[bibtex] [pdf]
[217] iDQ: Instantiation-Based DQBF Solving
Andreas Fröhlich, Gergely Kovásznai, Armin Biere, Helmut Veith
Proceedings of the 5th International Workshop on Pragmatics of SAT (POS 2014), aff. to SAT 2014, volume 27 of EPiC Series, pages 103-116, July 2014.
[bibtex] [pdf]
[216] Feedback Generation for Performance Problems in Introductory Programming Assignments
Sumit Gulwani, Ivan Radiček, Florian Zuleger
ArXiv e-prints, volume abs/1403.4064, March 2014.
Note: technical report/extended version of FSE14 paper
[bibtex] [pdf]
[215]Parameterized Model Checking of Token-Passing Systems
B. Aminof, S. Jacobs, A. Khalimov, S. Rubin
VMCAI 2014, volume 8318 of LNCS, pages 262-281, jan 2014.
[bibtex]
[214] On the Complexity of Symbolic Verification and Decision Problems in Bit-Vector Logic
Gergely Kovásznai, Helmut Veith, Andreas Fröhlich, Armin Biere
12-13 July 2014, 15th International Workshop on Logic and Computational Complexity and Workshop in Honor of Neil Immerman's 60th Birthday (LCC 2014/ImmermanFest).
[bibtex] [pdf]
[213]First Cycle Games
Sasha Rubin
2014, Highlights of Logic, Games and Automata.
[bibtex]
[212]Parameterised Verification of Robot Protocols: An Automata Theoretic Approach
Sasha Rubin
2014, FRIDA Workshop (FLoC 2014).
[bibtex]
[211]Explaining the decompositionality of monadic second order logic using applications to combinatorics
Tomer Kotek
2014, Fun With Formal Methods Workshop (FLoC 2014).
[bibtex]
[210]Towards a Description Logic for Program Analysis: Extending ALCQIO with Reachability
Tomer Kotek, Mantas Simkus, Helmut Veith, Florian Zuleger
Informal Proceedings of the 27th International Workshop on Description Logics, Vienna, Austria, July 17-20, 2014., pages 591-594, 2014.
[bibtex]
[209]Shape and Content: Incorporating Domain Knowledge into Shape Analysis
Diego Calvanese, Tomer Kotek, Mantas Simkus, Helmut Veith, Florian Zuleger
Informal Proceedings of the 27th International Workshop on Description Logics, Vienna, Austria, July 17-20, 2014., pages 124-127, 2014.
[bibtex]
[208]Parameterized Model Checking of Rendezvous Systems
Benjamin Aminof, Tomer Kotek, Sasha Rubin, Francesco Spegni, Helmut Veith
2014, Algorithmics of Infinite State Systems workshop (FLoC 2014).
[bibtex]
[207] Parameterized Model Checking of Rendezvous Systems
Benjamin Aminof, Tomer Kotek, Sasha Rubin, Francesco Spegni, Helmut Veith
Chapter in CONCUR 2014 – Concurrency Theory (Paolo Baldan, Daniele Gorla, eds.), volume 8704 of Lecture Notes in Computer Science, pages 109-124, 2014, Springer Berlin Heidelberg.
[bibtex] [pdf] [doi]
[206]Connection Matrices and the Definability of Graph Parameters
Tomer Kotek, Johann A. Makowsky
Logical Methods in Computer Science, volume 10, number 4, 2014.
[bibtex]
[205] Recurrence Relations for Graph Polynomials on Bi-iterative Families of Graphs
Tomer Kotek, Johann A Makowsky
European Journal of Combinatorics, volume 41, pages 47-67, 2014.
Comment: [arXiv]
[bibtex] [pdf]
[204]Silicon Fault Diagnosis Using Sequence Interpolation with Backbones
Charlie Shucheng Zhu, Georg Weissenbacher, Sharad Malik
International Conference on Computer-Aided Design (ICCAD), 2014, IEEE/ACM.
[bibtex]
[203]Abstraction and Mining of Traces to Explain Concurrency Bugs
Mitra Tabaei Befrouei, Chao Wang, Georg Weissenbacher
Runtime Verification Symposium, 2014, Springer Berlin Heidelberg.
[bibtex]
[202] A Simple and Scalable Static Analysis for Bound Analysis and Amortized Complexity Analysis
Moritz Sinn, Florian Zuleger, Helmut Veith
Chapter in Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings, pages 745-761, 2014.
[bibtex] [pdf] [doi]
[201] Solvability-Based Comparison of Failure Detectors
Srikanth Sastry, Josef Widder
IEEE NCA14, pages 269-276, 2014.
[bibtex] [pdf]
[200] Partial-Order Reduction for Multi-core LTL Model Checking
Alfons Laarman, Anton Wijs
Chapter in Hardware and Software: Verification and Testing (Eran Yahav, ed.), volume 8855 of Lecture Notes in Computer Science, pages 267-283, 2014, Springer International Publishing.
[bibtex] [pdf] [doi]
[199] Guard-based partial-order reduction
Alfons Laarman, Elwin Pater, Jaco van de Pol, Henri Hansen
International Journal on Software Tools for Technology Transfer, pages 1-22, 2014, Springer Berlin Heidelberg.
[bibtex] [pdf] [doi]
[198]A Representation Theorem for (q-)Holonomic Sequences
T. Kotek, J. A. Makowsky
Journal of Computer System Sciences, volume 80, pages 363-374, 2014.
Comment: [pdf]
[bibtex]
[197]How to Make a Simple Tool for Verification of Real-Time Systems
I.V. Konnov, V.V. Podymov, D.Yu. Volkanov, V.A. Zakharov, D.A. Zorin
Automatic Control and Computer Sciences, volume 48, number 7, pages 534-542, 2014, Allerton Press.
[bibtex] [doi]
[196] On the Completeness of Bounded Model Checking for Threshold-Based Distributed Algorithms: Reachability
Igor Konnov, Helmut Veith, Josef Widder
Chapter in CONCUR 2014 --- Concurrency Theory (Paolo Baldan, Daniele Gorla, eds.), volume 8704 of Lecture Notes in Computer Science, pages 125-140, 2014.
[bibtex] [pdf]
[195] Feedback Generation for Performance Problems in Introductory Programming Assignments
Sumit Gulwani, Ivan Radiček, Florian Zuleger
Proceedings of the 22Nd ACM SIGSOFT International Symposium on Foundations of Software Engineering, pages 41-51, 2014, ACM.
[bibtex] [pdf] [doi]
[194] Incremental Bounded Software Model Checking
Henning Günther, Georg Weissenbacher
SPIN, pages 40-47, 2014, ACM.
[bibtex] [pdf]
[193] Tutorial on Parameterized Model Checking of Fault-Tolerant Distributed Algorithms
Annu Gmeiner, Igor Konnov, Ulrich Schmid, Helmut Veith, Josef Widder
Formal Methods for Executable Software Models, pages 122-171, 2014, Springer.
[bibtex] [pdf]
[192] CBMC-GC: An ANSI C Compiler for Secure Two-Party Computations
Martin Franz, Andreas Holzer, Stefan Katzenbeisser, Christian Schallhart, Helmut Veith
Compiler Construction - 23rd International Conference, CC 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014. Proceedings (Albert Cohen, ed.), volume 8409 of Lecture Notes in Computer Science, pages 244-249, 2014, Springer.
[bibtex] [pdf] [doi]
[191]Concolic Testing of Concurrent Programs
Azadeh Farzan, Andreas Holzer, Niloofar Razavi, Helmut Veith
2014, CAV Workshop (EC)\^2.
[bibtex]
[190] A Logic-based Framework for Verifying Consensus Algorithms
Cezara Drăgoi, Thomas A. Henzinger, Helmut Veith, Josef Widder, Damien Zufferey
VMCAI, volume 8318 of LNCS, pages 161-181, 2014.
[bibtex] [pdf]
[189]Concolic Testing of Concurrent Programs
Azadeh Farzan, Andreas Holzer, Niloofar Razavi, Helmut Veith
Software Engineering 2014, Fachtagung des GI-Fachbereichs Softwaretechnik, 25. Februar - 28. Februar 2014, Kiel, Deutschland, pages 101-102, 2014.
[bibtex]
[188]Reusing Information in Multi-Goal Reachability Analyses
Dirk Beyer, Andreas Holzer, Michael Tautschnig, Helmut Veith
Software Engineering 2014, Fachtagung des GI-Fachbereichs Softwaretechnik, 25. Februar - 28. Februar 2014, Kiel, Deutschland, pages 97-98, 2014.
[bibtex]
[187] Size-Change Abstraction and Max-Plus Automata
Thomas Colcombet, Laure Daviaud, Florian Zuleger
Mathematical Foundations of Computer Science 2014 - 39th International Symposium, MFCS 2014, Budapest, Hungary, August 25-29, 2014. Proceedings, Part I, pages 208-219, 2014.
[bibtex] [pdf] [doi]
[186] Shape and Content - A Database-Theoretic Perspective on the Analysis of Data Structures
Diego Calvanese, Tomer Kotek, Mantas Simkus, Helmut Veith, Florian Zuleger
Integrated Formal Methods - 11th International Conference, IFM 2014, Bertinoro, Italy, September 9-11, 2014, Proceedings, pages 3-17, 2014.
[bibtex] [pdf] [doi]
[185] An Open Alternative for SMT-Based Verification of Scade Models
Henning Basold, Henning Günther, Michaela Huhn, Stefan Milius
Formal Methods for Industrial Critical Systems - 19th International Conference, FMICS 2014, Florence, Italy, September 11-12, 2014. Proceedings, pages 124-139, 2014.
[bibtex] [pdf] [doi]
[184] Reduction of Resolution Refutations and Interpolants via Subsumption
Roderick Bloem, Sharad Malik, Matthias Schlaipfer, Georg Weissenbacher
Chapter in Hardware and Software: Verification and Testing (Eran Yahav, ed.), volume 8855 of Lecture Notes in Computer Science, pages 188-203, 2014, Springer International Publishing.
[bibtex] [pdf] [doi]
[183]Counterexample to Induction-Guided Abstraction-Refinement (CTIGAR)
Johannes Birgmeier, Aaron Bradley, Georg Weissenbacher
Computer Aided Verification, volume 8559 of Lecture Notes in Computer Science, pages 829-846, 2014, Springer Berlin Heidelberg.
[bibtex]
[182]Cycle Games
B. Aminof, S. Rubin
SR2014, 2014.
[bibtex]
2013
[181] On the Concept of Variable Roles and its Use in Software Analysis
Yulia Demyanova, Helmut Veith, Florian Zuleger
ArXiv e-prints, volume abs/1305.6745, May 2013.
[bibtex] [pdf]
[180] Mining Sequential Patterns to Explain Concurrent Counterexamples
Stefan Leue, Mitra Tabaei Befrouei
SPIN, volume 7976 of LNCS, pages 264-281, 2013.
[bibtex] [pdf]
[179] Challenges in Compiler Construction for Secure Two-Party Computation
Andreas Holzer, Nikolaos P. Karvelas, Stefan Katzenbeisser, Helmut Veith, Martin Franz
(Martin Franz, Andreas Holzer, Rupak Majumdar, Bryan Parno, Helmut Veith, eds.), pages 3-6, 2013, ACM.
[bibtex] [pdf] [doi]
[178]Ramsey vs. Lexicographic Termination Proving
Byron Cook, Abigail See, Florian Zuleger
TACAS, pages 47-61, 2013.
[bibtex]
[177] Formal Verification of Distributed Algorithms (Dagstuhl Seminar 13141)
Bernadette Charron-Bost, Stephan Merz, Andrey Rybalchenko, Josef Widder
Dagstuhl Reports (Bernadette Charron-Bost, Stepahn Merz, Andrey Rybalchenko, Josef Widder, eds.), volume 3, number 4, pages 1-16, 2013, Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik.
[bibtex] [pdf] [doi]
[176]Advanced SAT Techniques for Abstract Argumentation
Johannes Peter Wallner, Georg Weissenbacher, Stefan Woltran
Chapter in Computational Logic in Multi-Agent Systems (João Leite, Tran Cao Son, Paolo Torroni, Leon Torre, Stefan Woltran, eds.), volume 8143 of Lecture Notes in Computer Science, pages 138-154, 2013, Springer Berlin Heidelberg.
[bibtex] [doi]
[175]Under-Approximating Loops in C Programs for Fast Counterexample Detection
Daniel Kroening, Matt Lewis, Georg Weissenbacher
Chapter in Computer Aided Verification (Natasha Sharygina, Helmut Veith, eds.), volume 8044 of Lecture Notes in Computer Science, pages 381-396, 2013, Springer Berlin Heidelberg.
[bibtex] [doi]
[174] Parameterized model checking of fault-tolerant distributed algorithms by abstraction
Annu John, Igor Konnov, Ulrich Schmid, Helmut Veith, Josef Widder
FMCAD, pages 201-209, 2013.
[bibtex] [pdf]
[173] Towards Modeling and Model Checking Fault-Tolerant Distributed Algorithms
Annu John, Igor Konnov, Ulrich Schmid, Helmut Veith, Josef Widder
SPIN, volume 7976 of LNCS, pages 209-226, 2013.
[bibtex] [pdf]
[172] On the Structure and Complexity of Rational Sets of Regular Languages
Andreas Holzer, Christian Schallhart, Michael Tautschnig, Helmut Veith
IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2013, December 12-14, 2013, Guwahati, India (Anil Seth, Nisheeth K. Vishnoi, eds.), volume 24 of LIPIcs, pages 377-388, 2013, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik.
[bibtex] [pdf] [doi]
[171] An experience on using simulation environment DYANA augmented with UPPAAL for verification of embedded systems defined by UML statecharts
Alevtina B. Glonina, Igor Konnov, Vladislav V. Podymov, Dmitry Yu. Volkanov, Vladimir A. Zakharov, Daniil A. Zorin
2013, CAV Workshop VES13.
[bibtex] [pdf]
[170]PETShop'13, Proceedings of the 2013 ACM Workshop on Language Support for Privacy-Enhancing Technologies, Co-located with CCS 2013, November 4, 2013, Berlin, Germany
(Martin Franz, Andreas Holzer, Rupak Majumdar, Bryan Parno, Helmut Veith, eds.), 2013, ACM.
[bibtex]
[169] On the Concept of Variable Roles and its Use in Software Analysis
Yulia Demyanova, Helmut Veith, Florian Zuleger
FMCAD, pages 226-229, 2013.
[bibtex] [pdf]
[168] On the Structure and Complexity of Rational Sets of Regular Languages
Andreas Holzer, Christian Schallhart, Michael Tautschnig, Helmut Veith
CoRR, volume abs/1305.6074, 2013.
[bibtex] [pdf]
[167]Solving Constraints for Generational Search
Daniel Pötzl, Andreas Holzer
Tests and Proofs - 7th International Conference, TAP 2013, Budapest, Hungary, June 16-20, 2013. Proceedings (Margus Veanes, Luca Viganò, eds.), volume 7942 of Lecture Notes in Computer Science, pages 197-213, 2013, Springer.
[bibtex]
[166] Con2colic testing
Azadeh Farzan, Andreas Holzer, Niloofar Razavi, Helmut Veith
Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering, ESEC/FSE'13, Saint Petersburg, Russian Federation, August 18-26, 2013 (Bertrand Meyer, Luciano Baresi, Mira Mezini, eds.), pages 37-47, 2013, ACM.
[bibtex] [pdf] [doi]
[165] Brief announcement: parameterized model checking of fault-tolerant distributed algorithms by abstraction
Annu John, Igor Konnov, Ulrich Schmid, Helmut Veith, Josef Widder
PODC, pages 119-121, 2013.
[bibtex] [pdf]
[164] Information Reuse for Multi-goal Reachability Analyses
Dirk Beyer, Andreas Holzer, Michael Tautschnig, Helmut Veith
ESOP, pages 472-491, 2013.
[bibtex] [pdf] [doi]
[163] The first workshop on language support for privacy-enhancing technologies (PETShop'13)
Martin Franz, Andreas Holzer, Rupak Majumdar, Bryan Parno, Helmut Veith
ACM Conference on Computer and Communications Security (Ahmad-Reza Sadeghi, Virgil D. Gligor, Moti Yung, eds.), pages 1485-1486, 2013, ACM.
[bibtex] [pdf] [doi]
[162] PETShop'13, Proceedings of the 2013 ACM Workshop on Language Support for Privacy-Enhancing Technologies, Co-located with CCS 2013, November 4, 2013, Berlin, Germany
(Martin Franz, Andreas Holzer, Rupak Majumdar, Bryan Parno, Helmut Veith, eds.), 2013, ACM.
[bibtex] [pdf]
[161] Verification across Intellectual Property Boundaries
Sagar Chaki, Christian Schallhart, Helmut Veith
ACM Trans. Softw. Eng. Methodol., volume 22, number 2, pages 15, 2013.
[bibtex] [pdf]
[160] Link Reversal Routing with Binary Link Labels: Work Complexity
Bernadette Charron-Bost, Antoine Gaillard, Jennifer Welch, Josef Widder
SIAM Journal on Computing, volume 42, number 2, pages 634-661, 2013.
[bibtex] [pdf]
[159] Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings
(Natasha Sharygina, Helmut Veith, eds.), volume 8044 of Lecture Notes in Computer Science, 2013, Springer.
[bibtex] [pdf]
[158] Cube-and-Conquer Approach for SAT Solving on Grids
Csaba Biró, Gergely Kovásznai, Armin Biere, Gábor Kusper, Gábor Geda
Annales Mathematicae et Informaticae, volume 42, pages 9-21, 2013.
[bibtex] [pdf]
2012
[157] Wait-Free Stabilizing Dining Using Regular Registers
Srikanth Sastry, Jennifer L. Welch, Josef Widder
OPODIS, volume 7702 of LNCS, pages 284-299, December 2012, Springer.
[bibtex] [pdf]
[156]Vinter: A Vampire-Based Tool for Interpolation
Kryštof Hoder, Andreas Holzer, Laura Kovács, Andrei Voronkov
APLAS, December 2012, Springer.
[bibtex]
[155]Coverage-based Trace Signal Selection for Fault Localisation in Post-Silicon Validation
Charlie Shucheng Zhu, Georg Weissenbacher, Sharad Malik
Haifa Verification Conference (HVC) (Armin Biere, Tanja E. J. Vos, Amir Nahir, eds.), November 2012, Springer.
[bibtex]
[154] Starting a Dialog between Model Checking and Fault-tolerant Distributed Algorithms
Annu John, Igor Konnov, Ulrich Schmid, Helmut Veith, Josef Widder
ArXiv e-prints, October 2012.
[bibtex] [pdf]
[153] Counter Attack on Byzantine Generals: Parameterized Model Checking of Fault-tolerant Distributed Algorithms
Annu John, Igor Konnov, Ulrich Schmid, Helmut Veith, Josef Widder
ArXiv e-prints, October 2012.
[bibtex] [pdf]
[152] Interpolant Strength Revisited
Georg Weissenbacher
Theory and Applications of Satisfiability Testing (SAT) (Alessandro Cimatti, Roberto Sebastiani, eds.), volume 7317 of Lecture Notes in Computer Science, pages 312-326, 2012, Springer.
[bibtex] [pdf] [doi]
[151] Parallel Assertions for Architectures with Weak Memory Models
Daniel Schwartz-Narbonne, Georg Weissenbacher, Sharad Malik
Automated Technology for Verification and Analysis (ATVA) (Supratik Chakraborty, Madhavan Mukund, eds.), pages 254-268, 2012, Springer.
[bibtex] [pdf] [doi]
[150] Consensus in the presence of mortal Byzantine faulty processes
Josef Widder, Martin Biely, Günther Gridling, Bettina Weiss, Jean-Paul Blanquart
Distributed Computing, volume 24, number 6, pages 299-321, 2012.
[bibtex] [pdf]
[149] Special Issue: Games in Verification
Helmut Veith
J. Comput. Syst. Sci., volume 78, number 2, pages 393, 2012.
[bibtex] [pdf]
[148]Interpretations in Trees with Countably Many Branches
Alexander Rabinovich, Sasha Rubin
LICS, pages 551-560, 2012.
[bibtex]
[147] Who is afraid of Model Checking Distributed Algorithms?
Igor Konnov, Helmut Veith, Josef Widder
2012, CAV Workshop (EC)\^2.
[bibtex] [pdf]
[146]A Myhill-Nerode theorem for automata with advice
Alex Kruckman, Sasha Rubin, John Sheridan, Ben Zax
GandALF, pages 238-246, 2012.
[bibtex]
[145] Parameterized Model Checking by Network Invariants: the Asynchronous Case
Igor Konnov
2012, LICS Workshop AISS.
[bibtex] [pdf]
[144] Efficient Checking of Link-Reversal-Based Concurrent Systems
Matthias Függer, Josef Widder
CONCUR, volume 7454 of LNCS, pages 486-499, 2012.
[bibtex] [pdf]
[143] Selected Papers of the Conference "Computer Science Logic CSL 2010": Preface
Anuj Dawar, Helmut Veith
Logical Methods in Computer Science, 2012.
[bibtex] [pdf]
[142] Proving Reachability Using FShell - (Competition Contribution)
Andreas Holzer, Daniel Kroening, Christian Schallhart, Michael Tautschnig, Helmut Veith
TACAS, volume 7214 of Lecture Notes in Computer Science, pages 538-541, 2012, Springer.
[bibtex] [pdf]
[141] Bounded-Interference Sequentialization for Testing Concurrent Programs
Niloofar Razavi, Azadeh Farzan, Andreas Holzer
ISoLA (1), volume 7609 of LNCS, pages 372-387, 2012.
[bibtex] [pdf]
[140] Secure Two-party Computations in ANSI C
Andreas Holzer, Martin Franz, Stefan Katzenbeisser, Helmut Veith
ACM Conference on Computer and Communications Security, pages 772-783, 2012.
[bibtex] [pdf]
2011
[139]An Introduction to Test Specification in FQL
Andreas Holzer, Christian Schallhart, Michael Tautschnig, Helmut Veith
Proceedings of 6th International Haifa Verification Conference (HVC 2011) (Sharon Barner, Ian G. Harris, Daniel Kroening, Orna Raz, eds.), volume 6504 of Lecture Notes in Computer Science, pages 9-22, October 2011, Springer.
[bibtex]
[138]Seamless Testing for Models and Code
Andreas Holzer, Visar Januzaj, Stefan Kugele, Boris Langer, Christian Schallhart, Michael Tautschnig, Helmut Veith
Proceedings of 14th International Conference on Fundamental Approaches to Software Engineering (FASE 2011), volume 6603 of Lecture Notes in Computer Science, pages 278-293, April 2011, Springer.
[bibtex]
[137]Improving the Confidence in Measurement-Based Timing Analysis
Sven Bünte, Raimund Kirner, Michael Zolda, Michael Tautschnig
2011 IEEE International Symposium on Object/Component/Service-Oriented Real-Time Distributed Computing, ISORC 2011, March 2011, IEEE Computer Society.
Note: To appear.
[bibtex]
[136] Bound analysis of imperative programs with the size-change abstraction
Florian Zuleger, Sumit Gulwani, Moritz Sinn, Helmut Veith
Proceedings of the 18th international conference on Static analysis, pages 280-297, 2011, Springer-Verlag.
[bibtex] [pdf]
2010
[135]Timely Time Estimates
Andreas Holzer, Visar Januzaj, Stefan Kugele, Michael Tautschnig
Proceedings of 4th International Symposium on Leveraging Applications (ISoLA 2010) (Tiziana Margaria, Bernhard Steffen, eds.), volume 6415 of Lecture Notes in Computer Science, pages 33-46, October 2010, Springer.
[bibtex] [doi]
[134]Seamless Model-driven Development put into Practice
Wolfgang Haberl, Markus Herrmannsdoerfer, Stefan Kugele, Michael Tautschnig, Martin Wechs
Proceedings of 4th International Symposium on Leveraging Applications (ISoLA 2010) (Tiziana Margaria, Bernhard Steffen, eds.), volume 6415 of Lecture Notes in Computer Science, pages 18-32, October 2010, Springer.
[bibtex] [doi]
[133]Precise Static Analysis of Untrusted Driver Binaries
Johannes Kinder, Helmut Veith
Proceedings of the 10th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2010) (Roderick Bloem, Natasha Sharygina, eds.), pages 43-50, October 2010.
[bibtex]
[132]How did you specify your test suite ?
Andreas Holzer, Christian Schallhart, Michael Tautschnig, Helmut Veith
Proceedings of the 25th IEEE/ACM International Conference on Automated Software Engineering (ASE 2010), pages 407-416, September 2010, ACM.
[bibtex]
[131]Model-Based Generation of Fault-Tolerant Embedded Systems
Wolfgang Haberl, Stefan Kugele, Uwe Baumgarten
Proceedings of the 2010 International Conference on Embedded Systems and Applications, ESA 2010 (Hamid R. Arabnia, Ashu M. G. Solo, eds.), pages 136-142, July 2010, CSREA Press.
[bibtex]
[130]Proving Memory Safety of Floating-Point Computations by Combining Static and Dynamic Program Analysis
Patrice Godefroid, Johannes Kinder
International Symposium on Software Testing and Analysis (ISSTA'10), pages 1-12, July 2010, ACM.
[bibtex]
[129]On the Distributivity of LTL Specifications
Marko Samer, Helmut Veith
ACM Transactions on Computational Logic (TOCL), volume 11, number 3, May 2010, ACM.
[bibtex]
[128]Constraint Satisfaction with Bounded Treewidth Revisited
Marko Samer, Stefan Szeider
Journal of Computer and System Sciences (JCSS), volume 76, number 2, pages 103-114, March 2010, Academic Press.
[bibtex] [doi]
[127]Algorithms for Propositional Model Counting
Marko Samer, Stefan Szeider
Journal of Discrete Algorithms (JDA), volume 8, number 1, pages 50-64, March 2010, Elsevier.
[bibtex] [doi]
[126]Don't care in SMT---Building flexible yet efficient abstraction/refinement solvers
Andreas Bauer, Martin Leucker, Christian Schallhart, Michael Tautschnig
International Journal on Software Tools for Technology Transfer, volume 12, number 1, pages 23-37, February 2010.
[bibtex] [doi]
[125]Proactive Detection of Computer Worms Using Model Checking
Johannes Kinder, Stefan Katzenbeisser, Christian Schallhart, Helmut Veith
IEEE Transactions on Dependable and Secure Computing, volume 7, number 4, pages 424-438, October-December 2010.
[bibtex]
[124]Loopus - A Tool for Computing Loop Bounds for C Programs
Florian Zuleger, Moritz Sinn
Proceedings of the 3rd Workshop on Invariant Generation (WING), 2010.
[bibtex]
[123]Semantic Integrity in Large-Scale Online Simulations
Somesh Jha, Stefan Katzenbeisser, Christian Schallhart, Helmut Veith, Stephen Chenney
ACM Transactions on Internet Technology (TOIT), 2010.
Note: accepted for publication
[bibtex]
[122]The reachability-bound problem
Sumit Gulwani, Florian Zuleger
PLDI, pages 292-304, 2010.
[bibtex]
[121]Runtime Verification for LTL and TLTL
Andreas Bauer, Martin Leucker, Christian Schallhart
ACM Transactions on Software and Methodology (TOSEM), 2010.
Note: accepted for publication
[bibtex]
[120]Comparing LTL Semantics for Runtime Verification
Andreas Bauer, Martin Leucker, Christian Schallhart
Journal of Logic and Computation (JLC), 2010.
Note: accepted for publication
[bibtex] [doi]
2009
[119]Slope Testing for Activity Diagrams and Safety Critical Software
Andreas Holzer, Visar Januzaj, Stefan Kugele, Christian Schallhart, Michael Tautschnig, Helmut Veith, Boris Langer
October 2009, Technical report, Technische Universität Darmstadt.
[bibtex] [pdf]
[118]An Application of Data Mining to Identify Data Quality Problems
Eshref Januzaj, Visar Januzaj
Proceedings of the Third International Conference on Advanced Engineering Computing and Applications in Sciences, ADVCOMP 2009, October 2009, IEEE Computer Society.
[bibtex]
[117]A Precise Specification Framework for White Box Program Testing
Andreas Holzer, Christian Schallhart, Michael Tautschnig, Helmut Veith
September 2009, Technical report, Technische Universität Darmstadt.
[bibtex] [pdf]
[116]Encoding Treewidth into SAT
Marko Samer, Helmut Veith
Proceedings of the 12th International Conference on Theory and Applications of Satisfiability Testing (SAT'09) (Oliver Kullmann, ed.), volume 5584 of Lecture Notes in Computer Science, pages 45-50, July 2009, Springer-Verlag.
[bibtex] [doi]
[115]Short Regular Expressions from Finite Automata: Empirical Results
Hermann Gruber, Markus Holzer, Michael Tautschnig
Proceedings of the 14th International Conference on Implementation and Application of Automata (CIAA 2009), volume 5642 of Lecture Notes in Computer Science, pages 188-197, July 2009, Springer.
[bibtex]
[114]Model Analysis via a Translation Schema to Coloured Petri Nets
Visar Januzaj, Stefan Kugele
Proceedings of the International Workshop on Petri Nets and Software Engineering, PNSE '09 (D. Moldt, ed.), pages 273-292, June 2009.
[bibtex]
[113]Generating Distributed Code From COLA Models
Wolfgang Haberl, Michael Tautschnig, Uwe Baumgarten
Chapter in 20, volume 33 of Lecture Notes in Electrical Engineering, March 2009, Springer.
[bibtex]
[112]Performance Modelling for Avionics Systems
Visar Januzaj, Ralf Mauersberger, Florian Biechele
12th International Conference on Computer Aided Systems Theory - EUROCAST 2009, volume 5717 of Lecture Notes in Computer Science, pages 833-840, February 2009, Springer.
[bibtex]
[111]Fixed-Parameter Tractability
Marko Samer, Stefan Szeider
Chapter in Handbook of Satisfiability (A. Biere, M. Heule, H. van Maaren, T. Walsh, eds.), volume 185 of Frontiers in Artificial Intelligence and Applications, pages 425-454, February 2009, IOS Press.
[bibtex] [doi]
[110]Backdoor Sets of Quantified Boolean Formulas
Marko Samer, Stefan Szeider
Journal of Automated Reasoning (JAR), volume 42, number 1, pages 77-97, January 2009.
[bibtex] [doi]
[109]Query-Driven Program Testing
Andreas Holzer, Christian Schallhart, Michael Tautschnig, Helmut Veith
Proceedings of the Tenth International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2009) (Neil D. Jones, Markus Müller-Olm, eds.), volume 5403 of Lecture Notes in Computer Science, pages 151-166, January 2009, Springer.
[bibtex]
[108]An Abstract Interpretation-Based Framework for Control Flow Reconstruction from Binaries
Johannes Kinder, Florian Zuleger, Helmut Veith
Proceedings of the Tenth International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2009) (Neil D. Jones, Markus Müller-Olm, eds.), volume 5403 of Lecture Notes in Computer Science, January 2009, Springer.
[bibtex]
[107]A Brief Account of Runtime Verification
Martin Leucker, Christian Schallhart
Journal of Logic and Algebraic Programming (JLAP), number 78, pages 293-303, 2009.
[bibtex]
[106]Towards Resource Consumption-Aware Programming
Andreas Holzer, Visar Januzaj, Stefan Kugele
, volume 0, pages 490-493, 2009, IEEE Computer Society.
[bibtex] [doi]
[105]Reliable Operating Modes for Distributed Embedded Systems
Wolfgang Haberl, Stefan Kugele, Uwe Baumgarten
Proceedings of the 6th International Workshop on Model-based Methodologies for Pervasive and Embedded Software, 2009, IEEE Computer Society.
[bibtex]
[104]One Click from Model to Reality
Wolfgang Haberl, Markus Herrmannsdoerfer, Stefan Kugele, Michael Tautschnig, Martin Wechs
Proceedings of Symposium on Automotive/Avionics Systems Engineering (SAASE 2009), 2009.
[bibtex]
[103]Dependency Coverage Criteria with FQL
Andreas Holzer, Christian Schallhart, Michael Tautschnig, Helmut Veith
2009, Technical report, Technische Universität Darmstadt.
[bibtex]
[102]Tractable Cases of the Extended Global Cardinality Constraint
Marko Samer, Stefan Szeider
Constraints, 2009, Springer Netherlands.
Note: In press.
[bibtex] [doi]
2008
[101]Optimizing Automatic Deployment Using Non-Functional Requirement Annotations
Stefan Kugele, Wolfgang Haberl, Michael Tautschnig, Martin Wechs
Leveraging Applications of Formal Methods, Verification and Validation (Tiziana Margaria, Bernhard Steffen, eds.), volume 17 of Communications in Computer and Information Science, pages 400-414, October 2008, Springer.
[bibtex]
[100]Navigating the Requirements Jungle
Boris Langer, Michael Tautschnig
Leveraging Applications of Formal Methods, Verification and Validation (Tiziana Margaria, Bernhard Steffen, eds.), volume 17 of Communications in Computer and Information Science, pages 354-368, October 2008, Springer.
[bibtex]
[99]Query-Driven Program Testing
Andreas Holzer, Christian Schallhart, Michael Tautschnig, Helmut Veith
October 2008, Technical report, Technische Universität Darmstadt.
[bibtex] [pdf]
[98]A Model Driven Development Approach for Implementing Reactive Systems in Hardware
Zhonglei Wang, Andreas Herkersdorf, Stefano Merenda, Michael Tautschnig
Forum on Specification and Design Languages (FDL08), pages 197-202, September 2008, IEEE Computer Society.
[bibtex] [doi]
[97]From COLA Models to Distributed Embedded Systems Code
Wolfgang Haberl, Michael Tautschnig, Uwe Baumgarten
IAENG International Journal of Computer Science, volume 35, number 3, pages 427-437, September 2008.
[bibtex]
[96]Jakstab: A Static Analysis Platform for Binaries
Johannes Kinder, Helmut Veith
Proceedings of the 20th International Conference on Computer Aided Verification (CAV 2008), volume 5123 of Lecture Notes in Computer Science, July 2008, Springer.
[bibtex]
[95]Domain Pattern Abstraction + Ptolemaic Abstract Domains = Environment Abstraction for Concurrent Systems
Murali Talupur, Helmut Veith
Exploiting Concurrency Efficiently and Correctly -- (EC)__MATH0__, July 2008.
[bibtex]
[94]FShell: Systematic Test Case Generation for Dynamic Analysis and Measurement
Andreas Holzer, Christian Schallhart, Michael Tautschnig, Helmut Veith
Proceedings of the 20th International Conference on Computer Aided Verification (CAV 2008), volume 5123 of Lecture Notes in Computer Science, pages 209-213, July 2008, Springer.
[bibtex]
[93]Mapping Data-Flow Dependencies onto Distributed Embedded Systems
Stefan Kugele, Wolfgang Haberl
Proceedings of the 2008 International Conference on Software Engineering Research & Practice, SERP 2008, July 2008.
[bibtex]
[92]Automatic Generation of SystemC Models from Component-based Designs for Early Design Validation and Performance Analysis
Zhonglei Wang, Wolfgang Haberl, Stefan Kugele, Michael Tautschnig
WOSP '08: Proceedings of the 7th International Workshop on Software and Performance, pages 139-144, June 2008, ACM.
[bibtex]
[91]A Benchmarking Suite for Measurement-Based WCET Analysis Tools
Sven Bünte, Michael Tautschnig
International Conference on Software Testing Verification and Validation Workshop (ICSTW'08), pages 353-356, April 2008, IEEE Computer Society Press.
[bibtex] [doi]
[90] Proving Ptolemy Right: The Environment Abstraction Framework for Model Checking Concurrent Systems
Edmund M. Clarke, Muralidhar Talupur, Helmut Veith
Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008 (C. R. Ramakrishnan, Jakob Rehof, eds.), volume 4963 of Lecture Notes in Computer Science, pages 33-47, April 2008, Springer.
[bibtex] [pdf]
[89]Running COLA on Embedded Systems
Wolfgang Haberl, Michael Tautschnig, Uwe Baumgarten
Proceedings of The International MultiConference of Engineers and Computer Scientists 2008, pages 922-928, March 2008.
[bibtex]
[88]The good, the bad, the ugly---but how ugly is ugly?
Andreas Bauer, Martin Leucker, Christian Schallhart
February 2008, Technical report, Institut für Informatik, Technische Universität München.
[bibtex]
[87]Towards Improvements in Design and Analysis of Embedded Systems (Abstract)
Visar Januzaj
Proceedings of the 3rd Annual Meeting of Institute Alb-Shkenca, 1 - 3 September 2008.
[bibtex]
[86]Impartial Anticipation in Runtime-Verification
Wei Dong, Martin Leucker, Christian Schallhart
Automated Technology for Verification and Analysis (ATVA'08), volume 5311 of Lecture Notes in Computer Science (LNCS), pages 386-396, 2008.
[bibtex]
[85]Variable Dependencies of Quantified CSPs
Marko Samer
Proceedings of the 15th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'08), volume 5330 of Lecture Notes in Computer Science, pages 512-527, 2008, Springer-Verlag.
[bibtex] [doi]
[84]25 Years of Model Checking - History, Achievements, Perspectives
(Orna Grumberg, Helmut Veith, eds.), volume 5000 of Lecture Notes in Computer Science, 2008, Springer.
[bibtex]
[83]Logic for Programming, Artificial Intelligence, and Reasoning, 15th International Conference, LPAR 2008, Doha, Qatar, November 22-27, 2008. Proceedings
(Iliano Cervesato, Helmut Veith, Andrei Voronkov, eds.), volume 5330 of Lecture Notes in Computer Science, 2008, Springer.
[bibtex]
2007
[82]Don't care in SMT---Building flexible yet efficient abstraction/refinement solvers
Andreas Bauer, Martin Leucker, Christian Schallhart, Michael Tautschnig
Proceedings of the 2007 ISoLA Workshop On Leveraging Applications of Formal Methods, Verification and Validation (ISoLA), pages 135-146, December 2007.
[bibtex]
[81]Software Transformations to Improve Malware Detection
Mihai Christodorescu, Johannes Kinder, Somesh Jha, Stefan Katzenbeisser, Helmut Veith
Journal in Computer Virology, volume 3, number 4, pages 253-265, November 2007.
[bibtex]
[80]CPNunf: A tool for McMillan's Unfolding of Coloured Petri Nets
Visar Januzaj
Eighth Workshop and Tutorial on Practical Use of Coloured Petri Nets and the CPN Tools (Kurt Jensen, ed.), October 2007.
[bibtex]
[79]COLA -- The component language
Stefan Kugele, Michael Tautschnig, Andreas Bauer, Christian Schallhart, Stefano Merenda, Wolfgang Haberl, Christian Kühnel, Florian Müller, Zhonglei Wang, Doris Wild, Sabine Rittmann, Martin Wechs
September 2007, Technical report, Institut für Informatik, Technische Universität München.
[bibtex]
[78]Compatibility and reuse in component-based systems via type and unit inference
Christian Kühnel, Andreas Bauer, Michael Tautschnig
Proceedings of the 33rd EUROMICRO Conference on Software Engineering and Advanced Applications (SEAA), pages 101-108, August 2007, IEEE Computer Society Press.
[bibtex] [doi]
[77]Compatibility and reuse in component-based systems via type and unit inference
Christian Kühnel, Andreas Bauer, Michael Tautschnig
May 2007, Technical report, Institut für Informatik, Technische Universität München.
[bibtex]
[76]Tool-support for the analysis of hybrid systems and models
Andreas Bauer, Markus Pister, Michael Tautschnig
Proceedings of the 2007 Conference on Design, Automation and Test in Europe (DATE), pages 924-929, April 2007, European Design and Automation Association.
[bibtex] [pdf] [doi]
[75]Architecture and Security in Networked Virtual Environments
Christian Schallhart
2007, PhD thesis, Vienna University of Technology.
[bibtex]
[74]Enforcing Semantic Integrity on Untrusted Clients in Networked Virtual Environments (Extended Abstract)
Somesh Jha, Stefan Katzenbeisser, Helmut Veith, Stephen Chenny
IEEE Security and Privacy (S&P'07), pages 179-186, 2007.
[bibtex]
[73]Verification Across Intellectual Property Boundaries
Sagar Chaki, Christian Schallhart, Helmut Veith
Computer Aided Verification (CAV'07), pages 82-94, 2007.
[bibtex]
[72]Runtime Verfication for LTL and TLTL
Andreas Bauer, Martin Leucker, Christian Schallhart
2007, Technical report, Institut für Informatik, Technische Universität München.
[bibtex]
[71]The good, the bad, and the ugly, but how ugly is ugly?
Andreas Bauer, Martin Leucker, Christian Schallhart
Workshop on Runtime Verification (RV'07), pages 126-138, 2007.
[bibtex]
[70]Using Verification Technology to Specify and Detect Malware
Andreas Holzer, Johannes Kinder, Helmut Veith
11th International Conference on Computer Aided Systems Theory (EUROCAST 2007), volume 4739 of Lecture Notes in Computer Science, pages 497-504, 2007, Springer.
[bibtex]
2006
[69]Development of a tool to solve mixed logical/linear constraint problems
Michael Tautschnig
February 2006, Master's thesis, Technische Universität München.
[bibtex]
[68]Runtime Reflection: Dynamic model-based analyis of component-based distributed embedded systems
Andreas Bauer, Martin Leucker, Christian Schallhart
Modellierung von Automotive Systems, 2006.
[bibtex]
[67]Monitoring of Realtime Properties
Andreas Bauer, Martin Leucker, Christian Schallhart
Foundations of Software Technology and Theoretical Computer Science (FSTTCS'06), pages 260-272, 2006.
[bibtex]
[66]Model-Based Runtime Analysis of Distributed Reactive Systems
Andreas Bauer, Martin Leucker, Christian Schallhart
Australian Software Engineering Conference (ASWEC'06), pages 243-252, 2006.
[bibtex]
[65] The first order definability of graphs: Upper bounds for quantifier depth
Oleg Pikhurko, Helmut Veith, Oleg Verbitsky
Discrete Applied Mathematics, volume 154, number 17, pages 2511-2529, 2006.
[bibtex] [pdf]
[64] Environment Abstraction for Parameterized Verification
Edmund M. Clarke, Muralidhar Talupur, Helmut Veith
Verification, Model Checking, and Abstract Interpretation, 7th International Conference, VMCAI 2006, Charleston, SC, USA, January 8-10, 2006, Proceedings (E. Allen Emerson, Kedar S. Namjoshi, eds.), pages 126-141, 2006, Springer.
[bibtex] [pdf]
[63]From Temporal Logic Queries to Vacuity Detection
Marko Samer, Helmut Veith
Verification of Infinite-State Systems with Applications to Security, Proceedings of the NATO Advanced Research Workshop "Verification of Infinite State Systems with Applications to Security VISSAS 2005", Timisoara, Romania, March 17-22, 2005 (Edmund M. Clarke, Marius Minea, Ferucio Laurentiu Tiplea, eds.), volume 1 of NATO Security through Science Series D: Information and Communication Security, pages 149-167, 2006, IOS Press.
[bibtex]
2005
[62]Malware Normalization
Mihai Christodorescu, Johannes Kinder, Somesh Jha, Stefan Katzenbeisser, Helmut Veith
November 2005, Technical report, University of Wisconsin, Madison.
[bibtex]
[61]Model Checking: Back and Forth between Hardware and Software
Edmund M. Clarke, Aarti Gupta, Himanshu Jain, Helmut Veith
Verified Software: Theories, Tools, Experiments, October 2005.
[bibtex]
[60] Detecting Malicious Code by Model Checking
Johannes Kinder, Stefan Katzenbeisser, Christian Schallhart, Helmut Veith
GI SIG SIDAR Conference on Detection of Intrusions and Malware & Vulnerability Assessment (DIMVA'05) (Klaus Julisch, Christopher Krügel, eds.), volume 3548 of Lecture Notes in Computer Science, pages 174-187, July 2005, Springer.
[bibtex] [pdf]
[59]Approximating Succinct MaxSat
Christian Schallhart, Luca Trevisan
Journal of Logic and Computation (JLC), volume 15, number 4, pages 551-557, 2005.
[bibtex]
[58]A Novel SAT Procedure for Linear Real Arithmetic
Peter Koppensteiner, Helmut Veith
Third Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR 2005), 2005.
[bibtex]
[57]Model-Based Testing of Reactive Systems
Axel Belinfante, Lars Franzen, Christian Schallhart
Chapter in Tools for Test Case Generation, volume 3472 of Lecture Notes in Computer Science, pages 391-438, 2005, Springer.
[bibtex]
[56]Runtime verification revisited
Oliver Arafat, Andreas Bauer, Martin Leucker, Christian Schallhart
2005, Technical report, Technische Universität München.
[bibtex]
[55] An Iterative Framework for Simulation Conformance
Sagar Chaki, Edmund M. Clarke, Somesh Jha, Helmut Veith
J. Log. Comput., volume 15, number 4, pages 465-488, 2005.
[bibtex] [pdf]
[54] Deterministic CTL Query Solving
Marko Samer, Helmut Veith
12th International Symposium on Temporal Representation and Reasoning (TIME 2005), 23-25 June 2005, Burlington, Vermont, USA, pages 156-165, 2005, IEEE Computer Society.
[bibtex] [pdf]
[53]Malware Engineering
Stefan Katzenbeisser, Christian Schallhart, Helmut Veith
Sicherheit 2005: Sicherheit - Schutz und Zuverlässigkeit, Beiträge der 2. Jahrestagung des Fachbereichs Sicherheit der Gesellschaft für Informatik e.v. (GI), 5.-8. April 2005 in Regensburg (Hannes Federrath, ed.), pages 139-148, 2005, GI.
[bibtex]
[52]Ensuring Media Integrity on Third-Party Infrastructures
Jana Dittmann, Stefan Katzenbeisser, Christian Schallhart, Helmut Veith
Security and Privacy in the Age of Ubiquitous Computing, IFIP TC11 20th International Conference on Information Security (SEC 2005), May 30 - June 1, 2005, Chiba, Japan (Ryôichi Sasaki, Sihan Qing, Eiji Okamoto, Hiroshi Yoshiura, eds.), pages 493-508, 2005, Springer.
[bibtex]
[51] State/Event Software Verification for Branching-Time Specifications
Sagar Chaki, Edmund M. Clarke, Orna Grumberg, Joël Ouaknine, Natasha Sharygina, Tayssir Touili, Helmut Veith
Integrated Formal Methods, 5th International Conference, IFM 2005, Eindhoven, The Netherlands, November 29 - December 2, 2005, Proceedings (Judi Romijn, Graeme Smith, Jaco van de Pol, eds.), pages 53-69, 2005, Springer.
[bibtex] [pdf]
[50]Temporal Logic Model Checking
Edmund M. Clarke, Ansgar Fehnker, Sumit Kumar Jha, Helmut Veith
Chapter in Handbook of Networked and Embedded Control Systems (Dimitrios Hristu-Varsakelis, William S. Levine, eds.), pages 539-558, 2005, Birkhäuser.
[bibtex]
2004
[49]Towards a formal semantics for ODRL
Markus Holzer, Stefan Katzenbeisser, Christian Schallhart
First ODRL International Workshop, pages 137-148, 2004.
[bibtex]
[48] Modular Verification of Software Components in C
Sagar Chaki, Edmund M. Clarke, Alex Groce, Somesh Jha, Helmut Veith
IEEE Trans. Software Eng., volume 30, number 6, pages 388-402, 2004.
[bibtex] [pdf]
[47] A Syntactic Characterization of Distributive LTL Queries
Marko Samer, Helmut Veith
Automata, Languages and Programming: 31st International Colloquium, ICALP 2004, Turku, Finland, July 12-16, 2004. Proceedings (Josep Díaz, Juhani Karhumäki, Arto Lepistö, Donald Sannella, eds.), pages 1099-1110, 2004, Springer.
[bibtex] [pdf]
[46] Parameterized Vacuity
Marko Samer, Helmut Veith
Formal Methods in Computer-Aided Design, 5th International Confrence, FMCAD 2004, Austin, Texas, USA, November 15-17, 2004, Proceedings (Alan J. Hu, Andrew K. Martin, eds.), pages 322-336, 2004, Springer.
[bibtex] [pdf]
[45] Verification by Network Decomposition
Edmund M. Clarke, Muralidhar Talupur, Tayssir Touili, Helmut Veith
CONCUR 2004 - Concurrency Theory, 15th International Conference, London, UK, August 31 - September 3, 2004, Proceedings (Philippa Gardner, Nobuko Yoshida, eds.), pages 276-291, 2004, Springer.
[bibtex] [pdf]
2003
[44]Transaction Processing for Clustered Virtual Environments
Christian Schallhart
NATO Advanced Research Workshop on Concurrent Information Processing and Computing, pages 146-158, July 2003.
[bibtex]
[43]The ATOM Middleware for Massively Parallel Multi-Player Online Games
Christian Schallhart, Georg Gottlob, Helmut Veith
March 2003, Technical report, Vienna University of Technology, Database and Artificial Intelligence Group.
[bibtex]
[42] Counterexample-guided abstraction refinement for symbolic model checking
Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, Helmut Veith
J. ACM, volume 50, number 5, pages 752-794, 2003.
[bibtex] [pdf]
[41]Integrating Publish/Subscribe into a Mobile Teamwork Support Platform
Sagar Chaki, Pascal Fenkam, Harald Gall, Somesh Jha, Engin Kirda, Helmut Veith
Proceedings of the Fifteenth International Conference on Software Engineering & Knowledge Engineering (SEKE'2003), Hotel Sofitel, San Francisco Bay, CA, USA, July 1-3, 2003, pages 510-517, 2003.
[bibtex]
[40] SAT Based Predicate Abstraction for Hardware Verification
Edmund M. Clarke, Muralidhar Talupur, Helmut Veith, Dong Wang
Theory and Applications of Satisfiability Testing, 6th International Conference, SAT 2003. Santa Margherita Ligure, Italy, May 5-8, 2003 Selected Revised Papers (Enrico Giunchiglia, Armando Tacchella, eds.), pages 78-92, 2003, Springer.
[bibtex] [pdf]
[39] Modular Verification of Software Components in C
Sagar Chaki, Edmund M. Clarke, Alex Groce, Somesh Jha, Helmut Veith
Proceedings of the 25th International Conference on Software Engineering, May 3-10, 2003, Portland, Oregon, USA, pages 385-395, 2003, IEEE Computer Society.
[bibtex] [pdf]
[38] Watermarking schemes provably secure against copy and ambiguity attacks
André Adelsbach, Stefan Katzenbeisser, Helmut Veith
Proceedings of the 2003 ACM workshop on Digital rights management 2003, Washington, DC, USA, October 27, 2003 (Moti Yung, ed.), pages 111-119, 2003, ACM.
[bibtex] [pdf]
[37] Friends or Foes? Communities in Software Verification (Invited Lecture)
Helmut Veith
Computer Science Logic, 17th International Workshop, CSL 2003, 12th Annual Conference of the EACSL, and 8th Kurt Güdel Colloquium, KGC 2003, Vienna, Austria, August 25-30, 2003, Proceedings (Matthias Baaz, Johann A. Makowsky, eds.), pages 528-529, 2003, Springer.
[bibtex] [pdf]
[36] Validity of CTL Queries Revisited
Marko Samer, Helmut Veith
Computer Science Logic, 17th International Workshop, CSL 2003, 12th Annual Conference of the EACSL, and 8th Kurt Güdel Colloquium, KGC 2003, Vienna, Austria, August 25-30, 2003, Proceedings (Matthias Baaz, Johann A. Makowsky, eds.), pages 470-483, 2003, Springer.
[bibtex] [pdf]
[35] Counterexamples Revisited: Principles, Algorithms, Applications
Edmund M. Clarke, Helmut Veith
Verification: Theory and Practice, Essays Dedicated to Zohar Manna on the Occasion of His 64th Birthday (Nachum Dershowitz, ed.), pages 208-224, 2003, Springer.
[bibtex] [pdf]
2002
[34]Securing Symmetric Watermarking Schemes Against Protocol Attacks
Stefan Katzenbeisser, Helmut Veith
Security and Watermarking of Multimedia Contents IV, volume 4675 of SPIE, pages 260-268, 2002.
[bibtex]
[33] Datalog LITE: a deductive query language with linear time model checking
Georg Gottlob, Erich Grädel, Helmut Veith
ACM Trans. Comput. Log., volume 3, number 1, pages 42-79, 2002.
[bibtex] [pdf]
[32]On the complexity of data disjunctions
Thomas Eiter, Helmut Veith
Theor. Comput. Sci., volume 288, number 1, pages 101-128, 2002.
[bibtex]
[31] Tree-Like Counterexamples in Model Checking
Edmund M. Clarke, Somesh Jha, Yuan Lu, Helmut Veith
17th IEEE Symposium on Logic in Computer Science (LICS 2002), 22-25 July 2002, Copenhagen, Denmark, Proceedings, pages 19-29, 2002, IEEE Computer Society.
[bibtex] [pdf]
[30] Automated Abstraction Refinement for Model Checking Large State Spaces Using SAT Based Conflict Analysis
Pankaj Chauhan, Edmund M. Clarke, James H. Kukula, Samir Sapra, Helmut Veith, Dong Wang
Formal Methods in Computer-Aided Design, 4th International Conference, FMCAD 2002, Portland, OR, USA, November 6-8, 2002, Proceedings (Mark Aagaard, John W. O'Leary, eds.), pages 33-51, 2002, Springer.
[bibtex] [pdf]
2001
[29]A Guide to Quantified Propositional Gödel Logic
Matthias Baaz, Agata Ciabattoni, Norbert Preining, Helmut Veith
Workshop on Theory and Applications of Quantified Boolean Formulas (QBF 2001), 2001.
[bibtex]
[28]Complexity of t-tautologies
Matthias Baaz, Petr Hájek, Franco Montagna, Helmut Veith
Ann. Pure Appl. Logic, volume 113, number 1-3, pages 3-11, 2001.
[bibtex]
[27]Efficient Filtering in Publish-Subscribe Systems Using Binary Decision Diagrams
Alexis Campailla, Sagar Chaki, Edmund M. Clarke, Somesh Jha, Helmut Veith
Proceedings of the 23rd International Conference on Software Engineering, ICSE 2001, 12-19 May 2001, Toronto, Ontario, Canada, pages 443-452, 2001, IEEE Computer Society.
[bibtex]
[26]Non-linear Quantification Scheduling in Image Computation
Pankaj Chauhan, Edmund M. Clarke, Somesh Jha, James H. Kukula, Thomas R. Shiple, Helmut Veith, Dong Wang
ICCAD, pages 293-, 2001.
[bibtex]
[25] Progress on the State Explosion Problem in Model Checking
Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, Helmut Veith
Informatics - 10 Years Back. 10 Years Ahead. (Reinhard Wilhelm, ed.), pages 176-194, 2001, Springer.
[bibtex] [pdf]
[24] Using Combinatorial Optimization Methods for Quantification Scheduling
Pankaj Chauhan, Edmund M. Clarke, Somesh Jha, James H. Kukula, Helmut Veith, Dong Wang
Correct Hardware Design and Verification Methods, 11th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2001, Livingston, Scotland, UK, September 4-7, 2001, Proceedings (Tiziana Margaria, Thomas F. Melham, eds.), pages 293-309, 2001, Springer.
[bibtex] [pdf]
2000
[23]Application of Approximation Theory to Succinct Data Representation
Christian Schallhart
2000, Master's thesis, Vienna University of Technology.
[bibtex]
[22]An Analytic Calculus for Quantified Propositional Gödel Logic
Matthias Baaz, Christian G. Fermüller, Helmut Veith
Automated Reasoning with Analytic Tableaux and Related Methods, International Conference, TABLEAUX 2000, St Andrews, Scotland, UK, July 3-7, 2000, Proceedings (Roy Dyckhoff, ed.), pages 112-126, 2000, Springer.
[bibtex]
[21] Executable Protocol Specification in ESL
Edmund M. Clarke, Steven M. German, Yuan Lu, Helmut Veith, Dong Wang
Formal Methods in Computer-Aided Design, Third International Conference, FMCAD 2000, Austin, Texas, USA, November 1-3, 2000, Proceedings (Warren A. Hunt Jr., Steven D. Johnson, eds.), pages 197-216, 2000, Springer.
[bibtex] [pdf]
[20]Counterexample-Guided Abstraction Refinement
Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, Helmut Veith
Computer Aided Verification, 12th International Conference, CAV 2000, Chicago, IL, USA, July 15-19, 2000, Proceedings (E. Allen Emerson, A. Prasad Sistla, eds.), pages 154-169, 2000, Springer.
[bibtex]
[19]An axiomatization of quantified proposition Gödel logic using the Takeuti-Titani rule
Matthias Baaz, Helmut Veith
Logic Colloquium 1998, volume 13 of Lecture Notes in Logic, pages 91-104, 2000, Association for Symbolic Logic.
[bibtex]
[18]Linear time datalog and branching time logic
Georg Gottlob, Erich Grädel, Helmut Veith
, pages 443-467, 2000, Kluwer Academic Publishers.
[bibtex]
1999
[17]Multiprocessor Scheduling using the DÉJÀ VU Scheduling Class Library
Jürgen Dorn, Anna Prianichnikova, Markus Stumptner, Helmut Veith, Johannes Reisinger, Ralf Schlatterbeck
ÖGAI (Journal of the Austrian Society for AI), volume 4, pages 16-25, 1999.
[bibtex]
[16]Succinctness as a Source of Complexity in Logical Formalisms
Georg Gottlob, Nicola Leone, Helmut Veith
Ann. Pure Appl. Logic, volume 97, number 1-3, pages 231-260, 1999.
[bibtex]
[15] On the Undecidability of some Sub-Classical First-Order Logics
Matthias Baaz, Agata Ciabattoni, Christian G. Fermüller, Helmut Veith
Foundations of Software Technology and Theoretical Computer Science, 19th Conference, Chennai, India, December 13-15, 1999, Proceedings (C. Pandu Rangan, Venkatesh Raman, R. Ramanujam, eds.), pages 258-268, 1999, Springer.
[bibtex] [pdf]
[14]Interpolation in Fuzzy Logic
Matthias Baaz, Helmut Veith
Archive for Mathematical Logic, volume 38, pages 461-489, 1999.
[bibtex]
1998
[13]Eine allgemeine Methode zur Bestimmung der Ausdruckskomplexität von Query Languages
Helmut Veith, Georg Gottlob, Nicola Leone
GI Workshop Grundlagen von Datenbanken, volume 63 of Konstanzer Schriften in Mathematik und Informatik, May 1998.
[bibtex]
[12]John W. Dawson, Jr., Logical Dilemmas: The Life and Work of Kurt Gödel
Helmut Veith
Chapter in (Werner Leinfellner, Eckehart Köhler, eds.), 1998, Springer.
[bibtex]
[11]Succinct Representation, Leaf Languages, and Projection Reductions
Helmut Veith
Inf. Comput., volume 142, number 2, pages 207-236, 1998.
[bibtex]
[10] Proof Theory of Fuzzy Logics: Urquhart's C and Related Logics
Matthias Baaz, Agata Ciabattoni, Christian G. Fermüller, Helmut Veith
Mathematical Foundations of Computer Science 1998, 23rd International Symposium, MFCS'98, Brno, Czech Republic, August 24-28, 1998, Proceedings (Lubos Brim, Jozef Gruska, Jirí Zlatuska, eds.), pages 203-212, 1998, Springer.
[bibtex] [pdf]
[9]A General Method to Determine the Expression Complexity of Database Query Languages
Helmut Veith
Grundlagen von Datenbanken, pages 134-137, 1998.
[bibtex]
[8]Quantifier Elimination in Fuzzy Logic
Matthias Baaz, Helmut Veith
Computer Science Logic, 12th International Workshop, CSL '98, Annual Conference of the EACSL, Brno, Czech Republic, August 24-28, 1998, Proceedings (Georg Gottlob, Etienne Grandjean, Katrin Seyr, eds.), pages 399-414, 1998, Springer.
[bibtex]
[7]How to Encode a Logical Structure by an OBDD
Helmut Veith
IEEE Conference on Computational Complexity, pages 122-131, 1998.
[bibtex] [doi]
1997
[6] Languages Represented by Boolean Formulas
Helmut Veith
Inf. Process. Lett., volume 63, number 5, pages 251-256, 1997.
[bibtex] [pdf]
[5]Modular Logic Programming and Generalized Quantifiers
Thomas Eiter, Georg Gottlob, Helmut Veith
Logic Programming and Nonmonotonic Reasoning, 4th International Conference, LPNMR'97, Dagstuhl Castle, Germany, July 28-31, 1997, Proceedings (Jürgen Dix, Ulrich Furbach, Anil Nerode, eds.), pages 290-309, 1997, Springer.
[bibtex]
[4] Generalized Quantifiers in Logic Programs
Thomas Eiter, Georg Gottlob, Helmut Veith
Generalized Quantifiers and Computation, 9th European Summer School in Logic, Language, and Information, ESSLLI'97 Workshop, Aix-en-Provence, France, August 11-22, 1997, Revised Lectures (Jouko A. Väänänen, ed.), pages 72-98, 1997, Springer.
[bibtex] [pdf]
1996
[3] Succinct Representation, Leaf Languages, and Projection Reductions
Helmut Veith
IEEE Conference on Computational Complexity, pages 118-126, 1996.
[bibtex] [pdf]
1995
[2] Succinct Representation and Leaf Languages
Helmut Veith
Electronic Colloquium on Computational Complexity (ECCC), volume 2, number 48, 1995.
[bibtex] [pdf]
[1]Second Order Logic and the Weak Exponential Hierarchies
Georg Gottlob, Nicola Leone, Helmut Veith
Mathematical Foundations of Computer Science 1995, 20th International Symposium, MFCS'95, Prague, Czech Republic, August 28 - September 1, 1995, Proceedings (Jirí Wiedermann, Petr Hájek, eds.), pages 66-81, 1995, Springer.
[bibtex]

Latest News

Two papers at POPL’17

Two papers co-authored by researchers from our group have been accepted for POPL’17: “Coming to Terms with Quantified Reasoning” by Simon Robillard, Andrei Voronkov, and Laura Kovacs; and “A Short Counterexample Property for Safety and Liveness Verification of Fault-tolerant Distributed Algorithms” by Igor Konnov, Marijana Lazic, Helmut Veith, and Josef Widder

Continue reading

Helmut Veith Stipend

Outstanding female students in the field of computer science who pursue (or plan to pursue) one of the master‘s programs in Computer Science at TU Wien taught in English are invited to apply for the Helmut Veith Stipend

Continue reading

LogicLounge in memoriam Helmut Veith

Will robots take away your job? In memory of Helmut Veith, this year’s Conference on Computer Aided Verification (CAV), which takes place in Toronto, will feature a LogicLounge on the effect of automation and artificial intelligence on our jobs.

Continue reading

Questions answered by Leslie Lamport

Leslie Lamport is going to answer questions about a Mathematical View of Computer Systems in Informatikhörsaal on Tuesday at 6pm. Check the announcement at the VCLA website and do not forget to watch the lecture beforehand.

Continue reading

Full news archive