Reachability analysis for annotated code. - Mikolás Janota; Radu Grigore; Michal Moskal (SAVCBS, 2007)

Reasoning about Feature Models in Higher-Order Logic. - Mikolás Janota; Joseph Kiniry (SPLC, 2007)

Formal Approach to Integrating Feature and Architecture Models. - Mikolás Janota; Goetz Botterweck (FASE, 2008)

Model Construction with External Constraints: An Interactive Journey from Semantics to Syntax. - Mikolás Janota; Victoria Kuzina; Andrzej Wasowski (MoDELS, 2008)

Do SAT Solvers Make Good Configurators? - Mikolás Janota (SPLC (2), 2008)

CLOPS: A DSL for Command Line Options. - Mikolás Janota; Fintan Fairmichael; Viliam Holub; Radu Grigore; Julien Charles; Dermot Cochran; Joseph R. Kiniry (DSL, 2009)

A Design of a Configurable Feature Model Configurator. - Goetz Botterweck; Mikolás Janota; Denny Schneeweiss (VaMoS, 2009)

Algorithms for finding dispensable variables - Mikolás Janota; João Marques-Silva 001; Radu Grigore (CoRR, 2009)

On Computing Backbones of Propositional Theories. - João Marques-Silva 001; Mikolás Janota; Inês Lynce (ECAI, 2010)

Counterexample Guided Abstraction Refinement Algorithm for Propositional Circumscription. - Mikolás Janota; Radu Grigore; João Marques-Silva 001 (JELIA, 2010)

How to Complete an Interactive Configuration Process? - Mikolás Janota; Goetz Botterweck; Radu Grigore; João Marques-Silva 001 (SOFSEM, 2010)

On Deciding MUS Membership with QBF. - Mikolás Janota; João Marques-Silva 001 (CP, 2011)

cmMUS: A Tool for Circumscription-Based MUS Membership Testing. - Mikolás Janota; João Marques-Silva 001 (LPNMR, 2011)

Abstraction-Based Algorithm for 2QBF. - Mikolás Janota; João Marques-Silva 001 (SAT, 2011)

On Computing Minimal Equivalent Subformulas. - Anton Belov; Mikolás Janota; Inês Lynce; João Marques-Silva 001 (CP, 2012)

QBf-based boolean function bi-decomposition. - Huan Chen 001; Mikolás Janota; João Marques-Silva 001 (DATE, 2012)

On Unit-Refutation Complete Formulae with Existentially Quantified Variables. - Lucas Bordeaux; Mikolás Janota; João Marques-Silva 001; Pierre Marquis (KR, 2012)

PackUp: Tools for Package Upgradability Solving. - Mikolás Janota; Inês Lynce; Vasco Manquinho; João Marques-Silva 001 (J. Satisf. Boolean Model. Comput., 2012)

Minimal Sets over Monotone Predicates in Boolean Formulae. - João Marques-Silva 001; Mikolás Janota; Anton Belov (CAV, 2013)

Solving QBF with Free Variables. - William Klieber; Mikolás Janota; João Marques-Silva 001; Edmund M. Clarke (CP, 2013)

On Computing Minimal Correction Subsets. - João Marques-Silva 001; Federico Heras; Mikolás Janota; Alessandro Previti; Anton Belov (IJCAI, 2013)

On QBF Proofs and Preprocessing. - Mikolás Janota; Radu Grigore; João Marques-Silva 001 (LPAR, 2013)

Quantified Maximum Satisfiability: - A Core-Guided Approach. - Alexey Ignatiev; Mikolás Janota; João Marques-Silva 001 (SAT, 2013)

On Propositional QBF Expansions and Q-Resolution. - Mikolás Janota; João Marques-Silva 001 (Electron. Colloquium Comput. Complex., 2013)

Towards efficient optimization in package management systems. - Alexey Ignatiev; Mikolás Janota; João Marques-Silva 001 (ICSE, 2014)

On lazy and eager interactive reconfiguration. - Mikolás Janota; Goetz Botterweck; João Marques-Silva 001 (VaMoS, 2014)

Algorithms for computing minimal equivalent subformulas. - Anton Belov; Mikolás Janota; Inês Lynce; João Marques-Silva 001 (Artif. Intell., 2014)

Computing Minimal Sets on Propositional Formulae I: Problems & Reductions. - João Marques-Silva 001; Mikolás Janota (CoRR, 2014)

Proof Complexity of Resolution-based QBF Calculi. - Olaf Beyersdorff; Leroy Chew; Mikolas Janota (Electron. Colloquium Comput. Complex., 2014)

On Unification of QBF Resolution-Based Calculi. - Mikolas Janota; Leroy Chew; Olaf Beyersdorff (Electron. Colloquium Comput. Complex., 2014)

On the Query Complexity of Selecting Few Minimal Sets. - João Marques-Silva 001; Mikolás Janota (Electron. Colloquium Comput. Complex., 2014)

MiFuMax - a Literate MaxSAT Solver. - Mikolas Janota (J. Satisf. Boolean Model. Comput., 2014)

The QBFGallery 2014: The QBF Competition at the FLoC Olympic Games. - Mikolas Janota; Charles Jordan; Will Klieber; Florian Lonsing; Martina Seidl; Allen Van Gelder (J. Satisf. Boolean Model. Comput., 2014)

Efficient Extraction of QBF (Counter)models from Long-Distance Resolution Proofs. - Valeriy Balabanov; Jie-Hong Roland Jiang; Mikolas Janota; Magdalena Widl (AAAI, 2015)

Solving QBF by Clause Selection. - Mikolás Janota; João Marques-Silva 001 (IJCAI, 2015)

Efficient Model Based Diagnosis with Maximum Satisfiability. - João Marques-Silva 001; Mikolás Janota; Alexey Ignatiev; António Morgado 001 (IJCAI, 2015)

Playing with Quantified Satisfaction. - Nikolaj S. Bjørner; Mikolás Janota (LPAR (short papers), 2015)

On Conflicts and Strategies in QBF. - Nikolaj S. Bjørner; Mikolás Janota; William Klieber (LPAR (short papers), 2015)

Exploiting Resolution-Based Representations for MaxSAT Solving. - Miguel Neves 001; Ruben Martins; Mikolás Janota; Inês Lynce; Vasco Manquinho (SAT, 2015)

Algorithms for computing backbones of propositional formulae. - Mikolás Janota; Inês Lynce; João Marques-Silva 001 (AI Commun., 2015)

Expansion-based QBF solving versus Q-resolution. - Mikolás Janota; João Marques-Silva 001 (Theor. Comput. Sci., 2015)

On Intervals and Bounds in Bit-vector Arithmetic. - Mikolás Janota; Christoph M. Wintersteiger (SMT@IJCAR, 2016)

On Incremental Core-Guided MaxSAT Solving. - Xujie Si; Xin Zhang 035; Vasco Manquinho; Mikolás Janota; Alexey Ignatiev; Mayur Naik (CP, 2016)

Solving QBF with counterexample guided refinement. - Mikolás Janota; William Klieber; João Marques-Silva 001; Edmund M. Clarke (Artif. Intell., 2016)

On the query complexity of selecting minimal sets for monotone predicates. - Mikolás Janota; João Marques-Silva 001 (Artif. Intell., 2016)

Quantified maximum satisfiability. - Alexey Ignatiev; Mikolás Janota; João Marques-Silva 001 (Constraints An Int. J., 2016)

Extension Variables in QBF Resolution. - Olaf Beyersdorff; Leroy Chew; Mikolas Janota (Electron. Colloquium Comput. Complex., 2016)

On Q-Resolution and CDCL QBF Solving. - Mikolas Janota (Electron. Colloquium Comput. Complex., 2016)

On Exponential Lower Bounds for Partially Ordered Resolution. - Mikolas Janota (J. Satisf. Boolean Model. Comput., 2016)

On the Quest for an Acyclic Graph. - Mikolás Janota; Radu Grigore; Vasco Manquinho (RCRA@AI*IA, 2017)

On Minimal Corrections in ASP. - Mikolás Janota; João Marques-Silva 001 (RCRA@AI*IA, 2017)

An Achilles' Heel of Term-Resolution. - Mikolás Janota; João Marques-Silva 001 (EPIA, 2017)

Minimal sets on propositional formulae. Problems and reductions. - João Marques-Silva 001; Mikolás Janota; Carlos Mencía (Artif. Intell., 2017)

An Achilles' Heel of Term-Resolution. - Mikolás Janota (CoRR, 2017)

QFUN: Towards Machine Learning in QBF. - Mikolás Janota (CoRR, 2017)

Towards Generalization in QBF Solving via Machine Learning. - Mikolás Janota (AAAI, 2018)

Towards Smarter MACE-style Model Finders. - Mikolas Janota; Martin Suda 001 (LPAR, 2018)

Circuit-Based Search Space Pruning in QBF. - Mikolás Janota (SAT, 2018)

On Unordered BDDs and Quantified Boolean Formulas. - Mikolás Janota (EPIA (2), 2019)

PrideMM: Second Order Model Checking for Memory Consistency Models. - Simon Cooksey; Sarah Harris; Mark Batty; Radu Grigore; Mikolás Janota (FM Workshops (2), 2019)

PrideMM: A Solver for Relaxed Memory Models. - Simon Cooksey; Sarah Harris; Mark Batty; Radu Grigore; Mikolás Janota (CoRR, 2019)

New Resolution-Based QBF Calculi and Their Proof Complexity. - Olaf Beyersdorff; Leroy Chew; Mikolás Janota (ACM Trans. Comput. Theory, 2019)

SAT-Based Encodings for Optimal Decision Trees with Explicit Paths. - Mikolás Janota; António Morgado 001 (SAT, 2020)

Filtering Isomorphic Models by Invariants (Short Paper). - João Araújo 002; Choiwah Chow; Mikolás Janota (CP, 2021)

The Seesaw Algorithm: Function Optimization Using Implicit Hitting Sets. - Mikolás Janota; António Morgado 001; José Fragoso Santos; Vasco Manquinho (CP, 2021)

Fair and Adventurous Enumeration of Quantifier Instantiations. - Mikolás Janota; Haniel Barbosa; Pascal Fontaine; Andrew Reynolds 001 (FMCAD, 2021)

Graph Neural Networks for Scheduling of SMT Solvers. - Jan Hula; David Mojzísek; Mikolás Janota (ICTAI, 2021)

First-Order Instantiation using Discriminating Terms. - Chad E. Brown; Mikolás Janota (SMT, 2021)

Characteristic Subsets of SMT-LIB Benchmarks. - Jan Jakubuv; Mikolás Janota; Andrew Reynolds 001 (SMT, 2021)

Learning Equational Theorem Proving. - Jelle Piepenbrock; Tom Heskes; Mikolás Janota; Josef Urban (CoRR, 2021)

Quantified Boolean Formulas. - Olaf Beyersdorff; Mikolás Janota; Florian Lonsing; Martina Seidl (Handbook of Satisfiability, 2021)

Guiding an Automated Theorem Prover with Neural Rewriting. - Jelle Piepenbrock; Tom Heskes; Mikolás Janota; Josef Urban (IJCAR, 2022)

Targeted Configuration of an SMT Solver. - Jan Hula; Jan Jakubuv; Mikolás Janota; Lukás Kubej (CICM, 2022)

TestSelector: Automatic Test Suite Selection for Student Projects. - Filipe Marques; António Morgado 001; José Fragoso Santos; Mikolás Janota (RV, 2022)

SAT-Based Leximax Optimisation Algorithms. - Miguel Cabral; Mikolás Janota; Vasco Manquinho (SAT, 2022)

Towards Learning Quantifier Instantiation in SMT. - Mikolás Janota; Jelle Piepenbrock; Bartosz Piotrowski (SAT, 2022)

MultIPAs: applying program transformations to introductory programming assignments for data augmentation. - Pedro Orvalho; Mikolás Janota; Vasco Manquinho (ESEC/SIGSOFT FSE, 2022)

Abstract: Challenges and Solutions for Higher-Order SMT Proofs. - Chad E. Brown; Mikolás Janota; Cezary Kaliszyk (SMT, 2022)

Boosting isomorphic model filtering with invariants. - João Araújo 002; Choiwah Chow; Mikolás Janota (Constraints An Int. J., 2022)

TestSelector: Automatic Test Suite Selection for Student Projects - Extended Version. - Filipe Marques; António Morgado 001; José Fragoso Santos; Mikolás Janota (CoRR, 2022)

Machine Learning Meets The Herbrand Universe. - Jelle Piepenbrock; Josef Urban; Konstantin Korovin; Miroslav Olsák; Tom Heskes; Mikolas Janota (CoRR, 2022)

Symmetries for Cube-And-Conquer in Finite Model Finding. - João Araújo 002; Choiwah Chow; Mikolás Janota (CP, 2023)

Graph Neural Networks for Mapping Variables Between Programs. - Pedro Orvalho; Jelle Piepenbrock; Mikolás Janota; Vasco Manquinho (ECAI, 2023)

Data-driven Single Machine Scheduling Minimizing Weighted Number of Tardy Jobs. - Nikolai Antonov; Premysl Sucha; Mikolás Janota (EPIA (1), 2023)

The FMCAD 2023 Student Forum. - Mikolas Janota; Nina Narodytska (FMCAD, 2023)

Fast Heuristic for Ricochet Robots. - Jan Hula; David Adamczyk; Mikolás Janota (ICAART (1), 2023)

Molecule Builder: Environment for Testing Reinforcement Learning Agents. - Petr Hyner; Jan Hula; Mikolás Janota (IJCCI, 2023)

A Mathematical Benchmark for Inductive Theorem Provers. - Thibault Gauthier; Chad E. Brown; Mikolas Janota; Josef Urban (LPAR, 2023)

Experiments on Infinite Model Finding in SMT Solving. - Julian Parsert; Chad E. Brown; Mikolas Janota; Cezary Kaliszyk (LPAR, 2023)

Selecting Quantifiers for Instantiation in SMT. - Jan Jakubuv; Mikolás Janota; Bartosz Piotrowski; Jelle Piepenbrock; Andrew Reynolds 001 (SMT, 2023)

Towards Learning Infinite SMT Models (Work in Progress). - Mikolás Janota; Bartosz Piotrowski; Karel Chvalovský (SYNASC, 2023)

Graph Neural Networks For Mapping Variables Between Programs - Extended Version. - Pedro Orvalho; Jelle Piepenbrock; Mikolás Janota; Vasco Manquinho (CoRR, 2023)

Integrated lot-sizing and scheduling: Mitigation of uncertainty in demand and processing time by machine learning. - Mohammad Rohaninejad; Mikolás Janota; Zdenek Hanzálek (Eng. Appl. Artif. Intell., 2023)

Computing generating sets of minimal size in finite algebras. - Mikolás Janota; António Morgado 001; Petr Vojtechovský (J. Symb. Comput., 2023)

SAT-Based Techniques for Lexicographically Smallest Finite Models. - Mikolás Janota; Choiwah Chow; João Araújo 002; Michael Codish; Petr Vojtechovský (AAAI, 2024)

Understanding GNNs for Boolean Satisfiability through Approximation Algorithms. - Jan Hula; David Mojzísek; Mikolás Janota (CIKM, 2024)

Cube-Based Isomorph-Free Finite Model Finding. - Choiwah Chow; Mikolás Janota; João Araújo 002 (ECAI, 2024)

Machine Learning for Quantifier Selection in cvc5. - Jan Jakubuv; Mikolás Janota; Jelle Piepenbrock; Josef Urban (ECAI, 2024)

cfaults: Model-Based Diagnosis for Fault Localization in C with Multiple Test Cases. - Pedro Orvalho; Mikolás Janota; Vasco M. Manquinho (FM (1), 2024)

C-Pack of IPAs: A C90 Program Benchmark of Introductory Programming Assignments. - Pedro Orvalho; Mikolás Janota; Vasco Manquinho (APR, 2024)

First Experiments with Neural cvc5. - Jelle Piepenbrock; Mikolas Janota; Josef Urban; Jan Jakubuv (LPAR, 2024)

Solving Hard Mizar Problems with Instantiation and Strategy Invention. - Jan Jakubuv; Mikolás Janota; Josef Urban (CICM, 2024)

Symbolic Computation for All the Fun. - Chad E. Brown; Mikolas Janota; Mirek Olsák (PAAR+SC²@IJCAR, 2024)

GitSEED: A Git-backed Automated Assessment Tool for Software Engineering and Programming Education. - Pedro Orvalho; Mikolás Janota; Vasco Manquinho (SIGCSE Virtual (1), 2024)

CFaults: Model-Based Diagnosis for Fault Localization in C Programs with Multiple Test Cases. - Pedro Orvalho; Mikolás Janota; Vasco Manquinho (CoRR, 2024)

Supplementary Material for Breaking Symmetries in Quantified Graph Search: A Comparative Study. - Tomás Peitl; Markus Kirchweger; Mikolás Janota; Stefan Szeider (Zenodo, 2024)

Complete Symmetry Breaking for Finite Models. - Marek Danco; Mikolás Janota; Michael Codish; João Jorge Araújo (AAAI, 2025)

Breaking Symmetries in Quantified Graph Search: A Comparative Study. - Mikolás Janota; Markus Kirchweger; Tomás Peitl; Stefan Szeider (AAAI, 2025)

Counterexample Guided Program Repair Using Zero-Shot Learning and MaxSAT-based Fault Localization. - Pedro Orvalho; Mikolás Janota; Vasco M. Manquinho (AAAI, 2025)

SMT and Functional Equation Solving over the Reals: Challenges from the IMO. - Chad E. Brown; Karel Chvalovský; Mikolás Janota; Mirek Olsák; Stefan Ratschan (CADE, 2025)

Breaking Symmetries with Involutions. - Michael Codish; Mikolás Janota (CP, 2025)

Breaking Symmetries from a Set-Covering Perspective. - Michael Codish; Mikolás Janota (CPAIOR (1), 2025)

Invariant neural architecture for learning term synthesis in instantiation proving. - Jelle Piepenbrock; Josef Urban; Konstantin Korovin; Miroslav Olsák; Tom Heskes; Mikolás Janota (J. Symb. Comput., 2025)

InvAASTCluster: On Applying Invariant-Based Program Clustering to Introductory Programming Assignments. - Pedro Orvalho; Mikolás Janota; Vasco Manquinho (J. Syst. Softw., 2025)

First Experiments with Neural cvc5. - Jelle Piepenbrock; Mikolás Janota; Jan Jakubuv (CoRR, 2025)

Complete Symmetry Breaking for Finite Models. - Marek Danco; Mikolás Janota; Michael Codish; João Araújo 002 (CoRR, 2025)

Neural Approaches to SAT Solving: Design Choices and Interpretability. - David Mojzísek; Jan Hula; Ziwei Li; Ziyu Zhou; Mikolás Janota (CoRR, 2025)

Geometric Reasoning in the Embedding Space. - Jan Hula; David Mojzísek; Jirí Janecek; David Herel; Mikolás Janota (CoRR, 2025)

From MBQI to Enumerative Instantiation and Back. - Marek Danco; Petra Hozzová; Mikolás Janota (CoRR, 2025)