[ 10 | 09 | 08 | 07 | 06 | 05 | 04 ]

Publications of current members: [ Biere | Brummayer | Lonsing ]

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

Earlier publications by members of FMV can either be found at the publications page of Prof. Armin Biere.

Other publications can be found on the list of publications of the HeuristicLab, or among the links of the publication page of the predecessor institute.

2010

M. Järvisalo, A. Biere, M. Heule. Blocked Clause Elimination. To appear in Proc. 16th Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'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), 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, 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.

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

[ formal-methods | heuristic-optimization ]

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

[ formal-methods | heuristic-optimization ]

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.