Alcoa: the alloy constraint analyzer (2009)
Daniel Jackson, Ian Schechter, Ilya Shlyakhter
Alcoa is a tool for analyzing object models. It has a range of uses. At one end, it can act as a support tool for object model diagrams, checking for consistency of multiplicities and generating...
MacCallum, Iain, Przybylski, Dariusz, Gnerre, Sante, Burton, Joshua, Shlyakhter, Ilya, Gnirke, Andreas, ...
Abstract We demonstrate that genome sequences approaching finished quality can be generated from short paired reads. Using 36 base (fragment) and 26 base (jumping) reads from five microbial genomes...
Reconstruction of Plausible 3D Tree Models from Instrumented Photographs (2007)
Ilya Shlyakhter, Max Rozenoer, Julie Dorsey, Seth Teller
Computer modeling of vegetation has been a fascinating, interdisciplinary research problem for decades, and a variety of methods for synthesizing models and images of plants have emerged. While...
Using statically computed invariants inside the predicate abstraction and refinement loop (2006)
Himanshu Jain, Franjo Ivančić, Aarti Gupta, Ilya Shlyakhter, Chao Wang
Abstract. Predicate abstraction is a powerful technique for extracting finite-state models from often complex source code. This paper reports on the usage of statically computed invariants inside the...
Model checking C programs using F-Soft (2005)
Franjo Ivančić, Ilya Shlyakhter, Aarti Gupta, Malay K. Ganai, Vineet Kahlon, Chao Wang, ...
Abstract — With the success of formal verification techniques like equivalence checking and model checking for hardware designs, there has been growing interest in applying such techniques for...
Alloy 3.0 Reference Manual (2004)
Daniel Jackson, Include Daniel Jackson, Manu Sridharan, Ilya Shlyakhter, Emina Torlak, Jonathan Edwards, ...
Debugging overconstrained declarative models using unsatisfiable cores (2003)
Ilya Shlyakhter, Robert Seater, Daniel Jackson, Manu Sridharan, Mana Taghdiri
Declarative models, in which conjunction and negation are freely used, are susceptible to unintentional overconstraint. Core extraction is a new analysis that mitigates this problem in the context of...
A Case for Ecient Solution Enumeration (2003)
Sarfraz Khurshid Darko, Darko Marinov, Ilya Shlyakhter, Daniel Jackson
SAT solvers have been ranked primarily by the time they take to find a solution or show that none exists. And indeed, for many problems that are reduced to SAT, finding a single solution is what...
Debugging Overconstrained Declarative Models Using Unsatisfiable Cores (2003)
Ilya Shlyakhter, Robert Seater, Daniel Jackson, Manu Sridharan
Declarative models, in which conjunction and negation are freely used, are susceptible to unintentional overconstraint. Core extraction is a new analysis that mitigates this problem in the context of...
Debugging overconstrained declarative models using unsatisfiable cores (2003)
Ilya Shlyakhter, Manu Sridharan
Declarative models, in which conjunction and negation are freely used, are susceptible to unintentional overconstraint. Core extraction is a new analysis that mitigates this problem in the context of...
A Case for Ecient Solution Enumeration (2003)
Sarfraz Khurshid Darko, Darko Marinov, Ilya Shlyakhter, Daniel Jackson
SAT solvers have been ranked primarily by the time they take to find a solution or show that none exists. And indeed, for many problems that are reduced to SAT, finding a single solution is what...
6.897: Advanced Data Structures Spring 2003 (2003)
Prof Erik, Demaine Scribes, Patrick Lam, Ilya Shlyakhter
In the previous lecture we discussed self-organizing list data structures, static optimality, and the move-to-front (MTF) and frequency-count (FC) algorithms for maintaining a list order which...
A case for efficient solution enumeration (2003)
Sarfraz Khurshid, Darko Marinov, Ilya Shlyakhter, Daniel Jackson
Abstract. SAT solvers have been ranked primarily by the time they take to find a solution or show that none exists. And indeed, for many problems that are reduced to SAT, finding a single solution is...
Exploiting Subformula Sharing in Automatic Analysis of Quantified Formulas (2003)
Ilya Shlyakhter, Manu Sridharan, Robert Seater, Daniel Jackson
Recent advances in SAT solvers have made it attractive to translate a variety of problems to SAT. In many cases, the source language is a logic that includes quanti ers. Grounding out these quanti...
Exploiting subformula sharing in automatic analysis of quantified formulas (2003)
Ilya Shlyakhter, Manu Sridharan, Robert Seater, Daniel Jackson
Constraints with quantifiers can be analyzed in one of two ways: They can be converted to a Quantified Boolean Formula and solved using a QBF solver [5], or the quantifiers can be ground out and the...
Alcoa: the alloy constraint analyzer (2000)
Daniel Jackson, Ian Schechter, Ilya Shlyakhter
Alcoa is a tool for analyzing object models. It has a range of uses. At one end, it can act as a support tool for object model diagrams, checking for consistency of multiplicities and generating...