Code

PVerifier Backend#803

Code

Closed

FedericoAureliano wants to merge 16 commits intomasterp-org/P:masterfrom experimental/pverifierp-org/P:experimental/pverifierCopy head branch name to clipboard

+4,772-57

Commits

Commits on Nov 28, 2024

• Prototype Support For Verification (#762)

  Show description for 0b6c4b5
  

  3 peoplecommitted
  0b6c4b5

• add install instructions for amazon linux

  FedericoAureliano

  committed
  f28f1ce

• [Feature] prove * using * command for incremental proof construction (#783)

  Show description for 45e4b29
  

  AD1024

  authored and

  FedericoAureliano

  committed
  45e4b29

• add support for foreign functions with contracts and update one tutorial to include an example

  FedericoAureliano

  committed
  8d40993

• allow duplicate invariant names in different groups using group name as prefix

  FedericoAureliano

  committed
  21ea906

• add caching using liteDB and md5 hash of uclid files

  FedericoAureliano

  committed
  4f68d8c

• fix bug in caching by simplifying process checklist

  FedericoAureliano

  committed
  97b0570

• fix bug in global procedures: always prepend self reference

  FedericoAureliano

  committed
  479ed18

• add default that captures P's proof obligations

  FedericoAureliano

  committed
  d62226d

• fix bug in file names

  FedericoAureliano

  committed
  92a01ed

• cleanup example for tutorial

  FedericoAureliano

  committed
  45f5269

• add 2pc verification tutorial

  FedericoAureliano

  committed
  be3227b

• pverifier backend and reorganize verification tutorials

  FedericoAureliano

  committed
  80eed8b

• init keyword -> init-condition keyword

  FedericoAureliano

  committed
  c12d6a7

• add error message when trying to use pverifier syntax for other backends

  FedericoAureliano

  committed
  c26fc9b

• move install instructions to docs and update link in 2pc verification tutorial.

  FedericoAureliano

  committed
  446859b