]>
begriffs open source - acsl-example/log
summary |
shortlog | log |
commit |
commitdiff |
tree
first ⋅ prev ⋅ next
Joe Nelson [Mon, 8 Sep 2025 01:49:48 +0000 (20:49 -0500)]
Incomplete coq proofs from why3
Joe Nelson [Mon, 8 Sep 2025 01:49:05 +0000 (20:49 -0500)]
Double down on coq prover, save session
Joe Nelson [Sun, 7 Sep 2025 05:00:00 +0000 (00:00 -0500)]
Remove ineffective way to work with coq
Joe Nelson [Sun, 7 Sep 2025 05:00:00 +0000 (00:00 -0500)]
More arguments to prove script
Joe Nelson [Sat, 6 Sep 2025 05:00:00 +0000 (00:00 -0500)]
Switch to simple script rather than Meson
Joe Nelson [Sat, 6 Sep 2025 03:54:08 +0000 (22:54 -0500)]
Use coq prover
Joe Nelson [Sat, 6 Sep 2025 02:49:33 +0000 (21:49 -0500)]
Detect goal timeout/failure and switch to alt-ergo prover
Joe Nelson [Fri, 5 Sep 2025 05:00:00 +0000 (00:00 -0500)]
Faster frama-c execution w/ caching
Joe Nelson [Fri, 5 Sep 2025 05:00:00 +0000 (00:00 -0500)]
Remove leftover headers
Joe Nelson [Fri, 5 Sep 2025 05:00:00 +0000 (00:00 -0500)]
Claude guidance for keeping proofs fast
Joe Nelson [Fri, 5 Sep 2025 05:00:00 +0000 (00:00 -0500)]
Don't clutter with timing logs
Joe Nelson [Fri, 5 Sep 2025 05:00:00 +0000 (00:00 -0500)]
Separate proof headers from library headers
Joe Nelson [Fri, 5 Sep 2025 05:00:00 +0000 (00:00 -0500)]
Better organization for fast proofs
Joe Nelson [Fri, 5 Sep 2025 05:00:00 +0000 (00:00 -0500)]
Initial examples from book
begriffs.com / projects / acsl-example / log