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

[ CiteSeerX Ranking | DBLP | CiteSeerX Citations | Google Scholar | JKU FoDok ]

2010

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.

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), Montreal, Canada, August 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.

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.

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.

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