Merge pull request #13 from h0nzZik/symex-3

A specification of symbolic execution and first steps towards an implementation
h0nzZik · Jun 24, 2024 · 3bcc436 · 3bcc436
2 parents 20c27c4 + c995308
commit 3bcc436
Show file tree

Hide file tree

Showing 18 changed files with 5,733 additions and 3,211 deletions.
diff --git a/examples-coq/theories/examples.v b/examples-coq/theories/examples.v
@@ -4,6 +4,7 @@ From stdpp Require Import countable.
 From Minuska Require Import
     prelude
     spec
+    basic_properties
     syntax_properties
     string_variables
     builtins

diff --git a/minuska/_CoqProject b/minuska/_CoqProject
@@ -2,6 +2,7 @@
 
 theories/prelude.v
 theories/spec.v
+theories/basic_properties.v
 theories/lowlang.v
 theories/properties.v
 theories/spec_syntax.v
@@ -31,5 +32,7 @@ theories/interp_loop.v
 theories/example.v
 theories/default_everything.v
 theories/unification_interface.v
+theories/textbook_unification_alg.v
 theories/textbook_unification.v
+theories/symex_spec.v
 theories/symex.v