Home Page of Mikoláš Janota
 |
 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
Theses
| 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 |
Technical Reports
| 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 |