Siert Wieringa

Researcher, Master of Science

Postal Address: Aalto University
Department of Information and Computer Science
P.O.Box 15400
FI-00076 Aalto
FINLAND
Street Address: Konemiehentie 2, Otaniemi, Espoo
Office: Room T-B252
Email: siert.wieringaATaalto.fi
Research interests: Boolean satisfiability (SAT), SAT-based model checking,
Parallel SAT, Incremental SAT, Unsatisfiable core extraction

Publications

Siert Wieringa and Keijo Heljanko, Concurrent Clause Strengthening, accepted for presentation at the 16th International Conference on Theory and Applications of Satisfiability Testing (SAT 2013)

Siert Wieringa and Keijo Heljanko, Asynchronous Multi-Core Incremental SAT solving, in proceedings of 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2013)

Siert Wieringa, Understanding, improving and parallelizing MUS finding using model rotation, in proceedings of Eighteenth Conference on Principles and Practice of Constraint Programming (CP2012), 2012. (PDF)

Marijn J.H. Heule, Oliver Kullmann, Siert Wieringa and Armin Biere, Cube and Conquer: Guiding CDCL SAT Solvers by Lookaheads, in proceedings of Haifa Verification Conference 2011 (HVC 2011).

Siert Wieringa, On Incremental Satisfiability and Bounded Model Checking, in proceedings of First International Workshop on Design and Implementation of Formal Tools and Systems (DIFTS11), 2011. (PDF)

Siert Wieringa, Matti Niemenmaa and Keijo Heljanko, Tarmo: A Framework for Parallelized Bounded Model Checking, In Lubos Brim and Jaco van de Pol, editors, Proceedings of the 8th International Workshop on Parallel and Distributed Methods in verifiCation (PDMC09), volume 14 of Electronic Proceedings in Theoretical Computer Science (EPTCS), pages 62-76, 2009.

Hans van Maaren and Siert Wieringa, Finding guaranteed MUSes fast, In H. Kleine Büning and X. Zhao (Eds.): Proceedings of SAT2008, LNCS 4996, pp. 291-304, Springer, Heidelberg (2008).

Recent software

Current versions of my software can be found on BitBucket

Resources and legacy software

SAT13 - Resources for the article Concurrent Clause Strengthening.

TACAS13 - Resources for the article Asynchronous Multi-Core Incremental SAT solving.

iCNF - Is a file format for sequences of incrementally encoded SAT instances.

DIFTS11 - Resources for the article On Incremental Satisfiability and Bounded Model Checking.

MiniUnsat - A tool for extracting minimal unsatisfiable subsets (MUS) from unsatisfiable CNF formulas.