[  20 | 19 | 18 | 17 | 16 | 15 | 14 | 13 | 12 | 11 ]

Selected Publications Martina Seidl

2020

David Cerna, Martina Seidl, Wolfgang Schreiner, Wolfgang Windsteiger. Computational Logic in the First Semester of Computer Science: An Experience Report. In Proc. 12th Intl. Conf. on Computer Supported Education (CSEDU'20), pages 374-381, SCITEPRESS 2020.
[ preprint | bibtex ]

David Cerna, Martina Seidl, Wolfgang Schreiner, Wolfgang Windsteiger. Aiding an Introduction to Formal Reasoning Within a First-Year Logic Course for CS Majors Using a Mobile Self-Study App. In Proc. Proc. ACM Conf. on Innovation and Technology in Computer Science Education (ITiCSE'20), pages 61-67, ACM 2020.
[ preprint | bibtex ]

2019

Luca Pulina, Martina Seidl. The 2016 and 2017 QBF solvers evaluations (QBFEVAL'16 and QBFEVAL'17). Artif. Intell. 274: 224-248, 2019.
[ paper | bibtex ]

Marijn Heule, Manuel Kauers, Martina Seidl: A family of schemes for multiplying 3 × 3 matrices with 23 coefficient multiplications. ACM Comm. Computer Algebra 53(3): 118-12, 2019.
[ paper | bibtex ]

Marijn J. H. Heule, Manuel Kauers, Martina Seidl. Local Search for Fast Matrix Multiplication. SAT 2019: 155-163, Lecture Notes in Computer Science, 2019.
[ paper | bibtex | arXiv | supplementary material ]

Benjamin Kiesl, Martina Seidl. QRAT Polynomially Simulates forall-Exp+Res. SAT 2019: 193-202, Lecture Notes in Computer Science, 2019.
[ paper | bibtex ]

Ankit Shukla, Armin Biere, Luca Pulina, Martina Seidl. A Survey on Applications of Quantified Boolean Formulas. Proceedings of the 31st International Conference on Tools with Artificial Intelligence
[ paper | bibtex ]

Luca Pulina, Martina Seidl. Notes from the Guest Editors. Special Volume on SAT 2018 Competitive Events, Journal on Satisfiability, Boolean Modeling and Computation - Volume 11, issue 1, 2019.
[ IOS Press ]

2018

Manuel Kauers, Martina Seidl. Symmetries of Quantified Boolean Formulas. Proc. of the 21th Int. Conf. on Theory and Applications of Satisfiability Testing (SAT 2018), Lecture Notes in Computer Science vol. 10491, Springer, pages 199-2016, 2018.
[ paper | bibtex | arXiv ]

Manuel Kauers, Martina Seidl. Short proofs for some symmetric Quantified Boolean Formulas. Information Processing Letters 140:4-7 2018.
[ paper | bibtex | arXiv ]

Florian Lonsing, Martina Seidl. Parallel Solving of Quantified Boolean Formulas. Handbook of Parallel Constraint Reasoning, pages 101-139, Springer, 2018.
[ bibtex ]

Martina Seidl, Steffen Zschaler. Software Technologies: Applications and Foundations: STAF 2017 Collocated Workshops, Marburg, Germany, July 17-21, 2017, Revised Selected Papers. Lecture Notes in Computer Science, volume 10748, 2018.
[ front matter | bibtex ]

Roderick Bloem, Nicolas Braud-Santoni, Vedad Hadzic, Uwe Egly, Florian Lonsing, Martina Seidl. Expansion-Based QBF Solving Without Recursion FMCAD 2018.
[ paper | arXiv ]

Benjamin Kiesl, Martina Seidl, Hans Tompits, Armin Biere. Local Redundancy in SAT: Generalizations of Blocked Clauses. Logical Methods in Computer Science, vol. 9, issue 4:3, pages 1-23, https://lmcs.episciences.org 2018.
[ paper | bibtex ]

2017

Best paper
Marijn Heule, Benjamin Kiesl, Martina Seidl, Armin Biere. PRuning Through Satisfaction. In Proc. 13th Haifa Verification Conference (HVC'17), Lecture Notes in Computer Science (LNCS) vol. 10629, pages 179-194, Springer 2017.
[ paper | bibtex | experiments ]

Katalin Fazekas, Marijn J. H. Heule, Martina Seidl, Armin Biere. Skolem Function Continuation for Quantified Boolean Formulas. Proc. 11th Intl. Conf. on Tests and Proofs (TAP'17). Lecture Notes in Computer Science vol. 10375, Springer, pages 129-138, 2017.
[ paper | bibtex | tool ]

Benjamin Kiesl, Martin Suda, Martina Seidl, Hans Tompits, Armin Biere. Blocked Clauses in First-Order Logic. Proc. 21st Intl. Conf. on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-21). EPiC Series in Computing vol. 46, Easychair, pages 31-48, 2017.
[ preliminary extended version | arxiv | EasyChair | bibtex ]

Benjamin Kiesl, Marijn J. H. Heule, Martina Seidl. A Little Blocked Literal Goes a Long Way. Proc. of the 20th Int. Conf. on Theory and Applications of Satisfiability Testing (SAT 2017), Lecture Notes in Computer Science vol. 10491, Springer, pages 281-297, 2017.
[ paper | bibtex ]

Benjamin Kiesl, Martina Seidl, Hans Tompits, Armin Biere. Blockedness in Propositional Logic: Are You Satisfied With Your Neighborhood? Proc. 26th Intl. Joint Conf. on Artificial Intelligence (IJCAI'17). ijcai.org, pages 4884-4888, 2017.
[ paper | bibtex ]

Swen Jacobs, Roderick Bloem, Romain Brenguier, Rüdiger Ehlers, Timotheus Hell, Robert Könighofer, Guillermo A. Pérez, Jean-François Raskin, Leonid Ryzhyk, Ocan Sankur, Martina Seidl, Leander Tentrup, Adam Walker. The First Reactive Synthesis Competition (SYNTCOMP 2014). Int. Journal on Software Tools for Technology Transfer (STTT) , 19(3), pages 367-390, June 2017.
[ preprint | bibtex | arxiv ]

Sebastian Gabmeyer, Petra Kaufmann, Martina Seidl, Martin Gogolla, Gerti Kappel. A feature-based classification of formal verification techniques for software models. Software & Systems Modeling, pages 1-26, online first, March 2017.
[ preprint | bibtex ]

Marijn Heule, Martina Seidl, Armin Biere. Validation and Extraction for QBF Preprocessing. Journal of Automated Reasoning, 58(1), pages 97-125, Springer 2017.
[ preprint | bibtex ]

2016

Katalin Fazekas, Martina Seidl, Armin Biere. A Duality-Aware Calculus for Quantified Boolean Formulas. In Proc. 18th Intl. Symp. on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'16), pages 181-186, IEEE Computer Society, 2016.
[ paper | bibtex ]

Swen Jacobs, Roderick Bloem, Romain Brenguier, Ayrat Khalimov, Felix Klein, Robert Könighofer, Jens Kreber, Alexander Legg, Nina Narodytska, Guillermo A. Pérez, Jean-François Raskin, Leonid Ryzhyk, Ocan Sankur, Martina Seidl, Leander Tentrup, Adam Walker. The 3rd Reactive Synthesis Competition (SYNTCOMP 2016): Benchmarks, Participants & Results. SYNT@CAV 2016: 149-177, 2016.
[ arxiv | bibtex ]

Roderick Bloem, Uwe Egly, Patrick Klampfl, Robert Könighofer, Florian Lonsing, Martina Seidl. Satisfiability-Based Methods for Reactive Synthesis from Safety Specifications. CoRR abs/1604.06204, 2016.
[ arxiv | bibtex ]

Florian Lonsing, Martina Seidl. Proceedings of the 4th International Workshop on Quantified Boolean Formulas (QBF 2016). In CEUR Workshop Proceedings 1719, CEUR-WS.org 2016.
[ proceedings | bibtex ]

Sebastian Gabmeyer, Martina Seidl. Lightweight Symbolic Verification of Graph Transformation Systems with Off-the-Shelf Hardware Model Checkers. In Proc. 10th Intl. Conf. on Tests & Proofs (TAP'16), Lecture Notes in Computer Science (LNCS) vol. 9762, pages 94-111, Springer 2016.
[ paper | bibtex ]

Florian Lonsing, Uwe Egly, Martina Seidl. Q-Resolution with Generalized Axioms. In Proc. 19th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'16), Lecture Notes in Computer Science (LNCS) vol. 9710, 435-452, Springer 2016.
[ paper | bibtex | arxiv ]

Benjamin Kiesl, Martina Seidl, Hans Tompits, Armin Biere. Super-Blocked Clauses. In Proc. 8th Joint Conf. on Automated Reasoning (IJCAR'16), Lecture Notes in Computer Science (LNCS) vol. 9706, 45-61, Springer 2016.
[ paper | bibtex ]

Mikolas Janota, Charles Jordan, Will Klieber, Florian Lonsing, Martina Seidl, Allen Van Gelder. The QBFGallery 2014: The QBF Competition at the FLoC Olympic Games. Journal of Satisfiability, Boolean Modeling and Computation (JSAT), vol. 9, pages 187-206, 2014 (published 2016), IOS Press.
[ paper | bibtex ]

Florian Lonsing, Martina Seidl, Allen Van Gelder. The QBF Gallery: Behind the scenes. In Artificial Intelligence 237:92-114 , 2016
[ paper | bibtex | arxiv ]

Charles Jordan, William Klieber, Martina Seidl. Non-CNF QBF Solving with QCIR. In AAAI-16 Workshop on Beyond NP, 7 pages, 2016.
[ paper | bibtex ]

2015

Florian Lonsing, Fahiem Bacchus, Armin Biere, Uwe Egly and Martina Seidl: Enhancing Search-Based QBF Solving by Dynamic Blocked Clause Elimination. In Proc. 20th Intl. Conf. on Logic for Programming , Artificial Intelligence, and Reasoning 2015 (LPAR-20), Lecture Notes in Computer Science (LNCS) vol. 9450, pages 418-433, Springer 2015.

IJCAI-JAIR 2019 Award
Marijn Heule, Matti Järvisalo, Florian Lonsing, Martina Seidl, Armin Biere.
Clause Elimination for SAT and QSAT.
Journal of Artificial Intelligence Research (JAIR).
vol. 53, pages 127-168, 2015.
[ link | preprint | bibtex | lingeling | bloqqer | award ]

Marijn Heule, Martina Seidl, Armin Biere. Blocked Literals are Universal. In Proc. 7th Intl. Symp. NASA Formal Methods (NFM'15), Lecture Notes in Computer Science (LNCS), vol. 9058, pages 436 - 442, Springer 2015.

Martina Seidl, Marion Scholz, Christian Huemer, Gerti Kappel: UML @ Classroom - An Introduction to Object-Oriented Modeling. Undergraduate Topics in Computer Science, Springer 2015, ISBN 978-3-319-12741-5, pp. 1-194

Petra Kaufmann, Martin Kronegger, Andreas Pfandler, Martina Seidl, Magdalena Widl: Intra- and interdiagram consistency checking of behavioral multiview models (Preprint). Computer Languages, Systems & Structures 44: 72-88 (2015)

Michalis Famelis, Daniel Ratiu, Martina Seidl, Gehan M. K. Selim: Proceedings of the 12th Workshop on Model-Driven Engineering, Verification and Validation co-located with ACM/IEEE 18th International Conference on Model Driven Engineering Languages and Systems, MoDeVVa@MoDELS 2015, Ottawa, Canada, September 29, 2015. CEUR Workshop Proceedings 1514, CEUR-WS.org 2015

Swen Jacobs, Roderick Bloem, Romain Brenguier, Rüdiger Ehlers, Timotheus Hell, Robert Könighofer, Guillermo A. Pérez, Jean-François Raskin, Leonid Ryzhyk, Ocan Sankur, Martina Seidl, Leander Tentrup, Adam Walker: The First Reactive Synthesis Competition (SYNTCOMP 2014). CoRR abs/1506.08726 (2015)

Florian Lonsing, Martina Seidl, Allen Van Gelder: The QBF Gallery: Behind the Scenes. CoRR abs/1508.01045 (2015)

Martina Seidl: Contributions to Rigorous Software Engineering: Models and Reasoning in the Context of Formal Verification. Habilitation Thesis, Johannes Kepler University Linz (Submitted), 2015

Cyrille Artho, Martina Seidl, Quentin Gros, Eun-Hye Choi, Takashi Kitamura, Akira Mori, Rudolf Ramler, Yoriyuki Yamagata: Model-based testing of stateful APIs with Modbat (Preprint). Proceddings of the 2015 30th IEEE/ACM International Conference on Automated Software Engineering (ASE 2015), pages 858-863, DOI 10.1109/ASE.2015.95, IEEE, November, 2015.

2014

Marijn Heule, Martina Seidl, Armin Biere. Efficient Extraction of Skolem Functions from QRAT Proofs. In Proc. 14th Intl. Conf. on Formal Methods in Computer Aided Design (FMCAD'14), 107-114, FMCAD Inc. 2014.

Marijn Heule, Martina Seidl, Armin Biere. A Unified Proof System for QBF Preprocessing, In Proc. 7th Joint Conf. on Automated Reasoning (IJCAR'14), Lecture Notes in Computer Science (LNCS) vol. 8562, 91-106, Springer 2014.

Petra Kaufmann, Martin Kronegger, Andreas Pfandler, Martina Seidl, Magdalena Widl: A SAT-Based Debugging Tool for State Machines and Sequence Diagrams. Best paper at the Int. Conf. on Software Language Engineering, Lecture Notes in Computer Science (SLE 2014), Lecture Notes in Computer Science, Volume 8706, 21-40, Springer, 2014.

Robert Bill, Sebastian Gabmeyer, Petra Kaufmann, Martina Seidl: Model Checking of CTL-Extended OCL Specifications. Proc. of the Int. Conf. on Software Language Engineering, Lecture Notes in Computer Science (SLE 2014), Lecture Notes in Computer Science, Volume 8706, 221-240, Springer, 2014.

Martina Seidl, Nikolai Tillmann (Eds.): Tests and Proofs - 8th International Conference (TAP 2014), Lecture Notes in Computer Science 8570, Springer 2014, ISBN 978-3-319-09098-6.

M. Seidl, R. Könighofer: Partial witnesses from preprocessed quantified Boolean formulas. Proc. of the Int. Design, Automation & Test in Europe Conference & Exhibition (DATE 2014): 1-6, IEEE, 2014.

R. Bloem, R. Könighofer, M. Seidl: SAT-Based Synthesis Methods for Safety Specs. Proc. of the 15th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2014), 20 pages, Lecture Notes in Computer Science (LNCS), Springer, 2014.

C. Jordan, L. Kaiser, F. Lonsing, M. Seidl: MPIDepQBF: Towards Parallel QBF Solving without Knowledge Sharing. In Proc. 17th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'14), Lecture Notes in Computer Science (LNCS) vol. 8561, 430-437, Springer 2014.

2013

Cyrille Artho, Armin Biere, Masami Hagiya, Eric Platon, Martina Seidl, Yoshinori Tanabe, Mitsuharu Yamamoto. Modbat: A Model-based API Tester for Event-driven Systems. In Proc. Haifa Verification Conference (HVC'13), Lecture Notes in Computer Science (LNCS) vol. 8244, pages 112-128, Springer 2013.

Cyrille Artho, Armin Biere, Martina Seidl. Model-Based Testing for Verification Backends. In Proc. 7th Intl. Conf. on Tests & Proofs (TAP'13), Lecture Notes in Computer Science (LNCS) vol. 7942, pages 39-55, Springer 2013.

Alexandra Goultiaeva, Martina Seidl, Armin 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

Magdalena Widl, Armin Biere, Petra Brosch, Uwe Egly, Marijn Heule, Gerti Kappel, Martina Seidl, Hans 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.

Aina Niemetz, Mathias Preiner, Florian Lonsing, Martina Seidl, Armin 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.
[ paper | bibtex | qbfcert ]

N. Creignou, U. Egly, M. Seidl: A Framework for the Specification of Random SAT and QSAT Formulas. Proc. of the 6th International Conference on Tests and Proofs (TAP 2012), Lecture Notes in Computer Science (LNCS), Springer, 6 pages, 2012

P. Brosch, U. Egly, S. Gabmeyer, G. Kappel, M. Seidl, H. Tompits, M. Widl, M. Wimmer: Towards Scenario-Based Testing of UML Diagrams, Proc. of the 6th International Conference on Tests and Proofs (TAP 2012), Lecture Notes in Computer Science (LNCS), Springer, 6 pages, 2012

2011

Armin Biere, Florian Lonsing, Martina 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.