![]() |
![]() ![]() ![]() ![]() Head of Formal Methods Research Group at the Czech Institute of of Informatics, Robotics and Cybernetics (CIIRC) Publications | Projects | Software | Links |
2023 |
Experiments on Infinite Model Finding in SMT Solving
[preprint]
in LPAR 2023 |
A Mathematical Benchmark for Inductive Theorem Provers
[preprint]
in LPAR 2023 |
Computing Generating Sets of Minimal Size in Finite Algebras
[preprint]
[doi]
in Journal of Symbolic Computation |
Fast Heuristic for Ricochet Robots
[pdf]
in ICAART-23 |
Integrated lot-sizing and scheduling: Mitigation of uncertainty in demand and processing time by machine learning
[doi]
in Engineering Applications of Artificial Intelligence 2023 |
2022 |
Towards Learning Quantifier Instantiation in SMT
[preprint]
[doi]
in SAT 2022 |
MultIPAs: applying program transformations to introductory programming assignments for data augmentation
[doi]
in ESEC/SIGSOFT FSE 2022 |
TestSelector: Automatic Test Suite Selection for Student Projects
[doi]
[arXiv]
in International Conference on Runtime Verification |
Targeted Configuration of an SMT Solver
[doi]
[preprint]
in CICM 2022 |
Boosting Isomorphic Model Filtering with Invariants [doi] [arXiv] in CONSTRAINTS |
Guiding an Automated Theorem Prover with Neural Rewriting
[preprint]
[doi]
in IJCAR 2022 |
SAT-based Leximax Optimisation Algorithms
[preprint]
[slides]
[doi]
in SAT 2022 |
Challenges and Solutions for Higher-Order SMT Proofs
[preprint]
[talk]
in SMT 2022 |
2021 |
Fair and Adventurous Enumeration of Quantifier Instantiations [doi] [preprint] [talk] [slides] in FMCAD 2021 |
The Seesaw Algorithm: Function Optimization using Implicit Hitting Sets [preprint] [talk] [doi] in CP 2021 |
Filtering Isomorphic Models by Invariants [preprint] [doi] in CP 2021 |
Graph Neural Networks for Scheduling of SMT Solvers [preprint] in ICTAI 2021 |
Characteristic Subsets of SMT-LIB Benchmarks [preprint] in SMT 2021 |
First-Order Instantiation using Discriminating Terms [preprint] in SMT 2021 |
How to Approximate Leximax-optimal Solutions [preprint] in POS 2021 |
2020 |
SAT-based Encodings for Optimal Decision Trees with Explicit Paths [ee] [talk] [tool] in SAT 2020 |
2019 |
New Resolution-Based QBF Calculi and Their Proof Complexity [ee] in ACM Transactions on Computation Theory (TOCT) |
PrideMM: Second Order Model Checking for Memory Consistency Models [slides]
[preprint] in TAPAS '19 |
Machine Learning of Strategies in QBF Solving [preprint] [slides] in RCRA '19 |
On Unordered BDDs and Quantified Boolean Formulas [preprint] in EPIA '19 |
2018 |
Towards Smarter MACE-style Model Finders [preprint] [ee] [slides] [bib] and in LPAR '18 |
QBF Solvers Submitted to QBF Competition 2018 [slides] in QBF '18 |
Circuit-based Search Space Pruning in QBF [ee]
[slides] [preprint] [github] in SAT '18 |
Towards Generalization in QBF Solving via Machine Learning
[tool]
[ee]
[preprint] in AAAI '18 |
2017 |
On the Quest for an Acyclic Graph [preprint] [slides] [arXiv] in RCRA '17 |
On Minimal Corrections in ASP [preprint] [slides] in RCRA '17 |
Minimal sets on propositional formulae. Problems and reductions [ee] in Artificial Intelligence |
An Achilles' Heel of Term-Resolution [ee] [preprint] in EPIA 17 |
2016 |
On Incremental Core-Guided MaxSAT Solving [pdf] in CP 16 |
On Q-Resolution and CDCL QBF Solving [pdf] [slides] [ee] in SAT 16 [ee] |
Extension Variables in QBF Resolution [eccc] in Beyond NP Workshop |
Current Trends in QBF Solving [slides] invited talk at the Beyond NP Workshop |
Solving QBF with Counterexample Guided Refinement [ee] [bib] in Journal of Artificial Intelligence (AI) |
On Intervals and Bounds in Bit-vector Arithmetic. [ee] in SMT@IJCAR |
On the Query Complexity of Selecting Minimal Sets for Monotone Predicates [ee] in Journal of Artificial Intelligence (AI) |
2015 |
MiFuMax-a Literate MaxSAT Solver [ee] [tool] in Journal on Satisfiability, Boolean Modeling and Computation (JSAT) |
Playing with Quantified Satisfaction [ee]
[preprint] [slides] in LPAR-20 |
On Conflicts and Strategies in QBF [ee] [preprint] [slides] in LPAR-20 |
Solving QBF by Clause Selection [ee] [preprint] [tool] [bib] in IJCAI '15 |
Efficient Model Based Diagnosis with Maximum Satisfiability [ee] in IJCAI '15 |
Quantified Maximum Satisfiability [ee] [bib] in Constraints, An International Journal |
Expansion-based QBF Solving versus Q-Resolution [ee]
[preprint] [bib] in Journal of Theoretical Computer Science (TCS) |
Exploiting Resolution-Based Representations for MaxSAT Solving [ee] in SAT '15 |
Proof Complexity of Resolution-based QBF Calculi [ee] [eccc] [bib] in STACS '15 |
Efficient Extraction of QBF (Counter)models from Long-Distance Resolution Proofs in AAAI '15 |
2014 |
On Unification of QBF Resolution-Based Calculi [preprint] [slides] [eccc] [ee] in Mathematical Foundations of Computer Science (MFCS '14). |
On Instantiation-Based Calculi for QBF [slides] in Invited talk at the QBF Workshop 2014. |
Towards efficient optimization in package management systems [ee] in International Conference on Software Engineering (ICSE '14) |
On lazy and eager interactive reconfiguration [slides] [ee] in International Workshop on Variability Modelling of Software-Intensive Systems (VaMoS '14) |
Algorithms for Computing Backbones of Propositional Formulae [preprint]
[ee] in Journal of AI Communications (AI-Com) |
Algorithms for computing minimal equivalent subformulas [ee] in Journal of Artificial Intelligence (AI) |
2013 |
On QBF Proofs and Preprocessing [preprint] [slides] [arXiv] [ee]
[blogpost] [tools] Logic for Programming Artificial Intelligence and Reasoning (LPAR-19) |
Solving QBF with Free Variables [preprint] 19th International Conference on Principles and Practice of Constraint Programming (CP'13) |
On Propositional QBF Expansions and Q-Resolution [ee] [preprint] [slides] [scripts] 16th International Conference on Theory and Applications of Satisfiability Testing (SAT '13) |
Quantified Maximum Satisfiability: A Core-Guided Approach [preprint] 16th International Conference on Theory and Applications of Satisfiability Testing (SAT '13) |
On Computing Minimal Correction Subsets [ee] IJCAI 2013 |
Minimal Sets over Monotone Predicates in Boolean Formulae [preprint] [ee] International Conference on Computer Aided Verification (CAV '13) |
2012 |
On Computing Minimal Equivalent Subformulas [ee]
[preprint] 18th International Conference on Principles and Practice of Constraint Programming (CP'12) |
Solving QBF with Counterexample Guided Refinement [ee] [preprint] [slides] [tool] [bib] The 15th International Conference on Theory and Applications of Satisfiability Testing (SAT '12) |
On Unit-Refutation Complete Formulae with Existentially Quantified Variables [ee] [preprint] [slides] International Conference on Principles of Knowledge Representation and Reasoning (KR), 2012 |
Experimental Analysis of Backbone Computation Algorithms [pdf] [ee] [slides] International Workshop on "Experimental Evaluation of Algorithms for solving problems with combinatorial explosion", RCRA |
On Checking of Skolem-based Models of QBF [ee]
[slides] International Workshop on "Experimental Evaluation of Algorithms for solving problems with combinatorial explosion", RCRA |
QBF-Based Boolean Function Bi-decomposition [arXiv] [ee] Design, Automation & Test in Europe Conference & Exhibition (DATE), 2012 |
PackUp: Tools for Package Upgradability Solving [ee] [tool] Journal on Satisfiability, Boolean Modeling and Computation, Volume 8, 2012 |
2011 |
On Deciding MUS Membership with QBF [bib] [slides] [pdf] [ee] 17th International Conference on Principles and Practice of Constraint Programming (CP'11) |
Abstraction-Based Algorithm for 2QBF [ee]
[slides] [pdf] 14th International Conference on Theory and Applications of Satisfiability Testing (SAT '11) |
cmMUS: A Tool for Circumscription-Based MUS Membership Testing [ee] [pdf] [tool] The 11th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR '11) |
2010 |
Counterexample Guided Abstraction Refinement Algorithm for Propositional Circumscription [slides] [bib] [ee] [pdf] The 12th European Conference on Logics in Artificial Intelligence (JELIA '10) |
On Computing Backbones of Propositional Theories [slides] [bib] [pdf] The 19th European Conference on Artificial Intelligence (ECAI '10). |
How to Complete an Interactive Configuration Process? [slides]
[bib] [pdf] International Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM '10). |
2009 |
CLOPS: A DSL for Command Line Options [slides] [bib] [pdf] [tool] IFIP Working Conference on Domain Specific Languages (DSL WC), Oxford, 2009. |
2008 |
Model Construction with External Constraints: An Interactive Journey from Semantics to Syntax [slides] [pdf] ACM/IEEE 11th Int. Conf. on Model Driven Eng. Languages and Systems Fundamental Approaches to Software Engineering (MODELS '08). |
Do SAT Solvers Make Good Configurators? [slides] [bib] [pdf] First Workshop on Analyses of Software Product Lines (ASPL '08). Limerick, Ireland, September 12, 2008. |
Formal Approach to Integrating Feature and Architecture Models [slides] [pdf] Fundamental Approaches to Software Engineering (FASE '08). Budapest, Hungary. April, 2008. |
2007 |
Reachability Analysis for Annotated Code [slides] [pdf] The 6th International Workshop on the Specification and Verification of Component-based Systems (SAVCBS '07). Dubrovnik, Croatia. September, 2007. |
Reasoning about Feature Models in Higher-Order Logic [slides] [pdf] The 11th International Software Product Lines Conference (SPLC 2007). Kyoto, Japan. September, 2007. |
Assertion-based Loop Invariant Generation [slides] [pdf] The 1st International Workshop on Invariant Generation (WING 2007). Hagenberg, Austria. June, 2007. |
POSTMAN --- Powering SMT Solvers by Machine Learning
QFUN, QBF Solver based on RAReQS and machine learning
CQESTO, A circuit-based version of QESTO.
QESTO, QBF Solver based on clause selection
AReQS, Abstraction Refinement QBF Solver for non-CNF 2QBF
RAReQS-NN, Recursive Abstraction Refinement QBF Solver supporting Non-CNF, Non-Prenex formulas
RAReQS, Recursive Abstraction Refinement QBF Solver
MiFuMaX, unsat-based MaXSAT solver based on minisat
qcnf2z3, a set of scripts that enable invoking Z3 on QDIMACS instances.
cmMUS, MUS-membership solver based on translation to propositional circumscription
PackUP, a framework for package upgradability solving, allows for an external OPB solver
cudf2msu, a package upgradability solver based on msuncore
cudf2pbo, a package upgradability solver based on WBO
PIEnum, a simple prime implicant/model enumerator
minibones, a program to compute backbones of a formula
SAT Solving in Interactive Configuration [pdf] [bib] PhD Thesis, Department of Computer Science at University College Dublin |
Automated Theorem Proving and Program Verification [pdf] MSc Thesis, Department of Theoretical Computer Science and Mathematical Logic at Charles University in Prague |
Formal Methods in Software Product Lines: Concepts, Survey, and Guidelines [bib] [pdf] Lero Technical Report, Lero-TR-SPL-2008-02, University of Limerick, May 2008. |
Proofgold: Blockchain for Formal Methods
[preprint]
in Formal Methods for Blockchain Protocols 2022 |
![]() |
Last updated: Sep 2, 2022 |