# Panagiotis Manolios - Northeastern University

## Contact Details

NamePanagiotis Manolios |
||

AffiliationNortheastern University |
||

CityBoston |
||

CountryUnited States |
||

## Pubs By Year |
||

## Pub CategoriesComputer Science - Logic in Computer Science (13) Computer Science - Programming Languages (3) Computer Science - Software Engineering (2) Computer Science - Discrete Mathematics (2) Computer Science - Artificial Intelligence (1) |

## Publications Authored By Panagiotis Manolios

We introduce a new methodology based on refinement for testing the functional correctness of hardware and low-level software. Our methodology overcomes several major drawbacks of the de facto testing methodologies used in industry: (1) it is difficult to determine completeness of the properties and tests under consideration (2) defining oracles for tests is expensive and error-prone (3) properties are defined in terms of low-level designs. Our approach compiles a formal refinement conjecture into a runtime check that is performed during simulation. Read More

**Affiliations:**

^{1}Northeastern University,

^{2}Northeastern University

We describe three case studies illustrating the use of ACL2s to prove the correctness of optimized reactive systems using skipping refinement. Reasoning about reactive systems using refinement involves defining an abstract, high-level specification system and a concrete, low-level system. Next, one shows that the behaviors of the implementation system are allowed by the specification system. Read More

We introduce skipping refinement, a new notion of correctness for reasoning about optimized reactive systems. Reasoning about reactive systems using refinement involves defining an abstract, high-level specification system and a concrete, low-level implementation system. One then shows that every behavior allowed by the implementation is also allowed by the specification. Read More

We describe a method of model checking called Computing Range Reduction (CRR). The CRR method is based on derivation of clauses that reduce the set of traces of reachable states in such a way that at least one counterexample remains (if any). These clauses are derived by a technique called Partial Quantifier Elimination (PQE). Read More

We consider the problem of Partial Quantifier Elimination (PQE). Given formula exists(X)[F(X,Y) & G(X,Y)], where F, G are in conjunctive normal form, the PQE problem is to find a formula F*(Y) such that F* & exists(X)[G] is logically equivalent to exists(X)[F & G]. We solve the PQE problem by generating and adding to F clauses over the free variables that make the clauses of F with quantified variables redundant. Read More

**Affiliations:**

^{1}Northeastern Univeristy,

^{2}Northeastern Univeristy,

^{3}Northeastern Univeristy

We present a data definition framework that enables the convenient specification of data types in ACL2s, the ACL2 Sedan. Our primary motivation for developing the data definition framework was pedagogical. We were teaching undergraduate students how to reason about programs using ACL2s and wanted to provide them with an effective method for defining, testing, and reasoning about data types in the context of an untyped theorem prover. Read More

The vast quantity of data generated and captured every day has led to a pressing need for tools and processes to organize, analyze and interrelate this data. Automated reasoning and optimization tools with inherent support for data could enable advancements in a variety of contexts, from data-backed decision making to data-intensive scientific research. To this end, we introduce a decidable logic aimed at database analysis. Read More

We introduce an algorithm for detection of bugs in sequential circuits. This algorithm is incomplete i.e. Read More

We present Integer Linear Programming (ILP) Modulo Theories (IMT). An IMT instance is an Integer Linear Programming instance, where some symbols have interpretations in background theories. In previous work, the IMT approach has been applied to industrial synthesis and design problems with real-time constraints arising in the development of the Boeing 787. Read More

We introduce a new algorithm for checking satisfiability based on a calculus of Dependency sequents (D-sequents). Given a CNF formula F(X), a D-sequent is a record stating that under a partial assignment a set of variables of X is redundant in formula \exists{X}[F]. The D-sequent calculus is based on operation join that forms a new D-sequent from two existing D-sequents. Read More

We consider the problem of elimination of existential quantifiers from a Boolean CNF formula. Our approach is based on the following observation. One can get rid of dependency on a set of variables of a quantified CNF formula F by adding resolvent clauses of F eliminating boundary points. Read More

We consider the problem of existential quantifier elimination for Boolean formulas in Conjunctive Normal Form (CNF). We present a new method for solving this problem called Derivation of Dependency-Sequents (DDS). A Dependency-sequent (D-sequent) is used to record that a set of quantified variables is redundant under a partial assignment. Read More

**Authors:**Harsh Raju Chamarthi

^{1}, Peter C. Dillinger

^{2}, Matt Kaufmann

^{3}, Panagiotis Manolios

^{4}

**Affiliations:**

^{1}Northeastern University,

^{2}Northeastern University,

^{3}University of Texas at Austin,

^{4}Northeastern University

Using an interactive theorem prover to reason about programs involves a sequence of interactions where the user challenges the theorem prover with conjectures. Invariably, many of the conjectures posed are in fact false, and users often spend considerable effort examining the theorem prover's output before realizing this. We present a synergistic integration of testing with theorem proving, implemented in the ACL2 Sedan (ACL2s), for automatically generating concrete counterexamples. Read More