Home Page of Mikoláš Janota
|
| Publications | Projects | Software | Positions | Links |
I have been working on the development of Formal Methods and Automated Reasoning during my whole academic career spanning now over 16 years, which includes SW verification, SAT, MaxSAT, or SMT solvers. I am contributing to the development of the SMT cvc5. More recently, I've been applying machine learning to improve SAT based solvers, mainly SMT (satisfiability modulo theories). I am the head of Formal Methods Research Group at the Czech Institute of of Informatics, Robotics and Cybernetics (CIIRC).
| 2024 |
|
Invariant neural architecture for learning term synthesis in instantiation proving
[doi]
in Journal of Symbolic Computation |
|
Symbolic Computation for All the Fun
[arxiv]
[pdf]
in Satisfiability Checking and Symbolic Computation, SC2 2024 |
|
Understanding GNNs for Boolean Satisfiability through Approximation Algorithms
[arxiv]
[preprint]
in Conference on Information and Knowledge Management (CIKM) 2024 |
|
Machine Learning for Quantifier Selection in cvc5
[arxiv]
[doi]
in ECAI 2024 |
|
C-Pack of IPAs: A C90 Program Benchmark of Introductory Programming Assignments
[doi]
[arxiv]
in APR '24: 5th ACM/IEEE International Workshop on Automated Program Repair |
|
Cube-based Isomorph-free Finite Model Finding
[preprint]
[doi]
[lightning-talk]
in ECAI 2024 |
|
Solving Hard Mizar Problems with Instantiation and Strategy Invention
[doi]
[arxiv]
in CICM 2024, Best Paper Award |
|
CFaults: Model-Based Diagnosis for Fault Localization in C with Multiple Test Cases
[arxiv]
[doi]
[bib]
in Formal Methods 2024 
|
|
GitSEED: A Git-backed Automated Assessment Tool for Software Engineering
[arxiv]
in SIGCSE Virtual 2024 |
|
SAT-based Techniques for Lexicographically Smallest Finite Models
[doi]
[preprint]
[tool]
[data]
[slides]
[talk]
in AAAI 2024 |
|
First Experiments with Neural cvc5
[doi]
[bib]
in LPAR 2024 |
| 2023 |
|
Graph Neural Networks For Mapping Variables Between Programs
[doi]
[arXiv]
in ECAI 2023 |
|
Symmetries for Cube-and-conquer in Finite Model Finding
[doi]
[preprint]
[slides]
in CP 2023 |
|
Towards Learning Infinite SMT Models
[preprint]
[slides]
in SYNASC 2023 |
|
Data-driven Single Machine Scheduling Minimizing Weighted Number of Tardy Jobs
[doi]
[preprint]
in EPIA 2023 |
|
Experiments on Infinite Model Finding in SMT Solving
[prepr]
[doi]
[examples]
in LPAR 2023 |
|
A Benchmark for Infinite Models in SMT
[prepr]
[data]
[slides]
[talk]
in AITP 2023 |
|
A Mathematical Benchmark for Inductive Theorem Provers
[preprint]
[doi]
in LPAR 2023 |
|
Computing Generating Sets of Minimal Size in Finite Algebras
[preprint]
[doi]
in Journal of Symbolic Computation |
| Selecting Quantifiers for Instantiation in SMT
[pdf]
in SMT 2023 |
| Molecule Builder: Environment for Testing Reinforcement Learning Agents
[doi]
in IJCCI 2023 |
| Fast Heuristic for Ricochet Robots
[doi]
[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 |
| 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
[doi]
[preprint]
in ICTAI 2021 |
| Characteristic Subsets of SMT-LIB Benchmarks [preprint] in SMT 2021 |
| First-Order Instantiation using Discriminating Terms
[preprint]
[talk]
in SMT 2021 |
| How to Approximate Leximax-optimal Solutions [preprint] in POS 2021 |
| 2020 |
| SAT-based Encodings for Optimal Decision Trees with Explicit Paths [doi] [talk] [tool] in SAT 2020 |
| 2019 |
| New Resolution-Based QBF Calculi and Their Proof Complexity [doi] 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]
[doi]
[slides]
[bib]
and in LPAR '18 |
| QBF Solvers Submitted to QBF Competition 2018 [slides] in QBF '18 |
| Circuit-based Search Space Pruning in QBF
[doi]
[slides] [preprint] [github] in SAT '18 |
| Towards Generalization in QBF Solving via Machine Learning
[tool]
[doi]
[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 [doi] in Artificial Intelligence |
| An Achilles' Heel of Term-Resolution [doi] [preprint] in EPIA 17 |
| 2016 |
| On Incremental Core-Guided MaxSAT Solving [pdf] in CP 16 |
| On Q-Resolution and CDCL QBF Solving [pdf] [slides]
[doi] in SAT 16 |
| 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 [doi] [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 [doi] in Journal of Artificial Intelligence (AI) |
| 2015 |
| MiFuMax-a Literate MaxSAT Solver [doi] [tool] in Journal on Satisfiability, Boolean Modeling and Computation (JSAT) |
| Playing with Quantified Satisfaction [doi]
[preprint] [slides] in LPAR-20 |
|
On Conflicts and Strategies in QBF
[doi]
[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 [doi] [bib] in Constraints, An International Journal |
| Expansion-based QBF Solving versus Q-Resolution [doi]
[preprint] [bib] in Journal of Theoretical Computer Science (TCS) |
| Exploiting Resolution-Based Representations for MaxSAT Solving [doi] in SAT '15 |
| Proof Complexity of Resolution-based QBF Calculi [doi] [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] [doi] 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 [doi] 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
[doi]
[preprint]
19th International Conference on Principles and Practice of Constraint Programming (CP'13) |
| On Propositional QBF Expansions and Q-Resolution [doi] [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] [doi] International Conference on Computer Aided Verification (CAV '13) |
| 2012 |
| On Computing Minimal Equivalent Subformulas
[doi]
18th International Conference on Principles and Practice of Constraint Programming (CP'12) |
| Solving QBF with Counterexample Guided Refinement [doi] [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] [doi] 17th International Conference on Principles and Practice of Constraint Programming (CP'11) |
| Abstraction-Based Algorithm for 2QBF [doi]
[slides] [pdf] 14th International Conference on Theory and Applications of Satisfiability Testing (SAT '11) |
| cmMUS: A Tool for Circumscription-Based MUS Membership Testing [doi] [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] [doi] [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
[doi]
[pdf]
[slides]
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
ROBOPROX --- Robotics and Advanced Industrial Production
mlex, a tool to calculate the lexicographically smallest isomorphic model for a given model (algebra).
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: Oct 18, 2024 20:23:52 |