Publications

2015
[267]UML \@Classroom - An Introduction to Object-Oriented Modeling
Marion Scholz Christian Huemer Gerti Kappel Martina Seidl
2015, Springer.
Note: to appear
[bibtex]
[266]A Scalable, Correct Time-Stamped Stack
M. Dodds, A. Haas, C.M. Kirsch
Proc. Symposium on Principles of Programming Languages (POPL), 2015, ACM.
Note: to appear
[bibtex]
[265]Congruences of Convex Algebras
Harald Woracek Ana Sokolova
Journal of Pure and Applied Algebra, 2015.
Note: to appear
[bibtex]
2014
[264] The Generalized Loneliness Detector and Weak System Models for __MATH0__-Set Agreement
Martin Biely, Peter Robinson, Ulrich Schmid
IEEE Transactions on Parallel and Distributed Systems, volume 25, number 4, pages 1078-1088, April 2014.
[bibtex] [pdf]
[263]Exact location of the phase transition for (1,2)-QSAT
U. Egly H.Daude R. Rossignol N. Creignou
RAIRO - Theoretical Informatics and Applications, 2014.
Note: to appear
[bibtex]
[262] Game-Theoretic Secure Localization in Wireless Sensor Networks
Susmit Jha, Krishnendu Chatterjee, Sanjit A. Seshia, Stavros Tripakis
Proceedings of the 4th International Conference on the Internet of Things (IoT), 2014.
[bibtex] [pdf]
[261] A Unified Proof System for QBF Preprocessing
Marijn Heule, Martina Seidl, Armin Biere
to appear, 2014, Springer.
[bibtex] [pdf]
[260] Fast Concurrent Data-Structures Through Explicit Timestamping
M. Dodds, A. Haas, C.M. Kirsch
Submitted, 2014.
[bibtex] [pdf]
[259]Partial Witnesses from Preprocessed Quantified Boolean Formulas
Martina Seidl, Robert Könighofer
Design, Automation and Test in Europe (DATE'14), 2014.
Note: To appear.
[bibtex]
[258] Scalloc: From Scalable Concurrent Data Structures to a Fast, Scalable, Low-Memory-Overhead Allocator
M. Aigner, C.M. Kirsch, M. Lippautz, A. Sokolova
Submitted, 2014.
[bibtex] [pdf]
[257] A Simple and Scalable Static Analysis for Bound Analysis and Amortized Complexity Analysis
Florian Zuleger Helmut Veith Moritz Sinn
CAV, 2014.
[bibtex] [pdf]
[256] Incremental QBF Solving
Florian Lonsing, Uwe Egly
20th International Conference on Principles and Practice of Constraint Programming (CP 2014), 2014.
[bibtex] [pdf]
[255] Verification of Markov Decision Processes using Learning Algorithms
Krishnendu Chatterjee Martin Chmelik Vojtech Forejt Jan Kretinsky Marta Z. Kwiatkowska David Parker Tomas Brazdil, Mateusz Ujma
ATVA, 2014.
[bibtex] [pdf]
[254] Lingva: Generating and Proving Program Properties using Symbol Elimination
Ioan Dragan, Laura Kovács
Proceedings of the 9th International Andrei Ershov Memorial Conference - Perspectives of Systems Informatic (PSI), 2014.
[bibtex] [pdf]
[253]Techniques for Real-Time Analysis of Distributed Systems (working title)
Alexander Kößler
2014, PhD thesis, Technische Universität Wien, Fakultät für Informatik.
Note: (to appear)
[bibtex]
[252] Turbo-Charging Lemmas on Demand with Don't Care Reasoning
Mathias Preiner Aina Niemetz, Armin Biere
FMCAD, 2014.
[bibtex] [pdf]
[251] Efficient Extraction of Skolem Functions from QRAT Proofs
Martina Seidl Marijn Heule, Armin Biere
FMCAD, 2014.
[bibtex] [pdf]
[250] MPIDepQBF: Towards Parallel QBF Solving Without Knowledge Sharing
Charles Jordan, Lukasz Kaiser, Florian Lonsing, Martina Seidl
17th International Conference on Theory and Applications of Satisfiability Testing (SAT 2014), 2014.
Note: To appear.
[bibtex] [pdf]
[249] Parameterized Synthesis
S. Jacobs, R. Bloem
Logical Methods in Computer Science, 2014.
[bibtex] [pdf]
[248] Tutorial on Parameterized Model Checking of Fault-Tolerant Distributed Algorithms
Annu Gmeiner, Igor Konnov, Ulrich Schmid, Helmut Veith, Josef Widder
Chapter in Formal Methods for Executable Software Models, 2014, Springer.
Note: (to appear)
[bibtex] [pdf]
[247] 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]
[246] Conformant Planning as a Case Study of Incremental QBF Solving
Uwe Egly, Martin Kronegger, Florian Lonsing, Andreas Pfandler
12th International Conference on Artificial Intelligence and Symbolic Computation AISC 2014, 2014.
[bibtex] [pdf]
[245] A Logic-Based Framework for Verifying Consensus Algorithms
Cezara Dragoi, Thomas A. Henzinger, Helmut Veith, Josef Widder, Damien Zufferey
VMCAI, pages 161-181, 2014.
[bibtex] [pdf]
[244] Fairness vs. Linearizability in a Concurrent FIFO Queue
M. Dodds, A. Haas, C.M. Kirsch
2014, Short Talk at the Joint Euro-TM/MEDIAN Workshop on Dependable Multicore and Transactional Memory Systems (DMTM).
[bibtex] [pdf]
[243]Suraq — A Controller Synthesis Tool using Uninterpreted Functions
Georg Hofferek, Ashutosh Gupta
HVC, 2014.
Note: to appear
[bibtex]
[242] Concurrent Cube-and-Conquer
Peter van der Tak, Marijn Heule, Armin Biere
CoRR, volume abs/1402.4465, 2014.
[bibtex] [pdf]
[241] Lipschitz Robustness of Finite-state Transducers
Thomas A. Henzinger, Jan Otop, Roopsha Samanta
FSTTCS, 2014.
[bibtex] [pdf]
[240] Conformant Planning as a Case Study of Incremental QBF Solving
Uwe Egly, Martin Kronegger, Florian Lonsing, Andreas Pfandler
AISC, 2014.
[bibtex] [pdf]
[239] A Framework for Automated Competitive Analysis of On-line Scheduling of Firm-Deadline Tasks
Krishnendu Chatterjee, Andreas Pavlogiannis, Alexander Kößler, Ulrich Schmid
IEEE Real-Time Systems Symposium (RTSS), 2014.
[bibtex] [pdf]
[238] Parameterized Synthesis Case Study: AMBA AHB
Roderick Bloem, Swen Jacobs, Ayrat Khalimov
Proceedings 3rd Workshop on Synthesis, SYNT 2014, Vienna, Austria, July 23-24, 2014., pages 68-83, 2014.
[bibtex] [pdf] [doi]
[237] SAT-Based Methods for Circuit Synthesis
Roderick Bloem, Uwe Egly, Patrick Klampfl, Robert Könighofer, Florian Lonsing
FMCAD, 2014.
[bibtex] [pdf]
[236] How to Handle Assumptions in Synthesis
Roderick Bloem, Rüdiger Ehlers, Swen Jacobs, Robert Könighofer
Proceedings 3rd Workshop on Synthesis, SYNT 2014, Vienna, Austria, July 23-24, 2014., pages 34-50, 2014.
[bibtex] [pdf]
[235] On cascade products of answer set programs
Christian Antic
ICLP, 2014.
[bibtex] [pdf]
[234]A SAT-Based Debugging Tool for State Machines and Sequence Diagrams
Petra Kaufmann, Martin Kronegger, Andreas Pfandler, Martina Seidl, Magdalena Widl
Software Language Engineering - 7th International Conference, SLE 2014, Västerås, Sweden, September 15-16, 2014. Proceedings, pages 21-40, 2014.
[bibtex] [doi]
[233] Cost-Aware Automatic Program Repair
Roopsha Samanta, Oswaldo Olivo, E. Allen Emerson
Static Analysis - 21st International Symposium, SAS 2014, Munich, Germany, September 11-13, 2014. Proceedings, pages 268-284, 2014.
[bibtex] [pdf] [doi]
[232]Incremental QBF Solving by DepQBF
Florian Lonsing, Uwe Egly
Mathematical Software - ICMS 2014 - 4th International Congress, Seoul, South Korea, August 5-9, 2014. Proceedings, pages 307-314, 2014.
Note: to appear
[bibtex] [doi]
[231] Incremental QBF Solving
Florian Lonsing, Uwe Egly
Principles and Practice of Constraint Programming - 20th International Conference, CP 2014, Lyon, France, September 8-12, 2014. Proceedings, pages 514-530, 2014.
[bibtex] [pdf] [doi]
[230]On the Completeness of Bounded Model Checking for Threshold-Based Distributed Algorithms: Reachability
Igor Konnov, Helmut Veith, Josef Widder
CONCUR 2014 - Concurrency Theory - 25th International Conference, CONCUR 2014, Rome, Italy, September 2-5, 2014. Proceedings, pages 125-140, 2014.
[bibtex] [doi]
[229] Cyber-Physical Cloud Computing Implemented as PaaS
C. Krainer, C.M. Kirsch
Proc. Workshop on Design, Modeling, and Evaluation of Cyber-Physical Systems (CyPhy), 2014, ACM.
[bibtex] [pdf]
[228] Cloud Computing in Space
J. Huang, C.M. Kirsch, R. Sengupta
Submitted, 2014.
[bibtex] [pdf]
[227] Battery transition systems
Udi Boker, Thomas A. Henzinger, Arjun Radhakrishna
POPL, pages 595-606, 2014.
[bibtex] [pdf]
[226] SAT-Based Synthesis Methods for Safety Specs
Roderick Bloem, Robert Könighofer, Martina Seidl
Verification, Model Checking, and Abstract Interpretation (VMCAI'14), volume 8318 of Lecture Notes in Computer Science, pages 1-20, 2014, Springer.
[bibtex] [pdf]
[225] Synthesis of Synchronization using Uninterpreted Functions
Roderick Paul Bloem, Georg Hofferek, Bettina Könighofer, Robert Könighofer, Simon Außerlechner, Raphael Spörk
, 2014.
Note: in press
[bibtex] [pdf]
[224]Programming a Robotic Network in Logical Space - A BigActor Approach
E. Pereira, P. Marques Da Silva, C. Krainer, C.M. Kirsch, R. Sengupta
Submitted, 2014.
[bibtex]
[223] QBF Resolution Systems and their Proof Complexities
Valeriy Balabanov, Magdalena Widl, Jie-Hong Roland Jiang
17th International Conference on Theory and Applications of Satisfiability Testing, 2014, Springer.
Note: to appear
[bibtex] [pdf]
[222] Extensional Crisis and Proving Identity
Laura Kovács Bernhard Kragl Andrei Voronkov Ashutosh Gupta
ATVA, 2014.
[bibtex] [pdf]
[221]Parameterized Model Checking of Rendezvous Systems
Benjamin Aminof, Tomer Kotek, Sasha Rubin, Francesco Spegni, Helmut Veith
CONCUR 2014, 2014.
Note: to appear
[bibtex]
[220] Parameterized Model Checking of Token-Passing Systems
B. Aminof, S. Jacobs, A. Khalimov, S. Rubin
VMCAI, volume 8318 of LNCS, pages 262-281, 2014, Springer.
[bibtex] [pdf]
[219]ACDC-JS: Explorative Benchmarking of JavaScript Memory Management
M. Aigner, T. Hütter, C.M. Kirsch, A. Miller, H. Payer, M. Preishuber
Submitted, 2014.
[bibtex]
2013
[218]Introduction to Special Section on Probabilistic Embedded Computing
C.M. Kirsch, V. Mooney (editors)
ACM Trans. Embed. Comput. Syst. (C.M. Kirsch, V. Mooney, eds.), volume 12, number 2s, pages 86:1-86:2, may 2013, ACM.
[bibtex] [doi]
[217] Mining Sequential Patterns to Explain Concurrent Counterexamples
Stefan Leue, Mitra Tabaei Befrouei
SPIN, volume 7976 of LNCS, pages 264-281, 2013.
[bibtex] [pdf]
[216] Solution extraction from long-distance resolution proofs
Uwe Egly, Magdalena Widl
International Workshop on Quantified Boolean Formulas 2013, Informal Workshop Report, pages 6, 2013.
[bibtex] [pdf]
[215] Lemmas on Demand for Lambdas
Mathias Preiner, Aina Niemetz, Armin Biere
DIFTS, volume 832 of CEUR Workshop Proceedings, 2013.
[bibtex] [pdf]
[214] ddSMT: A Delta Debugger for the SMT-LIB v2 Format
Aina Niemetz, Armin Biere
SMT Workshop 2013 11th International Workshop on Satisfiability Modulo Theories, 2013.
[bibtex] [pdf]
[213] Formal Verification of Distributed Algorithms (Dagstuhl Seminar 13141)
Bernadette Charron-Bost, Stephan Merz, Andrey Rybalchenko, Josef Widder
Dagstuhl Reports (Bernadette Charron-Bost, Stepahn Merz, Andrey Rybalchenko, Josef Widder, eds.), volume 3, number 4, pages 1-16, 2013, Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik.
[bibtex] [pdf] [doi]
[212] Easy Impossibility Proofs for __MATH0__-Set Agreement
Kyrill Winkler
2013, Master's thesis, Technische Universität Wien, Institut für Technische Informatik.
[bibtex] [pdf]
[211] Advanced SAT Techniques for Abstract Argumentation
Johannes Peter Wallner, Georg Weissenbacher, Stefan Woltran
Chapter in Computational Logic in Multi-Agent Systems (Joao Leite, Tran Cao Son, Paolo Torroni, Leon Torre, Stefan Woltran, eds.), volume 8143 of Lecture Notes in Computer Science, pages 138-154, 2013, Springer Berlin Heidelberg.
[bibtex] [pdf] [doi]
[210] Structural Counter Abstraction
Kshitij Bansal, Eric Koskinen, Thomas Wies, Damien Zufferey
TACAS, pages 62-77, 2013.
[bibtex] [pdf]
[209] Modeling and Controlling the Structure of Heterogeneous Mobile Robotic Systems: A BigActor Approach
E. Pereira, C. Potiron, C.M. Kirsch, R. Sengupta
International Systems Conference (SysCon), 2013, IEEE.
[bibtex] [pdf]
[208] Solving __MATH0__-Set Agreement in Dynamic Networks
Manfred Schwarz
2013, Master's thesis, Technische Universität Wien, Institut für Technische Informatik.
[bibtex] [pdf]
[207] Temporal Isolation in Real-Time Systems: The VBS Approach
S.S. Craciunas, C.M. Kirsch, H. Payer, H. Röck, A. Sokolova
Software Tools for Technology Transfer (STTT), volume 15, number 3, pages 189-209, 2013.
[bibtex] [pdf]
[206] Scalability of Vehicle Networks through Vehicle Virtualization
J. Huang, C.M. Kirsch, R. Sengupta
2013, Poster at the International Workshop on the Swarm at the Edge of the Cloud.
[bibtex] [pdf]
[205] A Networked Robotic System and its Use in an Oil Spill Monitoring Exercise
E. Pereira, P. Marques da Silva, C. Krainer, C.M. Kirsch, J. Morgado, R. Sengupta
2013, Short Talk at the International Workshop on the Swarm at the Edge of the Cloud.
[bibtex] [pdf]
[204]Analysis of Embedded Real-Time Systems at Runtime
Thomas Reinbacher
2013, PhD thesis, Technische Universität Wien, Institut für Technische Informatik.
Note: (Promotion sub auspiciis)
[bibtex]
[203] Real-Time Runtime Verification on Chip
Thomas Reinbacher, Matthias Függer, Jörg Brauer
Chapter in Runtime Verification (Shaz Qadeer, Serdar Tasiran, eds.), volume 7687 of Lecture Notes in Computer Science, pages 110-125, 2013, Springer Berlin Heidelberg.
[bibtex] [pdf]
[202]Runtime verification of embedded real-time systems
Thomas Reinbacher, Matthias Függer, Joerg Brauer
Formal Methods in System Design, pages 1-37, 2013, Springer US.
[bibtex]
[201]Solving Constraints for Generational Search
Daniel Pötzl, Andreas Holzer
Tests and Proofs - 7th International Conference, TAP 2013, Budapest, Hungary, June 16-20, 2013. Proceedings (Margus Veanes, Luca Viganò, eds.), volume 7942 of Lecture Notes in Computer Science, pages 197-213, 2013, Springer.
[bibtex]
[200] Analysis of Portfolio-Style Parallel SAT Solving on Current Multi-Core Architectures
M. Aigner, A. Biere, C.M. Kirsch, A. Niemetz, M. Preiner
Proc. Workshop on Pragmatics of SAT (PoS), 2013, EasyChair.
[bibtex] [pdf]
[199] Fast and Scalable, Lock-free k-FIFO Queues
C.M. Kirsch, M. Lippautz, H. Payer
Proc. International Conference on Parallel Computing Technologies (PaCT), 2013, Springer.
[bibtex] [pdf]
[198] Quantitative Relaxation of Concurrent Data Structures
T.A. Henzinger, C.M. Kirsch, H. Payer, A. Sezgin, A. Sokolova
Proc. Symposium on Principles of Programming Languages (POPL), 2013, ACM.
[bibtex] [pdf]
[197] Quantitative abstraction refinement
Pavol Cerný, Thomas A. Henzinger, Arjun Radhakrishna
POPL, pages 115-128, 2013.
[bibtex] [pdf]
[196] Automated Reencoding of Boolean Formulas
N. Manthey, M. Heule, A. Biere
Proc. Haifa Verification Conference (HVC'12), volume 7857 of LNCS, pages 16 pages, 2013, Springer.
Note: To be published
[bibtex] [pdf]
[195] Reconciling fault-tolerant distributed algorithms and real-time computing
Heinrich Moser, Ulrich Schmid
Distributed Computing, pages 1-28, 2013, Springer Berlin Heidelberg.
[bibtex] [pdf]
[194] Factoring Out Assumptions to Speed Up MUS Extraction
J.-M. Lagniez, A. Biere
Proc. 16th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'13), volume 7962 of LNCS, pages 17 pages, 2013, Springer.
[bibtex] [pdf]
[193] BV2EPR:AToolforPolynomiallyTranslatingQuantifier-freeBit-VectorFormulasintoEPR
G. Kovásznai, A. Fröhlich, A. Biere
Proc. 24th Intl. Conf. on Automated Deduction (CADE'13), pages 7 pages, 2013, Springer.
[bibtex] [pdf]
[192] The Auspicious Couple: Symbolic Execution and WCET Analysis
Armin Biere, Jens Knoop, Laura Kovács, Jakob Zwirchmayr
Proceedings of the 13th International Workshop on Worst-Case Execution Time Analysis (WCET), pages 53-63, 2013.
[bibtex] [pdf]
[191] Bound Propagation for Arithmetic Reasoning in Vampire
Ioan Dragan, Konstantin Korovin, Laura Kovács, Andrei Voronkov
Proceedings of the 15th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC), 2013.
[bibtex] [pdf]
[190] WCET Squeezing: On-demand Feasibility Refinement for Proven Precise WCET-bounds
Jens Knoop, Laura Kovács, Jakob Zwirchmayr
Proceedings of the 21st International Conference on Real-Time Networks and Systems (RTNS), pages 161-170, 2013.
[bibtex] [pdf]
[189] A Parametric Interpolation Framework for First-Order Theories
Laura Kovács, Simone Fulvio Rollini, Natasha Sharygina
Proceedings of the 12th Mexican International Conference on Artificial Intelligence - Advances in Artificial Intelligence and Its Applications (MICAI), pages 24-40, 2013.
[bibtex] [pdf]
[188] The Inverse Method for Many-Valued Logics
Laura Kovács, Andrei Mantsivoda, Andrei Voronkov
Proceedings of the 12th Mexican International Conference on Artificial Intelligence - Advances in Artificial Intelligence and Its Applications (MICAI), pages 12-23, 2013.
[bibtex] [pdf]
[187] First-Order Theorem Proving and Vampire
Laura Kovács, Andrei Voronkov
Proceedings of the 25th International Conference on Computer Aided Verification (CAV), pages 1-35, 2013.
[bibtex] [pdf]
[186] SmacC: A Retargetable Symbolic Execution Engine
Armin Biere, Jens Knoop, Laura Kovács, Jakob Zwirchmayr
Proceedings of the 11th International Symposium on Automated Technology for Verification and Analysis (ATVA), pages 482-486, 2013.
[bibtex] [pdf]
[185] Under-Approximating Loops in C Programs for Fast Counterexample Detection
Daniel Kroening, Matt Lewis, Georg Weissenbacher
Chapter in Computer Aided Verification (Natasha Sharygina, Helmut Veith, eds.), volume 8044 of Lecture Notes in Computer Science, pages 381-396, 2013, Springer Berlin Heidelberg.
[bibtex] [pdf] [doi]
[184] PARTY: Parameterized Synthesis of Token Rings
Ayrat Khalimov, Swen Jacobs, Roderick Bloem
Chapter in Computer Aided Verification, 2013.
[bibtex] [pdf]
[183] Towards Efficient Parameterized Synthesis
Ayrat Khalimov, Swen Jacobs, Roderick Bloem
Chapter in Verification, Model Checking, and Abstract Interpretation (Roberto Giacobazzi, Josh Berdine, Isabella Mastroeni, eds.), volume 7737 of Lecture Notes in Computer Science, pages 108-127, 2013, Springer Berlin Heidelberg.
[bibtex] [pdf] [doi]
[182] Towards Modeling and Model Checking Fault-Tolerant Distributed Algorithms
Annu John, Igor Konnov, Ulrich Schmid, Helmut Veith, Josef Widder
Proceedings 20th International Symposium on Model Checking Software (SPIN'13), Springer LNCS 7976, pages 209-226, 2013, Springer.
[bibtex] [pdf]
[181]Brief announcement: Parameterized model checking of fault-tolerant distributed algorithms by abstraction
Annu John, Igor Konnov, Ulrich Schmid, Helmut Veith, Josef Widder
Proceedings ACM Symposium on Principles of Distributed Computing (PODC'13), pages 119-121, 2013, ACM.
[bibtex]
[180] Parameterized model checking of fault-tolerant distributed algorithms by abstraction
Annu John, Igor Konnov, Ulrich Schmid, Helmut Veith, Josef Widder
Proceedings Formal Methods in Computer-Aided Design (FMCAD'13), pages 201-209, 2013, IEEE.
[bibtex] [pdf]
[179] Reductions for Synthesis Procedures
Swen Jacobs, Viktor Kuncak, Philippe Suter
Chapter in Verification, Model Checking, and Abstract Interpretation (Roberto Giacobazzi, Josh Berdine, Isabella Mastroeni, eds.), volume 7737 of Lecture Notes in Computer Science, pages 88-107, 2013, Springer Berlin Heidelberg.
[bibtex] [pdf] [doi]
[178] ACDC: Towards a Universal Mutator for Benchmarking Heap Management Systems
M. Aigner, C.M. Kirsch
Proc. International Symposium on Memory Management (ISMM), 2013, ACM.
[bibtex] [pdf]
[177] BigActors - A Model for Structure-aware Computation
E. Pereira, C.M. Kirsch, R. Sengupta, J. Borges de Sousa
Proc. International Conference on Cyber-Physical Systems (ICCPS), 2013, ACM.
[bibtex] [pdf]
[176]Challenges in compiler construction for secure two-party computation
Andreas Holzer, Nikolaos P. Karvelas, Stefan Katzenbeisser, Helmut Veith, Martin Franz
PETShop@CCS (Martin Franz, Andreas Holzer, Rupak Majumdar, Bryan Parno, Helmut Veith, eds.), pages 3-6, 2013, ACM.
[bibtex]
[175] 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]
[174] Synthesizing multiple boolean functions using interpolation on a single proof
Georg Hofferek, Ashutosh Gupta, Bettina Könighofer, Jie-Hong Roland Jiang, Roderick Bloem
FMCAD, pages 77-84, 2013.
[bibtex] [pdf]
[173] Revisiting Hyper Binary Resolution
M. Heule, M. Järvisalo, A. Biere
Proc. 10th Intl. Conf. on Integration of Artificial Intelligence and Operations Research Techniques in Constraint Programming (CPAIOR'13), volume 7874 of LNCS, pages 77-93, 2013, Springer.
[bibtex] [pdf]
[172] Aspect-Oriented Linearizability Proofs
Thomas A. Henzinger, Ali Sezgin, Viktor Vafeiadis
CONCUR, pages 242-256, 2013.
[bibtex] [pdf]
[171] From Model Checking to Model Measuring
Thomas A. Henzinger, Jan Otop
CONCUR, pages 273-287, 2013.
[bibtex] [pdf]
[170] Distributed queues in shared memory: multicore performance and scalability through quantitative relaxation
Andreas Haas, Michael Lippautz, Thomas A. Henzinger, Hannes Payer, Ana Sokolova, Christoph M. Kirsch, Ali Sezgin
Conf. Computing Frontiers, pages 17, 2013.
[bibtex] [pdf]
[169] Bridging the Gap between Dual Propagation and CNF-based QBF Solving
A. Goultiaeva, M. Seidl, A. Biere
Proc. Intl. Conf. on Design, Automation & Test in Europe (DATE'13), pages 811-814, 2013.
[bibtex] [pdf]
[168] Synthesis of AMBA AHB from formal specification: a case study
Yashdeep Godhal, Krishnendu Chatterjee, Thomas A. Henzinger
STTT, volume 15, number 5-6, pages 585-601, 2013.
[bibtex] [pdf]
[167] More on the Complexity of Quantifier-Free Fixed-Size Bit-Vector Logics with Binary Encoding
A. Fröhlich, G. Kovásznai, A. Biere
Proc. 8th Intl. Computer Science Symp. in Russia (CSR'13), pages 12 pages, 2013, Springer.
[bibtex] [pdf]
[166] Con2colic testing
Azadeh Farzan, Andreas Holzer, Niloofar Razavi, Helmut Veith
Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering, ESEC/FSE'13, Saint Petersburg, Russian Federation, August 18-26, 2013 (Bertrand Meyer, Luciano Baresi, Mira Mezini, eds.), pages 37-47, 2013, ACM.
[bibtex] [pdf]
[165]The Effect of Forgetting on the Performance of a Synchronizer
Matthias Függer, Alexander Kößler, Thomas Nowak, Ulrich Schmid, Martin Zeiner
Proceedings ALGOSENSORS'13, Springer LNCS 8243, pages 185-200, 2013, Springer.
[bibtex]
[164] Automatic Linearizability Proofs of Concurrent Objects with Cooperating Updates
Cezara Dragoi, Ashutosh Gupta, Thomas A. Henzinger
CAV, pages 174-190, 2013.
[bibtex] [pdf]
[163] Local Shape Analysis for Overlaid Data Structures
Cezara Dragoi, Constantin Enea, Mihaela Sighireanu
SAS, pages 150-171, 2013.
[bibtex] [pdf]
[162] 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]
[161] Semantics-Aware Versioning Challenge: Merging Sequence Diagrams along with State Machine Diagrams
Petra Brosch, Martina Seidl, Magdalena Widl
Softwaretechnik-Trends, volume 33, number 2, 2013.
[bibtex] [pdf]
[160] Complexity Classifications for logic-based Argumentation
Nadia Creignou, Uwe Egly, Johannes Schmidt
ACM TOCL, 2013.
[bibtex] [pdf]
[159] 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]
[158] Efficient Clause Learning for Quantified Boolean Formulas via QBF Pseudo Unit Propagation
Florian Lonsing, Uwe Egly, Allen Van Gelder
SAT, pages 100-115, 2013.
[bibtex] [pdf]
[157] Global State Checker: Towards SAT-Based Reachability Analysis of Communicating State Machines
Petra Kaufmann, Martin Kronegger, Andreas Pfandler, Martina Seidl, Magdalena Widl
MoDeVVa@MoDELS, pages 31-40, 2013.
[bibtex] [pdf]
[156] Blocked Clause Decomposition
Marijn Heule, Armin Biere
LPAR, volume 8312 of LNCS, pages 423-438, 2013, Springer.
[bibtex] [pdf]
[155] Long-Distance Resolution: Proof Generation and Strategy Extraction in Search-Based QBF Solving
Uwe Egly, Florian Lonsing, Magdalena Widl
LPAR, pages 291-308, 2013.
[bibtex] [pdf]
[154] How to Travel between Languages
Krishnendu Chatterjee, Siddhesh Chaubal, Sasha Rubin
LATA, pages 214-225, 2013.
[bibtex] [pdf]
[153] Modbat: A Model-Based API Tester for Event-Driven Systems
Cyrille Valentin Artho, Armin Biere, Masami Hagiya, Eric Platon, Martina Seidl, Yoshinori Tanabe, Mitsuharu Yamamoto
Haifa Verification Conference, volume 8244 of Lecture Notes in Computer Science, pages 112-128, 2013, Springer.
[bibtex] [pdf]
[152] Information Reuse for Multi-goal Reachability Analyses
Dirk Beyer, Andreas Holzer, Michael Tautschnig, Helmut Veith
ESOP, volume 7792 of Lecture Notes in Computer Science, pages 472-491, 2013, Springer.
[bibtex] [pdf]
[151] Strategy improvement for concurrent reachability and turn-based stochastic safety games
Krishnendu Chatterjee, Luca de Alfaro, Thomas A. Henzinger
J. Comput. Syst. Sci., volume 79, number 5, pages 640-657, 2013.
[bibtex] [pdf]
[150] A survey of partial-observation stochastic parity games
Krishnendu Chatterjee, Laurent Doyen, Thomas A. Henzinger
Formal Methods in System Design, volume 43, number 2, pages 268-284, 2013.
[bibtex] [pdf]
[149] Efficient Synthesis for Concurrency by Semantics-Preserving Transformations
Pavol Cerný, Thomas A. Henzinger, Arjun Radhakrishna, Leonid Ryzhyk, Thorsten Tarrach
CAV, pages 951-967, 2013.
[bibtex] [pdf]
[148] Hyperplane Separation Technique for Multidimensional Mean-Payoff Games
Krishnendu Chatterjee, Yaron Velner
Concurrency Theory - 24th International Conference (CONCUR 2013), volume 8052 of Lecture Notes in Computer Science, pages 500-515, 2013, Springer.
[bibtex] [pdf]
[147]Synthesis of memory-efficient, clock-memory free, and non-Zeno safety controllers for timed systems
Krishnendu Chatterjee, Vinayak S. Prabhu
Inf. Comput., volume 228, pages 83-119, 2013.
[bibtex]
[146] Quantitative timed simulation functions and refinement metrics for real-time systems
Krishnendu Chatterjee, Vinayak S. Prabhu
Proceedings of the 16th international conference on Hybrid systems: computation and control (HSCC 2013), pages 273-282, 2013, ACM.
[bibtex] [pdf]
[145]Automated Analysis of Real-Time Scheduling using Graph Games
Krishnendu Chatterjee, Alexander Köß ler, Ulrich Schmid
Proceedings of the 16th ACM international conference on Hybrid Systems: Computation and Control, pages 163-172, 2013, ACM.
[bibtex]
[144] Link Reversal Routing with Binary Link Labels: Work Complexity
Bernadette Charron-Bost, Antoine Gaillard, Jennifer Welch, Josef Widder
SIAM Journal on Computing, volume 42, number 2, pages 634-661, 2013.
[bibtex] [pdf]
[143] Transience Bounds for Distributed Algorithms
Bernadette Charron-Bost, Matthias Függer, Thomas Nowak
Proceedings of the 11th International Conference on Formal Modeling and Analysis of Timed Systems, pages 77-90, 2013, Springer-Verlag.
[bibtex] [pdf]
[142] Infinite-state games with finitary conditions
Krishnendu Chatterjee, Nathanaël Fijalkow
Computer Science Logic 2013 (CSL 2013), volume 23 of LIPIcs, pages 181-196, 2013, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik.
[bibtex] [pdf]
[141] Looking at Mean-Payoff and Total-Payoff through Windows
Krishnendu Chatterjee, Laurent Doyen, Mickael Randour, Jean-François Raskin
Automated Technology for Verification and Analysis (ATVA 2013), volume 8172 of Lecture Notes in Computer Science, pages 118-132, 2013, Springer.
[bibtex] [pdf]
[140] What is Decidable about Partially Observable Markov Decision Processes with omega-Regular Objectives
Krishnendu Chatterjee, Martin Chmelik, Mathieu Tracol
Computer Science Logic 2013 (CSL 2013), volume 23 of LIPIcs, pages 165-180, 2013, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik.
[bibtex] [pdf]
[139] Tree Interpolation in Vampire
Régis Blanc, Ashutosh Gupta, Laura Kovács, Bernhard Kragl
Proceedings of the 19th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-19), pages 173-181, 2013.
[bibtex] [pdf]
[138]The Benefits of Relaxing Concurrent Data Structures
A. Haas, T.A. Henzinger, C.M. Kirsch, M. Lippautz, H. Payer, A. Sezgin, A. Sokolova
Submitted, 2013.
[bibtex]
[137] Weak Synchrony Models and Failure Detectors for Message Passing __MATH0__-Set Agreement
Martin Biely, Peter Robinson, Ulrich Schmid
IEEE Transactions on Parallel and Distributed Systems, 2013.
Note: (to appear)
[bibtex] [pdf]
[136] Synthesizing robust systems
Roderick Bloem, Krishnendu Chatterjee, Karin Greimel, Thomas A. Henzinger, Georg Hofferek, Barbara Jobstmann, Bettina Könighofer, Robert Könighofer
Acta Informatica, 2013, Springer Berlin Heidelberg.
[bibtex] [pdf] [doi]
[135] Model-Based Testing for Verification Backends
C. Artho, A. Biere, M. Seidl
Proc. 7th Intl. Conf. on Tests & Proofs (TAP'13), pages 17 pages, 2013, Springer.
[bibtex] [pdf]
2012
[134] Wait-Free Stabilizing Dining Using Regular Registers
Srikanth Sastry, Jennifer L. Welch, Josef Widder
OPODIS, volume 7702 of LNCS, pages 284-299, December 2012, Springer.
[bibtex] [pdf]
[133] it Symbol Elimination in Program Analysis
Laura Kovács
November 2012, Habilitation Thesis, Vienna University of Technology, Austria.
[bibtex] [pdf]
[132] 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]
[131] 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]
[130] Fast and Scalable k-FIFO Queues
C.M. Kirsch, M. Lippautz, H. Payer
June 2012, Technical report, Department of Computer Sciences, University of Salzburg.
[bibtex] [pdf]
[129] Evolutionary game dynamics in populations with different learners
Krishnendu Chatterjee, Damien Zufferey, Martin A. Nowak
Journal of Theoretical Biology, volume 301, pages 161-173, may 2012.
[bibtex] [pdf] [doi]
[128] Proving Reachability Using FShell (Competition Contribution)
Andreas Holzer, Daniel Kroening, Christian Schallhart, Michael Tautschnig, Helmut Veith
Chapter in Tools and Algorithms for the Construction and Analysis of Systems (Cormac Flanagan, Barbara König, eds.), volume 7214 of Lecture Notes in Computer Science, pages 538-541, 2012, Springer Berlin Heidelberg.
[bibtex] [pdf] [doi]
[127] A Vampire-Based Tool for Minimising Interpolants
Krystof Hoder, Andreas Holzer, Laura Kovács, Andrei Voronkov
2012.
[bibtex] [pdf]
[126] On a Family of q-Binomial Distributions
Martin Zeiner
2012, Technical report, Technische Universität Wien, Institut für Technische Informatik.
[bibtex] [pdf]
[125] Consensus in the presence of mortal Byzantine faulty processes
Josef Widder, Martin Biely, Günther Gridling, Bettina Weiss, Jean-Paul Blanquart
Distributed Computing, volume 24, number 6, pages 299-321, 2012.
[bibtex] [pdf]
[124] Ideal Abstractions for Well-Structured Transition Systems
Damien Zufferey, Thomas Wies, Thomas A. Henzinger
VMCAI, pages 445-460, 2012.
[bibtex] [pdf]
[123] Concurrent Cube-and-Conquer
P. van der Tak, M. Heule, A. Biere
Proc. of SAT Challenge 2012: Solver and Benchmark Descriptions (A. Balint, A. Belov, A. Diepold, S. Gerber, M. Järvisalo, C. Sinz, eds.), volume B-2012-2 of Department of Computer Science Series of Publications B, University of Helsinki, pages 15-16, 2012.
[bibtex] [pdf]
[122] Algorithmic analysis of array-accessing programs
Rajeev Alur, Pavol Cerný, Scott Weinstein
ACM Trans. Comput. Log., volume 13, number 3, pages 27, 2012.
[bibtex] [pdf]
[121] Simulation distances
Pavol Cerný, Thomas A. Henzinger, Arjun Radhakrishna
Theor. Comput. Sci., volume 413, number 1, pages 21-35, 2012.
[bibtex] [pdf]
[120] QBF2EPR:AToolforGeneratingEPRFormulasfromQBF
M. Seidl, F. Lonsing, A. Biere
Proc. 3rd Intl. Work. on Practical Aspects of Automated Reasoning (PAAR'12), pages 10 pages, 2012.
[bibtex] [pdf]
[119] Solving Robust Glucose-Insulin Control by Dixon Resultant Computations
Laura Kovács, Béla Paláncz, Levente Kovács
Proceedings of International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC 2012), pages 53-61, 2012.
[bibtex] [pdf]
[118] Symbol Elimination in Program Analysis
Laura Kovács
Proceedings of the International Conference on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC), volume P3964 of IEEE Computer Society, pages 12, 2012.
[bibtex] [pdf]
[117] Generalized Reactivity(1) Synthesis without a Monolithic Strategy
Matthias Schlaipfer, Georg Hofferek, Roderick Paul Bloem
Hardware and Software: Verification and Testing. 7th International Haifa Verification Conference, HVC 2011, Haifa, Israel, December 6-8, 2011, Revised Selected Papers (João Lourenço Kerstin Eder, Onn Shehory, eds.), volume 7261 of Lecture Notes in Computer Science, pages 20 - 34, 2012, Springer.
[bibtex] [pdf]
[116] Separate compilation of hierarchical real-time programs into linear-bounded Embedded Machine code
Arkadeb Ghosal, Daniel T. Iercan, Christoph M. Kirsch, Thomas A. Henzinger, Alberto L. Sangiovanni-Vincentelli
Sci. Comput. Program., volume 77, number 2, pages 96-112, 2012.
[bibtex] [pdf]
[115] FFX: A Portable WCET Annotation Language
Armelle Bonenfant, Hugues Cassé, Marianne De Michiel, Jens Knoop, Laura Kovács, Jakob Zwirchmayr
Proceedings of the ACM International Conference on Real-Time and Network Systems (RNTS 2012), pages 91-100, 2012, ACM.
[bibtex] [pdf]
[114]The Effect of One Additional Driver Mutation on Tumor Progression
Johannes Reiter, Ivana Bozic, Ben Allen, Krishnendu Chatterjee, Martin A. Nowak
J. Evolutionary Applications, 2012.
[bibtex]
[113] How FIFO is Your Concurrent FIFO Queue?
A. Haas, C.M. Kirsch, M. Lippautz, H. Payer
Proc. OOPSLA Workshop on Relaxing Synchronization for Multicore and Manycore Scalability (RACES), 2012.
[bibtex] [pdf]
[112] Playing in the Grey Area of Proofs
Kryštof Hoder, Laura Kovács, Andrei Voronkov
Proceedings of ACM SIGACT-SIGPLAN International Symposium on Principles of Programming Languages (POPL), volume 47 of ACM SIGPLAN Notices, pages 259-272, 2012.
[bibtex] [pdf]
[111] Resolution-Based Certificate Extraction for QBF - (Tool Presentation)
A. Niemetz, M. Preiner, F. Lonsing, M. Seidl, A. Biere
Proc. 15th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'12), volume 7317 of LNCS, pages 430-435, 2012, Springer.
Note: Reported 2011 too, now formally published
[bibtex] [pdf]
[110] The molecular evolution of acquired resistance to targeted EGFR blockade in colorectal cancers
L. A. Diaz, R. Williams, J. Wu, I. Kinde, J. R. Hecht, J. Berlin, B. Allen, I. Bozic, J. G. Reiter, M. A. Nowak, K. W. Kinzler andd K. S. Oliner, B. Vogelstein
Nature, 2012.
[bibtex] [pdf]
[109] On the performance of a retransmission-based synchronizer
Thomas Nowak, Matthias Függer, Alexander Kößler
Theoretical Computer Science, volume (available online), 2012.
[bibtex] [pdf]
[108] r-TuBound: Loop Bounds for WCET Analysis (Tool Paper)
Jens Knoop, Laura Kovács, Jakob Zwirchmayr
Proceedings of International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-18), volume 7180 of LNCS, pages 435-444, 2012.
[bibtex] [pdf]
[107] On the Complexity of Fixed-Size Bit-Vector Logics with Binary Encoded Bit-Width
G. Kovásznai, A. Fröhlich, A. Biere
Proc. 10th Intl. Work. on Satisfiability Modulo Theories (SMT'12), pages 12 pages, 2012.
[bibtex] [pdf]
[106] Who is afraid of Model Checking Distributed Algorithms?
Igor Konnov, Helmut Veith, Josef Widder
2012, CAV Workshop (EC)$^2$.
[bibtex] [pdf]
[105] A Myhill-Nerode theorem for automata with advice
Alex Kruckman, Sasha Rubin, John Sheridan, Ben Zax
GandALF, pages 238-246, 2012.
[bibtex] [pdf]
[104] Repair with On-The-Fly Program Analysis
Robert Könighofer, Roderick Paul Bloem
, 2012, Springer.
Note: in press
[bibtex] [pdf]
[103] Parameterized Model Checking by Network Invariants: the Asynchronous Case
Igor Konnov
2012, LICS Workshop AISS.
[bibtex] [pdf]
[102] Inprocessing Rules
M. Järvisalo, M. Heule, A. Biere
Proc. 6th Intl. Joint Conf. on Automated Reasoning (IJCAR'12), volume 7364 of LNCS, pages 355-370, 2012, Springer.
Note: Reported 2011 too, now formally published
[bibtex] [pdf]
[101] Trace Semantics via Determinization
Bart Jacobs, Alexandra Silva, Ana Sokolova
CMCS, pages 109-129, 2012, LNCS 7399.
[bibtex] [pdf]
[100] Parameterized Synthesis
Swen Jacobs, Roderick Bloem
TACAS, pages 362-376, 2012.
[bibtex] [pdf]
[99]Foreword to the Special Issue on Invariant Generation and Advanced Techniques for Reasoning about Loops
Nikolaj Bjørner, Laura Kovács
Journal of Symbolic Computation, 2012.
[bibtex]
[98]Editorial to the Special Issue on Automated Specification and Verification of Web Systems
Laura Kovács, Temur Kutsia
Journal of Applied Logic, volume 10, number 1, pages 1, 2012.
[bibtex]
[97] Bounded-Interference Sequentialization for Testing Concurrent Programs
Niloofar Razavi, Azadeh Farzan, Andreas Holzer
Chapter in Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change (Tiziana Margaria, Bernhard Steffen, eds.), volume 7609 of Lecture Notes in Computer Science, pages 372-387, 2012, Springer Berlin Heidelberg.
[bibtex] [pdf] [doi]
[96] Hierarchical PLABs, CLABs, TLABs in Hotspot
C.M. Kirsch, H. Payer, H. Röck
Proc. International Conference on Systems (ICONS), 2012.
[bibtex] [pdf]
[95] Performance, Scalability, and Semantics of Concurrent FIFO Queues
C.M. Kirsch, H. Payer, H. Röck, A. Sokolova
Proc. International Conference on Algorithms and Architectures for Parallel Processing (ICA3PP), 2012, Springer.
[bibtex] [pdf]
[94] Secure two-party computations in ANSI C
Andreas Holzer, Martin Franz, Stefan Katzenbeisser, Helmut Veith
ACM Conference on Computer and Communications Security (Ting Yu, George Danezis, Virgil D. Gligor, eds.), pages 772-783, 2012, ACM.
[bibtex] [pdf]
[93] Cube and Conquer: Guiding CDCL SAT Solvers by Lookaheads
M. Heule, O. Kullmann, S. Wieringa, A. Biere
Proc. 7th Intl. Haifa Verification Conference (HVC'11), volume 7261 of LNCS, pages 50-65, 2012, Springer.
Note: \textbfBest paper award, reported 2011 too, now formally published
[bibtex] [pdf]
[92] HSF(C): A Software Verifier Based on Horn Clauses - (Competition Contribution)
Sergey Grebenshchikov, Ashutosh Gupta, Nuno P. Lopes, Corneliu Popeea, Andrey Rybalchenko
TACAS, pages 549-551, 2012.
[bibtex] [pdf]
[91] Interface Simulation Distances
Pavol Cerný, Martin Chmelik, Thomas A. Henzinger, Arjun Radhakrishna
GandALF, pages 29-42, 2012.
[bibtex] [pdf]
[90] Algorithm for Solving DQBF
A. Fröhlich, G. Kovásznai, A. Biere
Proc. 3rd Intl. Work. on Pragmatics of SAT (POS'12), pages 14 pages, 2012.
[bibtex] [pdf]
[89] Efficient Checking of Link-Reversal-Based Concurrent Systems
Matthias Függer, Josef Widder
Chapter in Proceedings CONCUR 2012 - Concurrency Theory (Maciej Koutny, Irek Ulidowski, eds.), volume 7454 of Lecture Notes in Computer Science, pages 486-499, 2012, Springer Berlin Heidelberg.
[bibtex] [pdf]
[88] On sequent systems and resolution for quantified Boolean formulas
U. Egly
SAT'12, 2012.
[bibtex] [pdf]
[87] The Power of Isolation
S.S. Craciunas, C.M. Kirsch
Proc. International Conference on Embedded and Ubiquitous Computing (EUC), 2012, IEEE.
[bibtex] [pdf]
[86] Synthesis from incompatible specifications
Pavol Cerný, Sivakanth Gopi, Thomas A. Henzinger, Arjun Radhakrishna, Nishant Totla
EMSOFT, pages 53-62, 2012.
[bibtex] [pdf]
[85] Symbolically Synthesizing Small Circuits
Rüdiger Ehlers, Robert Könighofer, Georg Hofferek
Proceedings of the 12th Conference on Formal Methods in Computer-Aided Design (FMCAD 2012), pages 91 - 100, 2012.
[bibtex] [pdf]
[84] Towards Scenario-Based Testing of UML Diagrams
U. Egly, S. Gabmeyer, M. Seidl, H. Tompits, M. Widl, M. Wimmer
Proceedings of the 6th International Conference on Tests and Proofs (TAP), 2012.
[bibtex] [pdf]
[83] Guided Merging of Sequence Diagrams
Magdalena Widl, Armin Biere, Petra Brosch, Uwe Egly, Marijn Heule, Gerti Kappel, Martina Seidl, Hans Tompits
SLE, pages 164-183, 2012.
[bibtex] [pdf]
[82] Interpretations in Trees with Countably Many Branches
Alexander Rabinovich, Sasha Rubin
Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, LICS 2012, Dubrovnik, Croatia, June 25-28, 2012, pages 551-560, 2012, IEEE.
[bibtex] [pdf]
[81] Complexity of logic-based argumentation in Schaefer's framework
Nadia Creignou, Uwe Egly, Johannes Schmidt
COMMA, pages 237-248, 2012.
[bibtex] [pdf]
[80] Cyber-Physical Cloud Computing: The Binding and Migration Problem
C.M. Kirsch, E. Pereira, R. Sengupta, H. Chen, R. Hansen, J. Huan, F. Landolt, M. Lippautz, A. Rottmann, R. Swick, R. Trummer, D. Vizzini
Proc. International Conference on Design, Automation and Test in Europe (DATE), 2012.
[bibtex] [pdf]
[79] Incorrect Systems: It's not the Problem, It's the Solution
C.M. Kirsch, H. Payer
Proc. Design Automation Conference (DAC), 2012, ACM.
[bibtex] [pdf]
[78] Code Aware Resource Management
Krishnendu Chatterjee, Luca de Alfaro, Marco Faella, Rupak Majumdar, Vishwanath Raman
Formal Methods in Computer Science, 2012.
[bibtex] [pdf]
[77] Mean-Payoff Pushdown Games
Krishnendu Chatterjee, Yaron Velner
LICS, pages 195-204, 2012.
[bibtex] [pdf]
[76] Decidable Problems for Probabilistic Automata on Infinite Words
Krishnendu Chatterjee, Mathieu Tracol
LICS, pages 185-194, 2012.
[bibtex] [pdf]
[75] Strategy Synthesis for Multi-Dimensional Quantitative Objectives
Krishnendu Chatterjee, Mickael Randour, Jean-François Raskin
CONCUR, pages 115-131, 2012.
[bibtex] [pdf]
[74] Evolutionary Dynamics of Biological Auctions
Krishnendu Chatterjee, Johannes G. Reiter, Martin A. Nowak
J. Theoretical Population Biology, 2012.
[bibtex] [pdf]
[73]Discounting and Averaging in Games across Time scales
Krishnendu Chatterjee, Rupak Majumdar
Int. J. Found. Comput. Sci., volume 23, number 3, pages 609-625, 2012.
[bibtex]
[72] Average Case Analysis of the Classical Algorithm for Markov Decision Processes with Büchi Objectives
Krishnendu Chatterjee, Manas Joglekar, Nisarg Shah
FSTTCS, pages 461-473, 2012.
[bibtex] [pdf]
[71] Strategy Complexity of Finite-Horizon Markov Decision Processes and Simple Stochastic Games
Krishnendu Chatterjee, Rasmus Ibsen-Jensen
MEMICS, pages 106-117, 2012.
[bibtex] [pdf]
[70]Finite automata with time-delay blocks
Krishnendu Chatterjee, Thomas A. Henzinger, Vinayak S. Prabhu
EMSOFT, pages 43-52, 2012.
[bibtex]
[69] Polynomial-Time Algorithms for Energy Games with Special Weight Structures
Krishnendu Chatterjee, Monika Henzinger, Sebastian Krinninger, Danupon Nanongkai
ESA, pages 301-312, 2012.
[bibtex] [pdf]
[68] A survey of stochastic __MATH0__-regular games
Krishnendu Chatterjee, Thomas A. Henzinger
J. Comput. Syst. Sci., volume 78, number 2, pages 394-413, 2012.
[bibtex] [pdf]
[67] A Framework for the Specification of Random SAT and QSAT Formulas
N. Creignou, U. Egly, M. Seidl
Proceedings of the 6th International Conference on Tests and Proofs (TAP), 2012.
[bibtex] [pdf]
[66] Strategy Improvement for Concurrent Reachability and Safety Games
Krishnendu Chatterjee, Luca de Alfaro, Thomas A. Henzinger
CoRR, volume abs/1201.2834, 2012.
[bibtex] [pdf]
[65] Energy parity games
Krishnendu Chatterjee, Laurent Doyen
Theor. Comput. Sci., volume 458, pages 49-60, 2012.
[bibtex] [pdf]
[64] Partial-Observation Stochastic Games: How to Win When Belief Fails
Krishnendu Chatterjee, Laurent Doyen
LICS, pages 175-184, 2012.
[bibtex] [pdf]
[63] Equivalence of Games with Probabilistic Uncertainty and Partial-Observation Games
Krishnendu Chatterjee, Martin Chmelik, Rupak Majumdar
ATVA, pages 385-399, 2012.
[bibtex] [pdf]
[62] Faster Algorithms for Alternating Refinement Relations
Krishnendu Chatterjee, Siddhesh Chaubal, Pritish Kamath
CSL, pages 167-182, 2012.
[bibtex] [pdf]
[61] The complexity of stochastic Müller games
Krishnendu Chatterjee
Inf. Comput., volume 211, pages 29-48, 2012.
[bibtex] [pdf]
[60] Lingeling and Friends Entering the SAT Challenge 2012
A. Biere
Proc. of SAT Challenge 2012: Solver and Benchmark Descriptions (A. Balint, A. Belov, A. Diepold, S. Gerber, M. Järvisalo, C. Sinz, eds.), volume B-2012-2 of Department of Computer Science Series of Publications B, University of Helsinki, pages 33-34, 2012.
[bibtex] [pdf]
[59] Agreement in Directed Dynamic Networks
Martin Biely, Peter Robinson, Ulrich Schmid
Proceedings 19th International Colloquium on Structural Information and Communication Complexity (SIROCCO'12), pages 73-84, 2012, Springer-Verlag.
[bibtex] [pdf]
[58] Synthesizing Robust Systems with RATSY
Roderick Paul Bloem, Hans-Jürgen Gamauf, Georg Hofferek, Bettina Könighofer, Robert Könighofer
Proceedings First Workshop on Synthesis (SYNT 2012) (Open Publishing Association, ed.), pages 47 - 53, 2012, Electronic Proceedings in Theoretical Computer Science.
[bibtex] [pdf]
[57] Towards Semantics-Aware Merge Support in Optimistic Model Versioning
P. Brosch, U. Egly, S. Gabmeyer, G. Kappel, M. Seidl, H. Tompits, M. Widl, M. Wimmer
Proceedings of the Models and Evolution Workshop \@ MoDELS'11, 2012.
[bibtex] [pdf]
[56] FoREnSiC - An Automatic Debugging Environment for C Programs
Roderick Paul Bloem, Rolf Drechsler, Görschwin Fey, Alexander Finder, Georg Hofferek, Robert Könighofer, Jaan Raik, Urmas Repinski, Andre Sülflow
, 2012, Springer.
Note: in press
[bibtex] [pdf]
[55] Efficient Controller Synthesis for Consumption Games with Multiple Resource Types
Tomás Brázdil, Krishnendu Chatterjee, Antonín Kucera, Petr Novotný
CAV, pages 23-38, 2012.
[bibtex] [pdf]
[54] Improved Single Pass Algorithms for Resolution Proof Reduction
Ashutosh Gupta
ATVA, pages 107-121, 2012.
[bibtex] [pdf]
[53] The Logical Execution Time Paradigm
C.M. Kirsch, A. Sokolova
Advances in Real-Time Systems, pages 103-120, 2012.
[bibtex] [pdf]
[52] Vinter: A Vampire-Based Tool for Interpolation
Kryštof Hoder, Andreas Holzer, Laura Kovács, Andrei Voronkov
Proceedings of Asian Symposium on Programming Languages and Systems (APLAS 2012), volume 7705 of LNCS, pages 148-146, 2012.
[bibtex] [pdf]
[51] Cloud Computing on Wings: Applications to Air Quality
H. Chen, R. Hansen, J. Huang, E. Pereira, R. Swick, D. Vizzini, R. Sengupta, C. M. Kirsch, F. Landolt, M. Lippautz, A. Rottmann, R. Trummer
Proc. American Astronautical Society Guidance and Control Conference (AASGNC), 2012, AAS.
[bibtex] [pdf]
2011
[50] Bound Analysis of Imperative Programs with the Size-Change Abstraction
Florian Zuleger, Sumit Gulwani, Moritz Sinn, Helmut Veith
SAS, pages 280-297, 2011.
[bibtex] [pdf]
[49] An Evaluation of WCET Analysis using Symbolic Loop Bounds
Jens Knoop, Laura Kovács, Jakob Zwirchmayr
Proceedings of the International Workshop on Worst-Case Execution Time Analysis (WCET), pages 93-103, 2011.
[bibtex] [pdf]
[48] A Theory of Synchronous Relational Interfaces
Stavros Tripakis, Ben Lickly, Thomas A. Henzinger, Edward A. Lee
ACM Trans. Program. Lang. Syst., volume 33, number 4, pages 14, 2011.
[bibtex] [pdf]
[47] The Asynchronous Bounded-Cycle Model
Peter Robinson, Ulrich Schmid
Theoretical Computer Science, volume 412, number 40, pages 5580-5601, 2011.
[bibtex] [pdf]
[46] Symbolic Loop Bound Computation for WCET Analysis
Jens Knoop, Laura Kovács, Jakob Zwirchmayr
Proceedings of the International Conference on Perspectives of System Informatics (PSI), volume 7162 of LNCS, pages 224-239, 2011.
[bibtex] [pdf]
[45] Brief Announcement: Scalability versus Semantics of Concurrent FIFO Queues
C.M. Kirsch, H. Payer, H. Röck, A. Sokolova
Proc. Symposium on Principles of Distributed Computing (PODC), pages 331-332, 2011, ACM.
[bibtex] [pdf]
[44] Case Studies on Invariant Generation Using a Saturation Theorem Prover
Krytsof Hoder, Laura Kovács, Andrei Voronkov
Proceedings of the Mexican International Conference on Artificial Intelligence (MICAI), volume 7094 of LNAI, pages 1-15, 2011.
[bibtex] [pdf]
[43] Failed Literal Detection for QBF
Florian Lonsing, Armin Biere
SAT, pages 259-272, 2011.
[bibtex] [pdf]
[42] Short-term Memory for Self-collecting Mutators
M. Aigner, A. Haas, C.M. Kirsch, M. Lippautz, A. Sokolova, S. Stroka, A. Unterweger
Proc. International Symposium on Memory Management (ISMM), 2011, ACM.
[bibtex] [pdf]
[41] Seamless Testing for Models and Code
Andreas Holzer, Visar Januzaj, Stefan Kugele, Boris Langer, Christian Schallhart, Michael Tautschnig, Helmut Veith
FASE, pages 278-293, 2011.
[bibtex] [pdf]
[40] Controller Synthesis for Pipelined Circuits Using Uninterpreted Functions
Georg Hofferek, Roderick Paul Bloem
Ninth ACM/IEEE International Conference on Formal Methods and Models for Codesign (MemoCODE 2011) (IEEE, ed.), pages 31 - 42, 2011, IEEE.
[bibtex] [pdf]
[39] Scheduling large jobs by abstraction refinement
Thomas A. Henzinger, Vasu Singh, Thomas Wies, Damien Zufferey
EuroSys, pages 329-342, 2011.
[bibtex] [pdf]
[38] Static Scheduling in Clouds
Thomas A. Henzinger, Anmol V. Singh, Vasu Singh, Thomas Wies, Damien Zufferey
Proceedings of the 3rd USENIX Workshop on Hot Topic in Cloud Computing (HotCloud'11), 2011.
[bibtex] [pdf]
[37] Efficient CNF Simplification Based on Binary Implication Graphs
Marijn Heule, Matti Järvisalo, Armin Biere
SAT, pages 201-215, 2011.
[bibtex] [pdf]
[36] Quantitative Evaluation of BFT Protocols
Raluca Halalai, Thomas A. Henzinger, Vasu Singh
QEST, pages 255-264, 2011.
[bibtex] [pdf]
[35] Solving Recursion-Free Horn Clauses over LI+UIF
Ashutosh Gupta, Corneliu Popeea, Andrey Rybalchenko
APLAS, pages 188-203, 2011.
[bibtex] [pdf]
[34] Verification of STM on relaxed memory models
Rachid Guerraoui, Thomas A. Henzinger, Vasu Singh
Formal Methods in System Design, volume 39, number 3, pages 297-331, 2011.
[bibtex] [pdf]
[33] On Efficient Checking of Link-reversal-based Concurrent Systems
Matthias Függer, Josef Widder
2011, Unpublished contribution to: (EC)2 2011: Workshop on Exploiting Concurrency Efficiently and Correctly.
[bibtex] [pdf]
[32] Dynamic Reactive Modules
Jasmin Fisher, Thomas A. Henzinger, Dejan Nickovic, Nir Piterman, Anmol V. Singh, Moshe Y. Vardi
CONCUR, pages 404-418, 2011.
[bibtex] [pdf]
[31]Graph Games with Reachability Objectives
Krishnendu Chatterjee
RP, pages 1, 2011.
[bibtex]
[30] On Transfinite Knuth-Bendix Orders
Laura Kovács, Georg Moser, Andrei Voronkov
Proceedings of the International Conference on Automated Deduction (CADE), volume 6803 of LNAI, pages 384-399, 2011, Springer.
[bibtex] [pdf]
[29] Synthesis of memory-efficient "real-time" controllers for safety objectives
Krishnendu Chatterjee, Vinayak S. Prabhu
HSCC, pages 221-230, 2011.
[bibtex] [pdf]
[28] Minimum Attention Controller Synthesis for Omega-Regular Objectives
Krishnendu Chatterjee, Rupak Majumdar
FORMATS, pages 145-159, 2011.
[bibtex] [pdf]
[27] Timed Parity Games: Complexity and Robustness
Krishnendu Chatterjee, Thomas A. Henzinger, Vinayak S. Prabhu
Logical Methods in Computer Science, volume 7, number 4, 2011.
[bibtex] [pdf]
[26] QUASY: Quantitative Synthesis Tool
Krishnendu Chatterjee, Thomas A. Henzinger, Barbara Jobstmann, Rohit Singh
TACAS, pages 267-271, 2011.
[bibtex] [pdf]
[25] Symbolic Algorithms for Qualitative Analysis of Markov Decision Processes with Büchi Objectives
Krishnendu Chatterjee, Monika Henzinger, Manas Joglekar, Nisarg Shah
CAV, pages 260-276, 2011.
[bibtex] [pdf]
[24] The Complexity of Request-Response Games
Krishnendu Chatterjee, Thomas A. Henzinger, Florian Horn
LATA, pages 227-237, 2011.
[bibtex] [pdf]
[23] From boolean to quantitative synthesis
Pavol Cerný, Thomas A. Henzinger
EMSOFT, pages 149-154, 2011.
[bibtex] [pdf]
[22] Brief Announcement: Full Reversal Routing as a Linear Dynamical S ystem
Bernadette Charron-Bost, Matthias Függer, Jennifer L. Welch, Josef Widder
SPAA, 2011.
[bibtex] [pdf]
[21] Partial is Full
Bernadette Charron-Bost, Matthias Függer, Jennifer L. Welch, Josef Widder
18th International Colloquium on Structural Information and Communication Complexity (SIROCCO), 2011.
[bibtex] [pdf]
[20] Full Reversal Routing as a Linear Dynamical System
Bernadette Charron-Bost, Matthias Függer, Jennifer L. Welch, Josef Widder
18th International Colloquium on Structural Information and Communication Complexity (SIROCCO), 2011.
[bibtex] [pdf]
[19] A reduction from parity games to simple stochastic games
Krishnendu Chatterjee, Nathanaël Fijalkow
GandALF, pages 74-86, 2011.
[bibtex] [pdf]
[18] Finitary Languages
Krishnendu Chatterjee, Nathanaël Fijalkow
LATA, pages 216-226, 2011.
[bibtex] [pdf]
[17] On Memoryless Quantitative Objectives
Krishnendu Chatterjee, Laurent Doyen, Rohit Singh
FCT, pages 148-159, 2011.
[bibtex] [pdf]
[16] Qualitative concurrent parity games
K. Chatterjee, L. de Alfaro, T. Henzinger
ACM Trans. Comput. Log., volume 12, number 4, pages 28, 2011.
[bibtex] [pdf]
[15] Games and Markov Decision Processes with Mean-Payoff Parity and Energy Parity Objectives
Krishnendu Chatterjee, Laurent Doyen
MEMICS, pages 37-46, 2011.
[bibtex] [pdf]
[14] Energy and Mean-Payoff Parity Markov Decision Processes
Krishnendu Chatterjee, Laurent Doyen
MFCS, pages 206-218, 2011.
[bibtex] [pdf]
[13] Quantitative Synthesis for Concurrent Programs
Pavol Cerný, Krishnendu Chatterjee, Thomas A. Henzinger, Arjun Radhakrishna, Rohit Singh
CAV, pages 243-259, 2011.
[bibtex] [pdf]
[12] The Complexity of Quantitative Information Flow Problems
Pavol Cerný, Krishnendu Chatterjee, Thomas A. Henzinger
CSF, pages 205-217, 2011.
[bibtex] [pdf]
[11]Specification-centered robustness
Roderick Paul Bloem, Krishnendu Chatterjee, Karin Greimel, Thomas A. Henzinger, Barbara Jobstmann
Symposium on Industrial Embedded Systems (IEEE, ed.), pages 176 - 185, 2011.
[bibtex]
[10] Blocked Clause Elimination for QBF
Armin Biere, Florian Lonsing, Martina Seidl
CADE, pages 101-115, 2011.
[bibtex] [pdf]
[9] Determinizing Discounted-Sum Automata
Udi Boker, Thomas A. Henzinger
CSL, pages 82-96, 2011.
[bibtex] [pdf]
[8] Temporal Specifications with Accumulative Values
Udi Boker, Krishnendu Chatterjee, Thomas A. Henzinger, Orna Kupferman
LICS, pages 43-52, 2011.
[bibtex] [pdf]
[7] Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes
Tomás Brázdil, Václav Brozek, Krishnendu Chatterjee, Vojtech Forejt, Antonín Kucera
LICS, pages 33-42, 2011.
[bibtex] [pdf]
2010
[6] Obliging Games
Krishnendu Chatterjee, Florian Horn, Christof Löding
CONCUR, pages 284-296, 2010.
[bibtex] [pdf]
2009
[5] The Theta-Model: Achieving Synchrony without Clocks
Josef Widder, Ulrich Schmid
Distributed Computing, volume 22, number 1, pages 29-47, apr 2009, Springer Verlag.
[bibtex] [pdf] [doi]
[4] Towards a real-time distributed computing model
Heinrich Moser
Theoretical Computer Science, volume 410, number 6--7, pages 629-659, Feb 2009.
[bibtex] [pdf]
[3] Concurrency and Scalability versus Fragmentation and Compaction with Compact-fit
S.S. Craciunas, C.M. Kirsch, H. Payer, H. Röck, A. Sokolova
4 2009, Technical report, Department of Computer Sciences, University of Salzburg.
[bibtex] [pdf]
[2] Simulating Circuit-Level Simplifications on CNF
Matti Järvisalo, Armin Biere, Marijn Heule
Journal of Automated Reasoning, pages 1-37, Springer Netherlands.
Note: 10.1007/s10817-011-9239-9
[bibtex] [pdf]
[1]Brief Announcement: The Degrading Effect of Forgetting on a Synchronizer
Matthias Függer, Alexander Köß ler, Thomas Nowak, Martin Zeiner
Chapter in Stabilization, Safety, and Security of Distributed Systems, volume 7596 of Lecture Notes in Computer Science, Springer Berlin Heidelberg.
[bibtex]