Publications
2021
The probabilistic termination tool amber
Marcel Moosbrugger, Ezio Bartocci, Joost-Pieter Katoen, Laura Kovacs.
Proc. Of FM 2021: The 24th international symposium of formal methods, 2021.
Automated termination analysis of polynomial probabilistic programs
Marcel Moosbrugger, Ezio Bartocci, Joost-Pieter Katoen, Laura Kovacs.
Proc. Of ESOP 2021: The 30th european symposium on programming, pages 491-518, 2021.
[pdf] [doi]
2020
Preface of the special issue on the conference on formal methods in computer-aided design 2017
Daryl Stewart, Georg Weissenbacher.
Formal Methods in System Design, volume 56, pages 1, 2020.
[doi]
Eliminating message counters in threshold automata
Ilina Stoilkovska, Igor Konnov, Josef Widder, Florian Zuleger.
Automated technology for verification and analysis - 18th symposium, 2020, hanoi, vietnam, volume 12302, pages 196-212, 2020.
[pdf] [doi]
Beyond symbolic heaps: Deciding separation logic with inductive definitions
Jens Katelaan, Florian Zuleger.
23rd international conference on logic for programming, artificial intelligence and reasoning, alicante, spain, volume 73, pages 390-408, 2020.
[pdf] [doi]
Induction with generalization in superposition reasoning
Marton Hajdu, Petra Hozzova, Laura Kovacs, Johannes Schoisswohl, Andrei Voronkov.
Proceedings of the 13th international conference on intelligent computer mathematics, pages 123-137, 2020.
[pdf] [doi]
Stochastic fairness and language-theoretic fairness in planning in nondeterministic domains
Benjamin Aminof, Giuseppe De Giacomo, Sasha Rubin.
Proceedings of the thirtieth international conference on automated planning and scheduling, nancy, france, pages 20-28, 2020.
[pdf]
Synthesizing strategies under expected and exceptional environment behaviors
Benjamin Aminof, Giuseppe De Giacomo, Alessio R. Lomuscio, Aniello Murano, Sasha Rubin.
Proceedings of the twenty-ninth international joint conference on artificial intelligence, pages 1674-1680, 2020.
[pdf] [doi]
An ExpTime upper bound for ALC with integers (extended version)
Nadia Labai, Mantas Simkus, M.Magdalena Ortiz de la Fuente.
2020.
[pdf]
Pebble-intervals automata and FO2 with two orders
Nadia Labai, Tomer Kotek, M.Magdalena Ortiz de la Fuente, Helmut Veith.
14th international conference on language and automata theory and applications, pages 208-221, 2020.
[pdf] [doi]
Extracting safe thread schedules from incomplete model checking results
Patrick Metzler, Neeraj Suri, Georg Weissenbacher.
International Journal on Software Tools for Technology Transfer, volume 22, pages 565-581, 2020.
[pdf] [doi]
The polynomial complexity of vector addition systems with states
Florian Zuleger.
Foundations of software science and computation structures - 23rd international conference, dublin, ireland, volume 12077, pages 622-641, 2020.
[pdf] [doi]
Analysis of bayesian networks via prob-solvable loops
Ezio Bartocci, Laura Kovacs, Miroslav Stankovic.
Proc. Of ICTAC 2020: The 17th international colloquium on theoretical aspects of computing, pages 221-241, 2020.
[doi]
Algebra-based loop synthesis
Andreas Humenberger, Nikolaj Bjorner, Laura Kovacs.
Proceedings of the 16th international conference on integrated formal methods, pages 440-459, 2020.
[doi]
Thread-modular counter abstraction for parameterized program safety
Thomas Pani, Georg Weissenbacher, Florian Zuleger.
Formal methods in computer-aided design, pages 67-76, 2020.
[pdf] [doi]
Trace logic for inductive loop reasoning
Pamina Georgiou, Bernhard Gleiss, Laura Kovacs.
Proceedings of the 20th conference on formal methods in computer-aided design - FMCAD 2020, pages 255-263, 2020.
[pdf] [doi]
Language inclusion for finite prime event structures
Andreas Fellner, Thorsten Tarrach, Georg Weissenbacher.
Verification, model checking, and abstract interpretation, pages 314-336, 2020.
[doi]
Mora - automatic generation of moment-based invariants
Ezio Bartocci, Laura Kovacs, Miroslav Stankovic.
Proc. Of TACAS 2020: The 26th international conference on tools and algorithms for the construction and analysis of systems, pages 492-498, 2020.
[doi]
RAT elimination
Adrian Rebola Pardo, Georg Weissenbacher.
Logic for programming, artificial intelligence and reasoning, pages 423-448, 2020.
[pdf] [doi]
Layered clause selection for saturation-based theorem proving
Bernhard Gleiss, Martin Suda.
Joint proceedings of the 7th workshop on practical aspects of automated reasoning (PAAR) and the 5th satisfiability checking and symbolic computation workshop (SC-square) workshop, pages 34-52, 2020.
[pdf]
Layered clause selection for theory reasoning (short paper)
Bernhard Gleiss, Martin Suda.
Proceedings of the 10th international joint conference on automated reasoning (IJCAR), pages 402-409, 2020.
[pdf] [doi]
Subsumption demodulation in first-order theorem proving
Bernhard Gleiss, Laura Kovacs, Jakob Rath.
Proceedings of the 10th international joint conference on automated reasoning (IJCAR), pages 297-315, 2020.
[pdf] [doi]
ProbInG: Distribution recovery for invariant generation of probabilistic programs
Ezio Bartocci, Laura Kovacs, Efstathia Bura.
2020.
Multi-linear strategy extraction for QBF expansion proofs via local soundness
Matthias Schlaipfer, Friedrich Slivovsky, Georg Weissenbacher, Florian Zuleger.
SAT 2020: Theory and applications of satisfiability testing - SAT 2020, pages 429-446, 2020.
[pdf] [doi]
Proceedings of the 23rd international conference on logic for programming, artificial intelligence and reasoning (LPAR-23)
2020.
[pdf]
Formalizing graph trail properties in isabelle/HOL
Laura Kovacs, Hanna Elif Lachnitt, Stefan Szeider.
CICM 2020: Intelligent computer mathematics, pages 190-205, 2020.
[pdf] [doi]
2019
Forward subsumption demodulation - fast conditional rewriting in vampire
Bernhard Gleiss, Laura Kovacs, Jakob Rath.
2019.
Abstraction for reasoning about agent behavior with answer set programming
Zeynep Gözen Saribatur.
2019.
[pdf]
Trace reasoning for formal verification using the first-order superposition calculus
Pamina Georgiou, Bernhard Gleiss, Laura Kovacs, Matteo Maffei.
2019.
Interactive visualization of saturation attempts in vampire
Bernhard Gleiss, Laura Kovacs, Lena Schnedlitz.
Proceedings of the 15th international conference on integrated formal methods (iFM) 2019, pages 504-513, 2019.
[pdf] [doi]
Automatic generation of moment-based invariants for prob-solvable loops
Ezio Bartocci, Laura Kovacs, Miroslav Stankovic.
Proc. Of ATVA 2019: The 17th international symposium on automated technology for verification and analysis, pages 255-276, 2019.
[pdf] [doi]
Verifying relational properties using trace logic
Gilles Barthe, Renate Eilers, Pamina Georgiou, Bernhard Gleiss, Laura Kovacs, Matteo Maffei.
Proceedings of formal methods in computer aided design (FMCAD), pages 170-178, 2019.
[pdf] [doi]
Superposition reasoning about quantified bitvector formulas
David Damestani, Laura Kovacs, Martin Suda.
Proceedings of the 21st international symposium on symbolic and numeric algorithms for scientific computing (SYNASC), 2019, pages 95-99, 2019.
[doi]
Model-based, mutation-driven test-case generation via heuristic-guided branching search
Andreas Fellner, Willibald Krenn, Rupert Schlick, Thorsten Tarrach, Georg Weissenbacher.
ACM Transactions on Embedded Computing Systems, volume 18, 2019.
[doi]
Removing apparent singularities of linear difference systems
Moulay Barkatou, Maximilian Jaroschek.
Journal of Symbolic Computation, volume to appear, 2019.
[pdf] [doi]
Communication-closed asynchronous protocols
Andrei Damian, Cezara Dragoi, Alexandru Militaru, Josef Widder.
International conference on computer aided verification, pages 344-363, 2019.
[pdf] [doi]
Foreword
James Davenport, Laura Kovacs, Daniela Zaharie.
Mathematics in Computer Science, volume 13, pages 459-460, 2019.
[pdf] [doi]
Foreword - formalization of geometry, automated and interactive geometric reasoning
Pascal Schreck, Tetsuo Ida, Laura Kovacs.
Annals of Mathematics and Artificial Intelligence, volume 85, pages 71-72, 2019.
[pdf] [doi]
Mutation testing with hyperproperties
Andreas Fellner, Mitra Tabaei Befrouei, Georg Weissenbacher.
Proc. Of SEFM 2019: The 17th international conference on software engineering and formal methods, pages 203-221, 2019.
[doi]
Verifying safety of synchronous fault-tolerant algorithms by bounded model checking
Ilina Stoilkovska, Igor Konnov, Josef Widder, Florian Zuleger.
International conference on tools and algorithms for the construction and analysis of systems, pages 357-374, 2019.
[pdf]
SL-COMP: Competition of solvers for separation logic
Mihaela Sighireanu, Jens Katelaan, Christoph Matheja, Thomas Noll, Florian Zuleger, .
25th international conference, TACAS 2019, pages 116-132, 2019.
[pdf]
Pebble-intervals automata and FO2 with two orders (extended version
Nadia Labai, Tomer Kotek, M.Magdalena Ortiz de la Fuente, Helmut Veith.
2019.
[pdf]
Portfolio SAT and SMT solving of cardinality constraints in sensor network optimization
Gergely Kovasznai, Krisztian Gajdar, Laura Kovacs.
Proceedings of the 21st international symposium on symbolic and numeric algorithms for scientific computing (SYNASC), 2019, pages 85-91, 2019.
[doi]
Model-based diagnosis with multiple observations
Alexey Ignatiev, António Morgado, João Marques-Silva, Georg Weissenbacher.
International joint conference on artificial intelligence, pages 1108-1115, 2019.
[doi]
Extracting safe thread schedules from incomplete model checking results
Patrick Metzler, Neeraj Suri, Georg Weissenbacher.
Model checking software, pages 153-171, 2019.
[doi]
Planning under LTL environment specifications
Benjamin Aminof, Giuseppe De Giacomo, Aniello Murano, Sasha Rubin.
29th international conference on automated planning and scheduling, pages 31-39, 2019.
[pdf]
Probabilistic strategy logic
Benjamin Aminof, Marta Kwiatkowska, Bastien Maubert, Aniello Murano, Sasha Rubin.
28th international joint conference on artificial intelligence, pages 32-38, 2019.
[pdf]
Verification of randomized consensus algorithms under round-rigid adversaries
Nathalie Bertrand, Igor Konnov, Marijana Lazić, Josef Widder.
30th international conference on concurrency theory, pages 33:1-33:15, 2019.
[pdf] [doi]
Effective entailment checking for separation logic with inductive definitions
Jens Katelaan, Christoph Matheja, Florian Zuleger.
25th international conference, TACAS 2019, pages 319-336, 2019.
[pdf]
2018
Parameterized model checking of rendezvous systems
Benjamin Aminof, Tomer Kotek, Sasha Rubin, Francesco Spegni, Helmut Veith.
Distributed Computing, volume 31, pages 187-222, 2018.
[pdf] [doi]
Desingularization of first order linear difference systems with rational function coefficients
Moulay Barkatou, Maximilian Jaroschek.
Proceedings of the 2018 ACM international symposium on symbolic and algebraic computation (ISSAC), pages 39-46, 2018.
[pdf] [doi]
Efficient algorithms for asymptotic bounds on termination time in VASS
Tomas Brazdil, Krishnendu Chatterjee, Antonin Kucera, Peter Novotny, Dominik Velan, Florian Zuleger.
Proceedings of the 33rd annual ACM/IEEE symposium on logic in computer science, LICS 2018, oxford, UK, july 09-12, 2018, pages 185-194, 2018.
[pdf] [doi]
Efficient translation of sequent calculus proofs into natural deduction proofs
Gabriel Ebner, Matthias Schlaipfer.
PAAR 2018 practical aspects of automated reasoning, volume 2162, pages 17-33, 2018.
Incremental solving with vampire
Giles Reger, Martin Suda.
Proceedings of the 4th vampire workshop, volume 53, 2018.
[pdf] [doi]
Local proofs and AVATAR
Giles Reger, Martin Suda.
Proceedings of the 4th vampire workshop, volume 53, 2018.
[pdf] [doi]
Aligator.jl - a julia package for loop invariant generation
Andreas Humenberger, Maximilian Jaroschek, Laura Kovacs.
Proceedings of the 11th international conference on intelligent computer mathematics (CICM), pages 111-117, 2018.
[pdf] [doi]
A FOOLish encoding of the next state relations of imperative programs.
Evgenii Kotelnikov, Laura Kovacs, Andrei Voronkov.
Proceedings of the 9th international joint conference on automated reasoning (IJCAR) 2018, pages 405-421, 2018.
[doi]
Local soundness for QBF calculi
Martin Suda, Bernhard Gleiss.
Proceedings of the 21st international conference on theory and applications of satisfiability testing (SAT), pages 217-234, 2018.
[doi]
Automated clustering and program repair for introductory programming assignments
Ivan Radicek, Sumit Gulwani, Florian Zuleger.
Proceedings of the 39th ACM SIGPLAN conference on programming language design and implementation, PLDI 2018, philadelphia, PA, USA, june 18-22, 2018, pages 465-480, 2018.
[pdf] [doi]
Extended resolution simulates DRAT
Benjamin Kiesl, Adrian Rebola Pardo, Marijn Heule.
Proceedings of the 9th international joint conference on automated reasoning (IJCAR) 2018, pages 516-531, 2018.
[doi]
Inductive termination proofs with transition invariants and their relationship to the size-change abstraction
Florian Zuleger.
Static analysis - 25th international symposium, SAS 2018, freiburg, germany, august 29-31, 2018, proceedings, pages 423-444, 2018.
[pdf] [doi]
Reachability in parameterized systems: All flavors of threshold automata
Jure Kukovec, Igor Konnov, Josef Widder.
29th international conference on concurrency theory (CONCUR 2018), pages 19:1-19:17, 2018.
[pdf] [doi]
Rely-guarantee reasoning for automated bound analysis of lock-free algorithms
Thomas Pani, Georg Weissenbacher, Florian Zuleger.
Formal methods in computer-aided design, pages 1-9, 2018.
[pdf] [doi]
Synthesis under assumptions
Benjamin Aminof, Giuseppe De Giacomo, Aniello Murano, Sasha Rubin.
Principles of knowledge representation and reasoning: Proceedings of the sixteenth international conference, KR 2018, tempe, arizona, 30 october - 2 november 2018, pages 615-616, 2018.
[pdf]
Automated reasoning for systems engineering
Laura Kovacs.
Foundations of information and knowledge systems (FOIKS) 2018, pages 1, 2018.
Communication-closed layers as paradigm for distributed systems: A manifesto
Cezara Dragoi, Marijana Lazić, Josef Widder.
Sinteza 2018 international scientific conference on information technology and data related research, pages 131-138, 2018.
[pdf] [doi]
Unification with abstraction and theory instantiation in saturation-based reasoning
Giles Reger, Martin Suda, Andrei Voronkov.
Proceedings of the 24th international conference on tools and algorithms for the construction and analysis of systems (TACAS), pages 3-22, 2018.
[pdf]
Monadic refinements for relational cost analysis
Ivan Radicek, Gilles Barthe, Marco Gaboardi, Deepak Garg, Florian Zuleger.
Proceedings of the ACM on programming languages, volume New York, NY, USA, pages 1-32, 2018.
[pdf] [doi]
Parameterized model checking of synchronous distributed algorithms by abstraction
Benjamin Aminof, Ilina Stoilkovska, Sasha Rubin, Josef Widder, Florian Zuleger.
Verification, model checking, and abstract interpretation - 19th international conference, VMCAI 2018, los angeles, CA, USA, january 7-9, 2018, proceedings, pages 1-24, 2018.
[pdf] [doi]
From shapes to amortized complexity
Tomas Fiedor, Lukas Holik, Adam Rogalewicz, Moritz Sinn, Tomás Vojnar, Florian Zuleger.
Verification, model checking, and abstract interpretation - 19th international conference, VMCAI 2018, los angeles, CA, USA, january 7-9, 2018, proceedings, pages 205-225, 2018.
[pdf] [doi]
Using loop bound analysis for invariant generation
Pavel Čadek, Clemens Danninger, Moritz Sinn, Florian Zuleger.
Formal methods in computer-aided design, pages 1-9, 2018.
[pdf] [doi]
Invariant generation for multi-path loops with polynomial assignments
Andreas Humenberger, Maximilian Jaroschek, Laura Kovacs.
Verification, model checking, and abstract interpretation - 19th international conference, pages 226-246, 2018.
[pdf] [doi]
Randomized testing of distributed systems with probabilistic guarantees
Burcu Kulahcioglu Ozkan, Rupak Majumdar, Filip Niksic, Mitra Tabaei Befrouei, Georg Weissenbacher.
Proceedings of the ACM on Programming Languages, volume 2, 2018.
[pdf] [doi]
Reinterpreting dependency schemes: Soundness meets incompleteness in DQBF
Olaf Beyersdorff, Joshua Blinkhorn, Leroy Chew, Renate Schmidt, Martin Suda.
Journal of Automated Reasoning, volume J Autom Reasoning, pages 1-27, 2018.
[pdf] [doi]
CTL\* with graded path modalities
Benjamin Aminof, Aniello Murano, Sasha Rubin.
Information and Computation, volume 262, pages 1-21, 2018.
[pdf] [doi]
Parameterized model checking of synchronous distributed algorithms by abstraction
Benjamin Aminof, Sasha Rubin, Ilina Stoilkovska, Josef Widder, Florian Zuleger.
VMCAI, pages 1-24, 2018.
[pdf] [doi]
Graded modalities in strategy logic
Benjamin Aminof, Vadim Malvone, Aniello Murano, Sasha Rubin.
Information and Computation, volume 261, pages 634-649, 2018.
[pdf] [doi]
Loop analysis by quantification over iterations
Bernhard Gleiss, Laura Kovacs, Simon Robillard.
Proceedings of the 22nd international conference on logic for programming, artificial intelligence and reasoning (LPAR), pages 381-399, 2018.
[pdf] [doi]
Towards smarter MACE-style model finders
Mikolás Janota, Martin Suda.
LPAR-22. 22nd international conference on logic for programming, artificial intelligence and reasoning, awassa, ethiopia, 16-21 november 2018., pages 454-470, 2018.
[pdf] [doi]
A theory of satisfiability-preserving proofs in SAT solving
Adrian Rebola Pardo, Martin Suda.
International conference on logic for programming, artificial intelligence and reasoning, pages 583-603, 2018.
[pdf] [doi]
A separation logic with data: Small models and automation
Jens Katelaan, Dejan Jovanovic, Georg Weissenbacher.
Automated reasoning, pages 455-471, 2018.
[pdf] [doi]
2017
Global subsumption revisited (briefly)
Giles Reger, Martin Suda.
Vampire\@IJCAR 2016. Proceedings of the 3rd vampire workshop, coimbra, portugal, july 2, 2016., volume 44, pages 61-73, 2017.
[pdf]
Measuring progress to predict success: Can a good proof strategy be evolved?
Giles Reger, Martin Suda.
2017.
Instantiation and pretending to be an SMT solver with vampire
Giles Reger, Martin Suda, Andrei Voronkov.
2017.
Polynomial invariant generation for multi-path loops
Andreas Humenberger, Maximilian Jaroschek, Laura Kovacs.
2017.
Model-based, mutation-driven test case generation via heuristic-guided branching search
Andreas Fellner, Willibald Krenn, Rupert Schlick, Thorsten Tarrach, Georg Weissenbacher.
Proceedings of the 15th ACM-IEEE international conference on formal methods and models for system design, MEMOCODE 2017, vienna, austria, september 29 - october 02, 2017, pages 56-66, 2017.
[doi]
Optimizing big-data queries using program synthesis
Matthias Schlaipfer, Kaushik Rajan, Akash Lal, Malavika Samak.
Symposium on operating systems principles, pages 631-646, 2017.
[doi]
First-order interpolation and interpolating proof systems
Laura Kovacs, Andrei Voronkov.
LPAR-21. 21st international conference on logic for programming, artificial intelligence and reasoning, pages 49-64, 2017.
Fuzzing and verifying RAT refutations with deletion information
Walter Forkel, Tobias Philipp, Adrian Rebola Pardo, Elias Werner.
Florida artificial intelligence research society conference, pages 190-193, 2017.
Preface of the special issue in memoriam helmut veith
Georg Gottlob, Thomas A. Henzinger, Georg Weissenbacher.
Formal Methods in System Design, volume 51, pages 267-269, 2017.
[doi]
Empirical software metrics for benchmarking of verification tools
Yulia Demyanova, Thomas Pani, Helmut Veith, Florian Zuleger.
Formal Methods in System Design, volume 50, pages 289-316, 2017.
[doi]
Complexity and resource bound analysis of imperative programs using difference constraints
Moritz Sinn, Helmut Veith, Florian Zuleger.
Journal of Automated Reasoning, volume 59, pages 3-45, 2017.
On the completeness of bounded model checking for threshold-based distributed algorithms: reachability
Igor Konnov, Helmut Veith, Josef Widder.
Information and Computation, volume 252, pages 95-109, 2017.
[pdf] [doi]
Para\^2: Parameterized path reduction, acceleration, and SMT for reachability in threshold-guarded distributed algorithms
Igor Konnov, Marijana Lazić, Helmut Veith, Josef Widder.
Formal Methods in System Design, volume 51, pages 270-307, 2017.
[doi]
Towards a semantics of unsatisfiability proofs with inprocessing
Tobias Philipp, Adrian Rebola Pardo.
Logic programming and automated reasoning (LPAR), pages 65-84, 2017.
[pdf]
Replacing conjectures by positive knowledge: Inferring proven precise worst-case execution time bounds using symbolic execution
Jens Knoop, Laura Kovacs, Jakob Zwirchmayr.
Journal of Symbolic Computation, volume 80, pages 101-124, 2017.
[doi]
Formal solutions of completely integrable pfaffian systems with normal crossings
Maximilian Jaroschek, Moulay Barkatou, Suzy Maddah.
Journal of Symbolic Computation, volume 81, pages 41-68, 2017.
First-cycle games
Benjamin Aminof, Sasha Rubin.
Information and Computation, volume 254, pages 195-216, 2017.
Synthesis of distributed algorithms with parameterized threshold guards
Marijana Lazić, Igor Konnov, Josef Widder, Roderick Bloem.
OPODIS, pages 32:1-32:20, 2017.
[pdf] [doi]
A supervisory control algorithm based on property-directed reachability
Koen Claessen, Jonatan Kilhamn, Laura Kovacs, Bengt Lennartson.
13th international haifa verification conference (HVC), pages 115-130, 2017.
[doi]
Logic-based merging in fragments of classical logic with inputs from social choice theory
Adrian Haret.
Proceedings of the 5th international conference on algorithmic decision theory (ADT 2017), pages 374-378, 2017.
[doi]
Automated invention of strategies and term orderings for vampire
Jan Jakubuv, Martin Suda, Josef Urban.
GCAI 2017. 3rd global conference on artificial intelligence, pages 121-133, 2017.
[pdf]
Deviation in belief change on fragments of propositional logic
Adrian Haret, Stefan Woltran.
Proceedings of the 6th workshop on dynamics of knowledge and belief (DKB-2017) and the 5th workshop KI & kognition (KIK-2017), 2017.
Automata and program analysis
Laure Daviaud, Thomas Colcombet, Florian Zuleger.
Fundamentals of computation theory - 21st international symposium, FCT 2017, pages 3-10, 2017.
Lpopt: A rule optimization tool for answer set programming
Michael Morak, Manuel Bichler, Stefan Woltran.
Proceedings of the 26th InternationalSymposium on logic-based program synthesis and transformation (LOPSTR 2016), pages 114-130, 2017.
[doi]
First-order interpolation and grey areas of proofs
Laura Kovacs.
Proceedings of the 26th EACSL annual conference on computer science logic (CSL), volume 82, pages 3:1, 2017.
[doi]
Splitting proofs for interpolation
Bernhard Gleiss, Laura Kovacs, Martin Suda.
Automated deduction - CADE 26 - 26th international conference on automated deduction, gothenburg, sweden, august 6-11, 2017, proceedings, pages 291-309, 2017.
[pdf] [doi]
A unifying principle for clause elimination in first-order logic
Benjamin Kiesl, Martin Suda.
Automated deduction - CADE 26 - 26th international conference on automated deduction, gothenburg, sweden, august 6-11, 2017, proceedings, pages 274-290, 2017.
[pdf] [doi]
Checkable proofs for first-order theorem proving
Giles Reger, Martin Suda.
ARCADE 2017. 1st international workshop on automated reasoning: Challenges, applications, directions, exemplary achievements, pages 55-63, 2017.
[pdf]
Automated generation of non-linear loop invariants utilizing hypergeometric sequences
Andreas Humenberger, Maximilian Jaroschek, Laura Kovacs.
ISSAC '17 proceedings of the 2017 ACM on international symposium on symbolic and algebraic computation, pages 221-228, 2017.
[pdf] [doi]
Testing a saturation-based theorem prover: Experiences and challenges
Giles Reger, Martin Suda, Andrei Voronkov.
Tests and proofs - 11th international conference, TAP 2017, held as part of STAF 2017, marburg, germany, july 19-20, 2017, proceedings, pages 152-161, 2017.
[pdf] [doi]
Constructive satisfiability procedure for ALCP(z) (preliminary report)
Nadia Labai, Martin Homola, M.Magdalena Ortiz de la Fuente.
Proceedings of the 30th international workshop on description logics, pages 1-13, 2017.
[pdf]
Systematic predicate abstraction using variable roles
Yulia Demyanova, Philipp Rümmer, Florian Zuleger.
NASA formal methods - 9th international symposium, NFM 2017, pages 265-281, 2017.
Blocked clauses in first-order logic
Benjamin Kiesl, Martin Suda, Martina Seidl, Hans Tompits, Armin Biere.
LPAR-21. 21st international conference on logic for programming, artificial intelligence and reasoning, pages 31-48, 2017.
[pdf]
Set of support for theory reasoning
Giles Reger, Martin Suda.
IWIL\@LPAR 2017 workshop and LPAR-21 short presentations, maun, botswana, may 7-12, 2017, pages 124-134, 2017.
[pdf]
Unified reasoning about robustness properties of symbolic-heap separation logic
Jens Katelaan, Christina Jansen, Florian Zuleger, Christoph Matheja, Thomas Noll.
Programming languages and systems - 26th european symposium on programming, pages 611-638, 2017.
[doi]
On the automated verification of web applications with embedded SQL
Itzhaky Shachar, Tomer Kotek, Noam Rinetzky, Mooly Sagiv, Orr Tamir, Helmut Veith, Florian Zuleger.
20th international conference on database theory, ICDT 2017, pages 1-18, 2017.
A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms
Igor Konnov, Marijana Lazić, Helmut Veith, Josef Widder.
POPL, pages 719-734, 2017.
[pdf] [doi]
Coming to terms with quantified reasoning
Laura Kovacs, Simon Robillard, Andrei Voronkov.
Proceedings of the 44th ACM SIGPLAN symposium on principles of programming languages (POPL), pages 260-270, 2017.
[pdf] [doi]
Dynamic reductions for model checking concurrent software
Henning Günther, Alfons Laarman, Ana Sokolova, Georg Weissenbacher.
Verification, model checking, and abstract interpretation, pages 246-265, 2017.
[doi]
Theory-specific reasoning about loops with arrays using vampire
Yuting Chen, Laura Kovacs, Simon Robillard.
Proceedings of the third vampire workshop, 2017.
2016
AVATAR modulo theories
Giles Reger, Nikolaj Bjorner, Martin Suda, Andrei Voronkov.
GCAI 2016. 2nd global conference on artificial intelligence, pages 39-52, 2016.
[pdf]
New techniques in clausal form generation
Giles Reger, Martin Suda, Andrei Voronkov.
GCAI 2016. 2nd global conference on artificial intelligence, pages 11-23, 2016.
[pdf]
Lpopt: A rule optimization tool for answer set programming
Manuel Bichler, Michael Morak, Stefan Woltran.
Pre-proceedings of the 26th international symposium on logic-based program synthesis and transformation (LOPSTR 2016), 2016.
Beyond IC postulates: Classification criteria for merging operators
Adrian Haret, Andreas Pfandler, Stefan Woltran.
ECAI 2016 - 22nd european conference on artificial intelligence, pages 372-380, 2016.
[doi]
Monadic second order finite satisfiability and unbounded tree-width
Tomer Kotek, Helmut Veith, Florian Zuleger.
CSL, pages 1-20, 2016.
Parameterized systems in BIP: Design and model checking
Igor Konnov, Tomer Kotek, Qiang Wang, Helmut Veith, Simon Bliudze, Joseph Sifakis.
CONCUR, pages 30:1-30:16, 2016.
[pdf] [doi]
Extended graded modalities in strategy logic
Benjamin Aminof, Vadim Malvone, Aniello Murano, Sasha Rubin.
SR, pages 1-14, 2016.
Distributing knowledge into simple bases
Adrian Haret, Jean-Guy Mailly, Stefan Woltran.
Proceedings of the 25th international joint conference on artificial intelligence, pages 1109-1115, 2016.
[pdf]
Lifting QBF resolution calculi to DQBF
Olaf Beyersdorff, Leroy Chew, Renate Schmidt, Martin Suda.
Theory and applications of satisfiability testing - SAT 2016 - 19th international conference, bordeaux, france, july 5-8, 2016, proceedings, pages 490-499, 2016.
[pdf] [doi]
Finding finite models in multi-sorted first-order logic
Giles Reger, Martin Suda, Andrei Voronkov.
Theory and applications of satisfiability testing - SAT 2016 - 19th international conference, bordeaux, france, july 5-8, 2016, proceedings, pages 323-341, 2016.
[pdf] [doi]
Model checking parameterised multi-token systems via the composition method
Benjamin Aminof, Sasha Rubin.
IJCAR, pages 499-515, 2016.
Selecting the selection
Krystof Hoder, Giles Reger, Martin Suda, Andrei Voronkov.
Automated reasoning - 8th international joint conference, IJCAR 2016, coimbra, portugal, june 27 - july 2, 2016, proceedings, pages 313-329, 2016.
[pdf] [doi]
Duality in STRIPS planning
Martin Suda.
8th workshop on heuristics and search for domain-independent planning (HSDIP), london, UK, june 13, 2016, proceedings, pages 21-27, 2016.
[pdf]
Symbolic computation and automated reasoning for program analysis
Laura Kovacs.
Proceedings of the 12th international conference on integrated formal methods (iFM), volume 9681, pages 20-27, 2016.
[pdf] [doi]
Graded strategy logic: Reasoning about uniqueness of nash equilibria
Benjamin Aminof, Vadim Malvone, Aniello Murano, Sasha Rubin.
AAMAS, pages 698-706, 2016.
Automatic verification of multi-agent systems in parameterised grid-environments
Benjamin Aminof, Aniello Murano, Sasha Rubin, Florian Zuleger.
AAMAS, pages 1190-1199, 2016.
Prompt alternating-time epistemic logics
Benjamin Aminof, Aniello Murano, Sasha Rubin, Florian Zuleger.
KR, pages 258-267, 2016.
Merging of abstract argumentation frameworks
Jerome Delobelle, Adrian Haret, Sebastien Konieczny, Jean-Guy Mailly, Julien Rossit, Stefan Woltran.
Principles of knowledge representation and reasoning: Proceedings of the 15th international conference, pages 33-42, 2016.
[pdf]
Distributing knowledge into simple bases
Adrian Haret, Jean-Guy Mailly, Stefan Woltran.
Proceedings of the 16th international workshop on non-monotonic reasoning, 2016.
[pdf]
The vampire and the FOOL
Evgenii Kotelnikov, Laura Kovacs, Giles Reger, Andrei Voronkov.
Proceedings of the 5th ACM SIGPLAN conference on certified programs and proofs (CPP), pages 37-48, 2016.
[pdf] [doi]
What you always wanted to know about model checking of fault-tolerant distributed algorithms
Igor Konnov, Helmut Veith, Josef Widder.
Perspectives of system informatics: 10th international andrei ershov informatics conference, PSI 2015, pages 6-21, 2016.
[pdf] [doi]
A clausal normal form translation for FOOL
Evgenii Kotelnikov, Laura Kovacs, Martin Suda, Andrei Voronkov.
GCAI 2016. 2nd global conference on artificial intelligence, pages 53-71, 2016.
[pdf]
Error invariants for concurrent traces
Andreas Holzer, Daniel Schwartz-Narbonne, Mitra Tabaei Befrouei, Georg Weissenbacher, Thomas Wies.
Formal methods, pages 370-387, 2016.
[doi]
DRAT proofs for XOR reasoning
Tobias Philipp, Adrian Rebola Pardo.
Logics in artificial intelligence, pages 415-429, 2016.
[doi]
Desingularization of first order linear difference systems with rational function coefficients
Moulay Barkatou, Maximilian Jaroschek.
2016.
Desingularization of first order linear difference systems with rational function coefficients
Maximilian Jaroschek, Moulay Barkatou.
2016.
Model checking of threshold-based fault-tolerant distributed algorithms
Marijana Lazić, Igor Konnov, Helmut Veith, Josef Widder.
2016.
Parameterized verification of liveness of distributed algorithms
Igor Konnov, Marijana Lazić, Helmut Veith, Josef Widder.
2016.
Abstraction and mining of traces to explain concurrency bugs
Mitra Tabaei Befrouei, Chao Wang, Georg Weissenbacher.
Formal Methods in System Design, volume 49, pages 1-32, 2016.
[doi]
Labelled interpolation systems for hyper-resolution, clausal, and local proofs
Matthias Schlaipfer, Georg Weissenbacher.
Journal of Automated Reasoning, volume 57, pages 3-36, 2016.
[pdf] [doi]
Angry-HEX: An artificial player for angry birds based on declarative knowledge bases
Giovambattista Ianni, Francesco Calimeri, Stefano Germano, Andreas Humenberger, Christoph Redl, Daria Stepanova, Andrea Tucci, Anton Wimmer.
IEEE Transactions on Computational Intelligence and AI in Games, volume 8, pages 128-139, 2016.
[doi]
Decidability of parameterized verification
Roderick Bloem, Swen Jacobs, Ayrat Khalimov, Igor Konnov, Sasha Rubin, Helmut Veith, Josef Widder.
ACM SIGACT News, volume 47, pages 53-64, 2016.
[pdf] [doi]
The power of non-ground rules in answer set programming
Manuel Bichler, Michael Morak, Stefan Woltran.
Theory and Practice of Logic Programming, volume 16, pages 552-569, 2016.
[doi]
Treewidth-preserving modeling in ASP
Manuel Bichler, Bernhard Bliem, Marius Moldovan, Michael Morak, Stefan Woltran.
2016.
2015
Perspectives on white-box testing: Coverage, concurrency, and concolic execution
Azadeh Farzan, Andreas Holzer, Helmut Veith.
ICST, pages 1-11, 2015.
[doi]
SMT and POR beat counter abstraction: Parameterized model checking of threshold-based distributed algorithms
Igor Konnov, Helmut Veith, Josef Widder.
Computer aided verification, pages 85-102, 2015.
[doi]
On the expressive power of communication primitives in parameterised systems
Benjamin Aminof, Sasha Rubin, Florian Zuleger.
LPAR, pages 313-328, 2015.
[doi]
Boolean satisfiability solvers and their applications in model checking
Yakir Vizel, Georg Weissenbacher, Sharad Malik.
Proceedings of the IEEE, volume 103, pages 2021-2035, 2015.
[pdf] [doi]
Loop patterns in c programs
Thomas Pani, Helmut Veith, Florian Zuleger.
ECEASST, volume 72, 2015.
[pdf]
Under-approximating loops in c programs for fast counterexample detection
Matt Lewis, Daniel Kroening, Georg Weissenbacher.
Formal Methods in System Design, volume 47, pages 75-92, 2015.
[doi]
Efficient computation of generalized ising polynomials on graphs with fixed clique-width
Tomer Kotek, Johann A. Makowsky.
Topics in Theoretical Computer Science (TTCS), volume 9541, pages 135-146, 2015.
Merging in the horn fragment
Adrian Haret, Stefan Rümmele, Stefan Woltran.
Proceedings of the twenty-fourth international joint conference on artificial intelligence - IJCAI 2015, pages 3041-3047, 2015.
Closure properties and complexity of rational sets of regular languages
Andreas Holzer, Christian Schallhart, Michael Tautschnig, Helmut Veith.
Theoretical Computer Science, volume 605, pages 62-79, 2015.
[doi]
Bipartition polynomials, the ising model and domination in graphs
Markus Dod, Tomer Kotek, James Preen, Peter Tittmann.
Discussiones Mathematicae Graph Theory, volume 35, pages 335-353, 2015.
Time complexity of link reversal routing
Bernadette Charron-Bost, Matthias Függer, Jennifer Welch, Josef Widder.
ACM Transactions on Algorithms, volume 11, pages 1-39, 2015.
[pdf] [doi]
Abstraction and mining of traces to explain concurrency bugs
Mitra Tabaei Befrouei.
Proceedings of the young researchers' conference "frontiers of formal methods", 2015.
[pdf]
Difference constraints: An adequate abstraction for complexity analysis of imperative programs
Moritz Sinn, Helmut Veith, Florian Zuleger.
FMCAD, pages 144-151, 2015.
Logics of finite hankel rank
Nadia Labai, Johann A. Makowsky.
Fields of logic and computation II, volume 9300, pages 237-252, 2015.
[doi]
An extension-based approach to belief revision in abstract argumentation
Martin Diller, Adrian Haret, Thomas Linsbichler, Stefan Rümmele, Stefan Woltran.
Proceedings of the twenty-fourth international joint conference on artificial intelligence - IJCAI 2015, pages 2926-2932, 2015.
Compilation for secure two-party computations
Martin Franz, Andreas Holzer, Stefan Katzenbeisser, Christian Schallhart, Helmut Veith.
Software engineering & management 2015, pages 143-145, 2015.
Empirical software metrics for benchmarking of verification tools
Yulia Demyanova, Thomas Pani, Helmut Veith, Florian Zuleger.
CAV, pages 561-579, 2015.
[doi]
Decidability of parameterized verification
Roderick Bloem, Swen Jacobs, Ayrat Khalimov, Igor Konnov, Sasha Rubin, Helmut Veith, Josef Widder.
2015.
[doi]
LTSmin: High-performance language-independent model checking
Stefan Blom, Tom Dijk, Kant Gijis, Alfons Laarman, Jeroen Meijer, Jaco Pol.
TACAS, pages 692-707, 2015.
[doi]
Asymptotically precise ranking functions for deterministic size-change systems
Florian Zuleger.
CSR, pages 426-442, 2015.
[doi]
Liveness of parameterized timed networks
Benjamin Aminof, Sasha Rubin, Francesco Spegni, Florian Zuleger.
ICALP, volume 9135, pages 375-387, 2015.
[doi]
Extending ALCQIO with trees
Tomer Kotek, Mantas Simkus, Helmut Veith, Florian Zuleger.
LICS 2015, pages 511-522, 2015.
[pdf] [doi]
Proving safety with trace automata and bounded model checking
Matt Lewis, Daniel Kroening, Georg Weissenbacher.
Formal methods, pages 325-341, 2015.
[doi]
Verification of asynchronous mobile-robots in partially-known environments
Benjamin Aminof, Aniello Murano, Sasha Rubin, Florian Zuleger.
PRIMA, pages 185-200, 2015.
[doi]
2014
CBMC-GC: An ANSI c compiler for secure two-party computations
Martin Franz, Andreas Holzer, Stefan Katzenbeisser, Christian Schallhart, Helmut Veith.
Compiler construction, pages 244-249, 2014.
[doi]
Solvability-based comparison of failure detectors
Srikanth Sastry, Josef Widder.
NCA, pages 269-276, 2014.
[doi]
Parameterized model checking of rendezvous systems
Benjamin Aminof, Tomer Kotek, Sasha Rubin, Francesco Spegni, Helmut Veith.
CONCUR, pages 109-124, 2014.
[doi]
Approaching verification and validation challenges in smart grids
Tobias Deutsch, Josef Widder.
Tagungsband ComForEn 2014, 2014.
[pdf]
A logic-based framework for verifying consensus algorithms
Cezara Dragoi, Thomas A. Henzinger, Helmut Veith, Josef Widder, Damien Zufferey.
VMCAI, pages 161-181, 2014.
[doi]
Reduction of resolution refutations and interpolants via subsumption
Roderick Bloem, Sharad Malik, Matthias Schlaipfer, Georg Weissenbacher.
Haifa verification conference (HVC), pages 188-203, 2014.
[doi]
Merging in the horn fragment
Adrian Haret.
2014.
Partial-order reduction for multi-core LTL model checking
Alfons Laarman, Anton Wijs.
Haifa verification conference (HVC), pages 267-283, 2014.
[doi]
Parameterized model checking of token-passing systems
Benjamin Aminof, Swen Jacobs, Ayrat Khalimov, Sasha Rubin.
VMCAI, pages 262-281, 2014.
[doi]
Concolic testing of concurrent programs
Azadeh Farzan, Andreas Holzer, Niloofar Razavi, Helmut Veith.
Software engineering 2014, pages 101-102, 2014.
[pdf]
Reusing information in multi-goal reachability analyses
Dirk Beyer, Andreas Holzer, Michael Tautschnig, Helmut Veith.
Software engineering 2014, pages 97-98, 2014.
On the complexity of symbolic verification and decision problems in bit-vector logic
Andreas Fröhlich, Gergely Kovasznai, Armin Biere, Helmut Veith.
POS, 2014.
[pdf]
Towards a description logic for program analysis: Extending ALCQIO with reachability
Tomer Kotek, Mantas Simkus, Helmut Veith, Florian Zuleger.
International workshop on description logics, 2014.
[pdf]
Feedback generation for performance problems in introductory programming assignments
Sumit Gulwani, Ivan Radicek, Florian Zuleger.
FSE, pages 41-51, 2014.
[doi]
Complexity results and algorithms for argumentation - dung's frameworks and beyond
Johannes Peter Wallner.
2014.
[pdf]
Shape and content: Incorporating domain knowledge into shape analysis
Diego Calvanese, Tomer Kotek, Mantas Simkus, Helmut Veith, Florian Zuleger.
International workshop on description logics, 2014.
[pdf]
A simple and scalable static analysis for bound analysis and amortized complexity analysis
Moritz Sinn, Florian Zuleger, Helmut Veith.
CAV, pages 745-761, 2014.
[doi]
Counterexample to induction-guided abstraction-refinement (CTIGAR)
Johannes Birgmeier, Aaron Bradley, Georg Weissenbacher.
CAV, pages 829-846, 2014.
[doi]
Connection matrices and the definability of graph parameters
Tomer Kotek, Johann A. Makowsky.
Logical Methods in Computer Science, volume 10, pages 1-33, 2014.
[pdf]
Recurrence relations for graph polynomials on bi-iterative families of graphs
Tomer Kotek, Johann A. Makowsky.
European Journal of Combinatorics, volume 41, pages 47-67, 2014.
[doi]
Silicon fault diagnosis using sequence interpolation with backbones
Charlie Shucheng Zhu, Georg Weissenbacher, Sharad Malik.
ICCAD, pages 348-355, 2014.
[pdf]
On the complexity of symbolic verification and decision problems in bit-vector logic
Gergely Kovasznai, Helmut Veith, Andreas Fröhlich, Armin Biere.
2014.
Explaining the decompositionality of monadic second order logic using applications to combinatorics
Tomer Kotek.
2014.
Concolic testing of concurrent programs
Azadeh Farzan, Andreas Holzer, Niloofar Razavi, Helmut Veith.
2014.
Parameterized model checking of rendezvous systems
Benjamin Aminof, Tomer Kotek, Sasha Rubin, Francesco Spegni, Helmut Veith.
2014.
AngryHEX: An angry birds-playing agent based on HEX-programs
Francesco Calimeri, Michael Fink, Stefano Germano, Andreas Humenberger, Giovambattista Ianni, Christoph Redl, Daria Stepanova, Andrea Tucci.
2014.
On the complexity of symbolic verification and decision problems in bit-vector logic
Gergely Kovasznai, Helmut Veith, Andreas Fröhlich, Armin Biere.
MFCS, pages 481-492, 2014.
[doi]
Size-change abstraction and max-plus automata
Thomas Colcombet, Laure Daviaud, Florian Zuleger.
MFCS, pages 208-219, 2014.
[doi]
On the completeness of bounded model checking for threshold-based distributed algorithms: reachability
Igor Konnov, Helmut Veith, Josef Widder.
CONCUR, pages 125-140, 2014.
[doi]
Incremental bounded software model checking
Henning Günther, Georg Weissenbacher.
SPIN, pages 40-47, 2014.
[doi]
Shape and content - a database-theoretic perspective on the analysis of data structures
Diego Calvanese, Tomer Kotek, Mantas Simkus, Helmut Veith, Florian Zuleger.
IFM, pages 3-17, 2014.
[doi]
An open alternative for SMT-based verification of scade models
Henning Basold, Henning Günther, Michaela Huhn, Stefan Milius.
FMICS, pages 124-139, 2014.
[doi]
Abstraction and mining of traces to explain concurrency bugs
Mitra Tabaei Befrouei, Chao Wang, Georg Weissenbacher.
Runtime verification, pages 162-177, 2014.
[doi]
A representation theorem for (q-)holonomic sequences
Tomer Kotek, Johann A. Makowsky.
Journal of Computer and System Sciences, volume 80, pages 363-374, 2014.
[doi]
Tutorial on parameterized model checking of fault-tolerant distributed algorithms
Annu Gmeiner, Igor Konnov, Ulrich Schmid, Helmut Veith, Josef Widder.
Formal methods for executable software models, pages 122-171, 2014.
[doi]
2013
Mining sequential patterns to explain concurrent counterexamples
Stefan Leue, Mitra Tabaei Befrouei.
SPIN, pages 264-281, 2013.
[doi]
Formal verification of distributed algorithms (dagstuhl seminar 13141)
Bernadette Charron-Bost, Andrey Rybalchenko, Stephan Merz, Josef Widder.
2013.
[doi]
Information reuse for multi-goal reachability analyses
Dirk Beyer, Andreas Holzer, Michael Tautschnig, Helmut Veith.
ESOP, pages 472-491, 2013.
[doi]
Ramsey vs. Lexicographic termination proving
Byron Cook, Abigail See, Florian Zuleger.
Tools and algorithms for the construction and analysis of systems, pages 47-61, 2013.
[doi]
Solving constraints for generational search
Daniel Pötzl, Andreas Holzer.
TAP, pages 197-213, 2013.
[doi]
Verification across intellectual property boundaries
Sagar Chaki, Christian Schallhart, Helmut Veith.
ACM Transactions on Software Engineering and Methodology, volume 22, pages Article 15, 2013.
[doi]
Towards modeling and model checking fault-tolerant distributed algorithms
Annu John, Igor Konnov, Ulrich Schmid, Helmut Veith, Josef Widder.
SPIN, pages 209-226, 2013.
[pdf] [doi]
Under-approximating loops in c programs for fast counterexample detection
Daniel Kroening, Matt Lewis, Georg Weissenbacher.
CAV, pages 381-396, 2013.
[doi]
Brief announcement: Parameterized model checking of fault-tolerant distributed algorithms by abstraction
Annu John, Igor Konnov, Ulrich Schmid, Helmut Veith, Josef Widder.
PODC, pages 119-121, 2013.
[doi]
Advanced SAT techniques for abstract argumentation
Johannes Peter Wallner, Georg Weissenbacher, Stefan Woltran.
CLIMA, pages 138-154, 2013.
[doi]
Parameterized model checking of fault-tolerant distributed algorithms by abstraction
Annu John, Igor Konnov, Ulrich Schmid, Helmut Veith, Josef Widder.
FMCAD, pages 201-209, 2013.
[pdf]
On the concept of variable roles and its use in software analysis
Yulia Demyanova, Helmut Veith, Florian Zuleger.
FMCAD, pages 226-230, 2013.
[pdf]
Challenges in compiler construction for secure two-party computation
Andreas Holzer, Nikolaos Karvelas, Stefan Katzenbeisser, Helmut Veith.
PETShop, pages 3-6, 2013.
[doi]
The first workshop on language support for privacy-enhancing technologies (PETShop'13)
Martin Franz, Andreas Holzer, Rupak Majumdar, Bryan Parno, Helmut Veith.
CCS, pages 1485-1486, 2013.
[doi]
On the structure and complexity of rational sets of regular languages
Andreas Holzer, Christian Schallhart, Michael Tautschnig, Helmut Veith.
FSTTCS, pages 377-388, 2013.
[doi]
Link reversal routing with binary link labels: Work complexity
Bernadette Charron-Bost, Antoine Gaillard, Jennifer Welch, Josef Widder.
SIAM JOURNAL ON COMPUTING, volume 42, pages 634-661, 2013.
[pdf] [doi]
Con2colic testing
Azadeh Farzan, Andreas Holzer, Niloofar Razavi, Helmut Veith.
Esec/sigsoft fse, pages 37-47, 2013.
[doi]
2012
Parameterized model checking of fault-tolerant distributed algorithms
Annu John, Igor Konnov, Ulrich Schmid, Helmut Veith, Josef Widder.
2012.
A myhill-nerode theorem for automata with advice
Alex Kruckman, Sasha Rubin, John Sheridan, Ben Zax.
Symposium on games, automata, logics and formal verification, pages 238-246, 2012.
[doi]
Wait-free stabilizing dining using regular registers
Srikanth Sastry, Jennifer Welch, Josef Widder.
OPODIS, pages 284-299, 2012.
[doi]
Vinter: A vampire-based tool for interpolation
Krystof Hoder, Andreas Holzer, Laura Kovacs, Andrei Voronkov.
APLAS, pages 148-156, 2012.
[doi]
Counter attack against byzantine generals
Annu John, Igor Konnov, Ulrich Schmid, Helmut Veith, Josef Widder.
2012.
Who is afraid of model checking distributed algorithms?
Igor Konnov, Helmut Veith, Josef Widder.
2012.
Coverage-based trace signal selection for fault localisation in post-silicon validation
Zhu Charlie Shucheng, Georg Weissenbacher, Sharad Malik.
Haifa verification conference (HVC), pages 132-147, 2012.
[doi]
Secure two-party computations in ANSI c
Andreas Holzer, Martin Franz, Stefan Katzenbeisser, Helmut Veith.
ACM conference on computer and communications security, pages 772-783, 2012.
[doi]
Bounded-interference sequentialization for testing concurrent programs
Niloofar Razavi, Azadeh Farzan, Andreas Holzer.
Leveraging applications of formal methods, verification and validation. Technologies for mastering change, pages 372-387, 2012.
[doi]
Parallel assertions for architectures with weak memory models
Daniel Schwartz-Narbonne, Georg Weissenbacher, Sharad Malik.
Automated technology for verification and analysis, pages 254-268, 2012.
[doi]
Efficient checking of link-reversal-based concurrent systems
Matthias Függer, Josef Widder.
CONCUR 2012 - concurrency theory, pages 486-499, 2012.
[doi]
Interpretations in trees with countably many branches
Alexander Rabinovic, Sasha Rubin.
Logic in computer science, pages 551-560, 2012.
[pdf] [doi]
Interpolant strength revisited
Georg Weissenbacher.
International conference on theory and applications of satisfiability testing (SAT), pages 312-326, 2012.
[pdf] [doi]
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, pages 299-321, 2012.
[pdf] [doi]
Special issue: Games in verification (foreword)
Helmut Veith.
Journal of Computer and System Sciences, volume 78, pages 393, 2012.
[pdf] [doi]
Selected papers of the conference "computer science logic CSL 2010": preface
Anuj Dawar, Helmut Veith.
Logical Methods in Computer Science, 2012.
[pdf] [doi]
Proving reachability using FShell
Andreas Holzer, Daniel Kroening, Christian Schallhart, Michael Tautschnig, Helmut Veith.
Proc. Of 18th international conference on tools and algorithms for the construction and analysis of systems (TACAS), pages 538-541, 2012.
[pdf] [doi]
Who is afraid of model checking distributed algorithms?
Annu John, Igor Konnov, Ulrich Schmid, Helmut Veith, Josef Widder.
2012.
2011
On efficient checking of link-reversal-based concurrent systems
Matthias Függer, Josef Widder.
2011.
Seamless testing for models and code
Andreas Holzer, Visar Januzaj, Stefan Kugele, Boris Langer, Christian Schallhart, Michael Tautschnig, Helmut Veith.
Lecture notes in computer science, pages 278-293, 2011.
[doi]
Improving the confidence in measurement-based timing analysis
Sven Bünte, Michael Zolda, Michael Tautschnig, Raimund Kirner.
2011 14th IEEE international symposium on object/component/service-oriented real-time distributed computing (ISORC 2011), pages 144-151, 2011.
Query-driven program testing
Michael Tautschnig.
2011.
Bound analysis of imperative programs with the size-change abstraction
Florian Zuleger, Moritz Sinn, Sumit Gulwani, Helmut Veith.
Lecture notes in computer science, pages 280-297, 2011.
[doi]
Decision procedures in soft, hard and bio-ware - follow up (dagstuhl seminar 11272)
Nikolaj Bjorner, Robert Nieuwenhuis, Helmut Veith, Andrei Voronkov.
Dagstuhl Reports, volume 1, pages 23-35, 2011.
[pdf] [doi]
Malware detection
Stefan Katzenbeisser, Johannes Kinder, Helmut Veith.
Encyclopedia of cryptography and security, pages 752-755, 2011.
[pdf] [doi]
2010
The reachability-bound problem
Sumit Gulwani, Florian Zuleger.
PLDI'10 proceedings of teh ACM SIGPLAN conference on programming language design and implementation, pages 292-304, 2010.
[doi]
Don't care in SMT---building flexible yet efficient abstraction/refinement solvers
Andreas Bauer, Martin Leucker, Christian Schallhart, Michael Tautschnig.
International Journal on Software Tools for Technology Transfer, volume 12, pages 23-37, 2010.
[doi]
On the distributivity of LTL specifications
Marko Samer, Helmut Veith.
ACM Transactions on Computational Logic, volume 11, 2010.
[doi]
Seamless model-driven development put into practice
Wolfgang Haberl, Markus Herrmannsdoerfer, Stefan Kugele, Michael Tautschnig, Martin Wechs.
Proceedings of 4th international symposium on leveraging applications, pages 18-32, 2010.
[doi]
Timely time estimates
Andreas Holzer, Visar Januzaj, Stefan Kugele, Michael Tautschnig.
Proceedings of 4th international symposium on leveraging applications (ISoLA 2010), pages 33-46, 2010.
[doi]
An introduction to test specification in FQL
Andreas Holzer, Christian Schallhart, Michael Tautschnig, Helmut Veith.
Lecture notes in computer science, pages 9-22, 2010.
[doi]
How did you specify your test suite?
Andreas Holzer, Christian Schallhart, Michael Tautschnig, Helmut Veith.
Proceedings of the 25th IEEE/ACM international conference on automated software engineering (ASE 2010), pages 407-416, 2010.
[doi]
Proactive detection of computer worms using model checking
Johannes Kinder, Stefan Katzenbeisser, Christian Schallhart, Helmut Veith.
IEEE Transactions on Dependable and Secure Computing, volume 7, pages 424-438, 2010.
[doi]
Semantic integrity in large-scale online simulations
Somesh Jha, Stefan Katzenbeisser, Christian Schallhart, Helmut Veith, Stephen Chenney.
ACM Transactions on Internet Technology, volume 10, 2010.
[doi]
2007
Architecture and security in networked virtual environments
Christian Schallhart.
2007.
Towards a systematic design of fault-tolerant asynchronous circuits
Ulrich Schmid, Andreas Steininger, Helmut Veith.
Fachtagung zuverlässigkeit und entwurf, pages 173-174, 2007.
2006
From temporal logic queries to vacuity detection
Marko Samer, Helmut Veith.
Verification of infinite-state systems with applications to security, pages 149-167, 2006.
2005
Deterministic CTL query solving
Marko Samer, Helmut Veith.
Proceedings of the 12th international symposium on temporal representation and reasoning, pages 156-165, 2005.
2004
Counterexamples revisited: Principles, algorithms, applications
Edmund Clarke, Helmut Veith.
Verification: Theory and practice: Essays dedicated to zohar manna on the occasion of his 64th birthday, pages 208-224, 2004.
SAT based predicate abstraction for hardware verification
Edmund Clarke, Muralidhar Talupur, Helmut Veith, Dong Wang.
Lecture notes in computer science, pages 78-92, 2004.
Reasoning about specifications in model checking
Marko Samer.
2004.
Cryptographic watermarking
Stefan Katzenbeisser.
2004.
A syntactic characterization of distributive LTL queries
Marko Samer, Helmut Veith.
Proceedings of the 31st international colloquium on automata, languages and programming, pages 1099-1110, 2004.
Parameterized vacuity
Marko Samer, Helmut Veith.
Proceedings of the 5th international conference on formal methods in computer-aided design, pages 322-336, 2004.
2003
Integrating publish/subscribe into a mobile teamwork support platform
N. Sagar, Pascal Fenkam, Helmut Veith, Harald Gall, Engin Kirda, Somesh Jha.
Proceedings of the 15th international conference on software engineering and knowledge engineering, pages 510-517, 2003.
Friends or foes? Communities in software verification
Helmut Veith.
Lecture notes in computer science, pages 528-529, 2003.
Watermarking schemes provably secure against copy and ambiguity attacks
André Adelsbach, Stefan Katzenbeisser, Helmut Veith.
Porceedings of the 2003 ACM workshop on digital rights management, pages 111-119, 2003.
Counterexample-guided abstraction refinement for symbolic model checking
Edmund Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, Helmut Veith.
Journal of the ACM, volume Volume 50, pages 752-794, 2003.
Validity of CTL queries revisited
Marko Samer, Helmut Veith.
Proceedings of the 12th annual conference of the european association for computer science logic, pages 470-483, 2003.
Symbolic model checking using NUSMV
Andreas Plaickner.
2003.
Symbolic model checking using NUSMV
Andreas Plaickner.
2003.
Modular verification of software components in c\*
Sagar Chaki, Edmund Clarke, Alex Groce, Somesh Jha, Helmut Veith.
Proceedings of the 25^th^ conference on software engineering, pages 385-395, 2003.
2002
Securing symmetric watermarking schemes against protocol attacks
Stefan Katzenbeisser, Helmut Veith.
Proceedings of SPIE 2002, pages 260-268, 2002.
Tree-like counterexamples in model cheking
Edmund Clarke, Somesh Jha, Yuan Lu, Helmut Veith.
Proceedings of the seventeenth annual IEEE symposium on logic in computer science (LICS' 2002), pages 19-29, 2002.
On the complexity of data disjunctions
Thomas Eiter, Helmut Veith.
Theoretical Computer Science, volume 288, pages 101-128, 2002.
Datalog LITE: A deductive query language with linear time model checking
Georg Gottlob, Erich Grädel, Helmut Veith.
ACM Transactions on Computational Logic, volume Volume 3, pages 42-79, 2002.
Temporal logic queries in model checking
Marko Samer.
2002.
Automated abstraction refinement for model checking large state spaces using SAT based conflict analysis
Pankaj Chauhan, Edmund Clarke, James Kukula, Samir Sapra, Helmut Veith, Dong Wang.
Proceedings of the 4^th^ international conference on formal methods in computer-aided design, pages 33-51, 2002.
[pdf]
The probabilistic termination tool amber
Marcel Moosbrugger, Ezio Bartocci, Joost-Pieter Katoen, Laura Kovacs.
Proc. Of FM 2021: The 24th international symposium of formal methods, 2021.
Marcel Moosbrugger, Ezio Bartocci, Joost-Pieter Katoen, Laura Kovacs.
Proc. Of FM 2021: The 24th international symposium of formal methods, 2021.
Automated termination analysis of polynomial probabilistic programs
Marcel Moosbrugger, Ezio Bartocci, Joost-Pieter Katoen, Laura Kovacs.
Proc. Of ESOP 2021: The 30th european symposium on programming, pages 491-518, 2021.
[pdf] [doi]
Marcel Moosbrugger, Ezio Bartocci, Joost-Pieter Katoen, Laura Kovacs.
Proc. Of ESOP 2021: The 30th european symposium on programming, pages 491-518, 2021.
[pdf] [doi]
Preface of the special issue on the conference on formal methods in computer-aided design 2017
Daryl Stewart, Georg Weissenbacher.
Formal Methods in System Design, volume 56, pages 1, 2020.
[doi]
Daryl Stewart, Georg Weissenbacher.
Formal Methods in System Design, volume 56, pages 1, 2020.
[doi]
Eliminating message counters in threshold automata
Ilina Stoilkovska, Igor Konnov, Josef Widder, Florian Zuleger.
Automated technology for verification and analysis - 18th symposium, 2020, hanoi, vietnam, volume 12302, pages 196-212, 2020.
[pdf] [doi]
Ilina Stoilkovska, Igor Konnov, Josef Widder, Florian Zuleger.
Automated technology for verification and analysis - 18th symposium, 2020, hanoi, vietnam, volume 12302, pages 196-212, 2020.
[pdf] [doi]
Beyond symbolic heaps: Deciding separation logic with inductive definitions
Jens Katelaan, Florian Zuleger.
23rd international conference on logic for programming, artificial intelligence and reasoning, alicante, spain, volume 73, pages 390-408, 2020.
[pdf] [doi]
Jens Katelaan, Florian Zuleger.
23rd international conference on logic for programming, artificial intelligence and reasoning, alicante, spain, volume 73, pages 390-408, 2020.
[pdf] [doi]
Induction with generalization in superposition reasoning
Marton Hajdu, Petra Hozzova, Laura Kovacs, Johannes Schoisswohl, Andrei Voronkov.
Proceedings of the 13th international conference on intelligent computer mathematics, pages 123-137, 2020.
[pdf] [doi]
Marton Hajdu, Petra Hozzova, Laura Kovacs, Johannes Schoisswohl, Andrei Voronkov.
Proceedings of the 13th international conference on intelligent computer mathematics, pages 123-137, 2020.
[pdf] [doi]
Stochastic fairness and language-theoretic fairness in planning in nondeterministic domains
Benjamin Aminof, Giuseppe De Giacomo, Sasha Rubin.
Proceedings of the thirtieth international conference on automated planning and scheduling, nancy, france, pages 20-28, 2020.
[pdf]
Benjamin Aminof, Giuseppe De Giacomo, Sasha Rubin.
Proceedings of the thirtieth international conference on automated planning and scheduling, nancy, france, pages 20-28, 2020.
[pdf]
Synthesizing strategies under expected and exceptional environment behaviors
Benjamin Aminof, Giuseppe De Giacomo, Alessio R. Lomuscio, Aniello Murano, Sasha Rubin.
Proceedings of the twenty-ninth international joint conference on artificial intelligence, pages 1674-1680, 2020.
[pdf] [doi]
Benjamin Aminof, Giuseppe De Giacomo, Alessio R. Lomuscio, Aniello Murano, Sasha Rubin.
Proceedings of the twenty-ninth international joint conference on artificial intelligence, pages 1674-1680, 2020.
[pdf] [doi]
An ExpTime upper bound for ALC with integers (extended version)
Nadia Labai, Mantas Simkus, M.Magdalena Ortiz de la Fuente.
2020.
[pdf]
Nadia Labai, Mantas Simkus, M.Magdalena Ortiz de la Fuente.
2020.
[pdf]
Pebble-intervals automata and FO2 with two orders
Nadia Labai, Tomer Kotek, M.Magdalena Ortiz de la Fuente, Helmut Veith.
14th international conference on language and automata theory and applications, pages 208-221, 2020.
[pdf] [doi]
Nadia Labai, Tomer Kotek, M.Magdalena Ortiz de la Fuente, Helmut Veith.
14th international conference on language and automata theory and applications, pages 208-221, 2020.
[pdf] [doi]
Extracting safe thread schedules from incomplete model checking results
Patrick Metzler, Neeraj Suri, Georg Weissenbacher.
International Journal on Software Tools for Technology Transfer, volume 22, pages 565-581, 2020.
[pdf] [doi]
Patrick Metzler, Neeraj Suri, Georg Weissenbacher.
International Journal on Software Tools for Technology Transfer, volume 22, pages 565-581, 2020.
[pdf] [doi]
The polynomial complexity of vector addition systems with states
Florian Zuleger.
Foundations of software science and computation structures - 23rd international conference, dublin, ireland, volume 12077, pages 622-641, 2020.
[pdf] [doi]
Florian Zuleger.
Foundations of software science and computation structures - 23rd international conference, dublin, ireland, volume 12077, pages 622-641, 2020.
[pdf] [doi]
Analysis of bayesian networks via prob-solvable loops
Ezio Bartocci, Laura Kovacs, Miroslav Stankovic.
Proc. Of ICTAC 2020: The 17th international colloquium on theoretical aspects of computing, pages 221-241, 2020.
[doi]
Ezio Bartocci, Laura Kovacs, Miroslav Stankovic.
Proc. Of ICTAC 2020: The 17th international colloquium on theoretical aspects of computing, pages 221-241, 2020.
[doi]
Algebra-based loop synthesis
Andreas Humenberger, Nikolaj Bjorner, Laura Kovacs.
Proceedings of the 16th international conference on integrated formal methods, pages 440-459, 2020.
[doi]
Andreas Humenberger, Nikolaj Bjorner, Laura Kovacs.
Proceedings of the 16th international conference on integrated formal methods, pages 440-459, 2020.
[doi]
Thread-modular counter abstraction for parameterized program safety
Thomas Pani, Georg Weissenbacher, Florian Zuleger.
Formal methods in computer-aided design, pages 67-76, 2020.
[pdf] [doi]
Thomas Pani, Georg Weissenbacher, Florian Zuleger.
Formal methods in computer-aided design, pages 67-76, 2020.
[pdf] [doi]
Trace logic for inductive loop reasoning
Pamina Georgiou, Bernhard Gleiss, Laura Kovacs.
Proceedings of the 20th conference on formal methods in computer-aided design - FMCAD 2020, pages 255-263, 2020.
[pdf] [doi]
Pamina Georgiou, Bernhard Gleiss, Laura Kovacs.
Proceedings of the 20th conference on formal methods in computer-aided design - FMCAD 2020, pages 255-263, 2020.
[pdf] [doi]
Language inclusion for finite prime event structures
Andreas Fellner, Thorsten Tarrach, Georg Weissenbacher.
Verification, model checking, and abstract interpretation, pages 314-336, 2020.
[doi]
Andreas Fellner, Thorsten Tarrach, Georg Weissenbacher.
Verification, model checking, and abstract interpretation, pages 314-336, 2020.
[doi]
Mora - automatic generation of moment-based invariants
Ezio Bartocci, Laura Kovacs, Miroslav Stankovic.
Proc. Of TACAS 2020: The 26th international conference on tools and algorithms for the construction and analysis of systems, pages 492-498, 2020.
[doi]
Ezio Bartocci, Laura Kovacs, Miroslav Stankovic.
Proc. Of TACAS 2020: The 26th international conference on tools and algorithms for the construction and analysis of systems, pages 492-498, 2020.
[doi]
RAT elimination
Adrian Rebola Pardo, Georg Weissenbacher.
Logic for programming, artificial intelligence and reasoning, pages 423-448, 2020.
[pdf] [doi]
Adrian Rebola Pardo, Georg Weissenbacher.
Logic for programming, artificial intelligence and reasoning, pages 423-448, 2020.
[pdf] [doi]
Layered clause selection for saturation-based theorem proving
Bernhard Gleiss, Martin Suda.
Joint proceedings of the 7th workshop on practical aspects of automated reasoning (PAAR) and the 5th satisfiability checking and symbolic computation workshop (SC-square) workshop, pages 34-52, 2020.
[pdf]
Bernhard Gleiss, Martin Suda.
Joint proceedings of the 7th workshop on practical aspects of automated reasoning (PAAR) and the 5th satisfiability checking and symbolic computation workshop (SC-square) workshop, pages 34-52, 2020.
[pdf]
Layered clause selection for theory reasoning (short paper)
Bernhard Gleiss, Martin Suda.
Proceedings of the 10th international joint conference on automated reasoning (IJCAR), pages 402-409, 2020.
[pdf] [doi]
Bernhard Gleiss, Martin Suda.
Proceedings of the 10th international joint conference on automated reasoning (IJCAR), pages 402-409, 2020.
[pdf] [doi]
Subsumption demodulation in first-order theorem proving
Bernhard Gleiss, Laura Kovacs, Jakob Rath.
Proceedings of the 10th international joint conference on automated reasoning (IJCAR), pages 297-315, 2020.
[pdf] [doi]
Bernhard Gleiss, Laura Kovacs, Jakob Rath.
Proceedings of the 10th international joint conference on automated reasoning (IJCAR), pages 297-315, 2020.
[pdf] [doi]
ProbInG: Distribution recovery for invariant generation of probabilistic programs
Ezio Bartocci, Laura Kovacs, Efstathia Bura.
2020.
Ezio Bartocci, Laura Kovacs, Efstathia Bura.
2020.
Multi-linear strategy extraction for QBF expansion proofs via local soundness
Matthias Schlaipfer, Friedrich Slivovsky, Georg Weissenbacher, Florian Zuleger.
SAT 2020: Theory and applications of satisfiability testing - SAT 2020, pages 429-446, 2020.
[pdf] [doi]
Matthias Schlaipfer, Friedrich Slivovsky, Georg Weissenbacher, Florian Zuleger.
SAT 2020: Theory and applications of satisfiability testing - SAT 2020, pages 429-446, 2020.
[pdf] [doi]
Proceedings of the 23rd international conference on logic for programming, artificial intelligence and reasoning (LPAR-23)
2020.
[pdf]
2020.
[pdf]
Formalizing graph trail properties in isabelle/HOL
Laura Kovacs, Hanna Elif Lachnitt, Stefan Szeider.
CICM 2020: Intelligent computer mathematics, pages 190-205, 2020.
[pdf] [doi]
Laura Kovacs, Hanna Elif Lachnitt, Stefan Szeider.
CICM 2020: Intelligent computer mathematics, pages 190-205, 2020.
[pdf] [doi]
Forward subsumption demodulation - fast conditional rewriting in vampire
Bernhard Gleiss, Laura Kovacs, Jakob Rath.
2019.
Bernhard Gleiss, Laura Kovacs, Jakob Rath.
2019.
Abstraction for reasoning about agent behavior with answer set programming
Zeynep Gözen Saribatur.
2019.
[pdf]
Zeynep Gözen Saribatur.
2019.
[pdf]
Trace reasoning for formal verification using the first-order superposition calculus
Pamina Georgiou, Bernhard Gleiss, Laura Kovacs, Matteo Maffei.
2019.
Pamina Georgiou, Bernhard Gleiss, Laura Kovacs, Matteo Maffei.
2019.
Interactive visualization of saturation attempts in vampire
Bernhard Gleiss, Laura Kovacs, Lena Schnedlitz.
Proceedings of the 15th international conference on integrated formal methods (iFM) 2019, pages 504-513, 2019.
[pdf] [doi]
Bernhard Gleiss, Laura Kovacs, Lena Schnedlitz.
Proceedings of the 15th international conference on integrated formal methods (iFM) 2019, pages 504-513, 2019.
[pdf] [doi]
Automatic generation of moment-based invariants for prob-solvable loops
Ezio Bartocci, Laura Kovacs, Miroslav Stankovic.
Proc. Of ATVA 2019: The 17th international symposium on automated technology for verification and analysis, pages 255-276, 2019.
[pdf] [doi]
Ezio Bartocci, Laura Kovacs, Miroslav Stankovic.
Proc. Of ATVA 2019: The 17th international symposium on automated technology for verification and analysis, pages 255-276, 2019.
[pdf] [doi]
Verifying relational properties using trace logic
Gilles Barthe, Renate Eilers, Pamina Georgiou, Bernhard Gleiss, Laura Kovacs, Matteo Maffei.
Proceedings of formal methods in computer aided design (FMCAD), pages 170-178, 2019.
[pdf] [doi]
Gilles Barthe, Renate Eilers, Pamina Georgiou, Bernhard Gleiss, Laura Kovacs, Matteo Maffei.
Proceedings of formal methods in computer aided design (FMCAD), pages 170-178, 2019.
[pdf] [doi]
Superposition reasoning about quantified bitvector formulas
David Damestani, Laura Kovacs, Martin Suda.
Proceedings of the 21st international symposium on symbolic and numeric algorithms for scientific computing (SYNASC), 2019, pages 95-99, 2019.
[doi]
David Damestani, Laura Kovacs, Martin Suda.
Proceedings of the 21st international symposium on symbolic and numeric algorithms for scientific computing (SYNASC), 2019, pages 95-99, 2019.
[doi]
Model-based, mutation-driven test-case generation via heuristic-guided branching search
Andreas Fellner, Willibald Krenn, Rupert Schlick, Thorsten Tarrach, Georg Weissenbacher.
ACM Transactions on Embedded Computing Systems, volume 18, 2019.
[doi]
Andreas Fellner, Willibald Krenn, Rupert Schlick, Thorsten Tarrach, Georg Weissenbacher.
ACM Transactions on Embedded Computing Systems, volume 18, 2019.
[doi]
Removing apparent singularities of linear difference systems
Moulay Barkatou, Maximilian Jaroschek.
Journal of Symbolic Computation, volume to appear, 2019.
[pdf] [doi]
Moulay Barkatou, Maximilian Jaroschek.
Journal of Symbolic Computation, volume to appear, 2019.
[pdf] [doi]
Communication-closed asynchronous protocols
Andrei Damian, Cezara Dragoi, Alexandru Militaru, Josef Widder.
International conference on computer aided verification, pages 344-363, 2019.
[pdf] [doi]
Andrei Damian, Cezara Dragoi, Alexandru Militaru, Josef Widder.
International conference on computer aided verification, pages 344-363, 2019.
[pdf] [doi]
Foreword
James Davenport, Laura Kovacs, Daniela Zaharie.
Mathematics in Computer Science, volume 13, pages 459-460, 2019.
[pdf] [doi]
James Davenport, Laura Kovacs, Daniela Zaharie.
Mathematics in Computer Science, volume 13, pages 459-460, 2019.
[pdf] [doi]
Foreword - formalization of geometry, automated and interactive geometric reasoning
Pascal Schreck, Tetsuo Ida, Laura Kovacs.
Annals of Mathematics and Artificial Intelligence, volume 85, pages 71-72, 2019.
[pdf] [doi]
Pascal Schreck, Tetsuo Ida, Laura Kovacs.
Annals of Mathematics and Artificial Intelligence, volume 85, pages 71-72, 2019.
[pdf] [doi]
Mutation testing with hyperproperties
Andreas Fellner, Mitra Tabaei Befrouei, Georg Weissenbacher.
Proc. Of SEFM 2019: The 17th international conference on software engineering and formal methods, pages 203-221, 2019.
[doi]
Andreas Fellner, Mitra Tabaei Befrouei, Georg Weissenbacher.
Proc. Of SEFM 2019: The 17th international conference on software engineering and formal methods, pages 203-221, 2019.
[doi]
Verifying safety of synchronous fault-tolerant algorithms by bounded model checking
Ilina Stoilkovska, Igor Konnov, Josef Widder, Florian Zuleger.
International conference on tools and algorithms for the construction and analysis of systems, pages 357-374, 2019.
[pdf]
Ilina Stoilkovska, Igor Konnov, Josef Widder, Florian Zuleger.
International conference on tools and algorithms for the construction and analysis of systems, pages 357-374, 2019.
[pdf]
SL-COMP: Competition of solvers for separation logic
Mihaela Sighireanu, Jens Katelaan, Christoph Matheja, Thomas Noll, Florian Zuleger, .
25th international conference, TACAS 2019, pages 116-132, 2019.
[pdf]
Mihaela Sighireanu, Jens Katelaan, Christoph Matheja, Thomas Noll, Florian Zuleger,
25th international conference, TACAS 2019, pages 116-132, 2019.
[pdf]
Pebble-intervals automata and FO2 with two orders (extended version
Nadia Labai, Tomer Kotek, M.Magdalena Ortiz de la Fuente, Helmut Veith.
2019.
[pdf]
Nadia Labai, Tomer Kotek, M.Magdalena Ortiz de la Fuente, Helmut Veith.
2019.
[pdf]
Portfolio SAT and SMT solving of cardinality constraints in sensor network optimization
Gergely Kovasznai, Krisztian Gajdar, Laura Kovacs.
Proceedings of the 21st international symposium on symbolic and numeric algorithms for scientific computing (SYNASC), 2019, pages 85-91, 2019.
[doi]
Gergely Kovasznai, Krisztian Gajdar, Laura Kovacs.
Proceedings of the 21st international symposium on symbolic and numeric algorithms for scientific computing (SYNASC), 2019, pages 85-91, 2019.
[doi]
Model-based diagnosis with multiple observations
Alexey Ignatiev, António Morgado, João Marques-Silva, Georg Weissenbacher.
International joint conference on artificial intelligence, pages 1108-1115, 2019.
[doi]
Alexey Ignatiev, António Morgado, João Marques-Silva, Georg Weissenbacher.
International joint conference on artificial intelligence, pages 1108-1115, 2019.
[doi]
Extracting safe thread schedules from incomplete model checking results
Patrick Metzler, Neeraj Suri, Georg Weissenbacher.
Model checking software, pages 153-171, 2019.
[doi]
Patrick Metzler, Neeraj Suri, Georg Weissenbacher.
Model checking software, pages 153-171, 2019.
[doi]
Planning under LTL environment specifications
Benjamin Aminof, Giuseppe De Giacomo, Aniello Murano, Sasha Rubin.
29th international conference on automated planning and scheduling, pages 31-39, 2019.
[pdf]
Benjamin Aminof, Giuseppe De Giacomo, Aniello Murano, Sasha Rubin.
29th international conference on automated planning and scheduling, pages 31-39, 2019.
[pdf]
Probabilistic strategy logic
Benjamin Aminof, Marta Kwiatkowska, Bastien Maubert, Aniello Murano, Sasha Rubin.
28th international joint conference on artificial intelligence, pages 32-38, 2019.
[pdf]
Benjamin Aminof, Marta Kwiatkowska, Bastien Maubert, Aniello Murano, Sasha Rubin.
28th international joint conference on artificial intelligence, pages 32-38, 2019.
[pdf]
Verification of randomized consensus algorithms under round-rigid adversaries
Nathalie Bertrand, Igor Konnov, Marijana Lazić, Josef Widder.
30th international conference on concurrency theory, pages 33:1-33:15, 2019.
[pdf] [doi]
Nathalie Bertrand, Igor Konnov, Marijana Lazić, Josef Widder.
30th international conference on concurrency theory, pages 33:1-33:15, 2019.
[pdf] [doi]
Effective entailment checking for separation logic with inductive definitions
Jens Katelaan, Christoph Matheja, Florian Zuleger.
25th international conference, TACAS 2019, pages 319-336, 2019.
[pdf]
Jens Katelaan, Christoph Matheja, Florian Zuleger.
25th international conference, TACAS 2019, pages 319-336, 2019.
[pdf]
Parameterized model checking of rendezvous systems
Benjamin Aminof, Tomer Kotek, Sasha Rubin, Francesco Spegni, Helmut Veith.
Distributed Computing, volume 31, pages 187-222, 2018.
[pdf] [doi]
Benjamin Aminof, Tomer Kotek, Sasha Rubin, Francesco Spegni, Helmut Veith.
Distributed Computing, volume 31, pages 187-222, 2018.
[pdf] [doi]
Desingularization of first order linear difference systems with rational function coefficients
Moulay Barkatou, Maximilian Jaroschek.
Proceedings of the 2018 ACM international symposium on symbolic and algebraic computation (ISSAC), pages 39-46, 2018.
[pdf] [doi]
Moulay Barkatou, Maximilian Jaroschek.
Proceedings of the 2018 ACM international symposium on symbolic and algebraic computation (ISSAC), pages 39-46, 2018.
[pdf] [doi]
Efficient algorithms for asymptotic bounds on termination time in VASS
Tomas Brazdil, Krishnendu Chatterjee, Antonin Kucera, Peter Novotny, Dominik Velan, Florian Zuleger.
Proceedings of the 33rd annual ACM/IEEE symposium on logic in computer science, LICS 2018, oxford, UK, july 09-12, 2018, pages 185-194, 2018.
[pdf] [doi]
Tomas Brazdil, Krishnendu Chatterjee, Antonin Kucera, Peter Novotny, Dominik Velan, Florian Zuleger.
Proceedings of the 33rd annual ACM/IEEE symposium on logic in computer science, LICS 2018, oxford, UK, july 09-12, 2018, pages 185-194, 2018.
[pdf] [doi]
Efficient translation of sequent calculus proofs into natural deduction proofs
Gabriel Ebner, Matthias Schlaipfer.
PAAR 2018 practical aspects of automated reasoning, volume 2162, pages 17-33, 2018.
Gabriel Ebner, Matthias Schlaipfer.
PAAR 2018 practical aspects of automated reasoning, volume 2162, pages 17-33, 2018.
Incremental solving with vampire
Giles Reger, Martin Suda.
Proceedings of the 4th vampire workshop, volume 53, 2018.
[pdf] [doi]
Giles Reger, Martin Suda.
Proceedings of the 4th vampire workshop, volume 53, 2018.
[pdf] [doi]
Local proofs and AVATAR
Giles Reger, Martin Suda.
Proceedings of the 4th vampire workshop, volume 53, 2018.
[pdf] [doi]
Giles Reger, Martin Suda.
Proceedings of the 4th vampire workshop, volume 53, 2018.
[pdf] [doi]
Aligator.jl - a julia package for loop invariant generation
Andreas Humenberger, Maximilian Jaroschek, Laura Kovacs.
Proceedings of the 11th international conference on intelligent computer mathematics (CICM), pages 111-117, 2018.
[pdf] [doi]
Andreas Humenberger, Maximilian Jaroschek, Laura Kovacs.
Proceedings of the 11th international conference on intelligent computer mathematics (CICM), pages 111-117, 2018.
[pdf] [doi]
A FOOLish encoding of the next state relations of imperative programs.
Evgenii Kotelnikov, Laura Kovacs, Andrei Voronkov.
Proceedings of the 9th international joint conference on automated reasoning (IJCAR) 2018, pages 405-421, 2018.
[doi]
Evgenii Kotelnikov, Laura Kovacs, Andrei Voronkov.
Proceedings of the 9th international joint conference on automated reasoning (IJCAR) 2018, pages 405-421, 2018.
[doi]
Local soundness for QBF calculi
Martin Suda, Bernhard Gleiss.
Proceedings of the 21st international conference on theory and applications of satisfiability testing (SAT), pages 217-234, 2018.
[doi]
Martin Suda, Bernhard Gleiss.
Proceedings of the 21st international conference on theory and applications of satisfiability testing (SAT), pages 217-234, 2018.
[doi]
Automated clustering and program repair for introductory programming assignments
Ivan Radicek, Sumit Gulwani, Florian Zuleger.
Proceedings of the 39th ACM SIGPLAN conference on programming language design and implementation, PLDI 2018, philadelphia, PA, USA, june 18-22, 2018, pages 465-480, 2018.
[pdf] [doi]
Ivan Radicek, Sumit Gulwani, Florian Zuleger.
Proceedings of the 39th ACM SIGPLAN conference on programming language design and implementation, PLDI 2018, philadelphia, PA, USA, june 18-22, 2018, pages 465-480, 2018.
[pdf] [doi]
Extended resolution simulates DRAT
Benjamin Kiesl, Adrian Rebola Pardo, Marijn Heule.
Proceedings of the 9th international joint conference on automated reasoning (IJCAR) 2018, pages 516-531, 2018.
[doi]
Benjamin Kiesl, Adrian Rebola Pardo, Marijn Heule.
Proceedings of the 9th international joint conference on automated reasoning (IJCAR) 2018, pages 516-531, 2018.
[doi]
Inductive termination proofs with transition invariants and their relationship to the size-change abstraction
Florian Zuleger.
Static analysis - 25th international symposium, SAS 2018, freiburg, germany, august 29-31, 2018, proceedings, pages 423-444, 2018.
[pdf] [doi]
Florian Zuleger.
Static analysis - 25th international symposium, SAS 2018, freiburg, germany, august 29-31, 2018, proceedings, pages 423-444, 2018.
[pdf] [doi]
Reachability in parameterized systems: All flavors of threshold automata
Jure Kukovec, Igor Konnov, Josef Widder.
29th international conference on concurrency theory (CONCUR 2018), pages 19:1-19:17, 2018.
[pdf] [doi]
Jure Kukovec, Igor Konnov, Josef Widder.
29th international conference on concurrency theory (CONCUR 2018), pages 19:1-19:17, 2018.
[pdf] [doi]
Rely-guarantee reasoning for automated bound analysis of lock-free algorithms
Thomas Pani, Georg Weissenbacher, Florian Zuleger.
Formal methods in computer-aided design, pages 1-9, 2018.
[pdf] [doi]
Thomas Pani, Georg Weissenbacher, Florian Zuleger.
Formal methods in computer-aided design, pages 1-9, 2018.
[pdf] [doi]
Synthesis under assumptions
Benjamin Aminof, Giuseppe De Giacomo, Aniello Murano, Sasha Rubin.
Principles of knowledge representation and reasoning: Proceedings of the sixteenth international conference, KR 2018, tempe, arizona, 30 october - 2 november 2018, pages 615-616, 2018.
[pdf]
Benjamin Aminof, Giuseppe De Giacomo, Aniello Murano, Sasha Rubin.
Principles of knowledge representation and reasoning: Proceedings of the sixteenth international conference, KR 2018, tempe, arizona, 30 october - 2 november 2018, pages 615-616, 2018.
[pdf]
Automated reasoning for systems engineering
Laura Kovacs.
Foundations of information and knowledge systems (FOIKS) 2018, pages 1, 2018.
Laura Kovacs.
Foundations of information and knowledge systems (FOIKS) 2018, pages 1, 2018.
Communication-closed layers as paradigm for distributed systems: A manifesto
Cezara Dragoi, Marijana Lazić, Josef Widder.
Sinteza 2018 international scientific conference on information technology and data related research, pages 131-138, 2018.
[pdf] [doi]
Cezara Dragoi, Marijana Lazić, Josef Widder.
Sinteza 2018 international scientific conference on information technology and data related research, pages 131-138, 2018.
[pdf] [doi]
Unification with abstraction and theory instantiation in saturation-based reasoning
Giles Reger, Martin Suda, Andrei Voronkov.
Proceedings of the 24th international conference on tools and algorithms for the construction and analysis of systems (TACAS), pages 3-22, 2018.
[pdf]
Giles Reger, Martin Suda, Andrei Voronkov.
Proceedings of the 24th international conference on tools and algorithms for the construction and analysis of systems (TACAS), pages 3-22, 2018.
[pdf]
Monadic refinements for relational cost analysis
Ivan Radicek, Gilles Barthe, Marco Gaboardi, Deepak Garg, Florian Zuleger.
Proceedings of the ACM on programming languages, volume New York, NY, USA, pages 1-32, 2018.
[pdf] [doi]
Ivan Radicek, Gilles Barthe, Marco Gaboardi, Deepak Garg, Florian Zuleger.
Proceedings of the ACM on programming languages, volume New York, NY, USA, pages 1-32, 2018.
[pdf] [doi]
Parameterized model checking of synchronous distributed algorithms by abstraction
Benjamin Aminof, Ilina Stoilkovska, Sasha Rubin, Josef Widder, Florian Zuleger.
Verification, model checking, and abstract interpretation - 19th international conference, VMCAI 2018, los angeles, CA, USA, january 7-9, 2018, proceedings, pages 1-24, 2018.
[pdf] [doi]
Benjamin Aminof, Ilina Stoilkovska, Sasha Rubin, Josef Widder, Florian Zuleger.
Verification, model checking, and abstract interpretation - 19th international conference, VMCAI 2018, los angeles, CA, USA, january 7-9, 2018, proceedings, pages 1-24, 2018.
[pdf] [doi]
From shapes to amortized complexity
Tomas Fiedor, Lukas Holik, Adam Rogalewicz, Moritz Sinn, Tomás Vojnar, Florian Zuleger.
Verification, model checking, and abstract interpretation - 19th international conference, VMCAI 2018, los angeles, CA, USA, january 7-9, 2018, proceedings, pages 205-225, 2018.
[pdf] [doi]
Tomas Fiedor, Lukas Holik, Adam Rogalewicz, Moritz Sinn, Tomás Vojnar, Florian Zuleger.
Verification, model checking, and abstract interpretation - 19th international conference, VMCAI 2018, los angeles, CA, USA, january 7-9, 2018, proceedings, pages 205-225, 2018.
[pdf] [doi]
Using loop bound analysis for invariant generation
Pavel Čadek, Clemens Danninger, Moritz Sinn, Florian Zuleger.
Formal methods in computer-aided design, pages 1-9, 2018.
[pdf] [doi]
Pavel Čadek, Clemens Danninger, Moritz Sinn, Florian Zuleger.
Formal methods in computer-aided design, pages 1-9, 2018.
[pdf] [doi]
Invariant generation for multi-path loops with polynomial assignments
Andreas Humenberger, Maximilian Jaroschek, Laura Kovacs.
Verification, model checking, and abstract interpretation - 19th international conference, pages 226-246, 2018.
[pdf] [doi]
Andreas Humenberger, Maximilian Jaroschek, Laura Kovacs.
Verification, model checking, and abstract interpretation - 19th international conference, pages 226-246, 2018.
[pdf] [doi]
Randomized testing of distributed systems with probabilistic guarantees
Burcu Kulahcioglu Ozkan, Rupak Majumdar, Filip Niksic, Mitra Tabaei Befrouei, Georg Weissenbacher.
Proceedings of the ACM on Programming Languages, volume 2, 2018.
[pdf] [doi]
Burcu Kulahcioglu Ozkan, Rupak Majumdar, Filip Niksic, Mitra Tabaei Befrouei, Georg Weissenbacher.
Proceedings of the ACM on Programming Languages, volume 2, 2018.
[pdf] [doi]
Reinterpreting dependency schemes: Soundness meets incompleteness in DQBF
Olaf Beyersdorff, Joshua Blinkhorn, Leroy Chew, Renate Schmidt, Martin Suda.
Journal of Automated Reasoning, volume J Autom Reasoning, pages 1-27, 2018.
[pdf] [doi]
Olaf Beyersdorff, Joshua Blinkhorn, Leroy Chew, Renate Schmidt, Martin Suda.
Journal of Automated Reasoning, volume J Autom Reasoning, pages 1-27, 2018.
[pdf] [doi]
CTL\* with graded path modalities
Benjamin Aminof, Aniello Murano, Sasha Rubin.
Information and Computation, volume 262, pages 1-21, 2018.
[pdf] [doi]
Benjamin Aminof, Aniello Murano, Sasha Rubin.
Information and Computation, volume 262, pages 1-21, 2018.
[pdf] [doi]
Parameterized model checking of synchronous distributed algorithms by abstraction
Benjamin Aminof, Sasha Rubin, Ilina Stoilkovska, Josef Widder, Florian Zuleger.
VMCAI, pages 1-24, 2018.
[pdf] [doi]
Benjamin Aminof, Sasha Rubin, Ilina Stoilkovska, Josef Widder, Florian Zuleger.
VMCAI, pages 1-24, 2018.
[pdf] [doi]
Graded modalities in strategy logic
Benjamin Aminof, Vadim Malvone, Aniello Murano, Sasha Rubin.
Information and Computation, volume 261, pages 634-649, 2018.
[pdf] [doi]
Benjamin Aminof, Vadim Malvone, Aniello Murano, Sasha Rubin.
Information and Computation, volume 261, pages 634-649, 2018.
[pdf] [doi]
Loop analysis by quantification over iterations
Bernhard Gleiss, Laura Kovacs, Simon Robillard.
Proceedings of the 22nd international conference on logic for programming, artificial intelligence and reasoning (LPAR), pages 381-399, 2018.
[pdf] [doi]
Bernhard Gleiss, Laura Kovacs, Simon Robillard.
Proceedings of the 22nd international conference on logic for programming, artificial intelligence and reasoning (LPAR), pages 381-399, 2018.
[pdf] [doi]
Towards smarter MACE-style model finders
Mikolás Janota, Martin Suda.
LPAR-22. 22nd international conference on logic for programming, artificial intelligence and reasoning, awassa, ethiopia, 16-21 november 2018., pages 454-470, 2018.
[pdf] [doi]
Mikolás Janota, Martin Suda.
LPAR-22. 22nd international conference on logic for programming, artificial intelligence and reasoning, awassa, ethiopia, 16-21 november 2018., pages 454-470, 2018.
[pdf] [doi]
A theory of satisfiability-preserving proofs in SAT solving
Adrian Rebola Pardo, Martin Suda.
International conference on logic for programming, artificial intelligence and reasoning, pages 583-603, 2018.
[pdf] [doi]
Adrian Rebola Pardo, Martin Suda.
International conference on logic for programming, artificial intelligence and reasoning, pages 583-603, 2018.
[pdf] [doi]
A separation logic with data: Small models and automation
Jens Katelaan, Dejan Jovanovic, Georg Weissenbacher.
Automated reasoning, pages 455-471, 2018.
[pdf] [doi]
Jens Katelaan, Dejan Jovanovic, Georg Weissenbacher.
Automated reasoning, pages 455-471, 2018.
[pdf] [doi]
Global subsumption revisited (briefly)
Giles Reger, Martin Suda.
Vampire\@IJCAR 2016. Proceedings of the 3rd vampire workshop, coimbra, portugal, july 2, 2016., volume 44, pages 61-73, 2017.
[pdf]
Giles Reger, Martin Suda.
Vampire\@IJCAR 2016. Proceedings of the 3rd vampire workshop, coimbra, portugal, july 2, 2016., volume 44, pages 61-73, 2017.
[pdf]
Measuring progress to predict success: Can a good proof strategy be evolved?
Giles Reger, Martin Suda.
2017.
Giles Reger, Martin Suda.
2017.
Instantiation and pretending to be an SMT solver with vampire
Giles Reger, Martin Suda, Andrei Voronkov.
2017.
Giles Reger, Martin Suda, Andrei Voronkov.
2017.
Polynomial invariant generation for multi-path loops
Andreas Humenberger, Maximilian Jaroschek, Laura Kovacs.
2017.
Andreas Humenberger, Maximilian Jaroschek, Laura Kovacs.
2017.
Model-based, mutation-driven test case generation via heuristic-guided branching search
Andreas Fellner, Willibald Krenn, Rupert Schlick, Thorsten Tarrach, Georg Weissenbacher.
Proceedings of the 15th ACM-IEEE international conference on formal methods and models for system design, MEMOCODE 2017, vienna, austria, september 29 - october 02, 2017, pages 56-66, 2017.
[doi]
Andreas Fellner, Willibald Krenn, Rupert Schlick, Thorsten Tarrach, Georg Weissenbacher.
Proceedings of the 15th ACM-IEEE international conference on formal methods and models for system design, MEMOCODE 2017, vienna, austria, september 29 - october 02, 2017, pages 56-66, 2017.
[doi]
Optimizing big-data queries using program synthesis
Matthias Schlaipfer, Kaushik Rajan, Akash Lal, Malavika Samak.
Symposium on operating systems principles, pages 631-646, 2017.
[doi]
Matthias Schlaipfer, Kaushik Rajan, Akash Lal, Malavika Samak.
Symposium on operating systems principles, pages 631-646, 2017.
[doi]
First-order interpolation and interpolating proof systems
Laura Kovacs, Andrei Voronkov.
LPAR-21. 21st international conference on logic for programming, artificial intelligence and reasoning, pages 49-64, 2017.
Laura Kovacs, Andrei Voronkov.
LPAR-21. 21st international conference on logic for programming, artificial intelligence and reasoning, pages 49-64, 2017.
Fuzzing and verifying RAT refutations with deletion information
Walter Forkel, Tobias Philipp, Adrian Rebola Pardo, Elias Werner.
Florida artificial intelligence research society conference, pages 190-193, 2017.
Walter Forkel, Tobias Philipp, Adrian Rebola Pardo, Elias Werner.
Florida artificial intelligence research society conference, pages 190-193, 2017.
Preface of the special issue in memoriam helmut veith
Georg Gottlob, Thomas A. Henzinger, Georg Weissenbacher.
Formal Methods in System Design, volume 51, pages 267-269, 2017.
[doi]
Georg Gottlob, Thomas A. Henzinger, Georg Weissenbacher.
Formal Methods in System Design, volume 51, pages 267-269, 2017.
[doi]
Empirical software metrics for benchmarking of verification tools
Yulia Demyanova, Thomas Pani, Helmut Veith, Florian Zuleger.
Formal Methods in System Design, volume 50, pages 289-316, 2017.
[doi]
Yulia Demyanova, Thomas Pani, Helmut Veith, Florian Zuleger.
Formal Methods in System Design, volume 50, pages 289-316, 2017.
[doi]
Complexity and resource bound analysis of imperative programs using difference constraints
Moritz Sinn, Helmut Veith, Florian Zuleger.
Journal of Automated Reasoning, volume 59, pages 3-45, 2017.
Moritz Sinn, Helmut Veith, Florian Zuleger.
Journal of Automated Reasoning, volume 59, pages 3-45, 2017.
On the completeness of bounded model checking for threshold-based distributed algorithms: reachability
Igor Konnov, Helmut Veith, Josef Widder.
Information and Computation, volume 252, pages 95-109, 2017.
[pdf] [doi]
Igor Konnov, Helmut Veith, Josef Widder.
Information and Computation, volume 252, pages 95-109, 2017.
[pdf] [doi]
Para\^2: Parameterized path reduction, acceleration, and SMT for reachability in threshold-guarded distributed algorithms
Igor Konnov, Marijana Lazić, Helmut Veith, Josef Widder.
Formal Methods in System Design, volume 51, pages 270-307, 2017.
[doi]
Igor Konnov, Marijana Lazić, Helmut Veith, Josef Widder.
Formal Methods in System Design, volume 51, pages 270-307, 2017.
[doi]
Towards a semantics of unsatisfiability proofs with inprocessing
Tobias Philipp, Adrian Rebola Pardo.
Logic programming and automated reasoning (LPAR), pages 65-84, 2017.
[pdf]
Tobias Philipp, Adrian Rebola Pardo.
Logic programming and automated reasoning (LPAR), pages 65-84, 2017.
[pdf]
Replacing conjectures by positive knowledge: Inferring proven precise worst-case execution time bounds using symbolic execution
Jens Knoop, Laura Kovacs, Jakob Zwirchmayr.
Journal of Symbolic Computation, volume 80, pages 101-124, 2017.
[doi]
Jens Knoop, Laura Kovacs, Jakob Zwirchmayr.
Journal of Symbolic Computation, volume 80, pages 101-124, 2017.
[doi]
Formal solutions of completely integrable pfaffian systems with normal crossings
Maximilian Jaroschek, Moulay Barkatou, Suzy Maddah.
Journal of Symbolic Computation, volume 81, pages 41-68, 2017.
Maximilian Jaroschek, Moulay Barkatou, Suzy Maddah.
Journal of Symbolic Computation, volume 81, pages 41-68, 2017.
First-cycle games
Benjamin Aminof, Sasha Rubin.
Information and Computation, volume 254, pages 195-216, 2017.
Benjamin Aminof, Sasha Rubin.
Information and Computation, volume 254, pages 195-216, 2017.
Synthesis of distributed algorithms with parameterized threshold guards
Marijana Lazić, Igor Konnov, Josef Widder, Roderick Bloem.
OPODIS, pages 32:1-32:20, 2017.
[pdf] [doi]
Marijana Lazić, Igor Konnov, Josef Widder, Roderick Bloem.
OPODIS, pages 32:1-32:20, 2017.
[pdf] [doi]
A supervisory control algorithm based on property-directed reachability
Koen Claessen, Jonatan Kilhamn, Laura Kovacs, Bengt Lennartson.
13th international haifa verification conference (HVC), pages 115-130, 2017.
[doi]
Koen Claessen, Jonatan Kilhamn, Laura Kovacs, Bengt Lennartson.
13th international haifa verification conference (HVC), pages 115-130, 2017.
[doi]
Logic-based merging in fragments of classical logic with inputs from social choice theory
Adrian Haret.
Proceedings of the 5th international conference on algorithmic decision theory (ADT 2017), pages 374-378, 2017.
[doi]
Adrian Haret.
Proceedings of the 5th international conference on algorithmic decision theory (ADT 2017), pages 374-378, 2017.
[doi]
Automated invention of strategies and term orderings for vampire
Jan Jakubuv, Martin Suda, Josef Urban.
GCAI 2017. 3rd global conference on artificial intelligence, pages 121-133, 2017.
[pdf]
Jan Jakubuv, Martin Suda, Josef Urban.
GCAI 2017. 3rd global conference on artificial intelligence, pages 121-133, 2017.
[pdf]
Deviation in belief change on fragments of propositional logic
Adrian Haret, Stefan Woltran.
Proceedings of the 6th workshop on dynamics of knowledge and belief (DKB-2017) and the 5th workshop KI & kognition (KIK-2017), 2017.
Adrian Haret, Stefan Woltran.
Proceedings of the 6th workshop on dynamics of knowledge and belief (DKB-2017) and the 5th workshop KI & kognition (KIK-2017), 2017.
Automata and program analysis
Laure Daviaud, Thomas Colcombet, Florian Zuleger.
Fundamentals of computation theory - 21st international symposium, FCT 2017, pages 3-10, 2017.
Laure Daviaud, Thomas Colcombet, Florian Zuleger.
Fundamentals of computation theory - 21st international symposium, FCT 2017, pages 3-10, 2017.
Lpopt: A rule optimization tool for answer set programming
Michael Morak, Manuel Bichler, Stefan Woltran.
Proceedings of the 26th InternationalSymposium on logic-based program synthesis and transformation (LOPSTR 2016), pages 114-130, 2017.
[doi]
Michael Morak, Manuel Bichler, Stefan Woltran.
Proceedings of the 26th InternationalSymposium on logic-based program synthesis and transformation (LOPSTR 2016), pages 114-130, 2017.
[doi]
First-order interpolation and grey areas of proofs
Laura Kovacs.
Proceedings of the 26th EACSL annual conference on computer science logic (CSL), volume 82, pages 3:1, 2017.
[doi]
Laura Kovacs.
Proceedings of the 26th EACSL annual conference on computer science logic (CSL), volume 82, pages 3:1, 2017.
[doi]
Splitting proofs for interpolation
Bernhard Gleiss, Laura Kovacs, Martin Suda.
Automated deduction - CADE 26 - 26th international conference on automated deduction, gothenburg, sweden, august 6-11, 2017, proceedings, pages 291-309, 2017.
[pdf] [doi]
Bernhard Gleiss, Laura Kovacs, Martin Suda.
Automated deduction - CADE 26 - 26th international conference on automated deduction, gothenburg, sweden, august 6-11, 2017, proceedings, pages 291-309, 2017.
[pdf] [doi]
A unifying principle for clause elimination in first-order logic
Benjamin Kiesl, Martin Suda.
Automated deduction - CADE 26 - 26th international conference on automated deduction, gothenburg, sweden, august 6-11, 2017, proceedings, pages 274-290, 2017.
[pdf] [doi]
Benjamin Kiesl, Martin Suda.
Automated deduction - CADE 26 - 26th international conference on automated deduction, gothenburg, sweden, august 6-11, 2017, proceedings, pages 274-290, 2017.
[pdf] [doi]
Checkable proofs for first-order theorem proving
Giles Reger, Martin Suda.
ARCADE 2017. 1st international workshop on automated reasoning: Challenges, applications, directions, exemplary achievements, pages 55-63, 2017.
[pdf]
Giles Reger, Martin Suda.
ARCADE 2017. 1st international workshop on automated reasoning: Challenges, applications, directions, exemplary achievements, pages 55-63, 2017.
[pdf]
Automated generation of non-linear loop invariants utilizing hypergeometric sequences
Andreas Humenberger, Maximilian Jaroschek, Laura Kovacs.
ISSAC '17 proceedings of the 2017 ACM on international symposium on symbolic and algebraic computation, pages 221-228, 2017.
[pdf] [doi]
Andreas Humenberger, Maximilian Jaroschek, Laura Kovacs.
ISSAC '17 proceedings of the 2017 ACM on international symposium on symbolic and algebraic computation, pages 221-228, 2017.
[pdf] [doi]
Testing a saturation-based theorem prover: Experiences and challenges
Giles Reger, Martin Suda, Andrei Voronkov.
Tests and proofs - 11th international conference, TAP 2017, held as part of STAF 2017, marburg, germany, july 19-20, 2017, proceedings, pages 152-161, 2017.
[pdf] [doi]
Giles Reger, Martin Suda, Andrei Voronkov.
Tests and proofs - 11th international conference, TAP 2017, held as part of STAF 2017, marburg, germany, july 19-20, 2017, proceedings, pages 152-161, 2017.
[pdf] [doi]
Constructive satisfiability procedure for ALCP(z) (preliminary report)
Nadia Labai, Martin Homola, M.Magdalena Ortiz de la Fuente.
Proceedings of the 30th international workshop on description logics, pages 1-13, 2017.
[pdf]
Nadia Labai, Martin Homola, M.Magdalena Ortiz de la Fuente.
Proceedings of the 30th international workshop on description logics, pages 1-13, 2017.
[pdf]
Systematic predicate abstraction using variable roles
Yulia Demyanova, Philipp Rümmer, Florian Zuleger.
NASA formal methods - 9th international symposium, NFM 2017, pages 265-281, 2017.
Yulia Demyanova, Philipp Rümmer, Florian Zuleger.
NASA formal methods - 9th international symposium, NFM 2017, pages 265-281, 2017.
Blocked clauses in first-order logic
Benjamin Kiesl, Martin Suda, Martina Seidl, Hans Tompits, Armin Biere.
LPAR-21. 21st international conference on logic for programming, artificial intelligence and reasoning, pages 31-48, 2017.
[pdf]
Benjamin Kiesl, Martin Suda, Martina Seidl, Hans Tompits, Armin Biere.
LPAR-21. 21st international conference on logic for programming, artificial intelligence and reasoning, pages 31-48, 2017.
[pdf]
Set of support for theory reasoning
Giles Reger, Martin Suda.
IWIL\@LPAR 2017 workshop and LPAR-21 short presentations, maun, botswana, may 7-12, 2017, pages 124-134, 2017.
[pdf]
Giles Reger, Martin Suda.
IWIL\@LPAR 2017 workshop and LPAR-21 short presentations, maun, botswana, may 7-12, 2017, pages 124-134, 2017.
[pdf]
Unified reasoning about robustness properties of symbolic-heap separation logic
Jens Katelaan, Christina Jansen, Florian Zuleger, Christoph Matheja, Thomas Noll.
Programming languages and systems - 26th european symposium on programming, pages 611-638, 2017.
[doi]
Jens Katelaan, Christina Jansen, Florian Zuleger, Christoph Matheja, Thomas Noll.
Programming languages and systems - 26th european symposium on programming, pages 611-638, 2017.
[doi]
On the automated verification of web applications with embedded SQL
Itzhaky Shachar, Tomer Kotek, Noam Rinetzky, Mooly Sagiv, Orr Tamir, Helmut Veith, Florian Zuleger.
20th international conference on database theory, ICDT 2017, pages 1-18, 2017.
Itzhaky Shachar, Tomer Kotek, Noam Rinetzky, Mooly Sagiv, Orr Tamir, Helmut Veith, Florian Zuleger.
20th international conference on database theory, ICDT 2017, pages 1-18, 2017.
A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms
Igor Konnov, Marijana Lazić, Helmut Veith, Josef Widder.
POPL, pages 719-734, 2017.
[pdf] [doi]
Igor Konnov, Marijana Lazić, Helmut Veith, Josef Widder.
POPL, pages 719-734, 2017.
[pdf] [doi]
Coming to terms with quantified reasoning
Laura Kovacs, Simon Robillard, Andrei Voronkov.
Proceedings of the 44th ACM SIGPLAN symposium on principles of programming languages (POPL), pages 260-270, 2017.
[pdf] [doi]
Laura Kovacs, Simon Robillard, Andrei Voronkov.
Proceedings of the 44th ACM SIGPLAN symposium on principles of programming languages (POPL), pages 260-270, 2017.
[pdf] [doi]
Dynamic reductions for model checking concurrent software
Henning Günther, Alfons Laarman, Ana Sokolova, Georg Weissenbacher.
Verification, model checking, and abstract interpretation, pages 246-265, 2017.
[doi]
Henning Günther, Alfons Laarman, Ana Sokolova, Georg Weissenbacher.
Verification, model checking, and abstract interpretation, pages 246-265, 2017.
[doi]
Theory-specific reasoning about loops with arrays using vampire
Yuting Chen, Laura Kovacs, Simon Robillard.
Proceedings of the third vampire workshop, 2017.
Yuting Chen, Laura Kovacs, Simon Robillard.
Proceedings of the third vampire workshop, 2017.
AVATAR modulo theories
Giles Reger, Nikolaj Bjorner, Martin Suda, Andrei Voronkov.
GCAI 2016. 2nd global conference on artificial intelligence, pages 39-52, 2016.
[pdf]
Giles Reger, Nikolaj Bjorner, Martin Suda, Andrei Voronkov.
GCAI 2016. 2nd global conference on artificial intelligence, pages 39-52, 2016.
[pdf]
New techniques in clausal form generation
Giles Reger, Martin Suda, Andrei Voronkov.
GCAI 2016. 2nd global conference on artificial intelligence, pages 11-23, 2016.
[pdf]
Giles Reger, Martin Suda, Andrei Voronkov.
GCAI 2016. 2nd global conference on artificial intelligence, pages 11-23, 2016.
[pdf]
Lpopt: A rule optimization tool for answer set programming
Manuel Bichler, Michael Morak, Stefan Woltran.
Pre-proceedings of the 26th international symposium on logic-based program synthesis and transformation (LOPSTR 2016), 2016.
Manuel Bichler, Michael Morak, Stefan Woltran.
Pre-proceedings of the 26th international symposium on logic-based program synthesis and transformation (LOPSTR 2016), 2016.
Beyond IC postulates: Classification criteria for merging operators
Adrian Haret, Andreas Pfandler, Stefan Woltran.
ECAI 2016 - 22nd european conference on artificial intelligence, pages 372-380, 2016.
[doi]
Adrian Haret, Andreas Pfandler, Stefan Woltran.
ECAI 2016 - 22nd european conference on artificial intelligence, pages 372-380, 2016.
[doi]
Monadic second order finite satisfiability and unbounded tree-width
Tomer Kotek, Helmut Veith, Florian Zuleger.
CSL, pages 1-20, 2016.
Tomer Kotek, Helmut Veith, Florian Zuleger.
CSL, pages 1-20, 2016.
Parameterized systems in BIP: Design and model checking
Igor Konnov, Tomer Kotek, Qiang Wang, Helmut Veith, Simon Bliudze, Joseph Sifakis.
CONCUR, pages 30:1-30:16, 2016.
[pdf] [doi]
Igor Konnov, Tomer Kotek, Qiang Wang, Helmut Veith, Simon Bliudze, Joseph Sifakis.
CONCUR, pages 30:1-30:16, 2016.
[pdf] [doi]
Extended graded modalities in strategy logic
Benjamin Aminof, Vadim Malvone, Aniello Murano, Sasha Rubin.
SR, pages 1-14, 2016.
Benjamin Aminof, Vadim Malvone, Aniello Murano, Sasha Rubin.
SR, pages 1-14, 2016.
Distributing knowledge into simple bases
Adrian Haret, Jean-Guy Mailly, Stefan Woltran.
Proceedings of the 25th international joint conference on artificial intelligence, pages 1109-1115, 2016.
[pdf]
Adrian Haret, Jean-Guy Mailly, Stefan Woltran.
Proceedings of the 25th international joint conference on artificial intelligence, pages 1109-1115, 2016.
[pdf]
Lifting QBF resolution calculi to DQBF
Olaf Beyersdorff, Leroy Chew, Renate Schmidt, Martin Suda.
Theory and applications of satisfiability testing - SAT 2016 - 19th international conference, bordeaux, france, july 5-8, 2016, proceedings, pages 490-499, 2016.
[pdf] [doi]
Olaf Beyersdorff, Leroy Chew, Renate Schmidt, Martin Suda.
Theory and applications of satisfiability testing - SAT 2016 - 19th international conference, bordeaux, france, july 5-8, 2016, proceedings, pages 490-499, 2016.
[pdf] [doi]
Finding finite models in multi-sorted first-order logic
Giles Reger, Martin Suda, Andrei Voronkov.
Theory and applications of satisfiability testing - SAT 2016 - 19th international conference, bordeaux, france, july 5-8, 2016, proceedings, pages 323-341, 2016.
[pdf] [doi]
Giles Reger, Martin Suda, Andrei Voronkov.
Theory and applications of satisfiability testing - SAT 2016 - 19th international conference, bordeaux, france, july 5-8, 2016, proceedings, pages 323-341, 2016.
[pdf] [doi]
Model checking parameterised multi-token systems via the composition method
Benjamin Aminof, Sasha Rubin.
IJCAR, pages 499-515, 2016.
Benjamin Aminof, Sasha Rubin.
IJCAR, pages 499-515, 2016.
Selecting the selection
Krystof Hoder, Giles Reger, Martin Suda, Andrei Voronkov.
Automated reasoning - 8th international joint conference, IJCAR 2016, coimbra, portugal, june 27 - july 2, 2016, proceedings, pages 313-329, 2016.
[pdf] [doi]
Krystof Hoder, Giles Reger, Martin Suda, Andrei Voronkov.
Automated reasoning - 8th international joint conference, IJCAR 2016, coimbra, portugal, june 27 - july 2, 2016, proceedings, pages 313-329, 2016.
[pdf] [doi]
Duality in STRIPS planning
Martin Suda.
8th workshop on heuristics and search for domain-independent planning (HSDIP), london, UK, june 13, 2016, proceedings, pages 21-27, 2016.
[pdf]
Martin Suda.
8th workshop on heuristics and search for domain-independent planning (HSDIP), london, UK, june 13, 2016, proceedings, pages 21-27, 2016.
[pdf]
Symbolic computation and automated reasoning for program analysis
Laura Kovacs.
Proceedings of the 12th international conference on integrated formal methods (iFM), volume 9681, pages 20-27, 2016.
[pdf] [doi]
Laura Kovacs.
Proceedings of the 12th international conference on integrated formal methods (iFM), volume 9681, pages 20-27, 2016.
[pdf] [doi]
Graded strategy logic: Reasoning about uniqueness of nash equilibria
Benjamin Aminof, Vadim Malvone, Aniello Murano, Sasha Rubin.
AAMAS, pages 698-706, 2016.
Benjamin Aminof, Vadim Malvone, Aniello Murano, Sasha Rubin.
AAMAS, pages 698-706, 2016.
Automatic verification of multi-agent systems in parameterised grid-environments
Benjamin Aminof, Aniello Murano, Sasha Rubin, Florian Zuleger.
AAMAS, pages 1190-1199, 2016.
Benjamin Aminof, Aniello Murano, Sasha Rubin, Florian Zuleger.
AAMAS, pages 1190-1199, 2016.
Prompt alternating-time epistemic logics
Benjamin Aminof, Aniello Murano, Sasha Rubin, Florian Zuleger.
KR, pages 258-267, 2016.
Benjamin Aminof, Aniello Murano, Sasha Rubin, Florian Zuleger.
KR, pages 258-267, 2016.
Merging of abstract argumentation frameworks
Jerome Delobelle, Adrian Haret, Sebastien Konieczny, Jean-Guy Mailly, Julien Rossit, Stefan Woltran.
Principles of knowledge representation and reasoning: Proceedings of the 15th international conference, pages 33-42, 2016.
[pdf]
Jerome Delobelle, Adrian Haret, Sebastien Konieczny, Jean-Guy Mailly, Julien Rossit, Stefan Woltran.
Principles of knowledge representation and reasoning: Proceedings of the 15th international conference, pages 33-42, 2016.
[pdf]
Distributing knowledge into simple bases
Adrian Haret, Jean-Guy Mailly, Stefan Woltran.
Proceedings of the 16th international workshop on non-monotonic reasoning, 2016.
[pdf]
Adrian Haret, Jean-Guy Mailly, Stefan Woltran.
Proceedings of the 16th international workshop on non-monotonic reasoning, 2016.
[pdf]
The vampire and the FOOL
Evgenii Kotelnikov, Laura Kovacs, Giles Reger, Andrei Voronkov.
Proceedings of the 5th ACM SIGPLAN conference on certified programs and proofs (CPP), pages 37-48, 2016.
[pdf] [doi]
Evgenii Kotelnikov, Laura Kovacs, Giles Reger, Andrei Voronkov.
Proceedings of the 5th ACM SIGPLAN conference on certified programs and proofs (CPP), pages 37-48, 2016.
[pdf] [doi]
What you always wanted to know about model checking of fault-tolerant distributed algorithms
Igor Konnov, Helmut Veith, Josef Widder.
Perspectives of system informatics: 10th international andrei ershov informatics conference, PSI 2015, pages 6-21, 2016.
[pdf] [doi]
Igor Konnov, Helmut Veith, Josef Widder.
Perspectives of system informatics: 10th international andrei ershov informatics conference, PSI 2015, pages 6-21, 2016.
[pdf] [doi]
A clausal normal form translation for FOOL
Evgenii Kotelnikov, Laura Kovacs, Martin Suda, Andrei Voronkov.
GCAI 2016. 2nd global conference on artificial intelligence, pages 53-71, 2016.
[pdf]
Evgenii Kotelnikov, Laura Kovacs, Martin Suda, Andrei Voronkov.
GCAI 2016. 2nd global conference on artificial intelligence, pages 53-71, 2016.
[pdf]
Error invariants for concurrent traces
Andreas Holzer, Daniel Schwartz-Narbonne, Mitra Tabaei Befrouei, Georg Weissenbacher, Thomas Wies.
Formal methods, pages 370-387, 2016.
[doi]
Andreas Holzer, Daniel Schwartz-Narbonne, Mitra Tabaei Befrouei, Georg Weissenbacher, Thomas Wies.
Formal methods, pages 370-387, 2016.
[doi]
DRAT proofs for XOR reasoning
Tobias Philipp, Adrian Rebola Pardo.
Logics in artificial intelligence, pages 415-429, 2016.
[doi]
Tobias Philipp, Adrian Rebola Pardo.
Logics in artificial intelligence, pages 415-429, 2016.
[doi]
Desingularization of first order linear difference systems with rational function coefficients
Moulay Barkatou, Maximilian Jaroschek.
2016.
Moulay Barkatou, Maximilian Jaroschek.
2016.
Desingularization of first order linear difference systems with rational function coefficients
Maximilian Jaroschek, Moulay Barkatou.
2016.
Maximilian Jaroschek, Moulay Barkatou.
2016.
Model checking of threshold-based fault-tolerant distributed algorithms
Marijana Lazić, Igor Konnov, Helmut Veith, Josef Widder.
2016.
Marijana Lazić, Igor Konnov, Helmut Veith, Josef Widder.
2016.
Parameterized verification of liveness of distributed algorithms
Igor Konnov, Marijana Lazić, Helmut Veith, Josef Widder.
2016.
Igor Konnov, Marijana Lazić, Helmut Veith, Josef Widder.
2016.
Abstraction and mining of traces to explain concurrency bugs
Mitra Tabaei Befrouei, Chao Wang, Georg Weissenbacher.
Formal Methods in System Design, volume 49, pages 1-32, 2016.
[doi]
Mitra Tabaei Befrouei, Chao Wang, Georg Weissenbacher.
Formal Methods in System Design, volume 49, pages 1-32, 2016.
[doi]
Labelled interpolation systems for hyper-resolution, clausal, and local proofs
Matthias Schlaipfer, Georg Weissenbacher.
Journal of Automated Reasoning, volume 57, pages 3-36, 2016.
[pdf] [doi]
Matthias Schlaipfer, Georg Weissenbacher.
Journal of Automated Reasoning, volume 57, pages 3-36, 2016.
[pdf] [doi]
Angry-HEX: An artificial player for angry birds based on declarative knowledge bases
Giovambattista Ianni, Francesco Calimeri, Stefano Germano, Andreas Humenberger, Christoph Redl, Daria Stepanova, Andrea Tucci, Anton Wimmer.
IEEE Transactions on Computational Intelligence and AI in Games, volume 8, pages 128-139, 2016.
[doi]
Giovambattista Ianni, Francesco Calimeri, Stefano Germano, Andreas Humenberger, Christoph Redl, Daria Stepanova, Andrea Tucci, Anton Wimmer.
IEEE Transactions on Computational Intelligence and AI in Games, volume 8, pages 128-139, 2016.
[doi]
Decidability of parameterized verification
Roderick Bloem, Swen Jacobs, Ayrat Khalimov, Igor Konnov, Sasha Rubin, Helmut Veith, Josef Widder.
ACM SIGACT News, volume 47, pages 53-64, 2016.
[pdf] [doi]
Roderick Bloem, Swen Jacobs, Ayrat Khalimov, Igor Konnov, Sasha Rubin, Helmut Veith, Josef Widder.
ACM SIGACT News, volume 47, pages 53-64, 2016.
[pdf] [doi]
The power of non-ground rules in answer set programming
Manuel Bichler, Michael Morak, Stefan Woltran.
Theory and Practice of Logic Programming, volume 16, pages 552-569, 2016.
[doi]
Manuel Bichler, Michael Morak, Stefan Woltran.
Theory and Practice of Logic Programming, volume 16, pages 552-569, 2016.
[doi]
Treewidth-preserving modeling in ASP
Manuel Bichler, Bernhard Bliem, Marius Moldovan, Michael Morak, Stefan Woltran.
2016.
Manuel Bichler, Bernhard Bliem, Marius Moldovan, Michael Morak, Stefan Woltran.
2016.
Perspectives on white-box testing: Coverage, concurrency, and concolic execution
Azadeh Farzan, Andreas Holzer, Helmut Veith.
ICST, pages 1-11, 2015.
[doi]
Azadeh Farzan, Andreas Holzer, Helmut Veith.
ICST, pages 1-11, 2015.
[doi]
SMT and POR beat counter abstraction: Parameterized model checking of threshold-based distributed algorithms
Igor Konnov, Helmut Veith, Josef Widder.
Computer aided verification, pages 85-102, 2015.
[doi]
Igor Konnov, Helmut Veith, Josef Widder.
Computer aided verification, pages 85-102, 2015.
[doi]
On the expressive power of communication primitives in parameterised systems
Benjamin Aminof, Sasha Rubin, Florian Zuleger.
LPAR, pages 313-328, 2015.
[doi]
Benjamin Aminof, Sasha Rubin, Florian Zuleger.
LPAR, pages 313-328, 2015.
[doi]
Boolean satisfiability solvers and their applications in model checking
Yakir Vizel, Georg Weissenbacher, Sharad Malik.
Proceedings of the IEEE, volume 103, pages 2021-2035, 2015.
[pdf] [doi]
Yakir Vizel, Georg Weissenbacher, Sharad Malik.
Proceedings of the IEEE, volume 103, pages 2021-2035, 2015.
[pdf] [doi]
Loop patterns in c programs
Thomas Pani, Helmut Veith, Florian Zuleger.
ECEASST, volume 72, 2015.
[pdf]
Thomas Pani, Helmut Veith, Florian Zuleger.
ECEASST, volume 72, 2015.
[pdf]
Under-approximating loops in c programs for fast counterexample detection
Matt Lewis, Daniel Kroening, Georg Weissenbacher.
Formal Methods in System Design, volume 47, pages 75-92, 2015.
[doi]
Matt Lewis, Daniel Kroening, Georg Weissenbacher.
Formal Methods in System Design, volume 47, pages 75-92, 2015.
[doi]
Efficient computation of generalized ising polynomials on graphs with fixed clique-width
Tomer Kotek, Johann A. Makowsky.
Topics in Theoretical Computer Science (TTCS), volume 9541, pages 135-146, 2015.
Tomer Kotek, Johann A. Makowsky.
Topics in Theoretical Computer Science (TTCS), volume 9541, pages 135-146, 2015.
Merging in the horn fragment
Adrian Haret, Stefan Rümmele, Stefan Woltran.
Proceedings of the twenty-fourth international joint conference on artificial intelligence - IJCAI 2015, pages 3041-3047, 2015.
Adrian Haret, Stefan Rümmele, Stefan Woltran.
Proceedings of the twenty-fourth international joint conference on artificial intelligence - IJCAI 2015, pages 3041-3047, 2015.
Closure properties and complexity of rational sets of regular languages
Andreas Holzer, Christian Schallhart, Michael Tautschnig, Helmut Veith.
Theoretical Computer Science, volume 605, pages 62-79, 2015.
[doi]
Andreas Holzer, Christian Schallhart, Michael Tautschnig, Helmut Veith.
Theoretical Computer Science, volume 605, pages 62-79, 2015.
[doi]
Bipartition polynomials, the ising model and domination in graphs
Markus Dod, Tomer Kotek, James Preen, Peter Tittmann.
Discussiones Mathematicae Graph Theory, volume 35, pages 335-353, 2015.
Markus Dod, Tomer Kotek, James Preen, Peter Tittmann.
Discussiones Mathematicae Graph Theory, volume 35, pages 335-353, 2015.
Time complexity of link reversal routing
Bernadette Charron-Bost, Matthias Függer, Jennifer Welch, Josef Widder.
ACM Transactions on Algorithms, volume 11, pages 1-39, 2015.
[pdf] [doi]
Bernadette Charron-Bost, Matthias Függer, Jennifer Welch, Josef Widder.
ACM Transactions on Algorithms, volume 11, pages 1-39, 2015.
[pdf] [doi]
Abstraction and mining of traces to explain concurrency bugs
Mitra Tabaei Befrouei.
Proceedings of the young researchers' conference "frontiers of formal methods", 2015.
[pdf]
Mitra Tabaei Befrouei.
Proceedings of the young researchers' conference "frontiers of formal methods", 2015.
[pdf]
Difference constraints: An adequate abstraction for complexity analysis of imperative programs
Moritz Sinn, Helmut Veith, Florian Zuleger.
FMCAD, pages 144-151, 2015.
Moritz Sinn, Helmut Veith, Florian Zuleger.
FMCAD, pages 144-151, 2015.
Logics of finite hankel rank
Nadia Labai, Johann A. Makowsky.
Fields of logic and computation II, volume 9300, pages 237-252, 2015.
[doi]
Nadia Labai, Johann A. Makowsky.
Fields of logic and computation II, volume 9300, pages 237-252, 2015.
[doi]
An extension-based approach to belief revision in abstract argumentation
Martin Diller, Adrian Haret, Thomas Linsbichler, Stefan Rümmele, Stefan Woltran.
Proceedings of the twenty-fourth international joint conference on artificial intelligence - IJCAI 2015, pages 2926-2932, 2015.
Martin Diller, Adrian Haret, Thomas Linsbichler, Stefan Rümmele, Stefan Woltran.
Proceedings of the twenty-fourth international joint conference on artificial intelligence - IJCAI 2015, pages 2926-2932, 2015.
Compilation for secure two-party computations
Martin Franz, Andreas Holzer, Stefan Katzenbeisser, Christian Schallhart, Helmut Veith.
Software engineering & management 2015, pages 143-145, 2015.
Martin Franz, Andreas Holzer, Stefan Katzenbeisser, Christian Schallhart, Helmut Veith.
Software engineering & management 2015, pages 143-145, 2015.
Empirical software metrics for benchmarking of verification tools
Yulia Demyanova, Thomas Pani, Helmut Veith, Florian Zuleger.
CAV, pages 561-579, 2015.
[doi]
Yulia Demyanova, Thomas Pani, Helmut Veith, Florian Zuleger.
CAV, pages 561-579, 2015.
[doi]
Decidability of parameterized verification
Roderick Bloem, Swen Jacobs, Ayrat Khalimov, Igor Konnov, Sasha Rubin, Helmut Veith, Josef Widder.
2015.
[doi]
Roderick Bloem, Swen Jacobs, Ayrat Khalimov, Igor Konnov, Sasha Rubin, Helmut Veith, Josef Widder.
2015.
[doi]
LTSmin: High-performance language-independent model checking
Stefan Blom, Tom Dijk, Kant Gijis, Alfons Laarman, Jeroen Meijer, Jaco Pol.
TACAS, pages 692-707, 2015.
[doi]
Stefan Blom, Tom Dijk, Kant Gijis, Alfons Laarman, Jeroen Meijer, Jaco Pol.
TACAS, pages 692-707, 2015.
[doi]
Asymptotically precise ranking functions for deterministic size-change systems
Florian Zuleger.
CSR, pages 426-442, 2015.
[doi]
Florian Zuleger.
CSR, pages 426-442, 2015.
[doi]
Liveness of parameterized timed networks
Benjamin Aminof, Sasha Rubin, Francesco Spegni, Florian Zuleger.
ICALP, volume 9135, pages 375-387, 2015.
[doi]
Benjamin Aminof, Sasha Rubin, Francesco Spegni, Florian Zuleger.
ICALP, volume 9135, pages 375-387, 2015.
[doi]
Extending ALCQIO with trees
Tomer Kotek, Mantas Simkus, Helmut Veith, Florian Zuleger.
LICS 2015, pages 511-522, 2015.
[pdf] [doi]
Tomer Kotek, Mantas Simkus, Helmut Veith, Florian Zuleger.
LICS 2015, pages 511-522, 2015.
[pdf] [doi]
Proving safety with trace automata and bounded model checking
Matt Lewis, Daniel Kroening, Georg Weissenbacher.
Formal methods, pages 325-341, 2015.
[doi]
Matt Lewis, Daniel Kroening, Georg Weissenbacher.
Formal methods, pages 325-341, 2015.
[doi]
Verification of asynchronous mobile-robots in partially-known environments
Benjamin Aminof, Aniello Murano, Sasha Rubin, Florian Zuleger.
PRIMA, pages 185-200, 2015.
[doi]
Benjamin Aminof, Aniello Murano, Sasha Rubin, Florian Zuleger.
PRIMA, pages 185-200, 2015.
[doi]
CBMC-GC: An ANSI c compiler for secure two-party computations
Martin Franz, Andreas Holzer, Stefan Katzenbeisser, Christian Schallhart, Helmut Veith.
Compiler construction, pages 244-249, 2014.
[doi]
Martin Franz, Andreas Holzer, Stefan Katzenbeisser, Christian Schallhart, Helmut Veith.
Compiler construction, pages 244-249, 2014.
[doi]
Solvability-based comparison of failure detectors
Srikanth Sastry, Josef Widder.
NCA, pages 269-276, 2014.
[doi]
Srikanth Sastry, Josef Widder.
NCA, pages 269-276, 2014.
[doi]
Parameterized model checking of rendezvous systems
Benjamin Aminof, Tomer Kotek, Sasha Rubin, Francesco Spegni, Helmut Veith.
CONCUR, pages 109-124, 2014.
[doi]
Benjamin Aminof, Tomer Kotek, Sasha Rubin, Francesco Spegni, Helmut Veith.
CONCUR, pages 109-124, 2014.
[doi]
Approaching verification and validation challenges in smart grids
Tobias Deutsch, Josef Widder.
Tagungsband ComForEn 2014, 2014.
[pdf]
Tobias Deutsch, Josef Widder.
Tagungsband ComForEn 2014, 2014.
[pdf]
A logic-based framework for verifying consensus algorithms
Cezara Dragoi, Thomas A. Henzinger, Helmut Veith, Josef Widder, Damien Zufferey.
VMCAI, pages 161-181, 2014.
[doi]
Cezara Dragoi, Thomas A. Henzinger, Helmut Veith, Josef Widder, Damien Zufferey.
VMCAI, pages 161-181, 2014.
[doi]
Reduction of resolution refutations and interpolants via subsumption
Roderick Bloem, Sharad Malik, Matthias Schlaipfer, Georg Weissenbacher.
Haifa verification conference (HVC), pages 188-203, 2014.
[doi]
Roderick Bloem, Sharad Malik, Matthias Schlaipfer, Georg Weissenbacher.
Haifa verification conference (HVC), pages 188-203, 2014.
[doi]
Merging in the horn fragment
Adrian Haret.
2014.
Adrian Haret.
2014.
Partial-order reduction for multi-core LTL model checking
Alfons Laarman, Anton Wijs.
Haifa verification conference (HVC), pages 267-283, 2014.
[doi]
Alfons Laarman, Anton Wijs.
Haifa verification conference (HVC), pages 267-283, 2014.
[doi]
Parameterized model checking of token-passing systems
Benjamin Aminof, Swen Jacobs, Ayrat Khalimov, Sasha Rubin.
VMCAI, pages 262-281, 2014.
[doi]
Benjamin Aminof, Swen Jacobs, Ayrat Khalimov, Sasha Rubin.
VMCAI, pages 262-281, 2014.
[doi]
Concolic testing of concurrent programs
Azadeh Farzan, Andreas Holzer, Niloofar Razavi, Helmut Veith.
Software engineering 2014, pages 101-102, 2014.
[pdf]
Azadeh Farzan, Andreas Holzer, Niloofar Razavi, Helmut Veith.
Software engineering 2014, pages 101-102, 2014.
[pdf]
Reusing information in multi-goal reachability analyses
Dirk Beyer, Andreas Holzer, Michael Tautschnig, Helmut Veith.
Software engineering 2014, pages 97-98, 2014.
Dirk Beyer, Andreas Holzer, Michael Tautschnig, Helmut Veith.
Software engineering 2014, pages 97-98, 2014.
On the complexity of symbolic verification and decision problems in bit-vector logic
Andreas Fröhlich, Gergely Kovasznai, Armin Biere, Helmut Veith.
POS, 2014.
[pdf]
Andreas Fröhlich, Gergely Kovasznai, Armin Biere, Helmut Veith.
POS, 2014.
[pdf]
Towards a description logic for program analysis: Extending ALCQIO with reachability
Tomer Kotek, Mantas Simkus, Helmut Veith, Florian Zuleger.
International workshop on description logics, 2014.
[pdf]
Tomer Kotek, Mantas Simkus, Helmut Veith, Florian Zuleger.
International workshop on description logics, 2014.
[pdf]
Feedback generation for performance problems in introductory programming assignments
Sumit Gulwani, Ivan Radicek, Florian Zuleger.
FSE, pages 41-51, 2014.
[doi]
Sumit Gulwani, Ivan Radicek, Florian Zuleger.
FSE, pages 41-51, 2014.
[doi]
Complexity results and algorithms for argumentation - dung's frameworks and beyond
Johannes Peter Wallner.
2014.
[pdf]
Johannes Peter Wallner.
2014.
[pdf]
Shape and content: Incorporating domain knowledge into shape analysis
Diego Calvanese, Tomer Kotek, Mantas Simkus, Helmut Veith, Florian Zuleger.
International workshop on description logics, 2014.
[pdf]
Diego Calvanese, Tomer Kotek, Mantas Simkus, Helmut Veith, Florian Zuleger.
International workshop on description logics, 2014.
[pdf]
A simple and scalable static analysis for bound analysis and amortized complexity analysis
Moritz Sinn, Florian Zuleger, Helmut Veith.
CAV, pages 745-761, 2014.
[doi]
Moritz Sinn, Florian Zuleger, Helmut Veith.
CAV, pages 745-761, 2014.
[doi]
Counterexample to induction-guided abstraction-refinement (CTIGAR)
Johannes Birgmeier, Aaron Bradley, Georg Weissenbacher.
CAV, pages 829-846, 2014.
[doi]
Johannes Birgmeier, Aaron Bradley, Georg Weissenbacher.
CAV, pages 829-846, 2014.
[doi]
Connection matrices and the definability of graph parameters
Tomer Kotek, Johann A. Makowsky.
Logical Methods in Computer Science, volume 10, pages 1-33, 2014.
[pdf]
Tomer Kotek, Johann A. Makowsky.
Logical Methods in Computer Science, volume 10, pages 1-33, 2014.
[pdf]
Recurrence relations for graph polynomials on bi-iterative families of graphs
Tomer Kotek, Johann A. Makowsky.
European Journal of Combinatorics, volume 41, pages 47-67, 2014.
[doi]
Tomer Kotek, Johann A. Makowsky.
European Journal of Combinatorics, volume 41, pages 47-67, 2014.
[doi]
Silicon fault diagnosis using sequence interpolation with backbones
Charlie Shucheng Zhu, Georg Weissenbacher, Sharad Malik.
ICCAD, pages 348-355, 2014.
[pdf]
Charlie Shucheng Zhu, Georg Weissenbacher, Sharad Malik.
ICCAD, pages 348-355, 2014.
[pdf]
On the complexity of symbolic verification and decision problems in bit-vector logic
Gergely Kovasznai, Helmut Veith, Andreas Fröhlich, Armin Biere.
2014.
Gergely Kovasznai, Helmut Veith, Andreas Fröhlich, Armin Biere.
2014.
Explaining the decompositionality of monadic second order logic using applications to combinatorics
Tomer Kotek.
2014.
Tomer Kotek.
2014.
Concolic testing of concurrent programs
Azadeh Farzan, Andreas Holzer, Niloofar Razavi, Helmut Veith.
2014.
Azadeh Farzan, Andreas Holzer, Niloofar Razavi, Helmut Veith.
2014.
Parameterized model checking of rendezvous systems
Benjamin Aminof, Tomer Kotek, Sasha Rubin, Francesco Spegni, Helmut Veith.
2014.
Benjamin Aminof, Tomer Kotek, Sasha Rubin, Francesco Spegni, Helmut Veith.
2014.
AngryHEX: An angry birds-playing agent based on HEX-programs
Francesco Calimeri, Michael Fink, Stefano Germano, Andreas Humenberger, Giovambattista Ianni, Christoph Redl, Daria Stepanova, Andrea Tucci.
2014.
Francesco Calimeri, Michael Fink, Stefano Germano, Andreas Humenberger, Giovambattista Ianni, Christoph Redl, Daria Stepanova, Andrea Tucci.
2014.
On the complexity of symbolic verification and decision problems in bit-vector logic
Gergely Kovasznai, Helmut Veith, Andreas Fröhlich, Armin Biere.
MFCS, pages 481-492, 2014.
[doi]
Gergely Kovasznai, Helmut Veith, Andreas Fröhlich, Armin Biere.
MFCS, pages 481-492, 2014.
[doi]
Size-change abstraction and max-plus automata
Thomas Colcombet, Laure Daviaud, Florian Zuleger.
MFCS, pages 208-219, 2014.
[doi]
Thomas Colcombet, Laure Daviaud, Florian Zuleger.
MFCS, pages 208-219, 2014.
[doi]
On the completeness of bounded model checking for threshold-based distributed algorithms: reachability
Igor Konnov, Helmut Veith, Josef Widder.
CONCUR, pages 125-140, 2014.
[doi]
Igor Konnov, Helmut Veith, Josef Widder.
CONCUR, pages 125-140, 2014.
[doi]
Incremental bounded software model checking
Henning Günther, Georg Weissenbacher.
SPIN, pages 40-47, 2014.
[doi]
Henning Günther, Georg Weissenbacher.
SPIN, pages 40-47, 2014.
[doi]
Shape and content - a database-theoretic perspective on the analysis of data structures
Diego Calvanese, Tomer Kotek, Mantas Simkus, Helmut Veith, Florian Zuleger.
IFM, pages 3-17, 2014.
[doi]
Diego Calvanese, Tomer Kotek, Mantas Simkus, Helmut Veith, Florian Zuleger.
IFM, pages 3-17, 2014.
[doi]
An open alternative for SMT-based verification of scade models
Henning Basold, Henning Günther, Michaela Huhn, Stefan Milius.
FMICS, pages 124-139, 2014.
[doi]
Henning Basold, Henning Günther, Michaela Huhn, Stefan Milius.
FMICS, pages 124-139, 2014.
[doi]
Abstraction and mining of traces to explain concurrency bugs
Mitra Tabaei Befrouei, Chao Wang, Georg Weissenbacher.
Runtime verification, pages 162-177, 2014.
[doi]
Mitra Tabaei Befrouei, Chao Wang, Georg Weissenbacher.
Runtime verification, pages 162-177, 2014.
[doi]
A representation theorem for (q-)holonomic sequences
Tomer Kotek, Johann A. Makowsky.
Journal of Computer and System Sciences, volume 80, pages 363-374, 2014.
[doi]
Tomer Kotek, Johann A. Makowsky.
Journal of Computer and System Sciences, volume 80, pages 363-374, 2014.
[doi]
Tutorial on parameterized model checking of fault-tolerant distributed algorithms
Annu Gmeiner, Igor Konnov, Ulrich Schmid, Helmut Veith, Josef Widder.
Formal methods for executable software models, pages 122-171, 2014.
[doi]
Annu Gmeiner, Igor Konnov, Ulrich Schmid, Helmut Veith, Josef Widder.
Formal methods for executable software models, pages 122-171, 2014.
[doi]
Mining sequential patterns to explain concurrent counterexamples
Stefan Leue, Mitra Tabaei Befrouei.
SPIN, pages 264-281, 2013.
[doi]
Stefan Leue, Mitra Tabaei Befrouei.
SPIN, pages 264-281, 2013.
[doi]
Formal verification of distributed algorithms (dagstuhl seminar 13141)
Bernadette Charron-Bost, Andrey Rybalchenko, Stephan Merz, Josef Widder.
2013.
[doi]
Bernadette Charron-Bost, Andrey Rybalchenko, Stephan Merz, Josef Widder.
2013.
[doi]
Information reuse for multi-goal reachability analyses
Dirk Beyer, Andreas Holzer, Michael Tautschnig, Helmut Veith.
ESOP, pages 472-491, 2013.
[doi]
Dirk Beyer, Andreas Holzer, Michael Tautschnig, Helmut Veith.
ESOP, pages 472-491, 2013.
[doi]
Ramsey vs. Lexicographic termination proving
Byron Cook, Abigail See, Florian Zuleger.
Tools and algorithms for the construction and analysis of systems, pages 47-61, 2013.
[doi]
Byron Cook, Abigail See, Florian Zuleger.
Tools and algorithms for the construction and analysis of systems, pages 47-61, 2013.
[doi]
Solving constraints for generational search
Daniel Pötzl, Andreas Holzer.
TAP, pages 197-213, 2013.
[doi]
Daniel Pötzl, Andreas Holzer.
TAP, pages 197-213, 2013.
[doi]
Verification across intellectual property boundaries
Sagar Chaki, Christian Schallhart, Helmut Veith.
ACM Transactions on Software Engineering and Methodology, volume 22, pages Article 15, 2013.
[doi]
Sagar Chaki, Christian Schallhart, Helmut Veith.
ACM Transactions on Software Engineering and Methodology, volume 22, pages Article 15, 2013.
[doi]
Towards modeling and model checking fault-tolerant distributed algorithms
Annu John, Igor Konnov, Ulrich Schmid, Helmut Veith, Josef Widder.
SPIN, pages 209-226, 2013.
[pdf] [doi]
Annu John, Igor Konnov, Ulrich Schmid, Helmut Veith, Josef Widder.
SPIN, pages 209-226, 2013.
[pdf] [doi]
Under-approximating loops in c programs for fast counterexample detection
Daniel Kroening, Matt Lewis, Georg Weissenbacher.
CAV, pages 381-396, 2013.
[doi]
Daniel Kroening, Matt Lewis, Georg Weissenbacher.
CAV, pages 381-396, 2013.
[doi]
Brief announcement: Parameterized model checking of fault-tolerant distributed algorithms by abstraction
Annu John, Igor Konnov, Ulrich Schmid, Helmut Veith, Josef Widder.
PODC, pages 119-121, 2013.
[doi]
Annu John, Igor Konnov, Ulrich Schmid, Helmut Veith, Josef Widder.
PODC, pages 119-121, 2013.
[doi]
Advanced SAT techniques for abstract argumentation
Johannes Peter Wallner, Georg Weissenbacher, Stefan Woltran.
CLIMA, pages 138-154, 2013.
[doi]
Johannes Peter Wallner, Georg Weissenbacher, Stefan Woltran.
CLIMA, pages 138-154, 2013.
[doi]
Parameterized model checking of fault-tolerant distributed algorithms by abstraction
Annu John, Igor Konnov, Ulrich Schmid, Helmut Veith, Josef Widder.
FMCAD, pages 201-209, 2013.
[pdf]
Annu John, Igor Konnov, Ulrich Schmid, Helmut Veith, Josef Widder.
FMCAD, pages 201-209, 2013.
[pdf]
On the concept of variable roles and its use in software analysis
Yulia Demyanova, Helmut Veith, Florian Zuleger.
FMCAD, pages 226-230, 2013.
[pdf]
Yulia Demyanova, Helmut Veith, Florian Zuleger.
FMCAD, pages 226-230, 2013.
[pdf]
Challenges in compiler construction for secure two-party computation
Andreas Holzer, Nikolaos Karvelas, Stefan Katzenbeisser, Helmut Veith.
PETShop, pages 3-6, 2013.
[doi]
Andreas Holzer, Nikolaos Karvelas, Stefan Katzenbeisser, Helmut Veith.
PETShop, pages 3-6, 2013.
[doi]
The first workshop on language support for privacy-enhancing technologies (PETShop'13)
Martin Franz, Andreas Holzer, Rupak Majumdar, Bryan Parno, Helmut Veith.
CCS, pages 1485-1486, 2013.
[doi]
Martin Franz, Andreas Holzer, Rupak Majumdar, Bryan Parno, Helmut Veith.
CCS, pages 1485-1486, 2013.
[doi]
On the structure and complexity of rational sets of regular languages
Andreas Holzer, Christian Schallhart, Michael Tautschnig, Helmut Veith.
FSTTCS, pages 377-388, 2013.
[doi]
Andreas Holzer, Christian Schallhart, Michael Tautschnig, Helmut Veith.
FSTTCS, pages 377-388, 2013.
[doi]
Link reversal routing with binary link labels: Work complexity
Bernadette Charron-Bost, Antoine Gaillard, Jennifer Welch, Josef Widder.
SIAM JOURNAL ON COMPUTING, volume 42, pages 634-661, 2013.
[pdf] [doi]
Bernadette Charron-Bost, Antoine Gaillard, Jennifer Welch, Josef Widder.
SIAM JOURNAL ON COMPUTING, volume 42, pages 634-661, 2013.
[pdf] [doi]
Con2colic testing
Azadeh Farzan, Andreas Holzer, Niloofar Razavi, Helmut Veith.
Esec/sigsoft fse, pages 37-47, 2013.
[doi]
Azadeh Farzan, Andreas Holzer, Niloofar Razavi, Helmut Veith.
Esec/sigsoft fse, pages 37-47, 2013.
[doi]
Parameterized model checking of fault-tolerant distributed algorithms
Annu John, Igor Konnov, Ulrich Schmid, Helmut Veith, Josef Widder.
2012.
Annu John, Igor Konnov, Ulrich Schmid, Helmut Veith, Josef Widder.
2012.
A myhill-nerode theorem for automata with advice
Alex Kruckman, Sasha Rubin, John Sheridan, Ben Zax.
Symposium on games, automata, logics and formal verification, pages 238-246, 2012.
[doi]
Alex Kruckman, Sasha Rubin, John Sheridan, Ben Zax.
Symposium on games, automata, logics and formal verification, pages 238-246, 2012.
[doi]
Wait-free stabilizing dining using regular registers
Srikanth Sastry, Jennifer Welch, Josef Widder.
OPODIS, pages 284-299, 2012.
[doi]
Srikanth Sastry, Jennifer Welch, Josef Widder.
OPODIS, pages 284-299, 2012.
[doi]
Vinter: A vampire-based tool for interpolation
Krystof Hoder, Andreas Holzer, Laura Kovacs, Andrei Voronkov.
APLAS, pages 148-156, 2012.
[doi]
Krystof Hoder, Andreas Holzer, Laura Kovacs, Andrei Voronkov.
APLAS, pages 148-156, 2012.
[doi]
Counter attack against byzantine generals
Annu John, Igor Konnov, Ulrich Schmid, Helmut Veith, Josef Widder.
2012.
Annu John, Igor Konnov, Ulrich Schmid, Helmut Veith, Josef Widder.
2012.
Who is afraid of model checking distributed algorithms?
Igor Konnov, Helmut Veith, Josef Widder.
2012.
Igor Konnov, Helmut Veith, Josef Widder.
2012.
Coverage-based trace signal selection for fault localisation in post-silicon validation
Zhu Charlie Shucheng, Georg Weissenbacher, Sharad Malik.
Haifa verification conference (HVC), pages 132-147, 2012.
[doi]
Zhu Charlie Shucheng, Georg Weissenbacher, Sharad Malik.
Haifa verification conference (HVC), pages 132-147, 2012.
[doi]
Secure two-party computations in ANSI c
Andreas Holzer, Martin Franz, Stefan Katzenbeisser, Helmut Veith.
ACM conference on computer and communications security, pages 772-783, 2012.
[doi]
Andreas Holzer, Martin Franz, Stefan Katzenbeisser, Helmut Veith.
ACM conference on computer and communications security, pages 772-783, 2012.
[doi]
Bounded-interference sequentialization for testing concurrent programs
Niloofar Razavi, Azadeh Farzan, Andreas Holzer.
Leveraging applications of formal methods, verification and validation. Technologies for mastering change, pages 372-387, 2012.
[doi]
Niloofar Razavi, Azadeh Farzan, Andreas Holzer.
Leveraging applications of formal methods, verification and validation. Technologies for mastering change, pages 372-387, 2012.
[doi]
Parallel assertions for architectures with weak memory models
Daniel Schwartz-Narbonne, Georg Weissenbacher, Sharad Malik.
Automated technology for verification and analysis, pages 254-268, 2012.
[doi]
Daniel Schwartz-Narbonne, Georg Weissenbacher, Sharad Malik.
Automated technology for verification and analysis, pages 254-268, 2012.
[doi]
Efficient checking of link-reversal-based concurrent systems
Matthias Függer, Josef Widder.
CONCUR 2012 - concurrency theory, pages 486-499, 2012.
[doi]
Matthias Függer, Josef Widder.
CONCUR 2012 - concurrency theory, pages 486-499, 2012.
[doi]
Interpretations in trees with countably many branches
Alexander Rabinovic, Sasha Rubin.
Logic in computer science, pages 551-560, 2012.
[pdf] [doi]
Alexander Rabinovic, Sasha Rubin.
Logic in computer science, pages 551-560, 2012.
[pdf] [doi]
Interpolant strength revisited
Georg Weissenbacher.
International conference on theory and applications of satisfiability testing (SAT), pages 312-326, 2012.
[pdf] [doi]
Georg Weissenbacher.
International conference on theory and applications of satisfiability testing (SAT), pages 312-326, 2012.
[pdf] [doi]
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, pages 299-321, 2012.
[pdf] [doi]
Josef Widder, Martin Biely, Günther Gridling, Bettina Weiss, Jean-Paul Blanquart.
Distributed Computing, volume 24, pages 299-321, 2012.
[pdf] [doi]
Special issue: Games in verification (foreword)
Helmut Veith.
Journal of Computer and System Sciences, volume 78, pages 393, 2012.
[pdf] [doi]
Helmut Veith.
Journal of Computer and System Sciences, volume 78, pages 393, 2012.
[pdf] [doi]
Selected papers of the conference "computer science logic CSL 2010": preface
Anuj Dawar, Helmut Veith.
Logical Methods in Computer Science, 2012.
[pdf] [doi]
Anuj Dawar, Helmut Veith.
Logical Methods in Computer Science, 2012.
[pdf] [doi]
Proving reachability using FShell
Andreas Holzer, Daniel Kroening, Christian Schallhart, Michael Tautschnig, Helmut Veith.
Proc. Of 18th international conference on tools and algorithms for the construction and analysis of systems (TACAS), pages 538-541, 2012.
[pdf] [doi]
Andreas Holzer, Daniel Kroening, Christian Schallhart, Michael Tautschnig, Helmut Veith.
Proc. Of 18th international conference on tools and algorithms for the construction and analysis of systems (TACAS), pages 538-541, 2012.
[pdf] [doi]
Who is afraid of model checking distributed algorithms?
Annu John, Igor Konnov, Ulrich Schmid, Helmut Veith, Josef Widder.
2012.
Annu John, Igor Konnov, Ulrich Schmid, Helmut Veith, Josef Widder.
2012.
On efficient checking of link-reversal-based concurrent systems
Matthias Függer, Josef Widder.
2011.
Matthias Függer, Josef Widder.
2011.
Seamless testing for models and code
Andreas Holzer, Visar Januzaj, Stefan Kugele, Boris Langer, Christian Schallhart, Michael Tautschnig, Helmut Veith.
Lecture notes in computer science, pages 278-293, 2011.
[doi]
Andreas Holzer, Visar Januzaj, Stefan Kugele, Boris Langer, Christian Schallhart, Michael Tautschnig, Helmut Veith.
Lecture notes in computer science, pages 278-293, 2011.
[doi]
Improving the confidence in measurement-based timing analysis
Sven Bünte, Michael Zolda, Michael Tautschnig, Raimund Kirner.
2011 14th IEEE international symposium on object/component/service-oriented real-time distributed computing (ISORC 2011), pages 144-151, 2011.
Sven Bünte, Michael Zolda, Michael Tautschnig, Raimund Kirner.
2011 14th IEEE international symposium on object/component/service-oriented real-time distributed computing (ISORC 2011), pages 144-151, 2011.
Query-driven program testing
Michael Tautschnig.
2011.
Michael Tautschnig.
2011.
Bound analysis of imperative programs with the size-change abstraction
Florian Zuleger, Moritz Sinn, Sumit Gulwani, Helmut Veith.
Lecture notes in computer science, pages 280-297, 2011.
[doi]
Florian Zuleger, Moritz Sinn, Sumit Gulwani, Helmut Veith.
Lecture notes in computer science, pages 280-297, 2011.
[doi]
Decision procedures in soft, hard and bio-ware - follow up (dagstuhl seminar 11272)
Nikolaj Bjorner, Robert Nieuwenhuis, Helmut Veith, Andrei Voronkov.
Dagstuhl Reports, volume 1, pages 23-35, 2011.
[pdf] [doi]
Nikolaj Bjorner, Robert Nieuwenhuis, Helmut Veith, Andrei Voronkov.
Dagstuhl Reports, volume 1, pages 23-35, 2011.
[pdf] [doi]
Malware detection
Stefan Katzenbeisser, Johannes Kinder, Helmut Veith.
Encyclopedia of cryptography and security, pages 752-755, 2011.
[pdf] [doi]
Stefan Katzenbeisser, Johannes Kinder, Helmut Veith.
Encyclopedia of cryptography and security, pages 752-755, 2011.
[pdf] [doi]
The reachability-bound problem
Sumit Gulwani, Florian Zuleger.
PLDI'10 proceedings of teh ACM SIGPLAN conference on programming language design and implementation, pages 292-304, 2010.
[doi]
Sumit Gulwani, Florian Zuleger.
PLDI'10 proceedings of teh ACM SIGPLAN conference on programming language design and implementation, pages 292-304, 2010.
[doi]
Don't care in SMT---building flexible yet efficient abstraction/refinement solvers
Andreas Bauer, Martin Leucker, Christian Schallhart, Michael Tautschnig.
International Journal on Software Tools for Technology Transfer, volume 12, pages 23-37, 2010.
[doi]
Andreas Bauer, Martin Leucker, Christian Schallhart, Michael Tautschnig.
International Journal on Software Tools for Technology Transfer, volume 12, pages 23-37, 2010.
[doi]
On the distributivity of LTL specifications
Marko Samer, Helmut Veith.
ACM Transactions on Computational Logic, volume 11, 2010.
[doi]
Marko Samer, Helmut Veith.
ACM Transactions on Computational Logic, volume 11, 2010.
[doi]
Seamless model-driven development put into practice
Wolfgang Haberl, Markus Herrmannsdoerfer, Stefan Kugele, Michael Tautschnig, Martin Wechs.
Proceedings of 4th international symposium on leveraging applications, pages 18-32, 2010.
[doi]
Wolfgang Haberl, Markus Herrmannsdoerfer, Stefan Kugele, Michael Tautschnig, Martin Wechs.
Proceedings of 4th international symposium on leveraging applications, pages 18-32, 2010.
[doi]
Timely time estimates
Andreas Holzer, Visar Januzaj, Stefan Kugele, Michael Tautschnig.
Proceedings of 4th international symposium on leveraging applications (ISoLA 2010), pages 33-46, 2010.
[doi]
Andreas Holzer, Visar Januzaj, Stefan Kugele, Michael Tautschnig.
Proceedings of 4th international symposium on leveraging applications (ISoLA 2010), pages 33-46, 2010.
[doi]
An introduction to test specification in FQL
Andreas Holzer, Christian Schallhart, Michael Tautschnig, Helmut Veith.
Lecture notes in computer science, pages 9-22, 2010.
[doi]
Andreas Holzer, Christian Schallhart, Michael Tautschnig, Helmut Veith.
Lecture notes in computer science, pages 9-22, 2010.
[doi]
How did you specify your test suite?
Andreas Holzer, Christian Schallhart, Michael Tautschnig, Helmut Veith.
Proceedings of the 25th IEEE/ACM international conference on automated software engineering (ASE 2010), pages 407-416, 2010.
[doi]
Andreas Holzer, Christian Schallhart, Michael Tautschnig, Helmut Veith.
Proceedings of the 25th IEEE/ACM international conference on automated software engineering (ASE 2010), pages 407-416, 2010.
[doi]
Proactive detection of computer worms using model checking
Johannes Kinder, Stefan Katzenbeisser, Christian Schallhart, Helmut Veith.
IEEE Transactions on Dependable and Secure Computing, volume 7, pages 424-438, 2010.
[doi]
Johannes Kinder, Stefan Katzenbeisser, Christian Schallhart, Helmut Veith.
IEEE Transactions on Dependable and Secure Computing, volume 7, pages 424-438, 2010.
[doi]
Semantic integrity in large-scale online simulations
Somesh Jha, Stefan Katzenbeisser, Christian Schallhart, Helmut Veith, Stephen Chenney.
ACM Transactions on Internet Technology, volume 10, 2010.
[doi]
Somesh Jha, Stefan Katzenbeisser, Christian Schallhart, Helmut Veith, Stephen Chenney.
ACM Transactions on Internet Technology, volume 10, 2010.
[doi]
Architecture and security in networked virtual environments
Christian Schallhart.
2007.
Christian Schallhart.
2007.
Towards a systematic design of fault-tolerant asynchronous circuits
Ulrich Schmid, Andreas Steininger, Helmut Veith.
Fachtagung zuverlässigkeit und entwurf, pages 173-174, 2007.
Ulrich Schmid, Andreas Steininger, Helmut Veith.
Fachtagung zuverlässigkeit und entwurf, pages 173-174, 2007.
From temporal logic queries to vacuity detection
Marko Samer, Helmut Veith.
Verification of infinite-state systems with applications to security, pages 149-167, 2006.
Marko Samer, Helmut Veith.
Verification of infinite-state systems with applications to security, pages 149-167, 2006.
Deterministic CTL query solving
Marko Samer, Helmut Veith.
Proceedings of the 12th international symposium on temporal representation and reasoning, pages 156-165, 2005.
Marko Samer, Helmut Veith.
Proceedings of the 12th international symposium on temporal representation and reasoning, pages 156-165, 2005.
Counterexamples revisited: Principles, algorithms, applications
Edmund Clarke, Helmut Veith.
Verification: Theory and practice: Essays dedicated to zohar manna on the occasion of his 64th birthday, pages 208-224, 2004.
Edmund Clarke, Helmut Veith.
Verification: Theory and practice: Essays dedicated to zohar manna on the occasion of his 64th birthday, pages 208-224, 2004.
SAT based predicate abstraction for hardware verification
Edmund Clarke, Muralidhar Talupur, Helmut Veith, Dong Wang.
Lecture notes in computer science, pages 78-92, 2004.
Edmund Clarke, Muralidhar Talupur, Helmut Veith, Dong Wang.
Lecture notes in computer science, pages 78-92, 2004.
Reasoning about specifications in model checking
Marko Samer.
2004.
Marko Samer.
2004.
Cryptographic watermarking
Stefan Katzenbeisser.
2004.
Stefan Katzenbeisser.
2004.
A syntactic characterization of distributive LTL queries
Marko Samer, Helmut Veith.
Proceedings of the 31st international colloquium on automata, languages and programming, pages 1099-1110, 2004.
Marko Samer, Helmut Veith.
Proceedings of the 31st international colloquium on automata, languages and programming, pages 1099-1110, 2004.
Parameterized vacuity
Marko Samer, Helmut Veith.
Proceedings of the 5th international conference on formal methods in computer-aided design, pages 322-336, 2004.
Marko Samer, Helmut Veith.
Proceedings of the 5th international conference on formal methods in computer-aided design, pages 322-336, 2004.
Integrating publish/subscribe into a mobile teamwork support platform
N. Sagar, Pascal Fenkam, Helmut Veith, Harald Gall, Engin Kirda, Somesh Jha.
Proceedings of the 15th international conference on software engineering and knowledge engineering, pages 510-517, 2003.
N. Sagar, Pascal Fenkam, Helmut Veith, Harald Gall, Engin Kirda, Somesh Jha.
Proceedings of the 15th international conference on software engineering and knowledge engineering, pages 510-517, 2003.
Friends or foes? Communities in software verification
Helmut Veith.
Lecture notes in computer science, pages 528-529, 2003.
Helmut Veith.
Lecture notes in computer science, pages 528-529, 2003.
Watermarking schemes provably secure against copy and ambiguity attacks
André Adelsbach, Stefan Katzenbeisser, Helmut Veith.
Porceedings of the 2003 ACM workshop on digital rights management, pages 111-119, 2003.
André Adelsbach, Stefan Katzenbeisser, Helmut Veith.
Porceedings of the 2003 ACM workshop on digital rights management, pages 111-119, 2003.
Counterexample-guided abstraction refinement for symbolic model checking
Edmund Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, Helmut Veith.
Journal of the ACM, volume Volume 50, pages 752-794, 2003.
Edmund Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, Helmut Veith.
Journal of the ACM, volume Volume 50, pages 752-794, 2003.
Validity of CTL queries revisited
Marko Samer, Helmut Veith.
Proceedings of the 12th annual conference of the european association for computer science logic, pages 470-483, 2003.
Marko Samer, Helmut Veith.
Proceedings of the 12th annual conference of the european association for computer science logic, pages 470-483, 2003.
Symbolic model checking using NUSMV
Andreas Plaickner.
2003.
Andreas Plaickner.
2003.
Symbolic model checking using NUSMV
Andreas Plaickner.
2003.
Andreas Plaickner.
2003.
Modular verification of software components in c\*
Sagar Chaki, Edmund Clarke, Alex Groce, Somesh Jha, Helmut Veith.
Proceedings of the 25^th^ conference on software engineering, pages 385-395, 2003.
Sagar Chaki, Edmund Clarke, Alex Groce, Somesh Jha, Helmut Veith.
Proceedings of the 25^th^ conference on software engineering, pages 385-395, 2003.
Securing symmetric watermarking schemes against protocol attacks
Stefan Katzenbeisser, Helmut Veith.
Proceedings of SPIE 2002, pages 260-268, 2002.
Stefan Katzenbeisser, Helmut Veith.
Proceedings of SPIE 2002, pages 260-268, 2002.
Tree-like counterexamples in model cheking
Edmund Clarke, Somesh Jha, Yuan Lu, Helmut Veith.
Proceedings of the seventeenth annual IEEE symposium on logic in computer science (LICS' 2002), pages 19-29, 2002.
Edmund Clarke, Somesh Jha, Yuan Lu, Helmut Veith.
Proceedings of the seventeenth annual IEEE symposium on logic in computer science (LICS' 2002), pages 19-29, 2002.
On the complexity of data disjunctions
Thomas Eiter, Helmut Veith.
Theoretical Computer Science, volume 288, pages 101-128, 2002.
Thomas Eiter, Helmut Veith.
Theoretical Computer Science, volume 288, pages 101-128, 2002.
Datalog LITE: A deductive query language with linear time model checking
Georg Gottlob, Erich Grädel, Helmut Veith.
ACM Transactions on Computational Logic, volume Volume 3, pages 42-79, 2002.
Georg Gottlob, Erich Grädel, Helmut Veith.
ACM Transactions on Computational Logic, volume Volume 3, pages 42-79, 2002.
Temporal logic queries in model checking
Marko Samer.
2002.
Marko Samer.
2002.
Automated abstraction refinement for model checking large state spaces using SAT based conflict analysis
Pankaj Chauhan, Edmund Clarke, James Kukula, Samir Sapra, Helmut Veith, Dong Wang.
Proceedings of the 4^th^ international conference on formal methods in computer-aided design, pages 33-51, 2002.
[pdf]
Pankaj Chauhan, Edmund Clarke, James Kukula, Samir Sapra, Helmut Veith, Dong Wang.
Proceedings of the 4^th^ international conference on formal methods in computer-aided design, pages 33-51, 2002.
[pdf]