52 citations · 103 across the 25 of their papers we have counts for
19 papers · 1 filter
Proceedings 19th International Workshop on the ACL2 Theorem Prover and Its Applications
Ruben Gamboa, Panagiotis Manolios
The ACL2 Workshop series is the major technical forum for users of the ACL2 theorem proving system to present research related to the ACL2 theorem prover and its applications. ACL2…
Proving Calculational Proofs Correct
Andrew T. Walter, Ankit Kumar, Panagiotis Manolios
Teaching proofs is a crucial component of any undergraduate-level program that covers formal reasoning. We have developed a calculational reasoning format and refined it over sever…
Verification of GossipSub in ACL2s
Ankit Kumar, Max von Hippel, Panagiotis Manolios +1
GossipSub is a popular new peer-to-peer network protocol designed to disseminate messages quickly and efficiently by allowing peers to forward the full content of messages only to…
Using Counterexample Generation and Theory Exploration to Suggest Missing Hypotheses
Ruben Gamboa, Panagiotis Manolios, Eric Smith +1
Newcomers to ACL2 are sometimes surprised that ACL2 rejects formulas that they believe should be theorems, such as (REVERSE (REVERSE X)) = X. Experienced ACL2 users will recognize…
A Case Study in Analytic Protocol Analysis in ACL2
Max von Hippel, Panagiotis Manolios, Kenneth L. McMillan +2
When verifying computer systems we sometimes want to study their asymptotic behaviors, i.e., how they behave in the long run. In such cases, we need real analysis, the area of math…
Calculational Proofs in ACL2s
Andrew T. Walter, Ankit Kumar, Panagiotis Manolios
Teaching college students how to write rigorous proofs is a critical objective in courses that introduce formal reasoning. Over the course of several years, we have developed a mec…
Automated Grading of Automata with ACL2s
Ankit Kumar, Andrew Walter, Panagiotis Manolios
Almost all Computer Science programs require students to take a course on the Theory of Computation (ToC) which covers various models of computation such as finite automata, push-d…
ACL2s Systems Programming
Andrew T. Walter, Panagiotis Manolios
ACL2 provides a systems programming capability that allows one to write code that uses and extends ACL2 inside of ACL2. However, for soundness reasons, ACL2 bars the unrestricted u…
An Efficient Runtime Validation Framework based on the Theory of Refinement
Mitesh Jain, 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 t…
Proving Skipping Refinement with ACL2s
Mitesh Jain, Panagiotis Manolios
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 usin…
Skipping Refinement
Mitesh Jain, Panagiotis Manolios
We introduce skipping refinement, a new notion of correctness for reasoning about optimized reactive systems. Reasoning about reactive systems using refinement involves defining an…
Bug Hunting By Computing Range Reduction
Eugene Goldberg, Panagiotis Manolios
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…
Partial Quantifier Elimination
Eugene Goldberg, Panagiotis Manolios
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 f…
ILP Modulo Data
Panagiotis Manolios, Vasilis Papavasileiou, Mirek Riedewald
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 an…
Verification of Sequential Circuits by Tests-As-Proofs Paradigm
Eugene Goldberg, Mitesh Jain, Panagiotis Manolios
We introduce an algorithm for detection of bugs in sequential circuits. This algorithm is incomplete i.e. its failure to find a bug breaking a property P does not imply that P hold…
ILP Modulo Theories
Panagiotis Manolios, Vasilis Papavasileiou
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…
Checking Satisfiability by Dependency Sequents
Eugene Goldberg, Panagiotis Manolios
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 und…
Removal of Quantifiers by Elimination of Boundary Points
Eugene Goldberg, Panagiotis Manolios
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…
Quantifier Elimination by Dependency Sequents
Eugene Goldberg, Panagiotis Manolios
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 Derivat…