2009 |
56 | EE | Robert Brummayer,
Armin Biere:
Boolector: An Efficient SMT Solver for Bit-Vectors and Arrays.
TACAS 2009: 174-177 |
2008 |
55 | EE | Armin Biere:
Tutorial on Model Checking: Modelling and Verification in Computer Science.
AB 2008: 16-21 |
54 | EE | Florian Lonsing,
Armin Biere:
Nenofex: Expanding NNF for QBF Solving.
SAT 2008: 196-210 |
53 | EE | Armin Biere:
Adaptive Restart Strategies for Conflict Driven SAT Solvers.
SAT 2008: 28-33 |
52 | EE | Armin Biere:
PicoSAT Essentials.
JSAT 4(2-4): 75-97 (2008) |
2007 |
51 | EE | Robert Brummayer,
Armin Biere:
C32SAT: Checking C Expressions.
CAV 2007: 294-297 |
50 | EE | Cyrille Artho,
Boris Zweimüller,
Armin Biere,
Etsuya Shibayama,
Shinichi Honiden:
Efficient Model Checking of Applications with Input/Output.
EUROCAST 2007: 515-522 |
49 | EE | Toni Jussila,
Armin Biere,
Carsten Sinz,
Daniel Kröning,
Christoph M. Wintersteiger:
A First Step Towards a Unified Proof Checker for QBF.
SAT 2007: 201-214 |
48 | EE | Ofer Strichman,
Armin Biere:
Preface.
Electr. Notes Theor. Comput. Sci. 174(3): 1-2 (2007) |
47 | EE | Toni Jussila,
Armin Biere:
Compressing BMC Encodings with QBF.
Electr. Notes Theor. Comput. Sci. 174(3): 45-56 (2007) |
2006 |
46 | | Armin Biere,
Carla P. Gomes:
Theory and Applications of Satisfiability Testing - SAT 2006, 9th International Conference, Seattle, WA, USA, August 12-15, 2006, Proceedings
Springer 2006 |
45 | EE | Carsten Sinz,
Armin Biere:
Extended Resolution Proofs for Conjoining BDDs.
CSR 2006: 600-611 |
44 | EE | Cyrille Artho,
Armin Biere,
Shinichi Honiden:
Enforcer - Efficient Failure Injection.
FM 2006: 412-427 |
43 | EE | Cyrille Artho,
Armin Biere,
Shinichi Honiden:
Exhaustive Testing of Exception Handlers with Enforcer.
FMCO 2006: 26-46 |
42 | EE | Toni Jussila,
Carsten Sinz,
Armin Biere:
Extended Resolution Proofs for Symbolic SAT Solving with Quantification.
SAT 2006: 54-60 |
41 | EE | Armin Biere,
Keijo Heljanko,
Tommi A. Junttila,
Timo Latvala,
Viktor Schuppan:
Linear Encodings of Bounded LTL Model Checking
CoRR abs/cs/0611029: (2006) |
40 | EE | Armin Biere,
Ofer Strichman:
Preface.
Electr. Notes Theor. Comput. Sci. 144(1): 1- (2006) |
39 | EE | Viktor Schuppan,
Armin Biere:
Liveness Checking as Safety Checking for Infinite State Spaces.
Electr. Notes Theor. Comput. Sci. 149(1): 79-96 (2006) |
38 | EE | Armin Biere,
Carsten Sinz:
Decomposing SAT Problems into Connected Components.
JSAT 2(1-4): 201-208 (2006) |
37 | EE | Armin Biere,
Keijo Heljanko,
Tommi A. Junttila,
Timo Latvala,
Viktor Schuppan:
Linear Encodings of Bounded LTL Model Checking.
Logical Methods in Computer Science 2(5): (2006) |
2005 |
36 | EE | Niklas Eén,
Armin Biere:
Effective Preprocessing in SAT Through Variable and Clause Elimination.
SAT 2005: 61-75 |
35 | EE | Malek Haroud,
Armin Biere:
SDL Versus C Equivalence Checking.
SDL Forum 2005: 323-338 |
34 | EE | Viktor Schuppan,
Armin Biere:
Shortest Counterexamples for Symbolic Model Checking of LTL with Past.
TACAS 2005: 493-509 |
33 | EE | Timo Latvala,
Armin Biere,
Keijo Heljanko,
Tommi A. Junttila:
Simple Is Better: Efficient Bounded Model Checking for Past LTL.
VMCAI 2005: 380-395 |
32 | EE | Viktor Schuppan,
Marcel Baur,
Armin Biere:
JVM Independent Replay in Java.
Electr. Notes Theor. Comput. Sci. 113: 85-104 (2005) |
31 | EE | Armin Biere,
Ofer Strichman:
Preface.
Electr. Notes Theor. Comput. Sci. 119(2): 1- (2005) |
30 | EE | Cyrille Artho,
Armin Biere:
Combined Static and Dynamic Analysis.
Electr. Notes Theor. Comput. Sci. 131: 3-14 (2005) |
29 | EE | Cyrille Artho,
Armin Biere:
Subroutine Inlining and Bytecode Abstraction to Simplify Static and Dynamic Analysis.
Electr. Notes Theor. Comput. Sci. 141(1): 109-128 (2005) |
28 | EE | Mukul R. Prasad,
Armin Biere,
Aarti Gupta:
A survey of recent advances in SAT-based formal verification.
STTT 7(2): 156-173 (2005) |
27 | EE | Armin Biere,
Ofer Strichman:
Introductory paper.
STTT 7(2): 87-88 (2005) |
2004 |
26 | EE | Cyrille Artho,
Klaus Havelund,
Armin Biere:
Using Block-Local Atomicity to Detect Stale-Value Concurrency Errors.
ATVA 2004: 150-164 |
25 | EE | Cyrille Artho,
Viktor Schuppan,
Armin Biere,
Pascal Eugster,
Marcel Baur,
Boris Zweimüller:
JNuke: Efficient Dynamic Analysis for Java.
CAV 2004: 462-465 |
24 | EE | Timo Latvala,
Armin Biere,
Keijo Heljanko,
Tommi A. Junttila:
Simple Bounded LTL Model Checking.
FMCAD 2004: 186-200 |
23 | EE | Armin Biere:
Resolve and Expand.
SAT 2004 |
22 | EE | Armin Biere:
Resolve and Expand.
SAT (Selected Papers 2004: 59-70 |
21 | EE | Viktor Schuppan,
Armin Biere:
Efficient reduction of finite state model checking to reachability analysis.
STTT 5(2-3): 185-204 (2004) |
2003 |
20 | | Cyrille Artho,
Klaus Havelund,
Armin Biere:
High-Level Data Races.
NDDL/VVEIS 2003: 82-93 |
19 | | Armin Biere,
Alessandro Cimatti,
Edmund M. Clarke,
Ofer Strichman,
Yunshan Zhu:
Bounded model checking.
Advances in Computers 58: 118-149 (2003) |
18 | EE | David A. Plaisted,
Armin Biere,
Yunshan Zhu:
A satisfiability procedure for quantified Boolean formulae.
Discrete Applied Mathematics 130(2): 291-328 (2003) |
17 | EE | Armin Biere,
Cyrille Artho,
Malek Haroud,
Viktor Schuppan:
Formal Methods Group ETH Zürich.
Electr. Notes Theor. Comput. Sci. 80: (2003) |
16 | EE | Viktor Schuppan,
Armin Biere:
Verifying the IEEE 1394 FireWire Tree Identify Protocol with SMV.
Formal Asp. Comput. 14(3): 267-280 (2003) |
15 | EE | Cyrille Artho,
Klaus Havelund,
Armin Biere:
High-level data races.
Softw. Test., Verif. Reliab. 13(4): 207-227 (2003) |
2002 |
14 | EE | Armin Biere,
Wolfgang Kunz:
SAT and ATPG: Boolean engines for formal hardware verification.
ICCAD 2002: 782-785 |
13 | EE | Armin Biere,
Cyrille Artho,
Viktor Schuppan:
Liveness Checking as Safety Checking.
Electr. Notes Theor. Comput. Sci. 66(2): (2002) |
12 | | Sergey Berezin,
Edmund M. 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 20(2): 159-186 (2002) |
2001 |
11 | EE | Cyrille Artho,
Armin Biere:
Applying Static Analysis to Large-Scale, Multi-Threaded Java Programs.
Australian Software Engineering Conference 2001: 68-75 |
10 | | Edmund M. Clarke,
Armin Biere,
Richard Raimi,
Yunshan Zhu:
Bounded Model Checking Using Satisfiability Solving.
Formal Methods in System Design 19(1): 7-34 (2001) |
2000 |
9 | | Poul Frederick Williams,
Armin Biere,
Edmund M. Clarke,
Anubhav Gupta:
Combining Decision Diagrams and SAT Procedures for Efficient Symbolic Model Checking.
CAV 2000: 124-138 |
1999 |
8 | EE | Armin Biere,
Edmund M. Clarke,
Richard Raimi,
Yunshan Zhu:
Verifiying Safety Properties of a Power PC Microprocessor Using Symbolic Model Checking without BDDs.
CAV 1999: 60-71 |
7 | EE | Armin Biere,
Edmund M. Clarke,
Yunshan Zhu:
Multiple State and Single State Tableaux for Combining Local and Global Model Checking.
Correct System Design 1999: 163-179 |
6 | EE | Armin Biere,
Alessandro Cimatti,
Edmund M. Clarke,
Masahiro Fujita,
Yunshan Zhu:
Symbolic Model Checking Using SAT Procedures instead of BDDs.
DAC 1999: 317-320 |
5 | EE | Armin Biere,
Alessandro Cimatti,
Edmund M. Clarke,
Yunshan Zhu:
Symbolic Model Checking without BDDs.
TACAS 1999: 193-207 |
4 | EE | Armin Biere,
Edmund M. Clarke,
Yunshan Zhu:
Combining Local and Global Model Checking.
Electr. Notes Theor. Comput. Sci. 23(2): (1999) |
1998 |
3 | EE | Bwolen Yang,
Randal E. Bryant,
David R. O'Hallaron,
Armin Biere,
Olivier Coudert,
Geert Janssen,
Rajeev K. Ranjan,
Fabio Somenzi:
A Performance Study of BDD-Based Model Checking.
FMCAD 1998: 255-289 |
2 | EE | Sergey Berezin,
Armin Biere,
Edmund M. Clarke,
Yunshan Zhu:
Combining Symbolic Model Checking with Uninterpreted Functions for Out-of-Order Processor Verification.
FMCAD 1998: 369-386 |
1997 |
1 | | Armin Biere:
µcke - Efficient µ-Calculus Model Checking.
CAV 1997: 468-471 |