Commits · b74ef8d3b4bf2e215f1e3fedbb53b353bbaaa213 · POLLIEN Baptiste / VFPG

Jan 25, 2023
- Add LICENSE · b74ef8d3
  POLLIEN Baptiste authored 2 years ago
  
  b74ef8d3
- Changing determinate -> deterministic · 8d824f96
  POLLIEN Baptiste authored 2 years ago
  
  8d824f96
Jan 24, 2023
- Update names · ad8db6c2
  POLLIEN Baptiste authored 2 years ago
  
  ad8db6c2
Jan 20, 2023
- [doc] minor changes · 390e8bcc
  POLLIEN Baptiste authored 2 years ago
  
  390e8bcc
Jan 06, 2023
- Separation of trace and state in fp_env · e7a4cd5c
  POLLIEN Baptiste authored 2 years ago
  
  e7a4cd5c
Jan 04, 2023
- Adding a Bisimulation property · 709bce00
  POLLIEN Baptiste authored 2 years ago
  
  709bce00
Dec 27, 2022
- Proving that Clight step is determinate · 1df7e900
  POLLIEN Baptiste authored 2 years ago
  
  1df7e900
Dec 15, 2022
- Change equiv into match · 1fc012b9
  POLLIEN Baptiste authored 2 years ago
  
  1fc012b9
Dec 14, 2022
- Merge branch 'dev' · 40a7c6e4
  POLLIEN Baptiste authored 2 years ago
  
  40a7c6e4
- Adding a specific arbitrary parsing function · db193fb5
  POLLIEN Baptiste authored 2 years ago
  
  db193fb5
- Merge branch 'dev' · f32f4273
  POLLIEN Baptiste authored 2 years ago
  
  f32f4273
- Adding a specific arbitrary parsing function · fa4710fd
  POLLIEN Baptiste authored 2 years ago
  
  fa4710fd
- Adding a specific arbitrary parsing function · 4a90513d
  POLLIEN Baptiste authored 2 years ago
  
  4a90513d
- Adding a specific arbitrary parsing function · 4202c797
  POLLIEN Baptiste authored 2 years ago
  
  4202c797
- Update Readme and documentation · 88c6e1d7
  POLLIEN Baptiste authored 2 years ago
  
  88c6e1d7
Dec 13, 2022
- Fix extraction, Update compcert and Documentation · 284ab9dd
  POLLIEN Baptiste authored 2 years ago
```
UPdate
```
  284ab9dd
Dec 12, 2022
- Taking GVARS into account for the verification of the semantics preservation · 918b9f85
  POLLIEN Baptiste authored 2 years ago
  
  918b9f85
- Adding CENV with trace in axioms · a95f23df
  POLLIEN Baptiste authored 2 years ago
  
  a95f23df
Dec 05, 2022
- Proof of size_verification_unchange_fp · e1a3cc21
  POLLIEN Baptiste authored 2 years ago
  
  e1a3cc21
Dec 04, 2022
- Remove drop_m and take_m · 0dc10dc2
  POLLIEN Baptiste authored 2 years ago
  
  0dc10dc2
Dec 02, 2022
- Remove proj1_sig · 5e31bbd1
  POLLIEN Baptiste authored 2 years ago
  
  5e31bbd1
- Adding a patch for compcert · 135e3e13
  POLLIEN Baptiste authored 2 years ago
  
  135e3e13
Dec 01, 2022
- Major refactor of modules and add global forward simulation proof (FP -> C) · 0bb88551
  POLLIEN Baptiste authored 2 years ago
  
  0bb88551
Nov 30, 2022
- Remove TODO · c17b797c
  POLLIEN Baptiste authored 2 years ago
  
  c17b797c
- Fix tests · d0242a27
  POLLIEN Baptiste authored 2 years ago
  
  d0242a27
Nov 29, 2022
- Replace assert with have · 1bd623d2
  POLLIEN Baptiste authored 2 years ago
  
  1bd623d2
- Add a init block to execute on_enter for the first block · 1005e21c
  POLLIEN Baptiste authored 2 years ago
  
  1005e21c
- Compatible with coq 8.16 · 1e3b0a0a
  POLLIEN Baptiste authored 2 years ago
  
  1e3b0a0a
- Add a module to regroup trace_appended definitions · 94c3abd1
  POLLIEN Baptiste authored 2 years ago
  
  94c3abd1
- Create a generic structure for the semantics of FP, FPE, FPS and Clight · a269186c
  POLLIEN Baptiste authored 2 years ago
  
  a269186c
Nov 23, 2022
- Update the semantics and definition of the env using trace instead of time · acc1d7dd
  POLLIEN Baptiste authored 2 years ago
  
  acc1d7dd
Nov 14, 2022
- Remove check · 29f22183
  POLLIEN Baptiste authored 2 years ago
  
  29f22183
- Improve Init proof · cd57829f
  POLLIEN Baptiste authored 2 years ago
  
  cd57829f
Nov 10, 2022
- Proof of the init state · 2bcf0be3
  POLLIEN Baptiste authored 2 years ago
  
  2bcf0be3
- Update the generator with the new features of paparazzi · fa3db1f0
  POLLIEN Baptiste authored 2 years ago
  
  fa3db1f0
- Update TODO · c28bee3a
  POLLIEN Baptiste authored 2 years ago
  
  c28bee3a
Nov 08, 2022
- Proof of string lemmas · a2e99c1d
  POLLIEN Baptiste authored 2 years ago
  
  a2e99c1d
- End of FPSizeVerification · 77c03b42
  POLLIEN Baptiste authored 2 years ago
  
  77c03b42
Nov 07, 2022
- Major update for FPSize verification · 49658101
  POLLIEN Baptiste authored 2 years ago
  
  49658101
- End of FP Big step size · ddd4ffde
  POLLIEN Baptiste authored 2 years ago
  
  ddd4ffde