52 citations · 103 across the 25 of their papers we have counts for
6 papers · 1 filter
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…