Edit Profile (opens in new tab) Biere, Armin Compute Distance To: Compute Author ID: biere.armin Published as: Biere, Armin; Biere, A. External Links: MGP · ORCID · dblp Documents Indexed: 82 Publications since 1999 13 Contributions as Editor Co-Authors: 72 Co-Authors with 89 Joint Publications 1,244 Co-Co-Authors all top 5 Co-Authors 4 single-authored 22 Heule, Marijn J. H. 9 Lonsing, Florian 9 Seidl, Martina 8 Fröhlich, Andreas M. 8 Järvisalo, Matti 7 Kiesl, Benjamin 5 Clarke, Edmund Melson jun. 5 Schuppan, Viktor 5 Sinz, Carsten 5 Zhu, Yunshan 4 Heljanko, Keijo 4 Kovásznai, Gergely 4 Strichman, Ofer 3 Fazekas, Katalin 3 Fleury, Mathias 3 Junttila, Tommi A. 3 Jussila, Toni 3 Latvala, Timo 3 Niemetz, Aina 3 Preiner, Mathias 3 Tompits, Hans 2 Artho, Cyrille 2 Balyo, Tomáš 2 Barnett, Lee A. 2 Brummayer, Robert 2 Kaufmann, Daniela 2 Kröning, Daniel 2 Möhle, Sibylle 2 Raimi, Richard 2 van Maaren, Hans 2 Walsh, Toby 1 Bacchus, Fahiem 1 Balint, Adrian 1 Baur, Marcel 1 Berezin, Sergey 1 Bloem, Roderick 1 Cai, Shaowei 1 Cerna, David M. 1 Eén, Niklas 1 Egly, Uwe 1 Eugster, Pascal 1 Gomes, Carla P. 1 Gupta, Anubhav 1 Havelund, Klaus 1 Heisinger, Maximilian 1 Iser, Markus 1 Kauers, Manuel 1 Lagniez, Jean-Marie 1 Le Berre, Daniel 1 Liu, Zhenjun 1 Lonca, Emmanuel 1 Manthey, Norbert 1 Nahir, Amir 1 Nawrocki, Wojciech 1 Parragh, Sophie N. 1 Plaisted, David Alan 1 Rebola-Pardo, Adrián 1 Scholl, Christoph 1 Schöning, Uwe 1 Sebastiani, Roberto 1 Sinnl, Markus 1 Suda, Martin 1 Tinelli, Cesare 1 Veith, Helmut 1 Vos, Tanja 1 Weidenbach, Christoph 1 Williams, Poul Frederick 1 Wintersteiger, Christoph M. 1 Yorav, Karen 1 Yu, Emily 1 Zhang, Xindi 1 Zweimüller, Boris all top 5 Serials 5 Journal of Automated Reasoning 5 Formal Methods in System Design 5 Lecture Notes in Computer Science 4 Electronic Notes in Theoretical Computer Science 3 Journal of Satisfiability, Boolean Modeling and Computation 2 The Journal of Artificial Intelligence Research (JAIR) 2 Frontiers in Artificial Intelligence and Applications 2 Logical Methods in Computer Science 1 Artificial Intelligence 1 Discrete Applied Mathematics 1 Formal Aspects of Computing 1 Theory of Computing Systems Fields 95 Computer science (68-XX) 24 Mathematical logic and foundations (03-XX) 12 General and overarching topics; collections (00-XX) 3 Information and communication theory, circuits (94-XX) 1 Operations research, mathematical programming (90-XX) Publications by Year all cited Publications top 5 cited Publications Citations contained in zbMATH Open 74 Publications have been cited 927 times in 514 Documents Cited by ▼ Year ▼ Handbook of satisfiability. Zbl 1183.68568 173 2009 Effective preprocessing in SAT through variable and clause elimination. Zbl 1128.68463Eén, Niklas; Biere, Armin 86 2005 Bounded model checking using satisfiability solving. Zbl 0985.68038Clarke, Edmund; Biere, Armin; Raimi, Richard; Zhu, Yunshan 61 2001 PicoSAT essentials. Zbl 1159.68403Biere, Armin 57 2008 Inprocessing rules. Zbl 1358.68256Järvisalo, Matti; Heule, Marijn J. H.; Biere, Armin 40 2012 Blocked clause elimination. Zbl 1284.03208Järvisalo, Matti; Biere, Armin; Heule, Marijn 31 2010 Resolve and expand. Zbl 1122.68585Biere, Armin 30 2005 Verifying safety properties of a PowerPC\(^{TM}\) microprocessor using symbolic model checking without BDDs. Zbl 1046.68578Biere, Armin; Clarke, Edmund; Raimi, Richard; Zhu, Yunshan 26 1999 Blocked clause elimination for QBF. Zbl 1341.68181Biere, Armin; Lonsing, Florian; Seidl, Martina 24 2011 Clause elimination for SAT and QSAT. Zbl 1336.68231Heule, Marijn; Järvisalo, Matti; Lonsing, Florian; Seidl, Martina; Biere, Armin 19 2015 Clause elimination procedures for CNF formulas. Zbl 1306.68144Heule, Marijn; Järvisalo, Matti; Biere, Armin 18 2010 Linear encodings of bounded LTL model checking. Zbl 1127.68057Biere, Armin; Heljanko, Keijo; Junttila, Tommi; Latvala, Timo; Schuppan, Viktor 18 2006 A unified proof system for QBF preprocessing. Zbl 1409.68257Heule, Marijn J. H.; Seidl, Martina; Biere, Armin 16 2014 Simulating circuit-level simplifications on CNF. Zbl 1267.94144Järvisalo, Matti; Biere, Armin; Heule, Marijn J. H. 16 2012 Lemmas on demand for the extensional theory of arrays. Zbl 1187.68168Brummayer, Robert; Biere, Armin 14 2009 Extended resolution proofs for conjoining BDDs. Zbl 1185.68635Sinz, Carsten; Biere, Armin 14 2006 Automated testing and debugging of SAT and QBF solvers. Zbl 1306.68155Brummayer, Robert; Lonsing, Florian; Biere, Armin 13 2010 A first step towards a unified proof checker for QBF. Zbl 1214.68334Jussila, Toni; Biere, Armin; Sinz, Carsten; Kröning, Daniel; Wintersteiger, Christoph M. 12 2007 Adaptive restart strategies for conflict driven SAT solvers. Zbl 1138.68533Biere, Armin 12 2008 Nenofex: Expanding NNF for QBF solving. Zbl 1138.68546Lonsing, Florian; Biere, Armin 12 2008 Enhancing search-based QBF solving by dynamic blocked clause elimination. Zbl 1471.68251Lonsing, Florian; Bacchus, Fahiem; Biere, Armin; Egly, Uwe; Seidl, Martina 12 2015 Efficient CNF simplification based on binary implication graphs. Zbl 1330.68269Heule, Marijn J. H.; Järvisalo, Matti; Biere, Armin 12 2011 Integrating dependency schemes in search-based QBF solvers. Zbl 1306.68165Lonsing, Florian; Biere, Armin 11 2010 Short proofs without new variables. Zbl 1468.03010Heule, Marijn J. H.; Kiesl, Benjamin; Biere, Armin 11 2017 Extended resolution proofs for symbolic SAT solving with quantification. Zbl 1187.68550Jussila, Toni; Sinz, Carsten; Biere, Armin 9 2006 Super-blocked clauses. Zbl 1475.68347Kiesl, Benjamin; Seidl, Martina; Tompits, Hans; Biere, Armin 9 2016 Factoring out assumptions to speed up MUS extraction. Zbl 1390.68601Lagniez, Jean-Marie; Biere, Armin 9 2013 SAT race 2015. Zbl 1392.68381Balyo, Tomáš; Biere, Armin; Iser, Markus; Sinz, Carsten 8 2016 Liveness checking as safety checking for infinite state spaces. Zbl 1273.68240Schuppan, Viktor; Biere, Armin 8 2006 Compressing BMC encodings with QBF. Zbl 1277.68136Jussila, Toni; Biere, Armin 8 2007 Strong extension-free proof systems. Zbl 1468.03011Heule, Marijn J. H.; Kiesl, Benjamin; Biere, Armin 7 2020 Evaluating CDCL variable scoring schemes. Zbl 1471.68238Biere, Armin; Fröhlich, Andreas 7 2015 What a difference a variable makes. Zbl 1423.68419Heule, Marijn J. H.; Biere, Armin 7 2018 Complexity of fixed-size bit-vector logics. Zbl 1357.68086Kovásznai, Gergely; Fröhlich, Andreas; Biere, Armin 7 2016 More on the complexity of quantifier-free fixed-size bit-vector logics with binary encoding. Zbl 1345.68172Fröhlich, Andreas; Kovásznai, Gergely; Biere, Armin 7 2013 Combining decision diagrams and SAT procedures for efficient symbolic model checking. Zbl 0974.68526Williams, Poul F.; Biere, Armin; Clarke, Edmund M.; Gupta, Anubhav 6 2000 Shortest counterexamples for symbolic model checking of LTL with past. Zbl 1087.68060Schuppan, Viktor; Biere, Armin 5 2005 Incremental inprocessing in SAT solving. Zbl 1441.68224Fazekas, Katalin; Biere, Armin; Scholl, Christoph 5 2019 A satisfiability procedure for quantified Boolean formulae. Zbl 1029.68082Plaisted, David A.; Biere, Armin; Zhu, Yunshan 5 2003 Blocked clauses in first-order logic. Zbl 1403.68240Kiesl, Benjamin; Suda, Martin; Seidl, Martina; Tompits, Hans; Biere, Armin 5 2017 Failed literal detection for QBF. Zbl 1330.68118Lonsing, Florian; Biere, Armin 5 2011 Blocked clause decomposition. Zbl 1407.68451Heule, Marijn J. H.; Biere, Armin 5 2013 Simple bounded LTL model checking. Zbl 1117.68432Latvala, Timo; Biere, Armin; Heljanko, Keijo; Junttila, Tommi 4 2004 Reconstructing solutions after blocked clause elimination. Zbl 1306.68159Järvisalo, Matti; Biere, Armin 4 2010 Propagation based local search for bit-precise reasoning. Zbl 1377.68134Niemetz, Aina; Preiner, Mathias; Biere, Armin 4 2017 Detecting cardinality constraints in CNF. Zbl 1423.68437Biere, Armin; Le Berre, Daniel; Lonca, Emmanuel; Manthey, Norbert 4 2014 Efficiently representing existential dependency sets for expansion-based QBF solvers. Zbl 1291.68358Lonsing, Florian; Biere, Armin 4 2009 Solution validation and extraction for QBF preprocessing. Zbl 1409.68258Heule, Marijn J. H.; Seidl, Martina; Biere, Armin 4 2017 Handbook of satisfiability. In 2 parts. 2nd updated and revised edition. Zbl 1456.68001 3 2021 Proofs for satisfiability problems. Zbl 1431.03024Heule, Marijn J. H.; Biere, Armin 3 2015 Compositional propositional proofs. Zbl 1471.68310Heule, Marijn J. H.; Biere, Armin 3 2015 Everything you always wanted to know about blocked sets (but were afraid to ask). Zbl 1423.68435Balyo, Tomáš; Fröhlich, Andreas; Heule, Marijn J. H.; Biere, Armin 3 2014 SAT-based model checking. Zbl 1392.68232Biere, Armin; Kröning, Daniel 3 2018 Decomposing SAT problems into connected components. Zbl 1116.68079Biere, Armin; Sinz, Carsten 2 2006 Tutorial on model checking: Modelling and verification in computer science. Zbl 1171.68546Biere, Armin 2 2008 Theory and applications of satisfiability testing – SAT 2006. 9th international conference, Seattle, WA, USA, August 12–15, 2006. Proceedings. Zbl 1114.68003 2 2006 Backing backtracking. Zbl 1441.68231Möhle, Sibylle; Biere, Armin 2 2019 Computer aided verification. 26th international conference, CAV 2014, held as part of the Vienna summer of logic, VSL 2014, Vienna, Austria, July 18–22, 2014. Proceedings. Zbl 1293.68018 2 2014 Truth assignments as conditional autarkies. Zbl 1437.68132Kiesl, Benjamin; Heule, Marijn J. H.; Biere, Armin 2 2019 Counterexample-guided model synthesis. Zbl 1452.68122Preiner, Mathias; Niemetz, Aina; Biere, Armin 2 2017 A compact representation for syntactic dependencies in QBFs. Zbl 1247.68238Lonsing, Florian; Biere, Armin 1 2009 Verification of out-of-order processor designs using model Checking and a light-weight completion function. Zbl 1014.68147Berezin, Sergey; Clarke, Edmund; Biere, Armin; Zhu, Yunshan 1 2002 Non-clausal redundancy properties. Zbl 07437083Barnett, Lee A.; Biere, Armin 1 2021 Incremental column-wise verification of arithmetic circuits using computer algebra. Zbl 07307313Kaufmann, Daniela; Biere, Armin; Kauers, Manuel 1 2020 Simulating strong practical proof systems with extended resolution. Zbl 1468.68293Kiesl, Benjamin; Rebola-Pardo, Adrián; Heule, Marijn J. H.; Biere, Armin 1 2020 Distributed cube and conquer with Paracooba. Zbl 07331016Heisinger, Maximilian; Fleury, Mathias; Biere, Armin 1 2020 Simple is better: Efficient bounded model checking for past LTL. Zbl 1111.68510Latvala, Timo; Biere, Armin; Heljanko, Keijo; Junttila, Tommi 1 2005 JNuke: Efficient dynamic analysis for Java. Zbl 1103.68602Artho, Cyrille; Schuppan, Viktor; Biere, Armin; Eugster, Pascal; Baur, Marcel; Zweimüller, Boris 1 2004 Verifying the IEEE 1394 fireWire tree identify protocol with SMV. Zbl 1029.68021Schuppan, Viktor; Biere, Armin 1 2002 Local redundancy in SAT: generalizations of blocked clauses. Zbl 1403.68239Kiesl, Benjamin; Seidl, Martina; Tompits, Hans; Biere, Armin 1 2018 Improving implementation of SLS solvers for SAT and new heuristics for \(k\)-SAT with long clauses. Zbl 1423.68434Balint, Adrian; Biere, Armin; Fröhlich, Andreas; Schöning, Uwe 1 2014 On the complexity of symbolic verification and decision problems in bit-vector logic. Zbl 1426.68127Kovásznai, Gergely; Veith, Helmut; Fröhlich, Andreas; Biere, Armin 1 2014 bv2epr: a tool for polynomially translating quantifier-free bit-vector formulas into EPR. Zbl 1382.68217Kovásznai, Gergely; Fröhlich, Andreas; Biere, Armin 1 2013 Precise and complete propagation based local search for satisfiability modulo theories. Zbl 1411.68070Niemetz, Aina; Preiner, Mathias; Biere, Armin 1 2016 Handbook of satisfiability. In 2 parts. 2nd updated and revised edition. Zbl 1456.68001 3 2021 Non-clausal redundancy properties. Zbl 07437083Barnett, Lee A.; Biere, Armin 1 2021 Strong extension-free proof systems. Zbl 1468.03011Heule, Marijn J. H.; Kiesl, Benjamin; Biere, Armin 7 2020 Incremental column-wise verification of arithmetic circuits using computer algebra. Zbl 07307313Kaufmann, Daniela; Biere, Armin; Kauers, Manuel 1 2020 Simulating strong practical proof systems with extended resolution. Zbl 1468.68293Kiesl, Benjamin; Rebola-Pardo, Adrián; Heule, Marijn J. H.; Biere, Armin 1 2020 Distributed cube and conquer with Paracooba. Zbl 07331016Heisinger, Maximilian; Fleury, Mathias; Biere, Armin 1 2020 Incremental inprocessing in SAT solving. Zbl 1441.68224Fazekas, Katalin; Biere, Armin; Scholl, Christoph 5 2019 Backing backtracking. Zbl 1441.68231Möhle, Sibylle; Biere, Armin 2 2019 Truth assignments as conditional autarkies. Zbl 1437.68132Kiesl, Benjamin; Heule, Marijn J. H.; Biere, Armin 2 2019 What a difference a variable makes. Zbl 1423.68419Heule, Marijn J. H.; Biere, Armin 7 2018 SAT-based model checking. Zbl 1392.68232Biere, Armin; Kröning, Daniel 3 2018 Local redundancy in SAT: generalizations of blocked clauses. Zbl 1403.68239Kiesl, Benjamin; Seidl, Martina; Tompits, Hans; Biere, Armin 1 2018 Short proofs without new variables. Zbl 1468.03010Heule, Marijn J. H.; Kiesl, Benjamin; Biere, Armin 11 2017 Blocked clauses in first-order logic. Zbl 1403.68240Kiesl, Benjamin; Suda, Martin; Seidl, Martina; Tompits, Hans; Biere, Armin 5 2017 Propagation based local search for bit-precise reasoning. Zbl 1377.68134Niemetz, Aina; Preiner, Mathias; Biere, Armin 4 2017 Solution validation and extraction for QBF preprocessing. Zbl 1409.68258Heule, Marijn J. H.; Seidl, Martina; Biere, Armin 4 2017 Counterexample-guided model synthesis. Zbl 1452.68122Preiner, Mathias; Niemetz, Aina; Biere, Armin 2 2017 Super-blocked clauses. Zbl 1475.68347Kiesl, Benjamin; Seidl, Martina; Tompits, Hans; Biere, Armin 9 2016 SAT race 2015. Zbl 1392.68381Balyo, Tomáš; Biere, Armin; Iser, Markus; Sinz, Carsten 8 2016 Complexity of fixed-size bit-vector logics. Zbl 1357.68086Kovásznai, Gergely; Fröhlich, Andreas; Biere, Armin 7 2016 Precise and complete propagation based local search for satisfiability modulo theories. Zbl 1411.68070Niemetz, Aina; Preiner, Mathias; Biere, Armin 1 2016 Clause elimination for SAT and QSAT. Zbl 1336.68231Heule, Marijn; Järvisalo, Matti; Lonsing, Florian; Seidl, Martina; Biere, Armin 19 2015 Enhancing search-based QBF solving by dynamic blocked clause elimination. Zbl 1471.68251Lonsing, Florian; Bacchus, Fahiem; Biere, Armin; Egly, Uwe; Seidl, Martina 12 2015 Evaluating CDCL variable scoring schemes. Zbl 1471.68238Biere, Armin; Fröhlich, Andreas 7 2015 Proofs for satisfiability problems. Zbl 1431.03024Heule, Marijn J. H.; Biere, Armin 3 2015 Compositional propositional proofs. Zbl 1471.68310Heule, Marijn J. H.; Biere, Armin 3 2015 A unified proof system for QBF preprocessing. Zbl 1409.68257Heule, Marijn J. H.; Seidl, Martina; Biere, Armin 16 2014 Detecting cardinality constraints in CNF. Zbl 1423.68437Biere, Armin; Le Berre, Daniel; Lonca, Emmanuel; Manthey, Norbert 4 2014 Everything you always wanted to know about blocked sets (but were afraid to ask). Zbl 1423.68435Balyo, Tomáš; Fröhlich, Andreas; Heule, Marijn J. H.; Biere, Armin 3 2014 Computer aided verification. 26th international conference, CAV 2014, held as part of the Vienna summer of logic, VSL 2014, Vienna, Austria, July 18–22, 2014. Proceedings. Zbl 1293.68018 2 2014 Improving implementation of SLS solvers for SAT and new heuristics for \(k\)-SAT with long clauses. Zbl 1423.68434Balint, Adrian; Biere, Armin; Fröhlich, Andreas; Schöning, Uwe 1 2014 On the complexity of symbolic verification and decision problems in bit-vector logic. Zbl 1426.68127Kovásznai, Gergely; Veith, Helmut; Fröhlich, Andreas; Biere, Armin 1 2014 Factoring out assumptions to speed up MUS extraction. Zbl 1390.68601Lagniez, Jean-Marie; Biere, Armin 9 2013 More on the complexity of quantifier-free fixed-size bit-vector logics with binary encoding. Zbl 1345.68172Fröhlich, Andreas; Kovásznai, Gergely; Biere, Armin 7 2013 Blocked clause decomposition. Zbl 1407.68451Heule, Marijn J. H.; Biere, Armin 5 2013 bv2epr: a tool for polynomially translating quantifier-free bit-vector formulas into EPR. Zbl 1382.68217Kovásznai, Gergely; Fröhlich, Andreas; Biere, Armin 1 2013 Inprocessing rules. Zbl 1358.68256Järvisalo, Matti; Heule, Marijn J. H.; Biere, Armin 40 2012 Simulating circuit-level simplifications on CNF. Zbl 1267.94144Järvisalo, Matti; Biere, Armin; Heule, Marijn J. H. 16 2012 Blocked clause elimination for QBF. Zbl 1341.68181Biere, Armin; Lonsing, Florian; Seidl, Martina 24 2011 Efficient CNF simplification based on binary implication graphs. Zbl 1330.68269Heule, Marijn J. H.; Järvisalo, Matti; Biere, Armin 12 2011 Failed literal detection for QBF. Zbl 1330.68118Lonsing, Florian; Biere, Armin 5 2011 Blocked clause elimination. Zbl 1284.03208Järvisalo, Matti; Biere, Armin; Heule, Marijn 31 2010 Clause elimination procedures for CNF formulas. Zbl 1306.68144Heule, Marijn; Järvisalo, Matti; Biere, Armin 18 2010 Automated testing and debugging of SAT and QBF solvers. Zbl 1306.68155Brummayer, Robert; Lonsing, Florian; Biere, Armin 13 2010 Integrating dependency schemes in search-based QBF solvers. Zbl 1306.68165Lonsing, Florian; Biere, Armin 11 2010 Reconstructing solutions after blocked clause elimination. Zbl 1306.68159Järvisalo, Matti; Biere, Armin 4 2010 Handbook of satisfiability. Zbl 1183.68568 173 2009 Lemmas on demand for the extensional theory of arrays. Zbl 1187.68168Brummayer, Robert; Biere, Armin 14 2009 Efficiently representing existential dependency sets for expansion-based QBF solvers. Zbl 1291.68358Lonsing, Florian; Biere, Armin 4 2009 A compact representation for syntactic dependencies in QBFs. Zbl 1247.68238Lonsing, Florian; Biere, Armin 1 2009 PicoSAT essentials. Zbl 1159.68403Biere, Armin 57 2008 Adaptive restart strategies for conflict driven SAT solvers. Zbl 1138.68533Biere, Armin 12 2008 Nenofex: Expanding NNF for QBF solving. Zbl 1138.68546Lonsing, Florian; Biere, Armin 12 2008 Tutorial on model checking: Modelling and verification in computer science. Zbl 1171.68546Biere, Armin 2 2008 A first step towards a unified proof checker for QBF. Zbl 1214.68334Jussila, Toni; Biere, Armin; Sinz, Carsten; Kröning, Daniel; Wintersteiger, Christoph M. 12 2007 Compressing BMC encodings with QBF. Zbl 1277.68136Jussila, Toni; Biere, Armin 8 2007 Linear encodings of bounded LTL model checking. Zbl 1127.68057Biere, Armin; Heljanko, Keijo; Junttila, Tommi; Latvala, Timo; Schuppan, Viktor 18 2006 Extended resolution proofs for conjoining BDDs. Zbl 1185.68635Sinz, Carsten; Biere, Armin 14 2006 Extended resolution proofs for symbolic SAT solving with quantification. Zbl 1187.68550Jussila, Toni; Sinz, Carsten; Biere, Armin 9 2006 Liveness checking as safety checking for infinite state spaces. Zbl 1273.68240Schuppan, Viktor; Biere, Armin 8 2006 Decomposing SAT problems into connected components. Zbl 1116.68079Biere, Armin; Sinz, Carsten 2 2006 Theory and applications of satisfiability testing – SAT 2006. 9th international conference, Seattle, WA, USA, August 12–15, 2006. Proceedings. Zbl 1114.68003 2 2006 Effective preprocessing in SAT through variable and clause elimination. Zbl 1128.68463Eén, Niklas; Biere, Armin 86 2005 Resolve and expand. Zbl 1122.68585Biere, Armin 30 2005 Shortest counterexamples for symbolic model checking of LTL with past. Zbl 1087.68060Schuppan, Viktor; Biere, Armin 5 2005 Simple is better: Efficient bounded model checking for past LTL. Zbl 1111.68510Latvala, Timo; Biere, Armin; Heljanko, Keijo; Junttila, Tommi 1 2005 Simple bounded LTL model checking. Zbl 1117.68432Latvala, Timo; Biere, Armin; Heljanko, Keijo; Junttila, Tommi 4 2004 JNuke: Efficient dynamic analysis for Java. Zbl 1103.68602Artho, Cyrille; Schuppan, Viktor; Biere, Armin; Eugster, Pascal; Baur, Marcel; Zweimüller, Boris 1 2004 A satisfiability procedure for quantified Boolean formulae. Zbl 1029.68082Plaisted, David A.; Biere, Armin; Zhu, Yunshan 5 2003 Verification of out-of-order processor designs using model Checking and a light-weight completion function. Zbl 1014.68147Berezin, Sergey; Clarke, Edmund; Biere, Armin; Zhu, Yunshan 1 2002 Verifying the IEEE 1394 fireWire tree identify protocol with SMV. Zbl 1029.68021Schuppan, Viktor; Biere, Armin 1 2002 Bounded model checking using satisfiability solving. Zbl 0985.68038Clarke, Edmund; Biere, Armin; Raimi, Richard; Zhu, Yunshan 61 2001 Combining decision diagrams and SAT procedures for efficient symbolic model checking. Zbl 0974.68526Williams, Poul F.; Biere, Armin; Clarke, Edmund M.; Gupta, Anubhav 6 2000 Verifying safety properties of a PowerPC\(^{TM}\) microprocessor using symbolic model checking without BDDs. Zbl 1046.68578Biere, Armin; Clarke, Edmund; Raimi, Richard; Zhu, Yunshan 26 1999 all cited Publications top 5 cited Publications all top 5 Cited by 955 Authors 26 Biere, Armin 24 Heule, Marijn J. H. 23 Marques-Silva, João P. 13 Seidl, Martina 11 Barrett, Clark W. 11 Järvisalo, Matti 10 Lonsing, Florian 10 Schaub, Torsten H. 9 Hoos, Holger H. 9 Janota, Mikoláš 9 Szeider, Stefan 9 Tinelli, Cesare 8 Becker, Bernd 8 Ignatyev, Alexey A. 7 Lindauer, Marius 7 Niemetz, Aina 7 Preiner, Mathias 7 Reynolds, Andrew 7 Sebastiani, Roberto 7 Semenov, Aleksandr Anatol’evich 7 Weidenbach, Christoph 6 Ábrahám, Erika 6 Ansótegui, Carlos 6 Beyersdorff, Olaf 6 Kröning, Daniel 6 Kullmann, Oliver 6 Leyton-Brown, Kevin 6 Suda, Martin 5 Chew, Leroy 5 Egly, Uwe 5 Gebser, Martin 5 Griggio, Alberto 5 Hutter, Frank 5 Kaufmann, Benjamin 5 Kiesl, Benjamin 5 Lynce, Inês 5 Mencía, Carlos 5 Scholl, Christoph 5 Sinz, Carsten 5 Slivovsky, Friedrich 5 Vardi, Moshe Ya’akov 5 Wimmer, Ralf D. 5 Zaikin, Oleg Sergeevich 4 Balabanov, Valeriy 4 Bryant, Randal E. 4 Cimatti, Alessandro 4 Dodaro, Carmine 4 Ganesh, Vijay 4 Jiang, Jie-Hong Roland 4 Kochemazov, Stepan 4 Lagniez, Jean-Marie 4 Manquinho, Vasco M. 4 Manthey, Norbert 4 Marić, Filip 4 Nadel, Alexander 4 Philipp, Tobias 4 Pulina, Luca 4 Ricca, Francesco 4 Ryvchin, Vadim 4 Saïs, Lakhdar 4 Schuppan, Viktor 4 Stump, Aaron 4 Tentrup, Leander 4 Trentin, Patrick 4 Woltran, Stefan 3 Amjad, Hasan 3 Balyo, Tomáš 3 Berend, Daniel 3 Berg, Jeremias 3 Blanchette, Jasmin Christian 3 Blinkhorn, Joshua 3 Bofill, Miquel 3 Bubeck, Uwe 3 Buss, Sam 3 Davenport, James Harold 3 de Moura, Leonardo 3 England, Matthew 3 Fichte, Johannes Klaus 3 Finkbeiner, Bernd 3 Fleury, Mathias 3 Fröhlich, Andreas M. 3 Gaspers, Serge 3 Graham-Lengrand, Stéphane 3 Hamadi, Youssef 3 Hecher, Markus 3 Heljanko, Keijo 3 Irfan, Ahmed 3 Iser, Markus 3 Jabbour, Said 3 Jonáš, Martin 3 Junttila, Tommi A. 3 Katoen, Joost-Pieter 3 Kauers, Manuel 3 Kleine Büning, Hans 3 Kotsireas, Ilias S. 3 Kremer, Gereon 3 Kupferman, Orna 3 Levy, Jordi 3 Mackey, John 3 Marquis, Pierre ...and 855 more Authors all top 5 Cited in 82 Serials 44 Artificial Intelligence 36 Journal of Automated Reasoning 22 Formal Methods in System Design 18 Constraints 17 Theoretical Computer Science 11 Theory and Practice of Logic Programming 8 Annals of Mathematics and Artificial Intelligence 7 Discrete Applied Mathematics 7 International Journal of Approximate Reasoning 7 Formal Aspects of Computing 7 Logical Methods in Computer Science 6 Acta Informatica 6 Journal of Symbolic Computation 6 Journal of Satisfiability, Boolean Modeling and Computation 5 Annals of Operations Research 4 Science of Computer Programming 4 Computers & Operations Research 4 Journal of Applied Mathematics 3 Information Processing Letters 3 Journal of Computer and System Sciences 3 Automation and Remote Control 3 Fundamenta Informaticae 3 ACM Transactions on Computational Logic 3 Journal of Applied Logic 2 SIAM Journal on Computing 2 Algorithmica 2 Information and Computation 2 AI Communications 2 Machine Learning 2 Computational Geometry 2 The Journal of Artificial Intelligence Research (JAIR) 2 Journal of Heuristics 2 Mathematical Problems in Engineering 2 Theory of Computing Systems 2 ACM Journal of Experimental Algorithmics 2 Mathematics in Computer Science 1 Computing 1 Fuzzy Sets and Systems 1 Information Sciences 1 Journal of Economic Theory 1 Studia Logica 1 Synthese 1 Graphs and Combinatorics 1 Journal of Computer Science and Technology 1 International Journal of Parallel Programming 1 Real-Time Systems 1 Japan Journal of Industrial and Applied Mathematics 1 International Journal of Algebra and Computation 1 Discrete Event Dynamic Systems 1 Designs, Codes and Cryptography 1 Bulletin of the American Mathematical Society. New Series 1 Distributed Computing 1 Computational Complexity 1 Journal of Mathematical Sciences (New York) 1 Advances in Applied Clifford Algebras 1 The Electronic Journal of Combinatorics 1 Top 1 Doklady Mathematics 1 Nonlinear Dynamics 1 Optimization Methods & Software 1 Journal of Combinatorial Optimization 1 Journal of Applied Mathematics and Decision Sciences 1 Journal of Graph Algorithms and Applications 1 International Journal of Applied Mathematics and Computer Science 1 Computer Languages, Systems & Structures 1 4OR 1 Journal of Discrete Algorithms 1 Fuzzy Optimization and Decision Making 1 Journal of Statistical Mechanics: Theory and Experiment 1 Electronic Notes in Theoretical Computer Science 1 Algorithms 1 Mathematical Programming Computation 1 Science China. Information Sciences 1 Symmetry 1 Diskretnyĭ Analiz i Issledovanie Operatsiĭ 1 Journal of Theoretical Biology 1 Frontiers of Computer Science 1 Computer Science Review 1 ACM Transactions on Computation Theory 1 Journal of Logical and Algebraic Methods in Programming 1 Philosophical Transactions of the Royal Society of London. A. Mathematical, Physical and Engineering Sciences 1 DML. Discrete Mathematics Letters all top 5 Cited in 24 Fields 466 Computer science (68-XX) 106 Mathematical logic and foundations (03-XX) 49 Operations research, mathematical programming (90-XX) 18 Combinatorics (05-XX) 13 Information and communication theory, circuits (94-XX) 9 Game theory, economics, finance, and other social and behavioral sciences (91-XX) 8 Biology and other natural sciences (92-XX) 5 Systems theory; control (93-XX) 4 Convex and discrete geometry (52-XX) 4 Statistics (62-XX) 3 General and overarching topics; collections (00-XX) 2 Linear and multilinear algebra; matrix theory (15-XX) 2 Dynamical systems and ergodic theory (37-XX) 2 Probability theory and stochastic processes (60-XX) 1 History and biography (01-XX) 1 Order, lattices, ordered algebraic structures (06-XX) 1 Number theory (11-XX) 1 Associative rings and algebras (16-XX) 1 Measure and integration (28-XX) 1 Numerical analysis (65-XX) 1 Classical thermodynamics, heat transfer (80-XX) 1 Quantum theory (81-XX) 1 Statistical mechanics, structure of matter (82-XX) 1 Mathematics education (97-XX) Citations by Year