Martina Seidl

Proceedings of the 18th International Working Conference on Variability Modelling of Software-Intensive Systems, 2024

2023

Search-Space Pruning with Int-Splits for Faster QBF Solving.

[BibT_eX]

[DOI]

CoRR, 2023

ParaQooba: A Fast and Flexible Framework for Parallel and Distributed QBF Solving.

[BibT_eX]

[DOI]

Maximilian Heisinger

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2023

Validation of QBF Encodings with Winning Strategies.

[BibT_eX]

[DOI]

Proceedings of the 26th International Conference on Theory and Applications of Satisfiability Testing, 2023

QMusExt: A Minimal (Un)satisfiable Core Extractor for Quantified Boolean Formulas.

[BibT_eX]

[DOI]

Andreas Plank

Proceedings of the 26th International Conference on Theory and Applications of Satisfiability Testing, 2023

Never Trust Your Solver: Certification for SAT and QBF.

[BibT_eX]

[DOI]

Proceedings of the Intelligent Computer Mathematics - 16th International Conference, 2023

True Crafted Formula Families for Benchmarking Quantified Satisfiability Solvers.

[BibT_eX]

[DOI]

Simone Heisinger

Proceedings of the Intelligent Computer Mathematics - 16th International Conference, 2023

Enumerative Level-2 Solution Counting for Quantified Boolean Formulas (Short Paper).

[BibT_eX]

[DOI]

Andreas Plank

Sibylle Möhle

Proceedings of the 29th International Conference on Principles and Practice of Constraint Programming, 2023

2022

What's New In QBF Solving? : (Invited Talk).

[BibT_eX]

[DOI]

Proceedings of the 24th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2022

FERPModels: A Certification Framework for Expansion-Based QBF Solving.

[BibT_eX]

[DOI]

Proceedings of the 24th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2022

QuAPI: Adding Assumptions to Non-Assuming SAT & QBF Solvers.

[BibT_eX]

[DOI]

Maximilian Heisinger

Proceedings of the Workshop on Practical Aspects of Automated Reasoning Co-located with the 11th International Joint Conference on Automated Reasoning (FLoC/IJCAR 2022), Haifa, Israel, August, 11, 2022

OuterCount: A First-Level Solution-Counter for Quantified Boolean Formulas.

[BibT_eX]

[DOI]

Proceedings of the Intelligent Computer Mathematics - 15th International Conference, 2022

2021

Quantified Boolean Formulas.

[BibT_eX]

[DOI]

Proceedings of the Handbook of Satisfiability - Second Edition, 2021

Beyond Uniform Equivalence between Answer-set Programs.

[BibT_eX]

[DOI]

ACM Trans. Comput. Log., 2021

New ways to multiply 3 × 3-matrices.

[BibT_eX]

[DOI]

J. Symb. Comput., 2021

Two SAT solvers for solving quantified Boolean formulas with an arbitrary number of quantifier alternations.

[BibT_eX]

[DOI]

Roderick Bloem

Nicolas Braud-Santoni

Formal Methods Syst. Des., 2021

QBFFam: A Tool for Generating QBF Families from Proof Complexity.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2021, 2021

2020

Aiding an Introduction to Formal Reasoning Within a First-Year Logic Course for CS Majors Using a Mobile Self-Study App.

[BibT_eX]

[DOI]

Proceedings of the 2020 ACM Conference on Innovation and Technology in Computer Science Education, 2020

Computational Logic in the First Semester of Computer Science: An Experience Report.

[BibT_eX]

[DOI]

Proceedings of the 12th International Conference on Computer Supported Education, 2020

2019

A feature-based classification of formal verification techniques for software models.

[BibT_eX]

[DOI]

Softw. Syst. Model., 2019

Notes from the Guest Editors.

[BibT_eX]

[DOI]

Luca Pulina

J. Satisf. Boolean Model. Comput., 2019

New ways to multiply 3 x 3-matrices.

[BibT_eX]

[DOI]

CoRR, 2019

On the maximal minimal cube lengths in distinct DNF tautologies.

[BibT_eX]

[DOI]

Doron Zeilberger

CoRR, 2019

A family of schemes for multiplying 3 × 3 matrices with 23 coefficient multiplications.

[BibT_eX]

[DOI]

ACM Commun. Comput. Algebra, 2019

The 2016 and 2017 QBF solvers evaluations (QBFEVAL'16 and QBFEVAL'17).

[BibT_eX]

[DOI]

Luca Pulina

Artif. Intell., 2019

QRAT Polynomially Simulates ∀ \text -Exp+Res.

[BibT_eX]

[DOI]

Benjamin Kiesl

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2019, 2019

Local Search for Fast Matrix Multiplication.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2019, 2019

A Survey on Applications of Quantified Boolean Formulas.

[BibT_eX]

[DOI]

Proceedings of the 31st IEEE International Conference on Tools with Artificial Intelligence, 2019

A Framework for Model Checking Against CTLK Using Quantified Boolean Formulas.

[BibT_eX]

[DOI]

Emily Yu

Proceedings of the Formal Techniques for Safety-Critical Systems, 2019

2018

Local Redundancy in SAT: Generalizations of Blocked Clauses.

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2018

Short proofs for some symmetric Quantified Boolean Formulas.

[BibT_eX]

[DOI]

Inf. Process. Lett., 2018

Symmetries of Quantified Boolean Formulas.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2018, 2018

Expansion-Based QBF Solving Without Recursion.

[BibT_eX]

[DOI]

Roderick Bloem

Nicolas Braud-Santoni

Proceedings of the 2018 Formal Methods in Computer Aided Design, 2018

Parallel Solving of Quantified Boolean Formulas.

[BibT_eX]

[DOI]

Proceedings of the Handbook of Parallel Constraint Reasoning., 2018

2017

The first reactive synthesis competition (SYNTCOMP 2014).

[BibT_eX]

[DOI]

Int. J. Softw. Tools Technol. Transf., 2017

Solution Validation and Extraction for QBF Preprocessing.

[BibT_eX]

[DOI]

J. Autom. Reason., 2017

Skolem Function Continuation for Quantified Boolean Formulas.

[BibT_eX]

[DOI]

Proceedings of the Tests and Proofs - 11th International Conference, 2017

A Little Blocked Literal Goes a Long Way.

[BibT_eX]

[DOI]

Benjamin Kiesl

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2017 - 20th International Conference, Melbourne, VIC, Australia, August 28, 2017

Blocked Clauses in First-Order Logic.

[BibT_eX]

[DOI]

Proceedings of the LPAR-21, 2017

Blockedness in Propositional Logic: Are You Satisfied With Your Neighborhood?

[BibT_eX]

[DOI]

Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, 2017

PRuning Through Satisfaction.

[BibT_eX]

[DOI]

Proceedings of the Hardware and Software: Verification and Testing, 2017

2016

The 3rd Reactive Synthesis Competition (SYNTCOMP 2016): Benchmarks, Participants & Results.

[BibT_eX]

[DOI]

Proceedings of the Proceedings Fifth Workshop on Synthesis, 2016

Satisfiability-Based Methods for Reactive Synthesis from Safety Specifications.

[BibT_eX]

[DOI]

CoRR, 2016

The QBF Gallery: Behind the scenes.

[BibT_eX]

[DOI]

Allen Van Gelder

Artif. Intell., 2016

Lightweight Symbolic Verification of Graph Transformation Systems with Off-the-Shelf Hardware Model Checkers.

[BibT_eX]

[DOI]

Sebastian Gabmeyer

Proceedings of the Tests and Proofs - 10th International Conference, 2016

A Duality-Aware Calculus for Quantified Boolean Formulas.

[BibT_eX]

[DOI]

Katalin Fazekas

Proceedings of the 18th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2016

Q-Resolution with Generalized Axioms.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2016, 2016

Super-Blocked Clauses.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning - 8th International Joint Conference, 2016

Non-CNF QBF Solving with QCIR.

[BibT_eX]

[DOI]

Charles Jordan

Will Klieber

Proceedings of the Beyond NP, 2016

2015

UML @ Classroom - An Introduction to Object-Oriented Modeling

[BibT_eX]

[DOI]

Undergraduate Topics in Computer Science, Springer, ISBN: 978-3-319-12742-2, 2015

Clause Elimination for SAT and QSAT.

[BibT_eX]

[DOI]

J. Artif. Intell. Res., 2015

The Second Reactive Synthesis Competition (SYNTCOMP 2015).

[BibT_eX]

[DOI]

Proceedings of the Proceedings Fourth Workshop on Synthesis, 2015

Intra- and interdiagram consistency checking of behavioral multiview models.

[BibT_eX]

[DOI]

Comput. Lang. Syst. Struct., 2015

Blocked Literals Are Universal.

[BibT_eX]

[DOI]

Proceedings of the NASA Formal Methods - 7th International Symposium, 2015

UML@Classroom: An Introduction to Object-Oriented Modeling.

[BibT_eX]

[DOI]

Proceedings of the MODELS Educators Symposium co-located with the ACM/IEEE 18th International Conference on Model Driven Engineering Languages and Systems (MODELS 2015), 2015

Enhancing Search-Based QBF Solving by Dynamic Blocked Clause Elimination.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2015

Model-Based Testing of Stateful APIs with Modbat.

[BibT_eX]

[DOI]

Proceedings of the 30th IEEE/ACM International Conference on Automated Software Engineering, 2015

2014

The QBFGallery 2014: The QBF Competition at the FLoC Olympic Games.

[BibT_eX]

[DOI]

J. Satisf. Boolean Model. Comput., 2014

SAT-Based Synthesis Methods for Safety Specs.

[BibT_eX]

[DOI]

Roderick Bloem

Robert Könighofer

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2014

MocOCL: A Model Checker for CTL-Extended OCL Specifications.

[BibT_eX]

[DOI]

Proceedings of the Third International Workshop on Verification of Model Transformations co-located with Software Technologies: Applications and Foundations, 2014

A SAT-Based Debugging Tool for State Machines and Sequence Diagrams.

[BibT_eX]

[DOI]

Proceedings of the Software Language Engineering - 7th International Conference, 2014

Model Checking of CTL-Extended OCL Specifications.

[BibT_eX]

[DOI]

Proceedings of the Software Language Engineering - 7th International Conference, 2014

MPIDepQBF: Towards Parallel QBF Solving without Knowledge Sharing.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2014, 2014

Efficient extraction of Skolem functions from QRAT proofs.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods in Computer-Aided Design, 2014

Partial witnesses from preprocessed quantified Boolean formulas.

[BibT_eX]

[DOI]

Robert Könighofer

Proceedings of the Design, Automation & Test in Europe Conference & Exhibition, 2014

A Unified Proof System for QBF Preprocessing.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning - 7th International Joint Conference, 2014

2013

Semantics-Aware Versioning Challenge: Merging Sequence Diagrams along with State Machine Diagrams.

[BibT_eX]

[DOI]

Magdalena Widl

Softwaretechnik-Trends, 2013

A posteriori operation detection in evolving software models.

[BibT_eX]

[DOI]

Philip Langer

Manuel Wimmer

Markus Herrmannsdörfer

Konrad Wieland

Gerti Kappel

J. Syst. Softw., 2013

Turning Conflicts into Collaboration.

[BibT_eX]

[DOI]

Comput. Support. Cooperative Work., 2013

Model-Based Testing for Verification Back-Ends.

[BibT_eX]

[DOI]

Cyrille Artho

Proceedings of the Tests and Proofs - 7th International Conference, 2013

Making UML "hip": A First Experience Report on Using Modern Teaching Tools for Object-Oriented Modelling.

[BibT_eX]

[DOI]

Marion Scholz

Petra Kaufmann

Proceedings of the Educators' Symposium co-located with ACM/IEEE 16th International Conference on Model Driven Engineering Languages and Systems (MODELS 2013), 2013

Global State Checker: Towards SAT-Based Reachability Analysis of Communicating State Machines.

[BibT_eX]

[DOI]

Proceedings of the 10th International Workshop on Model Driven Engineering, 2013

Research Questions for Validation and Verification in the Context of Model-Based Engineering.

[BibT_eX]

[DOI]

Proceedings of the 10th International Workshop on Model Driven Engineering, 2013

OCL meets CTL: Towards CTL-Extended OCL Model Checking.

[BibT_eX]

[DOI]

Proceedings of the MODELS 2013 OCL Workshop co-located with the 16th International ACM/IEEE Conference on Model Driven Engineering Languages and Systems (MODELS 2013), 2013

Modbat: A Model-Based API Tester for Event-Driven Systems.

[BibT_eX]

[DOI]

Cyrille Valentin Artho

Proceedings of the Hardware and Software: Verification and Testing, 2013

Bridging the gap between dual propagation and CNF-based QBF solving.

[BibT_eX]

[DOI]

Alexandra Goultiaeva

Proceedings of the Design, Automation and Test in Europe, 2013

2012

Generic vs. Language-Specific Model Versioning - Adaptability to the Rescue.

[BibT_eX]

[DOI]

Softwaretechnik-Trends, 2012

On formalizing EMF modeling operations with graph transformations.

[BibT_eX]

[DOI]

ACM SIGSOFT Softw. Eng. Notes, 2012

Conflict Visualization for Evolving UML Models.

[BibT_eX]

[DOI]

J. Object Technol., 2012

A Framework for the Specification of Random SAT and QSAT Formulas.

[BibT_eX]

[DOI]

Nadia Creignou

Proceedings of the Tests and Proofs - 6th International Conference, 2012

Towards Scenario-Based Testing of UML Diagrams.

[BibT_eX]

[DOI]

Proceedings of the Tests and Proofs - 6th International Conference, 2012

Guided Merging of Sequence Diagrams.

[BibT_eX]

[DOI]

Proceedings of the Software Language Engineering, 5th International Conference, 2012

An Introduction to Model Versioning.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods for Model-Driven Engineering, 2012

Resolution-Based Certificate Extraction for QBF - (Tool Presentation).

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2012, 2012

Replacing traditional classroom lectures with lecture videos: an experience report.

[BibT_eX]

[DOI]

Proceedings of the 8th edition of the Educators' Symposium, 2012

qbf2epr: A Tool for Generating EPR Formulas from QBF.

[BibT_eX]

[DOI]

Proceedings of the Third Workshop on Practical Aspects of Automated Reasoning, 2012

UML @ Classroom - Eine Einführung in die objektorientierte Modellierung.

[BibT_eX]

[DOI]

dpunkt.verlag, ISBN: 978-3-89864-776-2, 2012

2011

Towards an Understanding of Requirements for Model Versioning Support.

[BibT_eX]

[DOI]

Konrad Wieland

Geraldine Fitzpatrick

Gerti Kappel

Manuel Wimmer

Int. J. People Oriented Program., 2011

Position Paper: Software Modeling Education.

[BibT_eX]

[DOI]

Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2011

Software modeling in education.

[BibT_eX]

[DOI]

Comput. Sci. Educ., 2011

Towards Semantics-Aware Merge Support in Optimistic Model Versioning.

[BibT_eX]

[DOI]

Proceedings of the Models in Software Engineering, 2011

VIDEAS: A Development Tool for Answer-Set Programs Based on Model-Driven Engineering Technology.

[BibT_eX]

[DOI]

Proceedings of the Logic Programming and Nonmonotonic Reasoning, 2011

Blocked Clause Elimination for QBF.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31, 2011

2010

Preface.

[BibT_eX]

[DOI]

Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2010

Guiding modelers through conflict resolution: a recommender for model versioning.

[BibT_eX]

[DOI]

Konrad Wieland

Proceedings of the Companion to the 25th Annual ACM SIGPLAN Conference on Object-Oriented Programming, 2010

A recommender for conflict resolution support in optimistic model versioning.

[BibT_eX]

[DOI]

Gerti Kappel

Proceedings of the Companion to the 25th Annual ACM SIGPLAN Conference on Object-Oriented Programming, 2010

Software Modeling in Education: The 6th Educators' Symposium at MODELS 2010.

[BibT_eX]

[DOI]

Proceedings of the Models in Software Engineering, 2010

Conflicts as First-Class Entities: A UML Profile for Model Versioning.

[BibT_eX]

[DOI]

Proceedings of the Models in Software Engineering, 2010

Adaptable Model Versioning in Action.

[BibT_eX]

[DOI]

Proceedings of the Modellierung 2010, 24.-26. März 2010, Klagenfurt, Österreich, 2010

Colex: a web-based collaborative conflict lexicon.

[BibT_eX]

[DOI]

Proceedings of the 1st International Workshop on Model Comparison in Practice, 2010

Concurrent Modeling in Early Phases of the Software Development Life Cycle.

[BibT_eX]

[DOI]

Proceedings of the Collaboration and Technology - 16th International Conference, 2010

2009

A survey on model versioning approaches.

[BibT_eX]

[DOI]

Kerstin Altmanninger

Manuel Wimmer

Int. J. Web Inf. Syst., 2009

SmartMatcher: Improving Automatically Generated Transformations.

[BibT_eX]

Datenbank-Spektrum, 2009

A solver for QBFs in negation normal form.

[BibT_eX]

[DOI]

Stefan Woltran

Constraints An Int. J., 2009

On Realizing a Framework for Self-tuning Mappings.

[BibT_eX]

[DOI]

Proceedings of the Objects, Components, Models and Patterns, 47th International Conference, 2009

The operation recorder: specifying model refactorings by-example.

[BibT_eX]

[DOI]

Proceedings of the Companion to the 24th Annual ACM SIGPLAN Conference on Object-Oriented Programming, 2009

By-example adaptation of the generic model versioning system AMOR: how to include language-specific features for improving the check-in process.

[BibT_eX]

[DOI]

Proceedings of the Companion to the 24th Annual ACM SIGPLAN Conference on Object-Oriented Programming, 2009

An Example Is Worth a Thousand Words: Composite Operation Modeling By-Example.

[BibT_eX]

[DOI]

Werner Retschitzegger

Wieland Schwinger

Proceedings of the Model Driven Engineering Languages and Systems, 2009

ccT on Stage: Generalised Uniform Equivalence Testing for Verifying Student Assignment Solutions.

[BibT_eX]

[DOI]

Proceedings of the Logic Programming and Nonmonotonic Reasoning, 2009

Towards end-user adaptable model versioning: The By-Example Operation Recorder.

[BibT_eX]

[DOI]

Proceedings of the 2009 ICSE Workshop on Comparison and Versioning of Software Models, 2009

We can work it out: Collaborative Conflict Resolution in Model Versioning.

[BibT_eX]

[DOI]

Proceedings of the Eleventh European Conference on Computer Supported Cooperative Work, 2009

2007

Testing Relativised Uniform Equivalence under Answer-Set Projection in the System ccT.

[BibT_eX]

[DOI]

Proceedings of the Applications of Declarative Programming and Knowledge Management, 2007

Ein Beweiser für quantifizierte Boolsche Formeln in Negationsnormalform [A Solver for Quantified Boolean Formulas in Negation Normal Form].

[BibT_eX]

[DOI]

Proceedings of the Ausgezeichnete Informatikdissertationen 2007, 2007

Matching Metamodels with Semantic Systems - An Experience Report.

[BibT_eX]

Proceedings of the Datenbanksysteme in Business, 2007

A solver for quantified Boolean formulas in negation normal form.

[BibT_eX]

PhD thesis, 2007

2006

A Tool for Advanced Correspondence Checking in Answer-Set Programming: Preliminary Experimental Results.

[BibT_eX]

[DOI]

Proceedings of the 20th Workshop on Logic Programming, 2006

ccT: A Correspondence-Checking Tool for Logic Programs Under the Answer-Set Semantics.

[BibT_eX]

[DOI]

Proceedings of the Logics in Artificial Intelligence, 10th European Conference, 2006

A Solver for QBFs in Nonprenex Form.

[BibT_eX]