@article{SamSze09JCSS,

author = {Marko Samer and Stefan Szeider},

title = {Constraint Satisfaction with Bounded Treewidth Revisited},

number = {2},

month = {March},

year = {2010},

journal = {Journal of Computer and System Sciences (JCSS)},

pages = {103-114},

publisher = {Academic Press},

volume = {76},

abstract = {The constraint satisfaction problem can be solved in polynomial time for instances where certain parameters (e.g., the treewidth of primal graphs) are bounded. However, there is a trade-off between generality and performance: larger bounds on the parameters yield worse time complexities. It is desirable to pay for more generality only by a constant factor in the running time, not by a larger degree of the polynomial. Algorithms with such a uniform polynomial time complexity are known as fixed-parameter algorithms. In this paper we determine whether or not fixed-parameter algorithms for constraint satisfaction exist, considering all possible combinations of the following parameters: the treewidth of primal graphs, the treewidth of dual graphs, the treewidth of incidence graphs, the domain size, the maximum arity of constraints, and the maximum size of overlaps of constraint scopes. The negative cases are subject to the complexity theoretic assumption FPT ? W[1] which is the parameterized analog to P ? NP. For the positive cases we provide an effective fixed-parameter algorithm which is based on dynamic programming on “nice” tree decompositions.},

issn = {0022-0000},

doi = {10.1016/j.jcss.2009.04.003}

}

@article{SamSze09JDA,

author = {Marko Samer and Stefan Szeider},

title = {Algorithms for Propositional Model Counting},

number = {1},

month = {March},

year = {2010},

journal = {Journal of Discrete Algorithms (JDA)},

pages = {50-64},

publisher = {Elsevier},

volume = {8},

abstract = {We present algorithms for the propositional model counting problem #SAT. The algorithms are based on tree-decompositions of graphs associated with the given CNF formula, in particular primal, dual, and incidence graphs. We describe the algorithms in a coherent fashion that admits a direct comparison of their algorithmic advantages. We analyze and discuss several aspects of the algorithms including worst-case time and space requirements and simplicity of implementation. The algorithms are described in sufficient detail for making an implementation reasonably easy.},

issn = {1570-8667},

doi = {10.1016/j.jda.2009.06.002}

}

@article{bauer:leucker:schallhart:tautschnig:sttt,

author = {Andreas Bauer and Martin Leucker and Christian Schallhart and Michael Tautschnig},

title = {Don't care in {SMT}---Building flexible yet efficient abstraction/refinement solvers},

number = {1},

month = {February},

year = {2010},

journal = {International Journal on Software Tools for Technology Transfer},

pages = {23--37},

volume = {12},

doi = {10.1007/s10009-009-0133-2}

}

@article{jha09:_seman_integ_in_large_scale_onlin_simul,

author = {Somesh Jha and Stefan Katzenbeisser and Christian Schallhart and Helmut Veith and Stephen Chenney},

title = {{Semantic Integrity in Large-Scale Online Simulations}},

year = {2010},

journal = {{ACM Transactions on Internet Technology (TOIT)}},

note = {accepted for publication}

}

@article{bauer09:_compar_ltl_seman_for_runtim_verif,

author = {Andreas Bauer and Martin Leucker and Christian Schallhart},

title = {{Comparing LTL Semantics for Runtime Verification}},

year = {2010},

journal = {{Journal of Logic and Computation (JLC)}},

note = {accepted for publication},

doi = {doi: 10.1093/logcom/exn075}

}

@article{bauer09:_runtim_verif_for_ltl_and_tltl,

author = {Andreas Bauer and Martin Leucker and Christian Schallhart},

title = {{Runtime Verification for LTL and TLTL}},

year = {2010},

journal = {{ACM Transactions on Software and Methodology (TOSEM)}},

note = {accepted for publication}

}

@inproceedings{godefroidkinder-fpsafety10,

author = {Patrice Godefroid and Johannes Kinder},

title = {Proving Memory Safety of Floating-Point Computations by Combining Static and Dynamic Program Analysis},

year = {2010},

booktitle = {International Symposium on Software Testing and Analysis (ISSTA'10)},

note = {Accepted for publication}

}

@inbook{haberl:tautschnig:baumgarten:lnee,

author = {Wolfgang Haberl and Michael Tautschnig and Uwe Baumgarten},

title = {{Generating Distributed Code From COLA Models}},

month = {March},

year = {2009},

booktitle = {Trends in Communication Technologies and Engineering Science},

chapter = {20},

publisher = {Springer},

series = {Lecture Notes in Electrical Engineering},

volume = {33},

isbn = {978-1-4020-9492-7}

}

@incollection{SamSze09HBSAT,

author = {Marko Samer and Stefan Szeider},

title = {Fixed-Parameter Tractability},

month = {February},

year = {2009},

booktitle = {Handbook of Satisfiability},

chapter = {13},

editor = {A. Biere and M. Heule and H. van Maaren and T. Walsh},

pages = {425--454},

publisher = {IOS Press},

series = {Frontiers in Artificial Intelligence and Applications},

volume = {185},

abstract = {Parameterized complexity is a new theoretical framework that considers, in addition to the overall input size, the effects on computational complexity of a secondary measurement, the parameter. This two-dimensional viewpoint allows a fine-grained complexity analysis that takes structural properties of problem instances into account. The central notion is "fixed-parameter tractability" which refers to solvability in polynomial time for each fixed value of the parameter such that the order of the polynomial time bound is independent of the parameter. This chapter presents main concepts and recent results on the parameterized complexity of the satisfiability problem and it outlines fundamental algorithmic ideas that arise in this context. Among the parameters considered are the size of backdoor sets with respect to various tractable base classes and the treewidth of graph representations of satisfiability instances.},

isbn = {978-1-58603-929-5},

doi = {10.3233/978-1-58603-929-5-425}

}

@article{holzer:januzaj:kugele:2009,

author = {Andreas Holzer and Visar Januzaj and Stefan Kugele},

title = {Towards Resource Consumption-Aware Programming},

year = {2009},

address = {Los Alamitos, CA, USA},

journal = {Software Engineering Advances, International Conference on},

pages = {490-493},

publisher = {IEEE Computer Society},

volume = {0},

abstract = {In order to check the fulfilment of non-functional requirements at an early system design and development stage, we provide a framework that facilitates the combination of platform-independent and platform-specific information in a query-based manner to calculate estimates for the resource consumption of the software under investigation at fine grained levels of code. Based on an already optimised intermediate representation of the source code, using a testing infrastructure for C code, we count the occurrence of instructions during program executions in a platform-independent manner. These instruction counters can be determined at program or function level. By combining these counters with cost information of a hardware platform we can provide resource consumption estimates. This allows the software developer to tailor the code steadily towards the non-functional characteristics of the software.},

isbn = {978-0-7695-3777-1},

doi = {http://doi.ieeecomputersociety.org/10.1109/ICSEA.2009.77}

}

@article{leucker08:_brief_accoun_of_runtim_verif,

author = {Martin Leucker and Christian Schallhart},

title = {{A Brief Account of Runtime Verification}},

number = {78},

year = {2009},

journal = {{Journal of Logic and Algebraic Programming (JLAP)}},

pages = {293-303}

}

@article{SamSze09JAR,

author = {Marko Samer and Stefan Szeider},

title = {Backdoor Sets of Quantified Boolean Formulas},

number = {1},

month = {January},

year = {2009},

journal = {Journal of Automated Reasoning (JAR)},

pages = {77--97},

volume = {42},

abstract = {We generalize the notion of backdoor sets from propositional formulas to quantified Boolean formulas (QBF). This allows us to obtain hierarchies of tractable classes of quantified Boolean formulas with the classes of quantified Horn and quantified 2CNF formulas, respectively, at their first level, thus gradually generalizing these two important tractable classes. In contrast to known tractable classes based on bounded treewidth, the number of quantifier alternations of our classes is unbounded. As a side product of our considerations we develop a theory of variable dependency which is of independent interest.},

issn = {0168-7433},

doi = {10.1007/s10817-008-9114-5}

}

@article{SamSze09Cons,

author = {Marko Samer and Stefan Szeider},

title = {Tractable Cases of the Extended Global Cardinality Constraint},

year = {2009},

journal = {Constraints},

note = {In press.},

publisher = {Springer Netherlands},

abstract = {We study the consistency and domain consistency problem for extended global cardinality (EGC) constraints. An EGC constraint consists of a set X of variables, a set D of values, a domain D(x) ? D for each variable x, and a “cardinality set” K(d) of non-negative integers for each value d. The problem is to instantiate each variable x with a value in D(x) such that for each value d, the number of variables instantiated with d belongs to the cardinality set K(d). It is known that this problem is NP-complete in general, but solvable in polynomial time if all cardinality sets are intervals. First we pinpoint connections between EGC constraints and general factors in graphs. This allows us to extend the known polynomial-time case to certain non-interval cardinality sets. Second we consider EGC constraints under restrictions in terms of the treewidth of the value graph (the bipartite graph representing variable-value pairs) and the cardinality-width (the largest integer occurring in the cardinality sets). We show that EGC constraints can be solved in polynomial time for instances of bounded treewidth, where the order of the polynomial depends on the treewidth. We show that (subject to the complexity theoretic assumption FPT ? W[1]) this dependency cannot be avoided without imposing additional restrictions. If, however, also the cardinality-width is bounded, this dependency gets removed and EGC constraints can be solved in linear time.},

issn = {1383-7133},

doi = {10.1007/s10601-009-9079-y}

}

@inproceedings{januzaj:advcomp09,

author = {Eshref Januzaj and Visar Januzaj},

title = {An Application of Data Mining to Identify Data Quality Problems},

month = {October},

year = {2009},

address = {Sliema, Malta},

booktitle = {Proceedings of the Third International Conference on Advanced Engineering Computing and Applications in Sciences, ADVCOMP 2009},

publisher = {IEEE Computer Society}

}

@inproceedings{SamVei09SAT,

author = {Marko Samer and Helmut Veith},

title = {Encoding Treewidth into SAT},

month = {July},

year = {2009},

booktitle = {Proceedings of the 12th International Conference on Theory and Applications of Satisfiability Testing (SAT'09)},

editor = {Kullmann, Oliver},

pages = {45--50},

publisher = {Springer-Verlag},

series = {Lecture Notes in Computer Science},

volume = {5584},

abstract = {One of the most important structural parameters of graphs is treewidth, a measure for the ``tree-likeness'' and thus in many cases an indicator for the hardness of problem instances. The smaller the treewidth, the closer the graph is to a tree and the more efficiently the underlying instance often can be solved. However, computing the treewidth of a graph is NP-hard in general. In this paper we propose an encoding of the decision problem whether the treewidth of a given graph is at most k into the propositional satisfiability problem. The resulting SAT instance can then be fed to a SAT solver. In this way we are able to improve the known bounds on the treewidth of several benchmark graphs from the literature.},

isbn = {978-3-642-02776-5},

doi = {10.1007/978-3-642-02777-2_6}

}

@inproceedings{gruber:holzer:tautschnig:ciaa09,

author = {Hermann Gruber and Markus Holzer and Michael Tautschnig},

title = {Short Regular Expressions from Finite Automata: Empirical Results},

month = {July},

year = {2009},

address = {Sydney, Australia},

booktitle = {Proceedings of the 14th International Conference on Implementation and Application of Automata (CIAA 2009)},

pages = {188--197},

publisher = {Springer},

series = {Lecture Notes in Computer Science},

volume = {5642}

}

@inproceedings{januzaj:kugele:pnse09,

author = {Visar Januzaj and Stefan Kugele},

title = {Model Analysis via a Translation Schema to Coloured Petri Nets},

month = {June},

year = {2009},

address = {Paris, France},

booktitle = {Proceedings of the International Workshop on Petri Nets and Software Engineering, PNSE '09},

editor = {D. Moldt},

pages = {273-292}

}

@inproceedings{holzer:schallhart:tautschnig:veith:vmcai09,

author = {Andreas Holzer and Christian Schallhart and Michael Tautschnig and Helmut Veith},

title = {Query-Driven Program Testing},

month = {January},

year = {2009},

address = {Savannah, GA, USA},

booktitle = {Proceedings of the Tenth International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2009)},

editor = {Neil D.~Jones and Markus M{\"u}ller-Olm},

pages = {151--166},

publisher = {Springer},

series = {Lecture Notes in Computer Science},

volume = {5403}

}

@inproceedings{KinderZulegerVeith-vmcai09,

author = {Johannes Kinder and Florian Zuleger and Helmut Veith},

title = {An Abstract Interpretation-Based Framework for Control Flow Reconstruction from Binaries},

month = {January},

year = {2009},

address = {Savannah, GA, USA},

booktitle = {Proceedings of the Tenth International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2009)},

editor = {Neil D.~Jones and Markus M{\"u}ller-Olm},

publisher = {Springer},

series = {Lecture Notes in Computer Science},

volume = {5403}

}

@inproceedings{haberl:kugele:baumgarten:mompes09,

author = {Wolfgang Haberl and Stefan Kugele and Uwe Baumgarten},

title = {Reliable Operating Modes for Distributed Embedded Systems},

year = {2009},

address = {Washington, DC, USA},

booktitle = {Proceedings of the 6th International Workshop on Model-based Methodologies for Pervasive and Embedded Software},

publisher = {IEEE Computer Society}

}

@inproceedings{januzaj:mauersberger:biechele:eurocast09,

author = {Visar Januzaj and Ralf Mauersberger and Florian Biechele},

title = {Performance Modelling for Avionics Systems},

month = {15 - 20 February},

year = {2009},

address = {Las Palmas, Gran Canaria},

booktitle = {12th International Conference on Computer Aided Systems Theory - EUROCAST 2009},

pages = {833-840},

publisher = {Springer},

series = {Lecture Notes in Computer Science},

volume = {5717}

}

@inproceedings{haberl:herrmama:kugele:tautschnig:wechs:saase09,

author = {Wolfgang Haberl and Markus Herrmannsdoerfer and Stefan Kugele and Michael Tautschnig and Martin Wechs},

title = {One Click from Model to Reality},

year = {2009},

booktitle = {Proceedings of Symposium on Automotive/Avionics Systems Engineering (SAASE 2009)}

}

@techreport{TUD-CS-2009-0184,

author = {Andreas Holzer and Visar Januzaj and Stefan Kugele and Christian Schallhart and Michael Tautschnig and Helmut Veith and Boris Langer},

title = {Slope Testing for Activity Diagrams and Safety Critical Software},

number = {TUD-CS-2009-0184},

month = {October},

year = {2009},

institution = {Technische Universit\"at Darmstadt},

pdf = {/data/publications/1625_main.pdf}

}

@techreport{holzer:schallhart:tautschnig:veith:TUD-CS-2009-0148,

author = {Andreas Holzer and Christian Schallhart and Michael Tautschnig and Helmut Veith},

title = {A Precise Specification Framework for White Box Program Testing},

number = {TUD-CS-2009-0148},

month = {September},

year = {2009},

institution = {Technische Universit\"at Darmstadt},

pdf = {/data/publications/1583_TUD-CS-2009-0148.pdf}

}

@techreport{TUD-CS-2009-0149,

author = {Andreas Holzer and Christian Schallhart and Michael Tautschnig and Helmut Veith},

title = {Dependency Coverage Criteria with FQL},

number = {TUD-CS-2009-0149},

year = {2009},

institution = {Technische Universit\"at Darmstadt}

}

@proceedings{DBLP:conf/spin/5000,

title = {25 Years of Model Checking - History, Achievements, Perspectives},

year = {2008},

booktitle = {25 Years of Model Checking},

editor = {Orna Grumberg and Helmut Veith},

publisher = {Springer},

series = {Lecture Notes in Computer Science},

volume = {5000},

isbn = {978-3-540-69849-4}

}

@proceedings{DBLP:conf/lpar/2008,

title = {Logic for Programming, Artificial Intelligence, and Reasoning, 15th International Conference, LPAR 2008, Doha, Qatar, November 22-27, 2008. Proceedings},

year = {2008},

booktitle = {LPAR},

editor = {Iliano Cervesato and Helmut Veith and Andrei Voronkov},

publisher = {Springer},

series = {Lecture Notes in Computer Science},

volume = {5330},

isbn = {978-3-540-89438-4}

}

@article{haberl:tautschnig:baumgarten:ijcs,

author = {Wolfgang Haberl and Michael Tautschnig and Uwe Baumgarten},

title = {{From COLA Models to Distributed Embedded Systems Code}},

number = {3},

month = {September},

year = {2008},

journal = {IAENG International Journal of Computer Science},

pages = {427--437},

volume = {35},

issn = {1819-656X}

}

@article{Kinder:Katzenbeisser:Schallhart:Veith:ProactiveDetection,

author = {Johannes Kinder and Stefan Katzenbeisser and Christian Schallhart and Helmut Veith},

title = {Proactive Detection of Computer Worms Using Model Checking},

year = {2008},

howpublished = {preprint},

journal = {IEEE Transactions on Dependable and Secure Computing}

}

@inproceedings{kugele:haberl:tautschnig:wechs:isola08,

author = {Stefan Kugele and Wolfgang Haberl and Michael Tautschnig and Martin Wechs},

title = {Optimizing Automatic Deployment Using Non-Functional Requirement Annotations},

month = {October},

year = {2008},

address = {Porto Sani, Greece},

booktitle = {Leveraging Applications of Formal Methods, Verification and Validation},

editor = {Tiziana Margaria and Bernhard Steffen},

pages = {400--414},

publisher = {Springer},

series = {Communications in Computer and Information Science},

volume = {17},

isbn = {978-3-540-88478-1}

}

@inproceedings{langer:tautschnig:isola08,

author = {Boris Langer and Michael Tautschnig},

title = {Navigating the Requirements Jungle},

month = {October},

year = {2008},

address = {Porto Sani, Greece},

booktitle = {Leveraging Applications of Formal Methods, Verification and Validation},

editor = {Tiziana Margaria and Bernhard Steffen},

pages = {354--368},

publisher = {Springer},

series = {Communications in Computer and Information Science},

volume = {17},

isbn = {978-3-540-88478-1}

}

@inproceedings{wang:herkersdorf:merenda:tautschnig:fdl08,

author = {Zhonglei Wang and Andreas Herkersdorf and Stefano Merenda and Michael Tautschnig},

title = {A Model Driven Development Approach for Implementing Reactive Systems in Hardware},

month = {September},

year = {2008},

address = {Stuttgart, Germany},

booktitle = {Forum on Specification and Design Languages (FDL08)},

pages = {197--202},

publisher = {IEEE Computer Society},

doi = {10.1109/FDL.2008.4641445}

}

@inproceedings{kugele:haberl:serp08,

author = {Stefan Kugele and Wolfgang Haberl},

title = {{Mapping Data-Flow Dependencies onto Distributed Embedded Systems}},

month = {July},

year = {2008},

address = {Las Vegas Nevada, USA},

booktitle = {{Proceedings of the 2008 International Conference on Software Engineering Research & Practice, SERP 2008}}

}

@inproceedings{holzer:schallhart:tautschnig:veith:cav08,

author = {Andreas Holzer and Christian Schallhart and Michael Tautschnig and Helmut Veith},

title = {{FShell: Systematic Test Case Generation for Dynamic Analysis and Measurement}},

month = {July},

year = {2008},

address = {Princeton, NJ, USA},

booktitle = {Proceedings of the 20th International Conference on Computer Aided Verification (CAV 2008)},

pages = {209--213},

publisher = {Springer},

series = {Lecture Notes in Computer Science},

volume = {5123}

}

@inproceedings{KinderVeith-jakstabcav08,

author = {Johannes Kinder and Helmut Veith},

title = {Jakstab: A Static Analysis Platform for Binaries},

month = {July},

year = {2008},

booktitle = {Proceedings of the 20th International Conference on Computer Aided Verification (CAV 2008)},

publisher = {Springer},

series = {Lecture Notes in Computer Science},

volume = {5123}

}

@inproceedings{ec2:talpur:veith08,

author = {Murali Talupur and Helmut Veith},

title = {Domain Pattern Abstraction + Ptolemaic Abstract Domains = Environment Abstraction for Concurrent Systems},

month = {July},

year = {2008},

booktitle = {Exploiting Concurrency Efficiently and Correctly -- (EC)$^2$}

}

@inproceedings{wang:haberl:kugele:tautschnig:wosp08,

author = {Zhonglei Wang and Wolfgang Haberl and Stefan Kugele and Michael Tautschnig},

title = {{Automatic Generation of SystemC Models from Component-based Designs for Early Design Validation and Performance Analysis}},

month = {June},

year = {2008},

address = {Princeton, NJ, USA},

booktitle = {WOSP '08: Proceedings of the 7th International Workshop on Software and Performance},

pages = {139--144},

publisher = {ACM},

isbn = {978-1-59593-873-2},

keywords = {COLA, Code Generation, Simulation, SystemC}

}

@inproceedings{buente:tautschnig:testbench08,

author = {Sven B\"unte and Michael Tautschnig},

title = {{A Benchmarking Suite for Measurement-Based WCET Analysis Tools}},

month = {April},

year = {2008},

address = {Lillehammer, Norway},

booktitle = {International Conference on Software Testing Verification and Validation Workshop (ICSTW'08)},

pages = {353--356},

publisher = {IEEE Computer Society Press},

isbn = {978-0-7695-3388-9},

doi = {10.1109/ICSTW.2008.1}

}

@inproceedings{DBLP:conf/tacas/ClarkeTV08,

author = {Edmund M. Clarke and Muralidhar Talupur and Helmut Veith},

title = {Proving Ptolemy Right: The Environment Abstraction Framework for Model Checking Concurrent Systems},

month = {April},

year = {2008},

booktitle = {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},

editor = {C. R. Ramakrishnan and Jakob Rehof},

pages = {33--47},

publisher = {Springer},

series = {Lecture Notes in Computer Science},

volume = {4963},

isbn = {978-3-540-78799-0},

url = {http://dx.doi.org/10.1007/978-3-540-78800-3_4}

}

@inproceedings{haberl:tautschnig:baumgarten:iaeng08,

author = {Wolfgang Haberl and Michael Tautschnig and Uwe Baumgarten},

title = {{Running COLA on Embedded Systems}},

month = {March},

year = {2008},

address = {Hongkong, China},

booktitle = {Proceedings of The International MultiConference of Engineers and Computer Scientists 2008},

pages = {922--928},

isbn = {9789889867188},

keywords = {embedded systems, component-based models, automated code generation}

}

@inproceedings{Sam08LPAR,

author = {Marko Samer},

title = {Variable Dependencies of Quantified CSPs},

year = {2008},

booktitle = {Proceedings of the 15th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'08)},

pages = {512--527},

publisher = {Springer-Verlag},

series = {Lecture Notes in Computer Science},

volume = {5330},

abstract = {Quantified constraint satisfaction extends classical constraint satisfaction by a linear order of the variables and an associated existential or universal quantifier to each variable. In general, the semantics of the quantifiers does not allow to change the linear order of the variables arbitrarily without affecting the truth value of the instance. In this paper we investigate variable dependencies that are caused by the influence of the relative order between these variables on the truth value of the instance. Several approaches have been proposed in the literature for identifying such dependencies in the context of quantified Boolean formulas. We generalize these ideas to quantified constraint satisfaction and present new concepts that allow a refined analysis.},

isbn = {978-3-540-89438-4},

doi = {10.1007/978-3-540-89439-1_36}

}

@inproceedings{leucker08:_impar_antic_in_runtim_verif,

author = {Wei Dong and Martin Leucker and Christian Schallhart},

title = {{Impartial Anticipation in Runtime-Verification}},

year = {2008},

booktitle = {{Automated Technology for Verification and Analysis (ATVA'08)}},

pages = {386--396},

series = {Lecture Notes in Computer Science (LNCS)},

volume = {5311}

}

@inproceedings{januzaj:IASH08,

author = {Visar Januzaj},

title = {{Towards Improvements in Design and Analysis of Embedded Systems (Abstract)}},

month = {1 - 3 September},

year = {2008},

address = {Tirana, Albania},

booktitle = {{Proceedings of the 3rd Annual Meeting of Institute Alb-Shkenca}},

isbn = {978-99943-47-80-3}

}

@techreport{holzer:schallhart:tautschnig:veith:vmcai09techreport,

author = {Andreas Holzer and Christian Schallhart and Michael Tautschnig and Helmut Veith},

title = {Query-Driven Program Testing},

number = {TUD-CS-2008-1013},

month = {October},

year = {2008},

institution = {Technische Universit\"at Darmstadt},

pdf = {/data/publications/1408_TUD-CS-2008-1013.pdf}

}

@techreport{bauer08:_good_bad_ugly,

author = {Andreas Bauer and Martin Leucker and Christian Schallhart},

title = {The good, the bad, the ugly---but how ugly is ugly?},

number = {{TUM-I0803}},

month = {February},

year = {2008},

institution = {{Institut f{\"u}r Informatik, Technische Universit{\"a}t M{\"u}nchen}}

}

@article{ChristodorescuKinderJhaKatzenbeisserVeith-jicv07,

author = {Mihai Christodorescu and Johannes Kinder and Somesh Jha and Stefan Katzenbeisser and Helmut Veith},

title = {Software Transformations to Improve Malware Detection},

number = {4},

month = {November},

year = {2007},

journal = {Journal in Computer Virology},

pages = {253--265},

volume = {3},

abstract = {Malware is code designed for a malicious purpose, such as obtaining root privilege on a host. A malware detector identifies malware and thus prevents it from adversely affecting a host. In order to evade detection, malware writers use various obfuscation techniques to transform their malware. There is strong evidence that commercial malware detectors are susceptible to these evasion tactics. In this paper, we describe the design and implementation of a malware transformer that reverses the obfuscations performed by a malware writer. Our experimental evaluation demonstrates that this malware transformer can drastically improve the detection rates of commercial malware detectors.}

}

@inproceedings{bauer:leucker:schallhart:tautschnig:isola07,

author = {Andreas Bauer and Martin Leucker and Christian Schallhart and Michael Tautschnig},

title = {Don't care in {SMT}---Building flexible yet efficient abstraction/refinement solvers},

month = {December},

year = {2007},

address = {Poitiers, France},

booktitle = {Proceedings of the 2007 ISoLA Workshop On Leveraging Applications of Formal Methods, Verification and Validation (ISoLA)},

pages = {135--146},

isbn = {9782854288148}

}

@inproceedings{kuehnel:bauer:tautschnig:ecbse07,

author = {Christian K{\"u}hnel and Andreas Bauer and Michael Tautschnig},

title = {Compatibility and reuse in component-based systems via type and unit inference},

month = {August},

year = {2007},

address = {L\"ubeck, Germany},

booktitle = {Proceedings of the 33rd EUROMICRO Conference on Software Engineering and Advanced Applications (SEAA)},

pages = {101--108},

publisher = {IEEE Computer Society Press},

issn = {1089-6503},

doi = {10.1109/EUROMICRO.2007.24}

}

@inproceedings{bauer:pister:tautschnig:date07,

author = {Andreas Bauer and Markus Pister and Michael Tautschnig},

title = {Tool-support for the analysis of hybrid systems and models},

month = {April},

year = {2007},

address = {Nice, France},

booktitle = {Proceedings of the 2007 Conference on Design, Automation and Test in Europe (DATE)},

pages = {924--929},

publisher = {European Design and Automation Association},

abstract = {This paper introduces a method and tool-support for the automatic analysis and verification of hybrid and embedded control systems, whose continuous dynamics are often modelled using MATLAB/Simulink. The method is based upon converting system models into the uniform input language of our efficient multi-domain constraint solving library, ABsolver, which is then used for subsequent analysis. Basically, ABsolver is an extensible SMT-solver which addresses mixed Boolean and (nonlinear) arithmetic constraint problems as they appear in the design of hybrid control systems. It allows the integration and semantic connection of various domain specific solvers via a logical circuit, such that almost arbitrary multi-domain constraint problems can be formulated and solved. Its design has been tailored for extensibility, and thus facilitates the reuse of expert knowledge, in that the most appropriate solver for a given task can be integrated and used. As such the only constraint over the problem domain is the capability of the employed solvers. Our approach to systems verification has been validated in an industrial case study using the model of a car's steering control system. However, additional benchmarks show that other hard instances of problems could also be solved by ABsolver in respectable time, and that for some instances, ABsolver's approach was the only means of solving a problem at all.},

isbn = {978-3-9810801-2-4},

doi = {10.1109/DATE.2007.364411},

pdf = {/data/publications/253_date07.pdf}

}

@inproceedings{bauer07,

author = {Andreas Bauer and Martin Leucker and Christian Schallhart},

title = {{The good, the bad, and the ugly, but how ugly is ugly?}},

year = {2007},

booktitle = {Workshop on Runtime Verification (RV'07)},

pages = {126--138}

}

@inproceedings{chenny07:_enfor_seman_integ_untrus_clien,

author = {Somesh Jha and Stefan Katzenbeisser and Helmut Veith and Stephen Chenny},

title = {{Enforcing Semantic Integrity on Untrusted Clients in Networked Virtual Environments (Extended Abstract)}},

year = {2007},

booktitle = {IEEE Security and Privacy (S\&P'07)},

pages = {179--186}

}

@inproceedings{chaki07:_verif_acros_intel_proper_bound,

author = {Sagar Chaki and Christian Schallhart and Helmut Veith},

title = {{Verification Across Intellectual Property Boundaries}},

year = {2007},

booktitle = {{Computer Aided Verification (CAV'07)}},

pages = {82--94}

}

@inproceedings{HolzerKinderVeith-eurocast07,

author = {Andreas Holzer and Johannes Kinder and Helmut Veith},

title = {Using Verification Technology to Specify and Detect Malware},

year = {2007},

booktitle = {11th International Conference on Computer Aided Systems Theory (EUROCAST 2007)},

pages = {497--504},

publisher = {Springer},

series = {Lecture Notes in Computer Science},

volume = {4739},

abstract = {Computer viruses and worms are major threats for our computer infrastructure, and thus, for economy and society at large. Recent work has demonstrated that a model checking based approach to malware detection can capture the semantics of security exploits more accurately than traditional approaches, and consequently achieve higher detection rates. In this approach, malicious behavior is formalized using the expressive specification language CTPL based on classic CTL. This paper gives an overview of our toolchain for malware detection and presents our new system for computer assisted generation of malicious code specifications.}

}

@inproceedings{januzaj:cpn07,

author = {Visar Januzaj},

title = {CPNunf: A tool for McMillan's Unfolding of Coloured Petri Nets},

month = {22 - 24 October},

year = {2007},

address = {Aarhus, Denmark},

booktitle = {Eighth Workshop and Tutorial on Practical Use of Coloured Petri Nets and the CPN Tools},

editor = {Kurt Jensen},

howpublished = {DAIMI PB - 584},

issn = {0105-8517}

}

@phdthesis{schallhart07:_archit_secur_networ_virtual_envir,

author = {Christian Schallhart},

title = {{Architecture and Security in Networked Virtual Environments}},

year = {2007},

school = {Vienna University of Technology}

}

@techreport{tum-i0714,

author = {Stefan Kugele and Michael Tautschnig and Andreas Bauer and Christian Schallhart and Stefano Merenda and Wolfgang Haberl and Christian K{\"u}hnel and Florian M{\"uller} and Zhonglei Wang and Doris Wild and Sabine Rittmann and Martin Wechs},

title = {{COLA} -- The component language},

number = {TUM-I0714},

month = {September},

year = {2007},

institution = {Institut f{\"u}r Informatik, Technische Universit{\"a}t M{\"u}nchen}

}

@techreport{tum-i0716,

author = {Christian K{\"u}hnel and Andreas Bauer and Michael Tautschnig},

title = {Compatibility and reuse in component-based systems via type and unit inference},

number = {TUM-I0716},

month = {May},

year = {2007},

institution = {Institut f{\"u}r Informatik, Technische Universit{\"a}t M{\"u}nchen}

}

@techreport{bauer07:_runtim_verfic_ltl_tltl,

author = {Andreas Bauer and Martin Leucker and Christian Schallhart},

title = {{Runtime Verfication for LTL and TLTL}},

number = {{TUM-I0724}},

year = {2007},

institution = {{Institut f{\"u}r Informatik, Technische Universit{\"a}t M{\"u}nchen}}

}

@article{DBLP:journals/dam/PikhurkoVV06,

author = {Oleg Pikhurko and Helmut Veith and Oleg Verbitsky},

title = {The first order definability of graphs: Upper bounds for quantifier depth},

number = {17},

year = {2006},

journal = {Discrete Applied Mathematics},

pages = {2511--2529},

volume = {154},

url = {http://dx.doi.org/10.1016/j.dam.2006.03.002}

}

@inproceedings{bauer06:_monit_realt_proper,

author = {Andreas Bauer and Martin Leucker and Christian Schallhart},

title = {{Monitoring of Realtime Properties}},

year = {2006},

booktitle = {{Foundations of Software Technology and Theoretical Computer Science (FSTTCS'06)}},

pages = {260--272}

}

@inproceedings{bauer06:_runtim_reflec,

author = {Andreas Bauer and Martin Leucker and Christian Schallhart},

title = {{Runtime Reflection: Dynamic model-based analyis of component-based distributed embedded systems}},

year = {2006},

booktitle = {Modellierung von Automotive Systems}

}

@inproceedings{bauer06:_model_based_runtim_analy_distr_react_system,

author = {Andreas Bauer and Martin Leucker and Christian Schallhart},

title = {{Model-Based Runtime Analysis of Distributed Reactive Systems}},

year = {2006},

booktitle = {Australian Software Engineering Conference (ASWEC'06)},

pages = {243--252}

}

@inproceedings{DBLP:conf/vmcai/ClarkeTV06,

author = {Edmund M. Clarke and Muralidhar Talupur and Helmut Veith},

title = {Environment Abstraction for Parameterized Verification},

year = {2006},

booktitle = {Verification, Model Checking, and Abstract Interpretation, 7th International Conference, VMCAI 2006, Charleston, SC, USA, January 8-10, 2006, Proceedings},

editor = {E. Allen Emerson and Kedar S. Namjoshi},

pages = {126--141},

publisher = {Springer},

isbn = {3-540-31139-4},

url = {http://dx.doi.org/10.1007/11609773\_9}

}

@inproceedings{DBLP:conf/vissas/SamerV05,

author = {Marko Samer and Helmut Veith},

title = {From Temporal Logic Queries to Vacuity Detection},

year = {2006},

booktitle = {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},

editor = {Edmund M. Clarke and Marius Minea and Ferucio Laurentiu Tiplea},

pages = {149--167},

publisher = {IOS Press},

series = {NATO Security through Science Series D: Information and Communication Security},

volume = {1},

isbn = {1-58603-570-3}

}

@mastersthesis{tautschnig:diploma06,

author = {Michael Tautschnig},

title = {Development of a tool to solve mixed logical/linear constraint problems},

month = {February},

year = {2006},

school = {Technische Universit{\"a}t M{\"u}nchen},

abstract = {The problem of solving mixed arithmetic and Boolean constraint systems arises in many different areas, such as verification of soft- and hardware systems, resource planning or system design and has been studied extensively in recent time. Yet, the available solvers are neither easily extensible, nor do they offer ways to apply problem specific heuristics that are required for most of the hard problems in this area.\par

To overcome these limitations, a framework has been designed to integrate state-of-the-art solvers for the Boolean- and parts of the arithmetic domain to solve the combined problem. Thereby we benefit from the full strength of each of the tools in their special area. Furthermore, the architecture of the system emphasises extensibility, which already proved useful for the implemented extension to non-linear arithmetic constraints.\par

The results show that our implementation, albeit in in some parts not yet more than a proof of concept, can already compete with existing solvers. Due to the extension to non-linear arithmetic we are even able to tackle a new class of real-world problems.\par

The present work introduces this class of problems and our approach to solve them, accompanied by some real-life examples. Along with these descriptions we provide detailed insight into our tool and the hurdles we had to overcome.}

}

@article{schallhart05:_approx_succin_maxsat,

author = {Christian Schallhart and Luca Trevisan},

title = {{Approximating Succinct MaxSat}},

number = {4},

year = {2005},

journal = {{Journal of Logic and Computation (JLC)}},

pages = {551--557},

volume = {15}

}

@inbook{belinfante05:_model_based_testin_react_system,

author = {Axel Belinfante and Lars Franzen and Christian Schallhart},

title = {{Model-Based Testing of Reactive Systems}},

year = {2005},

chapter = {{Tools for Test Case Generation}},

pages = {391--438},

publisher = {Springer},

series = {Lecture Notes in Computer Science},

volume = {3472}

}

@incollection{DBLP:books/sp/necs2005/ClarkeFJV05,

author = {Edmund M. Clarke and Ansgar Fehnker and Sumit Kumar Jha and Helmut Veith},

title = {Temporal Logic Model Checking},

year = {2005},

booktitle = {Handbook of Networked and Embedded Control Systems},

editor = {Dimitrios Hristu-Varsakelis and William S. Levine},

pages = {539--558},

publisher = {Birkh{\"a}user},

isbn = {0-8176-3239-5}

}

@article{DBLP:journals/logcom/ChakiCJV05,

author = {Sagar Chaki and Edmund M. Clarke and Somesh Jha and Helmut Veith},

title = {An Iterative Framework for Simulation Conformance},

number = {4},

year = {2005},

journal = {J. Log. Comput.},

pages = {465--488},

volume = {15},

url = {http://dx.doi.org/10.1093/logcom/exi028}

}

@inproceedings{vstte2005:clarke:gupta:jain:veith06,

author = {Edmund M. Clarke and Aarti Gupta and Himanshu Jain and Helmut Veith},

title = {Model Checking: Back and Forth between Hardware and Software},

month = {October},

year = {2005},

booktitle = {Verified Software: Theories, Tools, Experiments}

}

@inproceedings{KinderKatzenbeisserSchallhartVeith-mcodedimva05,

author = {Johannes Kinder and Stefan Katzenbeisser and Christian Schallhart and Helmut Veith},

title = {Detecting Malicious Code by Model Checking},

month = {July},

year = {2005},

address = {Vienna, Austria},

booktitle = {GI SIG SIDAR Conference on Detection of Intrusions and Malware \& Vulnerability Assessment (DIMVA'05)},

editor = {Klaus Julisch and Christopher Kr{\"u}gel},

pages = {174--187},

publisher = {Springer},

series = {Lecture Notes in Computer Science},

volume = {3548},

abstract = {The ease of compiling malicious code from source code in higher programming languages has increased the volatility of malicious programs: The first appearance of a new worm in the wild is usually followed by modified versions in quick succession. As demonstrated by Christodorescu and Jha, however, classical detection software relies on static patterns, and is easily outsmarted. In this paper, we present a flexible method to detect malicious code patterns in executables by model checking. While model checking was originally developed to verify the correctness of systems against specifications, we argue that it lends itself equally well to the specification of malicious code patterns. To this end, we introduce the specification language CTPL (Computation Tree Predicate Logic) which extends the well-known logic CTL, and describe an efficient model checking algorithm. Our practical experiments demonstrate that we are able to detect a large number of worm variants with a single specification.},

isbn = {3-540-26613-5},

url = {http://dx.doi.org/10.1007/11506881\_11}

}

@inproceedings{DBLP:conf/ifm/ChakiCGOSTV05,

author = {Sagar Chaki and Edmund M. Clarke and Orna Grumberg and Jo{\"e}l Ouaknine and Natasha Sharygina and Tayssir Touili and Helmut Veith},

title = {State/Event Software Verification for Branching-Time Specifications},

year = {2005},

booktitle = {Integrated Formal Methods, 5th International Conference, IFM 2005, Eindhoven, The Netherlands, November 29 - December 2, 2005, Proceedings},

editor = {Judi Romijn and Graeme Smith and Jaco van de Pol},

pages = {53--69},

publisher = {Springer},

isbn = {3-540-30492-4},

url = {http://dx.doi.org/10.1007/11589976\_5}

}

@inproceedings{DBLP:conf/sec/DittmannKSV05,

author = {Jana Dittmann and Stefan Katzenbeisser and Christian Schallhart and Helmut Veith},

title = {Ensuring Media Integrity on Third-Party Infrastructures},

year = {2005},

booktitle = {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},

editor = {Ry{\^o}ichi Sasaki and Sihan Qing and Eiji Okamoto and Hiroshi Yoshiura},

pages = {493--508},

publisher = {Springer},

isbn = {0-387-25658-X}

}

@inproceedings{DBLP:conf/sicherheit/KatzenbeisserSV05,

author = {Stefan Katzenbeisser and Christian Schallhart and Helmut Veith},

title = {Malware Engineering},

year = {2005},

booktitle = {Sicherheit 2005: Sicherheit - Schutz und Zuverl{\"a}ssigkeit, Beitr{\"a}ge der 2. Jahrestagung des Fachbereichs Sicherheit der Gesellschaft f{\"u}r Informatik e.v. (GI), 5.-8. April 2005 in Regensburg},

editor = {Hannes Federrath},

pages = {139--148},

publisher = {GI},

isbn = {3-88579-391-1}

}

@inproceedings{DBLP:conf/time/SamerV05,

author = {Marko Samer and Helmut Veith},

title = {Deterministic CTL Query Solving},

year = {2005},

booktitle = {12th International Symposium on Temporal Representation and Reasoning (TIME 2005), 23-25 June 2005, Burlington, Vermont, USA},

pages = {156--165},

publisher = {IEEE Computer Society},

isbn = {0-7695-2370-6},

url = {http://dx.doi.org/10.1109/TIME.2005.20}

}

@inproceedings{koppensteiner:veith05,

author = {Peter Koppensteiner and Helmut Veith},

title = {A Novel SAT Procedure for Linear Real Arithmetic},

year = {2005},

booktitle = {Third Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR 2005)}

}

@techreport{ChristodorescuKinderJhaKatzenbeisserVeith-malnorm2005,

author = {Mihai Christodorescu and Johannes Kinder and Somesh Jha and Stefan Katzenbeisser and Helmut Veith},

title = {Malware Normalization},

number = {1539},

month = {November},

year = {2005},

address = {Wisconsin, USA},

institution = {University of Wisconsin, Madison},

abstract = {Malware is code designed for a malicious purpose, such as obtaining root privilege on a host. A malware detector identifies malware and thus prevents it from adversely affecting a host. In order to evade detection by malware detectors, malware writers use various obfuscation techniques to transform their malware. There is strong evidence that commercial malware detectors are susceptible to these evasion tactics. In this paper, we describe the design and implementation of a malware normalizer that undoes the obfuscations performed by a malware writer. Our experimental evaluation demonstrates that a malware normalizer can drastically improve detection rates of commercial malware detectors. Moreover, a malware normalizer can also ease the task of forensic analysis of malware.}

}

@techreport{arafat:bauer:leucker:schallhart:TUM:05,

author = {Oliver Arafat and Andreas Bauer and Martin Leucker and Christian Schallhart},

title = {{Runtime verification revisited}},

number = {TUM-I0518},

year = {2005},

institution = {Technische Universit\"at M\"unchen}

}

@article{DBLP:journals/tse/ChakiCGJV04,

author = {Sagar Chaki and Edmund M. Clarke and Alex Groce and Somesh Jha and Helmut Veith},

title = {Modular Verification of Software Components in C},

number = {6},

year = {2004},

journal = {IEEE Trans. Software Eng.},

pages = {388--402},

volume = {30},

url = {http://doi.ieeecomputersociety.org/10.1109/TSE.2004.22}

}

@inproceedings{holzer04:_towar_odrl,

author = {Markus Holzer and Stefan Katzenbeisser and Christian Schallhart},

title = {Towards a formal semantics for ODRL},

year = {2004},

booktitle = {First ODRL International Workshop},

pages = {137--148}

}

@inproceedings{DBLP:conf/concur/ClarkeTTV04,

author = {Edmund M. Clarke and Muralidhar Talupur and Tayssir Touili and Helmut Veith},

title = {Verification by Network Decomposition},

year = {2004},

booktitle = {CONCUR 2004 - Concurrency Theory, 15th International Conference, London, UK, August 31 - September 3, 2004, Proceedings},

editor = {Philippa Gardner and Nobuko Yoshida},

pages = {276--291},

publisher = {Springer},

isbn = {3-540-22940-X},

url = {http://springerlink.metapress.com/openurl.asp?genre$=\&issn$=$0% 302-9743\&volume$=$3170\&spage$=$276}

}

@inproceedings{DBLP:conf/fmcad/SamerV04,

author = {Marko Samer and Helmut Veith},

title = {Parameterized Vacuity},

year = {2004},

booktitle = {Formal Methods in Computer-Aided Design, 5th International Confrence, FMCAD 2004, Austin, Texas, USA, November 15-17, 2004, Proceedings},

editor = {Alan J. Hu and Andrew K. Martin},

pages = {322--336},

publisher = {Springer},

isbn = {3-540-23738-0},

url = {http://springerlink.metapress.com/openurl.asp?genre$=\&issn$=$0% 302-9743\&volume$=$3312\&spage$=$322}

}

@inproceedings{DBLP:conf/icalp/SamerV04,

author = {Marko Samer and Helmut Veith},

title = {A Syntactic Characterization of Distributive LTL Queries},

year = {2004},

booktitle = {Automata, Languages and Programming: 31st International Colloquium, ICALP 2004, Turku, Finland, July 12-16, 2004. Proceedings},

editor = {Josep D\'{\i}az and Juhani Karhum{\"a}ki and Arto Lepist{\"o} and Donald Sannella},

pages = {1099--1110},

publisher = {Springer},

isbn = {3-540-22849-7},

url = {http://springerlink.metapress.com/openurl.asp?genre$=\&issn$=$0% 302-9743\&volume$=$3142\&spage$=$1099}

}

@article{DBLP:journals/jacm/ClarkeGJLV03,

author = {Edmund M. Clarke and Orna Grumberg and Somesh Jha and Yuan Lu and Helmut Veith},

title = {Counterexample-guided abstraction refinement for symbolic model checking},

number = {5},

year = {2003},

journal = {J. ACM},

pages = {752--794},

volume = {50},

url = {http://doi.acm.org/10.1145/876638.876643}

}

@inproceedings{schallhart03:trans,

author = {Christian Schallhart},

title = {{Transaction Processing for Clustered Virtual Environments}},

month = {July},

year = {2003},

booktitle = {{NATO Advanced Research Workshop on Concurrent Information Processing and Computing}},

pages = {146--158}

}

@inproceedings{DBLP:conf/csl/SamerV03,

author = {Marko Samer and Helmut Veith},

title = {Validity of CTL Queries Revisited},

year = {2003},

booktitle = {Computer Science Logic, 17th International Workshop, CSL 2003, 12th Annual Conference of the EACSL, and 8th Kurt G{\"u}del Colloquium, KGC 2003, Vienna, Austria, August 25-30, 2003, Proceedings},

editor = {Matthias Baaz and Johann A. Makowsky},

pages = {470--483},

publisher = {Springer},

isbn = {3-540-40801-0},

url = {http://springerlink.metapress.com/openurl.asp?genre$=\&issn$=$0% 302-9743\&volume$=$2803\&spage$=$470}

}

@inproceedings{DBLP:conf/csl/Veith03,

author = {Helmut Veith},

title = {Friends or Foes? Communities in Software Verification (Invited Lecture)},

year = {2003},

booktitle = {Computer Science Logic, 17th International Workshop, CSL 2003, 12th Annual Conference of the EACSL, and 8th Kurt G{\"u}del Colloquium, KGC 2003, Vienna, Austria, August 25-30, 2003, Proceedings},

editor = {Matthias Baaz and Johann A. Makowsky},

pages = {528--529},

publisher = {Springer},

isbn = {3-540-40801-0},

url = {http://springerlink.metapress.com/openurl.asp?genre$=\&issn$=$0% 302-9743\&volume$=$2803\&spage$=$528}

}

@inproceedings{DBLP:conf/drm/AdelsbachKV03,

author = {Andr{\'e} Adelsbach and Stefan Katzenbeisser and Helmut Veith},

title = {Watermarking schemes provably secure against copy and ambiguity attacks},

year = {2003},

booktitle = {Proceedings of the 2003 ACM workshop on Digital rights management 2003, Washington, DC, USA, October 27, 2003},

editor = {Moti Yung},

pages = {111--119},

publisher = {ACM},

isbn = {1-58113-786-9},

url = {http://doi.acm.org/10.1145/947380.947395}

}

@inproceedings{DBLP:conf/icse/ChakiCGJV03,

author = {Sagar Chaki and Edmund M. Clarke and Alex Groce and Somesh Jha and Helmut Veith},

title = {Modular Verification of Software Components in C},

year = {2003},

booktitle = {Proceedings of the 25th International Conference on Software Engineering, May 3-10, 2003, Portland, Oregon, USA},

pages = {385--395},

publisher = {IEEE Computer Society},

url = {http://computer.org/proceedings/icse/1877/18770385abs.htm}

}

@inproceedings{DBLP:conf/sat/ClarkeTVW03,

author = {Edmund M. Clarke and Muralidhar Talupur and Helmut Veith and Dong Wang},

title = {SAT Based Predicate Abstraction for Hardware Verification},

year = {2003},

booktitle = {Theory and Applications of Satisfiability Testing, 6th International Conference, SAT 2003. Santa Margherita Ligure, Italy, May 5-8, 2003 Selected Revised Papers},

editor = {Enrico Giunchiglia and Armando Tacchella},

pages = {78--92},

publisher = {Springer},

isbn = {3-540-20851-8},

url = {http://springerlink.metapress.com/openurl.asp?genre$=\&issn$=$0% 302-9743\&volume$=$2919\&spage$=$78}

}

@inproceedings{DBLP:conf/seke/ChakiFGJKV03,

author = {Sagar Chaki and Pascal Fenkam and Harald Gall and Somesh Jha and Engin Kirda and Helmut Veith},

title = {Integrating Publish/Subscribe into a Mobile Teamwork Support Platform},

year = {2003},

booktitle = {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}

}

@inproceedings{DBLP:conf/birthday/ClarkeV03,

author = {Edmund M. Clarke and Helmut Veith},

title = {Counterexamples Revisited: Principles, Algorithms, Applications},

year = {2003},

booktitle = {Verification: Theory and Practice, Essays Dedicated to Zohar Manna on the Occasion of His 64th Birthday},

editor = {Nachum Dershowitz},

pages = {208--224},

publisher = {Springer},

isbn = {3-540-21002-4},

url = {http://springerlink.metapress.com/openurl.asp?genre$=\&issn$=$0% 302-9743\&volume$=$2772\&spage$=$208}

}

@techreport{schallhart03:_atom_middl_massiv_paral_multi,

author = {Christian Schallhart and Georg Gottlob and Helmut Veith},

title = {The ATOM Middleware for Massively Parallel Multi-Player Online Games},

number = {DBAI-TR-2003-48},

month = {March},

year = {2003},

institution = {Vienna University of Technology, Database and Artificial Intelligence Group}

}

@article{DBLP:journals/tocl/GottlobGV02,

author = {Georg Gottlob and Erich Gr{\"a}del and Helmut Veith},

title = {Datalog LITE: a deductive query language with linear time model checking},

number = {1},

year = {2002},

journal = {ACM Trans. Comput. Log.},

pages = {42--79},

volume = {3},

url = {http://doi.acm.org/10.1145/504077.504079}

}

@article{DBLP:journals/tcs/EiterV02,

author = {Thomas Eiter and Helmut Veith},

title = {On the complexity of data disjunctions},

number = {1},

year = {2002},

journal = {Theor. Comput. Sci.},

pages = {101--128},

volume = {288}

}

@inproceedings{DBLP:conf/fmcad/ChauhanCKSVW02,

author = {Pankaj Chauhan and Edmund M. Clarke and James H. Kukula and Samir Sapra and Helmut Veith and Dong Wang},

title = {Automated Abstraction Refinement for Model Checking Large State Spaces Using SAT Based Conflict Analysis},

year = {2002},

booktitle = {Formal Methods in Computer-Aided Design, 4th International Conference, FMCAD 2002, Portland, OR, USA, November 6-8, 2002, Proceedings},

editor = {Mark Aagaard and John W. O'Leary},

pages = {33--51},

publisher = {Springer},

isbn = {3-540-00116-6},

url = {http://link.springer.de/link/service/series/0558/bibs/2517/25170033.htm}

}

@inproceedings{DBLP:conf/lics/ClarkeJLV02,

author = {Edmund M. Clarke and Somesh Jha and Yuan Lu and Helmut Veith},

title = {Tree-Like Counterexamples in Model Checking},

year = {2002},

booktitle = {17th IEEE Symposium on Logic in Computer Science (LICS 2002), 22-25 July 2002, Copenhagen, Denmark, Proceedings},

pages = {19--29},

publisher = {IEEE Computer Society},

isbn = {0-7695-1483-9},

url = {http://computer.org/proceedings/lics/1483/14830019abs.htm}

}

@inproceedings{katzenbeisser02securing,

author = {Stefan Katzenbeisser and Helmut Veith},

title = {Securing Symmetric Watermarking Schemes Against Protocol Attacks},

year = {2002},

booktitle = {Security and Watermarking of Multimedia Contents IV},

pages = {260--268},

series = {SPIE},

volume = {4675}

}

@article{DBLP:journals/apal/BaazH01,

author = {Matthias Baaz and Petr H{\'a}jek and Franco Montagna and Helmut Veith},

title = {Complexity of t-tautologies},

number = {1-3},

year = {2001},

journal = {Ann. Pure Appl. Logic},

pages = {3--11},

volume = {113}

}

@inproceedings{DBLP:conf/charme/ChauhanCJKVW01,

author = {Pankaj Chauhan and Edmund M. Clarke and Somesh Jha and James H. Kukula and Helmut Veith and Dong Wang},

title = {Using Combinatorial Optimization Methods for Quantification Scheduling},

year = {2001},

booktitle = {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},

editor = {Tiziana Margaria and Thomas F. Melham},

pages = {293--309},

publisher = {Springer},

isbn = {3-540-42541-1},

url = {http://link.springer.de/link/service/series/0558/bibs/2144/21440293.htm}

}

@inproceedings{DBLP:conf/iccad/ChauhanCJKSVW01,

author = {Pankaj Chauhan and Edmund M. Clarke and Somesh Jha and James H. Kukula and Thomas R. Shiple and Helmut Veith and Dong Wang},

title = {Non-linear Quantification Scheduling in Image Computation},

year = {2001},

booktitle = {ICCAD},

pages = {293--},

url = {http://www.sigda.org/Archives/ProceedingArchives/Iccad/Iccad2001/papers/% 2001/iccad01/htmfiles/sun\_sgi/iccadabs.htm\#06a\_3}

}

@inproceedings{DBLP:conf/icse/CampaillaCCJV01,

author = {Alexis Campailla and Sagar Chaki and Edmund M. Clarke and Somesh Jha and Helmut Veith},

title = {Efficient Filtering in Publish-Subscribe Systems Using Binary Decision Diagrams},

year = {2001},

booktitle = {Proceedings of the 23rd International Conference on Software Engineering, ICSE 2001, 12-19 May 2001, Toronto, Ontario, Canada},

pages = {443--452},

publisher = {IEEE Computer Society},

isbn = {0-7695-1050-7}

}

@inproceedings{DBLP:conf/dagstuhl/ClarkeGJLV01,

author = {Edmund M. Clarke and Orna Grumberg and Somesh Jha and Yuan Lu and Helmut Veith},

title = {Progress on the State Explosion Problem in Model Checking},

year = {2001},

booktitle = {Informatics - 10 Years Back. 10 Years Ahead.},

editor = {Reinhard Wilhelm},

pages = {176--194},

publisher = {Springer},

isbn = {3-540-41635-8},

url = {http://link.springer.de/link/service/series/0558/bibs/2000/20000176.htm}

}

@inproceedings{qbf2001:veith01,

author = {Matthias Baaz and Agata Ciabattoni and Norbert Preining and Helmut Veith},

title = {A Guide to Quantified Propositional G{\"o}del Logic},

year = {2001},

booktitle = {Workshop on Theory and Applications of Quantified Boolean Formulas (QBF 2001)}

}

@article{566376,

author = {Georg Gottlob and Erich Gr\"{a}del and Helmut Veith},

title = {Linear time datalog and branching time logic},

year = {2000},

address = {Norwell, MA, USA},

booktitle = {Logic-based artificial intelligence},

pages = {443--467},

publisher = {Kluwer Academic Publishers},

isbn = {0-7923-7224-7}

}

@inproceedings{DBLP:conf/cav/ClarkeGJLV00,

author = {Edmund M. Clarke and Orna Grumberg and Somesh Jha and Yuan Lu and Helmut Veith},

title = {Counterexample-Guided Abstraction Refinement},

year = {2000},

booktitle = {Computer Aided Verification, 12th International Conference, CAV 2000, Chicago, IL, USA, July 15-19, 2000, Proceedings},

editor = {E. Allen Emerson and A. Prasad Sistla},

pages = {154--169},

publisher = {Springer},

isbn = {3-540-67770-4}

}

@inproceedings{DBLP:conf/fmcad/ClarkeGLVW00,

author = {Edmund M. Clarke and Steven M. German and Yuan Lu and Helmut Veith and Dong Wang},

title = {Executable Protocol Specification in ESL},

year = {2000},

booktitle = {Formal Methods in Computer-Aided Design, Third International Conference, FMCAD 2000, Austin, Texas, USA, November 1-3, 2000, Proceedings},

editor = {Warren A. Hunt Jr. and Steven D. Johnson},

pages = {197--216},

publisher = {Springer},

isbn = {3-540-41219-0},

url = {http://link.springer.de/link/service/series/0558/bibs/1954/19540197.htm}

}

@inproceedings{DBLP:conf/tableaux/BaazFV00,

author = {Matthias Baaz and Christian G. Ferm{\"u}ller and Helmut Veith},

title = {An Analytic Calculus for Quantified Propositional G{\"o}del Logic},

year = {2000},

booktitle = {Automated Reasoning with Analytic Tableaux and Related Methods, International Conference, TABLEAUX 2000, St Andrews, Scotland, UK, July 3-7, 2000, Proceedings},

editor = {Roy Dyckhoff},

pages = {112--126},

publisher = {Springer},

isbn = {3-540-67697-X}

}

@inproceedings{BaazVeith99LC,

author = {Matthias Baaz and Helmut Veith},

title = {An axiomatization of quantified proposition {G\"odel} logic using the {Takeuti}-{Titani} rule},

year = {2000},

address = {Prague},

booktitle = {Logic Colloquium 1998},

pages = {91--104},

publisher = {Association for Symbolic Logic},

series = {Lecture Notes in Logic},

volume = {13},

isbn = {1-56881-113-6}

}

@mastersthesis{schallhart00:_applic_approx_theor_succin_data_repres,

author = {Christian Schallhart},

title = {Application of Approximation Theory to Succinct Data Representation},

year = {2000},

school = {Vienna University of Technology}

}

@article{DBLP:journals/apal/GottlobLV99,

author = {Georg Gottlob and Nicola Leone and Helmut Veith},

title = {Succinctness as a Source of Complexity in Logical Formalisms},

number = {1-3},

year = {1999},

journal = {Ann. Pure Appl. Logic},

pages = {231--260},

volume = {97}

}

@article{BaazVeith99,

author = {Matthias Baaz and Helmut Veith},

title = {Interpolation in Fuzzy Logic},

year = {1999},

journal = {Archive for Mathematical Logic},

pages = {461--489},

volume = {38}

}

@article{dorn99,

author = {J{\"u}rgen Dorn and Anna Prianichnikova and Markus Stumptner and Helmut Veith and Johannes Reisinger and Ralf Schlatterbeck},

title = {Multiprocessor Scheduling using the D{\'E}J{\`A} VU Scheduling Class Library},

year = {1999},

journal = {{\"O}GAI (Journal of the Austrian Society for AI)},

pages = {16--25},

volume = {4}

}

@inproceedings{DBLP:conf/fsttcs/BaazCFV99,

author = {Matthias Baaz and Agata Ciabattoni and Christian G. Ferm{\"u}ller and Helmut Veith},

title = {On the Undecidability of some Sub-Classical First-Order Logics},

year = {1999},

booktitle = {Foundations of Software Technology and Theoretical Computer Science, 19th Conference, Chennai, India, December 13-15, 1999, Proceedings},

editor = {C. Pandu Rangan and Venkatesh Raman and R. Ramanujam},

pages = {258--268},

publisher = {Springer},

isbn = {3-540-66836-5},

url = {http://link.springer.de/link/service/series/0558/bibs/1738/17380258.htm}

}

@article{DBLP:journals/iandc/Veith98,

author = {Helmut Veith},

title = {Succinct Representation, Leaf Languages, and Projection Reductions},

number = {2},

year = {1998},

journal = {Inf. Comput.},

pages = {207--236},

volume = {142}

}

@inbook{vciyearbook:veith98,

author = {Helmut Veith},

title = {John W.~Dawson, Jr., Logical Dilemmas: The Life and Work of Kurt G{\"o}del},

year = {1998},

booktitle = {Game Theory, Experience, Rationality (Vienna Circle Institute Yearbook)},

editor = {Werner Leinfellner and Eckehart K{\"o}hler},

publisher = {Springer},

isbn = {978-0-7923-4943-3}

}

@inproceedings{glv98,

author = {Helmut Veith and Georg Gottlob and Nicola Leone},

title = {Eine allgemeine Methode zur Bestimmung der Ausdruckskomplexit{\"a}t von Query Languages},

month = {May},

year = {1998},

booktitle = {GI Workshop Grundlagen von Datenbanken},

series = {Konstanzer Schriften in Mathematik und Informatik},

volume = {63},

issn = {1430-3558}

}

@inproceedings{DBLP:conf/csl/BaazV98,

author = {Matthias Baaz and Helmut Veith},

title = {Quantifier Elimination in Fuzzy Logic},

year = {1998},

booktitle = {Computer Science Logic, 12th International Workshop, CSL '98, Annual Conference of the EACSL, Brno, Czech Republic, August 24-28, 1998, Proceedings},

editor = {Georg Gottlob and Etienne Grandjean and Katrin Seyr},

pages = {399--414},

publisher = {Springer},

isbn = {3-540-65922-6}

}

@inproceedings{DBLP:conf/gvd/Veith98,

author = {Helmut Veith},

title = {A General Method to Determine the Expression Complexity of Database Query Languages},

year = {1998},

booktitle = {Grundlagen von Datenbanken},

pages = {134--137}

}

@inproceedings{DBLP:conf/coco/Veith98,

author = {Helmut Veith},

title = {How to Encode a Logical Structure by an OBDD},

year = {1998},

booktitle = {IEEE Conference on Computational Complexity},

pages = {122--131},

doi = {10.1109/CCC.1998.694598}

}

@inproceedings{DBLP:conf/mfcs/BaazCFV98,

author = {Matthias Baaz and Agata Ciabattoni and Christian G. Ferm{\"u}ller and Helmut Veith},

title = {Proof Theory of Fuzzy Logics: Urquhart's C and Related Logics},

year = {1998},

booktitle = {Mathematical Foundations of Computer Science 1998, 23rd International Symposium, MFCS'98, Brno, Czech Republic, August 24-28, 1998, Proceedings},

editor = {Lubos Brim and Jozef Gruska and Jir\'{\i} Zlatuska},

pages = {203--212},

publisher = {Springer},

isbn = {3-540-64827-5},

url = {http://link.springer.de/link/service/series/0558/bibs/1450/14500203.htm}

}

@article{DBLP:journals/ipl/Veith97,

author = {Helmut Veith},

title = {Languages Represented by Boolean Formulas},

number = {5},

year = {1997},

journal = {Inf. Process. Lett.},

pages = {251--256},

volume = {63},

url = {http://dx.doi.org/10.1016/S0020-0190(97)00134-8}

}

@inproceedings{DBLP:conf/esslli/EiterGV97,

author = {Thomas Eiter and Georg Gottlob and Helmut Veith},

title = {Generalized Quantifiers in Logic Programs},

year = {1997},

booktitle = {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},

editor = {Jouko A. V{\"a}{\"a}n{\"a}nen},

pages = {72--98},

publisher = {Springer},

isbn = {3-540-66993-0},

url = {http://link.springer.de/link/service/series/0558/bibs/1754/17540072.htm}

}

@inproceedings{DBLP:conf/lpnmr/EiterGV97,

author = {Thomas Eiter and Georg Gottlob and Helmut Veith},

title = {Modular Logic Programming and Generalized Quantifiers},

year = {1997},

booktitle = {Logic Programming and Nonmonotonic Reasoning, 4th International Conference, LPNMR'97, Dagstuhl Castle, Germany, July 28-31, 1997, Proceedings},

editor = {J{\"u}rgen Dix and Ulrich Furbach and Anil Nerode},

pages = {290--309},

publisher = {Springer},

isbn = {3-540-63255-7}

}

@inproceedings{DBLP:conf/coco/Veith96,

author = {Helmut Veith},

title = {Succinct Representation, Leaf Languages, and Projection Reductions},

year = {1996},

booktitle = {IEEE Conference on Computational Complexity},

pages = {118--126},

url = {http://www.computer.org/proceedings/ccc/7386/73860118abs.htm}

}

@article{DBLP:journals/eccc/ECCC-TR95-048,

author = {Helmut Veith},

title = {Succinct Representation and Leaf Languages},

number = {48},

year = {1995},

journal = {Electronic Colloquium on Computational Complexity (ECCC)},

volume = {2},

url = {http://eccc.hpi-web.de/eccc-reports/1995/TR95-048/index.html}

}

@inproceedings{DBLP:conf/mfcs/GottlobLV95,

author = {Georg Gottlob and Nicola Leone and Helmut Veith},

title = {Second Order Logic and the Weak Exponential Hierarchies},

year = {1995},

booktitle = {Mathematical Foundations of Computer Science 1995, 20th International Symposium, MFCS'95, Prague, Czech Republic, August 28 - September 1, 1995, Proceedings},

editor = {Jir\'{\i} Wiedermann and Petr H{\'a}jek},

pages = {66--81},

publisher = {Springer},

isbn = {3-540-60246-1}

}

@article{SamVei09TOCL,

author = {Marko Samer and Helmut Veith},

title = {On the Distributivity of LTL Specifications},

year = {0},

journal = {ACM Transactions on Computational Logic (TOCL)},

note = {Accepted for publication.},

publisher = {ACM},

abstract = {In this paper we investigate LTL specifications where ?[? ? ?] is equivalent to ?[?] ? ?[?] independent of ? and ?. Formulas ? with this property are called distributive queries because they naturally arise in Chan's seminal approach to temporal logic query solving (Chan 2000). As recognizing distributive LTL queries is PSpace-complete, we consider distributive fragments of LTL defined by templates as in (Buccafurri et al. 2001). Our main result is a syntactic characterization of distributive LTL queries in terms of LTL templates: We construct a context-free template grammar LTLQ^x which guarantees that all specifications obtained from LTLQ^x are distributive, and all templates not obtained from LTLQ^x have simple non-distributive instantiations.},

issn = {1529-3785}

}