Publications

This page contains the list of publications of FMV since 2004.

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. To be published in Short Paper Proc. 17th Intl. Conf. on Logic for Programming, Artificial Intelligence and Reasoning, EasyChair Proceedings, 2010.

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.

R. Brummayer, M. Järvisalo. Testing and Debugging Techniques for Answer Set Solver Development. In Proc. Intl. Conf. on Logic Programming (ICLP'10), published in Theory and Practice of Logic Programming vol. 10(4-6), pages 741-758, 2010.

R. Brummayer, D. Oe, A. Stump. Exploring Predictability of SAT/SMT Solvers. Intl. Workshop on Evaluation Methods for Solvers and Quality Metrics for Solutions (EMSQMS'10), affiliated to IJCAR'10 and CAV'10 at FLOC'10.

2009

R. Brummayer. Efficient SMT Solving for Bit-Vectors and the Extensional Theory of Arrays. Ph.D. thesis, Johannes Kepler University Linz, Austria, November 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.

T. Jussila, J. Dubrovin, T. Junttila, T. Latvala, I. Porres Model Checking Dynamic and Hierarchical UML State Machines In Proc. 3rd International Workshop on Model Development, Validation and Verification (MoDeV2a) pages, 94-110, Genova, Italy, October 2006.

2005

Publications in Formal Methods in 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.

C. Sinz. Towards an optimal CNF encoding of Boolean cardinality constraints. In Proc. 11th Intl. Conf. on Principles and Practice of Constraint Programming (CP 2005), pages 827-831, Sitges, Spain, October 2005. Lecture Notes in Computer Science (LNCS), vol. 3709, Springer 2005.

Publications in Heuristic Optimization in 2005

M. Affenzeller, S. Wagner. Enhanced Genetic Algorithms Inspired by Population Genetics. To be published in: Intl. Journal of Systems Science. Taylor & Francis, 2005.

S. Winkler, H. Efendic, M. Affenzeller, L. Del Re, S. Wagner. On-Line Modeling Based on Genetic Programming. Accepted to be published in: Special Issue of the Intl. Journal of Intelligent Systems Technologies and Applications (IJISTA). 2005.

S. Winkler, M. Affenzeller, S. Wagner. A Genetic Programming Based Tool for Supporting Bioinformatical Classification Problems. Accepted to be published in: Proc. of FH Science Day Steyr. 2005.

S. Winkler, M. Affenzeller, S. Wagner. Genetic Programming Based Model Structure Identification Using On-Line System Data. Accepted to be published in: Proc. of Conceptual Modeling and Simulation Conf. (CMS'05). 2005.

M. Affenzeller. Population Genetics and Evolutionary Computation: Theoretical and Practical Aspects. Schriften der Johannes Kepler Universität Linz, Reihe C: Technik und Naturwissenschaften. Universitätsverlag Rudolf Trauner, 2005. ISBN 3-85487-823-0.

S. Wagner, M. Affenzeller. The Allele Meta-Model - Developing a Common Language for Genetic Algorithm. In Proc. 1st Intl. Work-Conf. on the Interplay between Natural and Artificial Computation (IWINAC'05), 2005.

M. Affenzeller, S. Wagner, S. Winkler. GA-Selection Revisited from an ES-Driven Point of View. In Proc. 1st Intl. Work-Conf. on the Interplay between Natural and Artificial Computation (IWINAC'05), 2005.

M. Affenzeller, S. Wagner, S. Winkler. Goal-Oriented Preservation of Essential Genetic Information by Offspring Selection. In Proc. Genetic and Evolutionary Computation Conf. (GECCO'05), 2005.

R. Braune, S. Wagner, M. Affenzeller. On the Analysis of Crossover Schemes for Genetic Algorithms Applied to the Job Shop Scheduling Problem. In Proc. 9th World Multi-Conference on Systemics, Cybernetics and Informatics (WMSCI'05), 2005.

S. Winkler, M. Affenzeller, S. Wagner. Solving Multiclass Classification Problems by Genetic Programming. In Proc. 9th World Multi-Conference on Systemics, Cybernetics and Informatics (WMSCI'05), 2005.

S. Wagner, M. Affenzeller. SexualGA: Gender-Specifc Selection for Genetic Algorithms. In Proc. 9th World Multi-Conference on Systemics, Cybernetics and Informatics (WMSCI'05), 2005.

M. Affenzeller, S. Winkler, S. Wagner. A New Genetic-Programming-Based Machine Learning Algorithm. In Proc. 9th World Multi-Conference on Systemics, Cybernetics and Informatics (WMSCI'05), 2005.

L. del Re, P. Langthaler, C. Furtmüller, S. Winkler, M. Affenzeller. NOx Virtual Sensor Based on Structure Identification and Global Optimization. In Proc. SAE World Congress (SAE'05), paper number 1005-01-0050, 2005.

M. Affenzeller, S. Wagner. Offspring Selection: A New Self-Adaptive Selection Scheme for Genetic Algorithms. In Proc. of the Intl. Conf. on Adaptive and Natural Computing Algorithms (ICANNGA'05), Springer Computer Science, Springer 2005.

S. Wagner, M. Affenzeller. HeuristicLab: A Generic and Extensible Optimization Environment. In Proc. of the Intl. Conf. on Adaptive and Natural Computing Algorithms (ICANNGA'05), Springer Computer Science, Springer 2005.

2004

Publications in Formal Methods in 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.

Publications in Heuristic Optimization in 2004

S. Wagner, M. Affenzeller HeuristicLab Grid - A Flexible and Extensible Environment for Parallel Heuristic Optimization. Journal of Systems Science, vol. 30, number 4, Oficyna Wydawnicza Politechniki Wroclawskiej, 2004.

M. Affenzeller, S. Wagner. The Influence of Population Genetics for the Redesign of Genetic Algorithms. Journal of Systems Science, vol. 30, number 4, Oficyna Wydawnicza Politechniki Wroclawskiej, 2004.

M. Affenzeller, S. Wagner. SASEGASA: A New Generic Parallel Evolutionary Algorithm for Achieving Highest Quality Results. Journal of Heuristics - Special Issue on New Advances on Parallel Meta-Heuristics for Complex Problems, vol. 10, pp. 239-263, Kluwer Academic Publishers, 2004.

M. Affenzeller, S. Wagner. Reconsidering the Selection Concept of Genetic Algorithms from a Population Genetics Inspired Point of View. Cybernetics and Systems 2004, pp. 701-706. Austrian Society for Cybernetic Studies, 2004.

S. Wagner, M. Affenzeller, D. Schragl. Traps and Dangers when Modelling Problems for Genetic Algorithms. Cybernetics and Systems 2004, pp. 79-84. Austrian Society for Cybernetic Studies, 2004.

R. Braune, S. Wagner, M. Affenzeller. Applying Genetic Algorithms to the Optimization of Production Planning in a Real-World Manufacturing Environment. Cybernetics and Systems 2004, pp. 41-46. Austrian Society for Cybernetic Studies, 2004.

S. Winkler, M. Affenzeller, S. Wagner. Identifying Nonlinear Model Structures Using Genetic Programming Techniques. Cybernetics and Systems 2004, pp. 689-694. Austrian Society for Cybernetic Studies, 2004.

M. Affenzeller, S. Wagner. The Influence of Population Genetics for the Redesign of Genetic Algorithms. Proc. of the 15th Intl. Conf. on Systems Science, vol. 3, pp. 53-60. Oficyna Wydawnicza Politechniki Wroclawskiej, 2004.

S. Wagner, M. Affenzeller. HeuristicLab Grid - A Flexible and Extensible Environment for Parallel Heuristic Optimization. Proc. of the 15th Intl. Conf. on Systems Science, vol. 1, pp. 289-296. Oficyna Wydawnicza Politechniki Wroclawskiej, 2004.

S. Winkler, M. Affenzeller, S. Wagner. New Methods for the Identification of Nonlinear Model Structures Based Upon Genetic Programming Techniques. Proc. of the 15th Intl. Conf. on Systems Science, vol. 1, pp. 386-393. Oficyna Wydawnicza Politechniki Wroclawskiej, 2004.

G. Weichhart, M. Affenzeller, A. Reitbauer, S. Wagner. (Modelling of an Agent-Based Schedule Optimisation System. Accepted to be published in: Proc. of the IMS Intl. Forum 2004, 2004.

S. Wagner, M. Affenzeller. The HeuristicLab Optimization Environment. Technical Report. Institute of Formal Models and Verification, Johannes Kepler University Linz, Austria, 2004.