Home Page of Mikoláš Janota
 |
electronic mail:
mikolas DOT-GOES-HERE janota AT-SIGN-GOES-HERE gmail DOT-GOES-HERE comwork: INESC-ID Lisboa, SAT Group Publications Software Links |
| Google Scholar Profile | DBLP |
|
Solving QBF with Counterexample Guided Refinement
[preprint]
The 15th International Conference on Theory and Applications of Satisfiability Testing (SAT '12), to appear |
|
On Unit-Refutation Complete Formulae with Existentially Quantified Variables
[preprint]
International Conference on Principles of Knowledge Representation and Reasoning (KR), 2012 |
|
QBF-Based Boolean Function Bi-decomposition
[arXiv]
[ee]
Design, Automation & Test in Europe Conference & Exhibition (DATE), 2012 |
|
PackUp: Tools for Package Upgradability Solving
[ee]
Journal on Satisfiability, Boolean Modeling and Computation, Volume 8, 2012 |
|
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) |
|
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). |
|
CLOPS: A DSL for Command Line Options
[slides]
[bib]
[pdf]
IFIP Working Conference on Domain Specific Languages (DSL WC), Oxford, 2009. |
|
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. |
|
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. |
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. |
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
Theses
| SAT Solving in Interactive Configuration
[pdf] PhD Thesis submitted to Department of Computer Science at University College Dublin |
| Automated Theorem Proving and Program Verification
[pdf] MSc Thesis submitted to Department of Theoretical Computer Science and Mathematical Logic at Charles University in Prague |
|
|
|
Last updated: Jan 15, 2012 18:48:16 |