Home

List of blog posts

Proving Calculational Proofs Correct
Enumerative Data Types with Constraints
Automated Grading of Automata with ACL2s
ACL2s Systems Programming
A Reasoning Engine for the Gamification of Loop-Invariant Discovery
Gamification of Loop-Invariant Discovery from Code

This site was generated using the Zola static site generator. The font used is Crimson Pro, which is licensed under the OFL 1.1. The source files for this website are available on Github. The content of this website is copyright (c) 2023 Andrew T. Walter.