[ 13 | 12 | 11 | 10 | 09 | 08 | 07 | 06 | 05 | 04 | 03 | 02 | 01 | 00 | 99 | 98 | 97 | 93 ]

papers, citations: [ DBLP | Google Scholar (User Profile) | Microsoft Academic Search | CiteSeerX | JKU FoDok ]

most cited authors rankings: [ Microsoft Author Search | CiteSeerX ]

[ JKU in Microsoft Author Search | FMV in JKU FoDok ]

2013

J.-M. Lagniez, A. Biere. Factoring Out Assumptions to Speed Up MUS Extraction. To appear in Proc. 16th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'13), Lecture Notes in Computer Science (LNCS) vol. 7962, 17 pages, Springer 2013.

G. Kovásznai, A. Fröhlich, A. Biere. BV2EPR: A Tool for Polynomially Translating Quantifier-free Bit-Vector Formulas into EPR. To appear in Proc. 24th Intl. Conf.  on Automated Deduction (CADE'13), Lecture Notes in Computer Science (LNCS), 7 pages, Springer 2013.

A. Fröhlich, G. Kovásznai, A. Biere. More on the Complexity of Quantifier-Free Fixed-Size Bit-Vector Logics with Binary Encoding. To appear in Proc. 8th Intl. Computer Science Symp. in Russia (CSR'13), Lecture Notes in Computer Science (LNCS), 12 pages, Springer 2013 (with appendix).

C. Artho, A. Biere, M. Seidl. Model-Based Testing for Verification Backends. To appear in Proc. 7th Intl. Conf. on Tests & Proofs (TAP'13), Lecture Notes in Computer Science (LNCS), 17 pages, Springer 2013.

M. Heule, M. Järvisalo, A. 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.

A. Goultiaeva, M. Seidl, A. 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.

2012

C. Artho, A. Biere, M. Hagiya, R. Potter, R. Ramler, Y. Tanabe, F. Weitl, M. 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.

N. Manthey, M. Heule, A. Biere. Automated Reencoding of Boolean Formulas. To appear in Proc. Haifa Verification Conference (HVC'12), Lecture Notes in Computer Science (LNCS) vol. 7857, 16 pages, Springer 2013.

M. Widl, A. Biere, P. Brosch, U. Egly, M. Heule, G. Kappel, M. Seidl, H. 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.

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

A. Nöhrer, A. Biere, A. 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.

G. Kovásznai, A. Fröhlich, A. 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), pages 44-55, aff. to IJCAR'12, Manchester, UK, 2012.

M. Seidl, F. Lonsing, A. Biere. QBF2EPR: A Tool for Generating EPR Formulas from QBF In Proc. 3rd Intl. Workshop. on Practical Aspects of Automated Reasoning (PAAR'12), aff. to IJCAR'12, Manchester, UK, 2012.

V. Klebanov, B. Beckert, A. Biere, G. Sutcliffe, editors, Proc. 1st Intl. Work. on Comparative Empirical Evaluation of Reasoning Systems (COMPARE'12), vol. 873, CEUR Workshop Proceedings.

A. Biere. Lingeling and Friends Entering the SAT Challenge 2012. In Proc.  of SAT Challenge 2012: Solver and Benchmark Descriptions, A. Balint, A. Belov, A. Diepold, S. Gerber, M. Järvisalo, and C. Sinz (editors), vol. B-2012-2 of Department of Computer Science Series of Publications B, pages 33-34, University of Helsinki, 2012.

P. van der Tak, M. Heule, and A. Biere. Concurrent Cube-and-Conquer. In Proc.  of SAT Challenge 2012: Solver and Benchmark Descriptions, A. Balint, A. Belov, A. Diepold, S. Gerber, M. Järvisalo, and C. Sinz (editors), vol. B-2012-2 of Department of Computer Science Series of Publications B, pages 15-16, University of Helsinki, 2012.

A. Niemetz, M. Preiner, F. Lonsing, M. Seidl, A. 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.

P. van der Tak, M. Heule, A. 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.

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

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

M. Järvisalo, M. Heule, A. 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.

A. Nöhrer, A. Biere, A. 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.

2011

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

M. Ganai, A. 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.

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

A. Biere, F. Lonsing, M. 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.

M. Heule, M. Järvisalo, A. 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.

F. Lonsing, A. 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.

A. 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.

2010

M. Heule, M. Järvisalo, A. Biere. Covered Clause Elimination. In Short Paper Proc. 17th Intl. Conf. on Logic for Programming, Artificial Intelligence and Reasoning, EPiC Series, vol. 13, pages 41-46, EasyChair 2013.

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

F. Lonsing, A. 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).

M. Järvisalo, A. 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.

R. Brummayer, F. Lonsing, A. 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.

F. Lonsing, A. 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).

M. Järvisalo, A. Biere, M. 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.

A. 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.

2009

A. Biere, C. Pixley, Editors. Proceedings 9th Intl. Conf. on Formal Methods in Computer Aided Design (FMCAD'09), IEEE 2009.

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

N. Sörensson, A. 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.

F. Lonsing, A. 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.

R. Brummayer, A. 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.

R. Brummayer, A. 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.

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

R. Brummayer, A. 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.

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

A. Biere, M. Heule, H. Van Maaren and T. Walsh, Editors. Handbook of Satisfiability. IOS Press, February 2009.

2008

A. Biere, R. 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.

F. Lonsing, A. 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)

A. 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.

R. Brummayer, A. Biere, F. 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.

R. Brummayer, A. 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.

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

F. Lonsing, A. 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.

A. 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.

A. Biere, D. Kröning, G. Weissenbacher, C. Wintersteiger. Digitaltechnik - Eine praxisnahe Einführung. Springer 2008.

2007

R. Brummayer, A. 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.

T. Jussila, A. Biere, C. Sinz, D. Kröning, C. 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.

C. Artho, B. Zweimüller, A. Biere, E. Shibayama, S. 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.

2006

A. Biere, K. Heljanko, T. Junttila, T. Latvala, V. 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.

R. Brummayer, A. 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.

O. Strichman, A. 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.

T. Jussila, A. 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.

A. Biere, C. P. 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.

T. Jussila, C. Sinz, A. 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.

C. Artho, A. Biere, S. 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.

C. Artho, A. Biere, S. Honiden, V. Schuppan, P. Eugster, M. Baur, B. Zweimüller, P. 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.

C. Sinz, A. 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.

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

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

2005

V. Schuppan, A. 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.

A. 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.

N. Eén, A. 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.

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

C. Artho, A. 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.

V. Schuppan, A. 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.

M. Prasad, A. Biere, A. 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.

V. Schuppan, A. 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.

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

C. Artho, A. 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.

T. Latvala, A. Biere, K. Heljanko, T. 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.

2004

C. Artho, K. Havelund, A. 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.

T. Latvala, A. Biere, K. Heljanko, T. 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.

M. Haroud, L. Blazevic, A. Biere. HW accelerated ultra wide band MAC protocol using SDL and SystemC. In Proc. IEEE Radio and Wireless Conference (RAWCON'04), IEEE, Sept. 2004.

T. Latvala, A. Biere, K. Heljanko, T. Junttila. Simple bounded LTL model checking. Research Report A92, Helsinki University of Technology, Laboratory for Theoretical Computer Science, Espoo, Finland, July 2004.

A. Biere, O. 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.

C. Artho, V. Schuppan, A. Biere, P. Eugster, M. Baur, B. 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.

A. 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.

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

V. Schuppan, M. Baur, A. 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.

V. Schuppan, A. 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.

2003

C. Artho, K. Havelund, A. Biere. High-Level Data Races. Software Testing, Verification & Reliability (STVR), vol. 13, number 4, John Wiley & Sons 2003.

V. Schuppan, A. Biere. Verifying the IEEE 1395 FireWire Tree Identify Protocol with SMV. Formal Aspects of Computing, vol. 14, number 3, Springer 2003.

D. Plaisted, A. Biere, Y. Zhu. A Satisfiability Tester for Quantified Boolean Formulae. Discrete Applied Mathematics (DAM), vol. 130, number 2, Elsevier 2003.

C. Artho, K. Havelund, A. 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.

A. Biere, A. Cimatti, E. Clarke, O. Strichman, Y. Zhu. Bounded Model Checking. In Advances in Computers, vol. 58, Academic Press 2003.

A. Biere, O. 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.

2002

A. 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.

A. Biere, C. Artho, V. 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.

S. Berezin, E. Clarke, A. Biere, Y. 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.

2001

A. 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

E. Clarke, A. Biere, R. Raimi, Y. Zhu. Bounded Model Checking Using Satisfiability Solving. Formal Methods in System Design (FMSD), vol. 19, number 1, Kluwer 2001.

C. Artho, A. Biere. Applying Static Analysis to Large-scale, Multi-threaded Java Programs. In Proc. Australian Software Engineering Conf. (ASWEC'01), IEEE 2001.

V. Schuppan, A. 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.

2000

P. Williams, A. Biere, E. Clarke, A. 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.

1999

A. Biere, E. Clarke, Y. 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.

A. Biere, A. Cimatti, E. Clarke, M. Fujita, Y. Zhu. Symbolic Model Checking using SAT procedures instead of BDDs. In Proc. ACM Design Automation Conf. (DAC'99), ACM 1999.

A. Biere, E. Clarke, R. Raimi, Y. 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.

A. Biere, A. Cimatti, E. Clarke, Y. 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.

A. Biere, E. Clarke, Y. 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.

1998

S. Berezin, A. Biere, E. Clarke, Y. 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.

B. Yang, R. E. Bryant, D. R. O'Hallaron, A. Biere, O. Coudert, G. Janssen, R. K. Ranjan, F. 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.

1997

A. 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.

A. Biere. Efficient Model Checking of the Mu-Calculus with Binary Decision Diagrams. Ph.D. Thesis Univ. of Karlsruhe, Germany, Jan. 1997 (in German only).

1993

A. Biere. Normalisation, Unification and Generalisation in Free Monoids. Diploma Thesis Univ. of Karlsruhe, Germany, Sept. 1993 (in German only).