Helmut Veith

 

 

 

Helmut Veith, (c) Philipp Horak

Helmut Veith is a professor at the Faculty of Informatics of Vienna University of Technology (TU Vienna), and an adjunct professor at Carnegie Mellon University. He has a diploma in Computational Logic and a PhD sub auspiciis praesidentis in Computer Science, both from Vienna University of Technology. Prior to his appointment to Vienna, he was holding professor positions at TU Darmstadt and TU Munich.

In his research, Helmut Veith applies formal and logical methods to problems in software technology and engineering. His current work is focusing on model checking, software verification and testing, embedded software and computer security.

Curriculum Vitae, February 2010

Publications in DBLP and Google scholar

Activities

Research Grants

Information for Students

Contact Information

Media on FORSYTE, RiSE, VCLA, VSL

Activities

  • Program committee co-chair of FMCAD 2015, CAV 2013, CSL 2010, LPAR 2008; Tutorial Chair, FMCAD 2010

     

  • Program committee member of TACAS 2015, ATVA 2010, CAV 2003, CAV 2005, CAV 2009, CAV 2010, CAV 2012, CSL 2009, CSL 2011, CSL 2012, CSR 2007-2009, DATE 2011, DATE 2012, EC2 2009-2012, FMCAD 2009, FMCAD 2010, FMCAD 2011, FMICS 2011, FSTTCS 2007, FORTE 2013, HVC 2010, HVC 2011, ICTAC 2009, ICTAC 2010, ICTERI 2011, ICTERI 2012, LATA 2013, LICS 2004, SOFSEM 2012, SPIN 2012, SPIN 2013, SYNASC 2008-2011, TACAS SW Verification Competition 2012, TASE 2011, VMCAI 2012, WING 2009, WING 2010, WOLLIC 2011 etc.

 

 vsl      Vienna Summer of Logic 2014 (co chair)dark_screen_rgb
FLoC 2014 (chair)

 

Doctoral Program LogiCS

FWF Doctoral College on Logical Methods in Computer Science (Speaker)

 

Logo ARiSE

FWF Research Network on Rigorous Systems Engineering (Deputy Coordinator)

Austrian Society for Rigorous Systems Engineering (President)

 

VCLA Logo

Vienna Center for Logic and Algorithms (co chair)

vcla1

 

KGS Logo

 Kurt Gödel Society (Exceutive Board)

 

eacsl

European Association for Computer Science Logic (EACSL) (Executive Board)

 

asl

Association for Symbolic Logic, Committee on Logic Education

 

TU Logo

Academic Senate of TU Vienna (vice speaker of professors)

TU Vienna Research focus in Computational Intelligence (coordinator)

TU Vienna curriculum commission for computer science

 

Information for Students

We are always looking for enthusiastic students on all levels to join our team. You can find projects and topics on our Research and Teaching pages. Please contact either me or a staff member by email for a personal appointment.

I am offering regular courses, seminars, and projects on Computer-Aided Verification, Formal Methods, Model Checking, Information Design, and Logic in Computer Science. Information about my courses can be found in TISS.

 

Contact Information

Phone+43-1-58801- 18441
Fax+43-1-58801- 18492
Secretary+43-1-58801- 18403 (Ms Forsthuber)
Skypehveith
Emailsee our Directory Page
Appointmentsby email
Postal Address     Technische Universität Wien
Institut für Informationssysteme 184/4
Arbeitsbereich Formal Methods in Systems Engineering
Favoritenstraße 9–11
1040 Wien
Austria
DirectionsSee our Directions Page

 

 Publications

 

2014
[114] 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]
[113] 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, 25-29 August 2014, Springer.
[bibtex] [pdf]
[112] 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, 13 July 2014.
[bibtex] [pdf]
[111]Towards a Description Logic for Program Analysis: Extending ALCQIO with Reachability (poster)
Mantas Simkus Helmut Veith Tomer Kotek, Florian Zuleger
2014, KR Workshop DL.
[bibtex]
[110]Shape and Content: Incorporating Domain Knowledge into Shape Analysis
Tomer Kotek Mantas Simkus Helmut Veith Diego Calvanese, Florian Zuleger
2014, KR Workshop DL.
[bibtex]
[109]Parameterized Model Checking of Rendezvous Systems
Benjamin Aminof, Tomer Kotek, Sasha Rubin, Francesco Spegni, Helmut Veith
2014, CSL-LICS Workshop AISS.
[bibtex]
[108]Parameterized Model Checking of Rendezvous Systems
Benjamin Aminof, Tomer Kotek, Sasha Rubin, Francesco Spegni, Helmut Veith
CONCUR, 2014.
Note: Accepted
[bibtex]
[107]A Simple and Scalable Approach to Bound Analysis and Amortized Complexity Analysis
Moritz Sinn, Florian Zuleger, Helmut Veith
Chapter in Computer Aided Verification, volume 8559 of Lecture Notes in Computer Science, pages 743–759, 2014, Springer Berlin Heidelberg.
[bibtex]
[106] 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]
[105] 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]
[104] 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]
[103]Concolic Testing of Concurrent Programs
Azadeh Farzan, Andreas Holzer, Niloofar Razavi, Helmut Veith
2014, CAV Workshop (EC)^2.
[bibtex]
[102] 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]
2013
[101] 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]
[100] 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]
[99] 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]
[98] 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]
[97] 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]
[96] 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]
[95] 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]
[94] 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]
[93] 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]
[92] Information Reuse for Multi-goal Reachability Analyses
Dirk Beyer, Andreas Holzer, Michael Tautschnig, Helmut Veith
ESOP, pages 472-491, 2013.
[bibtex] [pdf] [doi]
[91] 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]
[90] 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]
2012
[89] 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]
[88] 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]
[87] Special Issue: Games in Verification
Helmut Veith
J. Comput. Syst. Sci., volume 78, number 2, pages 393, 2012.
[bibtex] [pdf]
[86] Who is afraid of Model Checking Distributed Algorithms?
Igor Konnov, Helmut Veith, Josef Widder
2012, CAV Workshop (EC)^2.
[bibtex] [pdf]
[85] 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]
[84] 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]
[83] Selected Papers of the Conference "Computer Science Logic CSL 2010": Preface
Anuj Dawar, Helmut Veith
Logical Methods in Computer Science, 2012.
[bibtex] [pdf]
2011
[82]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]
[81]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]
[80] 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
[79]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]
[78]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]
[77]On the Distributivity of LTL Specifications
Marko Samer, Helmut Veith
ACM Transactions on Computational Logic (TOCL), volume 11, number 3, May 2010, ACM.
[bibtex]
[76]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]
[75]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]
2009
[74]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]
[73]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]
[72]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]
[71]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]
[70]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]
[69]Dependency Coverage Criteria with FQL
Andreas Holzer, Christian Schallhart, Michael Tautschnig, Helmut Veith
2009, Technical report, Technische Universität Darmstadt.
[bibtex]
2008
[68]Query-Driven Program Testing
Andreas Holzer, Christian Schallhart, Michael Tautschnig, Helmut Veith
October 2008, Technical report, Technische Universität Darmstadt.
[bibtex]
[67]Domain Pattern Abstraction + Ptolemaic Abstract Domains = Environment Abstraction for Concurrent Systems
Murali Talupur, Helmut Veith
Exploiting Concurrency Efficiently and Correctly -- (EC)$^2$, July 2008.
[bibtex]
[66]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]
[65]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]
[64] 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]
2007
[63]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]
[62]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]
[61]Verification Across Intellectual Property Boundaries
Sagar Chaki, Christian Schallhart, Helmut Veith
Computer Aided Verification (CAV'07), pages 82-94, 2007.
[bibtex]
[60]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
[59] 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]
[58] 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]
[57]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
[56]Malware Normalization
Mihai Christodorescu, Johannes Kinder, Somesh Jha, Stefan Katzenbeisser, Helmut Veith
November 2005, Technical report, University of Wisconsin, Madison.
[bibtex]
[55]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]
[54] 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]
[53]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]
[52] 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]
[51] 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]
[50]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]
[49]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]
[48] 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]
[47]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
[46] 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]
[45] 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]
[44] 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]
[43] 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
[42]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]
[41] 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]
[40]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]
[39] 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]
[38] 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]
[37] 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]
[36] 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]
[35] 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]
[34] 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
[33]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]
[32] 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]
[31]On the complexity of data disjunctions
Thomas Eiter, Helmut Veith
Theor. Comput. Sci., volume 288, number 1, pages 101-128, 2002.
[bibtex]
[30] 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]
[29] 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
[28]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]
[27]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]
[26]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]
[25] 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] [pdf]
[24] 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]
[23] 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
[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]