BibSLEIGH
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
EDIT!
CC-BY
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
Travelled to:
1 × Brazil
1 × China
1 × Cyprus
1 × Finland
1 × Hungary
1 × Israel
1 × Poland
1 × Portugal
1 × The Netherlands
2 × France
2 × Germany
2 × Italy
3 × Austria
3 × Canada
7 × USA
7 × United Kingdom
Collaborated with:
F.Lonsing ∅ M.Seidl M.Heule A.Fröhlich M.Järvisalo R.Brummayer C.Artho E.M.Clarke A.Niemetz M.Preiner Y.Zhu G.Kovásznai V.Schuppan B.Kiesl T.Jussila C.Sinz J.Lagniez N.Sörensson N.Eén A.Cimatti H.Tompits A.Yamada T.Kitamura E.Choi A.Goultiaeva A.Nöhrer A.Egyed S.Honiden M.J.H.Heule K.Fazekas F.Bacchus A.Balint U.Schöning T.Balyo D.L.Berre E.Lonca N.Manthey T.Latvala K.Heljanko T.A.Junttila P.F.Williams A.Gupta R.Raimi C.Wolf D.Kröning C.M.Wintersteiger M.Fujita Y.Oiwa P.Eugster M.Baur B.Zweimüller M.Widl P.Brosch U.Egly G.Kappel
Talks about:
sat (11) qbf (9) model (8) check (8) effici (7) claus (7) symbol (6) base (6) solver (5) block (5)

Person: Armin Biere

DBLP DBLP: Biere:Armin

Facilitated 2 volumes:

CAV 2014Ed
SAT 2006Ed

Contributed to:

ICST 20152015
SAT 20152015
IJCAR 20142014
SAT 20142014
CADE 20132013
DATE 20132013
SAT 20132013
TAP 20132013
IJCAR 20122012
SAT 20122012
SLE 20122012
SMT 20122012
SPLC 20122012
CADE 20112011
SAT 20112011
SAT 20102010
TACAS 20102010
SAT 20092009
TACAS 20092009
SAT 20082008
CAV 20072007
SAT 20072007
FM 20062006
SAT 20062006
SAT 20052005
TACAS 20052005
VMCAI 20052005
CAV 20042004
SAT 20042004
SAT 20042005
CAV 20002000
CAV 19991999
DAC 19991999
TACAS 19991999
CAV 19971997
ASE 20162016
CAV (1) 20162016
IJCAR 20162016
CADE 20172017
CAV (1) 20182018
IJCAR 20182018

Wrote 51 papers:

ICST-2015-YamadaKACOB #combinator #incremental #optimisation #satisfiability #testing
Optimization of Combinatorial Testing by Incremental SAT Solving (AY, TK, CA, EHC, YO, AB), pp. 1–10.
SAT-2015-BiereF
Evaluating CDCL Variable Scoring Schemes (AB, AF), pp. 405–422.
IJCAR-2014-HeuleSB #preprocessor #proving
A Unified Proof System for QBF Preprocessing (MH, MS, AB), pp. 91–106.
SAT-2014-BalintBFS #heuristic #implementation #satisfiability
Improving Implementation of SLS Solvers for SAT and New Heuristics for k-SAT with Long Clauses (AB, AB, AF, US), pp. 302–316.
SAT-2014-BalyoFHB #afraid to ask #set
Everything You Always Wanted to Know about Blocked Sets (But Were Afraid to Ask) (TB, AF, MH, AB), pp. 317–332.
SAT-2014-BiereBLM #constraints #detection
Detecting Cardinality Constraints in CNF (AB, DLB, EL, NM), pp. 285–301.
CADE-2013-KovasznaiFB #quantifier
: A Tool for Polynomially Translating Quantifier-Free Bit-Vector Formulas into (GK, AF, AB), pp. 443–449.
DATE-2013-GoultiaevaSB
Bridging the gap between dual propagation and CNF-based QBF solving (AG, MS, AB), pp. 811–814.
SAT-2013-LagniezB
Factoring Out Assumptions to Speed Up MUS Extraction (JML, AB), pp. 276–292.
TAP-2013-ArthoBS #modelling #testing #verification
Model-Based Testing for Verification Back-Ends (CA, AB, MS), pp. 39–55.
IJCAR-2012-JarvisaloHB
Inprocessing Rules (MJ, MH, AB), pp. 355–370.
SAT-2012-NiemetzPLSB
Resolution-Based Certificate Extraction for QBF — (AN, MP, FL, MS, AB), pp. 430–435.
SLE-2012-WidlBBEHKST #diagrams #sequence chart
Guided Merging of Sequence Diagrams (MW, AB, PB, UE, MH, GK, MS, HT), pp. 164–183.
SMT-2012-Biere #aspect-oriented #satisfiability
Practical Aspects of SAT Solving (AB), p. 1.
SMT-2012-KovasznaiFB #complexity #logic #on the
On the Complexity of Fixed-Size Bit-Vector Logics with Binary Encoded Bit-Width (GK, AF, AB), pp. 44–56.
SPLC-2012-NohrerBE #comparison #consistency #nondeterminism
A comparison of strategies for tolerating inconsistencies during decision-making (AN, AB, AE), pp. 11–20.
CADE-2011-BiereLS
Blocked Clause Elimination for QBF (AB, FL, MS), pp. 101–115.
SAT-2011-HeuleJB #graph #performance
Efficient CNF Simplification Based on Binary Implication Graphs (MH, MJ, AB), pp. 201–215.
SAT-2011-LonsingB #detection
Failed Literal Detection for QBF (FL, AB), pp. 259–272.
SAT-2010-BrummayerLB #automation #debugging #satisfiability #testing
Automated Testing and Debugging of SAT and QBF Solvers (RB, FL, AB), pp. 44–57.
SAT-2010-JarvisaloB
Reconstructing Solutions after Blocked Clause Elimination (MJ, AB), pp. 340–345.
SAT-2010-LonsingB #dependence #search-based
Integrating Dependency Schemes in Search-Based QBF Solvers (FL, AB), pp. 158–171.
TACAS-2010-JarvisaloBH
Blocked Clause Elimination (MJ, AB, MH), pp. 129–144.
SAT-2009-LonsingB #dependence #representation
A Compact Representation for Syntactic Dependencies in QBFs (FL, AB), pp. 398–411.
SAT-2009-SorenssonB
Minimizing Learned Clauses (NS, AB), pp. 237–243.
TACAS-2009-BrummayerB #array #named #performance #smt
Boolector: An Efficient SMT Solver for Bit-Vectors and Arrays (RB, AB), pp. 174–177.
SAT-2008-Biere #adaptation #satisfiability
Adaptive Restart Strategies for Conflict Driven SAT Solvers (AB), pp. 28–33.
SAT-2008-LonsingB #named
Nenofex: Expanding NNF for QBF Solving (FL, AB), pp. 196–210.
CAV-2007-BrummayerB #c #named #satisfiability
C32SAT: Checking C Expressions (RB, AB), pp. 294–297.
SAT-2007-JussilaBSKW #proving #towards
A First Step Towards a Unified Proof Checker for QBF (TJ, AB, CS, DK, CMW), pp. 201–214.
FM-2006-ArthoBH #injection #named #performance
Enforcer — Efficient Failure Injection (CA, AB, SH), pp. 412–427.
SAT-2006-JussilaSB #proving #quantifier #satisfiability
Extended Resolution Proofs for Symbolic SAT Solving with Quantification (TJ, CS, AB), pp. 54–60.
SAT-2005-EenB #effectiveness #preprocessor #satisfiability
Effective Preprocessing in SAT Through Variable and Clause Elimination (NE, AB), pp. 61–75.
TACAS-2005-SchuppanB #ltl #model checking
Shortest Counterexamples for Symbolic Model Checking of LTL with Past (VS, AB), pp. 493–509.
VMCAI-2005-LatvalaBHJ #bound #ltl #model checking #performance
Simple Is Better: Efficient Bounded Model Checking for Past LTL (TL, AB, KH, TAJ), pp. 380–395.
CAV-2004-ArthoSBEBZ #dynamic analysis #java #named #performance
JNuke: Efficient Dynamic Analysis for Java (CA, VS, AB, PE, MB, BZ), pp. 462–465.
SAT-2004-Biere
Resolve and Expand (AB), pp. 238–246.
SAT-J-2004-Biere05
Resolve and Expand (AB), pp. 59–70.
CAV-2000-WilliamsBCG #diagrams #model checking #performance #satisfiability
Combining Decision Diagrams and SAT Procedures for Efficient Symbolic Model Checking (PFW, AB, EMC, AG), pp. 124–138.
CAV-1999-BiereCRZ #model checking #safety #using
Verifiying Safety Properties of a Power PC Microprocessor Using Symbolic Model Checking without BDDs (AB, EMC, RR, YZ), pp. 60–71.
DAC-1999-BiereCCFZ #model checking #satisfiability #using
Symbolic Model Checking Using SAT Procedures instead of BDDs (AB, AC, EMC, MF, YZ), pp. 317–320.
TACAS-1999-BiereCCZ #model checking
Symbolic Model Checking without BDDs (AB, AC, EMC, YZ), pp. 193–207.
CAV-1997-Biere #calculus #model checking #named #performance #μ-calculus
μcke — Efficient μ-Calculus Model Checking (AB), pp. 468–471.
ASE-2016-YamadaBAKC #combinator #generative #satisfiability #testing #using
Greedy combinatorial test case generation using unsatisfiable cores (AY, AB, CA, TK, EHC), pp. 614–624.
CAV-2016-NiemetzPB #modulo theories #precise #satisfiability
Precise and Complete Propagation Based Local Search for Satisfiability Modulo Theories (AN, MP, AB), pp. 199–217.
IJCAR-2016-KieslSTB
Super-Blocked Clauses (BK, MS, HT, AB), pp. 45–61.
CADE-2017-HeuleKB #proving
Short Proofs Without New Variables (MJHH, BK, AB), pp. 130–147.
CAV-2018-NiemetzPWB
Btor2 , BtorMC and Boolector 3.0 (AN, MP, CW, AB), pp. 587–595.
IJCAR-2018-FazekasBB #algorithm #modulo theories #satisfiability #set
Implicit Hitting Set Algorithms for Maximum Satisfiability Modulo Theories (KF, FB, AB), pp. 134–151.
Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.