team |
[ 21 | 20 | 19 | 18 | 17 | 16 | 15 | 14 | 13 | 12 | 11 | 10 | 09 | 08 | 07 | 06 | 05 | 04 | 03 | 02 | 01 | 00 | 99 | 98 | 97 | 93 ] Publications Armin Biere[ DBLP | Google Scholar | Semantic Scholar | ORCID | Scopus | JKU FoDok ] [ JKU in Google Scholar | FMV in JKU FoDok ] 2021Nils Froleyks and Armin Biere. Single Clause
Assumption without Activation Literals to Speed-up IC3. In
Proc. 21st Intl. Conf. on Formal Methods in
Computer-Aided Design (FMCAD'21), pages 72-76, vol. 2, TU
Vienna Academic Press 2021. Cunjing Ge and Armin Biere. Decomposition
Strategies to Count Integer Solutions over Linear Constraints.
In Proc. 30th Intl. Joint Conf. on Artificial
Intelligence (IJCAI'21), pages 1389-1395, ijcai.org 2021. Armin Biere, Matti Järvisalo and Benjamin Kiesl. Preprocessing in
SAT Solving, Chapter 9 of
Handbook of Satisfiability (2nd ed.), vol. 336,
Frontiers in Artificial Intelligence and Applications, pages
391-435, IOS Press 2021. Armin Biere. Bounded Model
Checking, Chapter 18 of
Handbook of Satisfiability (2nd ed.), vol. 336,
Frontiers in Artificial Intelligence and Applications, pages
739-764, IOS Press 2021. Daniela Kaufmann and Armin Biere. AMulet 2.0
for Verifying Multiplier Circuits. In Proc. 14th
Intl. Conference on Tools and Algorithms for the Construction
and Analysis of Systems (TACAS), vol. 12652, pages
357-364, Lecture Notes
in Computer Science (LNCS) Springer 2021. Armin Biere, Mathias Fleury and Maximillian Heisinger.
CaDiCaL, Kissat, Paracooba Entering the SAT Competition 2021.
In Proc. of SAT Competition 2021 - Solver and Benchmark
Descriptions, Tomas Balyo, Nils Froleyks, Marijn Heule, Markus
Iser, Matti Järvisalo, Martin Suda (editors), vol. B-2021-1 of
Department of Computer Science Report Series B, pages 10-13,
University of Helsinki, 2021. Armin Biere.
CNF Encodings of Complete Pairwise Combinatorial Testing of our SAT
Solver Satch. In Proc. of SAT Competition 2021 - Solver
and Benchmark Descriptions, Tomas Balyo, Nils Froleyks, Marijn
Heule, Markus Iser, Matti Järvisalo, Martin Suda (editors),
vol. B-2021-1 of Department of Computer Science Report Series
B, 2021. page 46, University of Helsinki, 2021. Muhammad Osama, Anton Wijs and Armin Biere. SAT Solving
with GPU Accelerated Inprocessing. In Proc. 14th
Intl. Conference on Tools and Algorithms for the Construction
and Analysis of Systems (TACAS), vol. 12651, pages
131-151, Lecture Notes
in Computer Science (LNCS) Mathias Fleury and Armin Biere. Efficient
All-UIP Learned Clause Minimization. In Proc. 24rd
Intl. Conf. on Theory and Applications of Satisfiability
Testing (SAT'21), pages 171-187, volume 12831, Lecture Notes in Computer
Science (LNCS) Springer 2021. Wojciech Nawrocki, Zhenjun Liu, Andreas Fröhlich, Marijn J.H.
Heule and Armin Biere.
XOR Local Search for Boolean Brent Equations. In
Proc. 24rd Intl. Conf. on Theory and Applications
of Satisfiability Testing (SAT'21), pages 417-435, volume
12831, Lecture Notes in
Computer Science (LNCS) Springer 2021. Emily Yu, Armin Biere and Keijo Heljanko. Progress in
Certifying Hardware Model Checking Results. In
Proc. 24rd Computer Aided Verification (CAV'21), pages
363-386, volume 12760, Lecture Notes in Computer
Science (LNCS) Springer 2021. Lee Barnett and Armin Biere. Non-clausal
Redundancy Properties. In Proc. 28th International
Conference on Automated Deduction(CADE 28), pages 252-272,
volume 12699, Lecture
Notes in Computer Science (LNCS) Springer 2021. 2020Daniela Kaufmann, Mathias Fleury, Armin Biere. The
Proof Checkers Pacheck and Pastèque for the Practical Algebraic
Calculus. To appear in Proc. Intl. Conf. on
Formal Methods in Computer Aided Design (FMCAD'20), 6 pages,
IEEE 2020. Katalin Fazekas, Markus Sinnl, Armin Biere, Sophie Parragh.
Duplex
Encoding of Staircase At-Most-One Constraints for the Antibandwidth
Problem. In Proc. 17th Intl. Conf. on
Integration of Constraint Programming, Artificial Intelligence, and
Operations Research (CPAIOR'20), Lecture Notes in Computer
Science (LNCS) vol. 12296, pages 186-204, Springer
2020. Daniela Kaufmann, Armin Biere. Nullstellensatz-Proofs
for Multiplier Verification. In Proc. Computer Algebra
in Scientific Computing (CASC'20), Lecture Notes in Computer
Science (LNCS) vol. 12291, pages 368-389, Springer
2020. Armin Biere, Katalin Fazekas, Mathias Fleury, Maximillian
Heisinger.
CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling Entering the
SAT Competition 2020. In Proc. of SAT Competition 2020
- Solver and Benchmark Descriptions, Tomas Balyo, Nils
Froleyks, Marijn Heule, Markus Iser, Matti Järvisalo, Martin Suda
(editors), vol. B-2020-1 of Department of Computer Science
Report Series B, pages 50-53, University of Helsinki, 2020. Katalin Fazekas, Markus Sinnl, Armin Biere, Sophie Parragh.
Duplex Encoding of Antibandwidth Feasibility. In
Proc. of SAT Competition 2020 - Solver and Benchmark
Descriptions, Tomas Balyo, Nils Froleyks, Marijn Heule, Markus
Iser, Matti Järvisalo, Martin Suda (editors), vol. B-2020-1 of
Department of Computer Science Report Series B, 2020. pages 81-82,
University of Helsinki, 2020. Sibylle Möhle, Roberto Sebastiani, Armin Biere. Four
Flavors of Entailment. In Proc. 23rd
Intl. Conf. on Theory and Applications of Satisfiability
Testing (SAT'20), Lecture Notes in Computer
Science (LNCS) vol. 12178, pages 62-71, Springer 2020. Maximilian Heisinger, Mathias Fleury, Armin Biere. Distributed
Cube and Conquer with Paracooba. In Proc. 23rd
Intl. Conf. on Theory and Applications of Satisfiability
Testing (SAT'20), Lecture Notes in Computer
Science (LNCS) vol. 12178, pages 114-122, Springer
2020. Lee Barnett, David Cerna, Armin Biere. Covered
Clauses Are Not Propagation Redundant. In Proc. 10th
Intl. Joint Conf. on Automated Reasoning (IJCAR'20),
Lecture Notes in
Computer Science (LNCS) vol. 12166, pages 32-47, Springer
2020. David Cerna, Martina Seidl, Wolfgang Schreiner, Wolfgang
Windsteiger.
Computational Logic in the First Semester of Computer Science: An
Experience Report. In Proc. 12th Intl. Conf. on
Computer Supported Education (CSEDU'20), pages 374-381, SCITEPRESS
2020. David Cerna, Martina Seidl, Wolfgang Schreiner, Wolfgang
Windsteiger.
Aiding an Introduction to Formal Reasoning Within a First-Year
Logic Course for CS Majors Using a Mobile Self-Study App. In
Proc. Proc. ACM Conf. on Innovation and Technology
in Computer Science Education (ITiCSE'20), pages 61-67, ACM
2020. Daniela Kaufmann, Armin Biere, Manuel Kauers. From
DRUP to PAC and Back. In Proc. Design, Automation and
Test in Europe (DATE'20), pages 654-657, IEEE 2020. Marijn Heule, Benjamin Kiesl, Armin Biere. Strong
Extension-Free Proof Systems. In
Journal of Automated Reasoning, 64, pages 533-554,
Springer 2020. Daniela Kaufmann, Armin Biere, Manuel Kauers. SAT,
Computer Algebra, Multipliers. In Vampire 2018 and Vampire
2019. The 5th and 6th Vampire Workshops, pages 1-18, EasyChair
2020. 2019Benjamin Kiesl , Marijn Heule, Armin Biere. Truth
Assignments as Conditional Autarkies. To be published in
Proc. 17th Intl. Symp. on Automated Technology for
Verification and Analysis (ATVA'19), Lecture Notes in Computer
Science (LNCS), vol. 11781, pages 48-64, Springer
2019. Daniela Kaufmann, Armin Biere, Manuel Kauers. Verifying
Large Multipliers by Combining SAT and Computer Algebra. In
Proc. 19th Intl. Conf. on Formal Methods in
Computer Aided Design (FMCAD'19), pages 28-36, IEEE 2019. Best poster and interaction award Best student paper Sibylle Möhle, Armin Biere. Backing
Backtracking In Proc. 22nd Intl. Conf. on Theory
and Applications of Satisfiability Testing (SAT'19), Lecture Notes in Computer
Science (LNCS) vol. 11628, pages 250-166, Springer
2019. Armin Biere. CaDiCaL
at the SAT Race 2019, In
Proc. of SAT Race 2019 - Solver and Benchmark
Descriptions, Marijn Heule, Matti Järvisalo, Martin Suda
(editors), vol. B-2019-1 of Department of Computer Science
Series of Publications B, pages 8-9, University of Helsinki,
2019. Mate Soos, Armin Biere. CryptoMiniSat 5.6
with YalSAT at the SAT Race 2019, In
Proc. of SAT Race 2019 - Solver and Benchmark
Descriptions, Marijn Heule, Matti Järvisalo, Martin Suda
(editors), vol. B-2019-1 of Department of Computer Science
Series of Publications B, pages 14-15, University of Helsinki,
2019. Daniela Kaufmann, Manuel Kauers, Armin Biere, David Cok.
Arithmetic Verification Problems Submitted to the SAT Race
2019, In
Proc. of SAT Race 2019 - Solver and Benchmark
Descriptions, Marijn Heule, Matti Järvisalo, Martin Suda
(editors), vol. B-2019-1 of Department of Computer Science
Series of Publications B, pages 49, University of Helsinki,
2019. Marijn Heule, Benjamin Kiesl, Armin Biere. Clausal
Proofs of Mutilated Chessboards. In Proc. 11th
Intl. Symp. NASA Formal Methods (NFM'19), Lecture Notes in Computer
Science (LNCS) vol. 11460, pages 204-210 Nominated best paper Daniela Kaufmann, Armin Biere, Manuel Kauers. Incremental
column-wise verification of arithmetic circuits using computer
algebra. To be published in Formal Methods in System
Design, Springer 2019. 2018Sibylle Möhle, Armin Biere. Dualizing
Projected Model Counting. To be published in Proc. 30th
Intl. Conf. on Tools with Artificial Intelligence
(ICTAI'18), 8 pages, IEEE Computer Society, 2018. Benjamin Kiesl, Martina Seidl, Hans Tompits, Armin Biere.
Local
Redundancy in SAT: Generalizations of Blocked Clauses.
Logical Methods in Computer Science, vol. 9, issue 4:3,
pages 1-23, https://lmcs.episciences.org
2018. Armin Biere, Daniel Kröning. SAT-Based Model
Checking. In Handbook of Model
Checking, Springer 2018. Marijn Heule, Oliver Kullmann, Armin Biere. Cube-and-Conquer for
Satisfiability. In Handbook of Parallel
Constraint Reasoning, Springer 2018. Armin Biere. CaDiCaL,
Lingeling, Plingeling, Treengeling and YalSAT Entering the SAT
Competition 2018. In Proceedings of SAT Competition
2018 - Solver and Benchmark Descriptions, Marijn Heule,
Matti Järvisalo, Martin Suda (editors), vol. B-2018-1 of
Department of Computer Science Series of Publications B, pages
13-14, University of Helsinki, 2018. Armin Biere.
Divider and Unique Inverse Benchmarks Submitted to the SAT
Competition 2018. In Proceedings of SAT Competition
2018 - Solver and Benchmark Descriptions, Marijn Heule,
Matti Järvisalo, Martin Suda (editors), vol. B-2018-1 of
Department of Computer Science Series of Publications B, page 56,
University of Helsinki, 2018. Aina Niemetz, Mathias Preiner, Armin Biere.
Boolector at the SMT competition 2018. Technical Report
18/1, Stanford University and FMV Reports Series, Institute for Formal Models and
Verification, Johannes Kepler
University, Altenbergerstr. 69, 4040 Linz, Austria, June
2018. Daniela Ritirc, Armin Biere, Manuel Kauers. A
Practical Polynomial Calculus for Arithmetic Circuit
Verification. In Proc. 3rd Intl. Workshop on
Satisfiability Checking and Symbolic Computation (SC2'18),
pages 61-76, CEUR-WS, 2018. Katalin Fazekas, Fahiem Bacchus, Armin Biere. Implicit
Hitting Set Algorithms for Maximum Satisfiability Modulo
Theories. In Proc. 9th Intl. Joint Conf. on
Automated Reasoning (IJCAR'18), Lecture Notes in Computer
Science (LNCS), vol. 10900, pages 134-151, Springer
2018. Aina Niemetz, Mathias Preiner, Clifford Wolf, Armin Biere.
Btor2,
BtorMC and Boolector 3.0. In Proc. 30th
Intl. Conf. on Computer Aided Verification (CAV'18),
Lecture Notes in
Computer Science (LNCS), vol. 10981, pages 587-595,
Springer 2018. Adrian Rebola Pardo, Armin Biere. Two flavors
of DRAT. In Proc. 9th Work. on Pragmatics of SAT
2015 and 2018, EPiC Series in Computing, vol. 59, pages
94-110, EasyChair, 2019. Armin Biere, Marijn Heule. The Effect of
Scrambling CNFs. In Proc. 9th Work. on Pragmatics
of SAT 2015 and 2018, EPiC Series in Computing, vol. 59,
pages 111-126, EasyChair, 2019. Marijn Heule, Armin Biere. What a
Difference a Variable Makes. In Proc. 24th
Intl. Conf. on Tools and Algorithms for the Construction
and Analysis of Systems (TACAS'18), Lecture Notes in Computer
Science (LNCS) vol. 10806, pages 75-92, Springer 2018. Daniela Ritirc, Armin Biere, Manuel Kauers. Improving
and Extending the Algebraic Approach for Verifying Gate-Level
Multipliers. In Proc. Design, Automation and Test in
Europe (DATE'18), pages 1556-1561, IEEE 2018. Tom van Dijk, Rüdiger Ehlers, Armin Biere: Revisiting
Decision Diagrams for SAT. CoRR abs/1805.03496 (2018) 2017Marijn Heule, Martina Seidl, Armin Biere. Solution
Validation and Extraction for QBF Preprocessing.
Journal of Automated Reasoning, 58(1), pages 97-125,
Springer 2017. Benjamin Kiesl, Martina Seidl, Hans Tompits, Armin Biere.
Blockedness
in Propositional Logic: Are You Satisfied With Your
Neighborhood? Proc. 26th Intl. Joint Conf. on
Artificial Intelligence (IJCAI'17), pages 4884-4888, ijcai.org
2017. 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. Armin Biere, Manuel Kauers, Daniela Ritirc,. Challenges
in Verifying Arithmetic Circuits Using Computer Algebra. To
appear in Proc. 19th Intl. Symp. on Symbolic and
Numeric Algorithms for Scientific Computing (SYNASC'17),
IEEE. Best
paper Best
paper Armin Biere, Tom van Dijk, Keijo Heljanko. Hardware
Model Checking Competition 2017. In Proc. 17th
Intl. Conf. on Formal Methods in Computer Aided Design
(FMCAD'17), page 9, IEEE 2017. Aina Niemetz, Mathias Preiner, Armin Biere. Propagation
based local search for bit-precise reasoning . In Journal of
Formal Methods in
System Design, vol. 51(3), pages 608-636, Springer
2017. Armin Biere. CaDiCaL,
Lingeling, Plingeling, Treengeling, YalSAT Entering the SAT
Competition 2017. In Proceedings of SAT Competition
2017 - Solver and Benchmark Descriptions, Tomas Tomáš,
Marijn Heule, Matti Järvisalo (editors), vol. B-2017-1 of
Department of Computer Science Series of Publications B, pages
14-15, University of Helsinki, 2017. Armin Biere.
Deep Bound Hardware Model Checking Instances, Quadratic Propagation
Benchmarks and Reencoded Factorization Problems Submitted to the
SAT Competition 2017. In Proceedings of SAT Competition
2017 - Solver and Benchmark Descriptions, Tomas Tomáš,
Marijn Heule, Matti Järvisalo (editors), vol. B-2017-1 of
Department of Computer Science Series of Publications B, pages
40-41, University of Helsinki, 2017. Aina Niemetz, Mathias Preiner, Armin Biere. Model-Based
API Testing for SMT Solvers. In Proc. 15th
Intl. Workshop on Satisfiability Modulo Theories (SMT'17), 10
pages, aff. to CAV'17, Heidelberg, Germany, 2017. Best
paper Armin Biere, Steffen Hölldobler, Sibylle Möhle. An
Abstract Dual Propositional Model Counter. In Proc. Young
Scientist's Intl. Workshop on Trends in Information Processing
(YSIP2'17), vol. 1837 CEUR Workshop Proceedings, pages 17-26,
CEUR-WS.org 2017. 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. 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. 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. Aina Niemetz, Mathias Preiner, Armin Biere.
Boolector at the SMT competition 2017. Technical Report
17/1, June 2017, FMV
Reports Series, Institute for
Formal Models and Verification, Johannes Kepler University,
Altenbergerstr. 69, 4040 Linz, Austria. 2016Benjamin 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. Tomas Balyo, Armin Biere, Markus Iser, Carsten Sinz. SAT Race 2015,
in Journal of Artificial
Intelligence, vol. 241, pages 45-65, Elsevier 2016. 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. 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. 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. 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. 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. 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. 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. 2015Marijn 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. 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. 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. 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. Armin Biere, Andreas Fröhlich. Evaluating
CDCL Restart Schemes. In Proc. Intl. Workshop on
Pragmatics of SAT 2015 and 2018, EPiC Series in Computing,
vol. 59, pages 1-17, EasyChair, 2019. 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. 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. IJCAI-JAIR 2019 Award 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. 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. 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. 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. 2014Gilles 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. 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. 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. 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. 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. 2013Marijn 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. 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. 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. 2012Cyrille 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. 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. 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. 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. 2011Best paper 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. 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. Boolector
Entering the SMT Competition 2011. Technical Report
11/3, June 2011, FMV
Reports Series, Institute for
Formal Models and Verification, Johannes Kepler University,
Altenbergerstr. 69, 4040 Linz, Austria. 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. 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. 2010Marijn 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. 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. 2009Armin 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. 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. 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. 2008Armin 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. Best student paper 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. 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. 2007Armin 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. 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. 2006Armin 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. 2005Viktor 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. 2004Cyrille 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. 2003Cyrille Artho, Klaus Havelund, Armin Biere. High-Level Data Races. Software Testing, Verification & Reliability (STVR), vol. 13, number 4, John Wiley & Sons 2003. Viktor Schuppan, Armin Biere. Verifying the IEEE 1395 FireWire Tree Identify Protocol with SMV. Formal Aspects of Computing, vol. 14, number 3, Springer 2003. David Plaisted, Armin Biere, Yunshan Zhu. A Satisfiability Tester for Quantified Boolean Formulae. Discrete Applied Mathematics (DAM), vol. 130, number 2, Elsevier 2003. Cyrille Artho, Klaus Havelund, Armin Biere. High-Level Data Races. In Proc. 1st Intl. Workshop on Verification and Validation of Enterprise Information Systems (VVEIS'03), Angers, France, ICEIS Press 2003. Armin Biere, Alessandro Cimatti, Edmund Clarke, Ofer Strichman, Yunshan Zhu. Bounded Model Checking. In Advances in Computers, vol. 58, Academic Press 2003. Armin Biere, Ofer Strichman (editors). Proc. 1st Intl. Workshop on Bounded Model Checking (BMC'03), Electronic Notes in Theoretical Computer Science (ENTCS), vol. 89, issue 4, Elsevier 2004. 2002Armin Biere, Wolfgang Kunz. SAT and ATPG: Boolean Engines for Formal Hardware Verification. In Proc. IEEE/ACM Intl. on Computer Aided Design (ICCAD'02), Nov. 2002. Armin Biere, Cyrille Artho, Viktor Schuppan. Liveness Checking as Safety Checking. In Proc. 7th Intl. Workshop on Formal Methods for Industrial Critical Systems (FMICS'02), Electronic Notes in Theoretical Computer Science (ENTCS), vol. 66, number 2, Elsevier 2002. Sergey Berezin, Edmund Clarke, Armin Biere, Yunshan Zhu. Verification of Out-Of-Order Processor Designs Using Model Checking and a Light-Weight Completion Function. Formal Methods in System Design (FMSD), vol. 20, number 2, Kluwer 2002. 2001Armin Biere. Verifying Sequential Behavior with Model Checking. In Proc. 4th Intl. Conf. on ASIC (ASICON'01), Shanghai, China, IEEE Press and People's Posts & Telecommunications Publishing Office 2001 Edmund Clarke, Armin Biere, Richard Raimi, Yunshan Zhu. Bounded Model Checking Using Satisfiability Solving. Formal Methods in System Design (FMSD), vol. 19, number 1, Kluwer 2001. Cyrille Artho, Armin Biere. Applying Static Analysis to Large-scale, Multi-threaded Java Programs. In Proc. Australian Software Engineering Conf. (ASWEC'01), IEEE 2001, got most influential paper award in 2013. Viktor Schuppan, Armin Biere. A Simple Verification of the Tree Identify Protocol with SMV. In Proc. IEEE 1394 (FireWire) Workshop, Technical Report Dept. of Computing Science and Mathematics, Univ. of Stirling, March 2001. 2000Poul Williams, Armin Biere, Edmund Clarke, Aarti Gupta. Combining Decision Diagrams and SAT Procedures for Efficient Symbolic Model Checking. In Proc. Intl. Conf. on Computer-Aided Verification (CAV'00), Lecture Notes in Computer Science (LNCS), vol. 1855, Springer 2000, 10.1007/10722167_13. 1999Armin Biere, Edmund Clarke, Yunshan Zhu. Multiple State and Single State Tableaux for Combining Local and Global Model Checking. In E.-R. Olderog, B. Steffen (Eds.), Correct System Design Recent Insights and Advances, special issue dedicated to Hans Langmaack, Lecture Notes in Computer Science (LNCS), vol. 1710, Springer 1999, ext. version of our SMC'99 paper. Armin Biere, Alessandro Cimatti, Edmund Clarke, Masahiro Fujita, Yunshan Zhu. Symbolic Model Checking using SAT procedures instead of BDDs. In Proc. ACM Design Automation Conf. (DAC'99), ACM 1999. Armin Biere, Edmund Clarke, Richard Raimi, Yunshan Zhu. Verifying Safety Properties of a PowerPC™ Microprocessor Using Symbolic Model Checking without BDDs. In Proc. Intl. Conf. on Computer-Aided Verification (CAV'99), Lecture Notes in Computer Science (LNCS), vol. 1633, Springer 1999. Armin Biere, Alessandro Cimatti, Edmund Clarke, Yunshan Zhu.
Symbolic
Model Checking without BDDs. In
Proc. Intl. Conf. on Tools and Algorithms for the
Analysis and Construction of Systems (TACAS'99), Lecture Notes in Computer
Science (LNCS), vol. 1579, Springer 1999. Armin Biere, Edmund Clarke, Yunshan Zhu. Combining Local and Global Model Checking. In Proc. 1st Intl. Workshop on Symbolic Model Checking (SMC'99), Electronic Notes in Theoretical Computer Science (ENTCS), vol. 23, number 2, Elsevier 1999, long version. 1998Sergey Berezin, Armin Biere, Edmund Clarke, Yunshan Zhu. Combining Symbolic Model Checking with Uninterpreted Functions for Out-of-Order Processor Verification. In Proc. Intl. Conf. on Formal Methods in Computer-Aided Design (FMCAD'98), Lecture Notes in Computer Science (LNCS), vol. 1522, Springer 1998. Bwolen Yang, Randal Bryant, David O'Hallaron, Armin Biere, Olivier Coudert, Geert Janssen, Rajeev Ranjan, Fabio Somenzi. A Performance Study of BDD-based Model Checking. In Proc. Intl. Conf. on Formal Methods in Computer-Aided Design (FMCAD'98), Lecture Notes in Computer Science (LNCS), vol. 1522, Springer 1998. 1997Armin Biere. mu-cke - Efficient mu-Calculus Model Checking. In Proc. Intl. Conf. on Computer-Aided Verification (CAV'97), Lecture Notes in Computer Science (LNCS), vol. 1254, Springer 1997. Armin Biere. Efficient Model Checking of the Mu-Calculus with Binary Decision Diagrams. Ph.D. Thesis Univ. of Karlsruhe, Germany, Jan. 1997 (in German only). 1993Armin Biere. Normalisation, Unification and Generalisation in Free Monoids. Diploma Thesis Univ. of Karlsruhe, Germany, Sept. 1993 (in German only). |