5 citations · 9 across the 9 of their papers we have counts for
6 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…
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…
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…
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…