Home Page of Mikoláš Janota
me electronic mail: mikolas DOT janota AT gmail DOT com
work: Microsoft Research, Cambridge, PPT Group
previous: INESC-ID Lisboa, SAT Group
Publications | Software | Links| Google Scholar Profile | DBLP | ECCC

Publications
2016
Extension Variables in QBF Resolution [eccc]
Olaf Beyersdorff, Leroy Chew, Mikoláš Janota in Beyond NP Workshop
Current Trends in QBF Solving [slides]
Mikoláš Janota invited talk at the Beyond NP Workshop
Solving QBF with Counterexample Guided Refinement [ee]
Mikoláš Janota, William Klieber, Joao Marques-Silva, and Edmund M. Clarke in Journal of Artificial Intelligence (AI)
On the Query Complexity of Selecting Minimal Sets for Monotone Predicates [ee]
Mikoláš Janota, Joao Marques-Silva in Journal of Artificial Intelligence (AI)
2015
MiFuMax-a Literate MaxSAT Solver [ee] [tool]
Mikoláš Janota, in Journal on Satisfiability, Boolean Modeling and Computation (JSAT)
Playing with Quantified Satisfaction [ee] [preprint] [slides]
Nikolaj Bjørner, Mikoláš Janota, in LPAR-20
On Conflicts and Strategies in QBF [ee] [preprint] [slides]
Nikolaj Bjørner, Mikoláš Janota, William Klieber, in LPAR-20
Solving QBF by Clause Selection [ee] [preprint] [tool]
Mikoláš Janota, Joao Marques-Silva, in IJCAI '15
Efficient Model Based Diagnosis with Maximum Satisfiability [ee]
Joao Marques-Silva Mikoláš Janota, Alexey Ignatiev, António Morgado, in IJCAI '15
Quantified Maximum Satisfiability [ee] [bib]
Alexey Ignatiev, Mikoláš Janota, Joao Marques-Silva, in Constraints, An International Journal
Expansion-based QBF Solving versus Q-Resolution [ee] [preprint] [bib]
Mikoláš Janota, Joao Marques-Silva, in Journal of Theoretical Computer Science (TCS)
Exploiting Resolution-Based Representations for MaxSAT Solving [ee]
M. Neves, R. Martins, M. Janota, I. Lynce, V. Manquinho, in SAT '15
Proof Complexity of Resolution-based QBF Calculi [ee] [eccc] [bib]
Olaf Beyersdorff, Leroy Chew, Mikoláš Janota, in STACS '15
Efficient Extraction of QBF (Counter)models from Long-Distance Resolution Proofs
Valeriy Balabanov, Jie-Hong R. Jiang, Mikoláš Janota, and Magdalena Widl, in AAAI '15
2014
On Unification of QBF Resolution-Based Calculi [preprint] [slides] [eccc] [ee]
Olaf Beyersdorff, Leroy Chew, Mikoláš Janota
Mathematical Foundations of Computer Science (MFCS '14).
On Instantiation-Based Calculi for QBF [slides]
Mikoláš Janota, Leroy Chew, and Olaf Beyersdorff
Invited talk at the QBF Workshop 2014.
Towards efficient optimization in package management systems [ee]
Alexey Ignatiev, Mikoláš Janota, Joao Marques-Silva
International Conference on Software Engineering (ICSE '14)
On lazy and eager interactive reconfiguration [slides] [ee]
Mikoláš Janota, Goetz Botterweck, Joao Marques-Silva
International Workshop on Variability Modelling of Software-Intensive Systems (VaMoS '14)
Algorithms for Computing Backbones of Propositional Formulae [preprint] [ee]
Mikoláš Janota, Inês Lynce, and Joao Marques-Silva
Journal of AI Communications (AI-Com)
Algorithms for computing minimal equivalent subformulas [ee]
Anton Belov, Mikoláš Janota, Inês Lynce, and Joao Marques-Silva
Journal of Artificial Intelligence (AI)
2013
On QBF Proofs and Preprocessing [preprint] [slides] [arXiv] [ee] [blogpost] [tools]
Mikoláš Janota, Radu Grigore, Joao Marques-Silva
Logic for Programming Artificial Intelligence and Reasoning (LPAR-19)
Solving QBF with Free Variables [preprint]
William Klieber, Mikoláš Janota, Joao Marques-Silva, and Edmund M. Clarke
19th International Conference on Principles and Practice of Constraint Programming (CP'13)
On Propositional QBF Expansions and Q-Resolution [ee] [preprint] [slides] [scripts]
Mikoláš Janota, Joao Marques-Silva
16th International Conference on Theory and Applications of Satisfiability Testing (SAT '13)
Quantified Maximum Satisfiability: A Core-Guided Approach [preprint]
Alexey Ignatiev, Mikoláš Janota, Joao Marques-Silva
16th International Conference on Theory and Applications of Satisfiability Testing (SAT '13)
On Computing Minimal Correction Subsets [preprint]
Joao Marques-Silva, Federico Heras, Mikoláš Janota, Alessandro Previti, Anton Belov
IJCAI 2013
Minimal Sets over Monotone Predicates in Boolean Formulae [preprint] [ee]
Joao Marques-Silva, Mikoláš Janota, Anton Belov
International Conference on Computer Aided Verification (CAV '13)
2012
On Computing Minimal Equivalent Subformulas [ee] [preprint]
Anton Belov, Mikoláš Janota, Inês Lynce, and Joao Marques-Silva
18th International Conference on Principles and Practice of Constraint Programming (CP'12)
Solving QBF with Counterexample Guided Refinement [ee] [preprint] [slides] [tool]
Mikoláš Janota, William Klieber, Joao Marques-Silva, and Edmund M. Clarke
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]
Lucas Bordeaux, Mikoláš Janota, Joao Marques-Silva, and Pierre Marquis
International Conference on Principles of Knowledge Representation and Reasoning (KR), 2012
Experimental Analysis of Backbone Computation Algorithms [pdf] [ee] [slides]
Mikoláš Janota, Inês Lynce, and Joao Marques-Silva
International Workshop on "Experimental Evaluation of Algorithms for solving problems with combinatorial explosion", RCRA
On Checking of Skolem-based Models of QBF [ee] [slides]
Mikoláš Janota and Joao Marques-Silva
International Workshop on "Experimental Evaluation of Algorithms for solving problems with combinatorial explosion", RCRA
QBF-Based Boolean Function Bi-decomposition [arXiv] [ee]
Huan Chen, Mikoláš Janota, Joao Marques-Silva
Design, Automation & Test in Europe Conference & Exhibition (DATE), 2012
PackUp: Tools for Package Upgradability Solving [ee] [tool]
Mikoláš Janota, Inês Lynce, Vasco Manquinho, Joao Marques-Silva
Journal on Satisfiability, Boolean Modeling and Computation, Volume 8, 2012
2011
On Deciding MUS Membership with QBF [bib] [slides] [pdf] [ee]
Mikoláš Janota, Joao Marques-Silva
17th International Conference on Principles and Practice of Constraint Programming (CP'11)
Abstraction-Based Algorithm for 2QBF [ee] [slides] [pdf]
Mikoláš Janota, Joao Marques-Silva
14th International Conference on Theory and Applications of Satisfiability Testing (SAT '11)
cmMUS: A Tool for Circumscription-Based MUS Membership Testing [ee] [pdf] [tool]
Mikoláš Janota, Joao Marques-Silva
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]
Mikoláš Janota, Radu Grigore, Joao Marques-Silva
The 12th European Conference on Logics in Artificial Intelligence (JELIA '10)
On Computing Backbones of Propositional Theories [slides] [bib] [pdf]
Joao Marques-Silva, Mikoláš Janota, and Inês Lynce
The 19th European Conference on Artificial Intelligence (ECAI '10).
How to Complete an Interactive Configuration Process? [slides] [bib] [pdf]
Mikoláš Janota, Goetz Botterweck, Radu Grigore, and Joao Marques-Silva
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]
Mikoláš Janota, Fintan Fairmichael, Viliam Holub, Radu Grigore, Julien Charles, Dermot Cochran, and Joseph Kiniry.
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]
Mikoláš Janota, Victoria Kuzina, and Andrzej Wasowski.
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]
Mikoláš Janota.
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]
Mikoláš Janota and Goetz Botterweck.
Fundamental Approaches to Software Engineering (FASE '08). Budapest, Hungary. April, 2008.
2007
Reachability Analysis for Annotated Code [slides] [pdf]
Mikoláš Janota, Radu Grigore, and Michał Moskal.
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]
Mikoláš Janota, Joseph Kiniry.
The 11th International Software Product Lines Conference (SPLC 2007). Kyoto, Japan. September, 2007.
Assertion-based Loop Invariant Generation [slides] [pdf]
Mikoláš Janota
The 1st International Workshop on Invariant Generation (WING 2007). Hagenberg, Austria. June, 2007.
Software

QESTO, QBF Solver based on clause selection

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]
Mikoláš Janota, Joseph Kiniry, and Goetz Botterweck,
Lero Technical Report, Lero-TR-SPL-2008-02, University of Limerick, May 2008.

Valid XHTML 1.0 Strict VI Improved Last updated: Mar 29, 2016 13:43:15