University of Limerick Institutional Repository

Browsing LERO - Project partner authors by Author "Janota, Mikolas"

DSpace Repository

Browsing LERO - Project partner authors by Author "Janota, Mikolas"

Sort by: Order: Results:

  • Janota, Mikolas (2007)
    Many automated techniques for invariant generation are based on the idea that the invariant should show that something “bad” will not happen in the analyzed program. In this article we present an algorithm for loop invariant ...
  • Janota, Mikolas; Fairmichael, Fintan; Holub, Viliam; Grigore, Radu; Charles, Julien; Cochran, Dermot; Kiniry, Joseph R. (2009)
    Programmers often write custom parsers for the command line input of their programs. They do so, in part, because they believe that both their program’s parameterization and their option formats are simple. But as the ...
  • Janota, Mikolas; Kuzina, Victoria; Wasowski, Andrzej (Association for Computing Machinery, 2008)
    Mainstream development environments have recently assimilated guidance technologies based on constraint satisfaction. We investigate one class of such technologies, namely, interactive guided derivation of models, where ...
  • Belov, Anton; Janota, Mikolas; Lynce, Inês; Marques-Silva, Joao (Springer, 2012)
    A propositional formula in Conjunctive Normal Form (CNF) may contain redundant clauses | clauses whose removal from the for- mula does not a ect the set of its models. Identi cation of redundant clauses is important ...
  • Janota, Mikolas; Lynce, Inês; Manquinho, Vasco; Marques-Silva, Joao (IOS Press, 2012)
    This paper presents PackUp1. (PACKage UPgradability with Boolean formulations) a framework for solving the the software package upgradability problem. Earlier versions of the framework (cudf2msu, cudf2pbo) participated ...
  • Chen, Huan; Janota, Mikolas; Marques-Silva, Joao (IEEE Computer Society, 2012)
    Boolean function bi-decomposition is ubiquitous in logic synthesis. It entails the decomposition of a Boolean function using two-input simple logic gates. Existing solutions for bidecomposition are often based on BDDs ...
  • Janota, Mikolas; Grigore, Radu; Moskal, Michal (Association for Computing Machinery, 2007)
    We devised a reachability analysis that exploits code annotations and implemented it as a component of the extended static checker ESC/Java2. The component reports unchecked code and a class of errors previously undetected. ...
  • Janota, Mikolas; Kiniry, Joseph R. (IEEE Computer Society, 2007)
    A mechanically formalized feature modeling metamodel is presented. This theory is a generic higher-order formalization of a mathematical model synthesizing several feature modeling approaches found in the literature. This ...
  • Janota, Mikolas; Klieber, William; Marques-Silva, Joao; Clarke, Edmund (Springer, 2012)
    We propose two novel approaches for using Counterexample- Guided Abstraction Re nement (CEGAR) in Quanti ed Boolean Formula (QBF) solvers. The rst approach develops a recursive algorithm whose search is driven by CEGAR ...

Search ULIR


Browse

My Account

Statistics