Publications

This page contains the list of publications of FMV since 2004.

2017

Aina Niemetz. Bit Precise Reasoning Beyond Bit-Blasting. Dissertation Technische Wissenschaften, Informatik, Johannes Kepler Univerity, Linz, 2017.
[ thesis | bibtex ]

Mathias Preiner. Lambdas, Arrays and Quantifiers. Dissertation Technische Wissenschaften, Informatik, Johannes Kepler Univerity, Linz, 2017.
[ thesis | bibtex ]

Daniela Ritirc, Armin Biere, and Manuel Kauers. Column-Wise Verification of Multipliers Using Computer Algebra. In Proc. 17th Intl. Conf. on Formal Methods in Computer Aided Design (FMCAD'17), to appear.
[ paper | bibtex | experiments ]

Best paper
Marijn Heule, Benjamin Kiesl, Armin Biere. Short Proofs Without New Variables . In Proc. 26th Intl. Conf. on Automated Deduction (CADE'17). Lecture Notes in Computer Science (LNCS) vol. 10395, pages 130-147, Springer 2017.
[ paper | bibtex | experiments ]

Benjamin Kiesl, Martina Seidl, Hans Tompits, Armin Biere. Blockedness in Propositional Logic: Are You Satisfied With Your Neighborhood? Proc.&nbps;26th Intl. Joint Conf. on Artificial Intelligence (IJCAI'17). ijcai.org, pages 4884-4888, 2017.
[ paper | bibtex ]

Katalin Fazekas, Marijn J. H. Heule, Martina Seidl, Armin Biere. Skolem Function Continuation for Quantified Boolean Formulas. Proc. 11th Intl. Conf. on Tests and Proofs (TAP'17). Lecture Notes in Computer Science vol. 10375, Springer, pages 129-138, 2017
[ paper | bibtex | tool ]

Benjamin Kiesl, Martin Suda, Martina Seidl, Hans Tompits, Armin Biere. Blocked Clauses in First-Order Logic. Proc. 21st Intl. Conf. on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-21). EPiC Series in Computing vol. 46, Easychair, pages 31-48, 2017.
[ preliminary extended version | arxiv | EasyChair | bibtex ]

Mathias Preiner, Aina Niemetz, Armin Biere. Counterexample-Guided Model Synthesis. In Proc. 23rd Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'17), Lecture Notes in Computer Science (LNCS) vol. 10205, pages 264-280, Springer 2017.
[ paper | bibtex | data | boolector ]

Benjamin Kiesl, Marijn J. H. Heule, Martina Seidl. A Little Blocked Literal Goes a Long Way. Proc. of the 20th Int. Conf. on Theory and Applications of Satisfiability Testing (SAT 2017), Lecture Notes in Computer Science vol. 10491, Springer, pages 281-297, 2017.
[ paper | bibtex ]

Benjamin Kiesl, Martina Seidl, Hans Tompits, Armin Biere. Blockedness in Propositional Logic: Are You Satisfied With Your Neighborhood? Proc.&nbps;26th Intl. Joint Conf. on Artificial Intelligence (IJCAI'17). ijcai.org, pages 4884-4888, 2017.
[ paper | bibtex ]

Swen Jacobs, Roderick Bloem, Romain Brenguier, Rüdiger Ehlers, Timotheus Hell, Robert Könighofer, Guillermo A. Pérez, Jean-François Raskin, Leonid Ryzhyk, Ocan Sankur, Martina Seidl, Leander Tentrup, Adam Walker. The First Reactive Synthesis Competition (SYNTCOMP 2014). Int. Journal on Software Tools for Technology Transfer (STTT) , 19(3), pages 367-390, June 2017.
[ preprint | bibtex | arxiv ]

Sebastian Gabmeyer, Petra Kaufmann, Martina Seidl, Martin Gogolla, Gerti Kappel. A feature-based classification of formal verification techniques for software models. Software & Systems Modeling, pages 1-26, online first, March 2017.
[ preprint | bibtex ]

Marijn Heule, Martina Seidl, Armin Biere. Validation and Extraction for QBF Preprocessing. Journal of Automated Reasoning, 58(1), pages 97-125, Springer 2017.
[ preprint | bibtex ]

Katalin Fazekas, Martina Seidl, Armin Biere. A Duality-Aware Calculus for Quantified Boolean Formulas. In Proc. 18th Intl. Symp. on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'16), pages 181-186, IEEE Computer Society, 2016.
[ paper | bibtex ]

2016

Andreas Fröhlich. Theoretical and Practical Aspects of Bit-Vector Reasoning. Dissertation Technische Wissenschaften, Informatik, Johannes Kepler University, Linz, 2016.
[ thesis | bibtex ]

Tomas Balyo, Armin Biere, Markus Iser, Carsten Sinz. SAT Race 2015, in Journal of Artificial Intelligence, vol. 241, pages 45-65, Elsevier 2016.
[ preprint | bibtex | web | ipasir.zip | ipasir.h ]

Marijn Heule, Armin Biere. Clausal Proof Compression. In Proc. 11th Intl. Workshop on the Implementation of Logics (IWIL'15), EPiC Series in Computing vol. 40, pages 21-26, EasyChair, 2016.
[ paper | bibtex | ratz | sbp ]

Akihisa Yamada, Armin Biere, Cyrille Artho, Takashi Kitamura, Eun-Hye Choi. Greedy combinatorial test case generation using unsatisfiable cores In Proc. 31st IEEE/ACM Intl. Conf. on Automated Software Engineering (ASE'16), pages 614-624, ACM 2016.
[ paper | bibtex ]

Aina Niemetz, Mathias Preiner, Armin Biere. Precise and Complete Propagation Based Local Search for Satisfiability Modulo Theories. In Proc. 28th Intl. Conf. on Computer Aided Verification (CAV'16), Lecture Notes in Computer Science (LNCS) vol. 9779, pages 199-217, Springer 2016.
[ paper | bibtex | data | boolector ]

Aina Niemetz, Mathias Preiner, Armin Biere. Boolector at the SMT competition 2016. Technical Report 16/1, June 2016, FMV Reports Series, Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr. 69, 4040 Linz, Austria.
[ report | bibtex | boolector ]

Armin Biere. Splatz, Lingeling, Plingeling, Treengeling, YalSAT Entering the SAT Competition 2016. In Proceedings of SAT Competition 2016 - Solver and Benchmark Descriptions, Tomas Balyo, Marijn Heule, Matti Järvisalo (editors), vol. B-2016-1 of Department of Computer Science Series of Publications B, pages 44-45, University of Helsinki, 2016.
[ paper | bibtex ]

Armin Biere. Collection of Combinational Arithmetic Miters Submitted to the SAT Competition 2016. In Proceedings of SAT Competition 2016 - Solver and Benchmark Descriptions, Tomas Balyo, Marijn Heule, Matti Järvisalo (editors), vol. B-2016-1 of Department of Computer Science Series of Publications B, pages 65-66, University of Helsinki, 2016.
[ paper | bibtex | data ]

Gianpiero Cabodi, Carmelo Loiacono, Marco Palena, Paolo Pasini, Denis Patti, Stefano Quer, Danilo Vendraminetto, Armin Biere, Keijo Heljanko. Hardware Model Checking Competition 2014: An Analysis and Comparison of Solvers and Benchmarks. Journal of Satisfiability, Boolean Modeling and Computation (JSAT), vol. 9, pages 135-172, 2014 (published 2016), IOS Press.
[ paper | bibtex ]

Aina Niemetz, Mathias Preiner, Armin Biere. Boolector at the SMT competition 2016. Technical Report 16/1, June 2016, FMV Reports Series, Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr. 69, 4040 Linz, Austria.
[ report | bibtex | boolector ]

Swen Jacobs, Roderick Bloem, Romain Brenguier, Ayrat Khalimov, Felix Klein, Robert Könighofer, Jens Kreber, Alexander Legg, Nina Narodytska, Guillermo A. Pérez, Jean-François Raskin, Leonid Ryzhyk, Ocan Sankur, Martina Seidl, Leander Tentrup, Adam Walker. The 3rd Reactive Synthesis Competition (SYNTCOMP 2016): Benchmarks, Participants & Results. SYNT@CAV 2016: 149-177, 2016.
[ arxiv | bibtex ]

Roderick Bloem, Uwe Egly, Patrick Klampfl, Robert Könighofer, Florian Lonsing, Martina Seidl. Satisfiability-Based Methods for Reactive Synthesis from Safety Specifications. CoRR abs/1604.06204, 2016.
[ arxiv | bibtex ]

Florian Lonsing, Martina Seidl. Proceedings of the 4th International Workshop on Quantified Boolean Formulas (QBF 2016). In CEUR Workshop Proceedings 1719, CEUR-WS.org 2016.
[ proceedings | bibtex ]

Sebastian Gabmeyer, Martina Seidl. Lightweight Symbolic Verification of Graph Transformation Systems with Off-the-Shelf Hardware Model Checkers. In Proc. 10th Intl. Conf. on Tests & Proofs (TAP'16), Lecture Notes in Computer Science (LNCS) vol. 9762, pages 94-111, Springer 2016.
[ paper | bibtex ]

Florian Lonsing, Uwe Egly, Martina Seidl. Q-Resolution with Generalized Axioms. In Proc. 19th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'16), Lecture Notes in Computer Science (LNCS) vol. 9710, 435-452, Springer 2016.
[ paper | bibtex | arxiv ]

Benjamin Kiesl, Martina Seidl, Hans Tompits, Armin Biere. Super-Blocked Clauses. In Proc. 8th Joint Conf. on Automated Reasoning (IJCAR'16), Lecture Notes in Computer Science (LNCS) vol. 9706, 45-61, Springer 2016.
[ paper | bibtex ]

Mikolas Janota, Charles Jordan, Will Klieber, Florian Lonsing, Martina Seidl, Allen Van Gelder. The QBFGallery 2014: The QBF Competition at the FLoC Olympic Games. Journal of Satisfiability, Boolean Modeling and Computation (JSAT), vol. 9, pages 187-206, 2014 (published 2016), IOS Press.
[ paper | bibtex ]

Florian Lonsing, Martina Seidl, Allen Van Gelder. The QBF Gallery: Behind the scenes. In Artificial Intelligence 237:92-114 , 2016
[ paper | bibtex | arxiv ]

Charles Jordan, William Klieber, Martina Seidl. Non-CNF QBF Solving with QCIR. In AAAI-16 Workshop on Beyond NP, 7 pages, 2016.
[ paper | bibtex ]

2015

Marijn Heule, Armin Biere. Compositional Propositional Proofs. In Proc. 20th Intl. Conf. on Logic for Programming , Artificial Intelligence, and Reasoning 2015 (LPAR-20), Lecture Notes in Computer Science (LNCS) vol. 9450, pages 444-459, Springer 2015.
[ paper | bibtex | data | drabt ]

Florian Lonsing, Fahiem Bacchus, Armin Biere, Uwe Egly and Martina Seidl: Enhancing Search-Based QBF Solving by Dynamic Blocked Clause Elimination. In Proc. 20th Intl. Conf. on Logic for Programming , Artificial Intelligence, and Reasoning 2015 (LPAR-20), Lecture Notes in Computer Science (LNCS) vol. 9450, pages 418-433, Springer 2015.

Mathias Preiner, Aina Niemetz, Armin Biere. Better Lemmas with Lambda Extraction. In Proc. 15th Intl. Conf. on Formal Methods in Computer Aided Design (FMCAD'15), pages 128-135, FMCAD Inc. 2015.
[ paper | bibtex | boolector ]

Aina Niemetz, Mathias Preiner, Armin Biere, Andreas Fröhlich. Improving Local Search For Bit-Vector Logics in SMT with Path Propagation. In Proc. 4th Intl. Work. on Design and Implementation of Formal Tools and Systems (DIFTS'15), 10 pages, aff. to FMCAD'15, Austin, TX, USA, 2015.
[ paper | bibtex | data | boolector ]

Armin Biere, Andreas Fröhlich. Evaluating CDCL Variable Scoring Schemes. In Proc. 18th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'15), Lecture Notes in Computer Science (LNCS) vol. 9340, pages 405-422, Springer 2015.
[ paper | bibtex | data ]

Aina Niemetz, Mathias Preiner, Armin Biere. Boolector at the SMT Competition 2015. Technical Report 15/1, June 2015, FMV Reports Series, Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr. 69, 4040 Linz, Austria.
[ report | bibtex | boolector ]

Armin Biere. Lingeling and Friends Entering the SAT Race 2015. Technical Report 15/2, April 2015, FMV Reports Series, Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr. 69, 4040 Linz, Austria.
[ report | bibtex | lingeling ]

Armin Biere, Andreas Fröhlich. Evaluating CDCL Restart Schemes (preliminary version). In Proc. Intl. Workshop on Pragmatics of SAT (POS'15), 16 pages, aff. to SAT'15, Austing, TX, USA, 2015.

Gergely Kovásznai, Andreas Fröhlich, Armin Biere. Complexity of Fixed-Size Bit-Vector Logics (preprint). Theory of Computing Systems (TOCS), vol. 59, number 2, pages 323-376, Springer 2016, first online Sept. 2015.
[ preprint | bibtex ]

Aina Niemetz, Mathias Preiner, Armin Biere. Boolector 2.0. Journal of Satisfiability, Boolean Modeling and Computation (JSAT), vol. 9, pages 53-58, 2014 (published 2015), IOS Press.
[ paper | bibtex | boolector ]

Marijn Heule, Matti Järvisalo, Florian Lonsing, Martina Seidl, Armin Biere. Clause Elimination for SAT and QSAT. Journal of Artificial Intelligence Research (JAIR). vol. 53, pages 127-168, 2015.

Marijn Heule, Martina Seidl, Armin Biere. Blocked Literals are Universal. In Proc. 7th Intl. Symp. NASA Formal Methods (NFM'15), Lecture Notes in Computer Science (LNCS), vol. 9058, pages 436 - 442, Springer 2015.

Akihisa Yamada, Takashi Kitamura, Cyrille Artho, Eun-Hye Choi, Yutaka Oiwa, Armin Biere. Optimization of Combinatorial Testing by Incremental SAT Solving. In Proc. 8th IEEE Intl. Conf. on Software Testing Verification, and Validation (ICST'15), pages 1 - 10, IEEE 2015.

Andreas Fröhlich, Armin Biere, Christoph Wintersteiger, Youssef Hamadi. Stochastic Local Search for Satisfiability Modulo Theories. In Proc. 29th AAAI Conf. on Artificial Intelligence (AAAI'15), pages 1136 - 1143, AAAI Press 2015.
[ paper | bibtex ]

Marijn Heule, Armin Biere. Proofs for Satisfiability Problems. In All about Proofs, Proofs for All (APPA), Mathematical Logic and Foundations, vol. 55, pages 1 - 22, College Publications 2015.

Aina Niemetz, Mathias Preiner, Armin Biere. Boolector at the SMT Competition 2015. Technical Report 15/1, June 2015, FMV Reports Series, Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr. 69, 4040 Linz, Austria.
[ report | bibtex | boolector ]

Armin Biere. Lingeling and Friends Entering the SAT Race 2015. Technical Report 15/2, April 2015, FMV Reports Series, Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr. 69, 4040 Linz, Austria.
[ report | bibtex | lingeling ]

Martina Seidl, Marion Scholz, Christian Huemer, Gerti Kappel: UML @ Classroom - An Introduction to Object-Oriented Modeling. Undergraduate Topics in Computer Science, Springer 2015, ISBN 978-3-319-12741-5, pp. 1-194

Petra Kaufmann, Martin Kronegger, Andreas Pfandler, Martina Seidl, Magdalena Widl: Intra- and interdiagram consistency checking of behavioral multiview models (Preprint). Computer Languages, Systems & Structures 44: 72-88 (2015)

Michalis Famelis, Daniel Ratiu, Martina Seidl, Gehan M. K. Selim: Proceedings of the 12th Workshop on Model-Driven Engineering, Verification and Validation co-located with ACM/IEEE 18th International Conference on Model Driven Engineering Languages and Systems, MoDeVVa@MoDELS 2015, Ottawa, Canada, September 29, 2015. CEUR Workshop Proceedings 1514, CEUR-WS.org 2015

Swen Jacobs, Roderick Bloem, Romain Brenguier, Rüdiger Ehlers, Timotheus Hell, Robert Könighofer, Guillermo A. Pérez, Jean-François Raskin, Leonid Ryzhyk, Ocan Sankur, Martina Seidl, Leander Tentrup, Adam Walker: The First Reactive Synthesis Competition (SYNTCOMP 2014). CoRR abs/1506.08726 (2015)

Florian Lonsing, Martina Seidl, Allen Van Gelder: The QBF Gallery: Behind the Scenes. CoRR abs/1508.01045 (2015)

Martina Seidl: Contributions to Rigorous Software Engineering: Models and Reasoning in the Context of Formal Verification. Habilitation Thesis, Johannes Kepler University Linz (Submitted), 2015

Cyrille Artho, Martina Seidl, Quentin Gros, Eun-Hye Choi, Takashi Kitamura, Akira Mori, Rudolf Ramler, Yoriyuki Yamagata: Model-based testing of stateful APIs with Modbat (Preprint). Proceddings of the 2015 30th IEEE/ACM International Conference on Automated Software Engineering (ASE 2015), pages 858-863, DOI 10.1109/ASE.2015.95, IEEE, November, 2015.

Katalin Fazekas. EUF-Proofs for SMT4J. Master Thesis, Computer Science, Johannes Kepler University, Linz, 2015.

2014

Gilles Audemard, Armin Biere, Jean-Marie Lagniez, Laurent Simon. Améliorer SAT dans le cadre incrémental. Revue d'Intelligence Artificielle, 593-614, 28(5), 2014.

Marijn Heule, Martina Seidl, Armin Biere. Efficient Extraction of Skolem Functions from QRAT Proofs. In Proc. 14th Intl. Conf. on Formal Methods in Computer Aided Design (FMCAD'14), 107-114, FMCAD Inc. 2014.

Aina Niemetz, Mathias Preiner, Armin Biere. Turbo-Charging Lemmas on Demand with Don't Care Reasoning. In Proc. 14th Intl. Conf. on Formal Methods in Computer Aided Design (FMCAD'14), 179-186, FMCAD Inc 2014.
[ paper | bibtex | data | boolector ]

Armin Biere, Ioan Dragan, Laura Kovács, Andrei Voronkov. Experimenting with SAT Solvers in Vampire . In Proc. 13th Mexican Intl. Conf. on Artificial Intelligence (MICAI), Lecture Notes in Computer Science (LNCS), vol. 8856, 431-442, Springer 2014.
[ paper | bibtex ]

Gergely Kovásznai, Helmut Veith, Andreas Fröhlich, Armin Biere. On the Complexity of Symbolic Verification and Decision Problems in Bit-Vector Logic. In Proc. 39th Intl. Symp. on Mathematical Foundations of Computer Science (MFCS'14), Lecture Notes in Computer Science (LNCS), vol. 8635, 481-492, Springer 2014.

Armin Biere, Roderick Bloem (editors). Proc. 26th Intl. Conf. on Computer Aided Verification (CAV'14), Lecture Notes in Computer Science (LNCS), vol. 8559, Springer 2014.

Andreas Fröhlich, Gergely Kovásznai, Armin Biere, Helmut Veith. iDQ: Instantiation-Based DQBF Solving. In Proc. Intl. Workshop on Pragmatics of SAT (POS'14), EPiC Series in Computing, vol. 27, 103-116, EasyChair 2014.

Aina Niemetz, Mathias Preiner, Armin Biere. Boolector at the SMT competition 2014. Technical Report 14/1, June 2014, FMV Reports Series, Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr. 69, 4040 Linz, Austria.
[ report | bibtex | boolector ]

Armin Biere, Ioan Dragan, Laura Kovacs, Andrei Voronkov. SAT solving experiments in Vampire . In Proc. 1st and 2nd Vampire Workshop (Vampire'14 and Vampire'15), EPiC Series in Computing, vol. 38, 29-32, EasyChair 2016.
[ paper | bibtex ]

Armin Biere. Yet another Local Search Solver and Lingeling and Friends Entering the SAT Competition 2014. In Proceedings of SAT Competition 2014, Adrian Balint, Anton Belov, Marijn Heule, Matti Järvisalo (editors), vol. B-2014-2 of Department of Computer Science Series of Publications B, pages 39-40, University of Helsinki, 2014.

Marijn Heule, Martina Seidl, Armin Biere. A Unified Proof System for QBF Preprocessing, In Proc. 7th Joint Conf. on Automated Reasoning (IJCAR'14), Lecture Notes in Computer Science (LNCS) vol. 8562, 91-106, Springer 2014.

Adrian Balint, Armin Biere, Andreas Fröhlich, Uwe Schöning. Improving implementation of SLS solvers for SAT and new heuristics for k-SAT with long clauses. In Proc. 17th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'14), Lecture Notes in Computer Science (LNCS) vol. 8561, 302-316, Springer 2014.

Tomas Balyo, Andreas Fröhlich, Marijn Heule, Armin Biere. Everything You Always Wanted to Know About Blocked Sets (But Were Afraid to Ask). In Proc. 17th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'14), Lecture Notes in Computer Science (LNCS) vol. 8561, 317-332, Springer 2014.

Armin Biere, Daniel Le Berre, Emmanuel Lonca, Norbert Manthey. Detecting cardinality constraints in CNF. In Proc. 17th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'14), Lecture Notes in Computer Science (LNCS) vol. 8561, 285-301, Springer 2014.

Aina Niemetz, Mathias Preiner, Armin Biere. Boolector at the SMT competition 2014. Technical Report 14/1, June 2014, FMV Reports Series, Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr. 69, 4040 Linz, Austria.
[ report | bibtex | boolector ]

Petra Kaufmann, Martin Kronegger, Andreas Pfandler, Martina Seidl, Magdalena Widl: A SAT-Based Debugging Tool for State Machines and Sequence Diagrams. Best paper at the Int. Conf. on Software Language Engineering, Lecture Notes in Computer Science (SLE 2014), Lecture Notes in Computer Science, Volume 8706, 21-40, Springer, 2014.

Robert Bill, Sebastian Gabmeyer, Petra Kaufmann, Martina Seidl: Model Checking of CTL-Extended OCL Specifications. Proc. of the Int. Conf. on Software Language Engineering, Lecture Notes in Computer Science (SLE 2014), Lecture Notes in Computer Science, Volume 8706, 221-240, Springer, 2014.

Martina Seidl, Nikolai Tillmann (Eds.): Tests and Proofs - 8th International Conference (TAP 2014), Lecture Notes in Computer Science 8570, Springer 2014, ISBN 978-3-319-09098-6.

M. Seidl, R. Könighofer: Partial witnesses from preprocessed quantified Boolean formulas. Proc. of the Int. Design, Automation & Test in Europe Conference & Exhibition (DATE 2014): 1-6, IEEE, 2014.

R. Bloem, R. Könighofer, M. Seidl: SAT-Based Synthesis Methods for Safety Specs. Proc. of the 15th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2014), 20 pages, Lecture Notes in Computer Science (LNCS), Springer, 2014.

C. Jordan, L. Kaiser, F. Lonsing, M. Seidl: MPIDepQBF: Towards Parallel QBF Solving without Knowledge Sharing. In Proc. 17th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'14), Lecture Notes in Computer Science (LNCS) vol. 8561, 430-437, Springer 2014.

Christian Reisenberger. PBoolector: A Parallel SMT Solver for QF_BV by Combining Bit-Blasting with Look-Ahead. Master Thesis, Computer Science, Johannes Kepler University, Linz, 2014.

Harald Seltner. Extracting Hardware Circuits from CNF Formulas. Master Thesis, Computer Science, Johannes Kepler University, Linz, 2014.

2013

Marijn Heule, Armin Biere. Blocked Clause Decomposition. In Proc. 19th Intl. Conf. on Logic for Programming, Artificial Intelligence and Reasoning 2013 (LPAR-19), Lecture Notes in Computer Science (LNCS) vol. 8312, pages 423–438, Springer 2013.

Cyrille Artho, Armin Biere, Masami Hagiya, Eric Platon, Martina Seidl, Yoshinori Tanabe, Mitsuharu Yamamoto. Modbat: A Model-based API Tester for Event-driven Systems. In Proc. Haifa Verification Conference (HVC'13), Lecture Notes in Computer Science (LNCS) vol. 8244, pages 112-128, Springer 2013.

Mathias Preiner, Aina Niemetz, Armin Biere. Lemmas on Demand for Lambdas. In Proc. 2nd Intl. Work. on Design and Implementation of Formal Tools and Systems (DIFTS'13), 10 pages, aff. to FMCAD'13, Portland, Oregon, USA, 2013.
[ paper | bibtex | data | boolector ]

Armin Biere, Jens Knoop, Laura Kovács, Jakob Zwirchmayr. SmacC: A Retargetable Symbolic Execution Engine. In Proc. 11th Intl. Symp. on Automated Technology for Verification and Analysis (ATVA'13), Lecture Notes in Computer Science (LNCS) vol. 8172, pages 482-486, Springer 2013.

Andreas Fröhlich, Gergely Kovásznai, Armin Biere. Efficiently Solving Bit-Vector Problems Using Model Checkers. In Proc. 11th Intl. Workshop on Satisfiability Modulo Theories (SMT'13), pages 6-15, aff. to SAT'13, Helsinki, Finland, 2013.

Aina Niemetz, Armin Biere. ddSMT: A Delta Debugger for the SMT-LIB v2 Format. In Proc. 11th Intl. Workshop on Satisfiability Modulo Theories (SMT'13), pages 36-45, aff. to SAT'13, Helsinki, Finland, 2013.
[ paper | bibtex | ddsmt ]

Martin Aigner, Armin Biere, Christoph Kirsch, Aina Niemetz, Mathias Preiner. Analysis of Portfolio-Style Parallel SAT Solving on Current Multi-Core Architectures. In Proc. Intl. Workshop on Pragmatics of SAT (POS'13), EPiC Series in Computing, vol. 29, 28-40, EasyChair 2014.

Armin Biere, Jens Knoop, Laura Kovács, Jakob Zwirchmayr. The Auspicious Couple: Symbolic Execution and WCET Analysis. In Proc. 13th Intl. Work.  on Worst-Case Execution Time Analysis (WCET'13), OASICS series, vol. 30, pages 53-63, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2013.

Armin Biere. Lingeling, Plingeling and Treengeling Entering the SAT Competition 2013. In Proceedings of SAT Competition 2013, Adrian Balint, Anton Belov, Marijn Heule, Matti Järvisalo (editors), vol. B-2013-1 of Department of Computer Science Series of Publications B, pages 51-52, University of Helsinki, 2013.

Armin Biere. Two Pigeons per Hole Problem. In Proceedings of SAT Competition 2013, Adrian Balint, Anton Belov, Marijn Heule, Matti Järvisalo (editors), vol. B-2013-1 of Department of Computer Science Series of Publications B, page 103, University of Helsinki, 2013.

Armin Biere, Marijn Heule, Matti Järvisalo, Norbert Manthey. Equivalence checking of HWMCC 2012 Circuits. In Proceedings of SAT Competition 2013, Adrian Balint, Anton Belov, Marijn Heule, Matti Järvisalo (editors), vol. B-2013-1 of Department of Computer Science Series of Publications B, page 104 , University of Helsinki, 2013.

Gergely Kovásznai, Andreas Fröhlich, Armin Biere. Quantifier-Free Bit-Vector Formulas with Binary Encoding: Benchmark Description. In Proceedings of SAT Competition 2013, Adrian Balint, Anton Belov, Marijn Heule, Matti Järvisalo (editors), vol. B-2013-1 of Department of Computer Science Series of Publications B, pages 107-108 , University of Helsinki, 2013.

Jean-Marie Lagniez, Armin Biere. Factoring Out Assumptions to Speed Up MUS Extraction. In Proc. 16th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'13), Lecture Notes in Computer Science (LNCS) vol. 7962, pages 276-292, Springer 2013.

Gergely Kovásznai, Andreas Fröhlich, Armin Biere. BV2EPR: A Tool for Polynomially Translating Quantifier-free Bit-Vector Formulas into EPR. In Proc. 24th Intl. Conf.  on Automated Deduction (CADE'13), Lecture Notes in Computer Science (LNCS) vol. 7898, pages 443-449, Springer 2013.

Andreas Fröhlich, Gergely Kovásznai, Armin Biere. More on the Complexity of Quantifier-Free Fixed-Size Bit-Vector Logics with Binary Encoding. In Proc. 8th Intl. Computer Science Symp. in Russia (CSR'13), Lecture Notes in Computer Science (LNCS) vol. 7913, pages 378-390, Springer 2013 (with appendix).

Cyrille Artho, Armin Biere, Martina Seidl. Model-Based Testing for Verification Backends. In Proc. 7th Intl. Conf. on Tests & Proofs (TAP'13), Lecture Notes in Computer Science (LNCS) vol. 7942, pages 39-55, Springer 2013.

Marijn Heule, Matti Järvisalo, Armin Biere. Revisiting Hyper Binary Resolution. In Proc. 10th Intl. Conf. on Integration of Artificial Intelligence and Operations Research Techniques in Constraint Programming (CPAIOR'13), Lecture Notes in Computer Science (LNCS) vol. 7874, pages 77-93, Springer 2013.

Alexandra Goultiaeva, Martina Seidl, Armin Biere. Bridging the Gap between Dual Propagation and CNF-based QBF Solving. In Proc. Intl. Conf. on Design, Automation & Test in Europe (DATE'13), pages 811-814, 2013.

Robert Aistleitner. An Evaluation of Bit-Parallelization applied to Failed Literal Probing. Masterarbeit, Informatik, Johannes Kepler University, Linz, 2013.

2012

Florian Lonsing. Dependency Schemes and Search-Based QBF Solving: Theory and Practice. Dissertation Technische Wissenschaften, Informatik, Johannes Kepler University, Linz, 2012.
[ thesis | bibtex ]

Armin Biere. Boolector Entering the SMT Competition 2012. Technical Report 12/1, June 2012, FMV Reports Series, Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr. 69, 4040 Linz, Austria.
[ report | bibtex | boolector ]

Cyrille Artho, Armin Biere, Masami Hagiya, Richard Potter, Rudolf Ramler, Yoshinori Tanabe, Franz Weitl, Mitusharu Yamamoto. Modbat: A model-based API tester for event-driven systems. Short paper (tool demo) at the Dependable Systems Workshop 2012, 2 pages, Kobe, Japan, December 2012.

Norbert Manthey, Marijn Heule, Armin Biere. Automated Reencoding of Boolean Formulas. In Proc. Haifa Verification Conference (HVC'12), Lecture Notes in Computer Science (LNCS) vol. 7857, pages 102-117, Springer 2013.

Magdalena Widl, Armin Biere, Petra Brosch, Uwe Egly, Marijn Heule, Gerti Kappel, Martina Seidl, Hans Tompits. Guided Merging of Sequence Diagrams. In revised selected papers of 5th Intl. Conf.  on Software Language Engineering (SLE'12), Lecture Notes in Computer Science (LNCS) vol. 7745 pages 164-183, Springer 2012.

Matti Järvisalo, Armin Biere, Marijn Heule. Simulating Circuit-Level Simplifications on CNF. Journal of Automated Reasoning, 49(4), pages 583-619, Springer 2012.

Alexander Nöhrer, Armin Biere, Alexander Egyed. A comparison of strategies for tolerating inconsistencies during decision-making. In Proc. 16th Intl. Software Product Line Conf. (SPLC'12), pages 11-20, ACM, 2012.

Gergely Kovásznai, Andreas Fröhlich, Armin Biere. On the Complexity of Fixed-Size Bit-Vector Logics with Binary Encoded Bit-Width. In Proc. 10th Intl. Workshop on Satisfiability Modulo Theories (SMT'12), EPiC Series in Computing, vol. 20, pages 44-56, EasyChair 2013.

Martina Seidl, Florian Lonsing, Armin Biere. QBF2EPR: A Tool for Generating EPR Formulas from QBF In Proc. 3rd Intl. Workshop. on Practical Aspects of Automated Reasoning (PAAR'12), EPiC Series in Computing, vol. 21, pages 139-148, EasyChair 2013.

Vladimir Klebanov, Bernhard Beckert, Armin Biere, Geoff Sutcliffe (editors), Proc. 1st Intl. Work. on Comparative Empirical Evaluation of Reasoning Systems (COMPARE'12), vol. 873, CEUR Workshop Proceedings.

Armin Biere. Boolector Entering the SMT Competition 2012. Technical Report 12/1, June 2012, FMV Reports Series, Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr. 69, 4040 Linz, Austria.
[ report | bibtex | boolector ]

Armin Biere. Lingeling and Friends Entering the SAT Challenge 2012. In Proc.  of SAT Challenge 2012: Solver and Benchmark Descriptions, Adrian Balint, Anton Belov, Daniel Diepold, Simon Gerber, Matti Järvisalo, and Carsten Sinz (editors), vol. B-2012-2 of Department of Computer Science Series of Publications B, pages 33-34, University of Helsinki, 2012.

Peter van der Tak, Marijn Heule, and Armin Biere. Concurrent Cube-and-Conquer. In Proc.  of SAT Challenge 2012: Solver and Benchmark Descriptions, Adrian Balint, Anton Belov, Daniel Diepold, Simon Gerber, Matti Järvisalo, and Carsten Sinz (editors), vol. B-2012-2 of Department of Computer Science Series of Publications B, pages 15-16, University of Helsinki, 2012.

Aina Niemetz, Mathias Preiner, Florian Lonsing, Martina Seidl, Armin Biere. Resolution-Based Certificate Extraction for QBF (Tool Presentation). In Proc. 15th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'12), Lecture Notes in Computer Science (LNCS) vol. 7317, pages 430-435, Springer 2012.
[ paper | bibtex | qbfcert ]

Peter van der Tak, Marijn Heule, Armin Biere. Concurrent Cube-and-Conquer (Poster Presentation). In Proc. 15th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'12), Lecture Notes in Computer Science (LNCS) vol. 7317, pages 475-476, Springer 2012.

Andreas Fröhlich, Gergely Kovásznai, Armin Biere. A DPLL Algorithm for Solving DQBF. In Proc. Intl. Workshop on Pragmatics of SAT (POS'12), aff. to SAT'12, Trento, Italy, 2012.

Peter van der Tak, Marijn Heule, Armin Biere. Concurrent Cube-and-Conquer. In Proc. Intl. Workshop on Pragmatics of SAT (POS'12), aff. to SAT'12, Trento, Italy, 2012.

Matti Järvisalo, Marijn Heule, Armin Biere. Inprocessing Rules. In Bernhard Gramlich, Dale Miller, and Uli Sattler (editors), Proc. 6th Intl. Joint Conf. on Automated Reasoning (IJCAR'12), Lecture Notes in Computer Science (LNCS), vol. 7364, pages 355-370, Springer 2012.

Alexander Nöhrer, Armin Biere, Alexander Egyed. Managing SAT Inconsistencies with HUMUS. In Proc. 6th Intl. Workshop on Variability Modelling of Software-Intensive Systems (VaMoS'12), pages 83-91, ACM 2012.

N. Creignou, U. Egly, M. Seidl: A Framework for the Specification of Random SAT and QSAT Formulas. Proc. of the 6th International Conference on Tests and Proofs (TAP 2012), Lecture Notes in Computer Science (LNCS), Springer, 6 pages, 2012

P. Brosch, U. Egly, S. Gabmeyer, G. Kappel, M. Seidl, H. Tompits, M. Widl, M. Wimmer: Towards Scenario-Based Testing of UML Diagrams, Proc. of the 6th International Conference on Tests and Proofs (TAP 2012), Lecture Notes in Computer Science (LNCS), Springer, 6 pages, 2012

Aina Niemetz. Extracting and Checking Q-Resolution Proofs from a State-Of-The-Art QBF-Solver. Masterarbeit, Informatik, Johannes Kepler University, Linz, 2012.

Mathias Preiner. Extracting and Validating Skolem/Herbrand Function-Based QBF Certificates. Masterarbeit, Informatik, Johannes Kepler University, Linz, 2012.

2011

Best paper
Marijn Heule, Oliver Kullmann, Siert Wieringa, Armin Biere. Cube and Conquer: Guiding CDCL SAT Solvers by Lookaheads. In Proc. 7th Intl. Haifa Verification Conference (HVC'11), Lecture Notes in Computer Science (LNCS) vol. 7261, pages 50-65, Springer 2012 (software).

Malay Ganai, Armin Biere (editors). Proc. 1st Intl. Workshop on Design and Implementation of Formal Tools and Systems (DIFTS'11), vol. 832, CEUR Workshop Proceedings. Aff. workshop to FMCAD'2011, Austin, Texas, USA, Nov. 2011.

Armin Biere, Karen Yorav. Preface Special Issue on Hardware Verification Workshop (HWVW'10). Formal Methods in System Design, vol. 39, number 2, pages 115-116, Springer 2011.

Armin Biere, Florian Lonsing, Martina Seidl. Blocked Clause Elimination for QBF. In Proc. 23rd Intl. Conf. on Automated Deduction (CADE'11), Lecture Notes in Computer Science (LNCS) vol. 6803, pages 101-115, Springer 2011.

Armin Biere, Keijo Heljanko, Siert Wieringa. AIGER 1.9 And Beyond, Technical Report 11/2, July 2011, FMV Reports Series, Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr. 69, 4040 Linz, Austria.
[ report | bibtex | aiger ]

Marijn Heule, Matti Järvisalo, Armin Biere. Efficient CNF Simplification Based on Binary Implication Graphs. In Proc. 14th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'11), Lecture Notes in Computer Science (LNCS) vol. 6695, pages 201-215, Springer 2011.

Florian Lonsing, Armin Biere. Failed Literal Detection for QBF. In Proc. 14th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'11), Lecture Notes in Computer Science (LNCS) vol. 6695, pages 259-272, Springer 2011.

Armin Biere. Lingeling and Friends at the SAT Competition 2011. Technical Report 11/1, March 2011, FMV Reports Series, Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr. 69, 4040 Linz, Austria.
[ report | bibtex ]

Armin Biere, Keijo Heljanko, Siert Wieringa. AIGER 1.9 And Beyond, Technical Report 11/2, July 2011, FMV Reports Series, Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr. 69, 4040 Linz, Austria.
[ report | bibtex | aiger ]

Armin Biere. Lingeling and Friends at the SAT Competition 2011. Technical Report 11/1, March 2011, FMV Reports Series, Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr. 69, 4040 Linz, Austria.
[ report | bibtex ]

2010

Marijn Heule, Matti Järvisalo, Armin Biere. Covered Clause Elimination. In Short Paper Proc. 17th Intl. Conf. on Logic for Programming, Artificial Intelligence and Reasoning 2010 (LPAR-17), EPiC Series in Computing, vol. 13, pages 41-46, EasyChair 2013.

Marijn Heule, Matti Järvisalo, Armin Biere. Clause Elimination Procedures for CNF Formulas. In Proc. 17th Intl. Conf. on Logic for Programming, Artificial Intelligence and Reasoning 2010 (LPAR-17), Lecture Notes in Computer Science (LNCS) vol. 6397, pages 357–371, Springer 2010.

Armin Biere. Lingeling, Plingeling, PicoSAT and PrecoSAT at SAT Race 2010. Technical Report 10/1, August 2010, FMV Reports Series, Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr. 69, 4040 Linz, Austria.

Florian Lonsing, Armin Biere. Integrating Dependency Schemes in Search-Based QBF Solvers. In Proc. 13th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'10), Lecture Notes in Computer Science (LNCS) vol. 6175, pages 158-171, Springer 2010. (ERRATA).

Matti Järvisalo, Armin Biere. Reconstructing Solutions after Blocked Clause Elimination. In Proc. 13th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'10), Lecture Notes in Computer Science (LNCS) vol. 6175, pages 340-345, Springer 2010.

Robert Brummayer, Florian Lonsing, Armin Biere. Automated Testing and Debugging of SAT and QBF Solvers. In Proc. 13th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'10), Lecture Notes in Computer Science (LNCS) vol. 6175, pages 44-57, Springer 2010. [ paper | bibtex | qbfuzz | qbfdd ]

Florian Lonsing, Armin Biere. DepQBF: A Dependency-Aware QBF Solver (System Description). Journal on Satisfiability, Boolean Modeling and Computation (JSAT), vol. 7, 2010, pages 71-76.. Preliminary version appeared in Proc. 1st Intl. Work. on Pragmatics of SAT (POS'10).

Matti Järvisalo, Armin Biere, Marijn Heule. Blocked Clause Elimination. In Proc. 16th Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'10), Lecture Notes in Computer Science (LNCS), vol. 6015, pages 129-144, Springer 2010.

Armin Biere. Lingeling, Plingeling, PicoSAT and PrecoSAT at SAT Race 2010. Technical Report 10/1, August 2010, FMV Reports Series, Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr. 69, 4040 Linz, Austria.

R. Brummayer, M. Järvisalo. Testing and Debugging Techniques for Answer Set Solver Development. In Proc. Intl. Conf. on Logic Programming (ICLP'10), published in Theory and Practice of Logic Programming vol. 10(4-6), pages 741-758, 2010.

R. Brummayer, D. Oe, A. Stump. Exploring Predictability of SAT/SMT Solvers. Intl. Workshop on Evaluation Methods for Solvers and Quality Metrics for Solutions (EMSQMS'10), affiliated to IJCAR'10 and CAV'10 at FLOC'10.

2009

Robert Brummayer. Efficient SMT Solving for Bit-Vectors and the Extensional Theory of Arrays Dissertation Technische Wissenschaften, Informatik, Johannes Kepler University, Linz, 2009.
[ thesis | bibtex ]

Armin Biere, Carl Pixley (editors). Proceedings 9th Intl. Conf. on Formal Methods in Computer Aided Design (FMCAD'09), IEEE 2009.

Robert Brummayer, Armin Biere. Fuzzing and Delta-Debugging SMT Solvers. In Proc. 7th Intl. Workshop on Satisfiability Modulo Theories (SMT'09), 5 pages, ACM 2009.

Niklas Sörensson, Armin Biere. Minimizing Learned Clauses. In Proc. 12th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'09), Lecture Notes in Computer Science (LNCS) vol. 5584, pages 237-243, Springer 2009.

Florian Lonsing, Armin Biere. A Compact Representation for Syntactic Dependencies in QBFs. In Proc. 12th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'09), Lecture Notes in Computer Science (LNCS) vol. 5584, pages 398-411, Springer 2009.

Robert Brummayer, Armin Biere. Lemmas on Demand for the Extensional Theory of Arrays. Journal on Satisfiability, Boolean Modeling and Computation (JSAT), vol. 6, pages 165-201, Delft University, 2009.
[ paper | bibtex | boolector ]

Robert Brummayer, Armin Biere. Boolector: An Efficient SMT Solver for Bit-Vectors and Arrays. In Proc. 15th Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'09), Lecture Notes in Computer Science (LNCS), vol. 5505, pages 174-177, Springer 2009.
[ paper | bibtex | boolector ]

Armin Biere. P{re,i}coSAT@SC'09. Solver description for SAT Competition 2009. In SAT 2009 Competitive Event Booklet, 2009.

Robert Brummayer, Armin Biere. Effective Bit-Width and Under-Approximation. In Proc. 12th Intl. Conference on Computer Aided Systems Theory (EUROCAST'09), Lecture Notes in Computer Science (LNCS) vol. 5717, pages 304-311 Springer 2009.

Armin Biere. Bounded Model Checking. In Handbook of Satisfiability. IOS Press, February 2009, pages 455-481. See also this link.

Armin Biere, Marijn Heule, Hans Van Maaren and Toby Walsh (editors). Handbook of Satisfiability. IOS Press, February 2009.

Jürgen Holzleitner. Using feedback to improve black box fuzz testing of SAT solvers. Masterarbeit, Informatik, Johannes Kepler University, Linz, 2009.

Jakob Zwirchmayr, SmacC: A Satisfiability Modulo Theories Memory-Model and Assertion Checker for C. Masterarbeit, Informatik, Johannes Kepler University, Linz, 2009.

Stefan Riha. Memory leak detection and diagnosis in .Net and Java applications using run-time memory dumps. Masterarbeit, Informatik, Johannes Kepler University, Linz, 2009.

2008

Armin Biere, Robert Brummayer. Consistency Checking of All Different Constraints over Bit-Vectors within a SAT-Solver. In Proc. 8th Intl. Conf. on Formal Methods in Computer-Aided Design (FMCAD'08), IEEE 2008.

Florian Lonsing, Armin Biere. Efficiently Representing Existential Dependency Sets for Expansion-based QBF Solvers. In Selected Papers of Proc. 4th Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'08), Znojmo, Czech Republic, November 2008. Appeared in ENTCS, vol. 251, pages 83-95, Elsevier 2009. (DOI) (Preprint) (Preliminary version)

Armin Biere. Tutorial on Model Checking, Modelling and Verification in Computer Science. In Proc. 3rd Intl. Conf. on Algebraic Biology (AB'08), Lecture Notes in Computer Science (LNCS), vol. 5147, Springer 2008.

Robert Brummayer, Armin Biere, Florian Lonsing. BTOR: Bit-Precise Modelling of Word-Level Problems for Model Checking. In Proc. 1st Intl. Workshop on Bit-Precise Reasoning (BPR'08), Princeton, New Jersey, USA, July 2008.
[ paper | bibtex ]

Robert Brummayer, Armin Biere. Lemmas on Demand for the Extensional Theory of Arrays. In Proc. 6th Intl. Workshop on Satisfiability Modulo Theories (SMT'08), Princeton, New Jersey, USA, July 2008.
[ paper | bibtex | boolector ]

Armin Biere. PicoSAT Essentials. Journal on Satisfiability, Boolean Modeling and Computation (JSAT), vol. 4, pages 75-97, Delft University, 2008.

Florian Lonsing, Armin Biere. Nenofex: Expanding NNF for QBF Solving. In Proc. 11th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'08), Lecture Notes in Computer Science (LNCS) vol. 4996, Springer 2008.

Armin Biere. Adaptive Restart Control for Conflict Driven SAT Solvers. In Proc. 11th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'08), Lecture Notes in Computer Science (LNCS) vol. 4996, Springer 2008.

Armin Biere, Daniel Kröning, Georg Weissenbacher, Christoph Wintersteiger. Digitaltechnik - Eine praxisnahe Einführung. Springer 2008.

Andreas Vida. Random Test Case Generation and Delta Debugging for BitVector Logic with Arrays. Masterarbeit, Informatik, Johannes Kepler University, Linz, 2009.

2007

Armin Biere. The AIGER And-Inverter Graph (AIG) Format Version 20071012. Technical Report 07/1, October 2011, FMV Reports Series, Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr. 69, 4040 Linz, Austria.
[ report | bibtex | aiger ]

Robert Brummayer, Armin Biere. C32SAT: Checking C Expressions. In Proc. 19th Intl. Conf. on Computer Aided Verification (CAV'07), Lecture Notes in Computer Science (LNCS), vol. 4590, Springer 2007.

Toni Jussila, Armin Biere, Carsten Sinz, Daniel Kröning, Christoph Wintersteiger. A First Step Towards a Unified Proof Checker for QBF. In Proc. 10th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'07), Lecture Notes in Computer Science (LNCS) vol. 4501, Springer 2007.

Cyrille Artho, Boris Zweimüller, Armin Biere, Etsuya Shibayama, Shinichi Honiden. Efficient Model Checking of Applications with Input/Output. In Proc. Computer Aided Systems Theory (EUROCAST'07), Lecture Notes in Computer Science (LNCS) vol. 4739, Springer 2007.

Florian Lonsing. An Expansion-based QBF Solver For Negation Normal Form. Magisterarbeit, Informatik, Johannes Kepler University, Linz, 2007.

2006

Armin Biere, Keijo Heljanko, Tommi Junttila, Timo Latvala, Viktor Schuppan. Linear Encodings of Bounded LTL Model Checking. Logical Methods in Computer Science, vol. 2, issue 5:5, 2006, 10.2168/LMCS-2(5:5)2006.

Robert Brummayer, Armin Biere. Local Two-Level And-Inverter Graph Minimization without Blowup. In Proc. 2nd Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'06), Mikulov, Czechia, October 2006.

Ofer Strichman, Armin Biere (editors). Proc. 4th Intl. Workshop on Bounded Model Checking (BMC'06), Electronic Notes in Theoretical Computer Science (ENTCS), vol. 174, issue 3, Elsevier 2007.

Toni Jussila, Armin Biere. Compressing BMC Encodings with QBF. In Proc. 4th Intl. Workshop on Bounded Model Checking (BMC'06), to be published in Electronic Notes in Theoretical Computer Science (ENTCS), Seattle, USA, August 2006.

Armin Biere, Carla Gomes (editors). Proc. 9th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'06), Lecture Notes in Computer Science (LNCS), vol. 4121, Springer 2006, 10.1007/11814948.

Toni Jussila, Carsten Sinz, Armin Biere. Extended Resolution Proofs for Symbolic SAT Solving with Quantification. In Proc. 9th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'06), Lecture Notes in Computer Science (LNCS), vol. 4121, Springer 2006.

Cyrille Artho, Armin Biere, Shinichi Honiden. Enforcer - Efficient Failure Injection. In Proc. Formal Methods (FM'06), Lecture Notes in Computer Science (LNCS), vol. 4085, Springer 2006, 10.1007/11813040_28.

Cyrille Artho, Armin Biere, Shinichi Honiden, Viktor Schuppan, Pascal Eugster, Marcel Baur, Boris Zweimüller, Peter Farkas. Advanced Unit Testing - How to Scale Up a Unit Test Framework. In Proc. Workshop on Automation of Software Test (AST'06), Shanghai, China, May 2006.

Carsten Sinz, Armin Biere. Extended Resolution Proofs for Conjoining BDDs. In Proc. 1st Intl. Computer Science Symp. in Russia (CSR 2006), St. Petersburg, Russia, Lecture Notes in Computer Science (LNCS), vol. 3967, Springer 2006.

Armin Biere, Carsten Sinz. Decomposing SAT Problems into Connected Components. Journal on Satisfiability, Boolean Modeling and Computation (JSAT), vol. 2, Delft University, 2006.

Armin Biere. (Q)CompSAT and (Q)PicoSAT at the SAT’06 Race. SAT Race 2006 Solver Description, 2006.

Robert Brummayer. C32SAT: A satisfiability checker for C expressions. Magisterarbeit, Informatik, Johannes Kepler University, Linz, 2006.

T. Jussila, J. Dubrovin, T. Junttila, T. Latvala, I. Porres Model Checking Dynamic and Hierarchical UML State Machines In Proc. 3rd International Workshop on Model Development, Validation and Verification (MoDeV2a) pages, 94-110, Genova, Italy, October 2006.

2005

Publications in Formal Methods in 2005

Viktor Schuppan, Armin Biere. Liveness Checking as Safety Checking for Infinite State Spaces. Proc. 7th Intl. Workshop on Verification of Infinite-State Systems (INFINITY'05), Electronic Notes in Theoretical Computer Science (ENTCS), vol. 149, issue 1, Elsevier 2006.

Armin Biere, O. Strichman (editors). Proc. 3rd Intl. Workshop on Bounded Model Checking (BMC'05). Electronic Notes in Theoretical Computer Science (ENTCS), vol. 144, issue 1, Elsevier 2006.

Niklas Eén, Armin Biere. Effective Preprocessing in SAT through Variable and Clause Elimination. In Proc. 8th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'05), Lecture Notes in Computer Science (LNCS), vol. 3569, Springer 2005, 10.1007/11499107_5.

Malek Haroud, Armin Biere. SDL versus C Equivalence Checking. In Proc. 12th SDL Forum (SDL'05), Lecture Notes in Computer Science (LNCS), vol. 3530, Springer 2005.

Cyrille Artho, Armin Biere. Subroutine Inlining and Bytecode Abstraction to Simplify Static and Dynamic Analysis. In Proc. 1st Workshop on Bytecode Semantics, Verification, Analysis and Transformation (BYTECODE'05), Edinburgh, Scotland, UK, April 2005, Electronic Notes in Theoretical Computer Science (ENTCS), vol. 141, issue 1, Elsevier 2006.

Viktor Schuppan, Armin Biere. Shortest Counterexamples for Symbolic Model Checking of LTL with Past. In Proc. 11th Intl. Conf. on Tools and Algorithms for the Analysis and Construction of Systems (TACAS'05), Lecture Notes in Computer Science (LNCS), vol. 3440, Springer 2005, ext. version available as ETH Technical Report 470.

Mukul Prasad, Armin Biere, Aarti Gupta. A Survey of Recent Advances in SAT-based Formal Verification, Intl. Journal on Software Tools for Technology Transfer (STTT), vol. 7, number 2, Springer 2005.

Viktor Schuppan, Armin Biere. Shortest Counterexamples for Symbolic Model Checking of LTL with Past. Technical Report 470, Dept. of Computer Science, ETH Zürich, 2005, full version of our TACAS'05 paper.

Cyrille Artho, Armin Biere. Combined Static and Dynamic Analysis. Technical Report 466, Dept. of Computer Science, ETH Zürich, 2005, full version of our AIOOL'05 paper.

Cyrille Artho, Armin Biere. Combined Static and Dynamic Analysis. In Proc. 1st Intl. Workshop on Abstract Interpretation of Object-Oriented Languages (AIOOL'05), Paris, France, Jan. 2005, ext. version available as ETH Technical Report 466.

Timo Latvala, Armin Biere, Keijo Heljanko, Tommi Junttila. Simple is Better: Efficient Bounded Model Checking for Past LTL. In Proc. 6th Intl. Conf. on Verification, Model Checking and Abstract Interpretation (VMCAI'05), Paris, France, Jan. 2005, Lecture Notes in Computer Science (LNCS), vol. 3385, Springer 2005.

C. Sinz. Towards an optimal CNF encoding of Boolean cardinality constraints. In Proc. 11th Intl. Conf. on Principles and Practice of Constraint Programming (CP 2005), pages 827-831, Sitges, Spain, October 2005. Lecture Notes in Computer Science (LNCS), vol. 3709, Springer 2005.

Publications in Heuristic Optimization in 2005

M. Affenzeller, S. Wagner. Enhanced Genetic Algorithms Inspired by Population Genetics. To be published in: Intl. Journal of Systems Science. Taylor & Francis, 2005.

S. Winkler, H. Efendic, M. Affenzeller, L. Del Re, S. Wagner. On-Line Modeling Based on Genetic Programming. Accepted to be published in: Special Issue of the Intl. Journal of Intelligent Systems Technologies and Applications (IJISTA). 2005.

S. Winkler, M. Affenzeller, S. Wagner. A Genetic Programming Based Tool for Supporting Bioinformatical Classification Problems. Accepted to be published in: Proc. of FH Science Day Steyr. 2005.

S. Winkler, M. Affenzeller, S. Wagner. Genetic Programming Based Model Structure Identification Using On-Line System Data. Accepted to be published in: Proc. of Conceptual Modeling and Simulation Conf. (CMS'05). 2005.

M. Affenzeller. Population Genetics and Evolutionary Computation: Theoretical and Practical Aspects. Schriften der Johannes Kepler Universität Linz, Reihe C: Technik und Naturwissenschaften. Universitätsverlag Rudolf Trauner, 2005. ISBN 3-85487-823-0.

S. Wagner, M. Affenzeller. The Allele Meta-Model - Developing a Common Language for Genetic Algorithm. In Proc. 1st Intl. Work-Conf. on the Interplay between Natural and Artificial Computation (IWINAC'05), 2005.

M. Affenzeller, S. Wagner, S. Winkler. GA-Selection Revisited from an ES-Driven Point of View. In Proc. 1st Intl. Work-Conf. on the Interplay between Natural and Artificial Computation (IWINAC'05), 2005.

M. Affenzeller, S. Wagner, S. Winkler. Goal-Oriented Preservation of Essential Genetic Information by Offspring Selection. In Proc. Genetic and Evolutionary Computation Conf. (GECCO'05), 2005.

R. Braune, S. Wagner, M. Affenzeller. On the Analysis of Crossover Schemes for Genetic Algorithms Applied to the Job Shop Scheduling Problem. In Proc. 9th World Multi-Conference on Systemics, Cybernetics and Informatics (WMSCI'05), 2005.

S. Winkler, M. Affenzeller, S. Wagner. Solving Multiclass Classification Problems by Genetic Programming. In Proc. 9th World Multi-Conference on Systemics, Cybernetics and Informatics (WMSCI'05), 2005.

S. Wagner, M. Affenzeller. SexualGA: Gender-Specifc Selection for Genetic Algorithms. In Proc. 9th World Multi-Conference on Systemics, Cybernetics and Informatics (WMSCI'05), 2005.

M. Affenzeller, S. Winkler, S. Wagner. A New Genetic-Programming-Based Machine Learning Algorithm. In Proc. 9th World Multi-Conference on Systemics, Cybernetics and Informatics (WMSCI'05), 2005.

L. del Re, P. Langthaler, C. Furtmüller, S. Winkler, M. Affenzeller. NOx Virtual Sensor Based on Structure Identification and Global Optimization. In Proc. SAE World Congress (SAE'05), paper number 1005-01-0050, 2005.

M. Affenzeller, S. Wagner. Offspring Selection: A New Self-Adaptive Selection Scheme for Genetic Algorithms. In Proc. of the Intl. Conf. on Adaptive and Natural Computing Algorithms (ICANNGA'05), Springer Computer Science, Springer 2005.

S. Wagner, M. Affenzeller. HeuristicLab: A Generic and Extensible Optimization Environment. In Proc. of the Intl. Conf. on Adaptive and Natural Computing Algorithms (ICANNGA'05), Springer Computer Science, Springer 2005.

2004

Publications in Formal Methods in 2004

Cyrille Artho, Klaus Havelund, Armin Biere. Using Block-local Atomicity to Detect Stale-value Concurrency Errors. In Proc. 2nd Intl. Symp. on Automated Technology for Verification and Analysis (ATVA'04), Taipei, Nov. 2004, Lecture Notes in Computer Science (LNCS), vol. 3299, Springer 2004.

Timo Latvala, Armin Biere, Keijo Heljanko, Tommi Junttila. Simple Bounded LTL Model Checking. In Proc. Formal Methods in Computer-Aided Design (FMCAD'04), Austin Texas, Nov. 2004, Lecture Notes in Computer Science (LNCS), vol. 3312, Springer 2004.

Malek Haroud, Ljubica Blažević, Armin Biere. HW accelerated ultra wide band MAC protocol using SDL and SystemC. In Proc. IEEE Radio and Wireless Conference (RAWCON'04), IEEE, Sept. 2004.

Timo Latvala, Armin Biere, Keijo Heljanko, Tommi Junttila. Simple bounded LTL model checking. Research Report A92, Helsinki University of Technology, Laboratory for Theoretical Computer Science, Espoo, Finland, July 2004.

Armin Biere, Ofer Strichman (editors). Proc. 2nd Intl. Workshop on Bounded Model Checking (BMC'04). Electronic Notes in Theoretical Computer Science (ENTCS), vol. 119, issue 2, Elsevier 2005.

Cyrille Artho, Viktor Schuppan, Armin Biere, Pascal Eugster, Marcel Baur, Boris Zweimüller. JNuke: Efficient Dynamic Analysis for Java. In Proc. 16th Intl. Conf. on Computer-Aided Verification (CAV'04), Lecture Notes in Computer Science (LNCS), vol. 3114, Springer 2004.

Armin Biere. Resolve and Expand. In Proc. 7th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'04), Lecture Notes in Computer Science (LNCS), vol. 3542, Springer 2005, 10.1007/11527695_5.

Armin Biere. The Evolution from Limmat to Nanosat. Technical Report 444, Dept. of Computer Science, ETH Zürich 2004.

Viktor Schuppan, Marcel Baur, Armin Biere. VM Independent Replay in Java. In Proc. 4th Intl. Workshop on Runtime Verification (RV'04), Electronic Notes in Theoretical Computer Science (ENTCS), vol. 113, Elsevier 2005.

Viktor Schuppan, Armin Biere. Efficient reduction of finite state model checking to reachability analysis. Intl. Journal on Software Tools for Technology Transfer (STTT), vol. 5, number 2-3, Springer 2004.

Publications in Heuristic Optimization in 2004

S. Wagner, M. Affenzeller HeuristicLab Grid - A Flexible and Extensible Environment for Parallel Heuristic Optimization. Journal of Systems Science, vol. 30, number 4, Oficyna Wydawnicza Politechniki Wroclawskiej, 2004.

M. Affenzeller, S. Wagner. The Influence of Population Genetics for the Redesign of Genetic Algorithms. Journal of Systems Science, vol. 30, number 4, Oficyna Wydawnicza Politechniki Wroclawskiej, 2004.

M. Affenzeller, S. Wagner. SASEGASA: A New Generic Parallel Evolutionary Algorithm for Achieving Highest Quality Results. Journal of Heuristics - Special Issue on New Advances on Parallel Meta-Heuristics for Complex Problems, vol. 10, pp. 239-263, Kluwer Academic Publishers, 2004.

M. Affenzeller, S. Wagner. Reconsidering the Selection Concept of Genetic Algorithms from a Population Genetics Inspired Point of View. Cybernetics and Systems 2004, pp. 701-706. Austrian Society for Cybernetic Studies, 2004.

S. Wagner, M. Affenzeller, D. Schragl. Traps and Dangers when Modelling Problems for Genetic Algorithms. Cybernetics and Systems 2004, pp. 79-84. Austrian Society for Cybernetic Studies, 2004.

R. Braune, S. Wagner, M. Affenzeller. Applying Genetic Algorithms to the Optimization of Production Planning in a Real-World Manufacturing Environment. Cybernetics and Systems 2004, pp. 41-46. Austrian Society for Cybernetic Studies, 2004.

S. Winkler, M. Affenzeller, S. Wagner. Identifying Nonlinear Model Structures Using Genetic Programming Techniques. Cybernetics and Systems 2004, pp. 689-694. Austrian Society for Cybernetic Studies, 2004.

M. Affenzeller, S. Wagner. The Influence of Population Genetics for the Redesign of Genetic Algorithms. Proc. of the 15th Intl. Conf. on Systems Science, vol. 3, pp. 53-60. Oficyna Wydawnicza Politechniki Wroclawskiej, 2004.

S. Wagner, M. Affenzeller. HeuristicLab Grid - A Flexible and Extensible Environment for Parallel Heuristic Optimization. Proc. of the 15th Intl. Conf. on Systems Science, vol. 1, pp. 289-296. Oficyna Wydawnicza Politechniki Wroclawskiej, 2004.

S. Winkler, M. Affenzeller, S. Wagner. New Methods for the Identification of Nonlinear Model Structures Based Upon Genetic Programming Techniques. Proc. of the 15th Intl. Conf. on Systems Science, vol. 1, pp. 386-393. Oficyna Wydawnicza Politechniki Wroclawskiej, 2004.

G. Weichhart, M. Affenzeller, A. Reitbauer, S. Wagner. (Modelling of an Agent-Based Schedule Optimisation System. Accepted to be published in: Proc. of the IMS Intl. Forum 2004, 2004.

S. Wagner, M. Affenzeller. The HeuristicLab Optimization Environment. Technical Report. Institute of Formal Models and Verification, Johannes Kepler University Linz, Austria, 2004.